yonffthlem - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > yonffthlem		Structured version Visualization version GIF version

Theorem yonffthlem 18237

Description: Lemma for yonffth 18239. (Contributed by Mario Carneiro, 29-Jan-2017.)

**Hypotheses**
Ref	Expression
yoneda.y	⊢ 𝑌 = (Yon‘𝐶)
yoneda.b	⊢ 𝐵 = (Base‘𝐶)
yoneda.1	⊢ 1 = (Id‘𝐶)
yoneda.o	⊢ 𝑂 = (oppCat‘𝐶)
yoneda.s	⊢ 𝑆 = (SetCat‘𝑈)
yoneda.t	⊢ 𝑇 = (SetCat‘𝑉)
yoneda.q	⊢ 𝑄 = (𝑂 FuncCat 𝑆)
yoneda.h	⊢ 𝐻 = (Hom_F‘𝑄)
yoneda.r	⊢ 𝑅 = ((𝑄 ×_c 𝑂) FuncCat 𝑇)
yoneda.e	⊢ 𝐸 = (𝑂 eval_F 𝑆)
yoneda.z	⊢ 𝑍 = (𝐻 ∘_func ((⟨(1^st ‘𝑌), tpos (2^nd ‘𝑌)⟩ ∘_func (𝑄 2^nd_F 𝑂)) ⟨,⟩_F (𝑄 1^st_F 𝑂)))
yoneda.c	⊢ (𝜑 → 𝐶 ∈ Cat)
yoneda.w	⊢ (𝜑 → 𝑉 ∈ 𝑊)
yoneda.u	⊢ (𝜑 → ran (Hom_f ‘𝐶) ⊆ 𝑈)
yoneda.v	⊢ (𝜑 → (ran (Hom_f ‘𝑄) ∪ 𝑈) ⊆ 𝑉)
yoneda.m	⊢ 𝑀 = (𝑓 ∈ (𝑂 Func 𝑆), 𝑥 ∈ 𝐵 ↦ (𝑎 ∈ (((1^st ‘𝑌)‘𝑥)(𝑂 Nat 𝑆)𝑓) ↦ ((𝑎‘𝑥)‘( 1 ‘𝑥))))
yonedainv.i	⊢ 𝐼 = (Inv‘𝑅)
yonedainv.n	⊢ 𝑁 = (𝑓 ∈ (𝑂 Func 𝑆), 𝑥 ∈ 𝐵 ↦ (𝑢 ∈ ((1^st ‘𝑓)‘𝑥) ↦ (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥) ↦ (((𝑥(2^nd ‘𝑓)𝑦)‘𝑔)‘𝑢)))))

**Assertion**
Ref	Expression
yonffthlem	⊢ (𝜑 → 𝑌 ∈ ((𝐶 Full 𝑄) ∩ (𝐶 Faith 𝑄)))

Distinct variable groups: 𝑓,𝑎,𝑔,𝑥,𝑦, 1 𝑢,𝑎,𝑔,𝑦,𝐶,𝑓,𝑥 𝐸,𝑎,𝑓,𝑔,𝑢,𝑦 𝐵,𝑎,𝑓,𝑔,𝑢,𝑥,𝑦 𝑁,𝑎 𝑂,𝑎,𝑓,𝑔,𝑢,𝑥,𝑦 𝑆,𝑎,𝑓,𝑔,𝑢,𝑥,𝑦 𝑔,𝑀,𝑢,𝑦 𝑄,𝑎,𝑓,𝑔,𝑢,𝑥 𝑇,𝑓,𝑔,𝑢,𝑦 𝜑,𝑎,𝑓,𝑔,𝑢,𝑥,𝑦 𝑢,𝑅 𝑌,𝑎,𝑓,𝑔,𝑢,𝑥,𝑦 𝑍,𝑎,𝑓,𝑔,𝑢,𝑥,𝑦 Allowed substitution hints: 𝑄(𝑦) 𝑅(𝑥,𝑦,𝑓,𝑔,𝑎) 𝑇(𝑥,𝑎) 𝑈(𝑥,𝑦,𝑢,𝑓,𝑔,𝑎) 1 (𝑢) 𝐸(𝑥) 𝐻(𝑥,𝑦,𝑢,𝑓,𝑔,𝑎) 𝐼(𝑥,𝑦,𝑢,𝑓,𝑔,𝑎) 𝑀(𝑥,𝑓,𝑎) 𝑁(𝑥,𝑦,𝑢,𝑓,𝑔) 𝑉(𝑥,𝑦,𝑢,𝑓,𝑔,𝑎) 𝑊(𝑥,𝑦,𝑢,𝑓,𝑔,𝑎)

