yonedalem4c

	Ref	Expression
Hypotheses	yoneda.y	$⊢ Y = Yon (C)$
	yoneda.b	$⊢ B = {Base}_{C}$
	yoneda.1	$⊢ \underset{˙}{1} = Id (C)$
	yoneda.o	$⊢ O = oppCat (C)$
	yoneda.s	$⊢ S = SetCat (U)$
	yoneda.t	$⊢ T = SetCat (V)$
	yoneda.q	$⊢ Q = O FuncCat S$
	yoneda.h	$⊢ H = {Hom}_{F} (Q)$
	yoneda.r	$⊢ R = (Q \times_{c} O) FuncCat T$
	yoneda.e	$⊢ E = O {eval}_{F} S$
	yoneda.z	$⊢ Z = H \circ_{func} ((⟨1^{st} (Y), tpos 2^{nd} (Y)⟩ \circ_{func} (Q {2^{nd}}_{F} O)) {⟨,⟩}_{F} (Q {1^{st}}_{F} O))$
	yoneda.c	$⊢ φ \to C \in Cat$
	yoneda.w	$⊢ φ \to V \in W$
	yoneda.u	$⊢ φ \to ran {Hom}_{𝑓} (C) \subseteq U$
	yoneda.v	$⊢ φ \to ran {Hom}_{𝑓} (Q) \cup U \subseteq V$
	yonedalem21.f	$⊢ φ \to F \in (O Func S)$
	yonedalem21.x	$⊢ φ \to X \in B$
	yonedalem4.n	$⊢ N = (f \in (O Func S), x \in B ⟼ (u \in 1^{st} (f) (x) ⟼ (y \in B ⟼ (g \in (y Hom (C) x) ⟼ (x 2^{nd} (f) y) (g) (u)))))$
	yonedalem4.p	$⊢ φ \to A \in 1^{st} (F) (X)$
Assertion	yonedalem4c	$⊢ φ \to (F N X) (A) \in (1^{st} (Y) (X) (O Nat S) F)$

Proof

