| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | invfuc.u | . 2
⊢ (𝜑 → 𝑈 ∈ (𝐹𝑁𝐺)) | 
| 2 |  | invfuc.v | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑈‘𝑥)(((1st ‘𝐹)‘𝑥)𝐽((1st ‘𝐺)‘𝑥))𝑋) | 
| 3 |  | eqid 2736 | . . . . . . . . . 10
⊢
(Base‘𝐷) =
(Base‘𝐷) | 
| 4 |  | fucinv.j | . . . . . . . . . 10
⊢ 𝐽 = (Inv‘𝐷) | 
| 5 |  | fuciso.f | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) | 
| 6 |  | funcrcl 17909 | . . . . . . . . . . . . 13
⊢ (𝐹 ∈ (𝐶 Func 𝐷) → (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat)) | 
| 7 | 5, 6 | syl 17 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat)) | 
| 8 | 7 | simprd 495 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐷 ∈ Cat) | 
| 9 | 8 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐷 ∈ Cat) | 
| 10 |  | fuciso.b | . . . . . . . . . . . 12
⊢ 𝐵 = (Base‘𝐶) | 
| 11 |  | relfunc 17908 | . . . . . . . . . . . . 13
⊢ Rel
(𝐶 Func 𝐷) | 
| 12 |  | 1st2ndbr 8068 | . . . . . . . . . . . . 13
⊢ ((Rel
(𝐶 Func 𝐷) ∧ 𝐹 ∈ (𝐶 Func 𝐷)) → (1st ‘𝐹)(𝐶 Func 𝐷)(2nd ‘𝐹)) | 
| 13 | 11, 5, 12 | sylancr 587 | . . . . . . . . . . . 12
⊢ (𝜑 → (1st
‘𝐹)(𝐶 Func 𝐷)(2nd ‘𝐹)) | 
| 14 | 10, 3, 13 | funcf1 17912 | . . . . . . . . . . 11
⊢ (𝜑 → (1st
‘𝐹):𝐵⟶(Base‘𝐷)) | 
| 15 | 14 | ffvelcdmda 7103 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ((1st ‘𝐹)‘𝑥) ∈ (Base‘𝐷)) | 
| 16 |  | fuciso.g | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐷)) | 
| 17 |  | 1st2ndbr 8068 | . . . . . . . . . . . . 13
⊢ ((Rel
(𝐶 Func 𝐷) ∧ 𝐺 ∈ (𝐶 Func 𝐷)) → (1st ‘𝐺)(𝐶 Func 𝐷)(2nd ‘𝐺)) | 
| 18 | 11, 16, 17 | sylancr 587 | . . . . . . . . . . . 12
⊢ (𝜑 → (1st
‘𝐺)(𝐶 Func 𝐷)(2nd ‘𝐺)) | 
| 19 | 10, 3, 18 | funcf1 17912 | . . . . . . . . . . 11
⊢ (𝜑 → (1st
‘𝐺):𝐵⟶(Base‘𝐷)) | 
| 20 | 19 | ffvelcdmda 7103 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ((1st ‘𝐺)‘𝑥) ∈ (Base‘𝐷)) | 
| 21 |  | eqid 2736 | . . . . . . . . . 10
⊢ (Hom
‘𝐷) = (Hom
‘𝐷) | 
| 22 | 3, 4, 9, 15, 20, 21 | invss 17806 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (((1st ‘𝐹)‘𝑥)𝐽((1st ‘𝐺)‘𝑥)) ⊆ ((((1st ‘𝐹)‘𝑥)(Hom ‘𝐷)((1st ‘𝐺)‘𝑥)) × (((1st ‘𝐺)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑥)))) | 
| 23 | 22 | ssbrd 5185 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ((𝑈‘𝑥)(((1st ‘𝐹)‘𝑥)𝐽((1st ‘𝐺)‘𝑥))𝑋 → (𝑈‘𝑥)((((1st ‘𝐹)‘𝑥)(Hom ‘𝐷)((1st ‘𝐺)‘𝑥)) × (((1st ‘𝐺)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑥)))𝑋)) | 
| 24 | 2, 23 | mpd 15 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑈‘𝑥)((((1st ‘𝐹)‘𝑥)(Hom ‘𝐷)((1st ‘𝐺)‘𝑥)) × (((1st ‘𝐺)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑥)))𝑋) | 
| 25 |  | brxp 5733 | . . . . . . . 8
⊢ ((𝑈‘𝑥)((((1st ‘𝐹)‘𝑥)(Hom ‘𝐷)((1st ‘𝐺)‘𝑥)) × (((1st ‘𝐺)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑥)))𝑋 ↔ ((𝑈‘𝑥) ∈ (((1st ‘𝐹)‘𝑥)(Hom ‘𝐷)((1st ‘𝐺)‘𝑥)) ∧ 𝑋 ∈ (((1st ‘𝐺)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑥)))) | 
| 26 | 25 | simprbi 496 | . . . . . . 7
⊢ ((𝑈‘𝑥)((((1st ‘𝐹)‘𝑥)(Hom ‘𝐷)((1st ‘𝐺)‘𝑥)) × (((1st ‘𝐺)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑥)))𝑋 → 𝑋 ∈ (((1st ‘𝐺)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑥))) | 
| 27 | 24, 26 | syl 17 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑋 ∈ (((1st ‘𝐺)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑥))) | 
| 28 | 27 | ralrimiva 3145 | . . . . 5
⊢ (𝜑 → ∀𝑥 ∈ 𝐵 𝑋 ∈ (((1st ‘𝐺)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑥))) | 
| 29 | 10 | fvexi 6919 | . . . . . 6
⊢ 𝐵 ∈ V | 
| 30 |  | mptelixpg 8976 | . . . . . 6
⊢ (𝐵 ∈ V → ((𝑥 ∈ 𝐵 ↦ 𝑋) ∈ X𝑥 ∈ 𝐵 (((1st ‘𝐺)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑥)) ↔ ∀𝑥 ∈ 𝐵 𝑋 ∈ (((1st ‘𝐺)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑥)))) | 
| 31 | 29, 30 | ax-mp 5 | . . . . 5
⊢ ((𝑥 ∈ 𝐵 ↦ 𝑋) ∈ X𝑥 ∈ 𝐵 (((1st ‘𝐺)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑥)) ↔ ∀𝑥 ∈ 𝐵 𝑋 ∈ (((1st ‘𝐺)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑥))) | 
| 32 | 28, 31 | sylibr 234 | . . . 4
⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ 𝑋) ∈ X𝑥 ∈ 𝐵 (((1st ‘𝐺)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑥))) | 
| 33 |  | fveq2 6905 | . . . . . 6
⊢ (𝑥 = 𝑦 → ((1st ‘𝐺)‘𝑥) = ((1st ‘𝐺)‘𝑦)) | 
| 34 |  | fveq2 6905 | . . . . . 6
⊢ (𝑥 = 𝑦 → ((1st ‘𝐹)‘𝑥) = ((1st ‘𝐹)‘𝑦)) | 
| 35 | 33, 34 | oveq12d 7450 | . . . . 5
⊢ (𝑥 = 𝑦 → (((1st ‘𝐺)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑥)) = (((1st ‘𝐺)‘𝑦)(Hom ‘𝐷)((1st ‘𝐹)‘𝑦))) | 
| 36 | 35 | cbvixpv 8956 | . . . 4
⊢ X𝑥 ∈
𝐵 (((1st
‘𝐺)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑥)) = X𝑦 ∈ 𝐵 (((1st ‘𝐺)‘𝑦)(Hom ‘𝐷)((1st ‘𝐹)‘𝑦)) | 
| 37 | 32, 36 | eleqtrdi 2850 | . . 3
⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ 𝑋) ∈ X𝑦 ∈ 𝐵 (((1st ‘𝐺)‘𝑦)(Hom ‘𝐷)((1st ‘𝐹)‘𝑦))) | 
| 38 |  | simpr2 1195 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 𝑧 ∈ 𝐵) | 
| 39 |  | simpr 484 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐵) | 
| 40 |  | eqid 2736 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ 𝐵 ↦ 𝑋) = (𝑥 ∈ 𝐵 ↦ 𝑋) | 
| 41 | 40 | fvmpt2 7026 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑋 ∈ (((1st ‘𝐺)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑥))) → ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑥) = 𝑋) | 
| 42 | 39, 27, 41 | syl2anc 584 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑥) = 𝑋) | 
| 43 | 2, 42 | breqtrrd 5170 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑈‘𝑥)(((1st ‘𝐹)‘𝑥)𝐽((1st ‘𝐺)‘𝑥))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑥)) | 
| 44 | 43 | ralrimiva 3145 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ∀𝑥 ∈ 𝐵 (𝑈‘𝑥)(((1st ‘𝐹)‘𝑥)𝐽((1st ‘𝐺)‘𝑥))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑥)) | 
| 45 | 44 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ∀𝑥 ∈ 𝐵 (𝑈‘𝑥)(((1st ‘𝐹)‘𝑥)𝐽((1st ‘𝐺)‘𝑥))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑥)) | 
| 46 |  | nfcv 2904 | . . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑥(𝑈‘𝑧) | 
| 47 |  | nfcv 2904 | . . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑥(((1st ‘𝐹)‘𝑧)𝐽((1st ‘𝐺)‘𝑧)) | 
| 48 |  | nffvmpt1 6916 | . . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑥((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧) | 
| 49 | 46, 47, 48 | nfbr 5189 | . . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥(𝑈‘𝑧)(((1st ‘𝐹)‘𝑧)𝐽((1st ‘𝐺)‘𝑧))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧) | 
| 50 |  | fveq2 6905 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑧 → (𝑈‘𝑥) = (𝑈‘𝑧)) | 
| 51 |  | fveq2 6905 | . . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑧 → ((1st ‘𝐹)‘𝑥) = ((1st ‘𝐹)‘𝑧)) | 
| 52 |  | fveq2 6905 | . . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑧 → ((1st ‘𝐺)‘𝑥) = ((1st ‘𝐺)‘𝑧)) | 
| 53 | 51, 52 | oveq12d 7450 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑧 → (((1st ‘𝐹)‘𝑥)𝐽((1st ‘𝐺)‘𝑥)) = (((1st ‘𝐹)‘𝑧)𝐽((1st ‘𝐺)‘𝑧))) | 
| 54 |  | fveq2 6905 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑧 → ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑥) = ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧)) | 
| 55 | 50, 53, 54 | breq123d 5156 | . . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑧 → ((𝑈‘𝑥)(((1st ‘𝐹)‘𝑥)𝐽((1st ‘𝐺)‘𝑥))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑥) ↔ (𝑈‘𝑧)(((1st ‘𝐹)‘𝑧)𝐽((1st ‘𝐺)‘𝑧))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧))) | 
| 56 | 49, 55 | rspc 3609 | . . . . . . . . . . . . . 14
⊢ (𝑧 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 (𝑈‘𝑥)(((1st ‘𝐹)‘𝑥)𝐽((1st ‘𝐺)‘𝑥))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑥) → (𝑈‘𝑧)(((1st ‘𝐹)‘𝑧)𝐽((1st ‘𝐺)‘𝑧))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧))) | 
| 57 | 38, 45, 56 | sylc 65 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (𝑈‘𝑧)(((1st ‘𝐹)‘𝑧)𝐽((1st ‘𝐺)‘𝑧))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧)) | 
| 58 | 8 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 𝐷 ∈ Cat) | 
| 59 | 14 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (1st ‘𝐹):𝐵⟶(Base‘𝐷)) | 
| 60 | 59, 38 | ffvelcdmd 7104 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((1st ‘𝐹)‘𝑧) ∈ (Base‘𝐷)) | 
| 61 | 19 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (1st ‘𝐺):𝐵⟶(Base‘𝐷)) | 
| 62 | 61, 38 | ffvelcdmd 7104 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((1st ‘𝐺)‘𝑧) ∈ (Base‘𝐷)) | 
| 63 |  | eqid 2736 | . . . . . . . . . . . . . 14
⊢
(Sect‘𝐷) =
(Sect‘𝐷) | 
| 64 | 3, 4, 58, 60, 62, 63 | isinv 17805 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑈‘𝑧)(((1st ‘𝐹)‘𝑧)𝐽((1st ‘𝐺)‘𝑧))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧) ↔ ((𝑈‘𝑧)(((1st ‘𝐹)‘𝑧)(Sect‘𝐷)((1st ‘𝐺)‘𝑧))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧) ∧ ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧)(((1st ‘𝐺)‘𝑧)(Sect‘𝐷)((1st ‘𝐹)‘𝑧))(𝑈‘𝑧)))) | 
| 65 | 57, 64 | mpbid 232 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑈‘𝑧)(((1st ‘𝐹)‘𝑧)(Sect‘𝐷)((1st ‘𝐺)‘𝑧))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧) ∧ ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧)(((1st ‘𝐺)‘𝑧)(Sect‘𝐷)((1st ‘𝐹)‘𝑧))(𝑈‘𝑧))) | 
| 66 | 65 | simpld 494 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (𝑈‘𝑧)(((1st ‘𝐹)‘𝑧)(Sect‘𝐷)((1st ‘𝐺)‘𝑧))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧)) | 
| 67 |  | eqid 2736 | . . . . . . . . . . . 12
⊢
(comp‘𝐷) =
(comp‘𝐷) | 
| 68 |  | eqid 2736 | . . . . . . . . . . . 12
⊢
(Id‘𝐷) =
(Id‘𝐷) | 
| 69 | 3, 21, 67, 68, 63, 58, 60, 62 | issect 17798 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑈‘𝑧)(((1st ‘𝐹)‘𝑧)(Sect‘𝐷)((1st ‘𝐺)‘𝑧))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧) ↔ ((𝑈‘𝑧) ∈ (((1st ‘𝐹)‘𝑧)(Hom ‘𝐷)((1st ‘𝐺)‘𝑧)) ∧ ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧) ∈ (((1st ‘𝐺)‘𝑧)(Hom ‘𝐷)((1st ‘𝐹)‘𝑧)) ∧ (((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧)(〈((1st ‘𝐹)‘𝑧), ((1st ‘𝐺)‘𝑧)〉(comp‘𝐷)((1st ‘𝐹)‘𝑧))(𝑈‘𝑧)) = ((Id‘𝐷)‘((1st ‘𝐹)‘𝑧))))) | 
| 70 | 66, 69 | mpbid 232 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑈‘𝑧) ∈ (((1st ‘𝐹)‘𝑧)(Hom ‘𝐷)((1st ‘𝐺)‘𝑧)) ∧ ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧) ∈ (((1st ‘𝐺)‘𝑧)(Hom ‘𝐷)((1st ‘𝐹)‘𝑧)) ∧ (((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧)(〈((1st ‘𝐹)‘𝑧), ((1st ‘𝐺)‘𝑧)〉(comp‘𝐷)((1st ‘𝐹)‘𝑧))(𝑈‘𝑧)) = ((Id‘𝐷)‘((1st ‘𝐹)‘𝑧)))) | 
| 71 | 70 | simp3d 1144 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧)(〈((1st ‘𝐹)‘𝑧), ((1st ‘𝐺)‘𝑧)〉(comp‘𝐷)((1st ‘𝐹)‘𝑧))(𝑈‘𝑧)) = ((Id‘𝐷)‘((1st ‘𝐹)‘𝑧))) | 
| 72 | 71 | oveq1d 7447 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧)(〈((1st ‘𝐹)‘𝑧), ((1st ‘𝐺)‘𝑧)〉(comp‘𝐷)((1st ‘𝐹)‘𝑧))(𝑈‘𝑧))(〈((1st ‘𝐹)‘𝑦), ((1st ‘𝐹)‘𝑧)〉(comp‘𝐷)((1st ‘𝐹)‘𝑧))((𝑦(2nd ‘𝐹)𝑧)‘𝑓)) = (((Id‘𝐷)‘((1st ‘𝐹)‘𝑧))(〈((1st ‘𝐹)‘𝑦), ((1st ‘𝐹)‘𝑧)〉(comp‘𝐷)((1st ‘𝐹)‘𝑧))((𝑦(2nd ‘𝐹)𝑧)‘𝑓))) | 
| 73 |  | simpr1 1194 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 𝑦 ∈ 𝐵) | 
| 74 | 59, 73 | ffvelcdmd 7104 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((1st ‘𝐹)‘𝑦) ∈ (Base‘𝐷)) | 
| 75 |  | eqid 2736 | . . . . . . . . . . 11
⊢ (Hom
‘𝐶) = (Hom
‘𝐶) | 
| 76 | 13 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (1st ‘𝐹)(𝐶 Func 𝐷)(2nd ‘𝐹)) | 
| 77 | 10, 75, 21, 76, 73, 38 | funcf2 17914 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (𝑦(2nd ‘𝐹)𝑧):(𝑦(Hom ‘𝐶)𝑧)⟶(((1st ‘𝐹)‘𝑦)(Hom ‘𝐷)((1st ‘𝐹)‘𝑧))) | 
| 78 |  | simpr3 1196 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧)) | 
| 79 | 77, 78 | ffvelcdmd 7104 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑦(2nd ‘𝐹)𝑧)‘𝑓) ∈ (((1st ‘𝐹)‘𝑦)(Hom ‘𝐷)((1st ‘𝐹)‘𝑧))) | 
| 80 | 3, 21, 68, 58, 74, 67, 60, 79 | catlid 17727 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (((Id‘𝐷)‘((1st ‘𝐹)‘𝑧))(〈((1st ‘𝐹)‘𝑦), ((1st ‘𝐹)‘𝑧)〉(comp‘𝐷)((1st ‘𝐹)‘𝑧))((𝑦(2nd ‘𝐹)𝑧)‘𝑓)) = ((𝑦(2nd ‘𝐹)𝑧)‘𝑓)) | 
| 81 | 72, 80 | eqtr2d 2777 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑦(2nd ‘𝐹)𝑧)‘𝑓) = ((((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧)(〈((1st ‘𝐹)‘𝑧), ((1st ‘𝐺)‘𝑧)〉(comp‘𝐷)((1st ‘𝐹)‘𝑧))(𝑈‘𝑧))(〈((1st ‘𝐹)‘𝑦), ((1st ‘𝐹)‘𝑧)〉(comp‘𝐷)((1st ‘𝐹)‘𝑧))((𝑦(2nd ‘𝐹)𝑧)‘𝑓))) | 
| 82 |  | fuciso.n | . . . . . . . . 9
⊢ 𝑁 = (𝐶 Nat 𝐷) | 
| 83 | 1 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 𝑈 ∈ (𝐹𝑁𝐺)) | 
| 84 | 82, 83 | nat1st2nd 18000 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 𝑈 ∈ (〈(1st ‘𝐹), (2nd ‘𝐹)〉𝑁〈(1st ‘𝐺), (2nd ‘𝐺)〉)) | 
| 85 | 82, 84, 10, 21, 38 | natcl 18002 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (𝑈‘𝑧) ∈ (((1st ‘𝐹)‘𝑧)(Hom ‘𝐷)((1st ‘𝐺)‘𝑧))) | 
| 86 | 70 | simp2d 1143 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧) ∈ (((1st ‘𝐺)‘𝑧)(Hom ‘𝐷)((1st ‘𝐹)‘𝑧))) | 
| 87 | 3, 21, 67, 58, 74, 60, 62, 79, 85, 60, 86 | catass 17730 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧)(〈((1st ‘𝐹)‘𝑧), ((1st ‘𝐺)‘𝑧)〉(comp‘𝐷)((1st ‘𝐹)‘𝑧))(𝑈‘𝑧))(〈((1st ‘𝐹)‘𝑦), ((1st ‘𝐹)‘𝑧)〉(comp‘𝐷)((1st ‘𝐹)‘𝑧))((𝑦(2nd ‘𝐹)𝑧)‘𝑓)) = (((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧)(〈((1st ‘𝐹)‘𝑦), ((1st ‘𝐺)‘𝑧)〉(comp‘𝐷)((1st ‘𝐹)‘𝑧))((𝑈‘𝑧)(〈((1st ‘𝐹)‘𝑦), ((1st ‘𝐹)‘𝑧)〉(comp‘𝐷)((1st ‘𝐺)‘𝑧))((𝑦(2nd ‘𝐹)𝑧)‘𝑓)))) | 
| 88 | 82, 84, 10, 75, 67, 73, 38, 78 | nati 18004 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑈‘𝑧)(〈((1st ‘𝐹)‘𝑦), ((1st ‘𝐹)‘𝑧)〉(comp‘𝐷)((1st ‘𝐺)‘𝑧))((𝑦(2nd ‘𝐹)𝑧)‘𝑓)) = (((𝑦(2nd ‘𝐺)𝑧)‘𝑓)(〈((1st ‘𝐹)‘𝑦), ((1st ‘𝐺)‘𝑦)〉(comp‘𝐷)((1st ‘𝐺)‘𝑧))(𝑈‘𝑦))) | 
| 89 | 88 | oveq2d 7448 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧)(〈((1st ‘𝐹)‘𝑦), ((1st ‘𝐺)‘𝑧)〉(comp‘𝐷)((1st ‘𝐹)‘𝑧))((𝑈‘𝑧)(〈((1st ‘𝐹)‘𝑦), ((1st ‘𝐹)‘𝑧)〉(comp‘𝐷)((1st ‘𝐺)‘𝑧))((𝑦(2nd ‘𝐹)𝑧)‘𝑓))) = (((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧)(〈((1st ‘𝐹)‘𝑦), ((1st ‘𝐺)‘𝑧)〉(comp‘𝐷)((1st ‘𝐹)‘𝑧))(((𝑦(2nd ‘𝐺)𝑧)‘𝑓)(〈((1st ‘𝐹)‘𝑦), ((1st ‘𝐺)‘𝑦)〉(comp‘𝐷)((1st ‘𝐺)‘𝑧))(𝑈‘𝑦)))) | 
| 90 | 81, 87, 89 | 3eqtrd 2780 | . . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑦(2nd ‘𝐹)𝑧)‘𝑓) = (((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧)(〈((1st ‘𝐹)‘𝑦), ((1st ‘𝐺)‘𝑧)〉(comp‘𝐷)((1st ‘𝐹)‘𝑧))(((𝑦(2nd ‘𝐺)𝑧)‘𝑓)(〈((1st ‘𝐹)‘𝑦), ((1st ‘𝐺)‘𝑦)〉(comp‘𝐷)((1st ‘𝐺)‘𝑧))(𝑈‘𝑦)))) | 
| 91 | 90 | oveq1d 7447 | . . . . 5
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (((𝑦(2nd ‘𝐹)𝑧)‘𝑓)(〈((1st ‘𝐺)‘𝑦), ((1st ‘𝐹)‘𝑦)〉(comp‘𝐷)((1st ‘𝐹)‘𝑧))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦)) = ((((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧)(〈((1st ‘𝐹)‘𝑦), ((1st ‘𝐺)‘𝑧)〉(comp‘𝐷)((1st ‘𝐹)‘𝑧))(((𝑦(2nd ‘𝐺)𝑧)‘𝑓)(〈((1st ‘𝐹)‘𝑦), ((1st ‘𝐺)‘𝑦)〉(comp‘𝐷)((1st ‘𝐺)‘𝑧))(𝑈‘𝑦)))(〈((1st ‘𝐺)‘𝑦), ((1st ‘𝐹)‘𝑦)〉(comp‘𝐷)((1st ‘𝐹)‘𝑧))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦))) | 
| 92 | 61, 73 | ffvelcdmd 7104 | . . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((1st ‘𝐺)‘𝑦) ∈ (Base‘𝐷)) | 
| 93 |  | nfcv 2904 | . . . . . . . . . . . . 13
⊢
Ⅎ𝑥(𝑈‘𝑦) | 
| 94 |  | nfcv 2904 | . . . . . . . . . . . . 13
⊢
Ⅎ𝑥(((1st ‘𝐹)‘𝑦)𝐽((1st ‘𝐺)‘𝑦)) | 
| 95 |  | nffvmpt1 6916 | . . . . . . . . . . . . 13
⊢
Ⅎ𝑥((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦) | 
| 96 | 93, 94, 95 | nfbr 5189 | . . . . . . . . . . . 12
⊢
Ⅎ𝑥(𝑈‘𝑦)(((1st ‘𝐹)‘𝑦)𝐽((1st ‘𝐺)‘𝑦))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦) | 
| 97 |  | fveq2 6905 | . . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → (𝑈‘𝑥) = (𝑈‘𝑦)) | 
| 98 | 34, 33 | oveq12d 7450 | . . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → (((1st ‘𝐹)‘𝑥)𝐽((1st ‘𝐺)‘𝑥)) = (((1st ‘𝐹)‘𝑦)𝐽((1st ‘𝐺)‘𝑦))) | 
| 99 |  | fveq2 6905 | . . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑥) = ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦)) | 
| 100 | 97, 98, 99 | breq123d 5156 | . . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → ((𝑈‘𝑥)(((1st ‘𝐹)‘𝑥)𝐽((1st ‘𝐺)‘𝑥))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑥) ↔ (𝑈‘𝑦)(((1st ‘𝐹)‘𝑦)𝐽((1st ‘𝐺)‘𝑦))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦))) | 
| 101 | 96, 100 | rspc 3609 | . . . . . . . . . . 11
⊢ (𝑦 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 (𝑈‘𝑥)(((1st ‘𝐹)‘𝑥)𝐽((1st ‘𝐺)‘𝑥))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑥) → (𝑈‘𝑦)(((1st ‘𝐹)‘𝑦)𝐽((1st ‘𝐺)‘𝑦))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦))) | 
| 102 | 73, 45, 101 | sylc 65 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (𝑈‘𝑦)(((1st ‘𝐹)‘𝑦)𝐽((1st ‘𝐺)‘𝑦))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦)) | 
| 103 | 3, 4, 58, 74, 92, 63 | isinv 17805 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑈‘𝑦)(((1st ‘𝐹)‘𝑦)𝐽((1st ‘𝐺)‘𝑦))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦) ↔ ((𝑈‘𝑦)(((1st ‘𝐹)‘𝑦)(Sect‘𝐷)((1st ‘𝐺)‘𝑦))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦) ∧ ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦)(((1st ‘𝐺)‘𝑦)(Sect‘𝐷)((1st ‘𝐹)‘𝑦))(𝑈‘𝑦)))) | 
| 104 | 102, 103 | mpbid 232 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑈‘𝑦)(((1st ‘𝐹)‘𝑦)(Sect‘𝐷)((1st ‘𝐺)‘𝑦))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦) ∧ ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦)(((1st ‘𝐺)‘𝑦)(Sect‘𝐷)((1st ‘𝐹)‘𝑦))(𝑈‘𝑦))) | 
| 105 | 104 | simprd 495 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦)(((1st ‘𝐺)‘𝑦)(Sect‘𝐷)((1st ‘𝐹)‘𝑦))(𝑈‘𝑦)) | 
| 106 | 3, 21, 67, 68, 63, 58, 92, 74 | issect 17798 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦)(((1st ‘𝐺)‘𝑦)(Sect‘𝐷)((1st ‘𝐹)‘𝑦))(𝑈‘𝑦) ↔ (((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦) ∈ (((1st ‘𝐺)‘𝑦)(Hom ‘𝐷)((1st ‘𝐹)‘𝑦)) ∧ (𝑈‘𝑦) ∈ (((1st ‘𝐹)‘𝑦)(Hom ‘𝐷)((1st ‘𝐺)‘𝑦)) ∧ ((𝑈‘𝑦)(〈((1st ‘𝐺)‘𝑦), ((1st ‘𝐹)‘𝑦)〉(comp‘𝐷)((1st ‘𝐺)‘𝑦))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦)) = ((Id‘𝐷)‘((1st ‘𝐺)‘𝑦))))) | 
| 107 | 105, 106 | mpbid 232 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦) ∈ (((1st ‘𝐺)‘𝑦)(Hom ‘𝐷)((1st ‘𝐹)‘𝑦)) ∧ (𝑈‘𝑦) ∈ (((1st ‘𝐹)‘𝑦)(Hom ‘𝐷)((1st ‘𝐺)‘𝑦)) ∧ ((𝑈‘𝑦)(〈((1st ‘𝐺)‘𝑦), ((1st ‘𝐹)‘𝑦)〉(comp‘𝐷)((1st ‘𝐺)‘𝑦))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦)) = ((Id‘𝐷)‘((1st ‘𝐺)‘𝑦)))) | 
| 108 | 107 | simp1d 1142 | . . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦) ∈ (((1st ‘𝐺)‘𝑦)(Hom ‘𝐷)((1st ‘𝐹)‘𝑦))) | 
| 109 | 107 | simp2d 1143 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (𝑈‘𝑦) ∈ (((1st ‘𝐹)‘𝑦)(Hom ‘𝐷)((1st ‘𝐺)‘𝑦))) | 
| 110 | 18 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (1st ‘𝐺)(𝐶 Func 𝐷)(2nd ‘𝐺)) | 
| 111 | 10, 75, 21, 110, 73, 38 | funcf2 17914 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (𝑦(2nd ‘𝐺)𝑧):(𝑦(Hom ‘𝐶)𝑧)⟶(((1st ‘𝐺)‘𝑦)(Hom ‘𝐷)((1st ‘𝐺)‘𝑧))) | 
| 112 | 111, 78 | ffvelcdmd 7104 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑦(2nd ‘𝐺)𝑧)‘𝑓) ∈ (((1st ‘𝐺)‘𝑦)(Hom ‘𝐷)((1st ‘𝐺)‘𝑧))) | 
| 113 | 3, 21, 67, 58, 74, 92, 62, 109, 112 | catcocl 17729 | . . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (((𝑦(2nd ‘𝐺)𝑧)‘𝑓)(〈((1st ‘𝐹)‘𝑦), ((1st ‘𝐺)‘𝑦)〉(comp‘𝐷)((1st ‘𝐺)‘𝑧))(𝑈‘𝑦)) ∈ (((1st ‘𝐹)‘𝑦)(Hom ‘𝐷)((1st ‘𝐺)‘𝑧))) | 
| 114 | 3, 21, 67, 58, 92, 74, 62, 108, 113, 60, 86 | catass 17730 | . . . . 5
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧)(〈((1st ‘𝐹)‘𝑦), ((1st ‘𝐺)‘𝑧)〉(comp‘𝐷)((1st ‘𝐹)‘𝑧))(((𝑦(2nd ‘𝐺)𝑧)‘𝑓)(〈((1st ‘𝐹)‘𝑦), ((1st ‘𝐺)‘𝑦)〉(comp‘𝐷)((1st ‘𝐺)‘𝑧))(𝑈‘𝑦)))(〈((1st ‘𝐺)‘𝑦), ((1st ‘𝐹)‘𝑦)〉(comp‘𝐷)((1st ‘𝐹)‘𝑧))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦)) = (((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧)(〈((1st ‘𝐺)‘𝑦), ((1st ‘𝐺)‘𝑧)〉(comp‘𝐷)((1st ‘𝐹)‘𝑧))((((𝑦(2nd ‘𝐺)𝑧)‘𝑓)(〈((1st ‘𝐹)‘𝑦), ((1st ‘𝐺)‘𝑦)〉(comp‘𝐷)((1st ‘𝐺)‘𝑧))(𝑈‘𝑦))(〈((1st ‘𝐺)‘𝑦), ((1st ‘𝐹)‘𝑦)〉(comp‘𝐷)((1st ‘𝐺)‘𝑧))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦)))) | 
| 115 | 82, 84, 10, 21, 73 | natcl 18002 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (𝑈‘𝑦) ∈ (((1st ‘𝐹)‘𝑦)(Hom ‘𝐷)((1st ‘𝐺)‘𝑦))) | 
| 116 | 3, 21, 67, 58, 92, 74, 92, 108, 115, 62, 112 | catass 17730 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((((𝑦(2nd ‘𝐺)𝑧)‘𝑓)(〈((1st ‘𝐹)‘𝑦), ((1st ‘𝐺)‘𝑦)〉(comp‘𝐷)((1st ‘𝐺)‘𝑧))(𝑈‘𝑦))(〈((1st ‘𝐺)‘𝑦), ((1st ‘𝐹)‘𝑦)〉(comp‘𝐷)((1st ‘𝐺)‘𝑧))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦)) = (((𝑦(2nd ‘𝐺)𝑧)‘𝑓)(〈((1st ‘𝐺)‘𝑦), ((1st ‘𝐺)‘𝑦)〉(comp‘𝐷)((1st ‘𝐺)‘𝑧))((𝑈‘𝑦)(〈((1st ‘𝐺)‘𝑦), ((1st ‘𝐹)‘𝑦)〉(comp‘𝐷)((1st ‘𝐺)‘𝑦))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦)))) | 
| 117 | 107 | simp3d 1144 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑈‘𝑦)(〈((1st ‘𝐺)‘𝑦), ((1st ‘𝐹)‘𝑦)〉(comp‘𝐷)((1st ‘𝐺)‘𝑦))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦)) = ((Id‘𝐷)‘((1st ‘𝐺)‘𝑦))) | 
| 118 | 117 | oveq2d 7448 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (((𝑦(2nd ‘𝐺)𝑧)‘𝑓)(〈((1st ‘𝐺)‘𝑦), ((1st ‘𝐺)‘𝑦)〉(comp‘𝐷)((1st ‘𝐺)‘𝑧))((𝑈‘𝑦)(〈((1st ‘𝐺)‘𝑦), ((1st ‘𝐹)‘𝑦)〉(comp‘𝐷)((1st ‘𝐺)‘𝑦))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦))) = (((𝑦(2nd ‘𝐺)𝑧)‘𝑓)(〈((1st ‘𝐺)‘𝑦), ((1st ‘𝐺)‘𝑦)〉(comp‘𝐷)((1st ‘𝐺)‘𝑧))((Id‘𝐷)‘((1st ‘𝐺)‘𝑦)))) | 
| 119 | 3, 21, 68, 58, 92, 67, 62, 112 | catrid 17728 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (((𝑦(2nd ‘𝐺)𝑧)‘𝑓)(〈((1st ‘𝐺)‘𝑦), ((1st ‘𝐺)‘𝑦)〉(comp‘𝐷)((1st ‘𝐺)‘𝑧))((Id‘𝐷)‘((1st ‘𝐺)‘𝑦))) = ((𝑦(2nd ‘𝐺)𝑧)‘𝑓)) | 
| 120 | 116, 118,
119 | 3eqtrd 2780 | . . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((((𝑦(2nd ‘𝐺)𝑧)‘𝑓)(〈((1st ‘𝐹)‘𝑦), ((1st ‘𝐺)‘𝑦)〉(comp‘𝐷)((1st ‘𝐺)‘𝑧))(𝑈‘𝑦))(〈((1st ‘𝐺)‘𝑦), ((1st ‘𝐹)‘𝑦)〉(comp‘𝐷)((1st ‘𝐺)‘𝑧))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦)) = ((𝑦(2nd ‘𝐺)𝑧)‘𝑓)) | 
| 121 | 120 | oveq2d 7448 | . . . . 5
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧)(〈((1st ‘𝐺)‘𝑦), ((1st ‘𝐺)‘𝑧)〉(comp‘𝐷)((1st ‘𝐹)‘𝑧))((((𝑦(2nd ‘𝐺)𝑧)‘𝑓)(〈((1st ‘𝐹)‘𝑦), ((1st ‘𝐺)‘𝑦)〉(comp‘𝐷)((1st ‘𝐺)‘𝑧))(𝑈‘𝑦))(〈((1st ‘𝐺)‘𝑦), ((1st ‘𝐹)‘𝑦)〉(comp‘𝐷)((1st ‘𝐺)‘𝑧))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦))) = (((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧)(〈((1st ‘𝐺)‘𝑦), ((1st ‘𝐺)‘𝑧)〉(comp‘𝐷)((1st ‘𝐹)‘𝑧))((𝑦(2nd ‘𝐺)𝑧)‘𝑓))) | 
| 122 | 91, 114, 121 | 3eqtrrd 2781 | . . . 4
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧)(〈((1st ‘𝐺)‘𝑦), ((1st ‘𝐺)‘𝑧)〉(comp‘𝐷)((1st ‘𝐹)‘𝑧))((𝑦(2nd ‘𝐺)𝑧)‘𝑓)) = (((𝑦(2nd ‘𝐹)𝑧)‘𝑓)(〈((1st ‘𝐺)‘𝑦), ((1st ‘𝐹)‘𝑦)〉(comp‘𝐷)((1st ‘𝐹)‘𝑧))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦))) | 
| 123 | 122 | ralrimivvva 3204 | . . 3
⊢ (𝜑 → ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧)(((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧)(〈((1st ‘𝐺)‘𝑦), ((1st ‘𝐺)‘𝑧)〉(comp‘𝐷)((1st ‘𝐹)‘𝑧))((𝑦(2nd ‘𝐺)𝑧)‘𝑓)) = (((𝑦(2nd ‘𝐹)𝑧)‘𝑓)(〈((1st ‘𝐺)‘𝑦), ((1st ‘𝐹)‘𝑦)〉(comp‘𝐷)((1st ‘𝐹)‘𝑧))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦))) | 
| 124 | 82, 10, 75, 21, 67, 16, 5 | isnat2 17997 | . . 3
⊢ (𝜑 → ((𝑥 ∈ 𝐵 ↦ 𝑋) ∈ (𝐺𝑁𝐹) ↔ ((𝑥 ∈ 𝐵 ↦ 𝑋) ∈ X𝑦 ∈ 𝐵 (((1st ‘𝐺)‘𝑦)(Hom ‘𝐷)((1st ‘𝐹)‘𝑦)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑧)(((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑧)(〈((1st ‘𝐺)‘𝑦), ((1st ‘𝐺)‘𝑧)〉(comp‘𝐷)((1st ‘𝐹)‘𝑧))((𝑦(2nd ‘𝐺)𝑧)‘𝑓)) = (((𝑦(2nd ‘𝐹)𝑧)‘𝑓)(〈((1st ‘𝐺)‘𝑦), ((1st ‘𝐹)‘𝑦)〉(comp‘𝐷)((1st ‘𝐹)‘𝑧))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦))))) | 
| 125 | 37, 123, 124 | mpbir2and 713 | . 2
⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ 𝑋) ∈ (𝐺𝑁𝐹)) | 
| 126 |  | nfv 1913 | . . . 4
⊢
Ⅎ𝑦(𝑈‘𝑥)(((1st ‘𝐹)‘𝑥)𝐽((1st ‘𝐺)‘𝑥))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑥) | 
| 127 | 126, 96, 100 | cbvralw 3305 | . . 3
⊢
(∀𝑥 ∈
𝐵 (𝑈‘𝑥)(((1st ‘𝐹)‘𝑥)𝐽((1st ‘𝐺)‘𝑥))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑥) ↔ ∀𝑦 ∈ 𝐵 (𝑈‘𝑦)(((1st ‘𝐹)‘𝑦)𝐽((1st ‘𝐺)‘𝑦))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦)) | 
| 128 | 44, 127 | sylib 218 | . 2
⊢ (𝜑 → ∀𝑦 ∈ 𝐵 (𝑈‘𝑦)(((1st ‘𝐹)‘𝑦)𝐽((1st ‘𝐺)‘𝑦))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦)) | 
| 129 |  | fuciso.q | . . 3
⊢ 𝑄 = (𝐶 FuncCat 𝐷) | 
| 130 |  | fucinv.i | . . 3
⊢ 𝐼 = (Inv‘𝑄) | 
| 131 | 129, 10, 82, 5, 16, 130, 4 | fucinv 18022 | . 2
⊢ (𝜑 → (𝑈(𝐹𝐼𝐺)(𝑥 ∈ 𝐵 ↦ 𝑋) ↔ (𝑈 ∈ (𝐹𝑁𝐺) ∧ (𝑥 ∈ 𝐵 ↦ 𝑋) ∈ (𝐺𝑁𝐹) ∧ ∀𝑦 ∈ 𝐵 (𝑈‘𝑦)(((1st ‘𝐹)‘𝑦)𝐽((1st ‘𝐺)‘𝑦))((𝑥 ∈ 𝐵 ↦ 𝑋)‘𝑦)))) | 
| 132 | 1, 125, 128, 131 | mpbir3and 1342 | 1
⊢ (𝜑 → 𝑈(𝐹𝐼𝐺)(𝑥 ∈ 𝐵 ↦ 𝑋)) |