yonedalem3

	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$
	yoneda.m	$⊢ M = (f \in (O Func S), x \in B ⟼ (a \in (1^{st} (Y) (x) (O Nat S) f) ⟼ a (x) (\underset{˙}{1} (x))))$
Assertion	yonedalem3	$⊢ φ \to M \in (Z ((Q \times_{c} O) Nat T) E)$

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		yoneda.m	$⊢ M = (f \in (O Func S), x \in B ⟼ (a \in (1^{st} (Y) (x) (O Nat S) f) ⟼ a (x) (\underset{˙}{1} (x))))$
17		ovex	$⊢ 1^{st} (Y) (x) (O Nat S) f \in V$
18	17	mptex	$⊢ (a \in (1^{st} (Y) (x) (O Nat S) f) ⟼ a (x) (\underset{˙}{1} (x))) \in V$
19	16 18	fnmpoi	$⊢ M Fn ((O Func S) \times B)$
20	19	a1i	$⊢ φ \to M Fn ((O Func S) \times B)$
21	12	adantr	$⊢ (φ \land (g \in (O Func S) \land y \in B)) \to C \in Cat$
22	13	adantr	$⊢ (φ \land (g \in (O Func S) \land y \in B)) \to V \in W$
23	14	adantr	$⊢ (φ \land (g \in (O Func S) \land y \in B)) \to ran {Hom}_{𝑓} (C) \subseteq U$
24	15	adantr	$⊢ (φ \land (g \in (O Func S) \land y \in B)) \to ran {Hom}_{𝑓} (Q) \cup U \subseteq V$
25		simprl	$⊢ (φ \land (g \in (O Func S) \land y \in B)) \to g \in (O Func S)$
26		simprr	$⊢ (φ \land (g \in (O Func S) \land y \in B)) \to y \in B$
27	1 2 3 4 5 6 7 8 9 10 11 21 22 23 24 25 26 16	yonedalem3a	$⊢ (φ \land (g \in (O Func S) \land y \in B)) \to (g M y = (a \in (1^{st} (Y) (y) (O Nat S) g) ⟼ a (y) (\underset{˙}{1} (y))) \land (g M y) : g 1^{st} (Z) y ⟶ g 1^{st} (E) y)$
28	27	simprd	$⊢ (φ \land (g \in (O Func S) \land y \in B)) \to (g M y) : g 1^{st} (Z) y ⟶ g 1^{st} (E) y$
29		eqid	$⊢ Hom (T) = Hom (T)$
30		eqid	$⊢ Q \times_{c} O = Q \times_{c} O$
31	7	fucbas	$⊢ O Func S = {Base}_{Q}$
32	4 2	oppcbas	$⊢ B = {Base}_{O}$
33	30 31 32	xpcbas	$⊢ (O Func S) \times B = {Base}_{(Q \times_{c} O)}$
34		eqid	$⊢ {Base}_{T} = {Base}_{T}$
35		relfunc	$⊢ Rel ((Q \times_{c} O) Func T)$
36	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15	yonedalem1	$⊢ φ \to (Z \in ((Q \times_{c} O) Func T) \land E \in ((Q \times_{c} O) Func T))$
37	36	simpld	$⊢ φ \to Z \in ((Q \times_{c} O) Func T)$
38		1st2ndbr	$⊢ (Rel ((Q \times_{c} O) Func T) \land Z \in ((Q \times_{c} O) Func T)) \to 1^{st} (Z) ((Q \times_{c} O) Func T) 2^{nd} (Z)$
39	35 37 38	sylancr	$⊢ φ \to 1^{st} (Z) ((Q \times_{c} O) Func T) 2^{nd} (Z)$
40	33 34 39	funcf1	$⊢ φ \to 1^{st} (Z) : (O Func S) \times B ⟶ {Base}_{T}$
41	40	fovrnda	$⊢ (φ \land (g \in (O Func S) \land y \in B)) \to g 1^{st} (Z) y \in {Base}_{T}$
42	6 22	setcbas	$⊢ (φ \land (g \in (O Func S) \land y \in B)) \to V = {Base}_{T}$
43	41 42	eleqtrrd	$⊢ (φ \land (g \in (O Func S) \land y \in B)) \to g 1^{st} (Z) y \in V$
44	36	simprd	$⊢ φ \to E \in ((Q \times_{c} O) Func T)$
45		1st2ndbr	$⊢ (Rel ((Q \times_{c} O) Func T) \land E \in ((Q \times_{c} O) Func T)) \to 1^{st} (E) ((Q \times_{c} O) Func T) 2^{nd} (E)$
46	35 44 45	sylancr	$⊢ φ \to 1^{st} (E) ((Q \times_{c} O) Func T) 2^{nd} (E)$
47	33 34 46	funcf1	$⊢ φ \to 1^{st} (E) : (O Func S) \times B ⟶ {Base}_{T}$
48	47	fovrnda	$⊢ (φ \land (g \in (O Func S) \land y \in B)) \to g 1^{st} (E) y \in {Base}_{T}$
49	48 42	eleqtrrd	$⊢ (φ \land (g \in (O Func S) \land y \in B)) \to g 1^{st} (E) y \in V$
50	6 22 29 43 49	elsetchom	$⊢ (φ \land (g \in (O Func S) \land y \in B)) \to (g M y \in ((g 1^{st} (Z) y) Hom (T) (g 1^{st} (E) y)) \leftrightarrow (g M y) : g 1^{st} (Z) y ⟶ g 1^{st} (E) y)$
51	28 50	mpbird	$⊢ (φ \land (g \in (O Func S) \land y \in B)) \to g M y \in ((g 1^{st} (Z) y) Hom (T) (g 1^{st} (E) y))$
52	51	ralrimivva	$⊢ φ \to \forall g \in (O Func S) \forall y \in B g M y \in ((g 1^{st} (Z) y) Hom (T) (g 1^{st} (E) y))$
53		fveq2	$⊢ z = ⟨g, y⟩ \to M (z) = M (⟨g, y⟩)$
54		df-ov	$⊢ g M y = M (⟨g, y⟩)$
55	53 54	syl6eqr	$⊢ z = ⟨g, y⟩ \to M (z) = g M y$
56		fveq2	$⊢ z = ⟨g, y⟩ \to 1^{st} (Z) (z) = 1^{st} (Z) (⟨g, y⟩)$
57		df-ov	$⊢ g 1^{st} (Z) y = 1^{st} (Z) (⟨g, y⟩)$
58	56 57	syl6eqr	$⊢ z = ⟨g, y⟩ \to 1^{st} (Z) (z) = g 1^{st} (Z) y$
59		fveq2	$⊢ z = ⟨g, y⟩ \to 1^{st} (E) (z) = 1^{st} (E) (⟨g, y⟩)$
60		df-ov	$⊢ g 1^{st} (E) y = 1^{st} (E) (⟨g, y⟩)$
61	59 60	syl6eqr	$⊢ z = ⟨g, y⟩ \to 1^{st} (E) (z) = g 1^{st} (E) y$
62	58 61	oveq12d	$⊢ z = ⟨g, y⟩ \to 1^{st} (Z) (z) Hom (T) 1^{st} (E) (z) = (g 1^{st} (Z) y) Hom (T) (g 1^{st} (E) y)$
63	55 62	eleq12d	$⊢ z = ⟨g, y⟩ \to (M (z) \in (1^{st} (Z) (z) Hom (T) 1^{st} (E) (z)) \leftrightarrow g M y \in ((g 1^{st} (Z) y) Hom (T) (g 1^{st} (E) y)))$
64	63	ralxp	$⊢ \forall z \in ((O Func S) \times B) M (z) \in (1^{st} (Z) (z) Hom (T) 1^{st} (E) (z)) \leftrightarrow \forall g \in (O Func S) \forall y \in B g M y \in ((g 1^{st} (Z) y) Hom (T) (g 1^{st} (E) y))$
65	52 64	sylibr	$⊢ φ \to \forall z \in ((O Func S) \times B) M (z) \in (1^{st} (Z) (z) Hom (T) 1^{st} (E) (z))$
66		ovex	$⊢ O Func S \in V$
67	2	fvexi	$⊢ B \in V$
68	66 67	mpoex	$⊢ (f \in (O Func S), x \in B ⟼ (a \in (1^{st} (Y) (x) (O Nat S) f) ⟼ a (x) (\underset{˙}{1} (x)))) \in V$
69	16 68	eqeltri	$⊢ M \in V$
70	69	elixp	$⊢ M \in \underset{z \in (O Func S) \times B}{⨉} (1^{st} (Z) (z) Hom (T) 1^{st} (E) (z)) \leftrightarrow (M Fn ((O Func S) \times B) \land \forall z \in ((O Func S) \times B) M (z) \in (1^{st} (Z) (z) Hom (T) 1^{st} (E) (z)))$
71	20 65 70	sylanbrc	$⊢ φ \to M \in \underset{z \in (O Func S) \times B}{⨉} (1^{st} (Z) (z) Hom (T) 1^{st} (E) (z))$
72	12	adantr	$⊢ (φ \land (z \in ((O Func S) \times B) \land w \in ((O Func S) \times B) \land g \in (z Hom (Q \times_{c} O) w))) \to C \in Cat$
73	13	adantr	$⊢ (φ \land (z \in ((O Func S) \times B) \land w \in ((O Func S) \times B) \land g \in (z Hom (Q \times_{c} O) w))) \to V \in W$
74	14	adantr	$⊢ (φ \land (z \in ((O Func S) \times B) \land w \in ((O Func S) \times B) \land g \in (z Hom (Q \times_{c} O) w))) \to ran {Hom}_{𝑓} (C) \subseteq U$
75	15	adantr	$⊢ (φ \land (z \in ((O Func S) \times B) \land w \in ((O Func S) \times B) \land g \in (z Hom (Q \times_{c} O) w))) \to ran {Hom}_{𝑓} (Q) \cup U \subseteq V$
76		simpr1	$⊢ (φ \land (z \in ((O Func S) \times B) \land w \in ((O Func S) \times B) \land g \in (z Hom (Q \times_{c} O) w))) \to z \in ((O Func S) \times B)$
77		xp1st	$⊢ z \in ((O Func S) \times B) \to 1^{st} (z) \in (O Func S)$
78	76 77	syl	$⊢ (φ \land (z \in ((O Func S) \times B) \land w \in ((O Func S) \times B) \land g \in (z Hom (Q \times_{c} O) w))) \to 1^{st} (z) \in (O Func S)$
79		xp2nd	$⊢ z \in ((O Func S) \times B) \to 2^{nd} (z) \in B$
80	76 79	syl	$⊢ (φ \land (z \in ((O Func S) \times B) \land w \in ((O Func S) \times B) \land g \in (z Hom (Q \times_{c} O) w))) \to 2^{nd} (z) \in B$
81		simpr2	$⊢ (φ \land (z \in ((O Func S) \times B) \land w \in ((O Func S) \times B) \land g \in (z Hom (Q \times_{c} O) w))) \to w \in ((O Func S) \times B)$
82		xp1st	$⊢ w \in ((O Func S) \times B) \to 1^{st} (w) \in (O Func S)$
83	81 82	syl	$⊢ (φ \land (z \in ((O Func S) \times B) \land w \in ((O Func S) \times B) \land g \in (z Hom (Q \times_{c} O) w))) \to 1^{st} (w) \in (O Func S)$
84		xp2nd	$⊢ w \in ((O Func S) \times B) \to 2^{nd} (w) \in B$
85	81 84	syl	$⊢ (φ \land (z \in ((O Func S) \times B) \land w \in ((O Func S) \times B) \land g \in (z Hom (Q \times_{c} O) w))) \to 2^{nd} (w) \in B$
86		simpr3	$⊢ (φ \land (z \in ((O Func S) \times B) \land w \in ((O Func S) \times B) \land g \in (z Hom (Q \times_{c} O) w))) \to g \in (z Hom (Q \times_{c} O) w)$
87		eqid	$⊢ O Nat S = O Nat S$
88	7 87	fuchom	$⊢ O Nat S = Hom (Q)$
89		eqid	$⊢ Hom (O) = Hom (O)$
90		eqid	$⊢ Hom (Q \times_{c} O) = Hom (Q \times_{c} O)$
91	30 33 88 89 90 76 81	xpchom	$⊢ (φ \land (z \in ((O Func S) \times B) \land w \in ((O Func S) \times B) \land g \in (z Hom (Q \times_{c} O) w))) \to z Hom (Q \times_{c} O) w = (1^{st} (z) (O Nat S) 1^{st} (w)) \times (2^{nd} (z) Hom (O) 2^{nd} (w))$
92		eqid	$⊢ Hom (C) = Hom (C)$
93	92 4	oppchom	$⊢ 2^{nd} (z) Hom (O) 2^{nd} (w) = 2^{nd} (w) Hom (C) 2^{nd} (z)$
94	93	xpeq2i	$⊢ (1^{st} (z) (O Nat S) 1^{st} (w)) \times (2^{nd} (z) Hom (O) 2^{nd} (w)) = (1^{st} (z) (O Nat S) 1^{st} (w)) \times (2^{nd} (w) Hom (C) 2^{nd} (z))$
95	91 94	syl6eq	$⊢ (φ \land (z \in ((O Func S) \times B) \land w \in ((O Func S) \times B) \land g \in (z Hom (Q \times_{c} O) w))) \to z Hom (Q \times_{c} O) w = (1^{st} (z) (O Nat S) 1^{st} (w)) \times (2^{nd} (w) Hom (C) 2^{nd} (z))$
96	86 95	eleqtrd	$⊢ (φ \land (z \in ((O Func S) \times B) \land w \in ((O Func S) \times B) \land g \in (z Hom (Q \times_{c} O) w))) \to g \in ((1^{st} (z) (O Nat S) 1^{st} (w)) \times (2^{nd} (w) Hom (C) 2^{nd} (z)))$
97		xp1st	$⊢ g \in ((1^{st} (z) (O Nat S) 1^{st} (w)) \times (2^{nd} (w) Hom (C) 2^{nd} (z))) \to 1^{st} (g) \in (1^{st} (z) (O Nat S) 1^{st} (w))$
98	96 97	syl	$⊢ (φ \land (z \in ((O Func S) \times B) \land w \in ((O Func S) \times B) \land g \in (z Hom (Q \times_{c} O) w))) \to 1^{st} (g) \in (1^{st} (z) (O Nat S) 1^{st} (w))$
99		xp2nd	$⊢ g \in ((1^{st} (z) (O Nat S) 1^{st} (w)) \times (2^{nd} (w) Hom (C) 2^{nd} (z))) \to 2^{nd} (g) \in (2^{nd} (w) Hom (C) 2^{nd} (z))$
100	96 99	syl	$⊢ (φ \land (z \in ((O Func S) \times B) \land w \in ((O Func S) \times B) \land g \in (z Hom (Q \times_{c} O) w))) \to 2^{nd} (g) \in (2^{nd} (w) Hom (C) 2^{nd} (z))$
101	1 2 3 4 5 6 7 8 9 10 11 72 73 74 75 78 80 83 85 98 100 16	yonedalem3b	$⊢ (φ \land (z \in ((O Func S) \times B) \land w \in ((O Func S) \times B) \land g \in (z Hom (Q \times_{c} O) w))) \to (1^{st} (w) M 2^{nd} (w)) (⟨1^{st} (z) 1^{st} (Z) 2^{nd} (z), 1^{st} (w) 1^{st} (Z) 2^{nd} (w)⟩ comp (T) (1^{st} (w) 1^{st} (E) 2^{nd} (w))) (1^{st} (g) (⟨1^{st} (z), 2^{nd} (z)⟩ 2^{nd} (Z) ⟨1^{st} (w), 2^{nd} (w)⟩) 2^{nd} (g)) = (1^{st} (g) (⟨1^{st} (z), 2^{nd} (z)⟩ 2^{nd} (E) ⟨1^{st} (w), 2^{nd} (w)⟩) 2^{nd} (g)) (⟨1^{st} (z) 1^{st} (Z) 2^{nd} (z), 1^{st} (z) 1^{st} (E) 2^{nd} (z)⟩ comp (T) (1^{st} (w) 1^{st} (E) 2^{nd} (w))) (1^{st} (z) M 2^{nd} (z))$
102		1st2nd2	$⊢ z \in ((O Func S) \times B) \to z = ⟨1^{st} (z), 2^{nd} (z)⟩$
103	76 102	syl	$⊢ (φ \land (z \in ((O Func S) \times B) \land w \in ((O Func S) \times B) \land g \in (z Hom (Q \times_{c} O) w))) \to z = ⟨1^{st} (z), 2^{nd} (z)⟩$
104	103	fveq2d	$⊢ (φ \land (z \in ((O Func S) \times B) \land w \in ((O Func S) \times B) \land g \in (z Hom (Q \times_{c} O) w))) \to 1^{st} (Z) (z) = 1^{st} (Z) (⟨1^{st} (z), 2^{nd} (z)⟩)$
105		df-ov	$⊢ 1^{st} (z) 1^{st} (Z) 2^{nd} (z) = 1^{st} (Z) (⟨1^{st} (z), 2^{nd} (z)⟩)$
106	104 105	syl6eqr	$⊢ (φ \land (z \in ((O Func S) \times B) \land w \in ((O Func S) \times B) \land g \in (z Hom (Q \times_{c} O) w))) \to 1^{st} (Z) (z) = 1^{st} (z) 1^{st} (Z) 2^{nd} (z)$
107		1st2nd2	$⊢ w \in ((O Func S) \times B) \to w = ⟨1^{st} (w), 2^{nd} (w)⟩$
108	81 107	syl	$⊢ (φ \land (z \in ((O Func S) \times B) \land w \in ((O Func S) \times B) \land g \in (z Hom (Q \times_{c} O) w))) \to w = ⟨1^{st} (w), 2^{nd} (w)⟩$
109	108	fveq2d	$⊢ (φ \land (z \in ((O Func S) \times B) \land w \in ((O Func S) \times B) \land g \in (z Hom (Q \times_{c} O) w))) \to 1^{st} (Z) (w) = 1^{st} (Z) (⟨1^{st} (w), 2^{nd} (w)⟩)$
110		df-ov	$⊢ 1^{st} (w) 1^{st} (Z) 2^{nd} (w) = 1^{st} (Z) (⟨1^{st} (w), 2^{nd} (w)⟩)$
111	109 110	syl6eqr	$⊢ (φ \land (z \in ((O Func S) \times B) \land w \in ((O Func S) \times B) \land g \in (z Hom (Q \times_{c} O) w))) \to 1^{st} (Z) (w) = 1^{st} (w) 1^{st} (Z) 2^{nd} (w)$
112	106 111	opeq12d	$⊢ (φ \land (z \in ((O Func S) \times B) \land w \in ((O Func S) \times B) \land g \in (z Hom (Q \times_{c} O) w))) \to ⟨1^{st} (Z) (z), 1^{st} (Z) (w)⟩ = ⟨1^{st} (z) 1^{st} (Z) 2^{nd} (z), 1^{st} (w) 1^{st} (Z) 2^{nd} (w)⟩$
113	108	fveq2d	$⊢ (φ \land (z \in ((O Func S) \times B) \land w \in ((O Func S) \times B) \land g \in (z Hom (Q \times_{c} O) w))) \to 1^{st} (E) (w) = 1^{st} (E) (⟨1^{st} (w), 2^{nd} (w)⟩)$
114		df-ov	$⊢ 1^{st} (w) 1^{st} (E) 2^{nd} (w) = 1^{st} (E) (⟨1^{st} (w), 2^{nd} (w)⟩)$
115	113 114	syl6eqr	$⊢ (φ \land (z \in ((O Func S) \times B) \land w \in ((O Func S) \times B) \land g \in (z Hom (Q \times_{c} O) w))) \to 1^{st} (E) (w) = 1^{st} (w) 1^{st} (E) 2^{nd} (w)$
116	112 115	oveq12d	$⊢ (φ \land (z \in ((O Func S) \times B) \land w \in ((O Func S) \times B) \land g \in (z Hom (Q \times_{c} O) w))) \to ⟨1^{st} (Z) (z), 1^{st} (Z) (w)⟩ comp (T) 1^{st} (E) (w) = ⟨1^{st} (z) 1^{st} (Z) 2^{nd} (z), 1^{st} (w) 1^{st} (Z) 2^{nd} (w)⟩ comp (T) (1^{st} (w) 1^{st} (E) 2^{nd} (w))$
117	108	fveq2d	$⊢ (φ \land (z \in ((O Func S) \times B) \land w \in ((O Func S) \times B) \land g \in (z Hom (Q \times_{c} O) w))) \to M (w) = M (⟨1^{st} (w), 2^{nd} (w)⟩)$
118		df-ov	$⊢ 1^{st} (w) M 2^{nd} (w) = M (⟨1^{st} (w), 2^{nd} (w)⟩)$
119	117 118	syl6eqr	$⊢ (φ \land (z \in ((O Func S) \times B) \land w \in ((O Func S) \times B) \land g \in (z Hom (Q \times_{c} O) w))) \to M (w) = 1^{st} (w) M 2^{nd} (w)$
120	103 108	oveq12d	$⊢ (φ \land (z \in ((O Func S) \times B) \land w \in ((O Func S) \times B) \land g \in (z Hom (Q \times_{c} O) w))) \to z 2^{nd} (Z) w = ⟨1^{st} (z), 2^{nd} (z)⟩ 2^{nd} (Z) ⟨1^{st} (w), 2^{nd} (w)⟩$
121		1st2nd2	$⊢ g \in ((1^{st} (z) (O Nat S) 1^{st} (w)) \times (2^{nd} (w) Hom (C) 2^{nd} (z))) \to g = ⟨1^{st} (g), 2^{nd} (g)⟩$
122	96 121	syl	$⊢ (φ \land (z \in ((O Func S) \times B) \land w \in ((O Func S) \times B) \land g \in (z Hom (Q \times_{c} O) w))) \to g = ⟨1^{st} (g), 2^{nd} (g)⟩$
123	120 122	fveq12d	$⊢ (φ \land (z \in ((O Func S) \times B) \land w \in ((O Func S) \times B) \land g \in (z Hom (Q \times_{c} O) w))) \to (z 2^{nd} (Z) w) (g) = (⟨1^{st} (z), 2^{nd} (z)⟩ 2^{nd} (Z) ⟨1^{st} (w), 2^{nd} (w)⟩) (⟨1^{st} (g), 2^{nd} (g)⟩)$
124		df-ov	$⊢ 1^{st} (g) (⟨1^{st} (z), 2^{nd} (z)⟩ 2^{nd} (Z) ⟨1^{st} (w), 2^{nd} (w)⟩) 2^{nd} (g) = (⟨1^{st} (z), 2^{nd} (z)⟩ 2^{nd} (Z) ⟨1^{st} (w), 2^{nd} (w)⟩) (⟨1^{st} (g), 2^{nd} (g)⟩)$
125	123 124	syl6eqr	$⊢ (φ \land (z \in ((O Func S) \times B) \land w \in ((O Func S) \times B) \land g \in (z Hom (Q \times_{c} O) w))) \to (z 2^{nd} (Z) w) (g) = 1^{st} (g) (⟨1^{st} (z), 2^{nd} (z)⟩ 2^{nd} (Z) ⟨1^{st} (w), 2^{nd} (w)⟩) 2^{nd} (g)$
126	116 119 125	oveq123d	$⊢ (φ \land (z \in ((O Func S) \times B) \land w \in ((O Func S) \times B) \land g \in (z Hom (Q \times_{c} O) w))) \to M (w) (⟨1^{st} (Z) (z), 1^{st} (Z) (w)⟩ comp (T) 1^{st} (E) (w)) (z 2^{nd} (Z) w) (g) = (1^{st} (w) M 2^{nd} (w)) (⟨1^{st} (z) 1^{st} (Z) 2^{nd} (z), 1^{st} (w) 1^{st} (Z) 2^{nd} (w)⟩ comp (T) (1^{st} (w) 1^{st} (E) 2^{nd} (w))) (1^{st} (g) (⟨1^{st} (z), 2^{nd} (z)⟩ 2^{nd} (Z) ⟨1^{st} (w), 2^{nd} (w)⟩) 2^{nd} (g))$
127	103	fveq2d	$⊢ (φ \land (z \in ((O Func S) \times B) \land w \in ((O Func S) \times B) \land g \in (z Hom (Q \times_{c} O) w))) \to 1^{st} (E) (z) = 1^{st} (E) (⟨1^{st} (z), 2^{nd} (z)⟩)$
128		df-ov	$⊢ 1^{st} (z) 1^{st} (E) 2^{nd} (z) = 1^{st} (E) (⟨1^{st} (z), 2^{nd} (z)⟩)$
129	127 128	syl6eqr	$⊢ (φ \land (z \in ((O Func S) \times B) \land w \in ((O Func S) \times B) \land g \in (z Hom (Q \times_{c} O) w))) \to 1^{st} (E) (z) = 1^{st} (z) 1^{st} (E) 2^{nd} (z)$
130	106 129	opeq12d	$⊢ (φ \land (z \in ((O Func S) \times B) \land w \in ((O Func S) \times B) \land g \in (z Hom (Q \times_{c} O) w))) \to ⟨1^{st} (Z) (z), 1^{st} (E) (z)⟩ = ⟨1^{st} (z) 1^{st} (Z) 2^{nd} (z), 1^{st} (z) 1^{st} (E) 2^{nd} (z)⟩$
131	130 115	oveq12d	$⊢ (φ \land (z \in ((O Func S) \times B) \land w \in ((O Func S) \times B) \land g \in (z Hom (Q \times_{c} O) w))) \to ⟨1^{st} (Z) (z), 1^{st} (E) (z)⟩ comp (T) 1^{st} (E) (w) = ⟨1^{st} (z) 1^{st} (Z) 2^{nd} (z), 1^{st} (z) 1^{st} (E) 2^{nd} (z)⟩ comp (T) (1^{st} (w) 1^{st} (E) 2^{nd} (w))$
132	103 108	oveq12d	$⊢ (φ \land (z \in ((O Func S) \times B) \land w \in ((O Func S) \times B) \land g \in (z Hom (Q \times_{c} O) w))) \to z 2^{nd} (E) w = ⟨1^{st} (z), 2^{nd} (z)⟩ 2^{nd} (E) ⟨1^{st} (w), 2^{nd} (w)⟩$
133	132 122	fveq12d	$⊢ (φ \land (z \in ((O Func S) \times B) \land w \in ((O Func S) \times B) \land g \in (z Hom (Q \times_{c} O) w))) \to (z 2^{nd} (E) w) (g) = (⟨1^{st} (z), 2^{nd} (z)⟩ 2^{nd} (E) ⟨1^{st} (w), 2^{nd} (w)⟩) (⟨1^{st} (g), 2^{nd} (g)⟩)$
134		df-ov	$⊢ 1^{st} (g) (⟨1^{st} (z), 2^{nd} (z)⟩ 2^{nd} (E) ⟨1^{st} (w), 2^{nd} (w)⟩) 2^{nd} (g) = (⟨1^{st} (z), 2^{nd} (z)⟩ 2^{nd} (E) ⟨1^{st} (w), 2^{nd} (w)⟩) (⟨1^{st} (g), 2^{nd} (g)⟩)$
135	133 134	syl6eqr	$⊢ (φ \land (z \in ((O Func S) \times B) \land w \in ((O Func S) \times B) \land g \in (z Hom (Q \times_{c} O) w))) \to (z 2^{nd} (E) w) (g) = 1^{st} (g) (⟨1^{st} (z), 2^{nd} (z)⟩ 2^{nd} (E) ⟨1^{st} (w), 2^{nd} (w)⟩) 2^{nd} (g)$
136	103	fveq2d	$⊢ (φ \land (z \in ((O Func S) \times B) \land w \in ((O Func S) \times B) \land g \in (z Hom (Q \times_{c} O) w))) \to M (z) = M (⟨1^{st} (z), 2^{nd} (z)⟩)$
137		df-ov	$⊢ 1^{st} (z) M 2^{nd} (z) = M (⟨1^{st} (z), 2^{nd} (z)⟩)$
138	136 137	syl6eqr	$⊢ (φ \land (z \in ((O Func S) \times B) \land w \in ((O Func S) \times B) \land g \in (z Hom (Q \times_{c} O) w))) \to M (z) = 1^{st} (z) M 2^{nd} (z)$
139	131 135 138	oveq123d	$⊢ (φ \land (z \in ((O Func S) \times B) \land w \in ((O Func S) \times B) \land g \in (z Hom (Q \times_{c} O) w))) \to (z 2^{nd} (E) w) (g) (⟨1^{st} (Z) (z), 1^{st} (E) (z)⟩ comp (T) 1^{st} (E) (w)) M (z) = (1^{st} (g) (⟨1^{st} (z), 2^{nd} (z)⟩ 2^{nd} (E) ⟨1^{st} (w), 2^{nd} (w)⟩) 2^{nd} (g)) (⟨1^{st} (z) 1^{st} (Z) 2^{nd} (z), 1^{st} (z) 1^{st} (E) 2^{nd} (z)⟩ comp (T) (1^{st} (w) 1^{st} (E) 2^{nd} (w))) (1^{st} (z) M 2^{nd} (z))$
140	101 126 139	3eqtr4d	$⊢ (φ \land (z \in ((O Func S) \times B) \land w \in ((O Func S) \times B) \land g \in (z Hom (Q \times_{c} O) w))) \to M (w) (⟨1^{st} (Z) (z), 1^{st} (Z) (w)⟩ comp (T) 1^{st} (E) (w)) (z 2^{nd} (Z) w) (g) = (z 2^{nd} (E) w) (g) (⟨1^{st} (Z) (z), 1^{st} (E) (z)⟩ comp (T) 1^{st} (E) (w)) M (z)$
141	140	ralrimivvva	$⊢ φ \to \forall z \in ((O Func S) \times B) \forall w \in ((O Func S) \times B) \forall g \in (z Hom (Q \times_{c} O) w) M (w) (⟨1^{st} (Z) (z), 1^{st} (Z) (w)⟩ comp (T) 1^{st} (E) (w)) (z 2^{nd} (Z) w) (g) = (z 2^{nd} (E) w) (g) (⟨1^{st} (Z) (z), 1^{st} (E) (z)⟩ comp (T) 1^{st} (E) (w)) M (z)$
142		eqid	$⊢ (Q \times_{c} O) Nat T = (Q \times_{c} O) Nat T$
143		eqid	$⊢ comp (T) = comp (T)$
144	142 33 90 29 143 37 44	isnat2	$⊢ φ \to (M \in (Z ((Q \times_{c} O) Nat T) E) \leftrightarrow (M \in \underset{z \in (O Func S) \times B}{⨉} (1^{st} (Z) (z) Hom (T) 1^{st} (E) (z)) \land \forall z \in ((O Func S) \times B) \forall w \in ((O Func S) \times B) \forall g \in (z Hom (Q \times_{c} O) w) M (w) (⟨1^{st} (Z) (z), 1^{st} (Z) (w)⟩ comp (T) 1^{st} (E) (w)) (z 2^{nd} (Z) w) (g) = (z 2^{nd} (E) w) (g) (⟨1^{st} (Z) (z), 1^{st} (E) (z)⟩ comp (T) 1^{st} (E) (w)) M (z)))$
145	71 141 144	mpbir2and	$⊢ φ \to M \in (Z ((Q \times_{c} O) Nat T) E)$

Metamath Proof Explorer

Theorem yonedalem3

Proof