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

Theorem yonffthlem 17390
Description: Lemma for yonffth 17392. (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 𝐻 = (HomF𝑄)
yoneda.r 𝑅 = ((𝑄 ×c 𝑂) FuncCat 𝑇)
yoneda.e 𝐸 = (𝑂 evalF 𝑆)
yoneda.z 𝑍 = (𝐻func ((⟨(1st𝑌), tpos (2nd𝑌)⟩ ∘func (𝑄 2ndF 𝑂)) ⟨,⟩F (𝑄 1stF 𝑂)))
yoneda.c (𝜑𝐶 ∈ Cat)
yoneda.w (𝜑𝑉𝑊)
yoneda.u (𝜑 → ran (Homf𝐶) ⊆ 𝑈)
yoneda.v (𝜑 → (ran (Homf𝑄) ∪ 𝑈) ⊆ 𝑉)
yoneda.m 𝑀 = (𝑓 ∈ (𝑂 Func 𝑆), 𝑥𝐵 ↦ (𝑎 ∈ (((1st𝑌)‘𝑥)(𝑂 Nat 𝑆)𝑓) ↦ ((𝑎𝑥)‘( 1𝑥))))
yonedainv.i 𝐼 = (Inv‘𝑅)
yonedainv.n 𝑁 = (𝑓 ∈ (𝑂 Func 𝑆), 𝑥𝐵 ↦ (𝑢 ∈ ((1st𝑓)‘𝑥) ↦ (𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥) ↦ (((𝑥(2nd𝑓)𝑦)‘𝑔)‘𝑢)))))
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.
StepHypRef Expression
1 relfunc 16990 . . 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 (Homf𝑄) ∪ 𝑈) ⊆ 𝑉)
98unssbd 4053 . . . . 5 (𝜑𝑈𝑉)
107, 9ssexd 5084 . . . 4 (𝜑𝑈 ∈ V)
11 yoneda.u . . . 4 (𝜑 → ran (Homf𝐶) ⊆ 𝑈)
122, 3, 4, 5, 6, 10, 11yoncl 17370 . . 3 (𝜑𝑌 ∈ (𝐶 Func 𝑄))
13 1st2nd 7550 . . 3 ((Rel (𝐶 Func 𝑄) ∧ 𝑌 ∈ (𝐶 Func 𝑄)) → 𝑌 = ⟨(1st𝑌), (2nd𝑌)⟩)
141, 12, 13sylancr 578 . 2 (𝜑𝑌 = ⟨(1st𝑌), (2nd𝑌)⟩)
15 1st2ndbr 7553 . . . . 5 ((Rel (𝐶 Func 𝑄) ∧ 𝑌 ∈ (𝐶 Func 𝑄)) → (1st𝑌)(𝐶 Func 𝑄)(2nd𝑌))
161, 12, 15sylancr 578 . . . 4 (𝜑 → (1st𝑌)(𝐶 Func 𝑄)(2nd𝑌))
17 fveq2 6499 . . . . . . . . . . 11 (𝑣 = ⟨((1st𝑌)‘𝑤), 𝑧⟩ → (𝑁𝑣) = (𝑁‘⟨((1st𝑌)‘𝑤), 𝑧⟩))
18 df-ov 6979 . . . . . . . . . . 11 (((1st𝑌)‘𝑤)𝑁𝑧) = (𝑁‘⟨((1st𝑌)‘𝑤), 𝑧⟩)
1917, 18syl6eqr 2833 . . . . . . . . . 10 (𝑣 = ⟨((1st𝑌)‘𝑤), 𝑧⟩ → (𝑁𝑣) = (((1st𝑌)‘𝑤)𝑁𝑧))
20 fveq2 6499 . . . . . . . . . . . 12 (𝑣 = ⟨((1st𝑌)‘𝑤), 𝑧⟩ → ((1st𝐸)‘𝑣) = ((1st𝐸)‘⟨((1st𝑌)‘𝑤), 𝑧⟩))
21 df-ov 6979 . . . . . . . . . . . 12 (((1st𝑌)‘𝑤)(1st𝐸)𝑧) = ((1st𝐸)‘⟨((1st𝑌)‘𝑤), 𝑧⟩)
2220, 21syl6eqr 2833 . . . . . . . . . . 11 (𝑣 = ⟨((1st𝑌)‘𝑤), 𝑧⟩ → ((1st𝐸)‘𝑣) = (((1st𝑌)‘𝑤)(1st𝐸)𝑧))
23 fveq2 6499 . . . . . . . . . . . 12 (𝑣 = ⟨((1st𝑌)‘𝑤), 𝑧⟩ → ((1st𝑍)‘𝑣) = ((1st𝑍)‘⟨((1st𝑌)‘𝑤), 𝑧⟩))
24 df-ov 6979 . . . . . . . . . . . 12 (((1st𝑌)‘𝑤)(1st𝑍)𝑧) = ((1st𝑍)‘⟨((1st𝑌)‘𝑤), 𝑧⟩)
2523, 24syl6eqr 2833 . . . . . . . . . . 11 (𝑣 = ⟨((1st𝑌)‘𝑤), 𝑧⟩ → ((1st𝑍)‘𝑣) = (((1st𝑌)‘𝑤)(1st𝑍)𝑧))
2622, 25oveq12d 6994 . . . . . . . . . 10 (𝑣 = ⟨((1st𝑌)‘𝑤), 𝑧⟩ → (((1st𝐸)‘𝑣)(Iso‘𝑇)((1st𝑍)‘𝑣)) = ((((1st𝑌)‘𝑤)(1st𝐸)𝑧)(Iso‘𝑇)(((1st𝑌)‘𝑤)(1st𝑍)𝑧)))
2719, 26eleq12d 2861 . . . . . . . . 9 (𝑣 = ⟨((1st𝑌)‘𝑤), 𝑧⟩ → ((𝑁𝑣) ∈ (((1st𝐸)‘𝑣)(Iso‘𝑇)((1st𝑍)‘𝑣)) ↔ (((1st𝑌)‘𝑤)𝑁𝑧) ∈ ((((1st𝑌)‘𝑤)(1st𝐸)𝑧)(Iso‘𝑇)(((1st𝑌)‘𝑤)(1st𝑍)𝑧))))
28 yoneda.r . . . . . . . . . . . . . 14 𝑅 = ((𝑄 ×c 𝑂) FuncCat 𝑇)
2928fucbas 17088 . . . . . . . . . . . . 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 𝐻 = (HomF𝑄)
35 yoneda.e . . . . . . . . . . . . . . . . . 18 𝐸 = (𝑂 evalF 𝑆)
36 yoneda.z . . . . . . . . . . . . . . . . . 18 𝑍 = (𝐻func ((⟨(1st𝑌), tpos (2nd𝑌)⟩ ∘func (𝑄 2ndF 𝑂)) ⟨,⟩F (𝑄 1stF 𝑂)))
372, 31, 32, 4, 5, 33, 6, 34, 28, 35, 36, 3, 7, 11, 8yonedalem1 17380 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑍 ∈ ((𝑄 ×c 𝑂) Func 𝑇) ∧ 𝐸 ∈ ((𝑄 ×c 𝑂) Func 𝑇)))
3837simpld 487 . . . . . . . . . . . . . . . 16 (𝜑𝑍 ∈ ((𝑄 ×c 𝑂) Func 𝑇))
39 funcrcl 16991 . . . . . . . . . . . . . . . 16 (𝑍 ∈ ((𝑄 ×c 𝑂) Func 𝑇) → ((𝑄 ×c 𝑂) ∈ Cat ∧ 𝑇 ∈ Cat))
4038, 39syl 17 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑄 ×c 𝑂) ∈ Cat ∧ 𝑇 ∈ Cat))
4140simpld 487 . . . . . . . . . . . . . 14 (𝜑 → (𝑄 ×c 𝑂) ∈ Cat)
4240simprd 488 . . . . . . . . . . . . . 14 (𝜑𝑇 ∈ Cat)
4328, 41, 42fuccat 17098 . . . . . . . . . . . . 13 (𝜑𝑅 ∈ Cat)
4437simprd 488 . . . . . . . . . . . . 13 (𝜑𝐸 ∈ ((𝑄 ×c 𝑂) Func 𝑇))
45 eqid 2779 . . . . . . . . . . . . 13 (Iso‘𝑅) = (Iso‘𝑅)
46 yoneda.m . . . . . . . . . . . . . 14 𝑀 = (𝑓 ∈ (𝑂 Func 𝑆), 𝑥𝐵 ↦ (𝑎 ∈ (((1st𝑌)‘𝑥)(𝑂 Nat 𝑆)𝑓) ↦ ((𝑎𝑥)‘( 1𝑥))))
47 yonedainv.n . . . . . . . . . . . . . 14 𝑁 = (𝑓 ∈ (𝑂 Func 𝑆), 𝑥𝐵 ↦ (𝑢 ∈ ((1st𝑓)‘𝑥) ↦ (𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥) ↦ (((𝑥(2nd𝑓)𝑦)‘𝑔)‘𝑢)))))
482, 31, 32, 4, 5, 33, 6, 34, 28, 35, 36, 3, 7, 11, 8, 46, 30, 47yonedainv 17389 . . . . . . . . . . . . 13 (𝜑𝑀(𝑍𝐼𝐸)𝑁)
4929, 30, 43, 38, 44, 45, 48inviso2 16895 . . . . . . . . . . . 12 (𝜑𝑁 ∈ (𝐸(Iso‘𝑅)𝑍))
50 eqid 2779 . . . . . . . . . . . . . 14 (𝑄 ×c 𝑂) = (𝑄 ×c 𝑂)
516fucbas 17088 . . . . . . . . . . . . . 14 (𝑂 Func 𝑆) = (Base‘𝑄)
524, 31oppcbas 16846 . . . . . . . . . . . . . 14 𝐵 = (Base‘𝑂)
5350, 51, 52xpcbas 17286 . . . . . . . . . . . . 13 ((𝑂 Func 𝑆) × 𝐵) = (Base‘(𝑄 ×c 𝑂))
54 eqid 2779 . . . . . . . . . . . . 13 ((𝑄 ×c 𝑂) Nat 𝑇) = ((𝑄 ×c 𝑂) Nat 𝑇)
55 eqid 2779 . . . . . . . . . . . . 13 (Iso‘𝑇) = (Iso‘𝑇)
5628, 53, 54, 44, 38, 45, 55fuciso 17103 . . . . . . . . . . . 12 (𝜑 → (𝑁 ∈ (𝐸(Iso‘𝑅)𝑍) ↔ (𝑁 ∈ (𝐸((𝑄 ×c 𝑂) Nat 𝑇)𝑍) ∧ ∀𝑣 ∈ ((𝑂 Func 𝑆) × 𝐵)(𝑁𝑣) ∈ (((1st𝐸)‘𝑣)(Iso‘𝑇)((1st𝑍)‘𝑣)))))
5749, 56mpbid 224 . . . . . . . . . . 11 (𝜑 → (𝑁 ∈ (𝐸((𝑄 ×c 𝑂) Nat 𝑇)𝑍) ∧ ∀𝑣 ∈ ((𝑂 Func 𝑆) × 𝐵)(𝑁𝑣) ∈ (((1st𝐸)‘𝑣)(Iso‘𝑇)((1st𝑍)‘𝑣))))
5857simprd 488 . . . . . . . . . 10 (𝜑 → ∀𝑣 ∈ ((𝑂 Func 𝑆) × 𝐵)(𝑁𝑣) ∈ (((1st𝐸)‘𝑣)(Iso‘𝑇)((1st𝑍)‘𝑣)))
5958adantr 473 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝐵𝑤𝐵)) → ∀𝑣 ∈ ((𝑂 Func 𝑆) × 𝐵)(𝑁𝑣) ∈ (((1st𝐸)‘𝑣)(Iso‘𝑇)((1st𝑍)‘𝑣)))
6031, 51, 16funcf1 16994 . . . . . . . . . . . 12 (𝜑 → (1st𝑌):𝐵⟶(𝑂 Func 𝑆))
6160adantr 473 . . . . . . . . . . 11 ((𝜑 ∧ (𝑧𝐵𝑤𝐵)) → (1st𝑌):𝐵⟶(𝑂 Func 𝑆))
62 simprr 760 . . . . . . . . . . 11 ((𝜑 ∧ (𝑧𝐵𝑤𝐵)) → 𝑤𝐵)
6361, 62ffvelrnd 6677 . . . . . . . . . 10 ((𝜑 ∧ (𝑧𝐵𝑤𝐵)) → ((1st𝑌)‘𝑤) ∈ (𝑂 Func 𝑆))
64 simprl 758 . . . . . . . . . 10 ((𝜑 ∧ (𝑧𝐵𝑤𝐵)) → 𝑧𝐵)
6563, 64opelxpd 5445 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝐵𝑤𝐵)) → ⟨((1st𝑌)‘𝑤), 𝑧⟩ ∈ ((𝑂 Func 𝑆) × 𝐵))
6627, 59, 65rspcdva 3542 . . . . . . . 8 ((𝜑 ∧ (𝑧𝐵𝑤𝐵)) → (((1st𝑌)‘𝑤)𝑁𝑧) ∈ ((((1st𝑌)‘𝑤)(1st𝐸)𝑧)(Iso‘𝑇)(((1st𝑌)‘𝑤)(1st𝑍)𝑧)))
674oppccat 16850 . . . . . . . . . . . . 13 (𝐶 ∈ Cat → 𝑂 ∈ Cat)
683, 67syl 17 . . . . . . . . . . . 12 (𝜑𝑂 ∈ Cat)
6968adantr 473 . . . . . . . . . . 11 ((𝜑 ∧ (𝑧𝐵𝑤𝐵)) → 𝑂 ∈ Cat)
705setccat 17203 . . . . . . . . . . . . 13 (𝑈 ∈ V → 𝑆 ∈ Cat)
7110, 70syl 17 . . . . . . . . . . . 12 (𝜑𝑆 ∈ Cat)
7271adantr 473 . . . . . . . . . . 11 ((𝜑 ∧ (𝑧𝐵𝑤𝐵)) → 𝑆 ∈ Cat)
7335, 69, 72, 52, 63, 64evlf1 17328 . . . . . . . . . 10 ((𝜑 ∧ (𝑧𝐵𝑤𝐵)) → (((1st𝑌)‘𝑤)(1st𝐸)𝑧) = ((1st ‘((1st𝑌)‘𝑤))‘𝑧))
743adantr 473 . . . . . . . . . . 11 ((𝜑 ∧ (𝑧𝐵𝑤𝐵)) → 𝐶 ∈ Cat)
75 eqid 2779 . . . . . . . . . . 11 (Hom ‘𝐶) = (Hom ‘𝐶)
762, 31, 74, 62, 75, 64yon11 17372 . . . . . . . . . 10 ((𝜑 ∧ (𝑧𝐵𝑤𝐵)) → ((1st ‘((1st𝑌)‘𝑤))‘𝑧) = (𝑧(Hom ‘𝐶)𝑤))
7773, 76eqtrd 2815 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝐵𝑤𝐵)) → (((1st𝑌)‘𝑤)(1st𝐸)𝑧) = (𝑧(Hom ‘𝐶)𝑤))
787adantr 473 . . . . . . . . . 10 ((𝜑 ∧ (𝑧𝐵𝑤𝐵)) → 𝑉𝑊)
7911adantr 473 . . . . . . . . . 10 ((𝜑 ∧ (𝑧𝐵𝑤𝐵)) → ran (Homf𝐶) ⊆ 𝑈)
808adantr 473 . . . . . . . . . 10 ((𝜑 ∧ (𝑧𝐵𝑤𝐵)) → (ran (Homf𝑄) ∪ 𝑈) ⊆ 𝑉)
812, 31, 32, 4, 5, 33, 6, 34, 28, 35, 36, 74, 78, 79, 80, 63, 64yonedalem21 17381 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝐵𝑤𝐵)) → (((1st𝑌)‘𝑤)(1st𝑍)𝑧) = (((1st𝑌)‘𝑧)(𝑂 Nat 𝑆)((1st𝑌)‘𝑤)))
8277, 81oveq12d 6994 . . . . . . . 8 ((𝜑 ∧ (𝑧𝐵𝑤𝐵)) → ((((1st𝑌)‘𝑤)(1st𝐸)𝑧)(Iso‘𝑇)(((1st𝑌)‘𝑤)(1st𝑍)𝑧)) = ((𝑧(Hom ‘𝐶)𝑤)(Iso‘𝑇)(((1st𝑌)‘𝑧)(𝑂 Nat 𝑆)((1st𝑌)‘𝑤))))
8366, 82eleqtrd 2869 . . . . . . 7 ((𝜑 ∧ (𝑧𝐵𝑤𝐵)) → (((1st𝑌)‘𝑤)𝑁𝑧) ∈ ((𝑧(Hom ‘𝐶)𝑤)(Iso‘𝑇)(((1st𝑌)‘𝑧)(𝑂 Nat 𝑆)((1st𝑌)‘𝑤))))
849adantr 473 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝐵𝑤𝐵)) → 𝑈𝑉)
85 eqid 2779 . . . . . . . . . . . . 13 (Base‘𝑆) = (Base‘𝑆)
86 relfunc 16990 . . . . . . . . . . . . . 14 Rel (𝑂 Func 𝑆)
87 1st2ndbr 7553 . . . . . . . . . . . . . 14 ((Rel (𝑂 Func 𝑆) ∧ ((1st𝑌)‘𝑤) ∈ (𝑂 Func 𝑆)) → (1st ‘((1st𝑌)‘𝑤))(𝑂 Func 𝑆)(2nd ‘((1st𝑌)‘𝑤)))
8886, 63, 87sylancr 578 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑧𝐵𝑤𝐵)) → (1st ‘((1st𝑌)‘𝑤))(𝑂 Func 𝑆)(2nd ‘((1st𝑌)‘𝑤)))
8952, 85, 88funcf1 16994 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑧𝐵𝑤𝐵)) → (1st ‘((1st𝑌)‘𝑤)):𝐵⟶(Base‘𝑆))
9089, 64ffvelrnd 6677 . . . . . . . . . . 11 ((𝜑 ∧ (𝑧𝐵𝑤𝐵)) → ((1st ‘((1st𝑌)‘𝑤))‘𝑧) ∈ (Base‘𝑆))
915, 10setcbas 17196 . . . . . . . . . . . 12 (𝜑𝑈 = (Base‘𝑆))
9291adantr 473 . . . . . . . . . . 11 ((𝜑 ∧ (𝑧𝐵𝑤𝐵)) → 𝑈 = (Base‘𝑆))
9390, 92eleqtrrd 2870 . . . . . . . . . 10 ((𝜑 ∧ (𝑧𝐵𝑤𝐵)) → ((1st ‘((1st𝑌)‘𝑤))‘𝑧) ∈ 𝑈)
9476, 93eqeltrrd 2868 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝐵𝑤𝐵)) → (𝑧(Hom ‘𝐶)𝑤) ∈ 𝑈)
9584, 94sseldd 3860 . . . . . . . 8 ((𝜑 ∧ (𝑧𝐵𝑤𝐵)) → (𝑧(Hom ‘𝐶)𝑤) ∈ 𝑉)
96 eqid 2779 . . . . . . . . . 10 (Homf𝑄) = (Homf𝑄)
97 eqid 2779 . . . . . . . . . . 11 (𝑂 Nat 𝑆) = (𝑂 Nat 𝑆)
986, 97fuchom 17089 . . . . . . . . . 10 (𝑂 Nat 𝑆) = (Hom ‘𝑄)
9961, 64ffvelrnd 6677 . . . . . . . . . 10 ((𝜑 ∧ (𝑧𝐵𝑤𝐵)) → ((1st𝑌)‘𝑧) ∈ (𝑂 Func 𝑆))
10096, 51, 98, 99, 63homfval 16820 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝐵𝑤𝐵)) → (((1st𝑌)‘𝑧)(Homf𝑄)((1st𝑌)‘𝑤)) = (((1st𝑌)‘𝑧)(𝑂 Nat 𝑆)((1st𝑌)‘𝑤)))
1018unssad 4052 . . . . . . . . . . 11 (𝜑 → ran (Homf𝑄) ⊆ 𝑉)
102101adantr 473 . . . . . . . . . 10 ((𝜑 ∧ (𝑧𝐵𝑤𝐵)) → ran (Homf𝑄) ⊆ 𝑉)
10396, 51homffn 16821 . . . . . . . . . . 11 (Homf𝑄) Fn ((𝑂 Func 𝑆) × (𝑂 Func 𝑆))
104 fnovrn 7139 . . . . . . . . . . 11 (((Homf𝑄) Fn ((𝑂 Func 𝑆) × (𝑂 Func 𝑆)) ∧ ((1st𝑌)‘𝑧) ∈ (𝑂 Func 𝑆) ∧ ((1st𝑌)‘𝑤) ∈ (𝑂 Func 𝑆)) → (((1st𝑌)‘𝑧)(Homf𝑄)((1st𝑌)‘𝑤)) ∈ ran (Homf𝑄))
105103, 99, 63, 104mp3an2i 1445 . . . . . . . . . 10 ((𝜑 ∧ (𝑧𝐵𝑤𝐵)) → (((1st𝑌)‘𝑧)(Homf𝑄)((1st𝑌)‘𝑤)) ∈ ran (Homf𝑄))
106102, 105sseldd 3860 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝐵𝑤𝐵)) → (((1st𝑌)‘𝑧)(Homf𝑄)((1st𝑌)‘𝑤)) ∈ 𝑉)
107100, 106eqeltrrd 2868 . . . . . . . 8 ((𝜑 ∧ (𝑧𝐵𝑤𝐵)) → (((1st𝑌)‘𝑧)(𝑂 Nat 𝑆)((1st𝑌)‘𝑤)) ∈ 𝑉)
10833, 78, 95, 107, 55setciso 17209 . . . . . . 7 ((𝜑 ∧ (𝑧𝐵𝑤𝐵)) → ((((1st𝑌)‘𝑤)𝑁𝑧) ∈ ((𝑧(Hom ‘𝐶)𝑤)(Iso‘𝑇)(((1st𝑌)‘𝑧)(𝑂 Nat 𝑆)((1st𝑌)‘𝑤))) ↔ (((1st𝑌)‘𝑤)𝑁𝑧):(𝑧(Hom ‘𝐶)𝑤)–1-1-onto→(((1st𝑌)‘𝑧)(𝑂 Nat 𝑆)((1st𝑌)‘𝑤))))
10983, 108mpbid 224 . . . . . 6 ((𝜑 ∧ (𝑧𝐵𝑤𝐵)) → (((1st𝑌)‘𝑤)𝑁𝑧):(𝑧(Hom ‘𝐶)𝑤)–1-1-onto→(((1st𝑌)‘𝑧)(𝑂 Nat 𝑆)((1st𝑌)‘𝑤)))
11074adantr 473 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑧𝐵𝑤𝐵)) ∧ ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝐶 ∈ Cat)
111110adantr 473 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑧𝐵𝑤𝐵)) ∧ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ 𝑦𝐵) → 𝐶 ∈ Cat)
11264adantr 473 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑧𝐵𝑤𝐵)) ∧ ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑧𝐵)
113112adantr 473 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑧𝐵𝑤𝐵)) ∧ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ 𝑦𝐵) → 𝑧𝐵)
114 simpr 477 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑧𝐵𝑤𝐵)) ∧ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ 𝑦𝐵) → 𝑦𝐵)
1152, 31, 111, 113, 75, 114yon11 17372 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑧𝐵𝑤𝐵)) ∧ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ 𝑦𝐵) → ((1st ‘((1st𝑌)‘𝑧))‘𝑦) = (𝑦(Hom ‘𝐶)𝑧))
116115eqcomd 2785 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑧𝐵𝑤𝐵)) ∧ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ 𝑦𝐵) → (𝑦(Hom ‘𝐶)𝑧) = ((1st ‘((1st𝑌)‘𝑧))‘𝑦))
117111adantr 473 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ (𝑧𝐵𝑤𝐵)) ∧ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ 𝑦𝐵) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) → 𝐶 ∈ Cat)
11862ad3antrrr 717 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ (𝑧𝐵𝑤𝐵)) ∧ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ 𝑦𝐵) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) → 𝑤𝐵)
119113adantr 473 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ (𝑧𝐵𝑤𝐵)) ∧ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ 𝑦𝐵) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) → 𝑧𝐵)
120 eqid 2779 . . . . . . . . . . . . . . 15 (comp‘𝐶) = (comp‘𝐶)
121114adantr 473 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ (𝑧𝐵𝑤𝐵)) ∧ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ 𝑦𝐵) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) → 𝑦𝐵)
122 simpr 477 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ (𝑧𝐵𝑤𝐵)) ∧ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ 𝑦𝐵) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) → 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))
123 simpllr 763 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ (𝑧𝐵𝑤𝐵)) ∧ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ 𝑦𝐵) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) → ∈ (𝑧(Hom ‘𝐶)𝑤))
1242, 31, 117, 118, 75, 119, 120, 121, 122, 123yon12 17373 . . . . . . . . . . . . . 14 (((((𝜑 ∧ (𝑧𝐵𝑤𝐵)) ∧ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ 𝑦𝐵) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) → (((𝑧(2nd ‘((1st𝑌)‘𝑤))𝑦)‘𝑔)‘) = ((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔))
1252, 31, 117, 119, 75, 118, 120, 121, 123, 122yon2 17374 . . . . . . . . . . . . . 14 (((((𝜑 ∧ (𝑧𝐵𝑤𝐵)) ∧ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ 𝑦𝐵) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) → ((((𝑧(2nd𝑌)𝑤)‘)‘𝑦)‘𝑔) = ((⟨𝑦, 𝑧⟩(comp‘𝐶)𝑤)𝑔))
126124, 125eqtr4d 2818 . . . . . . . . . . . . 13 (((((𝜑 ∧ (𝑧𝐵𝑤𝐵)) ∧ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ 𝑦𝐵) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) → (((𝑧(2nd ‘((1st𝑌)‘𝑤))𝑦)‘𝑔)‘) = ((((𝑧(2nd𝑌)𝑤)‘)‘𝑦)‘𝑔))
127116, 126mpteq12dva 5011 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑧𝐵𝑤𝐵)) ∧ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ 𝑦𝐵) → (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧) ↦ (((𝑧(2nd ‘((1st𝑌)‘𝑤))𝑦)‘𝑔)‘)) = (𝑔 ∈ ((1st ‘((1st𝑌)‘𝑧))‘𝑦) ↦ ((((𝑧(2nd𝑌)𝑤)‘)‘𝑦)‘𝑔)))
12816adantr 473 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑧𝐵𝑤𝐵)) → (1st𝑌)(𝐶 Func 𝑄)(2nd𝑌))
12931, 75, 98, 128, 64, 62funcf2 16996 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑧𝐵𝑤𝐵)) → (𝑧(2nd𝑌)𝑤):(𝑧(Hom ‘𝐶)𝑤)⟶(((1st𝑌)‘𝑧)(𝑂 Nat 𝑆)((1st𝑌)‘𝑤)))
130129ffvelrnda 6676 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑧𝐵𝑤𝐵)) ∧ ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑧(2nd𝑌)𝑤)‘) ∈ (((1st𝑌)‘𝑧)(𝑂 Nat 𝑆)((1st𝑌)‘𝑤)))
13197, 130nat1st2nd 17079 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑧𝐵𝑤𝐵)) ∧ ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑧(2nd𝑌)𝑤)‘) ∈ (⟨(1st ‘((1st𝑌)‘𝑧)), (2nd ‘((1st𝑌)‘𝑧))⟩(𝑂 Nat 𝑆)⟨(1st ‘((1st𝑌)‘𝑤)), (2nd ‘((1st𝑌)‘𝑤))⟩))
132131adantr 473 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑧𝐵𝑤𝐵)) ∧ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ 𝑦𝐵) → ((𝑧(2nd𝑌)𝑤)‘) ∈ (⟨(1st ‘((1st𝑌)‘𝑧)), (2nd ‘((1st𝑌)‘𝑧))⟩(𝑂 Nat 𝑆)⟨(1st ‘((1st𝑌)‘𝑤)), (2nd ‘((1st𝑌)‘𝑤))⟩))
133 eqid 2779 . . . . . . . . . . . . . . 15 (Hom ‘𝑆) = (Hom ‘𝑆)
13497, 132, 52, 133, 114natcl 17081 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑧𝐵𝑤𝐵)) ∧ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ 𝑦𝐵) → (((𝑧(2nd𝑌)𝑤)‘)‘𝑦) ∈ (((1st ‘((1st𝑌)‘𝑧))‘𝑦)(Hom ‘𝑆)((1st ‘((1st𝑌)‘𝑤))‘𝑦)))
13510adantr 473 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑧𝐵𝑤𝐵)) → 𝑈 ∈ V)
136135ad2antrr 713 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑧𝐵𝑤𝐵)) ∧ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ 𝑦𝐵) → 𝑈 ∈ V)
13760ad2antrr 713 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑧𝐵𝑤𝐵)) ∧ ∈ (𝑧(Hom ‘𝐶)𝑤)) → (1st𝑌):𝐵⟶(𝑂 Func 𝑆))
138137, 112ffvelrnd 6677 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑧𝐵𝑤𝐵)) ∧ ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((1st𝑌)‘𝑧) ∈ (𝑂 Func 𝑆))
139 1st2ndbr 7553 . . . . . . . . . . . . . . . . . . 19 ((Rel (𝑂 Func 𝑆) ∧ ((1st𝑌)‘𝑧) ∈ (𝑂 Func 𝑆)) → (1st ‘((1st𝑌)‘𝑧))(𝑂 Func 𝑆)(2nd ‘((1st𝑌)‘𝑧)))
14086, 138, 139sylancr 578 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑧𝐵𝑤𝐵)) ∧ ∈ (𝑧(Hom ‘𝐶)𝑤)) → (1st ‘((1st𝑌)‘𝑧))(𝑂 Func 𝑆)(2nd ‘((1st𝑌)‘𝑧)))
14152, 85, 140funcf1 16994 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑧𝐵𝑤𝐵)) ∧ ∈ (𝑧(Hom ‘𝐶)𝑤)) → (1st ‘((1st𝑌)‘𝑧)):𝐵⟶(Base‘𝑆))
142141ffvelrnda 6676 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑧𝐵𝑤𝐵)) ∧ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ 𝑦𝐵) → ((1st ‘((1st𝑌)‘𝑧))‘𝑦) ∈ (Base‘𝑆))
14392ad2antrr 713 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑧𝐵𝑤𝐵)) ∧ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ 𝑦𝐵) → 𝑈 = (Base‘𝑆))
144142, 143eleqtrrd 2870 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑧𝐵𝑤𝐵)) ∧ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ 𝑦𝐵) → ((1st ‘((1st𝑌)‘𝑧))‘𝑦) ∈ 𝑈)
14589adantr 473 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑧𝐵𝑤𝐵)) ∧ ∈ (𝑧(Hom ‘𝐶)𝑤)) → (1st ‘((1st𝑌)‘𝑤)):𝐵⟶(Base‘𝑆))
146145ffvelrnda 6676 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑧𝐵𝑤𝐵)) ∧ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ 𝑦𝐵) → ((1st ‘((1st𝑌)‘𝑤))‘𝑦) ∈ (Base‘𝑆))
147146, 143eleqtrrd 2870 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑧𝐵𝑤𝐵)) ∧ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ 𝑦𝐵) → ((1st ‘((1st𝑌)‘𝑤))‘𝑦) ∈ 𝑈)
1485, 136, 133, 144, 147elsetchom 17199 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑧𝐵𝑤𝐵)) ∧ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ 𝑦𝐵) → ((((𝑧(2nd𝑌)𝑤)‘)‘𝑦) ∈ (((1st ‘((1st𝑌)‘𝑧))‘𝑦)(Hom ‘𝑆)((1st ‘((1st𝑌)‘𝑤))‘𝑦)) ↔ (((𝑧(2nd𝑌)𝑤)‘)‘𝑦):((1st ‘((1st𝑌)‘𝑧))‘𝑦)⟶((1st ‘((1st𝑌)‘𝑤))‘𝑦)))
149134, 148mpbid 224 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑧𝐵𝑤𝐵)) ∧ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ 𝑦𝐵) → (((𝑧(2nd𝑌)𝑤)‘)‘𝑦):((1st ‘((1st𝑌)‘𝑧))‘𝑦)⟶((1st ‘((1st𝑌)‘𝑤))‘𝑦))
150149feqmptd 6562 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑧𝐵𝑤𝐵)) ∧ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ 𝑦𝐵) → (((𝑧(2nd𝑌)𝑤)‘)‘𝑦) = (𝑔 ∈ ((1st ‘((1st𝑌)‘𝑧))‘𝑦) ↦ ((((𝑧(2nd𝑌)𝑤)‘)‘𝑦)‘𝑔)))
151127, 150eqtr4d 2818 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑧𝐵𝑤𝐵)) ∧ ∈ (𝑧(Hom ‘𝐶)𝑤)) ∧ 𝑦𝐵) → (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧) ↦ (((𝑧(2nd ‘((1st𝑌)‘𝑤))𝑦)‘𝑔)‘)) = (((𝑧(2nd𝑌)𝑤)‘)‘𝑦))
152151mpteq2dva 5022 . . . . . . . . . 10 (((𝜑 ∧ (𝑧𝐵𝑤𝐵)) ∧ ∈ (𝑧(Hom ‘𝐶)𝑤)) → (𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧) ↦ (((𝑧(2nd ‘((1st𝑌)‘𝑤))𝑦)‘𝑔)‘))) = (𝑦𝐵 ↦ (((𝑧(2nd𝑌)𝑤)‘)‘𝑦)))
15378adantr 473 . . . . . . . . . . 11 (((𝜑 ∧ (𝑧𝐵𝑤𝐵)) ∧ ∈ (𝑧(Hom ‘𝐶)𝑤)) → 𝑉𝑊)
15479adantr 473 . . . . . . . . . . 11 (((𝜑 ∧ (𝑧𝐵𝑤𝐵)) ∧ ∈ (𝑧(Hom ‘𝐶)𝑤)) → ran (Homf𝐶) ⊆ 𝑈)
15580adantr 473 . . . . . . . . . . 11 (((𝜑 ∧ (𝑧𝐵𝑤𝐵)) ∧ ∈ (𝑧(Hom ‘𝐶)𝑤)) → (ran (Homf𝑄) ∪ 𝑈) ⊆ 𝑉)
15663adantr 473 . . . . . . . . . . 11 (((𝜑 ∧ (𝑧𝐵𝑤𝐵)) ∧ ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((1st𝑌)‘𝑤) ∈ (𝑂 Func 𝑆))
15776eleq2d 2852 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑧𝐵𝑤𝐵)) → ( ∈ ((1st ‘((1st𝑌)‘𝑤))‘𝑧) ↔ ∈ (𝑧(Hom ‘𝐶)𝑤)))
158157biimpar 470 . . . . . . . . . . 11 (((𝜑 ∧ (𝑧𝐵𝑤𝐵)) ∧ ∈ (𝑧(Hom ‘𝐶)𝑤)) → ∈ ((1st ‘((1st𝑌)‘𝑤))‘𝑧))
1592, 31, 32, 4, 5, 33, 6, 34, 28, 35, 36, 110, 153, 154, 155, 156, 112, 47, 158yonedalem4a 17383 . . . . . . . . . 10 (((𝜑 ∧ (𝑧𝐵𝑤𝐵)) ∧ ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((((1st𝑌)‘𝑤)𝑁𝑧)‘) = (𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧) ↦ (((𝑧(2nd ‘((1st𝑌)‘𝑤))𝑦)‘𝑔)‘))))
16097, 131, 52natfn 17082 . . . . . . . . . . 11 (((𝜑 ∧ (𝑧𝐵𝑤𝐵)) ∧ ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑧(2nd𝑌)𝑤)‘) Fn 𝐵)
161 dffn5 6554 . . . . . . . . . . 11 (((𝑧(2nd𝑌)𝑤)‘) Fn 𝐵 ↔ ((𝑧(2nd𝑌)𝑤)‘) = (𝑦𝐵 ↦ (((𝑧(2nd𝑌)𝑤)‘)‘𝑦)))
162160, 161sylib 210 . . . . . . . . . 10 (((𝜑 ∧ (𝑧𝐵𝑤𝐵)) ∧ ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((𝑧(2nd𝑌)𝑤)‘) = (𝑦𝐵 ↦ (((𝑧(2nd𝑌)𝑤)‘)‘𝑦)))
163152, 159, 1623eqtr4d 2825 . . . . . . . . 9 (((𝜑 ∧ (𝑧𝐵𝑤𝐵)) ∧ ∈ (𝑧(Hom ‘𝐶)𝑤)) → ((((1st𝑌)‘𝑤)𝑁𝑧)‘) = ((𝑧(2nd𝑌)𝑤)‘))
164163mpteq2dva 5022 . . . . . . . 8 ((𝜑 ∧ (𝑧𝐵𝑤𝐵)) → ( ∈ (𝑧(Hom ‘𝐶)𝑤) ↦ ((((1st𝑌)‘𝑤)𝑁𝑧)‘)) = ( ∈ (𝑧(Hom ‘𝐶)𝑤) ↦ ((𝑧(2nd𝑌)𝑤)‘)))
165 f1of 6444 . . . . . . . . . 10 ((((1st𝑌)‘𝑤)𝑁𝑧):(𝑧(Hom ‘𝐶)𝑤)–1-1-onto→(((1st𝑌)‘𝑧)(𝑂 Nat 𝑆)((1st𝑌)‘𝑤)) → (((1st𝑌)‘𝑤)𝑁𝑧):(𝑧(Hom ‘𝐶)𝑤)⟶(((1st𝑌)‘𝑧)(𝑂 Nat 𝑆)((1st𝑌)‘𝑤)))
166109, 165syl 17 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝐵𝑤𝐵)) → (((1st𝑌)‘𝑤)𝑁𝑧):(𝑧(Hom ‘𝐶)𝑤)⟶(((1st𝑌)‘𝑧)(𝑂 Nat 𝑆)((1st𝑌)‘𝑤)))
167166feqmptd 6562 . . . . . . . 8 ((𝜑 ∧ (𝑧𝐵𝑤𝐵)) → (((1st𝑌)‘𝑤)𝑁𝑧) = ( ∈ (𝑧(Hom ‘𝐶)𝑤) ↦ ((((1st𝑌)‘𝑤)𝑁𝑧)‘)))
168129feqmptd 6562 . . . . . . . 8 ((𝜑 ∧ (𝑧𝐵𝑤𝐵)) → (𝑧(2nd𝑌)𝑤) = ( ∈ (𝑧(Hom ‘𝐶)𝑤) ↦ ((𝑧(2nd𝑌)𝑤)‘)))
169164, 167, 1683eqtr4d 2825 . . . . . . 7 ((𝜑 ∧ (𝑧𝐵𝑤𝐵)) → (((1st𝑌)‘𝑤)𝑁𝑧) = (𝑧(2nd𝑌)𝑤))
170 f1oeq1 6433 . . . . . . 7 ((((1st𝑌)‘𝑤)𝑁𝑧) = (𝑧(2nd𝑌)𝑤) → ((((1st𝑌)‘𝑤)𝑁𝑧):(𝑧(Hom ‘𝐶)𝑤)–1-1-onto→(((1st𝑌)‘𝑧)(𝑂 Nat 𝑆)((1st𝑌)‘𝑤)) ↔ (𝑧(2nd𝑌)𝑤):(𝑧(Hom ‘𝐶)𝑤)–1-1-onto→(((1st𝑌)‘𝑧)(𝑂 Nat 𝑆)((1st𝑌)‘𝑤))))
171169, 170syl 17 . . . . . 6 ((𝜑 ∧ (𝑧𝐵𝑤𝐵)) → ((((1st𝑌)‘𝑤)𝑁𝑧):(𝑧(Hom ‘𝐶)𝑤)–1-1-onto→(((1st𝑌)‘𝑧)(𝑂 Nat 𝑆)((1st𝑌)‘𝑤)) ↔ (𝑧(2nd𝑌)𝑤):(𝑧(Hom ‘𝐶)𝑤)–1-1-onto→(((1st𝑌)‘𝑧)(𝑂 Nat 𝑆)((1st𝑌)‘𝑤))))
172109, 171mpbid 224 . . . . 5 ((𝜑 ∧ (𝑧𝐵𝑤𝐵)) → (𝑧(2nd𝑌)𝑤):(𝑧(Hom ‘𝐶)𝑤)–1-1-onto→(((1st𝑌)‘𝑧)(𝑂 Nat 𝑆)((1st𝑌)‘𝑤)))
173172ralrimivva 3142 . . . 4 (𝜑 → ∀𝑧𝐵𝑤𝐵 (𝑧(2nd𝑌)𝑤):(𝑧(Hom ‘𝐶)𝑤)–1-1-onto→(((1st𝑌)‘𝑧)(𝑂 Nat 𝑆)((1st𝑌)‘𝑤)))
17431, 75, 98isffth2 17044 . . . 4 ((1st𝑌)((𝐶 Full 𝑄) ∩ (𝐶 Faith 𝑄))(2nd𝑌) ↔ ((1st𝑌)(𝐶 Func 𝑄)(2nd𝑌) ∧ ∀𝑧𝐵𝑤𝐵 (𝑧(2nd𝑌)𝑤):(𝑧(Hom ‘𝐶)𝑤)–1-1-onto→(((1st𝑌)‘𝑧)(𝑂 Nat 𝑆)((1st𝑌)‘𝑤))))
17516, 173, 174sylanbrc 575 . . 3 (𝜑 → (1st𝑌)((𝐶 Full 𝑄) ∩ (𝐶 Faith 𝑄))(2nd𝑌))
176 df-br 4930 . . 3 ((1st𝑌)((𝐶 Full 𝑄) ∩ (𝐶 Faith 𝑄))(2nd𝑌) ↔ ⟨(1st𝑌), (2nd𝑌)⟩ ∈ ((𝐶 Full 𝑄) ∩ (𝐶 Faith 𝑄)))
177175, 176sylib 210 . 2 (𝜑 → ⟨(1st𝑌), (2nd𝑌)⟩ ∈ ((𝐶 Full 𝑄) ∩ (𝐶 Faith 𝑄)))
17814, 177eqeltrd 2867 1 (𝜑𝑌 ∈ ((𝐶 Full 𝑄) ∩ (𝐶 Faith 𝑄)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 387   = wceq 1507  wcel 2050  wral 3089  Vcvv 3416  cun 3828  cin 3829  wss 3830  cop 4447   class class class wbr 4929  cmpt 5008   × cxp 5405  ran crn 5408  Rel wrel 5412   Fn wfn 6183  wf 6184  1-1-ontowf1o 6187  cfv 6188  (class class class)co 6976  cmpo 6978  1st c1st 7499  2nd c2nd 7500  tpos ctpos 7694  Basecbs 16339  Hom chom 16432  compcco 16433  Catccat 16793  Idccid 16794  Homf chomf 16795  oppCatcoppc 16839  Invcinv 16873  Isociso 16874   Func cfunc 16982  func ccofu 16984   Full cful 17030   Faith cfth 17031   Nat cnat 17069   FuncCat cfuc 17070  SetCatcsetc 17193   ×c cxpc 17276   1stF c1stf 17277   2ndF c2ndf 17278   ⟨,⟩F cprf 17279   evalF cevlf 17317  HomFchof 17356  Yoncyon 17357
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2751  ax-rep 5049  ax-sep 5060  ax-nul 5067  ax-pow 5119  ax-pr 5186  ax-un 7279  ax-cnex 10391  ax-resscn 10392  ax-1cn 10393  ax-icn 10394  ax-addcl 10395  ax-addrcl 10396  ax-mulcl 10397  ax-mulrcl 10398  ax-mulcom 10399  ax-addass 10400  ax-mulass 10401  ax-distr 10402  ax-i2m1 10403  ax-1ne0 10404  ax-1rid 10405  ax-rnegex 10406  ax-rrecex 10407  ax-cnre 10408  ax-pre-lttri 10409  ax-pre-lttrn 10410  ax-pre-ltadd 10411  ax-pre-mulgt0 10412
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3or 1069  df-3an 1070  df-tru 1510  df-fal 1520  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2584  df-clab 2760  df-cleq 2772  df-clel 2847  df-nfc 2919  df-ne 2969  df-nel 3075  df-ral 3094  df-rex 3095  df-reu 3096  df-rmo 3097  df-rab 3098  df-v 3418  df-sbc 3683  df-csb 3788  df-dif 3833  df-un 3835  df-in 3837  df-ss 3844  df-pss 3846  df-nul 4180  df-if 4351  df-pw 4424  df-sn 4442  df-pr 4444  df-tp 4446  df-op 4448  df-uni 4713  df-int 4750  df-iun 4794  df-br 4930  df-opab 4992  df-mpt 5009  df-tr 5031  df-id 5312  df-eprel 5317  df-po 5326  df-so 5327  df-fr 5366  df-we 5368  df-xp 5413  df-rel 5414  df-cnv 5415  df-co 5416  df-dm 5417  df-rn 5418  df-res 5419  df-ima 5420  df-pred 5986  df-ord 6032  df-on 6033  df-lim 6034  df-suc 6035  df-iota 6152  df-fun 6190  df-fn 6191  df-f 6192  df-f1 6193  df-fo 6194  df-f1o 6195  df-fv 6196  df-riota 6937  df-ov 6979  df-oprab 6980  df-mpo 6981  df-om 7397  df-1st 7501  df-2nd 7502  df-tpos 7695  df-wrecs 7750  df-recs 7812  df-rdg 7850  df-1o 7905  df-oadd 7909  df-er 8089  df-map 8208  df-pm 8209  df-ixp 8260  df-en 8307  df-dom 8308  df-sdom 8309  df-fin 8310  df-pnf 10476  df-mnf 10477  df-xr 10478  df-ltxr 10479  df-le 10480  df-sub 10672  df-neg 10673  df-nn 11440  df-2 11503  df-3 11504  df-4 11505  df-5 11506  df-6 11507  df-7 11508  df-8 11509  df-9 11510  df-n0 11708  df-z 11794  df-dec 11912  df-uz 12059  df-fz 12709  df-struct 16341  df-ndx 16342  df-slot 16343  df-base 16345  df-sets 16346  df-ress 16347  df-hom 16445  df-cco 16446  df-cat 16797  df-cid 16798  df-homf 16799  df-comf 16800  df-oppc 16840  df-sect 16875  df-inv 16876  df-iso 16877  df-ssc 16938  df-resc 16939  df-subc 16940  df-func 16986  df-cofu 16988  df-full 17032  df-fth 17033  df-nat 17071  df-fuc 17072  df-setc 17194  df-xpc 17280  df-1stf 17281  df-2ndf 17282  df-prf 17283  df-evlf 17321  df-curf 17322  df-hof 17358  df-yon 17359
This theorem is referenced by:  yonffth  17392
  Copyright terms: Public domain W3C validator