Step	Hyp	Ref	Expression
1		yoneda.y	$⊢ Y = Yon (C)$
2		yoneda.b	$⊢ B = {Base}_{C}$
3		yoneda.1	$⊢ \underset{˙}{1} = Id (C)$
4		yoneda.o	$⊢ O = oppCat (C)$
5		yoneda.s	$⊢ S = SetCat (U)$
6		yoneda.t	$⊢ T = SetCat (V)$
7		yoneda.q	$⊢ Q = O FuncCat S$
8		yoneda.h	$⊢ H = {Hom}_{F} (Q)$
9		yoneda.r	$⊢ R = (Q \times_{c} O) FuncCat T$
10		yoneda.e	$⊢ E = O {eval}_{F} S$
11		yoneda.z	$⊢ Z = H \circ_{func} ((⟨1^{st} (Y), tpos 2^{nd} (Y)⟩ \circ_{func} (Q {2^{nd}}_{F} O)) {⟨,⟩}_{F} (Q {1^{st}}_{F} O))$
12		yoneda.c	$⊢ φ \to C \in Cat$
13		yoneda.w	$⊢ φ \to V \in W$
14		yoneda.u	$⊢ φ \to ran {Hom}_{𝑓} (C) \subseteq U$
15		yoneda.v	$⊢ φ \to ran {Hom}_{𝑓} (Q) \cup U \subseteq V$
16		yonedalem21.f	$⊢ φ \to F \in (O Func S)$
17		yonedalem21.x	$⊢ φ \to X \in B$
18		yonedalem4.n	$⊢ N = (f \in (O Func S), x \in B ⟼ (u \in 1^{st} (f) (x) ⟼ (y \in B ⟼ (g \in (y Hom (C) x) ⟼ (x 2^{nd} (f) y) (g) (u)))))$
19		yonedalem4.p	$⊢ φ \to A \in 1^{st} (F) (X)$
20	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19	yonedalem4a	$⊢ φ \to (F N X) (A) = (y \in B ⟼ (g \in (y Hom (C) X) ⟼ (X 2^{nd} (F) y) (g) (A)))$
21		oveq1	$⊢ y = z \to y Hom (C) X = z Hom (C) X$
22		oveq2	$⊢ y = z \to X 2^{nd} (F) y = X 2^{nd} (F) z$
23	22	fveq1d	$⊢ y = z \to (X 2^{nd} (F) y) (g) = (X 2^{nd} (F) z) (g)$
24	23	fveq1d	$⊢ y = z \to (X 2^{nd} (F) y) (g) (A) = (X 2^{nd} (F) z) (g) (A)$
25	21 24	mpteq12dv	$⊢ y = z \to (g \in (y Hom (C) X) ⟼ (X 2^{nd} (F) y) (g) (A)) = (g \in (z Hom (C) X) ⟼ (X 2^{nd} (F) z) (g) (A))$
26	25	cbvmptv	$⊢ (y \in B ⟼ (g \in (y Hom (C) X) ⟼ (X 2^{nd} (F) y) (g) (A))) = (z \in B ⟼ (g \in (z Hom (C) X) ⟼ (X 2^{nd} (F) z) (g) (A)))$
27	20 26	eqtrdi	$⊢ φ \to (F N X) (A) = (z \in B ⟼ (g \in (z Hom (C) X) ⟼ (X 2^{nd} (F) z) (g) (A)))$
28	4 2	oppcbas	$⊢ B = {Base}_{O}$
29		eqid	$⊢ Hom (O) = Hom (O)$
30		eqid	$⊢ Hom (S) = Hom (S)$
31		relfunc	$⊢ Rel (O Func S)$
32		1st2ndbr	$⊢ (Rel (O Func S) \land F \in (O Func S)) \to 1^{st} (F) (O Func S) 2^{nd} (F)$
33	31 16 32	sylancr	$⊢ φ \to 1^{st} (F) (O Func S) 2^{nd} (F)$
34	33	adantr	$⊢ (φ \land z \in B) \to 1^{st} (F) (O Func S) 2^{nd} (F)$
35	17	adantr	$⊢ (φ \land z \in B) \to X \in B$
36		simpr	$⊢ (φ \land z \in B) \to z \in B$
37	28 29 30 34 35 36	funcf2	$⊢ (φ \land z \in B) \to (X 2^{nd} (F) z) : X Hom (O) z ⟶ 1^{st} (F) (X) Hom (S) 1^{st} (F) (z)$
38	37	adantr	$⊢ ((φ \land z \in B) \land g \in (z Hom (C) X)) \to (X 2^{nd} (F) z) : X Hom (O) z ⟶ 1^{st} (F) (X) Hom (S) 1^{st} (F) (z)$
39		simpr	$⊢ ((φ \land z \in B) \land g \in (z Hom (C) X)) \to g \in (z Hom (C) X)$
40		eqid	$⊢ Hom (C) = Hom (C)$
41	40 4	oppchom	$⊢ X Hom (O) z = z Hom (C) X$
42	39 41	eleqtrrdi	$⊢ ((φ \land z \in B) \land g \in (z Hom (C) X)) \to g \in (X Hom (O) z)$
43	38 42	ffvelrnd	$⊢ ((φ \land z \in B) \land g \in (z Hom (C) X)) \to (X 2^{nd} (F) z) (g) \in (1^{st} (F) (X) Hom (S) 1^{st} (F) (z))$
44	15	unssbd	$⊢ φ \to U \subseteq V$
45	13 44	ssexd	$⊢ φ \to U \in V$
46	45	adantr	$⊢ (φ \land z \in B) \to U \in V$
47	46	adantr	$⊢ ((φ \land z \in B) \land g \in (z Hom (C) X)) \to U \in V$
48		eqid	$⊢ {Base}_{S} = {Base}_{S}$
49	28 48 33	funcf1	$⊢ φ \to 1^{st} (F) : B ⟶ {Base}_{S}$
50	5 45	setcbas	$⊢ φ \to U = {Base}_{S}$
51	50	feq3d	$⊢ φ \to (1^{st} (F) : B ⟶ U \leftrightarrow 1^{st} (F) : B ⟶ {Base}_{S})$
52	49 51	mpbird	$⊢ φ \to 1^{st} (F) : B ⟶ U$
53	52 17	ffvelrnd	$⊢ φ \to 1^{st} (F) (X) \in U$
54	53	ad2antrr	$⊢ ((φ \land z \in B) \land g \in (z Hom (C) X)) \to 1^{st} (F) (X) \in U$
55	52	ffvelrnda	$⊢ (φ \land z \in B) \to 1^{st} (F) (z) \in U$
56	55	adantr	$⊢ ((φ \land z \in B) \land g \in (z Hom (C) X)) \to 1^{st} (F) (z) \in U$
57	5 47 30 54 56	elsetchom	$⊢ ((φ \land z \in B) \land g \in (z Hom (C) X)) \to ((X 2^{nd} (F) z) (g) \in (1^{st} (F) (X) Hom (S) 1^{st} (F) (z)) \leftrightarrow (X 2^{nd} (F) z) (g) : 1^{st} (F) (X) ⟶ 1^{st} (F) (z))$
58	43 57	mpbid	$⊢ ((φ \land z \in B) \land g \in (z Hom (C) X)) \to (X 2^{nd} (F) z) (g) : 1^{st} (F) (X) ⟶ 1^{st} (F) (z)$
59	19	ad2antrr	$⊢ ((φ \land z \in B) \land g \in (z Hom (C) X)) \to A \in 1^{st} (F) (X)$
60	58 59	ffvelrnd	$⊢ ((φ \land z \in B) \land g \in (z Hom (C) X)) \to (X 2^{nd} (F) z) (g) (A) \in 1^{st} (F) (z)$
61	60	fmpttd	$⊢ (φ \land z \in B) \to (g \in (z Hom (C) X) ⟼ (X 2^{nd} (F) z) (g) (A)) : z Hom (C) X ⟶ 1^{st} (F) (z)$
62	12	adantr	$⊢ (φ \land z \in B) \to C \in Cat$
63	1 2 62 35 40 36	yon11	$⊢ (φ \land z \in B) \to 1^{st} (1^{st} (Y) (X)) (z) = z Hom (C) X$
64	63	feq2d	$⊢ (φ \land z \in B) \to ((g \in (z Hom (C) X) ⟼ (X 2^{nd} (F) z) (g) (A)) : 1^{st} (1^{st} (Y) (X)) (z) ⟶ 1^{st} (F) (z) \leftrightarrow (g \in (z Hom (C) X) ⟼ (X 2^{nd} (F) z) (g) (A)) : z Hom (C) X ⟶ 1^{st} (F) (z))$
65	61 64	mpbird	$⊢ (φ \land z \in B) \to (g \in (z Hom (C) X) ⟼ (X 2^{nd} (F) z) (g) (A)) : 1^{st} (1^{st} (Y) (X)) (z) ⟶ 1^{st} (F) (z)$
66	1 2 12 17 4 5 45 14	yon1cl	$⊢ φ \to 1^{st} (Y) (X) \in (O Func S)$
67		1st2ndbr	$⊢ (Rel (O Func S) \land 1^{st} (Y) (X) \in (O Func S)) \to 1^{st} (1^{st} (Y) (X)) (O Func S) 2^{nd} (1^{st} (Y) (X))$
68	31 66 67	sylancr	$⊢ φ \to 1^{st} (1^{st} (Y) (X)) (O Func S) 2^{nd} (1^{st} (Y) (X))$
69	28 48 68	funcf1	$⊢ φ \to 1^{st} (1^{st} (Y) (X)) : B ⟶ {Base}_{S}$
70	50	feq3d	$⊢ φ \to (1^{st} (1^{st} (Y) (X)) : B ⟶ U \leftrightarrow 1^{st} (1^{st} (Y) (X)) : B ⟶ {Base}_{S})$
71	69 70	mpbird	$⊢ φ \to 1^{st} (1^{st} (Y) (X)) : B ⟶ U$
72	71	ffvelrnda	$⊢ (φ \land z \in B) \to 1^{st} (1^{st} (Y) (X)) (z) \in U$
73	5 46 30 72 55	elsetchom	$⊢ (φ \land z \in B) \to ((g \in (z Hom (C) X) ⟼ (X 2^{nd} (F) z) (g) (A)) \in (1^{st} (1^{st} (Y) (X)) (z) Hom (S) 1^{st} (F) (z)) \leftrightarrow (g \in (z Hom (C) X) ⟼ (X 2^{nd} (F) z) (g) (A)) : 1^{st} (1^{st} (Y) (X)) (z) ⟶ 1^{st} (F) (z))$
74	65 73	mpbird	$⊢ (φ \land z \in B) \to (g \in (z Hom (C) X) ⟼ (X 2^{nd} (F) z) (g) (A)) \in (1^{st} (1^{st} (Y) (X)) (z) Hom (S) 1^{st} (F) (z))$
75	74	ralrimiva	$⊢ φ \to \forall z \in B (g \in (z Hom (C) X) ⟼ (X 2^{nd} (F) z) (g) (A)) \in (1^{st} (1^{st} (Y) (X)) (z) Hom (S) 1^{st} (F) (z))$
76	2	fvexi	$⊢ B \in V$
77		mptelixpg	$⊢ B \in V \to ((z \in B ⟼ (g \in (z Hom (C) X) ⟼ (X 2^{nd} (F) z) (g) (A))) \in \underset{z \in B}{⨉} (1^{st} (1^{st} (Y) (X)) (z) Hom (S) 1^{st} (F) (z)) \leftrightarrow \forall z \in B (g \in (z Hom (C) X) ⟼ (X 2^{nd} (F) z) (g) (A)) \in (1^{st} (1^{st} (Y) (X)) (z) Hom (S) 1^{st} (F) (z)))$
78	76 77	ax-mp	$⊢ (z \in B ⟼ (g \in (z Hom (C) X) ⟼ (X 2^{nd} (F) z) (g) (A))) \in \underset{z \in B}{⨉} (1^{st} (1^{st} (Y) (X)) (z) Hom (S) 1^{st} (F) (z)) \leftrightarrow \forall z \in B (g \in (z Hom (C) X) ⟼ (X 2^{nd} (F) z) (g) (A)) \in (1^{st} (1^{st} (Y) (X)) (z) Hom (S) 1^{st} (F) (z))$
79	75 78	sylibr	$⊢ φ \to (z \in B ⟼ (g \in (z Hom (C) X) ⟼ (X 2^{nd} (F) z) (g) (A))) \in \underset{z \in B}{⨉} (1^{st} (1^{st} (Y) (X)) (z) Hom (S) 1^{st} (F) (z))$
80	27 79	eqeltrd	$⊢ φ \to (F N X) (A) \in \underset{z \in B}{⨉} (1^{st} (1^{st} (Y) (X)) (z) Hom (S) 1^{st} (F) (z))$
81	12	adantr	$⊢ (φ \land (z \in B \land w \in B \land h \in (z Hom (O) w))) \to C \in Cat$
82	17	adantr	$⊢ (φ \land (z \in B \land w \in B \land h \in (z Hom (O) w))) \to X \in B$
83		simpr1	$⊢ (φ \land (z \in B \land w \in B \land h \in (z Hom (O) w))) \to z \in B$
84	1 2 81 82 40 83	yon11	$⊢ (φ \land (z \in B \land w \in B \land h \in (z Hom (O) w))) \to 1^{st} (1^{st} (Y) (X)) (z) = z Hom (C) X$
85	84	eleq2d	$⊢ (φ \land (z \in B \land w \in B \land h \in (z Hom (O) w))) \to (k \in 1^{st} (1^{st} (Y) (X)) (z) \leftrightarrow k \in (z Hom (C) X))$
86	85	biimpa	$⊢ ((φ \land (z \in B \land w \in B \land h \in (z Hom (O) w))) \land k \in 1^{st} (1^{st} (Y) (X)) (z)) \to k \in (z Hom (C) X)$
87		eqid	$⊢ comp (O) = comp (O)$
88		eqid	$⊢ comp (S) = comp (S)$
89	33	adantr	$⊢ (φ \land (z \in B \land w \in B \land h \in (z Hom (O) w))) \to 1^{st} (F) (O Func S) 2^{nd} (F)$
90	89	adantr	$⊢ ((φ \land (z \in B \land w \in B \land h \in (z Hom (O) w))) \land k \in (z Hom (C) X)) \to 1^{st} (F) (O Func S) 2^{nd} (F)$
91	82	adantr	$⊢ ((φ \land (z \in B \land w \in B \land h \in (z Hom (O) w))) \land k \in (z Hom (C) X)) \to X \in B$
92	83	adantr	$⊢ ((φ \land (z \in B \land w \in B \land h \in (z Hom (O) w))) \land k \in (z Hom (C) X)) \to z \in B$
93		simpr2	$⊢ (φ \land (z \in B \land w \in B \land h \in (z Hom (O) w))) \to w \in B$
94	93	adantr	$⊢ ((φ \land (z \in B \land w \in B \land h \in (z Hom (O) w))) \land k \in (z Hom (C) X)) \to w \in B$
95		simpr	$⊢ ((φ \land (z \in B \land w \in B \land h \in (z Hom (O) w))) \land k \in (z Hom (C) X)) \to k \in (z Hom (C) X)$
96	95 41	eleqtrrdi	$⊢ ((φ \land (z \in B \land w \in B \land h \in (z Hom (O) w))) \land k \in (z Hom (C) X)) \to k \in (X Hom (O) z)$
97		simplr3	$⊢ ((φ \land (z \in B \land w \in B \land h \in (z Hom (O) w))) \land k \in (z Hom (C) X)) \to h \in (z Hom (O) w)$
98	28 29 87 88 90 91 92 94 96 97	funcco	$⊢ ((φ \land (z \in B \land w \in B \land h \in (z Hom (O) w))) \land k \in (z Hom (C) X)) \to (X 2^{nd} (F) w) (h (⟨X, z⟩ comp (O) w) k) = (z 2^{nd} (F) w) (h) (⟨1^{st} (F) (X), 1^{st} (F) (z)⟩ comp (S) 1^{st} (F) (w)) (X 2^{nd} (F) z) (k)$
99		eqid	$⊢ comp (C) = comp (C)$
100	2 99 4 91 92 94	oppcco	$⊢ ((φ \land (z \in B \land w \in B \land h \in (z Hom (O) w))) \land k \in (z Hom (C) X)) \to h (⟨X, z⟩ comp (O) w) k = k (⟨w, z⟩ comp (C) X) h$
101	100	fveq2d	$⊢ ((φ \land (z \in B \land w \in B \land h \in (z Hom (O) w))) \land k \in (z Hom (C) X)) \to (X 2^{nd} (F) w) (h (⟨X, z⟩ comp (O) w) k) = (X 2^{nd} (F) w) (k (⟨w, z⟩ comp (C) X) h)$
102	45	adantr	$⊢ (φ \land (z \in B \land w \in B \land h \in (z Hom (O) w))) \to U \in V$
103	102	adantr	$⊢ ((φ \land (z \in B \land w \in B \land h \in (z Hom (O) w))) \land k \in (z Hom (C) X)) \to U \in V$
104	53	ad2antrr	$⊢ ((φ \land (z \in B \land w \in B \land h \in (z Hom (O) w))) \land k \in (z Hom (C) X)) \to 1^{st} (F) (X) \in U$
105	55	3ad2antr1	$⊢ (φ \land (z \in B \land w \in B \land h \in (z Hom (O) w))) \to 1^{st} (F) (z) \in U$
106	105	adantr	$⊢ ((φ \land (z \in B \land w \in B \land h \in (z Hom (O) w))) \land k \in (z Hom (C) X)) \to 1^{st} (F) (z) \in U$
107	52	adantr	$⊢ (φ \land (z \in B \land w \in B \land h \in (z Hom (O) w))) \to 1^{st} (F) : B ⟶ U$
108	107 93	ffvelrnd	$⊢ (φ \land (z \in B \land w \in B \land h \in (z Hom (O) w))) \to 1^{st} (F) (w) \in U$
109	108	adantr	$⊢ ((φ \land (z \in B \land w \in B \land h \in (z Hom (O) w))) \land k \in (z Hom (C) X)) \to 1^{st} (F) (w) \in U$
110	28 29 30 89 82 83	funcf2	$⊢ (φ \land (z \in B \land w \in B \land h \in (z Hom (O) w))) \to (X 2^{nd} (F) z) : X Hom (O) z ⟶ 1^{st} (F) (X) Hom (S) 1^{st} (F) (z)$
111	110	adantr	$⊢ ((φ \land (z \in B \land w \in B \land h \in (z Hom (O) w))) \land k \in (z Hom (C) X)) \to (X 2^{nd} (F) z) : X Hom (O) z ⟶ 1^{st} (F) (X) Hom (S) 1^{st} (F) (z)$
112	111 96	ffvelrnd	$⊢ ((φ \land (z \in B \land w \in B \land h \in (z Hom (O) w))) \land k \in (z Hom (C) X)) \to (X 2^{nd} (F) z) (k) \in (1^{st} (F) (X) Hom (S) 1^{st} (F) (z))$
113	5 103 30 104 106	elsetchom	$⊢ ((φ \land (z \in B \land w \in B \land h \in (z Hom (O) w))) \land k \in (z Hom (C) X)) \to ((X 2^{nd} (F) z) (k) \in (1^{st} (F) (X) Hom (S) 1^{st} (F) (z)) \leftrightarrow (X 2^{nd} (F) z) (k) : 1^{st} (F) (X) ⟶ 1^{st} (F) (z))$
114	112 113	mpbid	$⊢ ((φ \land (z \in B \land w \in B \land h \in (z Hom (O) w))) \land k \in (z Hom (C) X)) \to (X 2^{nd} (F) z) (k) : 1^{st} (F) (X) ⟶ 1^{st} (F) (z)$
115	28 29 30 89 83 93	funcf2	$⊢ (φ \land (z \in B \land w \in B \land h \in (z Hom (O) w))) \to (z 2^{nd} (F) w) : z Hom (O) w ⟶ 1^{st} (F) (z) Hom (S) 1^{st} (F) (w)$
116		simpr3	$⊢ (φ \land (z \in B \land w \in B \land h \in (z Hom (O) w))) \to h \in (z Hom (O) w)$
117	115 116	ffvelrnd	$⊢ (φ \land (z \in B \land w \in B \land h \in (z Hom (O) w))) \to (z 2^{nd} (F) w) (h) \in (1^{st} (F) (z) Hom (S) 1^{st} (F) (w))$
118	5 102 30 105 108	elsetchom	$⊢ (φ \land (z \in B \land w \in B \land h \in (z Hom (O) w))) \to ((z 2^{nd} (F) w) (h) \in (1^{st} (F) (z) Hom (S) 1^{st} (F) (w)) \leftrightarrow (z 2^{nd} (F) w) (h) : 1^{st} (F) (z) ⟶ 1^{st} (F) (w))$
119	117 118	mpbid	$⊢ (φ \land (z \in B \land w \in B \land h \in (z Hom (O) w))) \to (z 2^{nd} (F) w) (h) : 1^{st} (F) (z) ⟶ 1^{st} (F) (w)$
120	119	adantr	$⊢ ((φ \land (z \in B \land w \in B \land h \in (z Hom (O) w))) \land k \in (z Hom (C) X)) \to (z 2^{nd} (F) w) (h) : 1^{st} (F) (z) ⟶ 1^{st} (F) (w)$
121	5 103 88 104 106 109 114 120	setcco	$⊢ ((φ \land (z \in B \land w \in B \land h \in (z Hom (O) w))) \land k \in (z Hom (C) X)) \to (z 2^{nd} (F) w) (h) (⟨1^{st} (F) (X), 1^{st} (F) (z)⟩ comp (S) 1^{st} (F) (w)) (X 2^{nd} (F) z) (k) = (z 2^{nd} (F) w) (h) \circ (X 2^{nd} (F) z) (k)$
122	98 101 121	3eqtr3d	$⊢ ((φ \land (z \in B \land w \in B \land h \in (z Hom (O) w))) \land k \in (z Hom (C) X)) \to (X 2^{nd} (F) w) (k (⟨w, z⟩ comp (C) X) h) = (z 2^{nd} (F) w) (h) \circ (X 2^{nd} (F) z) (k)$
123	122	fveq1d	$⊢ ((φ \land (z \in B \land w \in B \land h \in (z Hom (O) w))) \land k \in (z Hom (C) X)) \to (X 2^{nd} (F) w) (k (⟨w, z⟩ comp (C) X) h) (A) = ((z 2^{nd} (F) w) (h) \circ (X 2^{nd} (F) z) (k)) (A)$
124	19	ad2antrr	$⊢ ((φ \land (z \in B \land w \in B \land h \in (z Hom (O) w))) \land k \in (z Hom (C) X)) \to A \in 1^{st} (F) (X)$
125		fvco3	$⊢ ((X 2^{nd} (F) z) (k) : 1^{st} (F) (X) ⟶ 1^{st} (F) (z) \land A \in 1^{st} (F) (X)) \to ((z 2^{nd} (F) w) (h) \circ (X 2^{nd} (F) z) (k)) (A) = (z 2^{nd} (F) w) (h) ((X 2^{nd} (F) z) (k) (A))$
126	114 124 125	syl2anc	$⊢ ((φ \land (z \in B \land w \in B \land h \in (z Hom (O) w))) \land k \in (z Hom (C) X)) \to ((z 2^{nd} (F) w) (h) \circ (X 2^{nd} (F) z) (k)) (A) = (z 2^{nd} (F) w) (h) ((X 2^{nd} (F) z) (k) (A))$
127	123 126	eqtrd	$⊢ ((φ \land (z \in B \land w \in B \land h \in (z Hom (O) w))) \land k \in (z Hom (C) X)) \to (X 2^{nd} (F) w) (k (⟨w, z⟩ comp (C) X) h) (A) = (z 2^{nd} (F) w) (h) ((X 2^{nd} (F) z) (k) (A))$
128	81	adantr	$⊢ ((φ \land (z \in B \land w \in B \land h \in (z Hom (O) w))) \land k \in (z Hom (C) X)) \to C \in Cat$
129	40 4	oppchom	$⊢ z Hom (O) w = w Hom (C) z$
130	97 129	eleqtrdi	$⊢ ((φ \land (z \in B \land w \in B \land h \in (z Hom (O) w))) \land k \in (z Hom (C) X)) \to h \in (w Hom (C) z)$
131	1 2 128 91 40 92 99 94 130 95	yon12	$⊢ ((φ \land (z \in B \land w \in B \land h \in (z Hom (O) w))) \land k \in (z Hom (C) X)) \to (z 2^{nd} (1^{st} (Y) (X)) w) (h) (k) = k (⟨w, z⟩ comp (C) X) h$
132	131	fveq2d	$⊢ ((φ \land (z \in B \land w \in B \land h \in (z Hom (O) w))) \land k \in (z Hom (C) X)) \to (F N X) (A) (w) ((z 2^{nd} (1^{st} (Y) (X)) w) (h) (k)) = (F N X) (A) (w) (k (⟨w, z⟩ comp (C) X) h)$
133	13	ad2antrr	$⊢ ((φ \land (z \in B \land w \in B \land h \in (z Hom (O) w))) \land k \in (z Hom (C) X)) \to V \in W$
134	14	ad2antrr	$⊢ ((φ \land (z \in B \land w \in B \land h \in (z Hom (O) w))) \land k \in (z Hom (C) X)) \to ran {Hom}_{𝑓} (C) \subseteq U$
135	15	ad2antrr	$⊢ ((φ \land (z \in B \land w \in B \land h \in (z Hom (O) w))) \land k \in (z Hom (C) X)) \to ran {Hom}_{𝑓} (Q) \cup U \subseteq V$
136	16	ad2antrr	$⊢ ((φ \land (z \in B \land w \in B \land h \in (z Hom (O) w))) \land k \in (z Hom (C) X)) \to F \in (O Func S)$
137	2 40 99 128 94 92 91 130 95	catcocl	$⊢ ((φ \land (z \in B \land w \in B \land h \in (z Hom (O) w))) \land k \in (z Hom (C) X)) \to k (⟨w, z⟩ comp (C) X) h \in (w Hom (C) X)$
138	1 2 3 4 5 6 7 8 9 10 11 128 133 134 135 136 91 18 124 94 137	yonedalem4b	$⊢ ((φ \land (z \in B \land w \in B \land h \in (z Hom (O) w))) \land k \in (z Hom (C) X)) \to (F N X) (A) (w) (k (⟨w, z⟩ comp (C) X) h) = (X 2^{nd} (F) w) (k (⟨w, z⟩ comp (C) X) h) (A)$
139	132 138	eqtrd	$⊢ ((φ \land (z \in B \land w \in B \land h \in (z Hom (O) w))) \land k \in (z Hom (C) X)) \to (F N X) (A) (w) ((z 2^{nd} (1^{st} (Y) (X)) w) (h) (k)) = (X 2^{nd} (F) w) (k (⟨w, z⟩ comp (C) X) h) (A)$
140	1 2 3 4 5 6 7 8 9 10 11 128 133 134 135 136 91 18 124 92 95	yonedalem4b	$⊢ ((φ \land (z \in B \land w \in B \land h \in (z Hom (O) w))) \land k \in (z Hom (C) X)) \to (F N X) (A) (z) (k) = (X 2^{nd} (F) z) (k) (A)$
141	140	fveq2d	$⊢ ((φ \land (z \in B \land w \in B \land h \in (z Hom (O) w))) \land k \in (z Hom (C) X)) \to (z 2^{nd} (F) w) (h) ((F N X) (A) (z) (k)) = (z 2^{nd} (F) w) (h) ((X 2^{nd} (F) z) (k) (A))$
142	127 139 141	3eqtr4d	$⊢ ((φ \land (z \in B \land w \in B \land h \in (z Hom (O) w))) \land k \in (z Hom (C) X)) \to (F N X) (A) (w) ((z 2^{nd} (1^{st} (Y) (X)) w) (h) (k)) = (z 2^{nd} (F) w) (h) ((F N X) (A) (z) (k))$
143	86 142	syldan	$⊢ ((φ \land (z \in B \land w \in B \land h \in (z Hom (O) w))) \land k \in 1^{st} (1^{st} (Y) (X)) (z)) \to (F N X) (A) (w) ((z 2^{nd} (1^{st} (Y) (X)) w) (h) (k)) = (z 2^{nd} (F) w) (h) ((F N X) (A) (z) (k))$
144	143	mpteq2dva	$⊢ (φ \land (z \in B \land w \in B \land h \in (z Hom (O) w))) \to (k \in 1^{st} (1^{st} (Y) (X)) (z) ⟼ (F N X) (A) (w) ((z 2^{nd} (1^{st} (Y) (X)) w) (h) (k))) = (k \in 1^{st} (1^{st} (Y) (X)) (z) ⟼ (z 2^{nd} (F) w) (h) ((F N X) (A) (z) (k)))$
145		fveq2	$⊢ z = w \to (F N X) (A) (z) = (F N X) (A) (w)$
146		fveq2	$⊢ z = w \to 1^{st} (1^{st} (Y) (X)) (z) = 1^{st} (1^{st} (Y) (X)) (w)$
147		fveq2	$⊢ z = w \to 1^{st} (F) (z) = 1^{st} (F) (w)$
148	145 146 147	feq123d	$⊢ z = w \to ((F N X) (A) (z) : 1^{st} (1^{st} (Y) (X)) (z) ⟶ 1^{st} (F) (z) \leftrightarrow (F N X) (A) (w) : 1^{st} (1^{st} (Y) (X)) (w) ⟶ 1^{st} (F) (w))$
149	27	fveq1d	$⊢ φ \to (F N X) (A) (z) = (z \in B ⟼ (g \in (z Hom (C) X) ⟼ (X 2^{nd} (F) z) (g) (A))) (z)$
150		ovex	$⊢ z Hom (C) X \in V$
151	150	mptex	$⊢ (g \in (z Hom (C) X) ⟼ (X 2^{nd} (F) z) (g) (A)) \in V$
152		eqid	$⊢ (z \in B ⟼ (g \in (z Hom (C) X) ⟼ (X 2^{nd} (F) z) (g) (A))) = (z \in B ⟼ (g \in (z Hom (C) X) ⟼ (X 2^{nd} (F) z) (g) (A)))$
153	152	fvmpt2	$⊢ (z \in B \land (g \in (z Hom (C) X) ⟼ (X 2^{nd} (F) z) (g) (A)) \in V) \to (z \in B ⟼ (g \in (z Hom (C) X) ⟼ (X 2^{nd} (F) z) (g) (A))) (z) = (g \in (z Hom (C) X) ⟼ (X 2^{nd} (F) z) (g) (A))$
154	151 153	mpan2	$⊢ z \in B \to (z \in B ⟼ (g \in (z Hom (C) X) ⟼ (X 2^{nd} (F) z) (g) (A))) (z) = (g \in (z Hom (C) X) ⟼ (X 2^{nd} (F) z) (g) (A))$
155	149 154	sylan9eq	$⊢ (φ \land z \in B) \to (F N X) (A) (z) = (g \in (z Hom (C) X) ⟼ (X 2^{nd} (F) z) (g) (A))$
156	155	feq1d	$⊢ (φ \land z \in B) \to ((F N X) (A) (z) : 1^{st} (1^{st} (Y) (X)) (z) ⟶ 1^{st} (F) (z) \leftrightarrow (g \in (z Hom (C) X) ⟼ (X 2^{nd} (F) z) (g) (A)) : 1^{st} (1^{st} (Y) (X)) (z) ⟶ 1^{st} (F) (z))$
157	65 156	mpbird	$⊢ (φ \land z \in B) \to (F N X) (A) (z) : 1^{st} (1^{st} (Y) (X)) (z) ⟶ 1^{st} (F) (z)$
158	157	ralrimiva	$⊢ φ \to \forall z \in B (F N X) (A) (z) : 1^{st} (1^{st} (Y) (X)) (z) ⟶ 1^{st} (F) (z)$
159	158	adantr	$⊢ (φ \land (z \in B \land w \in B \land h \in (z Hom (O) w))) \to \forall z \in B (F N X) (A) (z) : 1^{st} (1^{st} (Y) (X)) (z) ⟶ 1^{st} (F) (z)$
160	148 159 93	rspcdva	$⊢ (φ \land (z \in B \land w \in B \land h \in (z Hom (O) w))) \to (F N X) (A) (w) : 1^{st} (1^{st} (Y) (X)) (w) ⟶ 1^{st} (F) (w)$
161	68	adantr	$⊢ (φ \land (z \in B \land w \in B \land h \in (z Hom (O) w))) \to 1^{st} (1^{st} (Y) (X)) (O Func S) 2^{nd} (1^{st} (Y) (X))$
162	28 29 30 161 83 93	funcf2	$⊢ (φ \land (z \in B \land w \in B \land h \in (z Hom (O) w))) \to (z 2^{nd} (1^{st} (Y) (X)) w) : z Hom (O) w ⟶ 1^{st} (1^{st} (Y) (X)) (z) Hom (S) 1^{st} (1^{st} (Y) (X)) (w)$
163	162 116	ffvelrnd	$⊢ (φ \land (z \in B \land w \in B \land h \in (z Hom (O) w))) \to (z 2^{nd} (1^{st} (Y) (X)) w) (h) \in (1^{st} (1^{st} (Y) (X)) (z) Hom (S) 1^{st} (1^{st} (Y) (X)) (w))$
164	72	3ad2antr1	$⊢ (φ \land (z \in B \land w \in B \land h \in (z Hom (O) w))) \to 1^{st} (1^{st} (Y) (X)) (z) \in U$
165	71	adantr	$⊢ (φ \land (z \in B \land w \in B \land h \in (z Hom (O) w))) \to 1^{st} (1^{st} (Y) (X)) : B ⟶ U$
166	165 93	ffvelrnd	$⊢ (φ \land (z \in B \land w \in B \land h \in (z Hom (O) w))) \to 1^{st} (1^{st} (Y) (X)) (w) \in U$
167	5 102 30 164 166	elsetchom	$⊢ (φ \land (z \in B \land w \in B \land h \in (z Hom (O) w))) \to ((z 2^{nd} (1^{st} (Y) (X)) w) (h) \in (1^{st} (1^{st} (Y) (X)) (z) Hom (S) 1^{st} (1^{st} (Y) (X)) (w)) \leftrightarrow (z 2^{nd} (1^{st} (Y) (X)) w) (h) : 1^{st} (1^{st} (Y) (X)) (z) ⟶ 1^{st} (1^{st} (Y) (X)) (w))$
168	163 167	mpbid	$⊢ (φ \land (z \in B \land w \in B \land h \in (z Hom (O) w))) \to (z 2^{nd} (1^{st} (Y) (X)) w) (h) : 1^{st} (1^{st} (Y) (X)) (z) ⟶ 1^{st} (1^{st} (Y) (X)) (w)$
169		fcompt	$⊢ ((F N X) (A) (w) : 1^{st} (1^{st} (Y) (X)) (w) ⟶ 1^{st} (F) (w) \land (z 2^{nd} (1^{st} (Y) (X)) w) (h) : 1^{st} (1^{st} (Y) (X)) (z) ⟶ 1^{st} (1^{st} (Y) (X)) (w)) \to (F N X) (A) (w) \circ (z 2^{nd} (1^{st} (Y) (X)) w) (h) = (k \in 1^{st} (1^{st} (Y) (X)) (z) ⟼ (F N X) (A) (w) ((z 2^{nd} (1^{st} (Y) (X)) w) (h) (k)))$
170	160 168 169	syl2anc	$⊢ (φ \land (z \in B \land w \in B \land h \in (z Hom (O) w))) \to (F N X) (A) (w) \circ (z 2^{nd} (1^{st} (Y) (X)) w) (h) = (k \in 1^{st} (1^{st} (Y) (X)) (z) ⟼ (F N X) (A) (w) ((z 2^{nd} (1^{st} (Y) (X)) w) (h) (k)))$
171	157	3ad2antr1	$⊢ (φ \land (z \in B \land w \in B \land h \in (z Hom (O) w))) \to (F N X) (A) (z) : 1^{st} (1^{st} (Y) (X)) (z) ⟶ 1^{st} (F) (z)$
172		fcompt	$⊢ ((z 2^{nd} (F) w) (h) : 1^{st} (F) (z) ⟶ 1^{st} (F) (w) \land (F N X) (A) (z) : 1^{st} (1^{st} (Y) (X)) (z) ⟶ 1^{st} (F) (z)) \to (z 2^{nd} (F) w) (h) \circ (F N X) (A) (z) = (k \in 1^{st} (1^{st} (Y) (X)) (z) ⟼ (z 2^{nd} (F) w) (h) ((F N X) (A) (z) (k)))$
173	119 171 172	syl2anc	$⊢ (φ \land (z \in B \land w \in B \land h \in (z Hom (O) w))) \to (z 2^{nd} (F) w) (h) \circ (F N X) (A) (z) = (k \in 1^{st} (1^{st} (Y) (X)) (z) ⟼ (z 2^{nd} (F) w) (h) ((F N X) (A) (z) (k)))$
174	144 170 173	3eqtr4d	$⊢ (φ \land (z \in B \land w \in B \land h \in (z Hom (O) w))) \to (F N X) (A) (w) \circ (z 2^{nd} (1^{st} (Y) (X)) w) (h) = (z 2^{nd} (F) w) (h) \circ (F N X) (A) (z)$
175	5 102 88 164 166 108 168 160	setcco	$⊢ (φ \land (z \in B \land w \in B \land h \in (z Hom (O) w))) \to (F N X) (A) (w) (⟨1^{st} (1^{st} (Y) (X)) (z), 1^{st} (1^{st} (Y) (X)) (w)⟩ comp (S) 1^{st} (F) (w)) (z 2^{nd} (1^{st} (Y) (X)) w) (h) = (F N X) (A) (w) \circ (z 2^{nd} (1^{st} (Y) (X)) w) (h)$
176	5 102 88 164 105 108 171 119	setcco	$⊢ (φ \land (z \in B \land w \in B \land h \in (z Hom (O) w))) \to (z 2^{nd} (F) w) (h) (⟨1^{st} (1^{st} (Y) (X)) (z), 1^{st} (F) (z)⟩ comp (S) 1^{st} (F) (w)) (F N X) (A) (z) = (z 2^{nd} (F) w) (h) \circ (F N X) (A) (z)$
177	174 175 176	3eqtr4d	$⊢ (φ \land (z \in B \land w \in B \land h \in (z Hom (O) w))) \to (F N X) (A) (w) (⟨1^{st} (1^{st} (Y) (X)) (z), 1^{st} (1^{st} (Y) (X)) (w)⟩ comp (S) 1^{st} (F) (w)) (z 2^{nd} (1^{st} (Y) (X)) w) (h) = (z 2^{nd} (F) w) (h) (⟨1^{st} (1^{st} (Y) (X)) (z), 1^{st} (F) (z)⟩ comp (S) 1^{st} (F) (w)) (F N X) (A) (z)$
178	177	ralrimivvva	$⊢ φ \to \forall z \in B \forall w \in B \forall h \in (z Hom (O) w) (F N X) (A) (w) (⟨1^{st} (1^{st} (Y) (X)) (z), 1^{st} (1^{st} (Y) (X)) (w)⟩ comp (S) 1^{st} (F) (w)) (z 2^{nd} (1^{st} (Y) (X)) w) (h) = (z 2^{nd} (F) w) (h) (⟨1^{st} (1^{st} (Y) (X)) (z), 1^{st} (F) (z)⟩ comp (S) 1^{st} (F) (w)) (F N X) (A) (z)$
179		eqid	$⊢ O Nat S = O Nat S$
180	179 28 29 30 88 66 16	isnat2	$⊢ φ \to ((F N X) (A) \in (1^{st} (Y) (X) (O Nat S) F) \leftrightarrow ((F N X) (A) \in \underset{z \in B}{⨉} (1^{st} (1^{st} (Y) (X)) (z) Hom (S) 1^{st} (F) (z)) \land \forall z \in B \forall w \in B \forall h \in (z Hom (O) w) (F N X) (A) (w) (⟨1^{st} (1^{st} (Y) (X)) (z), 1^{st} (1^{st} (Y) (X)) (w)⟩ comp (S) 1^{st} (F) (w)) (z 2^{nd} (1^{st} (Y) (X)) w) (h) = (z 2^{nd} (F) w) (h) (⟨1^{st} (1^{st} (Y) (X)) (z), 1^{st} (F) (z)⟩ comp (S) 1^{st} (F) (w)) (F N X) (A) (z)))$
181	80 178 180	mpbir2and	$⊢ φ \to (F N X) (A) \in (1^{st} (Y) (X) (O Nat S) F)$

Metamath Proof Explorer

Theorem yonedalem4c

Proof