Theorem imonclem 10619

Description: Lemma for ismonc 10620.

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 1473	. . . . . . 7 |- dom (dom` T) = dom (dom` T)
3		imonclem.2	. . . . . . 7 |- H = (hom` T)
4	1, 2, 3	ehm 10599	. . . . . 6 |- ((T e. Cat /\ B e. O /\ C e. O) -> (F e. (H` <.B, C>.) -> F e. dom (dom` T)))
5	4	3expib 835	. . . . 5 |- (T e. Cat -> ((B e. O /\ C e. O) -> (F e. (H` <.B, C>.) -> F e. dom (dom` T))))
6	5	3imp 826	. . . 4 |- ((T e. Cat /\ (B e. O /\ C e. O) /\ F e. (H` <.B, C>.)) -> F e. dom (dom` T))
7	6	adantr 389	. . 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 969	. . . . . 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 969	. . . . . . 7 |- (a e. O -> A.g a e. O)
10		hbra1 1684	. . . . . . 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 1683	. . . . . 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 1007	. . . . 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 969	. . . . . . 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 969	. . . . . . . 8 |- (a e. O -> A.h a e. O)
15		ax-17 969	. . . . . . . . 9 |- (g e. (H` <.a, B>.) -> A.h g e. (H` <.a, B>.))
16		hbra1 1684	. . . . . . . . 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 1683	. . . . . . . 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 1683	. . . . . . 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 1007	. . . . . 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		eqid 1473	. . . . . . . . . . . . . . 15 |- (dom` T) = (dom` T)
21	2, 1, 20	dmo 10589	. . . . . . . . . . . . . 14 |- ((T e. Cat /\ g e. dom (dom` T)) -> ((dom` T)` g) e. O)
22	21	expcom 374	. . . . . . . . . . . . 13 |- (g e. dom (dom` T) -> (T e. Cat -> ((dom` T)` g) e. O))
23	22	adantr 389	. . . . . . . . . . . 12 |- ((g e. dom (dom` T) /\ h e. dom (dom` T)) -> (T e. Cat -> ((dom` T)` g) e. O))
24		3simp1 787	. . . . . . . . . . . 12 |- ((T e. Cat /\ (B e. O /\ C e. O) /\ F e. (H` <.B, C>.)) -> T e. Cat)
25	23, 24	syl5com 52	. . . . . . . . . . 11 |- ((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	25	imp 350	. . . . . . . . . 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)
27		r2al 1673	. . . . . . . . . . . . 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)))
28	27	ralbii 1664	. . . . . . . . . . . 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)))
29		opeq1 2483	. . . . . . . . . . . . . . . . . . . 20 |- (a = ((dom` T)` g) -> <.a, B>. = <.((dom` T)` g), B>.)
30	29	fveq2d 3719	. . . . . . . . . . . . . . . . . . 19 |- (a = ((dom` T)` g) -> (H` <.a, B>.) = (H` <.((dom` T)` g), B>.))
31	30	eleq2d 1538	. . . . . . . . . . . . . . . . . 18 |- (a = ((dom` T)` g) -> (g e. (H` <.a, B>.) <-> g e. (H` <.((dom` T)` g), B>.)))
32	30	eleq2d 1538	. . . . . . . . . . . . . . . . . 18 |- (a = ((dom` T)` g) -> (h e. (H` <.a, B>.) <-> h e. (H` <.((dom` T)` g), B>.)))
33	31, 32	anbi12d 627	. . . . . . . . . . . . . . . . 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>.))))
34	33	imbi1d 612	. . . . . . . . . . . . . . . 16 |- (a = ((dom` T)` g) -> (((g e. (H` <.a, B>.) /\ h e. (H` <.a, B>.)) -> ((FRg)