Proof of Theorem yonffthlem Dummy variables ℎ 𝑤 𝑧 𝑣 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		relfunc 17811	. . 3 ⊢ Rel (𝐶 Func 𝑄)
2		yoneda.y	. . . 4 ⊢ 𝑌 = (Yon‘𝐶)
3		yoneda.c	. . . 4 ⊢ (𝜑 → 𝐶 ∈ Cat)
4		yoneda.o	. . . 4 ⊢ 𝑂 = (oppCat‘𝐶)
5		yoneda.s	. . . 4 ⊢ 𝑆 = (SetCat‘𝑈)
6		yoneda.q	. . . 4 ⊢ 𝑄 = (𝑂 FuncCat 𝑆)
7		yoneda.w	. . . . 5 ⊢ (𝜑 → 𝑉 ∈ 𝑊)
8		yoneda.v	. . . . . 6 ⊢ (𝜑 → (ran (Hom_f ‘𝑄) ∪ 𝑈) ⊆ 𝑉)
9	8	unssbd 4180	. . . . 5 ⊢ (𝜑 → 𝑈 ⊆ 𝑉)
10	7, 9	ssexd 5314	. . . 4 ⊢ (𝜑 → 𝑈 ∈ V)
11		yoneda.u	. . . 4 ⊢ (𝜑 → ran (Hom_f ‘𝐶) ⊆ 𝑈)
12	2, 3, 4, 5, 6, 10, 11	yoncl 18217	. . 3 ⊢ (𝜑 → 𝑌 ∈ (𝐶 Func 𝑄))
13		1st2nd 8018	. . 3 ⊢ ((Rel (𝐶 Func 𝑄) ∧ 𝑌 ∈ (𝐶 Func 𝑄)) → 𝑌 = ⟨(1^st ‘𝑌), (2^nd ‘𝑌)⟩)
14	1, 12, 13	sylancr 586	. 2 ⊢ (𝜑 → 𝑌 = ⟨(1^st ‘𝑌), (2^nd ‘𝑌)⟩)
15		1st2ndbr 8021	. . . . 5 ⊢ ((Rel (𝐶 Func 𝑄) ∧ 𝑌 ∈ (𝐶 Func 𝑄)) → (1^st ‘𝑌)(𝐶 Func 𝑄)(2^nd ‘𝑌))
16	1, 12, 15	sylancr 586	. . . 4 ⊢ (𝜑 → (1^st ‘𝑌)(𝐶 Func 𝑄)(2^nd ‘𝑌))
17		fveq2 6881	. . . . . . . . . . 11 ⊢ (𝑣 = ⟨((1^st ‘𝑌)‘𝑤), 𝑧⟩ → (𝑁‘𝑣) = (𝑁‘⟨((1^st ‘𝑌)‘𝑤), 𝑧⟩))
18		df-ov 7404	. . . . . . . . . . 11 ⊢ (((1^st ‘𝑌)‘𝑤)𝑁𝑧) = (𝑁‘⟨((1^st ‘𝑌)‘𝑤), 𝑧⟩)
19	17, 18	eqtr4di 2782	. . . . . . . . . 10 ⊢ (𝑣 = ⟨((1^st ‘𝑌)‘𝑤), 𝑧⟩ → (𝑁‘𝑣) = (((1^st ‘𝑌)‘𝑤)𝑁𝑧))
20		fveq2 6881	. . . . . . . . . . . 12 ⊢ (𝑣 = ⟨((1^st ‘𝑌)‘𝑤), 𝑧⟩ → ((1^st ‘𝐸)‘𝑣) = ((1^st ‘𝐸)‘⟨((1^st ‘𝑌)‘𝑤), 𝑧⟩))
21		df-ov 7404	. . . . . . . . . . . 12 ⊢ (((1^st ‘𝑌)‘𝑤)(1^st ‘𝐸)𝑧) = ((1^st ‘𝐸)‘⟨((1^st ‘𝑌)‘𝑤), 𝑧⟩)
22	20, 21	eqtr4di 2782	. . . . . . . . . . 11 ⊢ (𝑣 = ⟨((1^st ‘𝑌)‘𝑤), 𝑧⟩ → ((1^st ‘𝐸)‘𝑣) = (((1^st ‘𝑌)‘𝑤)(1^st ‘𝐸)𝑧))
23		fveq2 6881	. . . . . . . . . . . 12 ⊢ (𝑣 = ⟨((1^st ‘𝑌)‘𝑤), 𝑧⟩ → ((1^st ‘𝑍)‘𝑣) = ((1^st ‘𝑍)‘⟨((1^st ‘𝑌)‘𝑤), 𝑧⟩))
24		df-ov 7404	. . . . . . . . . . . 12 ⊢ (((1^st ‘𝑌)‘𝑤)(1^st ‘𝑍)𝑧) = ((1^st ‘𝑍)‘⟨((1^st ‘𝑌)‘𝑤), 𝑧⟩)
25	23, 24	eqtr4di 2782	. . . . . . . . . . 11 ⊢ (𝑣 = ⟨((1^st ‘𝑌)‘𝑤), 𝑧⟩ → ((1^st ‘𝑍)‘𝑣) = (((1^st ‘𝑌)‘𝑤)(1^st ‘𝑍)𝑧))
26	22, 25	oveq12d 7419	. . . . . . . . . 10 ⊢ (𝑣 = ⟨((1^st ‘𝑌)‘𝑤), 𝑧⟩ → (((1^st ‘𝐸)‘𝑣)(Iso‘𝑇)((1^st ‘𝑍)‘𝑣)) = ((((1^st ‘𝑌)‘𝑤)(1^st ‘𝐸)𝑧)(Iso‘𝑇)(((1^st ‘𝑌)‘𝑤)(1^st ‘𝑍)𝑧)))
27	19, 26	eleq12d 2819	. . . . . . . . 9 ⊢ (𝑣 = ⟨((1^st ‘𝑌)‘𝑤), 𝑧⟩ → ((𝑁‘𝑣) ∈ (((1^st ‘𝐸)‘𝑣)(Iso‘𝑇)((1^st ‘𝑍)‘𝑣)) ↔ (((1^st ‘𝑌)‘𝑤)𝑁𝑧) ∈ ((((1^st ‘𝑌)‘𝑤)(1^st ‘𝐸)𝑧)(Iso‘𝑇)(((1^st ‘𝑌)‘𝑤)(1^st ‘𝑍)𝑧))))
28		yoneda.r	. . . . . . . . . . . . . 14 ⊢ 𝑅 = ((𝑄 ×_c 𝑂) FuncCat 𝑇)
29	28	fucbas 17914	. . . . . . . . . . . . 13 ⊢ ((𝑄 ×_c 𝑂) Func 𝑇) = (Base‘𝑅)
30		yonedainv.i	. . . . . . . . . . . . 13 ⊢ 𝐼 = (Inv‘𝑅)
31		yoneda.b	. . . . . . . . . . . . . . . . . 18 ⊢ 𝐵 = (Base‘𝐶)
32		yoneda.1	. . . . . . . . . . . . . . . . . 18 ⊢ 1 = (Id‘𝐶)
33		yoneda.t	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑇 = (SetCat‘𝑉)
34		yoneda.h	. . . . . . . . . . . . . . . . . 18 ⊢ 𝐻 = (Hom_F‘𝑄)
35		yoneda.e	. . . . . . . . . . . . . . . . . 18 ⊢ 𝐸 = (𝑂 eval_F 𝑆)
36		yoneda.z	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑍 = (𝐻 ∘_func ((⟨(1^st ‘𝑌), tpos (2^nd ‘𝑌)⟩ ∘_func (𝑄 2^nd_F 𝑂)) ⟨,⟩_F (𝑄 1^st_F 𝑂)))
37	2, 31, 32, 4, 5, 33, 6, 34, 28, 35, 36, 3, 7, 11, 8	yonedalem1 18227	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑍 ∈ ((𝑄 ×_c 𝑂) Func 𝑇) ∧ 𝐸 ∈ ((𝑄 ×_c 𝑂) Func 𝑇)))
38	37	simpld 494	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑍 ∈ ((𝑄 ×_c 𝑂) Func 𝑇))
39		funcrcl 17812	. . . . . . . . . . . . . . . 16 ⊢ (𝑍 ∈ ((𝑄 ×_c 𝑂) Func 𝑇) → ((𝑄 ×_c 𝑂) ∈ Cat ∧ 𝑇 ∈ Cat))
40	38, 39	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑄 ×_c 𝑂) ∈ Cat ∧ 𝑇 ∈ Cat))
41	40	simpld 494	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑄 ×_c 𝑂) ∈ Cat)
42	40	simprd 495	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑇 ∈ Cat)
43	28, 41, 42	fuccat 17925	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑅 ∈ Cat)
44	37	simprd 495	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐸 ∈ ((𝑄 ×_c 𝑂) Func 𝑇))
45		eqid 2724	. . . . . . . . . . . . 13 ⊢ (Iso‘𝑅) = (Iso‘𝑅)
46		yoneda.m	. . . . . . . . . . . . . 14 ⊢ 𝑀 = (𝑓 ∈ (𝑂 Func 𝑆), 𝑥 ∈ 𝐵 ↦ (𝑎 ∈ (((1^st ‘𝑌)‘𝑥)(𝑂 Nat 𝑆)𝑓) ↦ ((𝑎‘𝑥)‘( 1 ‘𝑥))))
47		yonedainv.n	. . . . . . . . . . . . . 14 ⊢ 𝑁 = (𝑓 ∈ (𝑂 Func 𝑆), 𝑥 ∈ 𝐵 ↦ (𝑢 ∈ ((1^st ‘𝑓)‘𝑥) ↦ (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥) ↦ (((𝑥(2^nd ‘𝑓)𝑦)‘𝑔)‘𝑢)))))
48	2, 31, 32, 4, 5, 33, 6, 34, 28, 35, 36, 3, 7, 11, 8, 46, 30, 47	yonedainv 18236	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀(𝑍𝐼𝐸)𝑁)
49	29, 30, 43, 38, 44, 45, 48	inviso2 17713	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑁 ∈ (𝐸(Iso‘𝑅)𝑍))
50		eqid 2724	. . . . . . . . . . . . . 14 ⊢ (𝑄 ×_c 𝑂) = (𝑄 ×_c 𝑂)
51	6	fucbas 17914	. . . . . . . . . . . . . 14 ⊢ (𝑂 Func 𝑆) = (Base‘𝑄)
52	4, 31	oppcbas 17662	. . . . . . . . . . . . . 14 ⊢ 𝐵 = (Base‘𝑂)
53	50, 51, 52	xpcbas 18132	. . . . . . . . . . . . 13 ⊢ ((𝑂 Func 𝑆) × 𝐵) = (Base‘(𝑄 ×_c 𝑂))
54		eqid 2724	. . . . . . . . . . . . 13 ⊢ ((𝑄 ×_c 𝑂) Nat 𝑇) = ((𝑄 ×_c 𝑂) Nat 𝑇)
55		eqid 2724	. . . . . . . . . . . . 13 ⊢ (Iso‘𝑇) = (Iso‘𝑇)
56	28, 53, 54, 44, 38, 45, 55	fuciso 17930	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑁 ∈ (𝐸(Iso‘𝑅)𝑍) ↔ (𝑁 ∈ (𝐸((𝑄 ×_c 𝑂) Nat 𝑇)𝑍) ∧ ∀𝑣 ∈ ((𝑂 Func 𝑆) × 𝐵)(𝑁‘𝑣) ∈ (((1^st ‘𝐸)‘𝑣)(Iso‘𝑇)((1^st ‘𝑍)‘𝑣)))))
57	49, 56	mpbid 231	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑁 ∈ (𝐸((𝑄 ×_c 𝑂) Nat 𝑇)𝑍) ∧ ∀𝑣 ∈ ((𝑂 Func 𝑆) × 𝐵)(𝑁‘𝑣) ∈ (((1^st ‘𝐸)‘𝑣)(Iso‘𝑇)((1^st ‘𝑍)‘𝑣))))
58	57	simprd 495	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑣 ∈ ((𝑂 Func 𝑆) × 𝐵)(𝑁‘𝑣) ∈ (((1^st ‘𝐸)‘𝑣)(Iso‘𝑇)((1^st ‘𝑍)‘𝑣)))
59	58	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → ∀𝑣 ∈ ((𝑂 Func 𝑆) × 𝐵)(𝑁‘𝑣) ∈ (((1^st ‘𝐸)‘𝑣)(Iso‘𝑇)((1^st ‘𝑍)‘𝑣)))
60	31, 51, 16	funcf1 17815	. . . . . . . . . . . 12 ⊢ (𝜑 → (1^st ‘𝑌):𝐵⟶(𝑂 Func 𝑆))
61	60	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → (1^st ‘𝑌):𝐵⟶(𝑂 Func 𝑆))
62		simprr 770	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → 𝑤 ∈ 𝐵)
63	61, 62	ffvelcdmd 7077	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → ((1^st ‘𝑌)‘𝑤) ∈ (𝑂 Func 𝑆))
64		simprl 768	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → 𝑧 ∈ 𝐵)
65	63, 64	opelxpd 5705	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → ⟨((1^st ‘𝑌)‘𝑤), 𝑧⟩ ∈ ((𝑂 Func 𝑆) × 𝐵))
66	27, 59, 65	rspcdva 3605	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → (((1^st ‘𝑌)‘𝑤)𝑁𝑧) ∈ ((((1^st ‘𝑌)‘𝑤)(1^st ‘𝐸)𝑧)(Iso‘𝑇)(((1^st ‘𝑌)‘𝑤)(1^st ‘𝑍)𝑧)))
67	4	oppccat 17667	. . . . . . . . . . . . 13 ⊢ (𝐶 ∈ Cat → 𝑂 ∈ Cat)
68	3, 67	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑂 ∈ Cat)
69	68	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → 𝑂 ∈ Cat)
70	5	setccat 18037	. . . . . . . . . . . . 13 ⊢ (𝑈 ∈ V → 𝑆 ∈ Cat)
71	10, 70	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑆 ∈ Cat)
72	71	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → 𝑆 ∈ Cat)
73	35, 69, 72, 52, 63, 64	evlf1 18175	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → (((1^st ‘𝑌)‘𝑤)(1^st ‘𝐸)𝑧) = ((1^st ‘((1^st ‘𝑌)‘𝑤))‘𝑧))
74	3	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → 𝐶 ∈ Cat)
75		eqid 2724	. . . . . . . . . . 11 ⊢ (Hom ‘𝐶) = (Hom ‘𝐶)
76	2, 31, 74, 62, 75, 64	yon11 18219	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → ((1^st ‘((1^st ‘𝑌)‘𝑤))‘𝑧) = (𝑧(Hom ‘𝐶)𝑤))
77	73, 76	eqtrd 2764	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → (((1^st ‘𝑌)‘𝑤)(1^st ‘𝐸)𝑧) = (𝑧(Hom ‘𝐶)𝑤))
78	7	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → 𝑉 ∈ 𝑊)
79	11	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → ran (Hom_f ‘𝐶) ⊆ 𝑈)
80	8	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → (ran (Hom_f ‘𝑄) ∪ 𝑈) ⊆ 𝑉)
81	2, 31, 32, 4, 5, 33, 6, 34, 28, 35, 36, 74, 78, 79, 80, 63, 64	yonedalem21 18228	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → (((1^st ‘𝑌)‘𝑤)(1^st ‘𝑍)𝑧) = (((1^st ‘𝑌)‘𝑧)(𝑂 Nat 𝑆)((1^st ‘𝑌)‘𝑤)))
82	77, 81	oveq12d 7419	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → ((((1^st ‘𝑌)‘𝑤)(1^st ‘𝐸)𝑧)(Iso‘𝑇)(((1^st ‘𝑌)‘𝑤)(1^st ‘𝑍)𝑧)) = ((𝑧(Hom ‘𝐶)𝑤)(Iso‘𝑇)(((1^st ‘𝑌)‘𝑧)(𝑂 Nat 𝑆)((1^st ‘𝑌)‘𝑤))))
83	66, 82	eleqtrd 2827	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → (((1^st ‘𝑌)‘𝑤)𝑁𝑧) ∈ ((𝑧(Hom ‘𝐶)𝑤)(Iso‘𝑇)(((1^st ‘𝑌)‘𝑧)(𝑂 Nat 𝑆)((1^st ‘𝑌)‘𝑤))))
84	9	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → 𝑈 ⊆ 𝑉)
85		eqid 2724	. . . . . . . . . . . . 13 ⊢ (Base‘𝑆) = (Base‘𝑆)
86		relfunc 17811	. . . . . . . . . . . . . 14 ⊢ Rel (𝑂 Func 𝑆)
87		1st2ndbr 8021	. . . . . . . . . . . . . 14 ⊢ ((Rel (𝑂 Func 𝑆) ∧ ((1^st ‘𝑌)‘𝑤) ∈ (𝑂 Func 𝑆)) → (1^st ‘((1^st ‘𝑌)‘𝑤))(𝑂 Func 𝑆)(2^nd ‘((1^st ‘𝑌)‘𝑤)))
88	86, 63, 87	sylancr 586	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → (1^st ‘((1^st ‘𝑌)‘𝑤))(𝑂 Func 𝑆)(2^nd ‘((1^st ‘𝑌)‘𝑤)))
89	52, 85, 88	funcf1 17815	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → (1^st ‘((1^st ‘𝑌)‘𝑤)):𝐵⟶(Base‘𝑆))
90	89, 64	ffvelcdmd 7077	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → ((1^st ‘((1^st ‘𝑌)‘𝑤))‘𝑧) ∈ (Base‘𝑆))
91	5, 10	setcbas 18030	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑈 = (Base‘𝑆))
92	91	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → 𝑈 = (Base‘𝑆))
93	90, 92	eleqtrrd 2828	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → ((1^st ‘((1^st ‘𝑌)‘𝑤))‘𝑧) ∈ 𝑈)
94	76, 93	eqeltrrd 2826	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → (𝑧(Hom ‘𝐶)𝑤) ∈ 𝑈)
95	84, 94	sseldd 3975	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → (𝑧(Hom ‘𝐶)𝑤) ∈ 𝑉)
96		eqid 2724	. . . . . . . . . 10 ⊢ (Hom_f ‘𝑄) = (Hom_f ‘𝑄)
97		eqid 2724	. . . . . . . . . . 11 ⊢ (𝑂 Nat 𝑆) = (𝑂 Nat 𝑆)
98	6, 97	fuchom 17915	. . . . . . . . . 10 ⊢ (𝑂 Nat 𝑆) = (Hom ‘𝑄)
99	61, 64	ffvelcdmd 7077	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → ((1^st ‘𝑌)‘𝑧) ∈ (𝑂 Func 𝑆))
100	96, 51, 98, 99, 63	homfval 17635	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → (((1^st ‘𝑌)‘𝑧)(Hom_f ‘𝑄)((1^st ‘𝑌)‘𝑤)) = (((1^st ‘𝑌)‘𝑧)(𝑂 Nat 𝑆)((1^st ‘𝑌)‘𝑤)))
101	8	unssad 4179	. . . . . . . . . . 11 ⊢ (𝜑 → ran (Hom_f ‘𝑄) ⊆ 𝑉)
102	101	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → ran (Hom_f ‘𝑄) ⊆ 𝑉)
103	96, 51	homffn 17636	. . . . . . . . . . 11 ⊢ (Hom_f ‘𝑄) Fn ((𝑂 Func 𝑆) × (𝑂 Func 𝑆))
104		fnovrn 7575	. . . . . . . . . . 11 ⊢ (((Hom_f ‘𝑄) Fn ((𝑂 Func 𝑆) × (𝑂 Func 𝑆)) ∧ ((1^st ‘𝑌)‘𝑧) ∈ (𝑂 Func 𝑆) ∧ ((1^st ‘𝑌)‘𝑤) ∈ (𝑂 Func 𝑆)) → (((1^st ‘𝑌)‘𝑧)(Hom_f ‘𝑄)((1^st ‘𝑌)‘𝑤)) ∈ ran (Hom_f ‘𝑄))
105	103, 99, 63, 104	mp3an2i 1462	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → (((1^st ‘𝑌)‘𝑧)(Hom_f ‘𝑄)((1^st ‘𝑌)‘𝑤)) ∈ ran (Hom_f ‘𝑄))
106	102, 105	sseldd 3975	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → (((1^st ‘𝑌)‘𝑧)(Hom_f ‘𝑄)((1^st ‘𝑌)‘𝑤)) ∈ 𝑉)
107	100, 106	eqeltrrd 2826	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → (((1^st ‘𝑌)‘𝑧)(𝑂 Nat 𝑆)((1^st ‘𝑌)‘𝑤)) ∈ 𝑉)
108	33, 78, 95, 107, 55	setciso 18043	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → ((((1^st ‘𝑌)‘𝑤)𝑁𝑧) ∈ ((𝑧(Hom ‘𝐶)𝑤)(Iso‘𝑇)(((1^st ‘𝑌)‘𝑧)(𝑂 Nat 𝑆)((1^st ‘𝑌)‘𝑤))) ↔ (((1^st ‘𝑌)‘𝑤)𝑁𝑧):(𝑧(Hom ‘𝐶)𝑤)–1-1-onto→(((1^st ‘𝑌)‘𝑧)(𝑂 Nat 𝑆)((1^st ‘𝑌)‘𝑤))))
109	83, 108	mpbid 231	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → (((1^st ‘𝑌)‘𝑤)𝑁𝑧):(𝑧(Hom ‘𝐶)𝑤)–1-1-onto→(((1^st ‘𝑌)‘𝑧)(𝑂 Nat 𝑆)((1^st ‘𝑌)‘𝑤)))
110	74	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝐶 ∈ Cat)
111	110	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ 𝑦 ∈ 𝐵) → 𝐶 ∈ Cat)
112	64	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑧 ∈ 𝐵)
113	112	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ 𝑦 ∈ 𝐵) → 𝑧 ∈ 𝐵)
114		simpr 484	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ 𝐵)
115	2, 31, 111, 113, 75, 114	yon11 18219	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ 𝑦 ∈ 𝐵) → ((1^st ‘((1^st ‘𝑌)‘𝑧))‘𝑦) = (𝑦(Hom ‘𝐶)𝑧))
116	115	eqcomd 2730	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ 𝑦 ∈ 𝐵) → (𝑦(Hom ‘𝐶)𝑧) = ((1^st ‘((1^st ‘𝑌)‘𝑧))‘𝑦))
117	111	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ 𝑦 ∈ 𝐵) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) → 𝐶 ∈ Cat)
118	62	ad3antrrr 727	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ 𝑦 ∈ 𝐵) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) → 𝑤 ∈ 𝐵)
119	113	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ 𝑦 ∈ 𝐵) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) → 𝑧 ∈ 𝐵)
120		eqid 2724	. . . . . . . . . . . . . . 15 ⊢ (comp‘𝐶) = (comp‘𝐶)
121	114	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ 𝑦 ∈ 𝐵) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) → 𝑦 ∈ 𝐵)
122		simpr 484	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ 𝑦 ∈ 𝐵) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) → 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))
123		simpllr 773	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ 𝑦 ∈ 𝐵) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) → ℎ ∈ (𝑧(Hom ‘𝐶)𝑤))
124	2, 31, 117, 118, 75, 119, 120, 121, 122, 123	yon12 18220	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ 𝑦 ∈ 𝐵) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) → (((𝑧(2^nd ‘((1^st ‘𝑌)‘𝑤))𝑦)‘𝑔)‘ℎ) = (ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔))
125	2, 31, 117, 119, 75, 118, 120, 121, 123, 122	yon2 18221	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ 𝑦 ∈ 𝐵) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) → ((((𝑧(2^nd ‘𝑌)𝑤)‘ℎ)‘𝑦)‘𝑔) = (ℎ(⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔))
126	124, 125	eqtr4d 2767	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ 𝑦 ∈ 𝐵) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) → (((𝑧(2^nd ‘((1^st ‘𝑌)‘𝑤))𝑦)‘𝑔)‘ℎ) = ((((𝑧(2^nd ‘𝑌)𝑤)‘ℎ)‘𝑦)‘𝑔))
127	116, 126	mpteq12dva 5227	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ 𝑦 ∈ 𝐵) → (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧) ↦ (((𝑧(2^nd ‘((1^st ‘𝑌)‘𝑤))𝑦)‘𝑔)‘ℎ)) = (𝑔 ∈ ((1^st ‘((1^st ‘𝑌)‘𝑧))‘𝑦) ↦ ((((𝑧(2^nd ‘𝑌)𝑤)‘ℎ)‘𝑦)‘𝑔)))
128	16	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → (1^st ‘𝑌)(𝐶 Func 𝑄)(2^nd ‘𝑌))
129	31, 75, 98, 128, 64, 62	funcf2 17817	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → (𝑧(2^nd ‘𝑌)𝑤):(𝑧(Hom ‘𝐶)𝑤)⟶(((1^st ‘𝑌)‘𝑧)(𝑂 Nat 𝑆)((1^st ‘𝑌)‘𝑤)))
130	129	ffvelcdmda 7076	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑧(2^nd ‘𝑌)𝑤)‘ℎ) ∈ (((1^st ‘𝑌)‘𝑧)(𝑂 Nat 𝑆)((1^st ‘𝑌)‘𝑤)))
131	97, 130	nat1st2nd 17904	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑧(2^nd ‘𝑌)𝑤)‘ℎ) ∈ (⟨(1^st ‘((1^st ‘𝑌)‘𝑧)), (2^nd ‘((1^st ‘𝑌)‘𝑧))⟩(𝑂 Nat 𝑆)⟨(1^st ‘((1^st ‘𝑌)‘𝑤)), (2^nd ‘((1^st ‘𝑌)‘𝑤))⟩))
132	131	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ 𝑦 ∈ 𝐵) → ((𝑧(2^nd ‘𝑌)𝑤)‘ℎ) ∈ (⟨(1^st ‘((1^st ‘𝑌)‘𝑧)), (2^nd ‘((1^st ‘𝑌)‘𝑧))⟩(𝑂 Nat 𝑆)⟨(1^st ‘((1^st ‘𝑌)‘𝑤)), (2^nd ‘((1^st ‘𝑌)‘𝑤))⟩))
133		eqid 2724	. . . . . . . . . . . . . . 15 ⊢ (Hom ‘𝑆) = (Hom ‘𝑆)
134	97, 132, 52, 133, 114	natcl 17906	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ 𝑦 ∈ 𝐵) → (((𝑧(2^nd ‘𝑌)𝑤)‘ℎ)‘𝑦) ∈ (((1^st ‘((1^st ‘𝑌)‘𝑧))‘𝑦)(Hom ‘𝑆)((1^st ‘((1^st ‘𝑌)‘𝑤))‘𝑦)))
135	10	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → 𝑈 ∈ V)
136	135	ad2antrr 723	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ 𝑦 ∈ 𝐵) → 𝑈 ∈ V)
137	60	ad2antrr 723	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) → (1^st ‘𝑌):𝐵⟶(𝑂 Func 𝑆))
138	137, 112	ffvelcdmd 7077	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((1^st ‘𝑌)‘𝑧) ∈ (𝑂 Func 𝑆))
139		1st2ndbr 8021	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Rel (𝑂 Func 𝑆) ∧ ((1^st ‘𝑌)‘𝑧) ∈ (𝑂 Func 𝑆)) → (1^st ‘((1^st ‘𝑌)‘𝑧))(𝑂 Func 𝑆)(2^nd ‘((1^st ‘𝑌)‘𝑧)))
140	86, 138, 139	sylancr 586	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) → (1^st ‘((1^st ‘𝑌)‘𝑧))(𝑂 Func 𝑆)(2^nd ‘((1^st ‘𝑌)‘𝑧)))
141	52, 85, 140	funcf1 17815	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) → (1^st ‘((1^st ‘𝑌)‘𝑧)):𝐵⟶(Base‘𝑆))
142	141	ffvelcdmda 7076	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ 𝑦 ∈ 𝐵) → ((1^st ‘((1^st ‘𝑌)‘𝑧))‘𝑦) ∈ (Base‘𝑆))
143	92	ad2antrr 723	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ 𝑦 ∈ 𝐵) → 𝑈 = (Base‘𝑆))
144	142, 143	eleqtrrd 2828	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ 𝑦 ∈ 𝐵) → ((1^st ‘((1^st ‘𝑌)‘𝑧))‘𝑦) ∈ 𝑈)
145	89	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) → (1^st ‘((1^st ‘𝑌)‘𝑤)):𝐵⟶(Base‘𝑆))
146	145	ffvelcdmda 7076	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ 𝑦 ∈ 𝐵) → ((1^st ‘((1^st ‘𝑌)‘𝑤))‘𝑦) ∈ (Base‘𝑆))
147	146, 143	eleqtrrd 2828	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ 𝑦 ∈ 𝐵) → ((1^st ‘((1^st ‘𝑌)‘𝑤))‘𝑦) ∈ 𝑈)
148	5, 136, 133, 144, 147	elsetchom 18033	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ 𝑦 ∈ 𝐵) → ((((𝑧(2^nd ‘𝑌)𝑤)‘ℎ)‘𝑦) ∈ (((1^st ‘((1^st ‘𝑌)‘𝑧))‘𝑦)(Hom ‘𝑆)((1^st ‘((1^st ‘𝑌)‘𝑤))‘𝑦)) ↔ (((𝑧(2^nd ‘𝑌)𝑤)‘ℎ)‘𝑦):((1^st ‘((1^st ‘𝑌)‘𝑧))‘𝑦)⟶((1^st ‘((1^st ‘𝑌)‘𝑤))‘𝑦)))
149	134, 148	mpbid 231	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ 𝑦 ∈ 𝐵) → (((𝑧(2^nd ‘𝑌)𝑤)‘ℎ)‘𝑦):((1^st ‘((1^st ‘𝑌)‘𝑧))‘𝑦)⟶((1^st ‘((1^st ‘𝑌)‘𝑤))‘𝑦))
150	149	feqmptd 6950	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ 𝑦 ∈ 𝐵) → (((𝑧(2^nd ‘𝑌)𝑤)‘ℎ)‘𝑦) = (𝑔 ∈ ((1^st ‘((1^st ‘𝑌)‘𝑧))‘𝑦) ↦ ((((𝑧(2^nd ‘𝑌)𝑤)‘ℎ)‘𝑦)‘𝑔)))
151	127, 150	eqtr4d 2767	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ 𝑦 ∈ 𝐵) → (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧) ↦ (((𝑧(2^nd ‘((1^st ‘𝑌)‘𝑤))𝑦)‘𝑔)‘ℎ)) = (((𝑧(2^nd ‘𝑌)𝑤)‘ℎ)‘𝑦))
152	151	mpteq2dva 5238	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) → (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧) ↦ (((𝑧(2^nd ‘((1^st ‘𝑌)‘𝑤))𝑦)‘𝑔)‘ℎ))) = (𝑦 ∈ 𝐵 ↦ (((𝑧(2^nd ‘𝑌)𝑤)‘ℎ)‘𝑦)))
153	78	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑉 ∈ 𝑊)
154	79	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) → ran (Hom_f ‘𝐶) ⊆ 𝑈)
155	80	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) → (ran (Hom_f ‘𝑄) ∪ 𝑈) ⊆ 𝑉)
156	63	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((1^st ‘𝑌)‘𝑤) ∈ (𝑂 Func 𝑆))
157	76	eleq2d 2811	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → (ℎ ∈ ((1^st ‘((1^st ‘𝑌)‘𝑤))‘𝑧) ↔ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)))
158	157	biimpar 477	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) → ℎ ∈ ((1^st ‘((1^st ‘𝑌)‘𝑤))‘𝑧))
159	2, 31, 32, 4, 5, 33, 6, 34, 28, 35, 36, 110, 153, 154, 155, 156, 112, 47, 158	yonedalem4a 18230	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((((1^st ‘𝑌)‘𝑤)𝑁𝑧)‘ℎ) = (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧) ↦ (((𝑧(2^nd ‘((1^st ‘𝑌)‘𝑤))𝑦)‘𝑔)‘ℎ))))
160	97, 131, 52	natfn 17907	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑧(2^nd ‘𝑌)𝑤)‘ℎ) Fn 𝐵)
161		dffn5 6940	. . . . . . . . . . 11 ⊢ (((𝑧(2^nd ‘𝑌)𝑤)‘ℎ) Fn 𝐵 ↔ ((𝑧(2^nd ‘𝑌)𝑤)‘ℎ) = (𝑦 ∈ 𝐵 ↦ (((𝑧(2^nd ‘𝑌)𝑤)‘ℎ)‘𝑦)))
162	160, 161	sylib 217	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑧(2^nd ‘𝑌)𝑤)‘ℎ) = (𝑦 ∈ 𝐵 ↦ (((𝑧(2^nd ‘𝑌)𝑤)‘ℎ)‘𝑦)))
163	152, 159, 162	3eqtr4d 2774	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) ∧ ℎ ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((((1^st ‘𝑌)‘𝑤)𝑁𝑧)‘ℎ) = ((𝑧(2^nd ‘𝑌)𝑤)‘ℎ))
164	163	mpteq2dva 5238	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → (ℎ ∈ (𝑧(Hom ‘𝐶)𝑤) ↦ ((((1^st ‘𝑌)‘𝑤)𝑁𝑧)‘ℎ)) = (ℎ ∈ (𝑧(Hom ‘𝐶)𝑤) ↦ ((𝑧(2^nd ‘𝑌)𝑤)‘ℎ)))
165		f1of 6823	. . . . . . . . . 10 ⊢ ((((1^st ‘𝑌)‘𝑤)𝑁𝑧):(𝑧(Hom ‘𝐶)𝑤)–1-1-onto→(((1^st ‘𝑌)‘𝑧)(𝑂 Nat 𝑆)((1^st ‘𝑌)‘𝑤)) → (((1^st ‘𝑌)‘𝑤)𝑁𝑧):(𝑧(Hom ‘𝐶)𝑤)⟶(((1^st ‘𝑌)‘𝑧)(𝑂 Nat 𝑆)((1^st ‘𝑌)‘𝑤)))
166	109, 165	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → (((1^st ‘𝑌)‘𝑤)𝑁𝑧):(𝑧(Hom ‘𝐶)𝑤)⟶(((1^st ‘𝑌)‘𝑧)(𝑂 Nat 𝑆)((1^st ‘𝑌)‘𝑤)))
167	166	feqmptd 6950	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → (((1^st ‘𝑌)‘𝑤)𝑁𝑧) = (ℎ ∈ (𝑧(Hom ‘𝐶)𝑤) ↦ ((((1^st ‘𝑌)‘𝑤)𝑁𝑧)‘ℎ)))
168	129	feqmptd 6950	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → (𝑧(2^nd ‘𝑌)𝑤) = (ℎ ∈ (𝑧(Hom ‘𝐶)𝑤) ↦ ((𝑧(2^nd ‘𝑌)𝑤)‘ℎ)))
169	164, 167, 168	3eqtr4d 2774	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → (((1^st ‘𝑌)‘𝑤)𝑁𝑧) = (𝑧(2^nd ‘𝑌)𝑤))
170	169	f1oeq1d 6818	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → ((((1^st ‘𝑌)‘𝑤)𝑁𝑧):(𝑧(Hom ‘𝐶)𝑤)–1-1-onto→(((1^st ‘𝑌)‘𝑧)(𝑂 Nat 𝑆)((1^st ‘𝑌)‘𝑤)) ↔ (𝑧(2^nd ‘𝑌)𝑤):(𝑧(Hom ‘𝐶)𝑤)–1-1-onto→(((1^st ‘𝑌)‘𝑧)(𝑂 Nat 𝑆)((1^st ‘𝑌)‘𝑤))))
171	109, 170	mpbid 231	. . . . 5 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → (𝑧(2^nd ‘𝑌)𝑤):(𝑧(Hom ‘𝐶)𝑤)–1-1-onto→(((1^st ‘𝑌)‘𝑧)(𝑂 Nat 𝑆)((1^st ‘𝑌)‘𝑤)))
172	171	ralrimivva 3192	. . . 4 ⊢ (𝜑 → ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐵 (𝑧(2^nd ‘𝑌)𝑤):(𝑧(Hom ‘𝐶)𝑤)–1-1-onto→(((1^st ‘𝑌)‘𝑧)(𝑂 Nat 𝑆)((1^st ‘𝑌)‘𝑤)))
173	31, 75, 98	isffth2 17868	. . . 4 ⊢ ((1^st ‘𝑌)((𝐶 Full 𝑄) ∩ (𝐶 Faith 𝑄))(2^nd ‘𝑌) ↔ ((1^st ‘𝑌)(𝐶 Func 𝑄)(2^nd ‘𝑌) ∧ ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐵 (𝑧(2^nd ‘𝑌)𝑤):(𝑧(Hom ‘𝐶)𝑤)–1-1-onto→(((1^st ‘𝑌)‘𝑧)(𝑂 Nat 𝑆)((1^st ‘𝑌)‘𝑤))))
174	16, 172, 173	sylanbrc 582	. . 3 ⊢ (𝜑 → (1^st ‘𝑌)((𝐶 Full 𝑄) ∩ (𝐶 Faith 𝑄))(2^nd ‘𝑌))
175		df-br 5139	. . 3 ⊢ ((1^st ‘𝑌)((𝐶 Full 𝑄) ∩ (𝐶 Faith 𝑄))(2^nd ‘𝑌) ↔ ⟨(1^st ‘𝑌), (2^nd ‘𝑌)⟩ ∈ ((𝐶 Full 𝑄) ∩ (𝐶 Faith 𝑄)))
176	174, 175	sylib 217	. 2 ⊢ (𝜑 → ⟨(1^st ‘𝑌), (2^nd ‘𝑌)⟩ ∈ ((𝐶 Full 𝑄) ∩ (𝐶 Faith 𝑄)))
177	14, 176	eqeltrd 2825	1 ⊢ (𝜑 → 𝑌 ∈ ((𝐶 Full 𝑄) ∩ (𝐶 Faith 𝑄)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 = wceq 1533 ∈ wcel 2098 ∀wral 3053 Vcvv 3466 ∪ cun 3938 ∩ cin 3939 ⊆ wss 3940 ⟨cop 4626 class class class wbr 5138 ↦ cmpt 5221 × cxp 5664 ran crn 5667 Rel wrel 5671 Fn wfn 6528 ⟶wf 6529 –1-1-onto→wf1o 6532 ‘cfv 6533 (class class class)co 7401 ∈ cmpo 7403 1^st c1st 7966 2^nd c2nd 7967 tpos ctpos 8205 Basecbs 17143 Hom chom 17207 compcco 17208 Catccat 17607 Idccid 17608 Hom_f chomf 17609 oppCatcoppc 17654 Invcinv 17691 Isociso 17692 Func cfunc 17803 ∘_func ccofu 17805 Full cful 17854 Faith cfth 17855 Nat cnat 17894 FuncCat cfuc 17895 SetCatcsetc 18027 ×_c cxpc 18122 1^st_F c1stf 18123 2^nd_F c2ndf 18124 ⟨,⟩_F cprf 18125 eval_F cevlf 18164 Hom_Fchof 18203 Yoncyon 18204

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2163 ax-ext 2695 ax-rep 5275 ax-sep 5289 ax-nul 5296 ax-pow 5353 ax-pr 5417 ax-un 7718 ax-cnex 11162 ax-resscn 11163 ax-1cn 11164 ax-icn 11165 ax-addcl 11166 ax-addrcl 11167 ax-mulcl 11168 ax-mulrcl 11169 ax-mulcom 11170 ax-addass 11171 ax-mulass 11172 ax-distr 11173 ax-i2m1 11174 ax-1ne0 11175 ax-1rid 11176 ax-rnegex 11177 ax-rrecex 11178 ax-cnre 11179 ax-pre-lttri 11180 ax-pre-lttrn 11181 ax-pre-ltadd 11182 ax-pre-mulgt0 11183

This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3or 1085 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2526 df-eu 2555 df-clab 2702 df-cleq 2716 df-clel 2802 df-nfc 2877 df-ne 2933 df-nel 3039 df-ral 3054 df-rex 3063 df-rmo 3368 df-reu 3369 df-rab 3425 df-v 3468 df-sbc 3770 df-csb 3886 df-dif 3943 df-un 3945 df-in 3947 df-ss 3957 df-pss 3959 df-nul 4315 df-if 4521 df-pw 4596 df-sn 4621 df-pr 4623 df-tp 4625 df-op 4627 df-uni 4900 df-iun 4989 df-br 5139 df-opab 5201 df-mpt 5222 df-tr 5256 df-id 5564 df-eprel 5570 df-po 5578 df-so 5579 df-fr 5621 df-we 5623 df-xp 5672 df-rel 5673 df-cnv 5674 df-co 5675 df-dm 5676 df-rn 5677 df-res 5678 df-ima 5679 df-pred 6290 df-ord 6357 df-on 6358 df-lim 6359 df-suc 6360 df-iota 6485 df-fun 6535 df-fn 6536 df-f 6537 df-f1 6538 df-fo 6539 df-f1o 6540 df-fv 6541 df-riota 7357 df-ov 7404 df-oprab 7405 df-mpo 7406 df-om 7849 df-1st 7968 df-2nd 7969 df-tpos 8206 df-frecs 8261 df-wrecs 8292 df-recs 8366 df-rdg 8405 df-1o 8461 df-er 8699 df-map 8818 df-pm 8819 df-ixp 8888 df-en 8936 df-dom 8937 df-sdom 8938 df-fin 8939 df-pnf 11247 df-mnf 11248 df-xr 11249 df-ltxr 11250 df-le 11251 df-sub 11443 df-neg 11444 df-nn 12210 df-2 12272 df-3 12273 df-4 12274 df-5 12275 df-6 12276 df-7 12277 df-8 12278 df-9 12279 df-n0 12470 df-z 12556 df-dec 12675 df-uz 12820 df-fz 13482 df-struct 17079 df-sets 17096 df-slot 17114 df-ndx 17126 df-base 17144 df-ress 17173 df-hom 17220 df-cco 17221 df-cat 17611 df-cid 17612 df-homf 17613 df-comf 17614 df-oppc 17655 df-sect 17693 df-inv 17694 df-iso 17695 df-ssc 17756 df-resc 17757 df-subc 17758 df-func 17807 df-cofu 17809 df-full 17856 df-fth 17857 df-nat 17896 df-fuc 17897 df-setc 18028 df-xpc 18126 df-1stf 18127 df-2ndf 18128 df-prf 18129 df-evlf 18168 df-curf 18169 df-hof 18205 df-yon 18206

This theorem is referenced by: yonffth 18239

W3C validator