Theorem initoeu2lem0

Description: Lemma 0 for initoeu2 . (Contributed by AV, 9-Apr-2020)

	Ref	Expression
Hypotheses	initoeu1.c	$$⊢\phi \to C\in \mathrm{Cat}$$
	initoeu1.a	$$⊢\phi \to A\in \mathrm{InitO}\left(C\right)$$
	initoeu2lem.x	$$⊢X={\mathrm{Base}}_C$$
	initoeu2lem.h	$$⊢H=\mathrm{Hom}\left(C\right)$$
	initoeu2lem.i	$$⊢I=\mathrm{Iso}\left(C\right)$$
	initoeu2lem.o	No typesetting found for |- .o. = ( comp ` C ) with typecode |-
Assertion	initoeu2lem0	Could not format assertion : No typesetting found for |- ( ( ( ph /\ ( A e. X /\ B e. X /\ D e. X ) ) /\ ( K e. ( B I A ) /\ F e. ( A H D ) /\ G e. ( B H D ) ) /\ ( ( F ( <. B , A >. .o. D ) K ) ( <. A , B >. .o. D ) ( ( B ( Inv ` C ) A ) ` K ) ) = ( G ( <. A , B >. .o. D ) ( ( B ( Inv ` C ) A ) ` K ) ) ) -> G = ( F ( <. B , A >. .o. D ) K ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		initoeu1.c	$$⊢\phi \to C\in \mathrm{Cat}$$
2		initoeu1.a	$$⊢\phi \to A\in \mathrm{InitO}\left(C\right)$$
3		initoeu2lem.x	$$⊢X={\mathrm{Base}}_C$$
4		initoeu2lem.h	$$⊢H=\mathrm{Hom}\left(C\right)$$
5		initoeu2lem.i	$$⊢I=\mathrm{Iso}\left(C\right)$$
6		initoeu2lem.o	Could not format .o. = ( comp ` C ) : No typesetting found for |- .o. = ( comp ` C ) with typecode |-
7		3simpa	Could not format ( ( ( ph /\ ( A e. X /\ B e. X /\ D e. X ) ) /\ ( K e. ( B I A ) /\ F e. ( A H D ) /\ G e. ( B H D ) ) /\ ( ( F ( <. B , A >. .o. D ) K ) ( <. A , B >. .o. D ) ( ( B ( Inv ` C ) A ) ` K ) ) = ( G ( <. A , B >. .o. D ) ( ( B ( Inv ` C ) A ) ` K ) ) ) -> ( ( ph /\ ( A e. X /\ B e. X /\ D e. X ) ) /\ ( K e. ( B I A ) /\ F e. ( A H D ) /\ G e. ( B H D ) ) ) ) : No typesetting found for |- ( ( ( ph /\ ( A e. X /\ B e. X /\ D e. X ) ) /\ ( K e. ( B I A ) /\ F e. ( A H D ) /\ G e. ( B H D ) ) /\ ( ( F ( <. B , A >. .o. D ) K ) ( <. A , B >. .o. D ) ( ( B ( Inv ` C ) A ) ` K ) ) = ( G ( <. A , B >. .o. D ) ( ( B ( Inv ` C ) A ) ` K ) ) ) -> ( ( ph /\ ( A e. X /\ B e. X /\ D e. X ) ) /\ ( K e. ( B I A ) /\ F e. ( A H D ) /\ G e. ( B H D ) ) ) ) with typecode |-
8		simp3	Could not format ( ( ( ph /\ ( A e. X /\ B e. X /\ D e. X ) ) /\ ( K e. ( B I A ) /\ F e. ( A H D ) /\ G e. ( B H D ) ) /\ ( ( F ( <. B , A >. .o. D ) K ) ( <. A , B >. .o. D ) ( ( B ( Inv ` C ) A ) ` K ) ) = ( G ( <. A , B >. .o. D ) ( ( B ( Inv ` C ) A ) ` K ) ) ) -> ( ( F ( <. B , A >. .o. D ) K ) ( <. A , B >. .o. D ) ( ( B ( Inv ` C ) A ) ` K ) ) = ( G ( <. A , B >. .o. D ) ( ( B ( Inv ` C ) A ) ` K ) ) ) : No typesetting found for |- ( ( ( ph /\ ( A e. X /\ B e. X /\ D e. X ) ) /\ ( K e. ( B I A ) /\ F e. ( A H D ) /\ G e. ( B H D ) ) /\ ( ( F ( <. B , A >. .o. D ) K ) ( <. A , B >. .o. D ) ( ( B ( Inv ` C ) A ) ` K ) ) = ( G ( <. A , B >. .o. D ) ( ( B ( Inv ` C ) A ) ` K ) ) ) -> ( ( F ( <. B , A >. .o. D ) K ) ( <. A , B >. .o. D ) ( ( B ( Inv ` C ) A ) ` K ) ) = ( G ( <. A , B >. .o. D ) ( ( B ( Inv ` C ) A ) ` K ) ) ) with typecode |-
9	8	eqcomd	Could not format ( ( ( ph /\ ( A e. X /\ B e. X /\ D e. X ) ) /\ ( K e. ( B I A ) /\ F e. ( A H D ) /\ G e. ( B H D ) ) /\ ( ( F ( <. B , A >. .o. D ) K ) ( <. A , B >. .o. D ) ( ( B ( Inv ` C ) A ) ` K ) ) = ( G ( <. A , B >. .o. D ) ( ( B ( Inv ` C ) A ) ` K ) ) ) -> ( G ( <. A , B >. .o. D ) ( ( B ( Inv ` C ) A ) ` K ) ) = ( ( F ( <. B , A >. .o. D ) K ) ( <. A , B >. .o. D ) ( ( B ( Inv ` C ) A ) ` K ) ) ) : No typesetting found for |- ( ( ( ph /\ ( A e. X /\ B e. X /\ D e. X ) ) /\ ( K e. ( B I A ) /\ F e. ( A H D ) /\ G e. ( B H D ) ) /\ ( ( F ( <. B , A >. .o. D ) K ) ( <. A , B >. .o. D ) ( ( B ( Inv ` C ) A ) ` K ) ) = ( G ( <. A , B >. .o. D ) ( ( B ( Inv ` C ) A ) ` K ) ) ) -> ( G ( <. A , B >. .o. D ) ( ( B ( Inv ` C ) A ) ` K ) ) = ( ( F ( <. B , A >. .o. D ) K ) ( <. A , B >. .o. D ) ( ( B ( Inv ` C ) A ) ` K ) ) ) with typecode |-
10		eqid	$$⊢\mathrm{Inv}\left(C\right)=\mathrm{Inv}\left(C\right)$$
11	1	adantr	$$⊢\left(\phi \wedge \left(A\in X\wedge B\in X\wedge D\in X\right)\right)\to C\in \mathrm{Cat}$$
12	11	adantr	$$⊢\left(\left(\phi \wedge \left(A\in X\wedge B\in X\wedge D\in X\right)\right)\wedge \left(K\in \left(BIA\right)\wedge F\in \left(AHD\right)\wedge G\in \left(BHD\right)\right)\right)\to C\in \mathrm{Cat}$$
13		simpr1	$$⊢\left(\phi \wedge \left(A\in X\wedge B\in X\wedge D\in X\right)\right)\to A\in X$$
14	13	adantr	$$⊢\left(\left(\phi \wedge \left(A\in X\wedge B\in X\wedge D\in X\right)\right)\wedge \left(K\in \left(BIA\right)\wedge F\in \left(AHD\right)\wedge G\in \left(BHD\right)\right)\right)\to A\in X$$
15		simpr2	$$⊢\left(\phi \wedge \left(A\in X\wedge B\in X\wedge D\in X\right)\right)\to B\in X$$
16	15	adantr	$$⊢\left(\left(\phi \wedge \left(A\in X\wedge B\in X\wedge D\in X\right)\right)\wedge \left(K\in \left(BIA\right)\wedge F\in \left(AHD\right)\wedge G\in \left(BHD\right)\right)\right)\to B\in X$$
17		simplr3	$$⊢\left(\left(\phi \wedge \left(A\in X\wedge B\in X\wedge D\in X\right)\right)\wedge \left(K\in \left(BIA\right)\wedge F\in \left(AHD\right)\wedge G\in \left(BHD\right)\right)\right)\to D\in X$$
18	5	oveqi	$$⊢BIA=B\mathrm{Iso}\left(C\right)A$$
19	18	eleq2i	$$⊢K\in \left(BIA\right)\leftrightarrow K\in \left(B\mathrm{Iso}\left(C\right)A\right)$$
20	19	biimpi	$$⊢K\in \left(BIA\right)\to K\in \left(B\mathrm{Iso}\left(C\right)A\right)$$
21	20	3ad2ant1	$$⊢\left(K\in \left(BIA\right)\wedge F\in \left(AHD\right)\wedge G\in \left(BHD\right)\right)\to K\in \left(B\mathrm{Iso}\left(C\right)A\right)$$
22	21	adantl	$$⊢\left(\left(\phi \wedge \left(A\in X\wedge B\in X\wedge D\in X\right)\right)\wedge \left(K\in \left(BIA\right)\wedge F\in \left(AHD\right)\wedge G\in \left(BHD\right)\right)\right)\to K\in \left(B\mathrm{Iso}\left(C\right)A\right)$$
23	4	oveqi	$$⊢BHD=B\mathrm{Hom}\left(C\right)D$$
24	23	eleq2i	$$⊢G\in \left(BHD\right)\leftrightarrow G\in \left(B\mathrm{Hom}\left(C\right)D\right)$$
25	24	biimpi	$$⊢G\in \left(BHD\right)\to G\in \left(B\mathrm{Hom}\left(C\right)D\right)$$
26	25	3ad2ant3	$$⊢\left(K\in \left(BIA\right)\wedge F\in \left(AHD\right)\wedge G\in \left(BHD\right)\right)\to G\in \left(B\mathrm{Hom}\left(C\right)D\right)$$
27	26	adantl	$$⊢\left(\left(\phi \wedge \left(A\in X\wedge B\in X\wedge D\in X\right)\right)\wedge \left(K\in \left(BIA\right)\wedge F\in \left(AHD\right)\wedge G\in \left(BHD\right)\right)\right)\to G\in \left(B\mathrm{Hom}\left(C\right)D\right)$$
28		eqid	$$⊢\mathrm{Hom}\left(C\right)=\mathrm{Hom}\left(C\right)$$
29	3 28 5 11 15 13	isohom	$$⊢\left(\phi \wedge \left(A\in X\wedge B\in X\wedge D\in X\right)\right)\to BIA\subseteq B\mathrm{Hom}\left(C\right)A$$
30	29	sseld	$$⊢\left(\phi \wedge \left(A\in X\wedge B\in X\wedge D\in X\right)\right)\to \left(K\in \left(BIA\right)\to K\in \left(B\mathrm{Hom}\left(C\right)A\right)\right)$$
31	30	com12	$$⊢K\in \left(BIA\right)\to \left(\left(\phi \wedge \left(A\in X\wedge B\in X\wedge D\in X\right)\right)\to K\in \left(B\mathrm{Hom}\left(C\right)A\right)\right)$$
32	31	3ad2ant1	$$⊢\left(K\in \left(BIA\right)\wedge F\in \left(AHD\right)\wedge G\in \left(BHD\right)\right)\to \left(\left(\phi \wedge \left(A\in X\wedge B\in X\wedge D\in X\right)\right)\to K\in \left(B\mathrm{Hom}\left(C\right)A\right)\right)$$
33	32	impcom	$$⊢\left(\left(\phi \wedge \left(A\in X\wedge B\in X\wedge D\in X\right)\right)\wedge \left(K\in \left(BIA\right)\wedge F\in \left(AHD\right)\wedge G\in \left(BHD\right)\right)\right)\to K\in \left(B\mathrm{Hom}\left(C\right)A\right)$$
34	4	oveqi	$$⊢AHD=A\mathrm{Hom}\left(C\right)D$$
35	34	eleq2i	$$⊢F\in \left(AHD\right)\leftrightarrow F\in \left(A\mathrm{Hom}\left(C\right)D\right)$$
36	35	biimpi	$$⊢F\in \left(AHD\right)\to F\in \left(A\mathrm{Hom}\left(C\right)D\right)$$
37	36	3ad2ant2	$$⊢\left(K\in \left(BIA\right)\wedge F\in \left(AHD\right)\wedge G\in \left(BHD\right)\right)\to F\in \left(A\mathrm{Hom}\left(C\right)D\right)$$
38	37	adantl	$$⊢\left(\left(\phi \wedge \left(A\in X\wedge B\in X\wedge D\in X\right)\right)\wedge \left(K\in \left(BIA\right)\wedge F\in \left(AHD\right)\wedge G\in \left(BHD\right)\right)\right)\to F\in \left(A\mathrm{Hom}\left(C\right)D\right)$$
39	3 28 6 12 16 14 17 33 38	catcocl	Could not format ( ( ( ph /\ ( A e. X /\ B e. X /\ D e. X ) ) /\ ( K e. ( B I A ) /\ F e. ( A H D ) /\ G e. ( B H D ) ) ) -> ( F ( <. B , A >. .o. D ) K ) e. ( B ( Hom ` C ) D ) ) : No typesetting found for |- ( ( ( ph /\ ( A e. X /\ B e. X /\ D e. X ) ) /\ ( K e. ( B I A ) /\ F e. ( A H D ) /\ G e. ( B H D ) ) ) -> ( F ( <. B , A >. .o. D ) K ) e. ( B ( Hom ` C ) D ) ) with typecode |-
40		eqid	$$⊢\left(B\mathrm{Inv}\left(C\right)A\right)\left(K\right)=\left(B\mathrm{Inv}\left(C\right)A\right)\left(K\right)$$
41	6	oveqi	Could not format ( <. A , B >. .o. D ) = ( <. A , B >. ( comp ` C ) D ) : No typesetting found for |- ( <. A , B >. .o. D ) = ( <. A , B >. ( comp ` C ) D ) with typecode |-
42	3 10 12 14 16 17 22 27 39 40 41	rcaninv	Could not format ( ( ( ph /\ ( A e. X /\ B e. X /\ D e. X ) ) /\ ( K e. ( B I A ) /\ F e. ( A H D ) /\ G e. ( B H D ) ) ) -> ( ( G ( <. A , B >. .o. D ) ( ( B ( Inv ` C ) A ) ` K ) ) = ( ( F ( <. B , A >. .o. D ) K ) ( <. A , B >. .o. D ) ( ( B ( Inv ` C ) A ) ` K ) ) -> G = ( F ( <. B , A >. .o. D ) K ) ) ) : No typesetting found for |- ( ( ( ph /\ ( A e. X /\ B e. X /\ D e. X ) ) /\ ( K e. ( B I A ) /\ F e. ( A H D ) /\ G e. ( B H D ) ) ) -> ( ( G ( <. A , B >. .o. D ) ( ( B ( Inv ` C ) A ) ` K ) ) = ( ( F ( <. B , A >. .o. D ) K ) ( <. A , B >. .o. D ) ( ( B ( Inv ` C ) A ) ` K ) ) -> G = ( F ( <. B , A >. .o. D ) K ) ) ) with typecode |-
43	7 9 42	sylc	Could not format ( ( ( ph /\ ( A e. X /\ B e. X /\ D e. X ) ) /\ ( K e. ( B I A ) /\ F e. ( A H D ) /\ G e. ( B H D ) ) /\ ( ( F ( <. B , A >. .o. D ) K ) ( <. A , B >. .o. D ) ( ( B ( Inv ` C ) A ) ` K ) ) = ( G ( <. A , B >. .o. D ) ( ( B ( Inv ` C ) A ) ` K ) ) ) -> G = ( F ( <. B , A >. .o. D ) K ) ) : No typesetting found for |- ( ( ( ph /\ ( A e. X /\ B e. X /\ D e. X ) ) /\ ( K e. ( B I A ) /\ F e. ( A H D ) /\ G e. ( B H D ) ) /\ ( ( F ( <. B , A >. .o. D ) K ) ( <. A , B >. .o. D ) ( ( B ( Inv ` C ) A ) ` K ) ) = ( G ( <. A , B >. .o. D ) ( ( B ( Inv ` C ) A ) ` K ) ) ) -> G = ( F ( <. B , A >. .o. D ) K ) ) with typecode |-