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

Theorem yonedalem4c 18054
Description: Lemma for yoneda 18060. (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𝑄) ∪ 𝑈) ⊆ 𝑉)
yonedalem21.f (𝜑𝐹 ∈ (𝑂 Func 𝑆))
yonedalem21.x (𝜑𝑋𝐵)
yonedalem4.n 𝑁 = (𝑓 ∈ (𝑂 Func 𝑆), 𝑥𝐵 ↦ (𝑢 ∈ ((1st𝑓)‘𝑥) ↦ (𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥) ↦ (((𝑥(2nd𝑓)𝑦)‘𝑔)‘𝑢)))))
yonedalem4.p (𝜑𝐴 ∈ ((1st𝐹)‘𝑋))
Assertion
Ref Expression
yonedalem4c (𝜑 → ((𝐹𝑁𝑋)‘𝐴) ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹))
Distinct variable groups:   𝑓,𝑔,𝑥,𝑦, 1   𝑢,𝑔,𝐴,𝑦   𝑢,𝑓,𝐶,𝑔,𝑥,𝑦   𝑓,𝐸,𝑔,𝑢,𝑦   𝑓,𝐹,𝑔,𝑢,𝑥,𝑦   𝐵,𝑓,𝑔,𝑢,𝑥,𝑦   𝑓,𝑂,𝑔,𝑢,𝑥,𝑦   𝑆,𝑓,𝑔,𝑢,𝑥,𝑦   𝑄,𝑓,𝑔,𝑢,𝑥   𝑇,𝑓,𝑔,𝑢,𝑦   𝜑,𝑓,𝑔,𝑢,𝑥,𝑦   𝑢,𝑅   𝑓,𝑌,𝑔,𝑢,𝑥,𝑦   𝑓,𝑍,𝑔,𝑢,𝑥,𝑦   𝑓,𝑋,𝑔,𝑢,𝑥,𝑦
Allowed substitution hints:   𝐴(𝑥,𝑓)   𝑄(𝑦)   𝑅(𝑥,𝑦,𝑓,𝑔)   𝑇(𝑥)   𝑈(𝑥,𝑦,𝑢,𝑓,𝑔)   1 (𝑢)   𝐸(𝑥)   𝐻(𝑥,𝑦,𝑢,𝑓,𝑔)   𝑁(𝑥,𝑦,𝑢,𝑓,𝑔)   𝑉(𝑥,𝑦,𝑢,𝑓,𝑔)   𝑊(𝑥,𝑦,𝑢,𝑓,𝑔)

