initoeu2lem0

	Ref	Expression
Hypotheses	initoeu1.c	$⊢ φ \to C \in Cat$
	initoeu1.a	$⊢ φ \to A \in InitO (C)$
	initoeu2lem.x	$⊢ X = {Base}_{C}$
	initoeu2lem.h	$⊢ H = Hom (C)$
	initoeu2lem.i	$⊢ I = Iso (C)$
	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	$⊢ φ \to C \in Cat$
2		initoeu1.a	$⊢ φ \to A \in InitO (C)$
3		initoeu2lem.x	$⊢ X = {Base}_{C}$
4		initoeu2lem.h	$⊢ H = Hom (C)$
5		initoeu2lem.i	$⊢ I = Iso (C)$
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	$⊢ Inv (C) = Inv (C)$
11	1	adantr	$⊢ (φ \land (A \in X \land B \in X \land D \in X)) \to C \in Cat$
12	11	adantr	$⊢ ((φ \land (A \in X \land B \in X \land D \in X)) \land (K \in (B I A) \land F \in (A H D) \land G \in (B H D))) \to C \in Cat$
13		simpr1	$⊢ (φ \land (A \in X \land B \in X \land D \in X)) \to A \in X$
14	13	adantr	$⊢ ((φ \land (A \in X \land B \in X \land D \in X)) \land (K \in (B I A) \land F \in (A H D) \land G \in (B H D))) \to A \in X$
15		simpr2	$⊢ (φ \land (A \in X \land B \in X \land D \in X)) \to B \in X$
16	15	adantr	$⊢ ((φ \land (A \in X \land B \in X \land D \in X)) \land (K \in (B I A) \land F \in (A H D) \land G \in (B H D))) \to B \in X$
17		simplr3	$⊢ ((φ \land (A \in X \land B \in X \land D \in X)) \land (K \in (B I A) \land F \in (A H D) \land G \in (B H D))) \to D \in X$
18	5	oveqi	$⊢ B I A = B Iso (C) A$
19	18	eleq2i	$⊢ K \in (B I A) \leftrightarrow K \in (B Iso (C) A)$
20	19	biimpi	$⊢ K \in (B I A) \to K \in (B Iso (C) A)$
21	20	3ad2ant1	$⊢ (K \in (B I A) \land F \in (A H D) \land G \in (B H D)) \to K \in (B Iso (C) A)$
22	21	adantl	$⊢ ((φ \land (A \in X \land B \in X \land D \in X)) \land (K \in (B I A) \land F \in (A H D) \land G \in (B H D))) \to K \in (B Iso (C) A)$
23	4	oveqi	$⊢ B H D = B Hom (C) D$
24	23	eleq2i	$⊢ G \in (B H D) \leftrightarrow G \in (B Hom (C) D)$
25	24	biimpi	$⊢ G \in (B H D) \to G \in (B Hom (C) D)$
26	25	3ad2ant3	$⊢ (K \in (B I A) \land F \in (A H D) \land G \in (B H D)) \to G \in (B Hom (C) D)$
27	26	adantl	$⊢ ((φ \land (A \in X \land B \in X \land D \in X)) \land (K \in (B I A) \land F \in (A H D) \land G \in (B H D))) \to G \in (B Hom (C) D)$
28		eqid	$⊢ Hom (C) = Hom (C)$
29	3 28 5 11 15 13	isohom	$⊢ (φ \land (A \in X \land B \in X \land D \in X)) \to B I A \subseteq B Hom (C) A$
30	29	sseld	$⊢ (φ \land (A \in X \land B \in X \land D \in X)) \to (K \in (B I A) \to K \in (B Hom (C) A))$
31	30	com12	$⊢ K \in (B I A) \to ((φ \land (A \in X \land B \in X \land D \in X)) \to K \in (B Hom (C) A))$
32	31	3ad2ant1	$⊢ (K \in (B I A) \land F \in (A H D) \land G \in (B H D)) \to ((φ \land (A \in X \land B \in X \land D \in X)) \to K \in (B Hom (C) A))$
33	32	impcom	$⊢ ((φ \land (A \in X \land B \in X \land D \in X)) \land (K \in (B I A) \land F \in (A H D) \land G \in (B H D))) \to K \in (B Hom (C) A)$
34	4	oveqi	$⊢ A H D = A Hom (C) D$
35	34	eleq2i	$⊢ F \in (A H D) \leftrightarrow F \in (A Hom (C) D)$
36	35	biimpi	$⊢ F \in (A H D) \to F \in (A Hom (C) D)$
37	36	3ad2ant2	$⊢ (K \in (B I A) \land F \in (A H D) \land G \in (B H D)) \to F \in (A Hom (C) D)$
38	37	adantl	$⊢ ((φ \land (A \in X \land B \in X \land D \in X)) \land (K \in (B I A) \land F \in (A H D) \land G \in (B H D))) \to F \in (A Hom (C) D)$
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	$⊢ (B Inv (C) A) (K) = (B Inv (C) A) (K)$
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 \|-

Metamath Proof Explorer

Theorem initoeu2lem0

Proof