yonedainv

Description: The Yoneda Lemma with explicit inverse. (Contributed by Mario Carneiro, 29-Jan-2017)

	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))))$
	yonedainv.i	$⊢ I = Inv (R)$
	yonedainv.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)))))$
Assertion	yonedainv	$⊢ φ \to M (Z I E) N$

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		yonedainv.i	$⊢ I = Inv (R)$
18		yonedainv.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		eqid	$⊢ Q \times_{c} O = Q \times_{c} O$
20	7	fucbas	$⊢ O Func S = {Base}_{Q}$
21	4 2	oppcbas	$⊢ B = {Base}_{O}$
22	19 20 21	xpcbas	$⊢ (O Func S) \times B = {Base}_{(Q \times_{c} O)}$
23		eqid	$⊢ (Q \times_{c} O) Nat T = (Q \times_{c} O) Nat T$
24	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))$
25	24	simpld	$⊢ φ \to Z \in ((Q \times_{c} O) Func T)$
26	24	simprd	$⊢ φ \to E \in ((Q \times_{c} O) Func T)$
27		eqid	$⊢ Inv (T) = Inv (T)$
28	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16	yonedalem3	$⊢ φ \to M \in (Z ((Q \times_{c} O) Nat T) E)$
29	12	adantr	$⊢ (φ \land (h \in (O Func S) \land w \in B)) \to C \in Cat$
30	13	adantr	$⊢ (φ \land (h \in (O Func S) \land w \in B)) \to V \in W$
31	14	adantr	$⊢ (φ \land (h \in (O Func S) \land w \in B)) \to ran {Hom}_{𝑓} (C) \subseteq U$
32	15	adantr	$⊢ (φ \land (h \in (O Func S) \land w \in B)) \to ran {Hom}_{𝑓} (Q) \cup U \subseteq V$
33		simprl	$⊢ (φ \land (h \in (O Func S) \land w \in B)) \to h \in (O Func S)$
34		simprr	$⊢ (φ \land (h \in (O Func S) \land w \in B)) \to w \in B$
35	1 2 3 4 5 6 7 8 9 10 11 29 30 31 32 33 34 16	yonedalem3a	$⊢ (φ \land (h \in (O Func S) \land w \in B)) \to (h M w = (a \in (1^{st} (Y) (w) (O Nat S) h) ⟼ a (w) (\underset{˙}{1} (w))) \land (h M w) : h 1^{st} (Z) w ⟶ h 1^{st} (E) w)$
36	35	simprd	$⊢ (φ \land (h \in (O Func S) \land w \in B)) \to (h M w) : h 1^{st} (Z) w ⟶ h 1^{st} (E) w$
37	29	adantr	$⊢ ((φ \land (h \in (O Func S) \land w \in B)) \land b \in 1^{st} (h) (w)) \to C \in Cat$
38	30	adantr	$⊢ ((φ \land (h \in (O Func S) \land w \in B)) \land b \in 1^{st} (h) (w)) \to V \in W$
39	31	adantr	$⊢ ((φ \land (h \in (O Func S) \land w \in B)) \land b \in 1^{st} (h) (w)) \to ran {Hom}_{𝑓} (C) \subseteq U$
40	32	adantr	$⊢ ((φ \land (h \in (O Func S) \land w \in B)) \land b \in 1^{st} (h) (w)) \to ran {Hom}_{𝑓} (Q) \cup U \subseteq V$
41		simplrl	$⊢ ((φ \land (h \in (O Func S) \land w \in B)) \land b \in 1^{st} (h) (w)) \to h \in (O Func S)$
42		simplrr	$⊢ ((φ \land (h \in (O Func S) \land w \in B)) \land b \in 1^{st} (h) (w)) \to w \in B$
43		simpr	$⊢ ((φ \land (h \in (O Func S) \land w \in B)) \land b \in 1^{st} (h) (w)) \to b \in 1^{st} (h) (w)$
44	1 2 3 4 5 6 7 8 9 10 11 37 38 39 40 41 42 18 43	yonedalem4c	$⊢ ((φ \land (h \in (O Func S) \land w \in B)) \land b \in 1^{st} (h) (w)) \to (h N w) (b) \in (1^{st} (Y) (w) (O Nat S) h)$
45	44	fmpttd	$⊢ (φ \land (h \in (O Func S) \land w \in B)) \to (b \in 1^{st} (h) (w) ⟼ (h N w) (b)) : 1^{st} (h) (w) ⟶ 1^{st} (Y) (w) (O Nat S) h$
46	2	fvexi	$⊢ B \in V$
47	46	mptex	$⊢ (y \in B ⟼ (g \in (y Hom (C) w) ⟼ (w 2^{nd} (h) y) (g) (u))) \in V$
48		eqid	$⊢ (u \in 1^{st} (h) (w) ⟼ (y \in B ⟼ (g \in (y Hom (C) w) ⟼ (w 2^{nd} (h) y) (g) (u)))) = (u \in 1^{st} (h) (w) ⟼ (y \in B ⟼ (g \in (y Hom (C) w) ⟼ (w 2^{nd} (h) y) (g) (u))))$
49	47 48	fnmpti	$⊢ (u \in 1^{st} (h) (w) ⟼ (y \in B ⟼ (g \in (y Hom (C) w) ⟼ (w 2^{nd} (h) y) (g) (u)))) Fn 1^{st} (h) (w)$
50		simpl	$⊢ (f = h \land x = w) \to f = h$
51	50	fveq2d	$⊢ (f = h \land x = w) \to 1^{st} (f) = 1^{st} (h)$
52		simpr	$⊢ (f = h \land x = w) \to x = w$
53	51 52	fveq12d	$⊢ (f = h \land x = w) \to 1^{st} (f) (x) = 1^{st} (h) (w)$
54		simplr	$⊢ ((f = h \land x = w) \land y \in B) \to x = w$
55	54	oveq2d	$⊢ ((f = h \land x = w) \land y \in B) \to y Hom (C) x = y Hom (C) w$
56		simpll	$⊢ ((f = h \land x = w) \land y \in B) \to f = h$
57	56	fveq2d	$⊢ ((f = h \land x = w) \land y \in B) \to 2^{nd} (f) = 2^{nd} (h)$
58		eqidd	$⊢ ((f = h \land x = w) \land y \in B) \to y = y$
59	57 54 58	oveq123d	$⊢ ((f = h \land x = w) \land y \in B) \to x 2^{nd} (f) y = w 2^{nd} (h) y$
60	59	fveq1d	$⊢ ((f = h \land x = w) \land y \in B) \to (x 2^{nd} (f) y) (g) = (w 2^{nd} (h) y) (g)$
61	60	fveq1d	$⊢ ((f = h \land x = w) \land y \in B) \to (x 2^{nd} (f) y) (g) (u) = (w 2^{nd} (h) y) (g) (u)$
62	55 61	mpteq12dv	$⊢ ((f = h \land x = w) \land y \in B) \to (g \in (y Hom (C) x) ⟼ (x 2^{nd} (f) y) (g) (u)) = (g \in (y Hom (C) w) ⟼ (w 2^{nd} (h) y) (g) (u))$
63	62	mpteq2dva	$⊢ (f = h \land x = w) \to (y \in B ⟼ (g \in (y Hom (C) x) ⟼ (x 2^{nd} (f) y) (g) (u))) = (y \in B ⟼ (g \in (y Hom (C) w) ⟼ (w 2^{nd} (h) y) (g) (u)))$
64	53 63	mpteq12dv	$⊢ (f = h \land x = w) \to (u \in 1^{st} (f) (x) ⟼ (y \in B ⟼ (g \in (y Hom (C) x) ⟼ (x 2^{nd} (f) y) (g) (u)))) = (u \in 1^{st} (h) (w) ⟼ (y \in B ⟼ (g \in (y Hom (C) w) ⟼ (w 2^{nd} (h) y) (g) (u))))$
65		fvex	$⊢ 1^{st} (h) (w) \in V$
66	65	mptex	$⊢ (u \in 1^{st} (h) (w) ⟼ (y \in B ⟼ (g \in (y Hom (C) w) ⟼ (w 2^{nd} (h) y) (g) (u)))) \in V$
67	64 18 66	ovmpoa	$⊢ (h \in (O Func S) \land w \in B) \to h N w = (u \in 1^{st} (h) (w) ⟼ (y \in B ⟼ (g \in (y Hom (C) w) ⟼ (w 2^{nd} (h) y) (g) (u))))$
68	67	adantl	$⊢ (φ \land (h \in (O Func S) \land w \in B)) \to h N w = (u \in 1^{st} (h) (w) ⟼ (y \in B ⟼ (g \in (y Hom (C) w) ⟼ (w 2^{nd} (h) y) (g) (u))))$
69	68	fneq1d	$⊢ (φ \land (h \in (O Func S) \land w \in B)) \to ((h N w) Fn 1^{st} (h) (w) \leftrightarrow (u \in 1^{st} (h) (w) ⟼ (y \in B ⟼ (g \in (y Hom (C) w) ⟼ (w 2^{nd} (h) y) (g) (u)))) Fn 1^{st} (h) (w))$
70	49 69	mpbiri	$⊢ (φ \land (h \in (O Func S) \land w \in B)) \to (h N w) Fn 1^{st} (h) (w)$
71		dffn5	$⊢ (h N w) Fn 1^{st} (h) (w) \leftrightarrow h N w = (b \in 1^{st} (h) (w) ⟼ (h N w) (b))$
72	70 71	sylib	$⊢ (φ \land (h \in (O Func S) \land w \in B)) \to h N w = (b \in 1^{st} (h) (w) ⟼ (h N w) (b))$
73	4	oppccat	$⊢ C \in Cat \to O \in Cat$
74	12 73	syl	$⊢ φ \to O \in Cat$
75	74	adantr	$⊢ (φ \land (h \in (O Func S) \land w \in B)) \to O \in Cat$
76	15	unssbd	$⊢ φ \to U \subseteq V$
77	13 76	ssexd	$⊢ φ \to U \in V$
78	5	setccat	$⊢ U \in V \to S \in Cat$
79	77 78	syl	$⊢ φ \to S \in Cat$
80	79	adantr	$⊢ (φ \land (h \in (O Func S) \land w \in B)) \to S \in Cat$
81	10 75 80 21 33 34	evlf1	$⊢ (φ \land (h \in (O Func S) \land w \in B)) \to h 1^{st} (E) w = 1^{st} (h) (w)$
82	1 2 3 4 5 6 7 8 9 10 11 29 30 31 32 33 34	yonedalem21	$⊢ (φ \land (h \in (O Func S) \land w \in B)) \to h 1^{st} (Z) w = 1^{st} (Y) (w) (O Nat S) h$
83	72 81 82	feq123d	$⊢ (φ \land (h \in (O Func S) \land w \in B)) \to ((h N w) : h 1^{st} (E) w ⟶ h 1^{st} (Z) w \leftrightarrow (b \in 1^{st} (h) (w) ⟼ (h N w) (b)) : 1^{st} (h) (w) ⟶ 1^{st} (Y) (w) (O Nat S) h)$
84	45 83	mpbird	$⊢ (φ \land (h \in (O Func S) \land w \in B)) \to (h N w) : h 1^{st} (E) w ⟶ h 1^{st} (Z) w$
85		fcompt	$⊢ ((h M w) : h 1^{st} (Z) w ⟶ h 1^{st} (E) w \land (h N w) : h 1^{st} (E) w ⟶ h 1^{st} (Z) w) \to (h M w) \circ (h N w) = (k \in (h 1^{st} (E) w) ⟼ (h M w) ((h N w) (k)))$
86	36 84 85	syl2anc	$⊢ (φ \land (h \in (O Func S) \land w \in B)) \to (h M w) \circ (h N w) = (k \in (h 1^{st} (E) w) ⟼ (h M w) ((h N w) (k)))$
87	81	eleq2d	$⊢ (φ \land (h \in (O Func S) \land w \in B)) \to (k \in (h 1^{st} (E) w) \leftrightarrow k \in 1^{st} (h) (w))$
88	87	biimpa	$⊢ ((φ \land (h \in (O Func S) \land w \in B)) \land k \in (h 1^{st} (E) w)) \to k \in 1^{st} (h) (w)$
89	29	adantr	$⊢ ((φ \land (h \in (O Func S) \land w \in B)) \land k \in 1^{st} (h) (w)) \to C \in Cat$
90	30	adantr	$⊢ ((φ \land (h \in (O Func S) \land w \in B)) \land k \in 1^{st} (h) (w)) \to V \in W$
91	31	adantr	$⊢ ((φ \land (h \in (O Func S) \land w \in B)) \land k \in 1^{st} (h) (w)) \to ran {Hom}_{𝑓} (C) \subseteq U$
92	32	adantr	$⊢ ((φ \land (h \in (O Func S) \land w \in B)) \land k \in 1^{st} (h) (w)) \to ran {Hom}_{𝑓} (Q) \cup U \subseteq V$
93		simplrl	$⊢ ((φ \land (h \in (O Func S) \land w \in B)) \land k \in 1^{st} (h) (w)) \to h \in (O Func S)$
94		simplrr	$⊢ ((φ \land (h \in (O Func S) \land w \in B)) \land k \in 1^{st} (h) (w)) \to w \in B$
95	1 2 3 4 5 6 7 8 9 10 11 89 90 91 92 93 94 16	yonedalem3a	$⊢ ((φ \land (h \in (O Func S) \land w \in B)) \land k \in 1^{st} (h) (w)) \to (h M w = (a \in (1^{st} (Y) (w) (O Nat S) h) ⟼ a (w) (\underset{˙}{1} (w))) \land (h M w) : h 1^{st} (Z) w ⟶ h 1^{st} (E) w)$
96	95	simpld	$⊢ ((φ \land (h \in (O Func S) \land w \in B)) \land k \in 1^{st} (h) (w)) \to h M w = (a \in (1^{st} (Y) (w) (O Nat S) h) ⟼ a (w) (\underset{˙}{1} (w)))$
97	96	fveq1d	$⊢ ((φ \land (h \in (O Func S) \land w \in B)) \land k \in 1^{st} (h) (w)) \to (h M w) ((h N w) (k)) = (a \in (1^{st} (Y) (w) (O Nat S) h) ⟼ a (w) (\underset{˙}{1} (w))) ((h N w) (k))$
98	72 44	fmpt3d	$⊢ (φ \land (h \in (O Func S) \land w \in B)) \to (h N w) : 1^{st} (h) (w) ⟶ 1^{st} (Y) (w) (O Nat S) h$
99	98	ffvelrnda	$⊢ ((φ \land (h \in (O Func S) \land w \in B)) \land k \in 1^{st} (h) (w)) \to (h N w) (k) \in (1^{st} (Y) (w) (O Nat S) h)$
100		fveq1	$⊢ a = (h N w) (k) \to a (w) = (h N w) (k) (w)$
101	100	fveq1d	$⊢ a = (h N w) (k) \to a (w) (\underset{˙}{1} (w)) = (h N w) (k) (w) (\underset{˙}{1} (w))$
102		eqid	$⊢ (a \in (1^{st} (Y) (w) (O Nat S) h) ⟼ a (w) (\underset{˙}{1} (w))) = (a \in (1^{st} (Y) (w) (O Nat S) h) ⟼ a (w) (\underset{˙}{1} (w)))$
103		fvex	$⊢ (h N w) (k) (w) (\underset{˙}{1} (w)) \in V$
104	101 102 103	fvmpt	$⊢ (h N w) (k) \in (1^{st} (Y) (w) (O Nat S) h) \to (a \in (1^{st} (Y) (w) (O Nat S) h) ⟼ a (w) (\underset{˙}{1} (w))) ((h N w) (k)) = (h N w) (k) (w) (\underset{˙}{1} (w))$
105	99 104	syl	$⊢ ((φ \land (h \in (O Func S) \land w \in B)) \land k \in 1^{st} (h) (w)) \to (a \in (1^{st} (Y) (w) (O Nat S) h) ⟼ a (w) (\underset{˙}{1} (w))) ((h N w) (k)) = (h N w) (k) (w) (\underset{˙}{1} (w))$
106		simpr	$⊢ ((φ \land (h \in (O Func S) \land w \in B)) \land k \in 1^{st} (h) (w)) \to k \in 1^{st} (h) (w)$
107		eqid	$⊢ Hom (C) = Hom (C)$
108	2 107 3 89 94	catidcl	$⊢ ((φ \land (h \in (O Func S) \land w \in B)) \land k \in 1^{st} (h) (w)) \to \underset{˙}{1} (w) \in (w Hom (C) w)$
109	1 2 3 4 5 6 7 8 9 10 11 89 90 91 92 93 94 18 106 94 108	yonedalem4b	$⊢ ((φ \land (h \in (O Func S) \land w \in B)) \land k \in 1^{st} (h) (w)) \to (h N w) (k) (w) (\underset{˙}{1} (w)) = (w 2^{nd} (h) w) (\underset{˙}{1} (w)) (k)$
110		eqid	$⊢ Id (O) = Id (O)$
111		eqid	$⊢ Id (S) = Id (S)$
112		relfunc	$⊢ Rel (O Func S)$
113		1st2ndbr	$⊢ (Rel (O Func S) \land h \in (O Func S)) \to 1^{st} (h) (O Func S) 2^{nd} (h)$
114	112 93 113	sylancr	$⊢ ((φ \land (h \in (O Func S) \land w \in B)) \land k \in 1^{st} (h) (w)) \to 1^{st} (h) (O Func S) 2^{nd} (h)$
115	21 110 111 114 94	funcid	$⊢ ((φ \land (h \in (O Func S) \land w \in B)) \land k \in 1^{st} (h) (w)) \to (w 2^{nd} (h) w) (Id (O) (w)) = Id (S) (1^{st} (h) (w))$
116	4 3	oppcid	$⊢ C \in Cat \to Id (O) = \underset{˙}{1}$
117	89 116	syl	$⊢ ((φ \land (h \in (O Func S) \land w \in B)) \land k \in 1^{st} (h) (w)) \to Id (O) = \underset{˙}{1}$
118	117	fveq1d	$⊢ ((φ \land (h \in (O Func S) \land w \in B)) \land k \in 1^{st} (h) (w)) \to Id (O) (w) = \underset{˙}{1} (w)$
119	118	fveq2d	$⊢ ((φ \land (h \in (O Func S) \land w \in B)) \land k \in 1^{st} (h) (w)) \to (w 2^{nd} (h) w) (Id (O) (w)) = (w 2^{nd} (h) w) (\underset{˙}{1} (w))$
120	77	ad2antrr	$⊢ ((φ \land (h \in (O Func S) \land w \in B)) \land k \in 1^{st} (h) (w)) \to U \in V$
121		eqid	$⊢ {Base}_{S} = {Base}_{S}$
122	21 121 114	funcf1	$⊢ ((φ \land (h \in (O Func S) \land w \in B)) \land k \in 1^{st} (h) (w)) \to 1^{st} (h) : B ⟶ {Base}_{S}$
123	5 120	setcbas	$⊢ ((φ \land (h \in (O Func S) \land w \in B)) \land k \in 1^{st} (h) (w)) \to U = {Base}_{S}$
124	123	feq3d	$⊢ ((φ \land (h \in (O Func S) \land w \in B)) \land k \in 1^{st} (h) (w)) \to (1^{st} (h) : B ⟶ U \leftrightarrow 1^{st} (h) : B ⟶ {Base}_{S})$
125	122 124	mpbird	$⊢ ((φ \land (h \in (O Func S) \land w \in B)) \land k \in 1^{st} (h) (w)) \to 1^{st} (h) : B ⟶ U$
126	125 94	ffvelrnd	$⊢ ((φ \land (h \in (O Func S) \land w \in B)) \land k \in 1^{st} (h) (w)) \to 1^{st} (h) (w) \in U$
127	5 111 120 126	setcid	$⊢ ((φ \land (h \in (O Func S) \land w \in B)) \land k \in 1^{st} (h) (w)) \to Id (S) (1^{st} (h) (w)) = {I ↾}_{1^{st} (h) (w)}$
128	115 119 127	3eqtr3d	$⊢ ((φ \land (h \in (O Func S) \land w \in B)) \land k \in 1^{st} (h) (w)) \to (w 2^{nd} (h) w) (\underset{˙}{1} (w)) = {I ↾}_{1^{st} (h) (w)}$
129	128	fveq1d	$⊢ ((φ \land (h \in (O Func S) \land w \in B)) \land k \in 1^{st} (h) (w)) \to (w 2^{nd} (h) w) (\underset{˙}{1} (w)) (k) = ({I ↾}_{1^{st} (h) (w)}) (k)$
130		fvresi	$⊢ k \in 1^{st} (h) (w) \to ({I ↾}_{1^{st} (h) (w)}) (k) = k$
131	130	adantl	$⊢ ((φ \land (h \in (O Func S) \land w \in B)) \land k \in 1^{st} (h) (w)) \to ({I ↾}_{1^{st} (h) (w)}) (k) = k$
132	109 129 131	3eqtrd	$⊢ ((φ \land (h \in (O Func S) \land w \in B)) \land k \in 1^{st} (h) (w)) \to (h N w) (k) (w) (\underset{˙}{1} (w)) = k$
133	97 105 132	3eqtrd	$⊢ ((φ \land (h \in (O Func S) \land w \in B)) \land k \in 1^{st} (h) (w)) \to (h M w) ((h N w) (k)) = k$
134	88 133	syldan	$⊢ ((φ \land (h \in (O Func S) \land w \in B)) \land k \in (h 1^{st} (E) w)) \to (h M w) ((h N w) (k)) = k$
135	134	mpteq2dva	$⊢ (φ \land (h \in (O Func S) \land w \in B)) \to (k \in (h 1^{st} (E) w) ⟼ (h M w) ((h N w) (k))) = (k \in (h 1^{st} (E) w) ⟼ k)$
136		mptresid	$⊢ {I ↾}_{(h 1^{st} (E) w)} = (k \in (h 1^{st} (E) w) ⟼ k)$
137	135 136	eqtr4di	$⊢ (φ \land (h \in (O Func S) \land w \in B)) \to (k \in (h 1^{st} (E) w) ⟼ (h M w) ((h N w) (k))) = {I ↾}_{(h 1^{st} (E) w)}$
138	86 137	eqtrd	$⊢ (φ \land (h \in (O Func S) \land w \in B)) \to (h M w) \circ (h N w) = {I ↾}_{(h 1^{st} (E) w)}$
139		fcompt	$⊢ ((h N w) : h 1^{st} (E) w ⟶ h 1^{st} (Z) w \land (h M w) : h 1^{st} (Z) w ⟶ h 1^{st} (E) w) \to (h N w) \circ (h M w) = (b \in (h 1^{st} (Z) w) ⟼ (h N w) ((h M w) (b)))$
140	84 36 139	syl2anc	$⊢ (φ \land (h \in (O Func S) \land w \in B)) \to (h N w) \circ (h M w) = (b \in (h 1^{st} (Z) w) ⟼ (h N w) ((h M w) (b)))$
141		eqid	$⊢ O Nat S = O Nat S$
142	29	adantr	$⊢ ((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \to C \in Cat$
143	30	adantr	$⊢ ((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \to V \in W$
144	31	adantr	$⊢ ((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \to ran {Hom}_{𝑓} (C) \subseteq U$
145	32	adantr	$⊢ ((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \to ran {Hom}_{𝑓} (Q) \cup U \subseteq V$
146		simplrl	$⊢ ((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \to h \in (O Func S)$
147		simplrr	$⊢ ((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \to w \in B$
148	81	feq3d	$⊢ (φ \land (h \in (O Func S) \land w \in B)) \to ((h M w) : h 1^{st} (Z) w ⟶ h 1^{st} (E) w \leftrightarrow (h M w) : h 1^{st} (Z) w ⟶ 1^{st} (h) (w))$
149	36 148	mpbid	$⊢ (φ \land (h \in (O Func S) \land w \in B)) \to (h M w) : h 1^{st} (Z) w ⟶ 1^{st} (h) (w)$
150	149	ffvelrnda	$⊢ ((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \to (h M w) (b) \in 1^{st} (h) (w)$
151	1 2 3 4 5 6 7 8 9 10 11 142 143 144 145 146 147 18 150	yonedalem4c	$⊢ ((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \to (h N w) ((h M w) (b)) \in (1^{st} (Y) (w) (O Nat S) h)$
152	141 151	nat1st2nd	$⊢ ((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \to (h N w) ((h M w) (b)) \in (⟨1^{st} (1^{st} (Y) (w)), 2^{nd} (1^{st} (Y) (w))⟩ (O Nat S) ⟨1^{st} (h), 2^{nd} (h)⟩)$
153	141 152 21	natfn	$⊢ ((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \to (h N w) ((h M w) (b)) Fn B$
154	82	eleq2d	$⊢ (φ \land (h \in (O Func S) \land w \in B)) \to (b \in (h 1^{st} (Z) w) \leftrightarrow b \in (1^{st} (Y) (w) (O Nat S) h))$
155	154	biimpa	$⊢ ((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \to b \in (1^{st} (Y) (w) (O Nat S) h)$
156	141 155	nat1st2nd	$⊢ ((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \to b \in (⟨1^{st} (1^{st} (Y) (w)), 2^{nd} (1^{st} (Y) (w))⟩ (O Nat S) ⟨1^{st} (h), 2^{nd} (h)⟩)$
157	141 156 21	natfn	$⊢ ((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \to b Fn B$
158	142	adantr	$⊢ (((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \land z \in B) \to C \in Cat$
159	147	adantr	$⊢ (((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \land z \in B) \to w \in B$
160		simpr	$⊢ (((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \land z \in B) \to z \in B$
161	1 2 158 159 107 160	yon11	$⊢ (((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \land z \in B) \to 1^{st} (1^{st} (Y) (w)) (z) = z Hom (C) w$
162	161	eleq2d	$⊢ (((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \land z \in B) \to (k \in 1^{st} (1^{st} (Y) (w)) (z) \leftrightarrow k \in (z Hom (C) w))$
163	162	biimpa	$⊢ ((((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \land z \in B) \land k \in 1^{st} (1^{st} (Y) (w)) (z)) \to k \in (z Hom (C) w)$
164	158	adantr	$⊢ ((((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \land z \in B) \land k \in (z Hom (C) w)) \to C \in Cat$
165	143	ad2antrr	$⊢ ((((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \land z \in B) \land k \in (z Hom (C) w)) \to V \in W$
166	144	ad2antrr	$⊢ ((((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \land z \in B) \land k \in (z Hom (C) w)) \to ran {Hom}_{𝑓} (C) \subseteq U$
167	145	ad2antrr	$⊢ ((((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \land z \in B) \land k \in (z Hom (C) w)) \to ran {Hom}_{𝑓} (Q) \cup U \subseteq V$
168	146	ad2antrr	$⊢ ((((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \land z \in B) \land k \in (z Hom (C) w)) \to h \in (O Func S)$
169	159	adantr	$⊢ ((((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \land z \in B) \land k \in (z Hom (C) w)) \to w \in B$
170	150	ad2antrr	$⊢ ((((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \land z \in B) \land k \in (z Hom (C) w)) \to (h M w) (b) \in 1^{st} (h) (w)$
171		simplr	$⊢ ((((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \land z \in B) \land k \in (z Hom (C) w)) \to z \in B$
172		simpr	$⊢ ((((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \land z \in B) \land k \in (z Hom (C) w)) \to k \in (z Hom (C) w)$
173	1 2 3 4 5 6 7 8 9 10 11 164 165 166 167 168 169 18 170 171 172	yonedalem4b	$⊢ ((((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \land z \in B) \land k \in (z Hom (C) w)) \to (h N w) ((h M w) (b)) (z) (k) = (w 2^{nd} (h) z) (k) ((h M w) (b))$
174	1 2 3 4 5 6 7 8 9 10 11 164 165 166 167 168 169 16	yonedalem3a	$⊢ ((((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \land z \in B) \land k \in (z Hom (C) w)) \to (h M w = (a \in (1^{st} (Y) (w) (O Nat S) h) ⟼ a (w) (\underset{˙}{1} (w))) \land (h M w) : h 1^{st} (Z) w ⟶ h 1^{st} (E) w)$
175	174	simpld	$⊢ ((((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \land z \in B) \land k \in (z Hom (C) w)) \to h M w = (a \in (1^{st} (Y) (w) (O Nat S) h) ⟼ a (w) (\underset{˙}{1} (w)))$
176	175	fveq1d	$⊢ ((((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \land z \in B) \land k \in (z Hom (C) w)) \to (h M w) (b) = (a \in (1^{st} (Y) (w) (O Nat S) h) ⟼ a (w) (\underset{˙}{1} (w))) (b)$
177	155	ad2antrr	$⊢ ((((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \land z \in B) \land k \in (z Hom (C) w)) \to b \in (1^{st} (Y) (w) (O Nat S) h)$
178		fveq1	$⊢ a = b \to a (w) = b (w)$
179	178	fveq1d	$⊢ a = b \to a (w) (\underset{˙}{1} (w)) = b (w) (\underset{˙}{1} (w))$
180		fvex	$⊢ b (w) (\underset{˙}{1} (w)) \in V$
181	179 102 180	fvmpt	$⊢ b \in (1^{st} (Y) (w) (O Nat S) h) \to (a \in (1^{st} (Y) (w) (O Nat S) h) ⟼ a (w) (\underset{˙}{1} (w))) (b) = b (w) (\underset{˙}{1} (w))$
182	177 181	syl	$⊢ ((((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \land z \in B) \land k \in (z Hom (C) w)) \to (a \in (1^{st} (Y) (w) (O Nat S) h) ⟼ a (w) (\underset{˙}{1} (w))) (b) = b (w) (\underset{˙}{1} (w))$
183	176 182	eqtrd	$⊢ ((((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \land z \in B) \land k \in (z Hom (C) w)) \to (h M w) (b) = b (w) (\underset{˙}{1} (w))$
184	183	fveq2d	$⊢ ((((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \land z \in B) \land k \in (z Hom (C) w)) \to (w 2^{nd} (h) z) (k) ((h M w) (b)) = (w 2^{nd} (h) z) (k) (b (w) (\underset{˙}{1} (w)))$
185	156	ad2antrr	$⊢ ((((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \land z \in B) \land k \in (z Hom (C) w)) \to b \in (⟨1^{st} (1^{st} (Y) (w)), 2^{nd} (1^{st} (Y) (w))⟩ (O Nat S) ⟨1^{st} (h), 2^{nd} (h)⟩)$
186		eqid	$⊢ Hom (O) = Hom (O)$
187		eqid	$⊢ comp (S) = comp (S)$
188	107 4	oppchom	$⊢ w Hom (O) z = z Hom (C) w$
189	172 188	eleqtrrdi	$⊢ ((((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \land z \in B) \land k \in (z Hom (C) w)) \to k \in (w Hom (O) z)$
190	141 185 21 186 187 169 171 189	nati	$⊢ ((((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \land z \in B) \land k \in (z Hom (C) w)) \to b (z) (⟨1^{st} (1^{st} (Y) (w)) (w), 1^{st} (1^{st} (Y) (w)) (z)⟩ comp (S) 1^{st} (h) (z)) (w 2^{nd} (1^{st} (Y) (w)) z) (k) = (w 2^{nd} (h) z) (k) (⟨1^{st} (1^{st} (Y) (w)) (w), 1^{st} (h) (w)⟩ comp (S) 1^{st} (h) (z)) b (w)$
191	77	ad2antrr	$⊢ ((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \to U \in V$
192	191	adantr	$⊢ (((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \land z \in B) \to U \in V$
193	192	adantr	$⊢ ((((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \land z \in B) \land k \in (z Hom (C) w)) \to U \in V$
194		relfunc	$⊢ Rel (C Func Q)$
195	1 12 4 5 7 77 14	yoncl	$⊢ φ \to Y \in (C Func Q)$
196		1st2ndbr	$⊢ (Rel (C Func Q) \land Y \in (C Func Q)) \to 1^{st} (Y) (C Func Q) 2^{nd} (Y)$
197	194 195 196	sylancr	$⊢ φ \to 1^{st} (Y) (C Func Q) 2^{nd} (Y)$
198	2 20 197	funcf1	$⊢ φ \to 1^{st} (Y) : B ⟶ O Func S$
199	198	ad2antrr	$⊢ ((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \to 1^{st} (Y) : B ⟶ O Func S$
200	199 147	ffvelrnd	$⊢ ((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \to 1^{st} (Y) (w) \in (O Func S)$
201		1st2ndbr	$⊢ (Rel (O Func S) \land 1^{st} (Y) (w) \in (O Func S)) \to 1^{st} (1^{st} (Y) (w)) (O Func S) 2^{nd} (1^{st} (Y) (w))$
202	112 200 201	sylancr	$⊢ ((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \to 1^{st} (1^{st} (Y) (w)) (O Func S) 2^{nd} (1^{st} (Y) (w))$
203	21 121 202	funcf1	$⊢ ((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \to 1^{st} (1^{st} (Y) (w)) : B ⟶ {Base}_{S}$
204	5 191	setcbas	$⊢ ((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \to U = {Base}_{S}$
205	204	feq3d	$⊢ ((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \to (1^{st} (1^{st} (Y) (w)) : B ⟶ U \leftrightarrow 1^{st} (1^{st} (Y) (w)) : B ⟶ {Base}_{S})$
206	203 205	mpbird	$⊢ ((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \to 1^{st} (1^{st} (Y) (w)) : B ⟶ U$
207	206 147	ffvelrnd	$⊢ ((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \to 1^{st} (1^{st} (Y) (w)) (w) \in U$
208	207	ad2antrr	$⊢ ((((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \land z \in B) \land k \in (z Hom (C) w)) \to 1^{st} (1^{st} (Y) (w)) (w) \in U$
209	206	ffvelrnda	$⊢ (((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \land z \in B) \to 1^{st} (1^{st} (Y) (w)) (z) \in U$
210	209	adantr	$⊢ ((((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \land z \in B) \land k \in (z Hom (C) w)) \to 1^{st} (1^{st} (Y) (w)) (z) \in U$
211	112 146 113	sylancr	$⊢ ((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \to 1^{st} (h) (O Func S) 2^{nd} (h)$
212	21 121 211	funcf1	$⊢ ((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \to 1^{st} (h) : B ⟶ {Base}_{S}$
213	204	feq3d	$⊢ ((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \to (1^{st} (h) : B ⟶ U \leftrightarrow 1^{st} (h) : B ⟶ {Base}_{S})$
214	212 213	mpbird	$⊢ ((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \to 1^{st} (h) : B ⟶ U$
215	214	ffvelrnda	$⊢ (((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \land z \in B) \to 1^{st} (h) (z) \in U$
216	215	adantr	$⊢ ((((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \land z \in B) \land k \in (z Hom (C) w)) \to 1^{st} (h) (z) \in U$
217		eqid	$⊢ Hom (S) = Hom (S)$
218	202	ad2antrr	$⊢ ((((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \land z \in B) \land k \in (z Hom (C) w)) \to 1^{st} (1^{st} (Y) (w)) (O Func S) 2^{nd} (1^{st} (Y) (w))$
219	21 186 217 218 169 171	funcf2	$⊢ ((((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \land z \in B) \land k \in (z Hom (C) w)) \to (w 2^{nd} (1^{st} (Y) (w)) z) : w Hom (O) z ⟶ 1^{st} (1^{st} (Y) (w)) (w) Hom (S) 1^{st} (1^{st} (Y) (w)) (z)$
220	219 189	ffvelrnd	$⊢ ((((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \land z \in B) \land k \in (z Hom (C) w)) \to (w 2^{nd} (1^{st} (Y) (w)) z) (k) \in (1^{st} (1^{st} (Y) (w)) (w) Hom (S) 1^{st} (1^{st} (Y) (w)) (z))$
221	5 193 217 208 210	elsetchom	$⊢ ((((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \land z \in B) \land k \in (z Hom (C) w)) \to ((w 2^{nd} (1^{st} (Y) (w)) z) (k) \in (1^{st} (1^{st} (Y) (w)) (w) Hom (S) 1^{st} (1^{st} (Y) (w)) (z)) \leftrightarrow (w 2^{nd} (1^{st} (Y) (w)) z) (k) : 1^{st} (1^{st} (Y) (w)) (w) ⟶ 1^{st} (1^{st} (Y) (w)) (z))$
222	220 221	mpbid	$⊢ ((((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \land z \in B) \land k \in (z Hom (C) w)) \to (w 2^{nd} (1^{st} (Y) (w)) z) (k) : 1^{st} (1^{st} (Y) (w)) (w) ⟶ 1^{st} (1^{st} (Y) (w)) (z)$
223	156	adantr	$⊢ (((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \land z \in B) \to b \in (⟨1^{st} (1^{st} (Y) (w)), 2^{nd} (1^{st} (Y) (w))⟩ (O Nat S) ⟨1^{st} (h), 2^{nd} (h)⟩)$
224	141 223 21 217 160	natcl	$⊢ (((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \land z \in B) \to b (z) \in (1^{st} (1^{st} (Y) (w)) (z) Hom (S) 1^{st} (h) (z))$
225	5 192 217 209 215	elsetchom	$⊢ (((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \land z \in B) \to (b (z) \in (1^{st} (1^{st} (Y) (w)) (z) Hom (S) 1^{st} (h) (z)) \leftrightarrow b (z) : 1^{st} (1^{st} (Y) (w)) (z) ⟶ 1^{st} (h) (z))$
226	224 225	mpbid	$⊢ (((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \land z \in B) \to b (z) : 1^{st} (1^{st} (Y) (w)) (z) ⟶ 1^{st} (h) (z)$
227	226	adantr	$⊢ ((((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \land z \in B) \land k \in (z Hom (C) w)) \to b (z) : 1^{st} (1^{st} (Y) (w)) (z) ⟶ 1^{st} (h) (z)$
228	5 193 187 208 210 216 222 227	setcco	$⊢ ((((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \land z \in B) \land k \in (z Hom (C) w)) \to b (z) (⟨1^{st} (1^{st} (Y) (w)) (w), 1^{st} (1^{st} (Y) (w)) (z)⟩ comp (S) 1^{st} (h) (z)) (w 2^{nd} (1^{st} (Y) (w)) z) (k) = b (z) \circ (w 2^{nd} (1^{st} (Y) (w)) z) (k)$
229	214 147	ffvelrnd	$⊢ ((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \to 1^{st} (h) (w) \in U$
230	229	ad2antrr	$⊢ ((((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \land z \in B) \land k \in (z Hom (C) w)) \to 1^{st} (h) (w) \in U$
231	141 156 21 217 147	natcl	$⊢ ((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \to b (w) \in (1^{st} (1^{st} (Y) (w)) (w) Hom (S) 1^{st} (h) (w))$
232	5 191 217 207 229	elsetchom	$⊢ ((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \to (b (w) \in (1^{st} (1^{st} (Y) (w)) (w) Hom (S) 1^{st} (h) (w)) \leftrightarrow b (w) : 1^{st} (1^{st} (Y) (w)) (w) ⟶ 1^{st} (h) (w))$
233	231 232	mpbid	$⊢ ((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \to b (w) : 1^{st} (1^{st} (Y) (w)) (w) ⟶ 1^{st} (h) (w)$
234	233	ad2antrr	$⊢ ((((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \land z \in B) \land k \in (z Hom (C) w)) \to b (w) : 1^{st} (1^{st} (Y) (w)) (w) ⟶ 1^{st} (h) (w)$
235	112 168 113	sylancr	$⊢ ((((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \land z \in B) \land k \in (z Hom (C) w)) \to 1^{st} (h) (O Func S) 2^{nd} (h)$
236	21 186 217 235 169 171	funcf2	$⊢ ((((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \land z \in B) \land k \in (z Hom (C) w)) \to (w 2^{nd} (h) z) : w Hom (O) z ⟶ 1^{st} (h) (w) Hom (S) 1^{st} (h) (z)$
237	236 189	ffvelrnd	$⊢ ((((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \land z \in B) \land k \in (z Hom (C) w)) \to (w 2^{nd} (h) z) (k) \in (1^{st} (h) (w) Hom (S) 1^{st} (h) (z))$
238	5 193 217 230 216	elsetchom	$⊢ ((((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \land z \in B) \land k \in (z Hom (C) w)) \to ((w 2^{nd} (h) z) (k) \in (1^{st} (h) (w) Hom (S) 1^{st} (h) (z)) \leftrightarrow (w 2^{nd} (h) z) (k) : 1^{st} (h) (w) ⟶ 1^{st} (h) (z))$
239	237 238	mpbid	$⊢ ((((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \land z \in B) \land k \in (z Hom (C) w)) \to (w 2^{nd} (h) z) (k) : 1^{st} (h) (w) ⟶ 1^{st} (h) (z)$
240	5 193 187 208 230 216 234 239	setcco	$⊢ ((((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \land z \in B) \land k \in (z Hom (C) w)) \to (w 2^{nd} (h) z) (k) (⟨1^{st} (1^{st} (Y) (w)) (w), 1^{st} (h) (w)⟩ comp (S) 1^{st} (h) (z)) b (w) = (w 2^{nd} (h) z) (k) \circ b (w)$
241	190 228 240	3eqtr3d	$⊢ ((((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \land z \in B) \land k \in (z Hom (C) w)) \to b (z) \circ (w 2^{nd} (1^{st} (Y) (w)) z) (k) = (w 2^{nd} (h) z) (k) \circ b (w)$
242	241	fveq1d	$⊢ ((((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \land z \in B) \land k \in (z Hom (C) w)) \to (b (z) \circ (w 2^{nd} (1^{st} (Y) (w)) z) (k)) (\underset{˙}{1} (w)) = ((w 2^{nd} (h) z) (k) \circ b (w)) (\underset{˙}{1} (w))$
243	2 107 3 142 147	catidcl	$⊢ ((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \to \underset{˙}{1} (w) \in (w Hom (C) w)$
244	1 2 142 147 107 147	yon11	$⊢ ((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \to 1^{st} (1^{st} (Y) (w)) (w) = w Hom (C) w$
245	243 244	eleqtrrd	$⊢ ((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \to \underset{˙}{1} (w) \in 1^{st} (1^{st} (Y) (w)) (w)$
246	245	ad2antrr	$⊢ ((((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \land z \in B) \land k \in (z Hom (C) w)) \to \underset{˙}{1} (w) \in 1^{st} (1^{st} (Y) (w)) (w)$
247	222 246	fvco3d	$⊢ ((((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \land z \in B) \land k \in (z Hom (C) w)) \to (b (z) \circ (w 2^{nd} (1^{st} (Y) (w)) z) (k)) (\underset{˙}{1} (w)) = b (z) ((w 2^{nd} (1^{st} (Y) (w)) z) (k) (\underset{˙}{1} (w)))$
248	233 245	fvco3d	$⊢ ((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \to ((w 2^{nd} (h) z) (k) \circ b (w)) (\underset{˙}{1} (w)) = (w 2^{nd} (h) z) (k) (b (w) (\underset{˙}{1} (w)))$
249	248	ad2antrr	$⊢ ((((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \land z \in B) \land k \in (z Hom (C) w)) \to ((w 2^{nd} (h) z) (k) \circ b (w)) (\underset{˙}{1} (w)) = (w 2^{nd} (h) z) (k) (b (w) (\underset{˙}{1} (w)))$
250	242 247 249	3eqtr3d	$⊢ ((((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \land z \in B) \land k \in (z Hom (C) w)) \to b (z) ((w 2^{nd} (1^{st} (Y) (w)) z) (k) (\underset{˙}{1} (w))) = (w 2^{nd} (h) z) (k) (b (w) (\underset{˙}{1} (w)))$
251		eqid	$⊢ comp (C) = comp (C)$
252	243	ad2antrr	$⊢ ((((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \land z \in B) \land k \in (z Hom (C) w)) \to \underset{˙}{1} (w) \in (w Hom (C) w)$
253	1 2 164 169 107 169 251 171 172 252	yon12	$⊢ ((((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \land z \in B) \land k \in (z Hom (C) w)) \to (w 2^{nd} (1^{st} (Y) (w)) z) (k) (\underset{˙}{1} (w)) = \underset{˙}{1} (w) (⟨z, w⟩ comp (C) w) k$
254	2 107 3 164 171 251 169 172	catlid	$⊢ ((((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \land z \in B) \land k \in (z Hom (C) w)) \to \underset{˙}{1} (w) (⟨z, w⟩ comp (C) w) k = k$
255	253 254	eqtrd	$⊢ ((((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \land z \in B) \land k \in (z Hom (C) w)) \to (w 2^{nd} (1^{st} (Y) (w)) z) (k) (\underset{˙}{1} (w)) = k$
256	255	fveq2d	$⊢ ((((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \land z \in B) \land k \in (z Hom (C) w)) \to b (z) ((w 2^{nd} (1^{st} (Y) (w)) z) (k) (\underset{˙}{1} (w))) = b (z) (k)$
257	250 256	eqtr3d	$⊢ ((((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \land z \in B) \land k \in (z Hom (C) w)) \to (w 2^{nd} (h) z) (k) (b (w) (\underset{˙}{1} (w))) = b (z) (k)$
258	173 184 257	3eqtrd	$⊢ ((((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \land z \in B) \land k \in (z Hom (C) w)) \to (h N w) ((h M w) (b)) (z) (k) = b (z) (k)$
259	163 258	syldan	$⊢ ((((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \land z \in B) \land k \in 1^{st} (1^{st} (Y) (w)) (z)) \to (h N w) ((h M w) (b)) (z) (k) = b (z) (k)$
260	259	mpteq2dva	$⊢ (((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \land z \in B) \to (k \in 1^{st} (1^{st} (Y) (w)) (z) ⟼ (h N w) ((h M w) (b)) (z) (k)) = (k \in 1^{st} (1^{st} (Y) (w)) (z) ⟼ b (z) (k))$
261	152	adantr	$⊢ (((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \land z \in B) \to (h N w) ((h M w) (b)) \in (⟨1^{st} (1^{st} (Y) (w)), 2^{nd} (1^{st} (Y) (w))⟩ (O Nat S) ⟨1^{st} (h), 2^{nd} (h)⟩)$
262	141 261 21 217 160	natcl	$⊢ (((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \land z \in B) \to (h N w) ((h M w) (b)) (z) \in (1^{st} (1^{st} (Y) (w)) (z) Hom (S) 1^{st} (h) (z))$
263	5 192 217 209 215	elsetchom	$⊢ (((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \land z \in B) \to ((h N w) ((h M w) (b)) (z) \in (1^{st} (1^{st} (Y) (w)) (z) Hom (S) 1^{st} (h) (z)) \leftrightarrow (h N w) ((h M w) (b)) (z) : 1^{st} (1^{st} (Y) (w)) (z) ⟶ 1^{st} (h) (z))$
264	262 263	mpbid	$⊢ (((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \land z \in B) \to (h N w) ((h M w) (b)) (z) : 1^{st} (1^{st} (Y) (w)) (z) ⟶ 1^{st} (h) (z)$
265	264	feqmptd	$⊢ (((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \land z \in B) \to (h N w) ((h M w) (b)) (z) = (k \in 1^{st} (1^{st} (Y) (w)) (z) ⟼ (h N w) ((h M w) (b)) (z) (k))$
266	226	feqmptd	$⊢ (((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \land z \in B) \to b (z) = (k \in 1^{st} (1^{st} (Y) (w)) (z) ⟼ b (z) (k))$
267	260 265 266	3eqtr4d	$⊢ (((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \land z \in B) \to (h N w) ((h M w) (b)) (z) = b (z)$
268	153 157 267	eqfnfvd	$⊢ ((φ \land (h \in (O Func S) \land w \in B)) \land b \in (h 1^{st} (Z) w)) \to (h N w) ((h M w) (b)) = b$
269	268	mpteq2dva	$⊢ (φ \land (h \in (O Func S) \land w \in B)) \to (b \in (h 1^{st} (Z) w) ⟼ (h N w) ((h M w) (b))) = (b \in (h 1^{st} (Z) w) ⟼ b)$
270		mptresid	$⊢ {I ↾}_{(h 1^{st} (Z) w)} = (b \in (h 1^{st} (Z) w) ⟼ b)$
271	269 270	eqtr4di	$⊢ (φ \land (h \in (O Func S) \land w \in B)) \to (b \in (h 1^{st} (Z) w) ⟼ (h N w) ((h M w) (b))) = {I ↾}_{(h 1^{st} (Z) w)}$
272	140 271	eqtrd	$⊢ (φ \land (h \in (O Func S) \land w \in B)) \to (h N w) \circ (h M w) = {I ↾}_{(h 1^{st} (Z) w)}$
273		fcof1o	$⊢ (((h M w) : h 1^{st} (Z) w ⟶ h 1^{st} (E) w \land (h N w) : h 1^{st} (E) w ⟶ h 1^{st} (Z) w) \land ((h M w) \circ (h N w) = {I ↾}_{(h 1^{st} (E) w)} \land (h N w) \circ (h M w) = {I ↾}_{(h 1^{st} (Z) w)})) \to ((h M w) : h 1^{st} (Z) w \underset{1-1 onto}{⟶} h 1^{st} (E) w \land {(h M w)}^{-1} = h N w)$
274	36 84 138 272 273	syl22anc	$⊢ (φ \land (h \in (O Func S) \land w \in B)) \to ((h M w) : h 1^{st} (Z) w \underset{1-1 onto}{⟶} h 1^{st} (E) w \land {(h M w)}^{-1} = h N w)$
275		eqcom	$⊢ {(h M w)}^{-1} = h N w \leftrightarrow h N w = {(h M w)}^{-1}$
276	275	anbi2i	$⊢ ((h M w) : h 1^{st} (Z) w \underset{1-1 onto}{⟶} h 1^{st} (E) w \land {(h M w)}^{-1} = h N w) \leftrightarrow ((h M w) : h 1^{st} (Z) w \underset{1-1 onto}{⟶} h 1^{st} (E) w \land h N w = {(h M w)}^{-1})$
277	274 276	sylib	$⊢ (φ \land (h \in (O Func S) \land w \in B)) \to ((h M w) : h 1^{st} (Z) w \underset{1-1 onto}{⟶} h 1^{st} (E) w \land h N w = {(h M w)}^{-1})$
278		eqid	$⊢ {Base}_{T} = {Base}_{T}$
279		relfunc	$⊢ Rel ((Q \times_{c} O) Func T)$
280		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)$
281	279 25 280	sylancr	$⊢ φ \to 1^{st} (Z) ((Q \times_{c} O) Func T) 2^{nd} (Z)$
282	22 278 281	funcf1	$⊢ φ \to 1^{st} (Z) : (O Func S) \times B ⟶ {Base}_{T}$
283	6 13	setcbas	$⊢ φ \to V = {Base}_{T}$
284	283	feq3d	$⊢ φ \to (1^{st} (Z) : (O Func S) \times B ⟶ V \leftrightarrow 1^{st} (Z) : (O Func S) \times B ⟶ {Base}_{T})$
285	282 284	mpbird	$⊢ φ \to 1^{st} (Z) : (O Func S) \times B ⟶ V$
286	285	fovrnda	$⊢ (φ \land (h \in (O Func S) \land w \in B)) \to h 1^{st} (Z) w \in V$
287		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)$
288	279 26 287	sylancr	$⊢ φ \to 1^{st} (E) ((Q \times_{c} O) Func T) 2^{nd} (E)$
289	22 278 288	funcf1	$⊢ φ \to 1^{st} (E) : (O Func S) \times B ⟶ {Base}_{T}$
290	283	feq3d	$⊢ φ \to (1^{st} (E) : (O Func S) \times B ⟶ V \leftrightarrow 1^{st} (E) : (O Func S) \times B ⟶ {Base}_{T})$
291	289 290	mpbird	$⊢ φ \to 1^{st} (E) : (O Func S) \times B ⟶ V$
292	291	fovrnda	$⊢ (φ \land (h \in (O Func S) \land w \in B)) \to h 1^{st} (E) w \in V$
293	6 30 286 292 27	setcinv	$⊢ (φ \land (h \in (O Func S) \land w \in B)) \to ((h M w) ((h 1^{st} (Z) w) Inv (T) (h 1^{st} (E) w)) (h N w) \leftrightarrow ((h M w) : h 1^{st} (Z) w \underset{1-1 onto}{⟶} h 1^{st} (E) w \land h N w = {(h M w)}^{-1}))$
294	277 293	mpbird	$⊢ (φ \land (h \in (O Func S) \land w \in B)) \to (h M w) ((h 1^{st} (Z) w) Inv (T) (h 1^{st} (E) w)) (h N w)$
295	294	ralrimivva	$⊢ φ \to \forall h \in (O Func S) \forall w \in B (h M w) ((h 1^{st} (Z) w) Inv (T) (h 1^{st} (E) w)) (h N w)$
296		fveq2	$⊢ z = ⟨h, w⟩ \to M (z) = M (⟨h, w⟩)$
297		df-ov	$⊢ h M w = M (⟨h, w⟩)$
298	296 297	eqtr4di	$⊢ z = ⟨h, w⟩ \to M (z) = h M w$
299		fveq2	$⊢ z = ⟨h, w⟩ \to 1^{st} (Z) (z) = 1^{st} (Z) (⟨h, w⟩)$
300		df-ov	$⊢ h 1^{st} (Z) w = 1^{st} (Z) (⟨h, w⟩)$
301	299 300	eqtr4di	$⊢ z = ⟨h, w⟩ \to 1^{st} (Z) (z) = h 1^{st} (Z) w$
302		fveq2	$⊢ z = ⟨h, w⟩ \to 1^{st} (E) (z) = 1^{st} (E) (⟨h, w⟩)$
303		df-ov	$⊢ h 1^{st} (E) w = 1^{st} (E) (⟨h, w⟩)$
304	302 303	eqtr4di	$⊢ z = ⟨h, w⟩ \to 1^{st} (E) (z) = h 1^{st} (E) w$
305	301 304	oveq12d	$⊢ z = ⟨h, w⟩ \to 1^{st} (Z) (z) Inv (T) 1^{st} (E) (z) = (h 1^{st} (Z) w) Inv (T) (h 1^{st} (E) w)$
306		fveq2	$⊢ z = ⟨h, w⟩ \to N (z) = N (⟨h, w⟩)$
307		df-ov	$⊢ h N w = N (⟨h, w⟩)$
308	306 307	eqtr4di	$⊢ z = ⟨h, w⟩ \to N (z) = h N w$
309	298 305 308	breq123d	$⊢ z = ⟨h, w⟩ \to (M (z) (1^{st} (Z) (z) Inv (T) 1^{st} (E) (z)) N (z) \leftrightarrow (h M w) ((h 1^{st} (Z) w) Inv (T) (h 1^{st} (E) w)) (h N w))$
310	309	ralxp	$⊢ \forall z \in ((O Func S) \times B) M (z) (1^{st} (Z) (z) Inv (T) 1^{st} (E) (z)) N (z) \leftrightarrow \forall h \in (O Func S) \forall w \in B (h M w) ((h 1^{st} (Z) w) Inv (T) (h 1^{st} (E) w)) (h N w)$
311	295 310	sylibr	$⊢ φ \to \forall z \in ((O Func S) \times B) M (z) (1^{st} (Z) (z) Inv (T) 1^{st} (E) (z)) N (z)$
312	311	r19.21bi	$⊢ (φ \land z \in ((O Func S) \times B)) \to M (z) (1^{st} (Z) (z) Inv (T) 1^{st} (E) (z)) N (z)$
313	9 22 23 25 26 17 27 28 312	invfuc	$⊢ φ \to M (Z I E) (z \in ((O Func S) \times B) ⟼ N (z))$
314		fvex	$⊢ 1^{st} (f) (x) \in V$
315	314	mptex	$⊢ (u \in 1^{st} (f) (x) ⟼ (y \in B ⟼ (g \in (y Hom (C) x) ⟼ (x 2^{nd} (f) y) (g) (u)))) \in V$
316	18 315	fnmpoi	$⊢ N Fn ((O Func S) \times B)$
317		dffn5	$⊢ N Fn ((O Func S) \times B) \leftrightarrow N = (z \in ((O Func S) \times B) ⟼ N (z))$
318	316 317	mpbi	$⊢ N = (z \in ((O Func S) \times B) ⟼ N (z))$
319	313 318	breqtrrdi	$⊢ φ \to M (Z I E) N$

Metamath Proof Explorer

Theorem yonedainv

Proof