Proof of Theorem yonedalem4c
Dummy variables 𝑘 𝑤 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 yoneda.y . . . . 5 𝑌 = (Yon‘𝐶)
2 yoneda.b . . . . 5 𝐵 = (Base‘𝐶)
3 yoneda.1 . . . . 5 1 = (Id‘𝐶)
4 yoneda.o . . . . 5 𝑂 = (oppCat‘𝐶)
5 yoneda.s . . . . 5 𝑆 = (SetCat‘𝑈)
6 yoneda.t . . . . 5 𝑇 = (SetCat‘𝑉)
7 yoneda.q . . . . 5 𝑄 = (𝑂 FuncCat 𝑆)
8 yoneda.h . . . . 5 𝐻 = (HomF𝑄)
9 yoneda.r . . . . 5 𝑅 = ((𝑄 ×c 𝑂) FuncCat 𝑇)
10 yoneda.e . . . . 5 𝐸 = (𝑂 evalF 𝑆)
11 yoneda.z . . . . 5 𝑍 = (𝐻func ((⟨(1st𝑌), tpos (2nd𝑌)⟩ ∘func (𝑄 2ndF 𝑂)) ⟨,⟩F (𝑄 1stF 𝑂)))
12 yoneda.c . . . . 5 (𝜑𝐶 ∈ Cat)
13 yoneda.w . . . . 5 (𝜑𝑉𝑊)
14 yoneda.u . . . . 5 (𝜑 → ran (Homf𝐶) ⊆ 𝑈)
15 yoneda.v . . . . 5 (𝜑 → (ran (Homf𝑄) ∪ 𝑈) ⊆ 𝑉)
16 yonedalem21.f . . . . 5 (𝜑𝐹 ∈ (𝑂 Func 𝑆))
17 yonedalem21.x . . . . 5 (𝜑𝑋𝐵)
18 yonedalem4.n . . . . 5 𝑁 = (𝑓 ∈ (𝑂 Func 𝑆), 𝑥𝐵 ↦ (𝑢 ∈ ((1st𝑓)‘𝑥) ↦ (𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥) ↦ (((𝑥(2nd𝑓)𝑦)‘𝑔)‘𝑢)))))
19 yonedalem4.p . . . . 5 (𝜑𝐴 ∈ ((1st𝐹)‘𝑋))
201, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19yonedalem4a 18052 . . . 4 (𝜑 → ((𝐹𝑁𝑋)‘𝐴) = (𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd𝐹)𝑦)‘𝑔)‘𝐴))))
21 oveq1 7315 . . . . . 6 (𝑦 = 𝑧 → (𝑦(Hom ‘𝐶)𝑋) = (𝑧(Hom ‘𝐶)𝑋))
22 oveq2 7316 . . . . . . . 8 (𝑦 = 𝑧 → (𝑋(2nd𝐹)𝑦) = (𝑋(2nd𝐹)𝑧))
2322fveq1d 6806 . . . . . . 7 (𝑦 = 𝑧 → ((𝑋(2nd𝐹)𝑦)‘𝑔) = ((𝑋(2nd𝐹)𝑧)‘𝑔))
2423fveq1d 6806 . . . . . 6 (𝑦 = 𝑧 → (((𝑋(2nd𝐹)𝑦)‘𝑔)‘𝐴) = (((𝑋(2nd𝐹)𝑧)‘𝑔)‘𝐴))
2521, 24mpteq12dv 5171 . . . . 5 (𝑦 = 𝑧 → (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd𝐹)𝑦)‘𝑔)‘𝐴)) = (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd𝐹)𝑧)‘𝑔)‘𝐴)))
2625cbvmptv 5193 . . . 4 (𝑦𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd𝐹)𝑦)‘𝑔)‘𝐴))) = (𝑧𝐵 ↦ (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd𝐹)𝑧)‘𝑔)‘𝐴)))
2720, 26eqtrdi 2791 . . 3 (𝜑 → ((𝐹𝑁𝑋)‘𝐴) = (𝑧𝐵 ↦ (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd𝐹)𝑧)‘𝑔)‘𝐴))))
284, 2oppcbas 17487 . . . . . . . . . . . . 13 𝐵 = (Base‘𝑂)
29 eqid 2735 . . . . . . . . . . . . 13 (Hom ‘𝑂) = (Hom ‘𝑂)
30 eqid 2735 . . . . . . . . . . . . 13 (Hom ‘𝑆) = (Hom ‘𝑆)
31 relfunc 17636 . . . . . . . . . . . . . . 15 Rel (𝑂 Func 𝑆)
32 1st2ndbr 7919 . . . . . . . . . . . . . . 15 ((Rel (𝑂 Func 𝑆) ∧ 𝐹 ∈ (𝑂 Func 𝑆)) → (1st𝐹)(𝑂 Func 𝑆)(2nd𝐹))
3331, 16, 32sylancr 587 . . . . . . . . . . . . . 14 (𝜑 → (1st𝐹)(𝑂 Func 𝑆)(2nd𝐹))
3433adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑧𝐵) → (1st𝐹)(𝑂 Func 𝑆)(2nd𝐹))
3517adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑧𝐵) → 𝑋𝐵)
36 simpr 485 . . . . . . . . . . . . 13 ((𝜑𝑧𝐵) → 𝑧𝐵)
3728, 29, 30, 34, 35, 36funcf2 17642 . . . . . . . . . . . 12 ((𝜑𝑧𝐵) → (𝑋(2nd𝐹)𝑧):(𝑋(Hom ‘𝑂)𝑧)⟶(((1st𝐹)‘𝑋)(Hom ‘𝑆)((1st𝐹)‘𝑧)))
3837adantr 481 . . . . . . . . . . 11 (((𝜑𝑧𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋)) → (𝑋(2nd𝐹)𝑧):(𝑋(Hom ‘𝑂)𝑧)⟶(((1st𝐹)‘𝑋)(Hom ‘𝑆)((1st𝐹)‘𝑧)))
39 simpr 485 . . . . . . . . . . . 12 (((𝜑𝑧𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋)) → 𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋))
40 eqid 2735 . . . . . . . . . . . . 13 (Hom ‘𝐶) = (Hom ‘𝐶)
4140, 4oppchom 17484 . . . . . . . . . . . 12 (𝑋(Hom ‘𝑂)𝑧) = (𝑧(Hom ‘𝐶)𝑋)
4239, 41eleqtrrdi 2847 . . . . . . . . . . 11 (((𝜑𝑧𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋)) → 𝑔 ∈ (𝑋(Hom ‘𝑂)𝑧))
4338, 42ffvelcdmd 6994 . . . . . . . . . 10 (((𝜑𝑧𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋)) → ((𝑋(2nd𝐹)𝑧)‘𝑔) ∈ (((1st𝐹)‘𝑋)(Hom ‘𝑆)((1st𝐹)‘𝑧)))
4415unssbd 4127 . . . . . . . . . . . . . 14 (𝜑𝑈𝑉)
4513, 44ssexd 5256 . . . . . . . . . . . . 13 (𝜑𝑈 ∈ V)
4645adantr 481 . . . . . . . . . . . 12 ((𝜑𝑧𝐵) → 𝑈 ∈ V)
4746adantr 481 . . . . . . . . . . 11 (((𝜑𝑧𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋)) → 𝑈 ∈ V)
48 eqid 2735 . . . . . . . . . . . . . . 15 (Base‘𝑆) = (Base‘𝑆)
4928, 48, 33funcf1 17640 . . . . . . . . . . . . . 14 (𝜑 → (1st𝐹):𝐵⟶(Base‘𝑆))
505, 45setcbas 17852 . . . . . . . . . . . . . . 15 (𝜑𝑈 = (Base‘𝑆))
5150feq3d 6617 . . . . . . . . . . . . . 14 (𝜑 → ((1st𝐹):𝐵𝑈 ↔ (1st𝐹):𝐵⟶(Base‘𝑆)))
5249, 51mpbird 256 . . . . . . . . . . . . 13 (𝜑 → (1st𝐹):𝐵𝑈)
5352, 17ffvelcdmd 6994 . . . . . . . . . . . 12 (𝜑 → ((1st𝐹)‘𝑋) ∈ 𝑈)
5453ad2antrr 723 . . . . . . . . . . 11 (((𝜑𝑧𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋)) → ((1st𝐹)‘𝑋) ∈ 𝑈)
5552ffvelcdmda 6993 . . . . . . . . . . . 12 ((𝜑𝑧𝐵) → ((1st𝐹)‘𝑧) ∈ 𝑈)
5655adantr 481 . . . . . . . . . . 11 (((𝜑𝑧𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋)) → ((1st𝐹)‘𝑧) ∈ 𝑈)
575, 47, 30, 54, 56elsetchom 17855 . . . . . . . . . 10 (((𝜑𝑧𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋)) → (((𝑋(2nd𝐹)𝑧)‘𝑔) ∈ (((1st𝐹)‘𝑋)(Hom ‘𝑆)((1st𝐹)‘𝑧)) ↔ ((𝑋(2nd𝐹)𝑧)‘𝑔):((1st𝐹)‘𝑋)⟶((1st𝐹)‘𝑧)))
5843, 57mpbid 231 . . . . . . . . 9 (((𝜑𝑧𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋)) → ((𝑋(2nd𝐹)𝑧)‘𝑔):((1st𝐹)‘𝑋)⟶((1st𝐹)‘𝑧))
5919ad2antrr 723 . . . . . . . . 9 (((𝜑𝑧𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋)) → 𝐴 ∈ ((1st𝐹)‘𝑋))
6058, 59ffvelcdmd 6994 . . . . . . . 8 (((𝜑𝑧𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋)) → (((𝑋(2nd𝐹)𝑧)‘𝑔)‘𝐴) ∈ ((1st𝐹)‘𝑧))
6160fmpttd 7021 . . . . . . 7 ((𝜑𝑧𝐵) → (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd𝐹)𝑧)‘𝑔)‘𝐴)):(𝑧(Hom ‘𝐶)𝑋)⟶((1st𝐹)‘𝑧))
6212adantr 481 . . . . . . . . 9 ((𝜑𝑧𝐵) → 𝐶 ∈ Cat)
631, 2, 62, 35, 40, 36yon11 18041 . . . . . . . 8 ((𝜑𝑧𝐵) → ((1st ‘((1st𝑌)‘𝑋))‘𝑧) = (𝑧(Hom ‘𝐶)𝑋))
6463feq2d 6616 . . . . . . 7 ((𝜑𝑧𝐵) → ((𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd𝐹)𝑧)‘𝑔)‘𝐴)):((1st ‘((1st𝑌)‘𝑋))‘𝑧)⟶((1st𝐹)‘𝑧) ↔ (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd𝐹)𝑧)‘𝑔)‘𝐴)):(𝑧(Hom ‘𝐶)𝑋)⟶((1st𝐹)‘𝑧)))
6561, 64mpbird 256 . . . . . 6 ((𝜑𝑧𝐵) → (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd𝐹)𝑧)‘𝑔)‘𝐴)):((1st ‘((1st𝑌)‘𝑋))‘𝑧)⟶((1st𝐹)‘𝑧))
661, 2, 12, 17, 4, 5, 45, 14yon1cl 18040 . . . . . . . . . . 11 (𝜑 → ((1st𝑌)‘𝑋) ∈ (𝑂 Func 𝑆))
67 1st2ndbr 7919 . . . . . . . . . . 11 ((Rel (𝑂 Func 𝑆) ∧ ((1st𝑌)‘𝑋) ∈ (𝑂 Func 𝑆)) → (1st ‘((1st𝑌)‘𝑋))(𝑂 Func 𝑆)(2nd ‘((1st𝑌)‘𝑋)))
6831, 66, 67sylancr 587 . . . . . . . . . 10 (𝜑 → (1st ‘((1st𝑌)‘𝑋))(𝑂 Func 𝑆)(2nd ‘((1st𝑌)‘𝑋)))
6928, 48, 68funcf1 17640 . . . . . . . . 9 (𝜑 → (1st ‘((1st𝑌)‘𝑋)):𝐵⟶(Base‘𝑆))
7050feq3d 6617 . . . . . . . . 9 (𝜑 → ((1st ‘((1st𝑌)‘𝑋)):𝐵𝑈 ↔ (1st ‘((1st𝑌)‘𝑋)):𝐵⟶(Base‘𝑆)))
7169, 70mpbird 256 . . . . . . . 8 (𝜑 → (1st ‘((1st𝑌)‘𝑋)):𝐵𝑈)
7271ffvelcdmda 6993 . . . . . . 7 ((𝜑𝑧𝐵) → ((1st ‘((1st𝑌)‘𝑋))‘𝑧) ∈ 𝑈)
735, 46, 30, 72, 55elsetchom 17855 . . . . . 6 ((𝜑𝑧𝐵) → ((𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd𝐹)𝑧)‘𝑔)‘𝐴)) ∈ (((1st ‘((1st𝑌)‘𝑋))‘𝑧)(Hom ‘𝑆)((1st𝐹)‘𝑧)) ↔ (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd𝐹)𝑧)‘𝑔)‘𝐴)):((1st ‘((1st𝑌)‘𝑋))‘𝑧)⟶((1st𝐹)‘𝑧)))
7465, 73mpbird 256 . . . . 5 ((𝜑𝑧𝐵) → (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd𝐹)𝑧)‘𝑔)‘𝐴)) ∈ (((1st ‘((1st𝑌)‘𝑋))‘𝑧)(Hom ‘𝑆)((1st𝐹)‘𝑧)))
7574ralrimiva 3138 . . . 4 (𝜑 → ∀𝑧𝐵 (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd𝐹)𝑧)‘𝑔)‘𝐴)) ∈ (((1st ‘((1st𝑌)‘𝑋))‘𝑧)(Hom ‘𝑆)((1st𝐹)‘𝑧)))
762fvexi 6818 . . . . 5 𝐵 ∈ V
77 mptelixpg 8759 . . . . 5 (𝐵 ∈ V → ((𝑧𝐵 ↦ (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd𝐹)𝑧)‘𝑔)‘𝐴))) ∈ X𝑧𝐵 (((1st ‘((1st𝑌)‘𝑋))‘𝑧)(Hom ‘𝑆)((1st𝐹)‘𝑧)) ↔ ∀𝑧𝐵 (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd𝐹)𝑧)‘𝑔)‘𝐴)) ∈ (((1st ‘((1st𝑌)‘𝑋))‘𝑧)(Hom ‘𝑆)((1st𝐹)‘𝑧))))
7876, 77ax-mp 5 . . . 4 ((𝑧𝐵 ↦ (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd𝐹)𝑧)‘𝑔)‘𝐴))) ∈ X𝑧𝐵 (((1st ‘((1st𝑌)‘𝑋))‘𝑧)(Hom ‘𝑆)((1st𝐹)‘𝑧)) ↔ ∀𝑧𝐵 (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd𝐹)𝑧)‘𝑔)‘𝐴)) ∈ (((1st ‘((1st𝑌)‘𝑋))‘𝑧)(Hom ‘𝑆)((1st𝐹)‘𝑧)))
7975, 78sylibr 233 . . 3 (𝜑 → (𝑧𝐵 ↦ (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd𝐹)𝑧)‘𝑔)‘𝐴))) ∈ X𝑧𝐵 (((1st ‘((1st𝑌)‘𝑋))‘𝑧)(Hom ‘𝑆)((1st𝐹)‘𝑧)))
8027, 79eqeltrd 2836 . 2 (𝜑 → ((𝐹𝑁𝑋)‘𝐴) ∈ X𝑧𝐵 (((1st ‘((1st𝑌)‘𝑋))‘𝑧)(Hom ‘𝑆)((1st𝐹)‘𝑧)))
8112adantr 481 . . . . . . . . . 10 ((𝜑 ∧ (𝑧𝐵𝑤𝐵 ∈ (𝑧(Hom ‘𝑂)𝑤))) → 𝐶 ∈ Cat)
8217adantr 481 . . . . . . . . . 10 ((𝜑 ∧ (𝑧𝐵𝑤𝐵 ∈ (𝑧(Hom ‘𝑂)𝑤))) → 𝑋𝐵)
83 simpr1 1193 . . . . . . . . . 10 ((𝜑 ∧ (𝑧𝐵𝑤𝐵 ∈ (𝑧(Hom ‘𝑂)𝑤))) → 𝑧𝐵)
841, 2, 81, 82, 40, 83yon11 18041 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝐵𝑤𝐵 ∈ (𝑧(Hom ‘𝑂)𝑤))) → ((1st ‘((1st𝑌)‘𝑋))‘𝑧) = (𝑧(Hom ‘𝐶)𝑋))
8584eleq2d 2821 . . . . . . . 8 ((𝜑 ∧ (𝑧𝐵𝑤𝐵 ∈ (𝑧(Hom ‘𝑂)𝑤))) → (𝑘 ∈ ((1st ‘((1st𝑌)‘𝑋))‘𝑧) ↔ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)))
8685biimpa 477 . . . . . . 7 (((𝜑 ∧ (𝑧𝐵𝑤𝐵 ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ ((1st ‘((1st𝑌)‘𝑋))‘𝑧)) → 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋))
87 eqid 2735 . . . . . . . . . . . 12 (comp‘𝑂) = (comp‘𝑂)
88 eqid 2735 . . . . . . . . . . . 12 (comp‘𝑆) = (comp‘𝑆)
8933adantr 481 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑧𝐵𝑤𝐵 ∈ (𝑧(Hom ‘𝑂)𝑤))) → (1st𝐹)(𝑂 Func 𝑆)(2nd𝐹))
9089adantr 481 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑧𝐵𝑤𝐵 ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → (1st𝐹)(𝑂 Func 𝑆)(2nd𝐹))
9182adantr 481 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑧𝐵𝑤𝐵 ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → 𝑋𝐵)
9283adantr 481 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑧𝐵𝑤𝐵 ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → 𝑧𝐵)
93 simpr2 1194 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑧𝐵𝑤𝐵 ∈ (𝑧(Hom ‘𝑂)𝑤))) → 𝑤𝐵)
9493adantr 481 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑧𝐵𝑤𝐵 ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → 𝑤𝐵)
95 simpr 485 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑧𝐵𝑤𝐵 ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋))
9695, 41eleqtrrdi 2847 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑧𝐵𝑤𝐵 ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → 𝑘 ∈ (𝑋(Hom ‘𝑂)𝑧))
97 simplr3 1216 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑧𝐵𝑤𝐵 ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → ∈ (𝑧(Hom ‘𝑂)𝑤))
9828, 29, 87, 88, 90, 91, 92, 94, 96, 97funcco 17645 . . . . . . . . . . 11 (((𝜑 ∧ (𝑧𝐵𝑤𝐵 ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → ((𝑋(2nd𝐹)𝑤)‘((⟨𝑋, 𝑧⟩(comp‘𝑂)𝑤)𝑘)) = (((𝑧(2nd𝐹)𝑤)‘)(⟨((1st𝐹)‘𝑋), ((1st𝐹)‘𝑧)⟩(comp‘𝑆)((1st𝐹)‘𝑤))((𝑋(2nd𝐹)𝑧)‘𝑘)))
99 eqid 2735 . . . . . . . . . . . . 13 (comp‘𝐶) = (comp‘𝐶)
1002, 99, 4, 91, 92, 94oppcco 17486 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑧𝐵𝑤𝐵 ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → ((⟨𝑋, 𝑧⟩(comp‘𝑂)𝑤)𝑘) = (𝑘(⟨𝑤, 𝑧⟩(comp‘𝐶)𝑋)))
101100fveq2d 6808 . . . . . . . . . . 11 (((𝜑 ∧ (𝑧𝐵𝑤𝐵 ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → ((𝑋(2nd𝐹)𝑤)‘((⟨𝑋, 𝑧⟩(comp‘𝑂)𝑤)𝑘)) = ((𝑋(2nd𝐹)𝑤)‘(𝑘(⟨𝑤, 𝑧⟩(comp‘𝐶)𝑋))))
10245adantr 481 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑧𝐵𝑤𝐵 ∈ (𝑧(Hom ‘𝑂)𝑤))) → 𝑈 ∈ V)
103102adantr 481 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑧𝐵𝑤𝐵 ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → 𝑈 ∈ V)
10453ad2antrr 723 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑧𝐵𝑤𝐵 ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → ((1st𝐹)‘𝑋) ∈ 𝑈)
105553ad2antr1 1187 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑧𝐵𝑤𝐵 ∈ (𝑧(Hom ‘𝑂)𝑤))) → ((1st𝐹)‘𝑧) ∈ 𝑈)
106105adantr 481 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑧𝐵𝑤𝐵 ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → ((1st𝐹)‘𝑧) ∈ 𝑈)
10752adantr 481 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑧𝐵𝑤𝐵 ∈ (𝑧(Hom ‘𝑂)𝑤))) → (1st𝐹):𝐵𝑈)
108107, 93ffvelcdmd 6994 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑧𝐵𝑤𝐵 ∈ (𝑧(Hom ‘𝑂)𝑤))) → ((1st𝐹)‘𝑤) ∈ 𝑈)
109108adantr 481 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑧𝐵𝑤𝐵 ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → ((1st𝐹)‘𝑤) ∈ 𝑈)
11028, 29, 30, 89, 82, 83funcf2 17642 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑧𝐵𝑤𝐵 ∈ (𝑧(Hom ‘𝑂)𝑤))) → (𝑋(2nd𝐹)𝑧):(𝑋(Hom ‘𝑂)𝑧)⟶(((1st𝐹)‘𝑋)(Hom ‘𝑆)((1st𝐹)‘𝑧)))
111110adantr 481 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑧𝐵𝑤𝐵 ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → (𝑋(2nd𝐹)𝑧):(𝑋(Hom ‘𝑂)𝑧)⟶(((1st𝐹)‘𝑋)(Hom ‘𝑆)((1st𝐹)‘𝑧)))
112111, 96ffvelcdmd 6994 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑧𝐵𝑤𝐵 ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → ((𝑋(2nd𝐹)𝑧)‘𝑘) ∈ (((1st𝐹)‘𝑋)(Hom ‘𝑆)((1st𝐹)‘𝑧)))
1135, 103, 30, 104, 106elsetchom 17855 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑧𝐵𝑤𝐵 ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → (((𝑋(2nd𝐹)𝑧)‘𝑘) ∈ (((1st𝐹)‘𝑋)(Hom ‘𝑆)((1st𝐹)‘𝑧)) ↔ ((𝑋(2nd𝐹)𝑧)‘𝑘):((1st𝐹)‘𝑋)⟶((1st𝐹)‘𝑧)))
114112, 113mpbid 231 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑧𝐵𝑤𝐵 ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → ((𝑋(2nd𝐹)𝑧)‘𝑘):((1st𝐹)‘𝑋)⟶((1st𝐹)‘𝑧))
11528, 29, 30, 89, 83, 93funcf2 17642 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑧𝐵𝑤𝐵 ∈ (𝑧(Hom ‘𝑂)𝑤))) → (𝑧(2nd𝐹)𝑤):(𝑧(Hom ‘𝑂)𝑤)⟶(((1st𝐹)‘𝑧)(Hom ‘𝑆)((1st𝐹)‘𝑤)))
116 simpr3 1195 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑧𝐵𝑤𝐵 ∈ (𝑧(Hom ‘𝑂)𝑤))) → ∈ (𝑧(Hom ‘𝑂)𝑤))
117115, 116ffvelcdmd 6994 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑧𝐵𝑤𝐵 ∈ (𝑧(Hom ‘𝑂)𝑤))) → ((𝑧(2nd𝐹)𝑤)‘) ∈ (((1st𝐹)‘𝑧)(Hom ‘𝑆)((1st𝐹)‘𝑤)))
1185, 102, 30, 105, 108elsetchom 17855 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑧𝐵𝑤𝐵 ∈ (𝑧(Hom ‘𝑂)𝑤))) → (((𝑧(2nd𝐹)𝑤)‘) ∈ (((1st𝐹)‘𝑧)(Hom ‘𝑆)((1st𝐹)‘𝑤)) ↔ ((𝑧(2nd𝐹)𝑤)‘):((1st𝐹)‘𝑧)⟶((1st𝐹)‘𝑤)))
119117, 118mpbid 231 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑧𝐵𝑤𝐵 ∈ (𝑧(Hom ‘𝑂)𝑤))) → ((𝑧(2nd𝐹)𝑤)‘):((1st𝐹)‘𝑧)⟶((1st𝐹)‘𝑤))
120119adantr 481 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑧𝐵𝑤𝐵 ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → ((𝑧(2nd𝐹)𝑤)‘):((1st𝐹)‘𝑧)⟶((1st𝐹)‘𝑤))
1215, 103, 88, 104, 106, 109, 114, 120setcco 17857 . . . . . . . . . . 11 (((𝜑 ∧ (𝑧𝐵𝑤𝐵 ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → (((𝑧(2nd𝐹)𝑤)‘)(⟨((1st𝐹)‘𝑋), ((1st𝐹)‘𝑧)⟩(comp‘𝑆)((1st𝐹)‘𝑤))((𝑋(2nd𝐹)𝑧)‘𝑘)) = (((𝑧(2nd𝐹)𝑤)‘) ∘ ((𝑋(2nd𝐹)𝑧)‘𝑘)))
12298, 101, 1213eqtr3d 2783 . . . . . . . . . 10 (((𝜑 ∧ (𝑧𝐵𝑤𝐵 ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → ((𝑋(2nd𝐹)𝑤)‘(𝑘(⟨𝑤, 𝑧⟩(comp‘𝐶)𝑋))) = (((𝑧(2nd𝐹)𝑤)‘) ∘ ((𝑋(2nd𝐹)𝑧)‘𝑘)))
123122fveq1d 6806 . . . . . . . . 9 (((𝜑 ∧ (𝑧𝐵𝑤𝐵 ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → (((𝑋(2nd𝐹)𝑤)‘(𝑘(⟨𝑤, 𝑧⟩(comp‘𝐶)𝑋)))‘𝐴) = ((((𝑧(2nd𝐹)𝑤)‘) ∘ ((𝑋(2nd𝐹)𝑧)‘𝑘))‘𝐴))
12419ad2antrr 723 . . . . . . . . . 10 (((𝜑 ∧ (𝑧𝐵𝑤𝐵 ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → 𝐴 ∈ ((1st𝐹)‘𝑋))
125 fvco3 6899 . . . . . . . . . 10 ((((𝑋(2nd𝐹)𝑧)‘𝑘):((1st𝐹)‘𝑋)⟶((1st𝐹)‘𝑧) ∧ 𝐴 ∈ ((1st𝐹)‘𝑋)) → ((((𝑧(2nd𝐹)𝑤)‘) ∘ ((𝑋(2nd𝐹)𝑧)‘𝑘))‘𝐴) = (((𝑧(2nd𝐹)𝑤)‘)‘(((𝑋(2nd𝐹)𝑧)‘𝑘)‘𝐴)))
126114, 124, 125syl2anc 584 . . . . . . . . 9 (((𝜑 ∧ (𝑧𝐵𝑤𝐵 ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → ((((𝑧(2nd𝐹)𝑤)‘) ∘ ((𝑋(2nd𝐹)𝑧)‘𝑘))‘𝐴) = (((𝑧(2nd𝐹)𝑤)‘)‘(((𝑋(2nd𝐹)𝑧)‘𝑘)‘𝐴)))
127123, 126eqtrd 2775 . . . . . . . 8 (((𝜑 ∧ (𝑧𝐵𝑤𝐵 ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → (((𝑋(2nd𝐹)𝑤)‘(𝑘(⟨𝑤, 𝑧⟩(comp‘𝐶)𝑋)))‘𝐴) = (((𝑧(2nd𝐹)𝑤)‘)‘(((𝑋(2nd𝐹)𝑧)‘𝑘)‘𝐴)))
12881adantr 481 . . . . . . . . . . 11 (((𝜑 ∧ (𝑧𝐵𝑤𝐵 ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → 𝐶 ∈ Cat)
12940, 4oppchom 17484 . . . . . . . . . . . 12 (𝑧(Hom ‘𝑂)𝑤) = (𝑤(Hom ‘𝐶)𝑧)
13097, 129eleqtrdi 2846 . . . . . . . . . . 11 (((𝜑 ∧ (𝑧𝐵𝑤𝐵 ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → ∈ (𝑤(Hom ‘𝐶)𝑧))
1311, 2, 128, 91, 40, 92, 99, 94, 130, 95yon12 18042 . . . . . . . . . 10 (((𝜑 ∧ (𝑧𝐵𝑤𝐵 ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → (((𝑧(2nd ‘((1st𝑌)‘𝑋))𝑤)‘)‘𝑘) = (𝑘(⟨𝑤, 𝑧⟩(comp‘𝐶)𝑋)))
132131fveq2d 6808 . . . . . . . . 9 (((𝜑 ∧ (𝑧𝐵𝑤𝐵 ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → ((((𝐹𝑁𝑋)‘𝐴)‘𝑤)‘(((𝑧(2nd ‘((1st𝑌)‘𝑋))𝑤)‘)‘𝑘)) = ((((𝐹𝑁𝑋)‘𝐴)‘𝑤)‘(𝑘(⟨𝑤, 𝑧⟩(comp‘𝐶)𝑋))))
13313ad2antrr 723 . . . . . . . . . 10 (((𝜑 ∧ (𝑧𝐵𝑤𝐵 ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → 𝑉𝑊)
13414ad2antrr 723 . . . . . . . . . 10 (((𝜑 ∧ (𝑧𝐵𝑤𝐵 ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → ran (Homf𝐶) ⊆ 𝑈)
13515ad2antrr 723 . . . . . . . . . 10 (((𝜑 ∧ (𝑧𝐵𝑤𝐵 ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → (ran (Homf𝑄) ∪ 𝑈) ⊆ 𝑉)
13616ad2antrr 723 . . . . . . . . . 10 (((𝜑 ∧ (𝑧𝐵𝑤𝐵 ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → 𝐹 ∈ (𝑂 Func 𝑆))
1372, 40, 99, 128, 94, 92, 91, 130, 95catcocl 17453 . . . . . . . . . 10 (((𝜑 ∧ (𝑧𝐵𝑤𝐵 ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → (𝑘(⟨𝑤, 𝑧⟩(comp‘𝐶)𝑋)) ∈ (𝑤(Hom ‘𝐶)𝑋))
1381, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 128, 133, 134, 135, 136, 91, 18, 124, 94, 137yonedalem4b 18053 . . . . . . . . 9 (((𝜑 ∧ (𝑧𝐵𝑤𝐵 ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → ((((𝐹𝑁𝑋)‘𝐴)‘𝑤)‘(𝑘(⟨𝑤, 𝑧⟩(comp‘𝐶)𝑋))) = (((𝑋(2nd𝐹)𝑤)‘(𝑘(⟨𝑤, 𝑧⟩(comp‘𝐶)𝑋)))‘𝐴))
139132, 138eqtrd 2775 . . . . . . . 8 (((𝜑 ∧ (𝑧𝐵𝑤𝐵 ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → ((((𝐹𝑁𝑋)‘𝐴)‘𝑤)‘(((𝑧(2nd ‘((1st𝑌)‘𝑋))𝑤)‘)‘𝑘)) = (((𝑋(2nd𝐹)𝑤)‘(𝑘(⟨𝑤, 𝑧⟩(comp‘𝐶)𝑋)))‘𝐴))
1401, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 128, 133, 134, 135, 136, 91, 18, 124, 92, 95yonedalem4b 18053 . . . . . . . . 9 (((𝜑 ∧ (𝑧𝐵𝑤𝐵 ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → ((((𝐹𝑁𝑋)‘𝐴)‘𝑧)‘𝑘) = (((𝑋(2nd𝐹)𝑧)‘𝑘)‘𝐴))
141140fveq2d 6808 . . . . . . . 8 (((𝜑 ∧ (𝑧𝐵𝑤𝐵 ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → (((𝑧(2nd𝐹)𝑤)‘)‘((((𝐹𝑁𝑋)‘𝐴)‘𝑧)‘𝑘)) = (((𝑧(2nd𝐹)𝑤)‘)‘(((𝑋(2nd𝐹)𝑧)‘𝑘)‘𝐴)))
142127, 139, 1413eqtr4d 2785 . . . . . . 7 (((𝜑 ∧ (𝑧𝐵𝑤𝐵 ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → ((((𝐹𝑁𝑋)‘𝐴)‘𝑤)‘(((𝑧(2nd ‘((1st𝑌)‘𝑋))𝑤)‘)‘𝑘)) = (((𝑧(2nd𝐹)𝑤)‘)‘((((𝐹𝑁𝑋)‘𝐴)‘𝑧)‘𝑘)))
14386, 142syldan 591 . . . . . 6 (((𝜑 ∧ (𝑧𝐵𝑤𝐵 ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ ((1st ‘((1st𝑌)‘𝑋))‘𝑧)) → ((((𝐹𝑁𝑋)‘𝐴)‘𝑤)‘(((𝑧(2nd ‘((1st𝑌)‘𝑋))𝑤)‘)‘𝑘)) = (((𝑧(2nd𝐹)𝑤)‘)‘((((𝐹𝑁𝑋)‘𝐴)‘𝑧)‘𝑘)))
144143mpteq2dva 5180 . . . . 5 ((𝜑 ∧ (𝑧𝐵𝑤𝐵 ∈ (𝑧(Hom ‘𝑂)𝑤))) → (𝑘 ∈ ((1st ‘((1st𝑌)‘𝑋))‘𝑧) ↦ ((((𝐹𝑁𝑋)‘𝐴)‘𝑤)‘(((𝑧(2nd ‘((1st𝑌)‘𝑋))𝑤)‘)‘𝑘))) = (𝑘 ∈ ((1st ‘((1st𝑌)‘𝑋))‘𝑧) ↦ (((𝑧(2nd𝐹)𝑤)‘)‘((((𝐹𝑁𝑋)‘𝐴)‘𝑧)‘𝑘))))
145 fveq2 6804 . . . . . . . 8 (𝑧 = 𝑤 → (((𝐹𝑁𝑋)‘𝐴)‘𝑧) = (((𝐹𝑁𝑋)‘𝐴)‘𝑤))
146 fveq2 6804 . . . . . . . 8 (𝑧 = 𝑤 → ((1st ‘((1st𝑌)‘𝑋))‘𝑧) = ((1st ‘((1st𝑌)‘𝑋))‘𝑤))
147 fveq2 6804 . . . . . . . 8 (𝑧 = 𝑤 → ((1st𝐹)‘𝑧) = ((1st𝐹)‘𝑤))
148145, 146, 147feq123d 6619 . . . . . . 7 (𝑧 = 𝑤 → ((((𝐹𝑁𝑋)‘𝐴)‘𝑧):((1st ‘((1st𝑌)‘𝑋))‘𝑧)⟶((1st𝐹)‘𝑧) ↔ (((𝐹𝑁𝑋)‘𝐴)‘𝑤):((1st ‘((1st𝑌)‘𝑋))‘𝑤)⟶((1st𝐹)‘𝑤)))
14927fveq1d 6806 . . . . . . . . . . . 12 (𝜑 → (((𝐹𝑁𝑋)‘𝐴)‘𝑧) = ((𝑧𝐵 ↦ (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd𝐹)𝑧)‘𝑔)‘𝐴)))‘𝑧))
150 ovex 7341 . . . . . . . . . . . . . 14 (𝑧(Hom ‘𝐶)𝑋) ∈ V
151150mptex 7131 . . . . . . . . . . . . 13 (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd𝐹)𝑧)‘𝑔)‘𝐴)) ∈ V
152 eqid 2735 . . . . . . . . . . . . . 14 (𝑧𝐵 ↦ (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd𝐹)𝑧)‘𝑔)‘𝐴))) = (𝑧𝐵 ↦ (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd𝐹)𝑧)‘𝑔)‘𝐴)))
153152fvmpt2 6918 . . . . . . . . . . . . 13 ((𝑧𝐵 ∧ (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd𝐹)𝑧)‘𝑔)‘𝐴)) ∈ V) → ((𝑧𝐵 ↦ (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd𝐹)𝑧)‘𝑔)‘𝐴)))‘𝑧) = (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd𝐹)𝑧)‘𝑔)‘𝐴)))
154151, 153mpan2 688 . . . . . . . . . . . 12 (𝑧𝐵 → ((𝑧𝐵 ↦ (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd𝐹)𝑧)‘𝑔)‘𝐴)))‘𝑧) = (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd𝐹)𝑧)‘𝑔)‘𝐴)))
155149, 154sylan9eq 2795 . . . . . . . . . . 11 ((𝜑𝑧𝐵) → (((𝐹𝑁𝑋)‘𝐴)‘𝑧) = (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd𝐹)𝑧)‘𝑔)‘𝐴)))
156155feq1d 6615 . . . . . . . . . 10 ((𝜑𝑧𝐵) → ((((𝐹𝑁𝑋)‘𝐴)‘𝑧):((1st ‘((1st𝑌)‘𝑋))‘𝑧)⟶((1st𝐹)‘𝑧) ↔ (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd𝐹)𝑧)‘𝑔)‘𝐴)):((1st ‘((1st𝑌)‘𝑋))‘𝑧)⟶((1st𝐹)‘𝑧)))
15765, 156mpbird 256 . . . . . . . . 9 ((𝜑𝑧𝐵) → (((𝐹𝑁𝑋)‘𝐴)‘𝑧):((1st ‘((1st𝑌)‘𝑋))‘𝑧)⟶((1st𝐹)‘𝑧))
158157ralrimiva 3138 . . . . . . . 8 (𝜑 → ∀𝑧𝐵 (((𝐹𝑁𝑋)‘𝐴)‘𝑧):((1st ‘((1st𝑌)‘𝑋))‘𝑧)⟶((1st𝐹)‘𝑧))
159158adantr 481 . . . . . . 7 ((𝜑 ∧ (𝑧𝐵𝑤𝐵 ∈ (𝑧(Hom ‘𝑂)𝑤))) → ∀𝑧𝐵 (((𝐹𝑁𝑋)‘𝐴)‘𝑧):((1st ‘((1st𝑌)‘𝑋))‘𝑧)⟶((1st𝐹)‘𝑧))
160148, 159, 93rspcdva 3566 . . . . . 6 ((𝜑 ∧ (𝑧𝐵𝑤𝐵 ∈ (𝑧(Hom ‘𝑂)𝑤))) → (((𝐹𝑁𝑋)‘𝐴)‘𝑤):((1st ‘((1st𝑌)‘𝑋))‘𝑤)⟶((1st𝐹)‘𝑤))
16168adantr 481 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝐵𝑤𝐵 ∈ (𝑧(Hom ‘𝑂)𝑤))) → (1st ‘((1st𝑌)‘𝑋))(𝑂 Func 𝑆)(2nd ‘((1st𝑌)‘𝑋)))
16228, 29, 30, 161, 83, 93funcf2 17642 . . . . . . . 8 ((𝜑 ∧ (𝑧𝐵𝑤𝐵 ∈ (𝑧(Hom ‘𝑂)𝑤))) → (𝑧(2nd ‘((1st𝑌)‘𝑋))𝑤):(𝑧(Hom ‘𝑂)𝑤)⟶(((1st ‘((1st𝑌)‘𝑋))‘𝑧)(Hom ‘𝑆)((1st ‘((1st𝑌)‘𝑋))‘𝑤)))
163162, 116ffvelcdmd 6994 . . . . . . 7 ((𝜑 ∧ (𝑧𝐵𝑤𝐵 ∈ (𝑧(Hom ‘𝑂)𝑤))) → ((𝑧(2nd ‘((1st𝑌)‘𝑋))𝑤)‘) ∈ (((1st ‘((1st𝑌)‘𝑋))‘𝑧)(Hom ‘𝑆)((1st ‘((1st𝑌)‘𝑋))‘𝑤)))
164723ad2antr1 1187 . . . . . . . 8 ((𝜑 ∧ (𝑧𝐵𝑤𝐵 ∈ (𝑧(Hom ‘𝑂)𝑤))) → ((1st ‘((1st𝑌)‘𝑋))‘𝑧) ∈ 𝑈)
16571adantr 481 . . . . . . . . 9 ((𝜑 ∧ (𝑧𝐵𝑤𝐵 ∈ (𝑧(Hom ‘𝑂)𝑤))) → (1st ‘((1st𝑌)‘𝑋)):𝐵𝑈)
166165, 93ffvelcdmd 6994 . . . . . . . 8 ((𝜑 ∧ (𝑧𝐵𝑤𝐵 ∈ (𝑧(Hom ‘𝑂)𝑤))) → ((1st ‘((1st𝑌)‘𝑋))‘𝑤) ∈ 𝑈)
1675, 102, 30, 164, 166elsetchom 17855 . . . . . . 7 ((𝜑 ∧ (𝑧𝐵𝑤𝐵 ∈ (𝑧(Hom ‘𝑂)𝑤))) → (((𝑧(2nd ‘((1st𝑌)‘𝑋))𝑤)‘) ∈ (((1st ‘((1st𝑌)‘𝑋))‘𝑧)(Hom ‘𝑆)((1st ‘((1st𝑌)‘𝑋))‘𝑤)) ↔ ((𝑧(2nd ‘((1st𝑌)‘𝑋))𝑤)‘):((1st ‘((1st𝑌)‘𝑋))‘𝑧)⟶((1st ‘((1st𝑌)‘𝑋))‘𝑤)))
168163, 167mpbid 231 . . . . . 6 ((𝜑 ∧ (𝑧𝐵𝑤𝐵 ∈ (𝑧(Hom ‘𝑂)𝑤))) → ((𝑧(2nd ‘((1st𝑌)‘𝑋))𝑤)‘):((1st ‘((1st𝑌)‘𝑋))‘𝑧)⟶((1st ‘((1st𝑌)‘𝑋))‘𝑤))
169 fcompt 7037 . . . . . 6 (((((𝐹𝑁𝑋)‘𝐴)‘𝑤):((1st ‘((1st𝑌)‘𝑋))‘𝑤)⟶((1st𝐹)‘𝑤) ∧ ((𝑧(2nd ‘((1st𝑌)‘𝑋))𝑤)‘):((1st ‘((1st𝑌)‘𝑋))‘𝑧)⟶((1st ‘((1st𝑌)‘𝑋))‘𝑤)) → ((((𝐹𝑁𝑋)‘𝐴)‘𝑤) ∘ ((𝑧(2nd ‘((1st𝑌)‘𝑋))𝑤)‘)) = (𝑘 ∈ ((1st ‘((1st𝑌)‘𝑋))‘𝑧) ↦ ((((𝐹𝑁𝑋)‘𝐴)‘𝑤)‘(((𝑧(2nd ‘((1st𝑌)‘𝑋))𝑤)‘)‘𝑘))))
170160, 168, 169syl2anc 584 . . . . 5 ((𝜑 ∧ (𝑧𝐵𝑤𝐵 ∈ (𝑧(Hom ‘𝑂)𝑤))) → ((((𝐹𝑁𝑋)‘𝐴)‘𝑤) ∘ ((𝑧(2nd ‘((1st𝑌)‘𝑋))𝑤)‘)) = (𝑘 ∈ ((1st ‘((1st𝑌)‘𝑋))‘𝑧) ↦ ((((𝐹𝑁𝑋)‘𝐴)‘𝑤)‘(((𝑧(2nd ‘((1st𝑌)‘𝑋))𝑤)‘)‘𝑘))))
1711573ad2antr1 1187 . . . . . 6 ((𝜑 ∧ (𝑧𝐵𝑤𝐵 ∈ (𝑧(Hom ‘𝑂)𝑤))) → (((𝐹𝑁𝑋)‘𝐴)‘𝑧):((1st ‘((1st𝑌)‘𝑋))‘𝑧)⟶((1st𝐹)‘𝑧))
172 fcompt 7037 . . . . . 6 ((((𝑧(2nd𝐹)𝑤)‘):((1st𝐹)‘𝑧)⟶((1st𝐹)‘𝑤) ∧ (((𝐹𝑁𝑋)‘𝐴)‘𝑧):((1st ‘((1st𝑌)‘𝑋))‘𝑧)⟶((1st𝐹)‘𝑧)) → (((𝑧(2nd𝐹)𝑤)‘) ∘ (((𝐹𝑁𝑋)‘𝐴)‘𝑧)) = (𝑘 ∈ ((1st ‘((1st𝑌)‘𝑋))‘𝑧) ↦ (((𝑧(2nd𝐹)𝑤)‘)‘((((𝐹𝑁𝑋)‘𝐴)‘𝑧)‘𝑘))))
173119, 171, 172syl2anc 584 . . . . 5 ((𝜑 ∧ (𝑧𝐵𝑤𝐵 ∈ (𝑧(Hom ‘𝑂)𝑤))) → (((𝑧(2nd𝐹)𝑤)‘) ∘ (((𝐹𝑁𝑋)‘𝐴)‘𝑧)) = (𝑘 ∈ ((1st ‘((1st𝑌)‘𝑋))‘𝑧) ↦ (((𝑧(2nd𝐹)𝑤)‘)‘((((𝐹𝑁𝑋)‘𝐴)‘𝑧)‘𝑘))))
174144, 170, 1733eqtr4d 2785 . . . 4 ((𝜑 ∧ (𝑧𝐵𝑤𝐵 ∈ (𝑧(Hom ‘𝑂)𝑤))) → ((((𝐹𝑁𝑋)‘𝐴)‘𝑤) ∘ ((𝑧(2nd ‘((1st𝑌)‘𝑋))𝑤)‘)) = (((𝑧(2nd𝐹)𝑤)‘) ∘ (((𝐹𝑁𝑋)‘𝐴)‘𝑧)))
1755, 102, 88, 164, 166, 108, 168, 160setcco 17857 . . . 4 ((𝜑 ∧ (𝑧𝐵𝑤𝐵 ∈ (𝑧(Hom ‘𝑂)𝑤))) → ((((𝐹𝑁𝑋)‘𝐴)‘𝑤)(⟨((1st ‘((1st𝑌)‘𝑋))‘𝑧), ((1st ‘((1st𝑌)‘𝑋))‘𝑤)⟩(comp‘𝑆)((1st𝐹)‘𝑤))((𝑧(2nd ‘((1st𝑌)‘𝑋))𝑤)‘)) = ((((𝐹𝑁𝑋)‘𝐴)‘𝑤) ∘ ((𝑧(2nd ‘((1st𝑌)‘𝑋))𝑤)‘)))
1765, 102, 88, 164, 105, 108, 171, 119setcco 17857 . . . 4 ((𝜑 ∧ (𝑧𝐵𝑤𝐵 ∈ (𝑧(Hom ‘𝑂)𝑤))) → (((𝑧(2nd𝐹)𝑤)‘)(⟨((1st ‘((1st𝑌)‘𝑋))‘𝑧), ((1st𝐹)‘𝑧)⟩(comp‘𝑆)((1st𝐹)‘𝑤))(((𝐹𝑁𝑋)‘𝐴)‘𝑧)) = (((𝑧(2nd𝐹)𝑤)‘) ∘ (((𝐹𝑁𝑋)‘𝐴)‘𝑧)))
177174, 175, 1763eqtr4d 2785 . . 3 ((𝜑 ∧ (𝑧𝐵𝑤𝐵 ∈ (𝑧(Hom ‘𝑂)𝑤))) → ((((𝐹𝑁𝑋)‘𝐴)‘𝑤)(⟨((1st ‘((1st𝑌)‘𝑋))‘𝑧), ((1st ‘((1st𝑌)‘𝑋))‘𝑤)⟩(comp‘𝑆)((1st𝐹)‘𝑤))((𝑧(2nd ‘((1st𝑌)‘𝑋))𝑤)‘)) = (((𝑧(2nd𝐹)𝑤)‘)(⟨((1st ‘((1st𝑌)‘𝑋))‘𝑧), ((1st𝐹)‘𝑧)⟩(comp‘𝑆)((1st𝐹)‘𝑤))(((𝐹𝑁𝑋)‘𝐴)‘𝑧)))
178177ralrimivvva 3195 . 2 (𝜑 → ∀𝑧𝐵𝑤𝐵 ∈ (𝑧(Hom ‘𝑂)𝑤)((((𝐹𝑁𝑋)‘𝐴)‘𝑤)(⟨((1st ‘((1st𝑌)‘𝑋))‘𝑧), ((1st ‘((1st𝑌)‘𝑋))‘𝑤)⟩(comp‘𝑆)((1st𝐹)‘𝑤))((𝑧(2nd ‘((1st𝑌)‘𝑋))𝑤)‘)) = (((𝑧(2nd𝐹)𝑤)‘)(⟨((1st ‘((1st𝑌)‘𝑋))‘𝑧), ((1st𝐹)‘𝑧)⟩(comp‘𝑆)((1st𝐹)‘𝑤))(((𝐹𝑁𝑋)‘𝐴)‘𝑧)))
179 eqid 2735 . . 3 (𝑂 Nat 𝑆) = (𝑂 Nat 𝑆)
180179, 28, 29, 30, 88, 66, 16isnat2 17723 . 2 (𝜑 → (((𝐹𝑁𝑋)‘𝐴) ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↔ (((𝐹𝑁𝑋)‘𝐴) ∈ X𝑧𝐵 (((1st ‘((1st𝑌)‘𝑋))‘𝑧)(Hom ‘𝑆)((1st𝐹)‘𝑧)) ∧ ∀𝑧𝐵𝑤𝐵 ∈ (𝑧(Hom ‘𝑂)𝑤)((((𝐹𝑁𝑋)‘𝐴)‘𝑤)(⟨((1st ‘((1st𝑌)‘𝑋))‘𝑧), ((1st ‘((1st𝑌)‘𝑋))‘𝑤)⟩(comp‘𝑆)((1st𝐹)‘𝑤))((𝑧(2nd ‘((1st𝑌)‘𝑋))𝑤)‘)) = (((𝑧(2nd𝐹)𝑤)‘)(⟨((1st ‘((1st𝑌)‘𝑋))‘𝑧), ((1st𝐹)‘𝑧)⟩(comp‘𝑆)((1st𝐹)‘𝑤))(((𝐹𝑁𝑋)‘𝐴)‘𝑧)))))
18180, 178, 180mpbir2and 710 1 (𝜑 → ((𝐹𝑁𝑋)‘𝐴) ∈ (((1st𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  w3a 1086   = wceq 1538  wcel 2103  wral 3060  Vcvv 3436  cun 3889  wss 3891  cop 4570   class class class wbr 5080  cmpt 5163  ran crn 5601  ccom 5604  Rel wrel 5605  wf 6454  cfv 6458  (class class class)co 7308  cmpo 7310  1st c1st 7865  2nd c2nd 7866  tpos ctpos 8076  Xcixp 8721  Basecbs 16971  Hom chom 17032  compcco 17033  Catccat 17432  Idccid 17433  Homf chomf 17434  oppCatcoppc 17479   Func cfunc 17628  func ccofu 17630   Nat cnat 17716   FuncCat cfuc 17717  SetCatcsetc 17849   ×c cxpc 17944   1stF c1stf 17945   2ndF c2ndf 17946   ⟨,⟩F cprf 17947   evalF cevlf 17986  HomFchof 18025  Yoncyon 18026
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1910  ax-6 1968  ax-7 2008  ax-8 2105  ax-9 2113  ax-10 2134  ax-11 2151  ax-12 2168  ax-ext 2706  ax-rep 5217  ax-sep 5231  ax-nul 5238  ax-pow 5296  ax-pr 5360  ax-un 7621  ax-cnex 10987  ax-resscn 10988  ax-1cn 10989  ax-icn 10990  ax-addcl 10991  ax-addrcl 10992  ax-mulcl 10993  ax-mulrcl 10994  ax-mulcom 10995  ax-addass 10996  ax-mulass 10997  ax-distr 10998  ax-i2m1 10999  ax-1ne0 11000  ax-1rid 11001  ax-rnegex 11002  ax-rrecex 11003  ax-cnre 11004  ax-pre-lttri 11005  ax-pre-lttrn 11006  ax-pre-ltadd 11007  ax-pre-mulgt0 11008
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1541  df-fal 1551  df-ex 1779  df-nf 1783  df-sb 2065  df-mo 2537  df-eu 2566  df-clab 2713  df-cleq 2727  df-clel 2813  df-nfc 2885  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3339  df-reu 3340  df-rab 3357  df-v 3438  df-sbc 3721  df-csb 3837  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-pss 3910  df-nul 4262  df-if 4465  df-pw 4540  df-sn 4565  df-pr 4567  df-tp 4569  df-op 4571  df-uni 4844  df-iun 4932  df-br 5081  df-opab 5143  df-mpt 5164  df-tr 5198  df-id 5500  df-eprel 5506  df-po 5514  df-so 5515  df-fr 5555  df-we 5557  df-xp 5606  df-rel 5607  df-cnv 5608  df-co 5609  df-dm 5610  df-rn 5611  df-res 5612  df-ima 5613  df-pred 6217  df-ord 6284  df-on 6285  df-lim 6286  df-suc 6287  df-iota 6410  df-fun 6460  df-fn 6461  df-f 6462  df-f1 6463  df-fo 6464  df-f1o 6465  df-fv 6466  df-riota 7265  df-ov 7311  df-oprab 7312  df-mpo 7313  df-om 7749  df-1st 7867  df-2nd 7868  df-tpos 8077  df-frecs 8132  df-wrecs 8163  df-recs 8237  df-rdg 8276  df-1o 8332  df-er 8534  df-map 8653  df-ixp 8722  df-en 8770  df-dom 8771  df-sdom 8772  df-fin 8773  df-pnf 11071  df-mnf 11072  df-xr 11073  df-ltxr 11074  df-le 11075  df-sub 11267  df-neg 11268  df-nn 12034  df-2 12096  df-3 12097  df-4 12098  df-5 12099  df-6 12100  df-7 12101  df-8 12102  df-9 12103  df-n0 12294  df-z 12380  df-dec 12498  df-uz 12643  df-fz 13300  df-struct 16907  df-sets 16924  df-slot 16942  df-ndx 16954  df-base 16972  df-hom 17045  df-cco 17046  df-cat 17436  df-cid 17437  df-homf 17438  df-comf 17439  df-oppc 17480  df-func 17632  df-nat 17718  df-fuc 17719  df-setc 17850  df-xpc 17948  df-curf 17991  df-hof 18027  df-yon 18028
This theorem is referenced by:  yonedainv  18058
  Copyright terms: Public domain W3C validator