Theorem imonclem 10732

Description: Lemma for ismonc 10733.

Hypotheses

Ref	Expression
imonclem.1	|- O = dom (id` T)
imonclem.2	|- H = (hom` T)
imonclem.3	|- R = (o` T)

Assertion

Ref	Expression
imonclem	|- ((T e. Cat /\ (B e. O /\ C e. O) /\ F e. (H` <.B, C>.)) -> (A.a e. O A.g e. (H` <.a, B>.)A.h e. (H` <.a, B>.)((FRg) = (FRh) -> g = h) -> (F e. dom (dom` T) /\ A.g e. dom (dom` T)A.h e. dom (dom` T)((((dom` T)` g) = ((dom` T)` h) /\ ((cod` T)` g) = ((dom` T)` F) /\ ((cod` T)` h) = ((dom` T)` F)) -> ((FRg) = (FRh) -> g = h)))))

Distinct variable groups:   B,a,g,h   C,a,g,h   F,a,g,h   H,a,g,h   O,a,g,h   R,a   T,a,g,h

Proof of Theorem imonclem

Step	Hyp	Ref	Expression
1		imonclem.1	. . . . . . 7 |- O = dom (id` T)
2		eqid 1479	. . . . . . 7 |- dom (dom` T) = dom (dom` T)
3		imonclem.2	. . . . . . 7 |- H = (hom` T)
4	1, 2, 3	ehm 10710	. . . . . 6 |- ((T e. Cat /\ B e. O /\ C e. O) -> (F e. (H` <.B, C>.) -> F e. dom (dom` T)))
5	4	3expib 839	. . . . 5 |- (T e. Cat -> ((B e. O /\ C e. O) -> (F e. (H` <.B, C>.) -> F e. dom (dom` T))))
6	5	3imp 830	. . . 4 |- ((T e. Cat /\ (B e. O /\ C e. O) /\ F e. (H` <.B, C>.)) -> F e. dom (dom` T))
7	6	adantr 391	. . 3 |- (((T e. Cat /\ (B e. O /\ C e. O) /\ F e. (H` <.B, C>.)) /\ A.a e. O A.g e. (H` <.a, B>.)A.h e. (H` <.a, B>.)((FRg) = (FRh) -> g = h)) -> F e. dom (dom` T))
8		ax-17 974	. . . . . 6 |- ((T e. Cat /\ (B e. O /\ C e. O) /\ F e. (H` <.B, C>.)) -> A.g(T e. Cat /\ (B e. O /\ C e. O) /\ F e. (H` <.B, C>.)))
9		ax-17 974	. . . . . . 7 |- (a e. O -> A.g a e. O)
10		hbra1 1691	. . . . . . 7 |- (A.g e. (H` <.a, B>.)A.h e. (H` <.a, B>.)((FRg) = (FRh) -> g = h) -> A.gA.g e. (H` <.a, B>.)A.h e. (H` <.a, B>.)((FRg) = (FRh) -> g = h))
11	9, 10	hbral 1690	. . . . . 6 |- (A.a e. O A.g e. (H` <.a, B>.)A.h e. (H` <.a, B>.)((FRg) = (FRh) -> g = h) -> A.gA.a e. O A.g e. (H` <.a, B>.)A.h e. (H` <.a, B>.)((FRg) = (FRh) -> g = h))
12	8, 11	hban 1012	. . . . 5 |- (((T e. Cat /\ (B e. O /\ C e. O) /\ F e. (H` <.B, C>.)) /\ A.a e. O A.g e. (H` <.a, B>.)A.h e. (H` <.a, B>.)((FRg) = (FRh) -> g = h)) -> A.g((T e. Cat /\ (B e. O /\ C e. O) /\ F e. (H` <.B, C>.)) /\ A.a e. O A.g e. (H` <.a, B>.)A.h e. (H` <.a, B>.)((FRg) = (FRh) -> g = h)))
13		ax-17 974	. . . . . . 7 |- ((T e. Cat /\ (B e. O /\ C e. O) /\ F e. (H` <.B, C>.)) -> A.h(T e. Cat /\ (B e. O /\ C e. O) /\ F e. (H` <.B, C>.)))
14		ax-17 974	. . . . . . . 8 |- (a e. O -> A.h a e. O)
15		ax-17 974	. . . . . . . . 9 |- (g e. (H` <.a, B>.) -> A.h g e. (H` <.a, B>.))
16		hbra1 1691	. . . . . . . . 9 |- (A.h e. (H` <.a, B>.)((FRg) = (FRh) -> g = h) -> A.hA.h e. (H` <.a, B>.)((FRg) = (FRh) -> g = h))
17	15, 16	hbral 1690	. . . . . . . 8 |- (A.g e. (H` <.a, B>.)A.h e. (H` <.a, B>.)((FRg) = (FRh) -> g = h) -> A.hA.g e. (H` <.a, B>.)A.h e. (H` <.a, B>.)((FRg) = (FRh) -> g = h))
18	14, 17	hbral 1690	. . . . . . 7 |- (A.a e. O A.g e. (H` <.a, B>.)A.h e. (H` <.a, B>.)((FRg) = (FRh) -> g = h) -> A.hA.a e. O A.g e. (H` <.a, B>.)A.h e. (H` <.a, B>.)((FRg) = (FRh) -> g = h))
19	13, 18	hban 1012	. . . . . 6 |- (((T e. Cat /\ (B e. O /\ C e. O) /\ F e. (H` <.B, C>.)) /\ A.a e. O A.g e. (H` <.a, B>.)A.h e. (H` <.a, B>.)((FRg) = (FRh) -> g = h)) -> A.h((T e. Cat /\ (B e. O /\ C e. O) /\ F e. (H` <.B, C>.)) /\ A.a e. O A.g e. (H` <.a, B>.)A.h e. (H` <.a, B>.)((FRg) = (FRh) -> g = h)))
20		3simp1 791	. . . . . . . . . . 11 |- ((T e. Cat /\ (B e. O /\ C e. O) /\ F e. (H` <.B, C>.)) -> T e. Cat)
21		eqid 1479	. . . . . . . . . . . . . 14 |- (dom` T) = (dom` T)
22	2, 1, 21	dmo 10700	. . . . . . . . . . . . 13 |- ((T e. Cat /\ g e. dom (dom` T)) -> ((dom` T)` g) e. O)
23	22	expcom 374	. . . . . . . . . . . 12 |- (g e. dom (dom` T) -> (T e. Cat -> ((dom` T)` g) e. O))
24	23	adantr 391	. . . . . . . . . . 11 |- ((g e. dom (dom` T) /\ h e. dom (dom` T)) -> (T e. Cat -> ((dom` T)` g) e. O))
25	20, 24	mpan9 472	. . . . . . . . . 10 |- (((T e. Cat /\ (B e. O /\ C e. O) /\ F e. (H` <.B, C>.)) /\ (g e. dom (dom` T) /\ h e. dom (dom` T))) -> ((dom` T)` g) e. O)
26		r2al 1680	. . . . . . . . . . . . 13 |- (A.g e. (H` <.a, B>.)A.h e. (H` <.a, B>.)((FRg) = (FRh) -> g = h) <-> A.gA.h((g e. (H` <.a, B>.) /\ h e. (H` <.a, B>.)) -> ((FRg) = (FRh) -> g = h)))
27	26	ralbii 1671	. . . . . . . . . . . 12 |- (A.a e. O A.g e. (H` <.a, B>.)A.h e. (H` <.a, B>.)((FRg) = (FRh) -> g = h) <-> A.a e. O A.gA.h((g e. (H` <.a, B>.) /\ h e. (H` <.a, B>.)) -> ((FRg) = (FRh) -> g = h)))
28		opeq1 2494	. . . . . . . . . . . . . . . . . . . 20 |- (a = ((dom` T)` g) -> <.a, B>. = <.((dom` T)` g), B>.)
29	28	fveq2d 3737	. . . . . . . . . . . . . . . . . . 19 |- (a = ((dom` T)` g) -> (H` <.a, B>.) = (H` <.((dom` T)` g), B>.))
30	29	eleq2d 1545	. . . . . . . . . . . . . . . . . 18 |- (a = ((dom` T)` g) -> (g e. (H` <.a, B>.) <-> g e. (H` <.((dom` T)` g), B>.)))
31	29	eleq2d 1545	. . . . . . . . . . . . . . . . . 18 |- (a = ((dom` T)` g) -> (h e. (H` <.a, B>.) <-> h e. (H` <.((dom` T)` g), B>.)))
32	30, 31	anbi12d 630	. . . . . . . . . . . . . . . . 17 |- (a = ((dom` T)` g) -> ((g e. (H` <.a, B>.) /\ h e. (H` <.a, B>.)) <-> (g e. (H` <.((dom` T)` g), B>.) /\ h e. (H` <.((dom` T)` g), B>.))))
33	32	imbi1d 615	. . . . . . . . . . . . . . . 16 |- (a = ((dom` T)` g) -> (((g e. (H` <.a, B>.) /\ h e. (H` <.a, B>.)) -> ((FRg) = (FRh) -> g = h)) <-> ((g e. (H` <.((dom` T)` g), B>.) /\ h e. (H` <.((dom` T)` g), B>.)) -> ((FRg) = (FRh