uptrlem1

	Ref	Expression
Hypotheses	uptrlem1.h	$⊢ H = Hom (C)$
	uptrlem1.i	$⊢ I = Hom (D)$
	uptrlem1.j	$⊢ J = Hom (E)$
	uptrlem1.d	$⊢ \underset{˙}{∙} = comp (D)$
	uptrlem1.e	No typesetting found for \|- .o. = ( comp ` E ) with typecode \|-
	uptrlem1.x	$⊢ φ \to X \in {Base}_{D}$
	uptrlem1.y	$⊢ φ \to M (X) = Y$
	uptrlem1.z	$⊢ φ \to Z \in {Base}_{C}$
	uptrlem1.w	$⊢ φ \to W \in {Base}_{C}$
	uptrlem1.a	$⊢ φ \to A \in (X I F (Z))$
	uptrlem1.b	$⊢ φ \to (X N F (Z)) (A) = B$
	uptrlem1.f	$⊢ φ \to F (C Func D) G$
	uptrlem1.m	$⊢ φ \to M ((D Full E) \cap (D Faith E)) N$
	uptrlem1.k	$⊢ φ \to ⟨M, N⟩ \circ_{func} ⟨F, G⟩ = ⟨K, L⟩$
Assertion	uptrlem1	Could not format assertion : No typesetting found for \|- ( ph -> ( A. h e. ( Y J ( K ` W ) ) E! k e. ( Z H W ) h = ( ( ( Z L W ) ` k ) ( <. Y , ( K ` Z ) >. .o. ( K ` W ) ) B ) <-> A. g e. ( X I ( F ` W ) ) E! k e. ( Z H W ) g = ( ( ( Z G W ) ` k ) ( <. X , ( F ` Z ) >. .xb ( F ` W ) ) A ) ) ) with typecode \|-

Proof

Step	Hyp	Ref	Expression
1		uptrlem1.h	$⊢ H = Hom (C)$
2		uptrlem1.i	$⊢ I = Hom (D)$
3		uptrlem1.j	$⊢ J = Hom (E)$
4		uptrlem1.d	$⊢ \underset{˙}{∙} = comp (D)$
5		uptrlem1.e	Could not format .o. = ( comp ` E ) : No typesetting found for \|- .o. = ( comp ` E ) with typecode \|-
6		uptrlem1.x	$⊢ φ \to X \in {Base}_{D}$
7		uptrlem1.y	$⊢ φ \to M (X) = Y$
8		uptrlem1.z	$⊢ φ \to Z \in {Base}_{C}$
9		uptrlem1.w	$⊢ φ \to W \in {Base}_{C}$
10		uptrlem1.a	$⊢ φ \to A \in (X I F (Z))$
11		uptrlem1.b	$⊢ φ \to (X N F (Z)) (A) = B$
12		uptrlem1.f	$⊢ φ \to F (C Func D) G$
13		uptrlem1.m	$⊢ φ \to M ((D Full E) \cap (D Faith E)) N$
14		uptrlem1.k	$⊢ φ \to ⟨M, N⟩ \circ_{func} ⟨F, G⟩ = ⟨K, L⟩$
15		eqid	$⊢ {Base}_{D} = {Base}_{D}$
16		eqid	$⊢ {Base}_{C} = {Base}_{C}$
17	16 15 12	funcf1	$⊢ φ \to F : {Base}_{C} ⟶ {Base}_{D}$
18	17 9	ffvelcdmd	$⊢ φ \to F (W) \in {Base}_{D}$
19	15 2 3 13 6 18	ffthf1o	$⊢ φ \to (X N F (W)) : X I F (W) \underset{1-1 onto}{⟶} M (X) J M (F (W))$
20		inss1	$⊢ (D Full E) \cap (D Faith E) \subseteq D Full E$
21		fullfunc	$⊢ D Full E \subseteq D Func E$
22	20 21	sstri	$⊢ (D Full E) \cap (D Faith E) \subseteq D Func E$
23	22	ssbri	$⊢ M ((D Full E) \cap (D Faith E)) N \to M (D Func E) N$
24	13 23	syl	$⊢ φ \to M (D Func E) N$
25	16 12 24 14 9	cofu1a	$⊢ φ \to M (F (W)) = K (W)$
26	7 25	oveq12d	$⊢ φ \to M (X) J M (F (W)) = Y J K (W)$
27	26	f1oeq3d	$⊢ φ \to ((X N F (W)) : X I F (W) \underset{1-1 onto}{⟶} M (X) J M (F (W)) \leftrightarrow (X N F (W)) : X I F (W) \underset{1-1 onto}{⟶} Y J K (W))$
28	19 27	mpbid	$⊢ φ \to (X N F (W)) : X I F (W) \underset{1-1 onto}{⟶} Y J K (W)$
29		f1of	$⊢ (X N F (W)) : X I F (W) \underset{1-1 onto}{⟶} Y J K (W) \to (X N F (W)) : X I F (W) ⟶ Y J K (W)$
30	28 29	syl	$⊢ φ \to (X N F (W)) : X I F (W) ⟶ Y J K (W)$
31	30	ffvelcdmda	$⊢ (φ \land g \in (X I F (W))) \to (X N F (W)) (g) \in (Y J K (W))$
32		f1ofo	$⊢ (X N F (W)) : X I F (W) \underset{1-1 onto}{⟶} Y J K (W) \to (X N F (W)) : X I F (W) \underset{onto}{⟶} Y J K (W)$
33	28 32	syl	$⊢ φ \to (X N F (W)) : X I F (W) \underset{onto}{⟶} Y J K (W)$
34		foelrn	$⊢ ((X N F (W)) : X I F (W) \underset{onto}{⟶} Y J K (W) \land h \in (Y J K (W))) \to \exists g \in (X I F (W)) h = (X N F (W)) (g)$
35	33 34	sylan	$⊢ (φ \land h \in (Y J K (W))) \to \exists g \in (X I F (W)) h = (X N F (W)) (g)$
36		simpl3	$⊢ ((φ \land g \in (X I F (W)) \land h = (X N F (W)) (g)) \land k \in (Z H W)) \to h = (X N F (W)) (g)$
37	36	eqeq1d	Could not format ( ( ( ph /\ g e. ( X I ( F ` W ) ) /\ h = ( ( X N ( F ` W ) ) ` g ) ) /\ k e. ( Z H W ) ) -> ( h = ( ( ( Z L W ) ` k ) ( <. Y , ( K ` Z ) >. .o. ( K ` W ) ) B ) <-> ( ( X N ( F ` W ) ) ` g ) = ( ( ( Z L W ) ` k ) ( <. Y , ( K ` Z ) >. .o. ( K ` W ) ) B ) ) ) : No typesetting found for \|- ( ( ( ph /\ g e. ( X I ( F ` W ) ) /\ h = ( ( X N ( F ` W ) ) ` g ) ) /\ k e. ( Z H W ) ) -> ( h = ( ( ( Z L W ) ` k ) ( <. Y , ( K ` Z ) >. .o. ( K ` W ) ) B ) <-> ( ( X N ( F ` W ) ) ` g ) = ( ( ( Z L W ) ` k ) ( <. Y , ( K ` Z ) >. .o. ( K ` W ) ) B ) ) ) with typecode \|-
38	24	ad2antrr	$⊢ ((φ \land g \in (X I F (W))) \land k \in (Z H W)) \to M (D Func E) N$
39	6	ad2antrr	$⊢ ((φ \land g \in (X I F (W))) \land k \in (Z H W)) \to X \in {Base}_{D}$
40	17 8	ffvelcdmd	$⊢ φ \to F (Z) \in {Base}_{D}$
41	40	ad2antrr	$⊢ ((φ \land g \in (X I F (W))) \land k \in (Z H W)) \to F (Z) \in {Base}_{D}$
42	18	ad2antrr	$⊢ ((φ \land g \in (X I F (W))) \land k \in (Z H W)) \to F (W) \in {Base}_{D}$
43	10	ad2antrr	$⊢ ((φ \land g \in (X I F (W))) \land k \in (Z H W)) \to A \in (X I F (Z))$
44	16 1 2 12 8 9	funcf2	$⊢ φ \to (Z G W) : Z H W ⟶ F (Z) I F (W)$
45	44	adantr	$⊢ (φ \land g \in (X I F (W))) \to (Z G W) : Z H W ⟶ F (Z) I F (W)$
46	45	ffvelcdmda	$⊢ ((φ \land g \in (X I F (W))) \land k \in (Z H W)) \to (Z G W) (k) \in (F (Z) I F (W))$
47	15 2 4 5 38 39 41 42 43 46	funcco	Could not format ( ( ( ph /\ g e. ( X I ( F ` W ) ) ) /\ k e. ( Z H W ) ) -> ( ( X N ( F ` W ) ) ` ( ( ( Z G W ) ` k ) ( <. X , ( F ` Z ) >. .xb ( F ` W ) ) A ) ) = ( ( ( ( F ` Z ) N ( F ` W ) ) ` ( ( Z G W ) ` k ) ) ( <. ( M ` X ) , ( M ` ( F ` Z ) ) >. .o. ( M ` ( F ` W ) ) ) ( ( X N ( F ` Z ) ) ` A ) ) ) : No typesetting found for \|- ( ( ( ph /\ g e. ( X I ( F ` W ) ) ) /\ k e. ( Z H W ) ) -> ( ( X N ( F ` W ) ) ` ( ( ( Z G W ) ` k ) ( <. X , ( F ` Z ) >. .xb ( F ` W ) ) A ) ) = ( ( ( ( F ` Z ) N ( F ` W ) ) ` ( ( Z G W ) ` k ) ) ( <. ( M ` X ) , ( M ` ( F ` Z ) ) >. .o. ( M ` ( F ` W ) ) ) ( ( X N ( F ` Z ) ) ` A ) ) ) with typecode \|-
48	7	ad2antrr	$⊢ ((φ \land g \in (X I F (W))) \land k \in (Z H W)) \to M (X) = Y$
49	16 12 24 14 8	cofu1a	$⊢ φ \to M (F (Z)) = K (Z)$
50	49	ad2antrr	$⊢ ((φ \land g \in (X I F (W))) \land k \in (Z H W)) \to M (F (Z)) = K (Z)$
51	48 50	opeq12d	$⊢ ((φ \land g \in (X I F (W))) \land k \in (Z H W)) \to ⟨M (X), M (F (Z))⟩ = ⟨Y, K (Z)⟩$
52	25	ad2antrr	$⊢ ((φ \land g \in (X I F (W))) \land k \in (Z H W)) \to M (F (W)) = K (W)$
53	51 52	oveq12d	Could not format ( ( ( ph /\ g e. ( X I ( F ` W ) ) ) /\ k e. ( Z H W ) ) -> ( <. ( M ` X ) , ( M ` ( F ` Z ) ) >. .o. ( M ` ( F ` W ) ) ) = ( <. Y , ( K ` Z ) >. .o. ( K ` W ) ) ) : No typesetting found for \|- ( ( ( ph /\ g e. ( X I ( F ` W ) ) ) /\ k e. ( Z H W ) ) -> ( <. ( M ` X ) , ( M ` ( F ` Z ) ) >. .o. ( M ` ( F ` W ) ) ) = ( <. Y , ( K ` Z ) >. .o. ( K ` W ) ) ) with typecode \|-
54	12	ad2antrr	$⊢ ((φ \land g \in (X I F (W))) \land k \in (Z H W)) \to F (C Func D) G$
55	14	ad2antrr	$⊢ ((φ \land g \in (X I F (W))) \land k \in (Z H W)) \to ⟨M, N⟩ \circ_{func} ⟨F, G⟩ = ⟨K, L⟩$
56	8	ad2antrr	$⊢ ((φ \land g \in (X I F (W))) \land k \in (Z H W)) \to Z \in {Base}_{C}$
57	9	ad2antrr	$⊢ ((φ \land g \in (X I F (W))) \land k \in (Z H W)) \to W \in {Base}_{C}$
58		simpr	$⊢ ((φ \land g \in (X I F (W))) \land k \in (Z H W)) \to k \in (Z H W)$
59	16 54 38 55 56 57 1 58	cofu2a	$⊢ ((φ \land g \in (X I F (W))) \land k \in (Z H W)) \to (F (Z) N F (W)) ((Z G W) (k)) = (Z L W) (k)$
60	11	ad2antrr	$⊢ ((φ \land g \in (X I F (W))) \land k \in (Z H W)) \to (X N F (Z)) (A) = B$
61	53 59 60	oveq123d	Could not format ( ( ( ph /\ g e. ( X I ( F ` W ) ) ) /\ k e. ( Z H W ) ) -> ( ( ( ( F ` Z ) N ( F ` W ) ) ` ( ( Z G W ) ` k ) ) ( <. ( M ` X ) , ( M ` ( F ` Z ) ) >. .o. ( M ` ( F ` W ) ) ) ( ( X N ( F ` Z ) ) ` A ) ) = ( ( ( Z L W ) ` k ) ( <. Y , ( K ` Z ) >. .o. ( K ` W ) ) B ) ) : No typesetting found for \|- ( ( ( ph /\ g e. ( X I ( F ` W ) ) ) /\ k e. ( Z H W ) ) -> ( ( ( ( F ` Z ) N ( F ` W ) ) ` ( ( Z G W ) ` k ) ) ( <. ( M ` X ) , ( M ` ( F ` Z ) ) >. .o. ( M ` ( F ` W ) ) ) ( ( X N ( F ` Z ) ) ` A ) ) = ( ( ( Z L W ) ` k ) ( <. Y , ( K ` Z ) >. .o. ( K ` W ) ) B ) ) with typecode \|-
62	47 61	eqtrd	Could not format ( ( ( ph /\ g e. ( X I ( F ` W ) ) ) /\ k e. ( Z H W ) ) -> ( ( X N ( F ` W ) ) ` ( ( ( Z G W ) ` k ) ( <. X , ( F ` Z ) >. .xb ( F ` W ) ) A ) ) = ( ( ( Z L W ) ` k ) ( <. Y , ( K ` Z ) >. .o. ( K ` W ) ) B ) ) : No typesetting found for \|- ( ( ( ph /\ g e. ( X I ( F ` W ) ) ) /\ k e. ( Z H W ) ) -> ( ( X N ( F ` W ) ) ` ( ( ( Z G W ) ` k ) ( <. X , ( F ` Z ) >. .xb ( F ` W ) ) A ) ) = ( ( ( Z L W ) ` k ) ( <. Y , ( K ` Z ) >. .o. ( K ` W ) ) B ) ) with typecode \|-
63	62	eqeq2d	Could not format ( ( ( ph /\ g e. ( X I ( F ` W ) ) ) /\ k e. ( Z H W ) ) -> ( ( ( X N ( F ` W ) ) ` g ) = ( ( X N ( F ` W ) ) ` ( ( ( Z G W ) ` k ) ( <. X , ( F ` Z ) >. .xb ( F ` W ) ) A ) ) <-> ( ( X N ( F ` W ) ) ` g ) = ( ( ( Z L W ) ` k ) ( <. Y , ( K ` Z ) >. .o. ( K ` W ) ) B ) ) ) : No typesetting found for \|- ( ( ( ph /\ g e. ( X I ( F ` W ) ) ) /\ k e. ( Z H W ) ) -> ( ( ( X N ( F ` W ) ) ` g ) = ( ( X N ( F ` W ) ) ` ( ( ( Z G W ) ` k ) ( <. X , ( F ` Z ) >. .xb ( F ` W ) ) A ) ) <-> ( ( X N ( F ` W ) ) ` g ) = ( ( ( Z L W ) ` k ) ( <. Y , ( K ` Z ) >. .o. ( K ` W ) ) B ) ) ) with typecode \|-
64		f1of1	$⊢ (X N F (W)) : X I F (W) \underset{1-1 onto}{⟶} Y J K (W) \to (X N F (W)) : X I F (W) \underset{1-1}{⟶} Y J K (W)$
65	28 64	syl	$⊢ φ \to (X N F (W)) : X I F (W) \underset{1-1}{⟶} Y J K (W)$
66	65	ad2antrr	$⊢ ((φ \land g \in (X I F (W))) \land k \in (Z H W)) \to (X N F (W)) : X I F (W) \underset{1-1}{⟶} Y J K (W)$
67		simplr	$⊢ ((φ \land g \in (X I F (W))) \land k \in (Z H W)) \to g \in (X I F (W))$
68	38	funcrcl2	$⊢ ((φ \land g \in (X I F (W))) \land k \in (Z H W)) \to D \in Cat$
69	15 2 4 68 39 41 42 43 46	catcocl	$⊢ ((φ \land g \in (X I F (W))) \land k \in (Z H W)) \to (Z G W) (k) (⟨X, F (Z)⟩ \underset{˙}{∙} F (W)) A \in (X I F (W))$
70		f1fveq	$⊢ ((X N F (W)) : X I F (W) \underset{1-1}{⟶} Y J K (W) \land (g \in (X I F (W)) \land (Z G W) (k) (⟨X, F (Z)⟩ \underset{˙}{∙} F (W)) A \in (X I F (W)))) \to ((X N F (W)) (g) = (X N F (W)) ((Z G W) (k) (⟨X, F (Z)⟩ \underset{˙}{∙} F (W)) A) \leftrightarrow g = (Z G W) (k) (⟨X, F (Z)⟩ \underset{˙}{∙} F (W)) A)$
71	66 67 69 70	syl12anc	$⊢ ((φ \land g \in (X I F (W))) \land k \in (Z H W)) \to ((X N F (W)) (g) = (X N F (W)) ((Z G W) (k) (⟨X, F (Z)⟩ \underset{˙}{∙} F (W)) A) \leftrightarrow g = (Z G W) (k) (⟨X, F (Z)⟩ \underset{˙}{∙} F (W)) A)$
72	63 71	bitr3d	Could not format ( ( ( ph /\ g e. ( X I ( F ` W ) ) ) /\ k e. ( Z H W ) ) -> ( ( ( X N ( F ` W ) ) ` g ) = ( ( ( Z L W ) ` k ) ( <. Y , ( K ` Z ) >. .o. ( K ` W ) ) B ) <-> g = ( ( ( Z G W ) ` k ) ( <. X , ( F ` Z ) >. .xb ( F ` W ) ) A ) ) ) : No typesetting found for \|- ( ( ( ph /\ g e. ( X I ( F ` W ) ) ) /\ k e. ( Z H W ) ) -> ( ( ( X N ( F ` W ) ) ` g ) = ( ( ( Z L W ) ` k ) ( <. Y , ( K ` Z ) >. .o. ( K ` W ) ) B ) <-> g = ( ( ( Z G W ) ` k ) ( <. X , ( F ` Z ) >. .xb ( F ` W ) ) A ) ) ) with typecode \|-
73	72	3adantl3	Could not format ( ( ( ph /\ g e. ( X I ( F ` W ) ) /\ h = ( ( X N ( F ` W ) ) ` g ) ) /\ k e. ( Z H W ) ) -> ( ( ( X N ( F ` W ) ) ` g ) = ( ( ( Z L W ) ` k ) ( <. Y , ( K ` Z ) >. .o. ( K ` W ) ) B ) <-> g = ( ( ( Z G W ) ` k ) ( <. X , ( F ` Z ) >. .xb ( F ` W ) ) A ) ) ) : No typesetting found for \|- ( ( ( ph /\ g e. ( X I ( F ` W ) ) /\ h = ( ( X N ( F ` W ) ) ` g ) ) /\ k e. ( Z H W ) ) -> ( ( ( X N ( F ` W ) ) ` g ) = ( ( ( Z L W ) ` k ) ( <. Y , ( K ` Z ) >. .o. ( K ` W ) ) B ) <-> g = ( ( ( Z G W ) ` k ) ( <. X , ( F ` Z ) >. .xb ( F ` W ) ) A ) ) ) with typecode \|-
74	37 73	bitrd	Could not format ( ( ( ph /\ g e. ( X I ( F ` W ) ) /\ h = ( ( X N ( F ` W ) ) ` g ) ) /\ k e. ( Z H W ) ) -> ( h = ( ( ( Z L W ) ` k ) ( <. Y , ( K ` Z ) >. .o. ( K ` W ) ) B ) <-> g = ( ( ( Z G W ) ` k ) ( <. X , ( F ` Z ) >. .xb ( F ` W ) ) A ) ) ) : No typesetting found for \|- ( ( ( ph /\ g e. ( X I ( F ` W ) ) /\ h = ( ( X N ( F ` W ) ) ` g ) ) /\ k e. ( Z H W ) ) -> ( h = ( ( ( Z L W ) ` k ) ( <. Y , ( K ` Z ) >. .o. ( K ` W ) ) B ) <-> g = ( ( ( Z G W ) ` k ) ( <. X , ( F ` Z ) >. .xb ( F ` W ) ) A ) ) ) with typecode \|-
75	74	reubidva	Could not format ( ( ph /\ g e. ( X I ( F ` W ) ) /\ h = ( ( X N ( F ` W ) ) ` g ) ) -> ( E! k e. ( Z H W ) h = ( ( ( Z L W ) ` k ) ( <. Y , ( K ` Z ) >. .o. ( K ` W ) ) B ) <-> E! k e. ( Z H W ) g = ( ( ( Z G W ) ` k ) ( <. X , ( F ` Z ) >. .xb ( F ` W ) ) A ) ) ) : No typesetting found for \|- ( ( ph /\ g e. ( X I ( F ` W ) ) /\ h = ( ( X N ( F ` W ) ) ` g ) ) -> ( E! k e. ( Z H W ) h = ( ( ( Z L W ) ` k ) ( <. Y , ( K ` Z ) >. .o. ( K ` W ) ) B ) <-> E! k e. ( Z H W ) g = ( ( ( Z G W ) ` k ) ( <. X , ( F ` Z ) >. .xb ( F ` W ) ) A ) ) ) with typecode \|-
76	31 35 75	ralxfrd2	Could not format ( ph -> ( A. h e. ( Y J ( K ` W ) ) E! k e. ( Z H W ) h = ( ( ( Z L W ) ` k ) ( <. Y , ( K ` Z ) >. .o. ( K ` W ) ) B ) <-> A. g e. ( X I ( F ` W ) ) E! k e. ( Z H W ) g = ( ( ( Z G W ) ` k ) ( <. X , ( F ` Z ) >. .xb ( F ` W ) ) A ) ) ) : No typesetting found for \|- ( ph -> ( A. h e. ( Y J ( K ` W ) ) E! k e. ( Z H W ) h = ( ( ( Z L W ) ` k ) ( <. Y , ( K ` Z ) >. .o. ( K ` W ) ) B ) <-> A. g e. ( X I ( F ` W ) ) E! k e. ( Z H W ) g = ( ( ( Z G W ) ` k ) ( <. X , ( F ` Z ) >. .xb ( F ` W ) ) A ) ) ) with typecode \|-

Metamath Proof Explorer

Theorem uptrlem1

Proof