| Step | Hyp | Ref | 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 ‘𝐹)‘𝑋)) | 
| 20 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 14, 15, 16, 17, 18, 19 | yonedalem4a 18321 | . . . 4
⊢ (𝜑 → ((𝐹𝑁𝑋)‘𝐴) = (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd ‘𝐹)𝑦)‘𝑔)‘𝐴)))) | 
| 21 |  | oveq1 7439 | . . . . . 6
⊢ (𝑦 = 𝑧 → (𝑦(Hom ‘𝐶)𝑋) = (𝑧(Hom ‘𝐶)𝑋)) | 
| 22 |  | oveq2 7440 | . . . . . . . 8
⊢ (𝑦 = 𝑧 → (𝑋(2nd ‘𝐹)𝑦) = (𝑋(2nd ‘𝐹)𝑧)) | 
| 23 | 22 | fveq1d 6907 | . . . . . . 7
⊢ (𝑦 = 𝑧 → ((𝑋(2nd ‘𝐹)𝑦)‘𝑔) = ((𝑋(2nd ‘𝐹)𝑧)‘𝑔)) | 
| 24 | 23 | fveq1d 6907 | . . . . . 6
⊢ (𝑦 = 𝑧 → (((𝑋(2nd ‘𝐹)𝑦)‘𝑔)‘𝐴) = (((𝑋(2nd ‘𝐹)𝑧)‘𝑔)‘𝐴)) | 
| 25 | 21, 24 | mpteq12dv 5232 | . . . . 5
⊢ (𝑦 = 𝑧 → (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd ‘𝐹)𝑦)‘𝑔)‘𝐴)) = (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd ‘𝐹)𝑧)‘𝑔)‘𝐴))) | 
| 26 | 25 | cbvmptv 5254 | . . . 4
⊢ (𝑦 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd ‘𝐹)𝑦)‘𝑔)‘𝐴))) = (𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd ‘𝐹)𝑧)‘𝑔)‘𝐴))) | 
| 27 | 20, 26 | eqtrdi 2792 | . . 3
⊢ (𝜑 → ((𝐹𝑁𝑋)‘𝐴) = (𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd ‘𝐹)𝑧)‘𝑔)‘𝐴)))) | 
| 28 | 4, 2 | oppcbas 17762 | . . . . . . . . . . . . 13
⊢ 𝐵 = (Base‘𝑂) | 
| 29 |  | eqid 2736 | . . . . . . . . . . . . 13
⊢ (Hom
‘𝑂) = (Hom
‘𝑂) | 
| 30 |  | eqid 2736 | . . . . . . . . . . . . 13
⊢ (Hom
‘𝑆) = (Hom
‘𝑆) | 
| 31 |  | relfunc 17908 | . . . . . . . . . . . . . . 15
⊢ Rel
(𝑂 Func 𝑆) | 
| 32 |  | 1st2ndbr 8068 | . . . . . . . . . . . . . . 15
⊢ ((Rel
(𝑂 Func 𝑆) ∧ 𝐹 ∈ (𝑂 Func 𝑆)) → (1st ‘𝐹)(𝑂 Func 𝑆)(2nd ‘𝐹)) | 
| 33 | 31, 16, 32 | sylancr 587 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (1st
‘𝐹)(𝑂 Func 𝑆)(2nd ‘𝐹)) | 
| 34 | 33 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (1st ‘𝐹)(𝑂 Func 𝑆)(2nd ‘𝐹)) | 
| 35 | 17 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → 𝑋 ∈ 𝐵) | 
| 36 |  | simpr 484 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → 𝑧 ∈ 𝐵) | 
| 37 | 28, 29, 30, 34, 35, 36 | funcf2 17914 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (𝑋(2nd ‘𝐹)𝑧):(𝑋(Hom ‘𝑂)𝑧)⟶(((1st ‘𝐹)‘𝑋)(Hom ‘𝑆)((1st ‘𝐹)‘𝑧))) | 
| 38 | 37 | adantr 480 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋)) → (𝑋(2nd ‘𝐹)𝑧):(𝑋(Hom ‘𝑂)𝑧)⟶(((1st ‘𝐹)‘𝑋)(Hom ‘𝑆)((1st ‘𝐹)‘𝑧))) | 
| 39 |  | simpr 484 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋)) → 𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋)) | 
| 40 |  | eqid 2736 | . . . . . . . . . . . . 13
⊢ (Hom
‘𝐶) = (Hom
‘𝐶) | 
| 41 | 40, 4 | oppchom 17759 | . . . . . . . . . . . 12
⊢ (𝑋(Hom ‘𝑂)𝑧) = (𝑧(Hom ‘𝐶)𝑋) | 
| 42 | 39, 41 | eleqtrrdi 2851 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋)) → 𝑔 ∈ (𝑋(Hom ‘𝑂)𝑧)) | 
| 43 | 38, 42 | ffvelcdmd 7104 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋)) → ((𝑋(2nd ‘𝐹)𝑧)‘𝑔) ∈ (((1st ‘𝐹)‘𝑋)(Hom ‘𝑆)((1st ‘𝐹)‘𝑧))) | 
| 44 | 15 | unssbd 4193 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑈 ⊆ 𝑉) | 
| 45 | 13, 44 | ssexd 5323 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝑈 ∈ V) | 
| 46 | 45 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → 𝑈 ∈ V) | 
| 47 | 46 | adantr 480 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋)) → 𝑈 ∈ V) | 
| 48 |  | eqid 2736 | . . . . . . . . . . . . . . 15
⊢
(Base‘𝑆) =
(Base‘𝑆) | 
| 49 | 28, 48, 33 | funcf1 17912 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (1st
‘𝐹):𝐵⟶(Base‘𝑆)) | 
| 50 | 5, 45 | setcbas 18124 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑈 = (Base‘𝑆)) | 
| 51 | 50 | feq3d 6722 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ((1st
‘𝐹):𝐵⟶𝑈 ↔ (1st ‘𝐹):𝐵⟶(Base‘𝑆))) | 
| 52 | 49, 51 | mpbird 257 | . . . . . . . . . . . . 13
⊢ (𝜑 → (1st
‘𝐹):𝐵⟶𝑈) | 
| 53 | 52, 17 | ffvelcdmd 7104 | . . . . . . . . . . . 12
⊢ (𝜑 → ((1st
‘𝐹)‘𝑋) ∈ 𝑈) | 
| 54 | 53 | ad2antrr 726 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋)) → ((1st ‘𝐹)‘𝑋) ∈ 𝑈) | 
| 55 | 52 | ffvelcdmda 7103 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → ((1st ‘𝐹)‘𝑧) ∈ 𝑈) | 
| 56 | 55 | adantr 480 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋)) → ((1st ‘𝐹)‘𝑧) ∈ 𝑈) | 
| 57 | 5, 47, 30, 54, 56 | elsetchom 18127 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋)) → (((𝑋(2nd ‘𝐹)𝑧)‘𝑔) ∈ (((1st ‘𝐹)‘𝑋)(Hom ‘𝑆)((1st ‘𝐹)‘𝑧)) ↔ ((𝑋(2nd ‘𝐹)𝑧)‘𝑔):((1st ‘𝐹)‘𝑋)⟶((1st ‘𝐹)‘𝑧))) | 
| 58 | 43, 57 | mpbid 232 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋)) → ((𝑋(2nd ‘𝐹)𝑧)‘𝑔):((1st ‘𝐹)‘𝑋)⟶((1st ‘𝐹)‘𝑧)) | 
| 59 | 19 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋)) → 𝐴 ∈ ((1st ‘𝐹)‘𝑋)) | 
| 60 | 58, 59 | ffvelcdmd 7104 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ 𝐵) ∧ 𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋)) → (((𝑋(2nd ‘𝐹)𝑧)‘𝑔)‘𝐴) ∈ ((1st ‘𝐹)‘𝑧)) | 
| 61 | 60 | fmpttd 7134 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd ‘𝐹)𝑧)‘𝑔)‘𝐴)):(𝑧(Hom ‘𝐶)𝑋)⟶((1st ‘𝐹)‘𝑧)) | 
| 62 | 12 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → 𝐶 ∈ Cat) | 
| 63 | 1, 2, 62, 35, 40, 36 | yon11 18310 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → ((1st
‘((1st ‘𝑌)‘𝑋))‘𝑧) = (𝑧(Hom ‘𝐶)𝑋)) | 
| 64 | 63 | feq2d 6721 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → ((𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd ‘𝐹)𝑧)‘𝑔)‘𝐴)):((1st ‘((1st
‘𝑌)‘𝑋))‘𝑧)⟶((1st ‘𝐹)‘𝑧) ↔ (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd ‘𝐹)𝑧)‘𝑔)‘𝐴)):(𝑧(Hom ‘𝐶)𝑋)⟶((1st ‘𝐹)‘𝑧))) | 
| 65 | 61, 64 | mpbird 257 | . . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd ‘𝐹)𝑧)‘𝑔)‘𝐴)):((1st ‘((1st
‘𝑌)‘𝑋))‘𝑧)⟶((1st ‘𝐹)‘𝑧)) | 
| 66 | 1, 2, 12, 17, 4, 5, 45, 14 | yon1cl 18309 | . . . . . . . . . . 11
⊢ (𝜑 → ((1st
‘𝑌)‘𝑋) ∈ (𝑂 Func 𝑆)) | 
| 67 |  | 1st2ndbr 8068 | . . . . . . . . . . 11
⊢ ((Rel
(𝑂 Func 𝑆) ∧ ((1st ‘𝑌)‘𝑋) ∈ (𝑂 Func 𝑆)) → (1st
‘((1st ‘𝑌)‘𝑋))(𝑂 Func 𝑆)(2nd ‘((1st
‘𝑌)‘𝑋))) | 
| 68 | 31, 66, 67 | sylancr 587 | . . . . . . . . . 10
⊢ (𝜑 → (1st
‘((1st ‘𝑌)‘𝑋))(𝑂 Func 𝑆)(2nd ‘((1st
‘𝑌)‘𝑋))) | 
| 69 | 28, 48, 68 | funcf1 17912 | . . . . . . . . 9
⊢ (𝜑 → (1st
‘((1st ‘𝑌)‘𝑋)):𝐵⟶(Base‘𝑆)) | 
| 70 | 50 | feq3d 6722 | . . . . . . . . 9
⊢ (𝜑 → ((1st
‘((1st ‘𝑌)‘𝑋)):𝐵⟶𝑈 ↔ (1st
‘((1st ‘𝑌)‘𝑋)):𝐵⟶(Base‘𝑆))) | 
| 71 | 69, 70 | mpbird 257 | . . . . . . . 8
⊢ (𝜑 → (1st
‘((1st ‘𝑌)‘𝑋)):𝐵⟶𝑈) | 
| 72 | 71 | ffvelcdmda 7103 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → ((1st
‘((1st ‘𝑌)‘𝑋))‘𝑧) ∈ 𝑈) | 
| 73 | 5, 46, 30, 72, 55 | elsetchom 18127 | . . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → ((𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd ‘𝐹)𝑧)‘𝑔)‘𝐴)) ∈ (((1st
‘((1st ‘𝑌)‘𝑋))‘𝑧)(Hom ‘𝑆)((1st ‘𝐹)‘𝑧)) ↔ (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd ‘𝐹)𝑧)‘𝑔)‘𝐴)):((1st ‘((1st
‘𝑌)‘𝑋))‘𝑧)⟶((1st ‘𝐹)‘𝑧))) | 
| 74 | 65, 73 | mpbird 257 | . . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd ‘𝐹)𝑧)‘𝑔)‘𝐴)) ∈ (((1st
‘((1st ‘𝑌)‘𝑋))‘𝑧)(Hom ‘𝑆)((1st ‘𝐹)‘𝑧))) | 
| 75 | 74 | ralrimiva 3145 | . . . 4
⊢ (𝜑 → ∀𝑧 ∈ 𝐵 (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd ‘𝐹)𝑧)‘𝑔)‘𝐴)) ∈ (((1st
‘((1st ‘𝑌)‘𝑋))‘𝑧)(Hom ‘𝑆)((1st ‘𝐹)‘𝑧))) | 
| 76 | 2 | fvexi 6919 | . . . . 5
⊢ 𝐵 ∈ V | 
| 77 |  | mptelixpg 8976 | . . . . 5
⊢ (𝐵 ∈ V → ((𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd ‘𝐹)𝑧)‘𝑔)‘𝐴))) ∈ X𝑧 ∈ 𝐵 (((1st ‘((1st
‘𝑌)‘𝑋))‘𝑧)(Hom ‘𝑆)((1st ‘𝐹)‘𝑧)) ↔ ∀𝑧 ∈ 𝐵 (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd ‘𝐹)𝑧)‘𝑔)‘𝐴)) ∈ (((1st
‘((1st ‘𝑌)‘𝑋))‘𝑧)(Hom ‘𝑆)((1st ‘𝐹)‘𝑧)))) | 
| 78 | 76, 77 | ax-mp 5 | . . . 4
⊢ ((𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd ‘𝐹)𝑧)‘𝑔)‘𝐴))) ∈ X𝑧 ∈ 𝐵 (((1st ‘((1st
‘𝑌)‘𝑋))‘𝑧)(Hom ‘𝑆)((1st ‘𝐹)‘𝑧)) ↔ ∀𝑧 ∈ 𝐵 (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd ‘𝐹)𝑧)‘𝑔)‘𝐴)) ∈ (((1st
‘((1st ‘𝑌)‘𝑋))‘𝑧)(Hom ‘𝑆)((1st ‘𝐹)‘𝑧))) | 
| 79 | 75, 78 | sylibr 234 | . . 3
⊢ (𝜑 → (𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd ‘𝐹)𝑧)‘𝑔)‘𝐴))) ∈ X𝑧 ∈ 𝐵 (((1st ‘((1st
‘𝑌)‘𝑋))‘𝑧)(Hom ‘𝑆)((1st ‘𝐹)‘𝑧))) | 
| 80 | 27, 79 | eqeltrd 2840 | . 2
⊢ (𝜑 → ((𝐹𝑁𝑋)‘𝐴) ∈ X𝑧 ∈ 𝐵 (((1st ‘((1st
‘𝑌)‘𝑋))‘𝑧)(Hom ‘𝑆)((1st ‘𝐹)‘𝑧))) | 
| 81 | 12 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) → 𝐶 ∈ Cat) | 
| 82 | 17 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) → 𝑋 ∈ 𝐵) | 
| 83 |  | simpr1 1194 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) → 𝑧 ∈ 𝐵) | 
| 84 | 1, 2, 81, 82, 40, 83 | yon11 18310 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) → ((1st
‘((1st ‘𝑌)‘𝑋))‘𝑧) = (𝑧(Hom ‘𝐶)𝑋)) | 
| 85 | 84 | eleq2d 2826 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) → (𝑘 ∈ ((1st
‘((1st ‘𝑌)‘𝑋))‘𝑧) ↔ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋))) | 
| 86 | 85 | biimpa 476 | . . . . . . 7
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ ((1st
‘((1st ‘𝑌)‘𝑋))‘𝑧)) → 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) | 
| 87 |  | eqid 2736 | . . . . . . . . . . . 12
⊢
(comp‘𝑂) =
(comp‘𝑂) | 
| 88 |  | eqid 2736 | . . . . . . . . . . . 12
⊢
(comp‘𝑆) =
(comp‘𝑆) | 
| 89 | 33 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) → (1st ‘𝐹)(𝑂 Func 𝑆)(2nd ‘𝐹)) | 
| 90 | 89 | adantr 480 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → (1st ‘𝐹)(𝑂 Func 𝑆)(2nd ‘𝐹)) | 
| 91 | 82 | adantr 480 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → 𝑋 ∈ 𝐵) | 
| 92 | 83 | adantr 480 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → 𝑧 ∈ 𝐵) | 
| 93 |  | simpr2 1195 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) → 𝑤 ∈ 𝐵) | 
| 94 | 93 | adantr 480 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → 𝑤 ∈ 𝐵) | 
| 95 |  | simpr 484 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) | 
| 96 | 95, 41 | eleqtrrdi 2851 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → 𝑘 ∈ (𝑋(Hom ‘𝑂)𝑧)) | 
| 97 |  | simplr3 1217 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → ℎ ∈ (𝑧(Hom ‘𝑂)𝑤)) | 
| 98 | 28, 29, 87, 88, 90, 91, 92, 94, 96, 97 | funcco 17917 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → ((𝑋(2nd ‘𝐹)𝑤)‘(ℎ(〈𝑋, 𝑧〉(comp‘𝑂)𝑤)𝑘)) = (((𝑧(2nd ‘𝐹)𝑤)‘ℎ)(〈((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑧)〉(comp‘𝑆)((1st ‘𝐹)‘𝑤))((𝑋(2nd ‘𝐹)𝑧)‘𝑘))) | 
| 99 |  | eqid 2736 | . . . . . . . . . . . . 13
⊢
(comp‘𝐶) =
(comp‘𝐶) | 
| 100 | 2, 99, 4, 91, 92, 94 | oppcco 17761 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → (ℎ(〈𝑋, 𝑧〉(comp‘𝑂)𝑤)𝑘) = (𝑘(〈𝑤, 𝑧〉(comp‘𝐶)𝑋)ℎ)) | 
| 101 | 100 | fveq2d 6909 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → ((𝑋(2nd ‘𝐹)𝑤)‘(ℎ(〈𝑋, 𝑧〉(comp‘𝑂)𝑤)𝑘)) = ((𝑋(2nd ‘𝐹)𝑤)‘(𝑘(〈𝑤, 𝑧〉(comp‘𝐶)𝑋)ℎ))) | 
| 102 | 45 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) → 𝑈 ∈ V) | 
| 103 | 102 | adantr 480 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → 𝑈 ∈ V) | 
| 104 | 53 | ad2antrr 726 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → ((1st ‘𝐹)‘𝑋) ∈ 𝑈) | 
| 105 | 55 | 3ad2antr1 1188 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) → ((1st ‘𝐹)‘𝑧) ∈ 𝑈) | 
| 106 | 105 | adantr 480 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → ((1st ‘𝐹)‘𝑧) ∈ 𝑈) | 
| 107 | 52 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) → (1st ‘𝐹):𝐵⟶𝑈) | 
| 108 | 107, 93 | ffvelcdmd 7104 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) → ((1st ‘𝐹)‘𝑤) ∈ 𝑈) | 
| 109 | 108 | adantr 480 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → ((1st ‘𝐹)‘𝑤) ∈ 𝑈) | 
| 110 | 28, 29, 30, 89, 82, 83 | funcf2 17914 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) → (𝑋(2nd ‘𝐹)𝑧):(𝑋(Hom ‘𝑂)𝑧)⟶(((1st ‘𝐹)‘𝑋)(Hom ‘𝑆)((1st ‘𝐹)‘𝑧))) | 
| 111 | 110 | adantr 480 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → (𝑋(2nd ‘𝐹)𝑧):(𝑋(Hom ‘𝑂)𝑧)⟶(((1st ‘𝐹)‘𝑋)(Hom ‘𝑆)((1st ‘𝐹)‘𝑧))) | 
| 112 | 111, 96 | ffvelcdmd 7104 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → ((𝑋(2nd ‘𝐹)𝑧)‘𝑘) ∈ (((1st ‘𝐹)‘𝑋)(Hom ‘𝑆)((1st ‘𝐹)‘𝑧))) | 
| 113 | 5, 103, 30, 104, 106 | elsetchom 18127 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → (((𝑋(2nd ‘𝐹)𝑧)‘𝑘) ∈ (((1st ‘𝐹)‘𝑋)(Hom ‘𝑆)((1st ‘𝐹)‘𝑧)) ↔ ((𝑋(2nd ‘𝐹)𝑧)‘𝑘):((1st ‘𝐹)‘𝑋)⟶((1st ‘𝐹)‘𝑧))) | 
| 114 | 112, 113 | mpbid 232 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → ((𝑋(2nd ‘𝐹)𝑧)‘𝑘):((1st ‘𝐹)‘𝑋)⟶((1st ‘𝐹)‘𝑧)) | 
| 115 | 28, 29, 30, 89, 83, 93 | funcf2 17914 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) → (𝑧(2nd ‘𝐹)𝑤):(𝑧(Hom ‘𝑂)𝑤)⟶(((1st ‘𝐹)‘𝑧)(Hom ‘𝑆)((1st ‘𝐹)‘𝑤))) | 
| 116 |  | simpr3 1196 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) → ℎ ∈ (𝑧(Hom ‘𝑂)𝑤)) | 
| 117 | 115, 116 | ffvelcdmd 7104 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) → ((𝑧(2nd ‘𝐹)𝑤)‘ℎ) ∈ (((1st ‘𝐹)‘𝑧)(Hom ‘𝑆)((1st ‘𝐹)‘𝑤))) | 
| 118 | 5, 102, 30, 105, 108 | elsetchom 18127 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) → (((𝑧(2nd ‘𝐹)𝑤)‘ℎ) ∈ (((1st ‘𝐹)‘𝑧)(Hom ‘𝑆)((1st ‘𝐹)‘𝑤)) ↔ ((𝑧(2nd ‘𝐹)𝑤)‘ℎ):((1st ‘𝐹)‘𝑧)⟶((1st ‘𝐹)‘𝑤))) | 
| 119 | 117, 118 | mpbid 232 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) → ((𝑧(2nd ‘𝐹)𝑤)‘ℎ):((1st ‘𝐹)‘𝑧)⟶((1st ‘𝐹)‘𝑤)) | 
| 120 | 119 | adantr 480 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → ((𝑧(2nd ‘𝐹)𝑤)‘ℎ):((1st ‘𝐹)‘𝑧)⟶((1st ‘𝐹)‘𝑤)) | 
| 121 | 5, 103, 88, 104, 106, 109, 114, 120 | setcco 18129 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → (((𝑧(2nd ‘𝐹)𝑤)‘ℎ)(〈((1st ‘𝐹)‘𝑋), ((1st ‘𝐹)‘𝑧)〉(comp‘𝑆)((1st ‘𝐹)‘𝑤))((𝑋(2nd ‘𝐹)𝑧)‘𝑘)) = (((𝑧(2nd ‘𝐹)𝑤)‘ℎ) ∘ ((𝑋(2nd ‘𝐹)𝑧)‘𝑘))) | 
| 122 | 98, 101, 121 | 3eqtr3d 2784 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → ((𝑋(2nd ‘𝐹)𝑤)‘(𝑘(〈𝑤, 𝑧〉(comp‘𝐶)𝑋)ℎ)) = (((𝑧(2nd ‘𝐹)𝑤)‘ℎ) ∘ ((𝑋(2nd ‘𝐹)𝑧)‘𝑘))) | 
| 123 | 122 | fveq1d 6907 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → (((𝑋(2nd ‘𝐹)𝑤)‘(𝑘(〈𝑤, 𝑧〉(comp‘𝐶)𝑋)ℎ))‘𝐴) = ((((𝑧(2nd ‘𝐹)𝑤)‘ℎ) ∘ ((𝑋(2nd ‘𝐹)𝑧)‘𝑘))‘𝐴)) | 
| 124 | 19 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → 𝐴 ∈ ((1st ‘𝐹)‘𝑋)) | 
| 125 |  | fvco3 7007 | . . . . . . . . . 10
⊢ ((((𝑋(2nd ‘𝐹)𝑧)‘𝑘):((1st ‘𝐹)‘𝑋)⟶((1st ‘𝐹)‘𝑧) ∧ 𝐴 ∈ ((1st ‘𝐹)‘𝑋)) → ((((𝑧(2nd ‘𝐹)𝑤)‘ℎ) ∘ ((𝑋(2nd ‘𝐹)𝑧)‘𝑘))‘𝐴) = (((𝑧(2nd ‘𝐹)𝑤)‘ℎ)‘(((𝑋(2nd ‘𝐹)𝑧)‘𝑘)‘𝐴))) | 
| 126 | 114, 124,
125 | syl2anc 584 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → ((((𝑧(2nd ‘𝐹)𝑤)‘ℎ) ∘ ((𝑋(2nd ‘𝐹)𝑧)‘𝑘))‘𝐴) = (((𝑧(2nd ‘𝐹)𝑤)‘ℎ)‘(((𝑋(2nd ‘𝐹)𝑧)‘𝑘)‘𝐴))) | 
| 127 | 123, 126 | eqtrd 2776 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → (((𝑋(2nd ‘𝐹)𝑤)‘(𝑘(〈𝑤, 𝑧〉(comp‘𝐶)𝑋)ℎ))‘𝐴) = (((𝑧(2nd ‘𝐹)𝑤)‘ℎ)‘(((𝑋(2nd ‘𝐹)𝑧)‘𝑘)‘𝐴))) | 
| 128 | 81 | adantr 480 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → 𝐶 ∈ Cat) | 
| 129 | 40, 4 | oppchom 17759 | . . . . . . . . . . . 12
⊢ (𝑧(Hom ‘𝑂)𝑤) = (𝑤(Hom ‘𝐶)𝑧) | 
| 130 | 97, 129 | eleqtrdi 2850 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → ℎ ∈ (𝑤(Hom ‘𝐶)𝑧)) | 
| 131 | 1, 2, 128, 91, 40, 92, 99, 94, 130, 95 | yon12 18311 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → (((𝑧(2nd ‘((1st
‘𝑌)‘𝑋))𝑤)‘ℎ)‘𝑘) = (𝑘(〈𝑤, 𝑧〉(comp‘𝐶)𝑋)ℎ)) | 
| 132 | 131 | fveq2d 6909 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → ((((𝐹𝑁𝑋)‘𝐴)‘𝑤)‘(((𝑧(2nd ‘((1st
‘𝑌)‘𝑋))𝑤)‘ℎ)‘𝑘)) = ((((𝐹𝑁𝑋)‘𝐴)‘𝑤)‘(𝑘(〈𝑤, 𝑧〉(comp‘𝐶)𝑋)ℎ))) | 
| 133 | 13 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → 𝑉 ∈ 𝑊) | 
| 134 | 14 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → ran (Homf
‘𝐶) ⊆ 𝑈) | 
| 135 | 15 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → (ran (Homf
‘𝑄) ∪ 𝑈) ⊆ 𝑉) | 
| 136 | 16 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → 𝐹 ∈ (𝑂 Func 𝑆)) | 
| 137 | 2, 40, 99, 128, 94, 92, 91, 130, 95 | catcocl 17729 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → (𝑘(〈𝑤, 𝑧〉(comp‘𝐶)𝑋)ℎ) ∈ (𝑤(Hom ‘𝐶)𝑋)) | 
| 138 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 128, 133, 134, 135, 136, 91, 18, 124, 94, 137 | yonedalem4b 18322 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → ((((𝐹𝑁𝑋)‘𝐴)‘𝑤)‘(𝑘(〈𝑤, 𝑧〉(comp‘𝐶)𝑋)ℎ)) = (((𝑋(2nd ‘𝐹)𝑤)‘(𝑘(〈𝑤, 𝑧〉(comp‘𝐶)𝑋)ℎ))‘𝐴)) | 
| 139 | 132, 138 | eqtrd 2776 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → ((((𝐹𝑁𝑋)‘𝐴)‘𝑤)‘(((𝑧(2nd ‘((1st
‘𝑌)‘𝑋))𝑤)‘ℎ)‘𝑘)) = (((𝑋(2nd ‘𝐹)𝑤)‘(𝑘(〈𝑤, 𝑧〉(comp‘𝐶)𝑋)ℎ))‘𝐴)) | 
| 140 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 128, 133, 134, 135, 136, 91, 18, 124, 92, 95 | yonedalem4b 18322 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → ((((𝐹𝑁𝑋)‘𝐴)‘𝑧)‘𝑘) = (((𝑋(2nd ‘𝐹)𝑧)‘𝑘)‘𝐴)) | 
| 141 | 140 | fveq2d 6909 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → (((𝑧(2nd ‘𝐹)𝑤)‘ℎ)‘((((𝐹𝑁𝑋)‘𝐴)‘𝑧)‘𝑘)) = (((𝑧(2nd ‘𝐹)𝑤)‘ℎ)‘(((𝑋(2nd ‘𝐹)𝑧)‘𝑘)‘𝐴))) | 
| 142 | 127, 139,
141 | 3eqtr4d 2786 | . . . . . . 7
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ (𝑧(Hom ‘𝐶)𝑋)) → ((((𝐹𝑁𝑋)‘𝐴)‘𝑤)‘(((𝑧(2nd ‘((1st
‘𝑌)‘𝑋))𝑤)‘ℎ)‘𝑘)) = (((𝑧(2nd ‘𝐹)𝑤)‘ℎ)‘((((𝐹𝑁𝑋)‘𝐴)‘𝑧)‘𝑘))) | 
| 143 | 86, 142 | syldan 591 | . . . . . 6
⊢ (((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) ∧ 𝑘 ∈ ((1st
‘((1st ‘𝑌)‘𝑋))‘𝑧)) → ((((𝐹𝑁𝑋)‘𝐴)‘𝑤)‘(((𝑧(2nd ‘((1st
‘𝑌)‘𝑋))𝑤)‘ℎ)‘𝑘)) = (((𝑧(2nd ‘𝐹)𝑤)‘ℎ)‘((((𝐹𝑁𝑋)‘𝐴)‘𝑧)‘𝑘))) | 
| 144 | 143 | mpteq2dva 5241 | . . . . 5
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) → (𝑘 ∈ ((1st
‘((1st ‘𝑌)‘𝑋))‘𝑧) ↦ ((((𝐹𝑁𝑋)‘𝐴)‘𝑤)‘(((𝑧(2nd ‘((1st
‘𝑌)‘𝑋))𝑤)‘ℎ)‘𝑘))) = (𝑘 ∈ ((1st
‘((1st ‘𝑌)‘𝑋))‘𝑧) ↦ (((𝑧(2nd ‘𝐹)𝑤)‘ℎ)‘((((𝐹𝑁𝑋)‘𝐴)‘𝑧)‘𝑘)))) | 
| 145 |  | fveq2 6905 | . . . . . . . 8
⊢ (𝑧 = 𝑤 → (((𝐹𝑁𝑋)‘𝐴)‘𝑧) = (((𝐹𝑁𝑋)‘𝐴)‘𝑤)) | 
| 146 |  | fveq2 6905 | . . . . . . . 8
⊢ (𝑧 = 𝑤 → ((1st
‘((1st ‘𝑌)‘𝑋))‘𝑧) = ((1st ‘((1st
‘𝑌)‘𝑋))‘𝑤)) | 
| 147 |  | fveq2 6905 | . . . . . . . 8
⊢ (𝑧 = 𝑤 → ((1st ‘𝐹)‘𝑧) = ((1st ‘𝐹)‘𝑤)) | 
| 148 | 145, 146,
147 | feq123d 6724 | . . . . . . 7
⊢ (𝑧 = 𝑤 → ((((𝐹𝑁𝑋)‘𝐴)‘𝑧):((1st ‘((1st
‘𝑌)‘𝑋))‘𝑧)⟶((1st ‘𝐹)‘𝑧) ↔ (((𝐹𝑁𝑋)‘𝐴)‘𝑤):((1st ‘((1st
‘𝑌)‘𝑋))‘𝑤)⟶((1st ‘𝐹)‘𝑤))) | 
| 149 | 27 | fveq1d 6907 | . . . . . . . . . . . 12
⊢ (𝜑 → (((𝐹𝑁𝑋)‘𝐴)‘𝑧) = ((𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd ‘𝐹)𝑧)‘𝑔)‘𝐴)))‘𝑧)) | 
| 150 |  | ovex 7465 | . . . . . . . . . . . . . 14
⊢ (𝑧(Hom ‘𝐶)𝑋) ∈ V | 
| 151 | 150 | mptex 7244 | . . . . . . . . . . . . 13
⊢ (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd ‘𝐹)𝑧)‘𝑔)‘𝐴)) ∈ V | 
| 152 |  | eqid 2736 | . . . . . . . . . . . . . 14
⊢ (𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd ‘𝐹)𝑧)‘𝑔)‘𝐴))) = (𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd ‘𝐹)𝑧)‘𝑔)‘𝐴))) | 
| 153 | 152 | fvmpt2 7026 | . . . . . . . . . . . . 13
⊢ ((𝑧 ∈ 𝐵 ∧ (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd ‘𝐹)𝑧)‘𝑔)‘𝐴)) ∈ V) → ((𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd ‘𝐹)𝑧)‘𝑔)‘𝐴)))‘𝑧) = (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd ‘𝐹)𝑧)‘𝑔)‘𝐴))) | 
| 154 | 151, 153 | mpan2 691 | . . . . . . . . . . . 12
⊢ (𝑧 ∈ 𝐵 → ((𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd ‘𝐹)𝑧)‘𝑔)‘𝐴)))‘𝑧) = (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd ‘𝐹)𝑧)‘𝑔)‘𝐴))) | 
| 155 | 149, 154 | sylan9eq 2796 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (((𝐹𝑁𝑋)‘𝐴)‘𝑧) = (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd ‘𝐹)𝑧)‘𝑔)‘𝐴))) | 
| 156 | 155 | feq1d 6719 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → ((((𝐹𝑁𝑋)‘𝐴)‘𝑧):((1st ‘((1st
‘𝑌)‘𝑋))‘𝑧)⟶((1st ‘𝐹)‘𝑧) ↔ (𝑔 ∈ (𝑧(Hom ‘𝐶)𝑋) ↦ (((𝑋(2nd ‘𝐹)𝑧)‘𝑔)‘𝐴)):((1st ‘((1st
‘𝑌)‘𝑋))‘𝑧)⟶((1st ‘𝐹)‘𝑧))) | 
| 157 | 65, 156 | mpbird 257 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐵) → (((𝐹𝑁𝑋)‘𝐴)‘𝑧):((1st ‘((1st
‘𝑌)‘𝑋))‘𝑧)⟶((1st ‘𝐹)‘𝑧)) | 
| 158 | 157 | ralrimiva 3145 | . . . . . . . 8
⊢ (𝜑 → ∀𝑧 ∈ 𝐵 (((𝐹𝑁𝑋)‘𝐴)‘𝑧):((1st ‘((1st
‘𝑌)‘𝑋))‘𝑧)⟶((1st ‘𝐹)‘𝑧)) | 
| 159 | 158 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) → ∀𝑧 ∈ 𝐵 (((𝐹𝑁𝑋)‘𝐴)‘𝑧):((1st ‘((1st
‘𝑌)‘𝑋))‘𝑧)⟶((1st ‘𝐹)‘𝑧)) | 
| 160 | 148, 159,
93 | rspcdva 3622 | . . . . . 6
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) → (((𝐹𝑁𝑋)‘𝐴)‘𝑤):((1st ‘((1st
‘𝑌)‘𝑋))‘𝑤)⟶((1st ‘𝐹)‘𝑤)) | 
| 161 | 68 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) → (1st
‘((1st ‘𝑌)‘𝑋))(𝑂 Func 𝑆)(2nd ‘((1st
‘𝑌)‘𝑋))) | 
| 162 | 28, 29, 30, 161, 83, 93 | funcf2 17914 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) → (𝑧(2nd ‘((1st
‘𝑌)‘𝑋))𝑤):(𝑧(Hom ‘𝑂)𝑤)⟶(((1st
‘((1st ‘𝑌)‘𝑋))‘𝑧)(Hom ‘𝑆)((1st ‘((1st
‘𝑌)‘𝑋))‘𝑤))) | 
| 163 | 162, 116 | ffvelcdmd 7104 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) → ((𝑧(2nd ‘((1st
‘𝑌)‘𝑋))𝑤)‘ℎ) ∈ (((1st
‘((1st ‘𝑌)‘𝑋))‘𝑧)(Hom ‘𝑆)((1st ‘((1st
‘𝑌)‘𝑋))‘𝑤))) | 
| 164 | 72 | 3ad2antr1 1188 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) → ((1st
‘((1st ‘𝑌)‘𝑋))‘𝑧) ∈ 𝑈) | 
| 165 | 71 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) → (1st
‘((1st ‘𝑌)‘𝑋)):𝐵⟶𝑈) | 
| 166 | 165, 93 | ffvelcdmd 7104 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) → ((1st
‘((1st ‘𝑌)‘𝑋))‘𝑤) ∈ 𝑈) | 
| 167 | 5, 102, 30, 164, 166 | elsetchom 18127 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) → (((𝑧(2nd ‘((1st
‘𝑌)‘𝑋))𝑤)‘ℎ) ∈ (((1st
‘((1st ‘𝑌)‘𝑋))‘𝑧)(Hom ‘𝑆)((1st ‘((1st
‘𝑌)‘𝑋))‘𝑤)) ↔ ((𝑧(2nd ‘((1st
‘𝑌)‘𝑋))𝑤)‘ℎ):((1st ‘((1st
‘𝑌)‘𝑋))‘𝑧)⟶((1st
‘((1st ‘𝑌)‘𝑋))‘𝑤))) | 
| 168 | 163, 167 | mpbid 232 | . . . . . 6
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) → ((𝑧(2nd ‘((1st
‘𝑌)‘𝑋))𝑤)‘ℎ):((1st ‘((1st
‘𝑌)‘𝑋))‘𝑧)⟶((1st
‘((1st ‘𝑌)‘𝑋))‘𝑤)) | 
| 169 |  | fcompt 7152 | . . . . . 6
⊢
(((((𝐹𝑁𝑋)‘𝐴)‘𝑤):((1st ‘((1st
‘𝑌)‘𝑋))‘𝑤)⟶((1st ‘𝐹)‘𝑤) ∧ ((𝑧(2nd ‘((1st
‘𝑌)‘𝑋))𝑤)‘ℎ):((1st ‘((1st
‘𝑌)‘𝑋))‘𝑧)⟶((1st
‘((1st ‘𝑌)‘𝑋))‘𝑤)) → ((((𝐹𝑁𝑋)‘𝐴)‘𝑤) ∘ ((𝑧(2nd ‘((1st
‘𝑌)‘𝑋))𝑤)‘ℎ)) = (𝑘 ∈ ((1st
‘((1st ‘𝑌)‘𝑋))‘𝑧) ↦ ((((𝐹𝑁𝑋)‘𝐴)‘𝑤)‘(((𝑧(2nd ‘((1st
‘𝑌)‘𝑋))𝑤)‘ℎ)‘𝑘)))) | 
| 170 | 160, 168,
169 | syl2anc 584 | . . . . 5
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) → ((((𝐹𝑁𝑋)‘𝐴)‘𝑤) ∘ ((𝑧(2nd ‘((1st
‘𝑌)‘𝑋))𝑤)‘ℎ)) = (𝑘 ∈ ((1st
‘((1st ‘𝑌)‘𝑋))‘𝑧) ↦ ((((𝐹𝑁𝑋)‘𝐴)‘𝑤)‘(((𝑧(2nd ‘((1st
‘𝑌)‘𝑋))𝑤)‘ℎ)‘𝑘)))) | 
| 171 | 157 | 3ad2antr1 1188 | . . . . . 6
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) → (((𝐹𝑁𝑋)‘𝐴)‘𝑧):((1st ‘((1st
‘𝑌)‘𝑋))‘𝑧)⟶((1st ‘𝐹)‘𝑧)) | 
| 172 |  | fcompt 7152 | . . . . . 6
⊢ ((((𝑧(2nd ‘𝐹)𝑤)‘ℎ):((1st ‘𝐹)‘𝑧)⟶((1st ‘𝐹)‘𝑤) ∧ (((𝐹𝑁𝑋)‘𝐴)‘𝑧):((1st ‘((1st
‘𝑌)‘𝑋))‘𝑧)⟶((1st ‘𝐹)‘𝑧)) → (((𝑧(2nd ‘𝐹)𝑤)‘ℎ) ∘ (((𝐹𝑁𝑋)‘𝐴)‘𝑧)) = (𝑘 ∈ ((1st
‘((1st ‘𝑌)‘𝑋))‘𝑧) ↦ (((𝑧(2nd ‘𝐹)𝑤)‘ℎ)‘((((𝐹𝑁𝑋)‘𝐴)‘𝑧)‘𝑘)))) | 
| 173 | 119, 171,
172 | syl2anc 584 | . . . . 5
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) → (((𝑧(2nd ‘𝐹)𝑤)‘ℎ) ∘ (((𝐹𝑁𝑋)‘𝐴)‘𝑧)) = (𝑘 ∈ ((1st
‘((1st ‘𝑌)‘𝑋))‘𝑧) ↦ (((𝑧(2nd ‘𝐹)𝑤)‘ℎ)‘((((𝐹𝑁𝑋)‘𝐴)‘𝑧)‘𝑘)))) | 
| 174 | 144, 170,
173 | 3eqtr4d 2786 | . . . 4
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) → ((((𝐹𝑁𝑋)‘𝐴)‘𝑤) ∘ ((𝑧(2nd ‘((1st
‘𝑌)‘𝑋))𝑤)‘ℎ)) = (((𝑧(2nd ‘𝐹)𝑤)‘ℎ) ∘ (((𝐹𝑁𝑋)‘𝐴)‘𝑧))) | 
| 175 | 5, 102, 88, 164, 166, 108, 168, 160 | setcco 18129 | . . . 4
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) → ((((𝐹𝑁𝑋)‘𝐴)‘𝑤)(〈((1st
‘((1st ‘𝑌)‘𝑋))‘𝑧), ((1st ‘((1st
‘𝑌)‘𝑋))‘𝑤)〉(comp‘𝑆)((1st ‘𝐹)‘𝑤))((𝑧(2nd ‘((1st
‘𝑌)‘𝑋))𝑤)‘ℎ)) = ((((𝐹𝑁𝑋)‘𝐴)‘𝑤) ∘ ((𝑧(2nd ‘((1st
‘𝑌)‘𝑋))𝑤)‘ℎ))) | 
| 176 | 5, 102, 88, 164, 105, 108, 171, 119 | setcco 18129 | . . . 4
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) → (((𝑧(2nd ‘𝐹)𝑤)‘ℎ)(〈((1st
‘((1st ‘𝑌)‘𝑋))‘𝑧), ((1st ‘𝐹)‘𝑧)〉(comp‘𝑆)((1st ‘𝐹)‘𝑤))(((𝐹𝑁𝑋)‘𝐴)‘𝑧)) = (((𝑧(2nd ‘𝐹)𝑤)‘ℎ) ∘ (((𝐹𝑁𝑋)‘𝐴)‘𝑧))) | 
| 177 | 174, 175,
176 | 3eqtr4d 2786 | . . 3
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ℎ ∈ (𝑧(Hom ‘𝑂)𝑤))) → ((((𝐹𝑁𝑋)‘𝐴)‘𝑤)(〈((1st
‘((1st ‘𝑌)‘𝑋))‘𝑧), ((1st ‘((1st
‘𝑌)‘𝑋))‘𝑤)〉(comp‘𝑆)((1st ‘𝐹)‘𝑤))((𝑧(2nd ‘((1st
‘𝑌)‘𝑋))𝑤)‘ℎ)) = (((𝑧(2nd ‘𝐹)𝑤)‘ℎ)(〈((1st
‘((1st ‘𝑌)‘𝑋))‘𝑧), ((1st ‘𝐹)‘𝑧)〉(comp‘𝑆)((1st ‘𝐹)‘𝑤))(((𝐹𝑁𝑋)‘𝐴)‘𝑧))) | 
| 178 | 177 | ralrimivvva 3204 | . 2
⊢ (𝜑 → ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐵 ∀ℎ ∈ (𝑧(Hom ‘𝑂)𝑤)((((𝐹𝑁𝑋)‘𝐴)‘𝑤)(〈((1st
‘((1st ‘𝑌)‘𝑋))‘𝑧), ((1st ‘((1st
‘𝑌)‘𝑋))‘𝑤)〉(comp‘𝑆)((1st ‘𝐹)‘𝑤))((𝑧(2nd ‘((1st
‘𝑌)‘𝑋))𝑤)‘ℎ)) = (((𝑧(2nd ‘𝐹)𝑤)‘ℎ)(〈((1st
‘((1st ‘𝑌)‘𝑋))‘𝑧), ((1st ‘𝐹)‘𝑧)〉(comp‘𝑆)((1st ‘𝐹)‘𝑤))(((𝐹𝑁𝑋)‘𝐴)‘𝑧))) | 
| 179 |  | eqid 2736 | . . 3
⊢ (𝑂 Nat 𝑆) = (𝑂 Nat 𝑆) | 
| 180 | 179, 28, 29, 30, 88, 66, 16 | isnat2 17997 | . 2
⊢ (𝜑 → (((𝐹𝑁𝑋)‘𝐴) ∈ (((1st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹) ↔ (((𝐹𝑁𝑋)‘𝐴) ∈ X𝑧 ∈ 𝐵 (((1st ‘((1st
‘𝑌)‘𝑋))‘𝑧)(Hom ‘𝑆)((1st ‘𝐹)‘𝑧)) ∧ ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐵 ∀ℎ ∈ (𝑧(Hom ‘𝑂)𝑤)((((𝐹𝑁𝑋)‘𝐴)‘𝑤)(〈((1st
‘((1st ‘𝑌)‘𝑋))‘𝑧), ((1st ‘((1st
‘𝑌)‘𝑋))‘𝑤)〉(comp‘𝑆)((1st ‘𝐹)‘𝑤))((𝑧(2nd ‘((1st
‘𝑌)‘𝑋))𝑤)‘ℎ)) = (((𝑧(2nd ‘𝐹)𝑤)‘ℎ)(〈((1st
‘((1st ‘𝑌)‘𝑋))‘𝑧), ((1st ‘𝐹)‘𝑧)〉(comp‘𝑆)((1st ‘𝐹)‘𝑤))(((𝐹𝑁𝑋)‘𝐴)‘𝑧))))) | 
| 181 | 80, 178, 180 | mpbir2and 713 | 1
⊢ (𝜑 → ((𝐹𝑁𝑋)‘𝐴) ∈ (((1st ‘𝑌)‘𝑋)(𝑂 Nat 𝑆)𝐹)) |