| Step | Hyp | Ref
| Expression |
| 1 | | catcxpccl.o |
. . . . 5
⊢ 𝑇 = (𝑋 ×c 𝑌) |
| 2 | | eqid 2737 |
. . . . 5
⊢
(Base‘𝑋) =
(Base‘𝑋) |
| 3 | | eqid 2737 |
. . . . 5
⊢
(Base‘𝑌) =
(Base‘𝑌) |
| 4 | | eqid 2737 |
. . . . 5
⊢ (Hom
‘𝑋) = (Hom
‘𝑋) |
| 5 | | eqid 2737 |
. . . . 5
⊢ (Hom
‘𝑌) = (Hom
‘𝑌) |
| 6 | | eqid 2737 |
. . . . 5
⊢
(comp‘𝑋) =
(comp‘𝑋) |
| 7 | | eqid 2737 |
. . . . 5
⊢
(comp‘𝑌) =
(comp‘𝑌) |
| 8 | | catcxpccl.x |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
| 9 | | catcxpccl.y |
. . . . 5
⊢ (𝜑 → 𝑌 ∈ 𝐵) |
| 10 | | eqidd 2738 |
. . . . 5
⊢ (𝜑 → ((Base‘𝑋) × (Base‘𝑌)) = ((Base‘𝑋) × (Base‘𝑌))) |
| 11 | 1, 2, 3 | xpcbas 18223 |
. . . . . . 7
⊢
((Base‘𝑋)
× (Base‘𝑌)) =
(Base‘𝑇) |
| 12 | | eqid 2737 |
. . . . . . 7
⊢ (Hom
‘𝑇) = (Hom
‘𝑇) |
| 13 | 1, 11, 4, 5, 12 | xpchomfval 18224 |
. . . . . 6
⊢ (Hom
‘𝑇) = (𝑢 ∈ ((Base‘𝑋) × (Base‘𝑌)), 𝑣 ∈ ((Base‘𝑋) × (Base‘𝑌)) ↦ (((1st ‘𝑢)(Hom ‘𝑋)(1st ‘𝑣)) × ((2nd ‘𝑢)(Hom ‘𝑌)(2nd ‘𝑣)))) |
| 14 | 13 | a1i 11 |
. . . . 5
⊢ (𝜑 → (Hom ‘𝑇) = (𝑢 ∈ ((Base‘𝑋) × (Base‘𝑌)), 𝑣 ∈ ((Base‘𝑋) × (Base‘𝑌)) ↦ (((1st ‘𝑢)(Hom ‘𝑋)(1st ‘𝑣)) × ((2nd ‘𝑢)(Hom ‘𝑌)(2nd ‘𝑣))))) |
| 15 | | eqidd 2738 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (((Base‘𝑋) × (Base‘𝑌)) × ((Base‘𝑋) × (Base‘𝑌))), 𝑦 ∈ ((Base‘𝑋) × (Base‘𝑌)) ↦ (𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝑇)𝑦), 𝑓 ∈ ((Hom ‘𝑇)‘𝑥) ↦ 〈((1st ‘𝑔)(〈(1st
‘(1st ‘𝑥)), (1st ‘(2nd
‘𝑥))〉(comp‘𝑋)(1st ‘𝑦))(1st ‘𝑓)), ((2nd ‘𝑔)(〈(2nd
‘(1st ‘𝑥)), (2nd ‘(2nd
‘𝑥))〉(comp‘𝑌)(2nd ‘𝑦))(2nd ‘𝑓))〉)) = (𝑥 ∈ (((Base‘𝑋) × (Base‘𝑌)) × ((Base‘𝑋) × (Base‘𝑌))), 𝑦 ∈ ((Base‘𝑋) × (Base‘𝑌)) ↦ (𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝑇)𝑦), 𝑓 ∈ ((Hom ‘𝑇)‘𝑥) ↦ 〈((1st ‘𝑔)(〈(1st
‘(1st ‘𝑥)), (1st ‘(2nd
‘𝑥))〉(comp‘𝑋)(1st ‘𝑦))(1st ‘𝑓)), ((2nd ‘𝑔)(〈(2nd
‘(1st ‘𝑥)), (2nd ‘(2nd
‘𝑥))〉(comp‘𝑌)(2nd ‘𝑦))(2nd ‘𝑓))〉))) |
| 16 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
14, 15 | xpcval 18222 |
. . . 4
⊢ (𝜑 → 𝑇 = {〈(Base‘ndx),
((Base‘𝑋) ×
(Base‘𝑌))〉,
〈(Hom ‘ndx), (Hom ‘𝑇)〉, 〈(comp‘ndx), (𝑥 ∈ (((Base‘𝑋) × (Base‘𝑌)) × ((Base‘𝑋) × (Base‘𝑌))), 𝑦 ∈ ((Base‘𝑋) × (Base‘𝑌)) ↦ (𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝑇)𝑦), 𝑓 ∈ ((Hom ‘𝑇)‘𝑥) ↦ 〈((1st ‘𝑔)(〈(1st
‘(1st ‘𝑥)), (1st ‘(2nd
‘𝑥))〉(comp‘𝑋)(1st ‘𝑦))(1st ‘𝑓)), ((2nd ‘𝑔)(〈(2nd
‘(1st ‘𝑥)), (2nd ‘(2nd
‘𝑥))〉(comp‘𝑌)(2nd ‘𝑦))(2nd ‘𝑓))〉))〉}) |
| 17 | | catcxpccl.u |
. . . . 5
⊢ (𝜑 → 𝑈 ∈ WUni) |
| 18 | | baseid 17250 |
. . . . . . 7
⊢ Base =
Slot (Base‘ndx) |
| 19 | | catcxpccl.1 |
. . . . . . . 8
⊢ (𝜑 → ω ∈ 𝑈) |
| 20 | 17, 19 | wunndx 17232 |
. . . . . . 7
⊢ (𝜑 → ndx ∈ 𝑈) |
| 21 | 18, 17, 20 | wunstr 17225 |
. . . . . 6
⊢ (𝜑 → (Base‘ndx) ∈
𝑈) |
| 22 | | catcxpccl.c |
. . . . . . . 8
⊢ 𝐶 = (CatCat‘𝑈) |
| 23 | | catcxpccl.b |
. . . . . . . 8
⊢ 𝐵 = (Base‘𝐶) |
| 24 | 22, 23, 17, 8 | catcbaselcl 18159 |
. . . . . . 7
⊢ (𝜑 → (Base‘𝑋) ∈ 𝑈) |
| 25 | 22, 23, 17, 9 | catcbaselcl 18159 |
. . . . . . 7
⊢ (𝜑 → (Base‘𝑌) ∈ 𝑈) |
| 26 | 17, 24, 25 | wunxp 10764 |
. . . . . 6
⊢ (𝜑 → ((Base‘𝑋) × (Base‘𝑌)) ∈ 𝑈) |
| 27 | 17, 21, 26 | wunop 10762 |
. . . . 5
⊢ (𝜑 → 〈(Base‘ndx),
((Base‘𝑋) ×
(Base‘𝑌))〉
∈ 𝑈) |
| 28 | | homid 17456 |
. . . . . . 7
⊢ Hom =
Slot (Hom ‘ndx) |
| 29 | 28, 17, 20 | wunstr 17225 |
. . . . . 6
⊢ (𝜑 → (Hom ‘ndx) ∈
𝑈) |
| 30 | 17, 26, 26 | wunxp 10764 |
. . . . . . . 8
⊢ (𝜑 → (((Base‘𝑋) × (Base‘𝑌)) × ((Base‘𝑋) × (Base‘𝑌))) ∈ 𝑈) |
| 31 | 22, 23, 17, 8 | catchomcl 18160 |
. . . . . . . . . . . 12
⊢ (𝜑 → (Hom ‘𝑋) ∈ 𝑈) |
| 32 | 17, 31 | wunrn 10769 |
. . . . . . . . . . 11
⊢ (𝜑 → ran (Hom ‘𝑋) ∈ 𝑈) |
| 33 | 17, 32 | wununi 10746 |
. . . . . . . . . 10
⊢ (𝜑 → ∪ ran (Hom ‘𝑋) ∈ 𝑈) |
| 34 | 22, 23, 17, 9 | catchomcl 18160 |
. . . . . . . . . . . 12
⊢ (𝜑 → (Hom ‘𝑌) ∈ 𝑈) |
| 35 | 17, 34 | wunrn 10769 |
. . . . . . . . . . 11
⊢ (𝜑 → ran (Hom ‘𝑌) ∈ 𝑈) |
| 36 | 17, 35 | wununi 10746 |
. . . . . . . . . 10
⊢ (𝜑 → ∪ ran (Hom ‘𝑌) ∈ 𝑈) |
| 37 | 17, 33, 36 | wunxp 10764 |
. . . . . . . . 9
⊢ (𝜑 → (∪ ran (Hom ‘𝑋) × ∪ ran
(Hom ‘𝑌)) ∈
𝑈) |
| 38 | 17, 37 | wunpw 10747 |
. . . . . . . 8
⊢ (𝜑 → 𝒫 (∪ ran (Hom ‘𝑋) × ∪ ran
(Hom ‘𝑌)) ∈
𝑈) |
| 39 | | ovssunirn 7467 |
. . . . . . . . . . . . 13
⊢
((1st ‘𝑢)(Hom ‘𝑋)(1st ‘𝑣)) ⊆ ∪ ran
(Hom ‘𝑋) |
| 40 | | ovssunirn 7467 |
. . . . . . . . . . . . 13
⊢
((2nd ‘𝑢)(Hom ‘𝑌)(2nd ‘𝑣)) ⊆ ∪ ran
(Hom ‘𝑌) |
| 41 | | xpss12 5700 |
. . . . . . . . . . . . 13
⊢
((((1st ‘𝑢)(Hom ‘𝑋)(1st ‘𝑣)) ⊆ ∪ ran
(Hom ‘𝑋) ∧
((2nd ‘𝑢)(Hom ‘𝑌)(2nd ‘𝑣)) ⊆ ∪ ran
(Hom ‘𝑌)) →
(((1st ‘𝑢)(Hom ‘𝑋)(1st ‘𝑣)) × ((2nd ‘𝑢)(Hom ‘𝑌)(2nd ‘𝑣))) ⊆ (∪ ran
(Hom ‘𝑋) ×
∪ ran (Hom ‘𝑌))) |
| 42 | 39, 40, 41 | mp2an 692 |
. . . . . . . . . . . 12
⊢
(((1st ‘𝑢)(Hom ‘𝑋)(1st ‘𝑣)) × ((2nd ‘𝑢)(Hom ‘𝑌)(2nd ‘𝑣))) ⊆ (∪ ran
(Hom ‘𝑋) ×
∪ ran (Hom ‘𝑌)) |
| 43 | | ovex 7464 |
. . . . . . . . . . . . . 14
⊢
((1st ‘𝑢)(Hom ‘𝑋)(1st ‘𝑣)) ∈ V |
| 44 | | ovex 7464 |
. . . . . . . . . . . . . 14
⊢
((2nd ‘𝑢)(Hom ‘𝑌)(2nd ‘𝑣)) ∈ V |
| 45 | 43, 44 | xpex 7773 |
. . . . . . . . . . . . 13
⊢
(((1st ‘𝑢)(Hom ‘𝑋)(1st ‘𝑣)) × ((2nd ‘𝑢)(Hom ‘𝑌)(2nd ‘𝑣))) ∈ V |
| 46 | 45 | elpw 4604 |
. . . . . . . . . . . 12
⊢
((((1st ‘𝑢)(Hom ‘𝑋)(1st ‘𝑣)) × ((2nd ‘𝑢)(Hom ‘𝑌)(2nd ‘𝑣))) ∈ 𝒫 (∪ ran (Hom ‘𝑋) × ∪ ran
(Hom ‘𝑌)) ↔
(((1st ‘𝑢)(Hom ‘𝑋)(1st ‘𝑣)) × ((2nd ‘𝑢)(Hom ‘𝑌)(2nd ‘𝑣))) ⊆ (∪ ran
(Hom ‘𝑋) ×
∪ ran (Hom ‘𝑌))) |
| 47 | 42, 46 | mpbir 231 |
. . . . . . . . . . 11
⊢
(((1st ‘𝑢)(Hom ‘𝑋)(1st ‘𝑣)) × ((2nd ‘𝑢)(Hom ‘𝑌)(2nd ‘𝑣))) ∈ 𝒫 (∪ ran (Hom ‘𝑋) × ∪ ran
(Hom ‘𝑌)) |
| 48 | 47 | rgen2w 3066 |
. . . . . . . . . 10
⊢
∀𝑢 ∈
((Base‘𝑋) ×
(Base‘𝑌))∀𝑣 ∈ ((Base‘𝑋) × (Base‘𝑌))(((1st ‘𝑢)(Hom ‘𝑋)(1st ‘𝑣)) × ((2nd ‘𝑢)(Hom ‘𝑌)(2nd ‘𝑣))) ∈ 𝒫 (∪ ran (Hom ‘𝑋) × ∪ ran
(Hom ‘𝑌)) |
| 49 | | eqid 2737 |
. . . . . . . . . . 11
⊢ (𝑢 ∈ ((Base‘𝑋) × (Base‘𝑌)), 𝑣 ∈ ((Base‘𝑋) × (Base‘𝑌)) ↦ (((1st ‘𝑢)(Hom ‘𝑋)(1st ‘𝑣)) × ((2nd ‘𝑢)(Hom ‘𝑌)(2nd ‘𝑣)))) = (𝑢 ∈ ((Base‘𝑋) × (Base‘𝑌)), 𝑣 ∈ ((Base‘𝑋) × (Base‘𝑌)) ↦ (((1st ‘𝑢)(Hom ‘𝑋)(1st ‘𝑣)) × ((2nd ‘𝑢)(Hom ‘𝑌)(2nd ‘𝑣)))) |
| 50 | 49 | fmpo 8093 |
. . . . . . . . . 10
⊢
(∀𝑢 ∈
((Base‘𝑋) ×
(Base‘𝑌))∀𝑣 ∈ ((Base‘𝑋) × (Base‘𝑌))(((1st ‘𝑢)(Hom ‘𝑋)(1st ‘𝑣)) × ((2nd ‘𝑢)(Hom ‘𝑌)(2nd ‘𝑣))) ∈ 𝒫 (∪ ran (Hom ‘𝑋) × ∪ ran
(Hom ‘𝑌)) ↔
(𝑢 ∈
((Base‘𝑋) ×
(Base‘𝑌)), 𝑣 ∈ ((Base‘𝑋) × (Base‘𝑌)) ↦ (((1st
‘𝑢)(Hom ‘𝑋)(1st ‘𝑣)) × ((2nd
‘𝑢)(Hom ‘𝑌)(2nd ‘𝑣)))):(((Base‘𝑋) × (Base‘𝑌)) × ((Base‘𝑋) × (Base‘𝑌)))⟶𝒫 (∪ ran (Hom ‘𝑋) × ∪ ran
(Hom ‘𝑌))) |
| 51 | 48, 50 | mpbi 230 |
. . . . . . . . 9
⊢ (𝑢 ∈ ((Base‘𝑋) × (Base‘𝑌)), 𝑣 ∈ ((Base‘𝑋) × (Base‘𝑌)) ↦ (((1st ‘𝑢)(Hom ‘𝑋)(1st ‘𝑣)) × ((2nd ‘𝑢)(Hom ‘𝑌)(2nd ‘𝑣)))):(((Base‘𝑋) × (Base‘𝑌)) × ((Base‘𝑋) × (Base‘𝑌)))⟶𝒫 (∪ ran (Hom ‘𝑋) × ∪ ran
(Hom ‘𝑌)) |
| 52 | 51 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → (𝑢 ∈ ((Base‘𝑋) × (Base‘𝑌)), 𝑣 ∈ ((Base‘𝑋) × (Base‘𝑌)) ↦ (((1st ‘𝑢)(Hom ‘𝑋)(1st ‘𝑣)) × ((2nd ‘𝑢)(Hom ‘𝑌)(2nd ‘𝑣)))):(((Base‘𝑋) × (Base‘𝑌)) × ((Base‘𝑋) × (Base‘𝑌)))⟶𝒫 (∪ ran (Hom ‘𝑋) × ∪ ran
(Hom ‘𝑌))) |
| 53 | 17, 30, 38, 52 | wunf 10767 |
. . . . . . 7
⊢ (𝜑 → (𝑢 ∈ ((Base‘𝑋) × (Base‘𝑌)), 𝑣 ∈ ((Base‘𝑋) × (Base‘𝑌)) ↦ (((1st ‘𝑢)(Hom ‘𝑋)(1st ‘𝑣)) × ((2nd ‘𝑢)(Hom ‘𝑌)(2nd ‘𝑣)))) ∈ 𝑈) |
| 54 | 13, 53 | eqeltrid 2845 |
. . . . . 6
⊢ (𝜑 → (Hom ‘𝑇) ∈ 𝑈) |
| 55 | 17, 29, 54 | wunop 10762 |
. . . . 5
⊢ (𝜑 → 〈(Hom ‘ndx),
(Hom ‘𝑇)〉 ∈
𝑈) |
| 56 | | ccoid 17458 |
. . . . . . 7
⊢ comp =
Slot (comp‘ndx) |
| 57 | 56, 17, 20 | wunstr 17225 |
. . . . . 6
⊢ (𝜑 → (comp‘ndx) ∈
𝑈) |
| 58 | 17, 30, 26 | wunxp 10764 |
. . . . . . 7
⊢ (𝜑 → ((((Base‘𝑋) × (Base‘𝑌)) × ((Base‘𝑋) × (Base‘𝑌))) × ((Base‘𝑋) × (Base‘𝑌))) ∈ 𝑈) |
| 59 | 22, 23, 17, 8 | catcccocl 18161 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (comp‘𝑋) ∈ 𝑈) |
| 60 | 17, 59 | wunrn 10769 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ran (comp‘𝑋) ∈ 𝑈) |
| 61 | 17, 60 | wununi 10746 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∪ ran (comp‘𝑋) ∈ 𝑈) |
| 62 | 17, 61 | wunrn 10769 |
. . . . . . . . . . 11
⊢ (𝜑 → ran ∪ ran (comp‘𝑋) ∈ 𝑈) |
| 63 | 17, 62 | wununi 10746 |
. . . . . . . . . 10
⊢ (𝜑 → ∪ ran ∪ ran (comp‘𝑋) ∈ 𝑈) |
| 64 | 17, 63 | wunpw 10747 |
. . . . . . . . 9
⊢ (𝜑 → 𝒫 ∪ ran ∪ ran (comp‘𝑋) ∈ 𝑈) |
| 65 | 22, 23, 17, 9 | catcccocl 18161 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (comp‘𝑌) ∈ 𝑈) |
| 66 | 17, 65 | wunrn 10769 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ran (comp‘𝑌) ∈ 𝑈) |
| 67 | 17, 66 | wununi 10746 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∪ ran (comp‘𝑌) ∈ 𝑈) |
| 68 | 17, 67 | wunrn 10769 |
. . . . . . . . . . 11
⊢ (𝜑 → ran ∪ ran (comp‘𝑌) ∈ 𝑈) |
| 69 | 17, 68 | wununi 10746 |
. . . . . . . . . 10
⊢ (𝜑 → ∪ ran ∪ ran (comp‘𝑌) ∈ 𝑈) |
| 70 | 17, 69 | wunpw 10747 |
. . . . . . . . 9
⊢ (𝜑 → 𝒫 ∪ ran ∪ ran (comp‘𝑌) ∈ 𝑈) |
| 71 | 17, 64, 70 | wunxp 10764 |
. . . . . . . 8
⊢ (𝜑 → (𝒫 ∪ ran ∪ ran (comp‘𝑋) × 𝒫 ∪ ran ∪ ran (comp‘𝑌)) ∈ 𝑈) |
| 72 | 17, 54 | wunrn 10769 |
. . . . . . . . . 10
⊢ (𝜑 → ran (Hom ‘𝑇) ∈ 𝑈) |
| 73 | 17, 72 | wununi 10746 |
. . . . . . . . 9
⊢ (𝜑 → ∪ ran (Hom ‘𝑇) ∈ 𝑈) |
| 74 | 17, 73, 73 | wunxp 10764 |
. . . . . . . 8
⊢ (𝜑 → (∪ ran (Hom ‘𝑇) × ∪ ran
(Hom ‘𝑇)) ∈
𝑈) |
| 75 | 17, 71, 74 | wunpm 10765 |
. . . . . . 7
⊢ (𝜑 → ((𝒫 ∪ ran ∪ ran (comp‘𝑋) × 𝒫 ∪ ran ∪ ran (comp‘𝑌)) ↑pm (∪ ran (Hom ‘𝑇) × ∪ ran
(Hom ‘𝑇))) ∈
𝑈) |
| 76 | | fvex 6919 |
. . . . . . . . . . . . . . . . 17
⊢
(comp‘𝑋)
∈ V |
| 77 | 76 | rnex 7932 |
. . . . . . . . . . . . . . . 16
⊢ ran
(comp‘𝑋) ∈
V |
| 78 | 77 | uniex 7761 |
. . . . . . . . . . . . . . 15
⊢ ∪ ran (comp‘𝑋) ∈ V |
| 79 | 78 | rnex 7932 |
. . . . . . . . . . . . . 14
⊢ ran ∪ ran (comp‘𝑋) ∈ V |
| 80 | 79 | uniex 7761 |
. . . . . . . . . . . . 13
⊢ ∪ ran ∪ ran (comp‘𝑋) ∈ V |
| 81 | 80 | pwex 5380 |
. . . . . . . . . . . 12
⊢ 𝒫
∪ ran ∪ ran
(comp‘𝑋) ∈
V |
| 82 | | fvex 6919 |
. . . . . . . . . . . . . . . . 17
⊢
(comp‘𝑌)
∈ V |
| 83 | 82 | rnex 7932 |
. . . . . . . . . . . . . . . 16
⊢ ran
(comp‘𝑌) ∈
V |
| 84 | 83 | uniex 7761 |
. . . . . . . . . . . . . . 15
⊢ ∪ ran (comp‘𝑌) ∈ V |
| 85 | 84 | rnex 7932 |
. . . . . . . . . . . . . 14
⊢ ran ∪ ran (comp‘𝑌) ∈ V |
| 86 | 85 | uniex 7761 |
. . . . . . . . . . . . 13
⊢ ∪ ran ∪ ran (comp‘𝑌) ∈ V |
| 87 | 86 | pwex 5380 |
. . . . . . . . . . . 12
⊢ 𝒫
∪ ran ∪ ran
(comp‘𝑌) ∈
V |
| 88 | 81, 87 | xpex 7773 |
. . . . . . . . . . 11
⊢
(𝒫 ∪ ran ∪
ran (comp‘𝑋) ×
𝒫 ∪ ran ∪ ran
(comp‘𝑌)) ∈
V |
| 89 | | fvex 6919 |
. . . . . . . . . . . . . 14
⊢ (Hom
‘𝑇) ∈
V |
| 90 | 89 | rnex 7932 |
. . . . . . . . . . . . 13
⊢ ran (Hom
‘𝑇) ∈
V |
| 91 | 90 | uniex 7761 |
. . . . . . . . . . . 12
⊢ ∪ ran (Hom ‘𝑇) ∈ V |
| 92 | 91, 91 | xpex 7773 |
. . . . . . . . . . 11
⊢ (∪ ran (Hom ‘𝑇) × ∪ ran
(Hom ‘𝑇)) ∈
V |
| 93 | | ovssunirn 7467 |
. . . . . . . . . . . . . . . 16
⊢
((1st ‘𝑔)(〈(1st
‘(1st ‘𝑥)), (1st ‘(2nd
‘𝑥))〉(comp‘𝑋)(1st ‘𝑦))(1st ‘𝑓)) ⊆ ∪ ran
(〈(1st ‘(1st ‘𝑥)), (1st ‘(2nd
‘𝑥))〉(comp‘𝑋)(1st ‘𝑦)) |
| 94 | | ovssunirn 7467 |
. . . . . . . . . . . . . . . . 17
⊢
(〈(1st ‘(1st ‘𝑥)), (1st ‘(2nd
‘𝑥))〉(comp‘𝑋)(1st ‘𝑦)) ⊆ ∪ ran
(comp‘𝑋) |
| 95 | | rnss 5950 |
. . . . . . . . . . . . . . . . 17
⊢
((〈(1st ‘(1st ‘𝑥)), (1st ‘(2nd
‘𝑥))〉(comp‘𝑋)(1st ‘𝑦)) ⊆ ∪ ran
(comp‘𝑋) → ran
(〈(1st ‘(1st ‘𝑥)), (1st ‘(2nd
‘𝑥))〉(comp‘𝑋)(1st ‘𝑦)) ⊆ ran ∪
ran (comp‘𝑋)) |
| 96 | | uniss 4915 |
. . . . . . . . . . . . . . . . 17
⊢ (ran
(〈(1st ‘(1st ‘𝑥)), (1st ‘(2nd
‘𝑥))〉(comp‘𝑋)(1st ‘𝑦)) ⊆ ran ∪
ran (comp‘𝑋) →
∪ ran (〈(1st ‘(1st
‘𝑥)), (1st
‘(2nd ‘𝑥))〉(comp‘𝑋)(1st ‘𝑦)) ⊆ ∪ ran
∪ ran (comp‘𝑋)) |
| 97 | 94, 95, 96 | mp2b 10 |
. . . . . . . . . . . . . . . 16
⊢ ∪ ran (〈(1st ‘(1st
‘𝑥)), (1st
‘(2nd ‘𝑥))〉(comp‘𝑋)(1st ‘𝑦)) ⊆ ∪ ran
∪ ran (comp‘𝑋) |
| 98 | 93, 97 | sstri 3993 |
. . . . . . . . . . . . . . 15
⊢
((1st ‘𝑔)(〈(1st
‘(1st ‘𝑥)), (1st ‘(2nd
‘𝑥))〉(comp‘𝑋)(1st ‘𝑦))(1st ‘𝑓)) ⊆ ∪ ran
∪ ran (comp‘𝑋) |
| 99 | | ovex 7464 |
. . . . . . . . . . . . . . . 16
⊢
((1st ‘𝑔)(〈(1st
‘(1st ‘𝑥)), (1st ‘(2nd
‘𝑥))〉(comp‘𝑋)(1st ‘𝑦))(1st ‘𝑓)) ∈ V |
| 100 | 99 | elpw 4604 |
. . . . . . . . . . . . . . 15
⊢
(((1st ‘𝑔)(〈(1st
‘(1st ‘𝑥)), (1st ‘(2nd
‘𝑥))〉(comp‘𝑋)(1st ‘𝑦))(1st ‘𝑓)) ∈ 𝒫 ∪ ran ∪ ran (comp‘𝑋) ↔ ((1st
‘𝑔)(〈(1st
‘(1st ‘𝑥)), (1st ‘(2nd
‘𝑥))〉(comp‘𝑋)(1st ‘𝑦))(1st ‘𝑓)) ⊆ ∪ ran
∪ ran (comp‘𝑋)) |
| 101 | 98, 100 | mpbir 231 |
. . . . . . . . . . . . . 14
⊢
((1st ‘𝑔)(〈(1st
‘(1st ‘𝑥)), (1st ‘(2nd
‘𝑥))〉(comp‘𝑋)(1st ‘𝑦))(1st ‘𝑓)) ∈ 𝒫 ∪ ran ∪ ran (comp‘𝑋) |
| 102 | | ovssunirn 7467 |
. . . . . . . . . . . . . . . 16
⊢
((2nd ‘𝑔)(〈(2nd
‘(1st ‘𝑥)), (2nd ‘(2nd
‘𝑥))〉(comp‘𝑌)(2nd ‘𝑦))(2nd ‘𝑓)) ⊆ ∪ ran
(〈(2nd ‘(1st ‘𝑥)), (2nd ‘(2nd
‘𝑥))〉(comp‘𝑌)(2nd ‘𝑦)) |
| 103 | | ovssunirn 7467 |
. . . . . . . . . . . . . . . . 17
⊢
(〈(2nd ‘(1st ‘𝑥)), (2nd ‘(2nd
‘𝑥))〉(comp‘𝑌)(2nd ‘𝑦)) ⊆ ∪ ran
(comp‘𝑌) |
| 104 | | rnss 5950 |
. . . . . . . . . . . . . . . . 17
⊢
((〈(2nd ‘(1st ‘𝑥)), (2nd ‘(2nd
‘𝑥))〉(comp‘𝑌)(2nd ‘𝑦)) ⊆ ∪ ran
(comp‘𝑌) → ran
(〈(2nd ‘(1st ‘𝑥)), (2nd ‘(2nd
‘𝑥))〉(comp‘𝑌)(2nd ‘𝑦)) ⊆ ran ∪
ran (comp‘𝑌)) |
| 105 | | uniss 4915 |
. . . . . . . . . . . . . . . . 17
⊢ (ran
(〈(2nd ‘(1st ‘𝑥)), (2nd ‘(2nd
‘𝑥))〉(comp‘𝑌)(2nd ‘𝑦)) ⊆ ran ∪
ran (comp‘𝑌) →
∪ ran (〈(2nd ‘(1st
‘𝑥)), (2nd
‘(2nd ‘𝑥))〉(comp‘𝑌)(2nd ‘𝑦)) ⊆ ∪ ran
∪ ran (comp‘𝑌)) |
| 106 | 103, 104,
105 | mp2b 10 |
. . . . . . . . . . . . . . . 16
⊢ ∪ ran (〈(2nd ‘(1st
‘𝑥)), (2nd
‘(2nd ‘𝑥))〉(comp‘𝑌)(2nd ‘𝑦)) ⊆ ∪ ran
∪ ran (comp‘𝑌) |
| 107 | 102, 106 | sstri 3993 |
. . . . . . . . . . . . . . 15
⊢
((2nd ‘𝑔)(〈(2nd
‘(1st ‘𝑥)), (2nd ‘(2nd
‘𝑥))〉(comp‘𝑌)(2nd ‘𝑦))(2nd ‘𝑓)) ⊆ ∪ ran
∪ ran (comp‘𝑌) |
| 108 | | ovex 7464 |
. . . . . . . . . . . . . . . 16
⊢
((2nd ‘𝑔)(〈(2nd
‘(1st ‘𝑥)), (2nd ‘(2nd
‘𝑥))〉(comp‘𝑌)(2nd ‘𝑦))(2nd ‘𝑓)) ∈ V |
| 109 | 108 | elpw 4604 |
. . . . . . . . . . . . . . 15
⊢
(((2nd ‘𝑔)(〈(2nd
‘(1st ‘𝑥)), (2nd ‘(2nd
‘𝑥))〉(comp‘𝑌)(2nd ‘𝑦))(2nd ‘𝑓)) ∈ 𝒫 ∪ ran ∪ ran (comp‘𝑌) ↔ ((2nd
‘𝑔)(〈(2nd
‘(1st ‘𝑥)), (2nd ‘(2nd
‘𝑥))〉(comp‘𝑌)(2nd ‘𝑦))(2nd ‘𝑓)) ⊆ ∪ ran
∪ ran (comp‘𝑌)) |
| 110 | 107, 109 | mpbir 231 |
. . . . . . . . . . . . . 14
⊢
((2nd ‘𝑔)(〈(2nd
‘(1st ‘𝑥)), (2nd ‘(2nd
‘𝑥))〉(comp‘𝑌)(2nd ‘𝑦))(2nd ‘𝑓)) ∈ 𝒫 ∪ ran ∪ ran (comp‘𝑌) |
| 111 | | opelxpi 5722 |
. . . . . . . . . . . . . 14
⊢
((((1st ‘𝑔)(〈(1st
‘(1st ‘𝑥)), (1st ‘(2nd
‘𝑥))〉(comp‘𝑋)(1st ‘𝑦))(1st ‘𝑓)) ∈ 𝒫 ∪ ran ∪ ran (comp‘𝑋) ∧ ((2nd
‘𝑔)(〈(2nd
‘(1st ‘𝑥)), (2nd ‘(2nd
‘𝑥))〉(comp‘𝑌)(2nd ‘𝑦))(2nd ‘𝑓)) ∈ 𝒫 ∪ ran ∪ ran (comp‘𝑌)) → 〈((1st
‘𝑔)(〈(1st
‘(1st ‘𝑥)), (1st ‘(2nd
‘𝑥))〉(comp‘𝑋)(1st ‘𝑦))(1st ‘𝑓)), ((2nd ‘𝑔)(〈(2nd
‘(1st ‘𝑥)), (2nd ‘(2nd
‘𝑥))〉(comp‘𝑌)(2nd ‘𝑦))(2nd ‘𝑓))〉 ∈ (𝒫 ∪ ran ∪ ran (comp‘𝑋) × 𝒫 ∪ ran ∪ ran (comp‘𝑌))) |
| 112 | 101, 110,
111 | mp2an 692 |
. . . . . . . . . . . . 13
⊢
〈((1st ‘𝑔)(〈(1st
‘(1st ‘𝑥)), (1st ‘(2nd
‘𝑥))〉(comp‘𝑋)(1st ‘𝑦))(1st ‘𝑓)), ((2nd ‘𝑔)(〈(2nd
‘(1st ‘𝑥)), (2nd ‘(2nd
‘𝑥))〉(comp‘𝑌)(2nd ‘𝑦))(2nd ‘𝑓))〉 ∈ (𝒫 ∪ ran ∪ ran (comp‘𝑋) × 𝒫 ∪ ran ∪ ran (comp‘𝑌)) |
| 113 | 112 | rgen2w 3066 |
. . . . . . . . . . . 12
⊢
∀𝑔 ∈
((2nd ‘𝑥)(Hom ‘𝑇)𝑦)∀𝑓 ∈ ((Hom ‘𝑇)‘𝑥)〈((1st ‘𝑔)(〈(1st
‘(1st ‘𝑥)), (1st ‘(2nd
‘𝑥))〉(comp‘𝑋)(1st ‘𝑦))(1st ‘𝑓)), ((2nd ‘𝑔)(〈(2nd
‘(1st ‘𝑥)), (2nd ‘(2nd
‘𝑥))〉(comp‘𝑌)(2nd ‘𝑦))(2nd ‘𝑓))〉 ∈ (𝒫 ∪ ran ∪ ran (comp‘𝑋) × 𝒫 ∪ ran ∪ ran (comp‘𝑌)) |
| 114 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢ (𝑔 ∈ ((2nd
‘𝑥)(Hom ‘𝑇)𝑦), 𝑓 ∈ ((Hom ‘𝑇)‘𝑥) ↦ 〈((1st ‘𝑔)(〈(1st
‘(1st ‘𝑥)), (1st ‘(2nd
‘𝑥))〉(comp‘𝑋)(1st ‘𝑦))(1st ‘𝑓)), ((2nd ‘𝑔)(〈(2nd
‘(1st ‘𝑥)), (2nd ‘(2nd
‘𝑥))〉(comp‘𝑌)(2nd ‘𝑦))(2nd ‘𝑓))〉) = (𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝑇)𝑦), 𝑓 ∈ ((Hom ‘𝑇)‘𝑥) ↦ 〈((1st ‘𝑔)(〈(1st
‘(1st ‘𝑥)), (1st ‘(2nd
‘𝑥))〉(comp‘𝑋)(1st ‘𝑦))(1st ‘𝑓)), ((2nd ‘𝑔)(〈(2nd
‘(1st ‘𝑥)), (2nd ‘(2nd
‘𝑥))〉(comp‘𝑌)(2nd ‘𝑦))(2nd ‘𝑓))〉) |
| 115 | 114 | fmpo 8093 |
. . . . . . . . . . . 12
⊢
(∀𝑔 ∈
((2nd ‘𝑥)(Hom ‘𝑇)𝑦)∀𝑓 ∈ ((Hom ‘𝑇)‘𝑥)〈((1st ‘𝑔)(〈(1st
‘(1st ‘𝑥)), (1st ‘(2nd
‘𝑥))〉(comp‘𝑋)(1st ‘𝑦))(1st ‘𝑓)), ((2nd ‘𝑔)(〈(2nd
‘(1st ‘𝑥)), (2nd ‘(2nd
‘𝑥))〉(comp‘𝑌)(2nd ‘𝑦))(2nd ‘𝑓))〉 ∈ (𝒫 ∪ ran ∪ ran (comp‘𝑋) × 𝒫 ∪ ran ∪ ran (comp‘𝑌)) ↔ (𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝑇)𝑦), 𝑓 ∈ ((Hom ‘𝑇)‘𝑥) ↦ 〈((1st ‘𝑔)(〈(1st
‘(1st ‘𝑥)), (1st ‘(2nd
‘𝑥))〉(comp‘𝑋)(1st ‘𝑦))(1st ‘𝑓)), ((2nd ‘𝑔)(〈(2nd
‘(1st ‘𝑥)), (2nd ‘(2nd
‘𝑥))〉(comp‘𝑌)(2nd ‘𝑦))(2nd ‘𝑓))〉):(((2nd ‘𝑥)(Hom ‘𝑇)𝑦) × ((Hom ‘𝑇)‘𝑥))⟶(𝒫 ∪ ran ∪ ran (comp‘𝑋) × 𝒫 ∪ ran ∪ ran (comp‘𝑌))) |
| 116 | 113, 115 | mpbi 230 |
. . . . . . . . . . 11
⊢ (𝑔 ∈ ((2nd
‘𝑥)(Hom ‘𝑇)𝑦), 𝑓 ∈ ((Hom ‘𝑇)‘𝑥) ↦ 〈((1st ‘𝑔)(〈(1st
‘(1st ‘𝑥)), (1st ‘(2nd
‘𝑥))〉(comp‘𝑋)(1st ‘𝑦))(1st ‘𝑓)), ((2nd ‘𝑔)(〈(2nd
‘(1st ‘𝑥)), (2nd ‘(2nd
‘𝑥))〉(comp‘𝑌)(2nd ‘𝑦))(2nd ‘𝑓))〉):(((2nd ‘𝑥)(Hom ‘𝑇)𝑦) × ((Hom ‘𝑇)‘𝑥))⟶(𝒫 ∪ ran ∪ ran (comp‘𝑋) × 𝒫 ∪ ran ∪ ran (comp‘𝑌)) |
| 117 | | ovssunirn 7467 |
. . . . . . . . . . . 12
⊢
((2nd ‘𝑥)(Hom ‘𝑇)𝑦) ⊆ ∪ ran
(Hom ‘𝑇) |
| 118 | | fvssunirn 6939 |
. . . . . . . . . . . 12
⊢ ((Hom
‘𝑇)‘𝑥) ⊆ ∪ ran (Hom ‘𝑇) |
| 119 | | xpss12 5700 |
. . . . . . . . . . . 12
⊢
((((2nd ‘𝑥)(Hom ‘𝑇)𝑦) ⊆ ∪ ran
(Hom ‘𝑇) ∧ ((Hom
‘𝑇)‘𝑥) ⊆ ∪ ran (Hom ‘𝑇)) → (((2nd ‘𝑥)(Hom ‘𝑇)𝑦) × ((Hom ‘𝑇)‘𝑥)) ⊆ (∪ ran
(Hom ‘𝑇) ×
∪ ran (Hom ‘𝑇))) |
| 120 | 117, 118,
119 | mp2an 692 |
. . . . . . . . . . 11
⊢
(((2nd ‘𝑥)(Hom ‘𝑇)𝑦) × ((Hom ‘𝑇)‘𝑥)) ⊆ (∪ ran
(Hom ‘𝑇) ×
∪ ran (Hom ‘𝑇)) |
| 121 | | elpm2r 8885 |
. . . . . . . . . . 11
⊢
((((𝒫 ∪ ran ∪ ran (comp‘𝑋) × 𝒫 ∪ ran ∪ ran (comp‘𝑌)) ∈ V ∧ (∪ ran (Hom ‘𝑇) × ∪ ran
(Hom ‘𝑇)) ∈ V)
∧ ((𝑔 ∈
((2nd ‘𝑥)(Hom ‘𝑇)𝑦), 𝑓 ∈ ((Hom ‘𝑇)‘𝑥) ↦ 〈((1st ‘𝑔)(〈(1st
‘(1st ‘𝑥)), (1st ‘(2nd
‘𝑥))〉(comp‘𝑋)(1st ‘𝑦))(1st ‘𝑓)), ((2nd ‘𝑔)(〈(2nd
‘(1st ‘𝑥)), (2nd ‘(2nd
‘𝑥))〉(comp‘𝑌)(2nd ‘𝑦))(2nd ‘𝑓))〉):(((2nd ‘𝑥)(Hom ‘𝑇)𝑦) × ((Hom ‘𝑇)‘𝑥))⟶(𝒫 ∪ ran ∪ ran (comp‘𝑋) × 𝒫 ∪ ran ∪ ran (comp‘𝑌)) ∧ (((2nd
‘𝑥)(Hom ‘𝑇)𝑦) × ((Hom ‘𝑇)‘𝑥)) ⊆ (∪ ran
(Hom ‘𝑇) ×
∪ ran (Hom ‘𝑇)))) → (𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝑇)𝑦), 𝑓 ∈ ((Hom ‘𝑇)‘𝑥) ↦ 〈((1st ‘𝑔)(〈(1st
‘(1st ‘𝑥)), (1st ‘(2nd
‘𝑥))〉(comp‘𝑋)(1st ‘𝑦))(1st ‘𝑓)), ((2nd ‘𝑔)(〈(2nd
‘(1st ‘𝑥)), (2nd ‘(2nd
‘𝑥))〉(comp‘𝑌)(2nd ‘𝑦))(2nd ‘𝑓))〉) ∈ ((𝒫 ∪ ran ∪ ran (comp‘𝑋) × 𝒫 ∪ ran ∪ ran (comp‘𝑌)) ↑pm (∪ ran (Hom ‘𝑇) × ∪ ran
(Hom ‘𝑇)))) |
| 122 | 88, 92, 116, 120, 121 | mp4an 693 |
. . . . . . . . . 10
⊢ (𝑔 ∈ ((2nd
‘𝑥)(Hom ‘𝑇)𝑦), 𝑓 ∈ ((Hom ‘𝑇)‘𝑥) ↦ 〈((1st ‘𝑔)(〈(1st
‘(1st ‘𝑥)), (1st ‘(2nd
‘𝑥))〉(comp‘𝑋)(1st ‘𝑦))(1st ‘𝑓)), ((2nd ‘𝑔)(〈(2nd
‘(1st ‘𝑥)), (2nd ‘(2nd
‘𝑥))〉(comp‘𝑌)(2nd ‘𝑦))(2nd ‘𝑓))〉) ∈ ((𝒫 ∪ ran ∪ ran (comp‘𝑋) × 𝒫 ∪ ran ∪ ran (comp‘𝑌)) ↑pm (∪ ran (Hom ‘𝑇) × ∪ ran
(Hom ‘𝑇))) |
| 123 | 122 | rgen2w 3066 |
. . . . . . . . 9
⊢
∀𝑥 ∈
(((Base‘𝑋) ×
(Base‘𝑌)) ×
((Base‘𝑋) ×
(Base‘𝑌)))∀𝑦 ∈ ((Base‘𝑋) × (Base‘𝑌))(𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝑇)𝑦), 𝑓 ∈ ((Hom ‘𝑇)‘𝑥) ↦ 〈((1st ‘𝑔)(〈(1st
‘(1st ‘𝑥)), (1st ‘(2nd
‘𝑥))〉(comp‘𝑋)(1st ‘𝑦))(1st ‘𝑓)), ((2nd ‘𝑔)(〈(2nd
‘(1st ‘𝑥)), (2nd ‘(2nd
‘𝑥))〉(comp‘𝑌)(2nd ‘𝑦))(2nd ‘𝑓))〉) ∈ ((𝒫 ∪ ran ∪ ran (comp‘𝑋) × 𝒫 ∪ ran ∪ ran (comp‘𝑌)) ↑pm (∪ ran (Hom ‘𝑇) × ∪ ran
(Hom ‘𝑇))) |
| 124 | | eqid 2737 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (((Base‘𝑋) × (Base‘𝑌)) × ((Base‘𝑋) × (Base‘𝑌))), 𝑦 ∈ ((Base‘𝑋) × (Base‘𝑌)) ↦ (𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝑇)𝑦), 𝑓 ∈ ((Hom ‘𝑇)‘𝑥) ↦ 〈((1st ‘𝑔)(〈(1st
‘(1st ‘𝑥)), (1st ‘(2nd
‘𝑥))〉(comp‘𝑋)(1st ‘𝑦))(1st ‘𝑓)), ((2nd ‘𝑔)(〈(2nd
‘(1st ‘𝑥)), (2nd ‘(2nd
‘𝑥))〉(comp‘𝑌)(2nd ‘𝑦))(2nd ‘𝑓))〉)) = (𝑥 ∈ (((Base‘𝑋) × (Base‘𝑌)) × ((Base‘𝑋) × (Base‘𝑌))), 𝑦 ∈ ((Base‘𝑋) × (Base‘𝑌)) ↦ (𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝑇)𝑦), 𝑓 ∈ ((Hom ‘𝑇)‘𝑥) ↦ 〈((1st ‘𝑔)(〈(1st
‘(1st ‘𝑥)), (1st ‘(2nd
‘𝑥))〉(comp‘𝑋)(1st ‘𝑦))(1st ‘𝑓)), ((2nd ‘𝑔)(〈(2nd
‘(1st ‘𝑥)), (2nd ‘(2nd
‘𝑥))〉(comp‘𝑌)(2nd ‘𝑦))(2nd ‘𝑓))〉)) |
| 125 | 124 | fmpo 8093 |
. . . . . . . . 9
⊢
(∀𝑥 ∈
(((Base‘𝑋) ×
(Base‘𝑌)) ×
((Base‘𝑋) ×
(Base‘𝑌)))∀𝑦 ∈ ((Base‘𝑋) × (Base‘𝑌))(𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝑇)𝑦), 𝑓 ∈ ((Hom ‘𝑇)‘𝑥) ↦ 〈((1st ‘𝑔)(〈(1st
‘(1st ‘𝑥)), (1st ‘(2nd
‘𝑥))〉(comp‘𝑋)(1st ‘𝑦))(1st ‘𝑓)), ((2nd ‘𝑔)(〈(2nd
‘(1st ‘𝑥)), (2nd ‘(2nd
‘𝑥))〉(comp‘𝑌)(2nd ‘𝑦))(2nd ‘𝑓))〉) ∈ ((𝒫 ∪ ran ∪ ran (comp‘𝑋) × 𝒫 ∪ ran ∪ ran (comp‘𝑌)) ↑pm (∪ ran (Hom ‘𝑇) × ∪ ran
(Hom ‘𝑇))) ↔
(𝑥 ∈
(((Base‘𝑋) ×
(Base‘𝑌)) ×
((Base‘𝑋) ×
(Base‘𝑌))), 𝑦 ∈ ((Base‘𝑋) × (Base‘𝑌)) ↦ (𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝑇)𝑦), 𝑓 ∈ ((Hom ‘𝑇)‘𝑥) ↦ 〈((1st ‘𝑔)(〈(1st
‘(1st ‘𝑥)), (1st ‘(2nd
‘𝑥))〉(comp‘𝑋)(1st ‘𝑦))(1st ‘𝑓)), ((2nd ‘𝑔)(〈(2nd
‘(1st ‘𝑥)), (2nd ‘(2nd
‘𝑥))〉(comp‘𝑌)(2nd ‘𝑦))(2nd ‘𝑓))〉)):((((Base‘𝑋) × (Base‘𝑌)) × ((Base‘𝑋) × (Base‘𝑌))) × ((Base‘𝑋) × (Base‘𝑌)))⟶((𝒫 ∪ ran ∪ ran (comp‘𝑋) × 𝒫 ∪ ran ∪ ran (comp‘𝑌)) ↑pm (∪ ran (Hom ‘𝑇) × ∪ ran
(Hom ‘𝑇)))) |
| 126 | 123, 125 | mpbi 230 |
. . . . . . . 8
⊢ (𝑥 ∈ (((Base‘𝑋) × (Base‘𝑌)) × ((Base‘𝑋) × (Base‘𝑌))), 𝑦 ∈ ((Base‘𝑋) × (Base‘𝑌)) ↦ (𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝑇)𝑦), 𝑓 ∈ ((Hom ‘𝑇)‘𝑥) ↦ 〈((1st ‘𝑔)(〈(1st
‘(1st ‘𝑥)), (1st ‘(2nd
‘𝑥))〉(comp‘𝑋)(1st ‘𝑦))(1st ‘𝑓)), ((2nd ‘𝑔)(〈(2nd
‘(1st ‘𝑥)), (2nd ‘(2nd
‘𝑥))〉(comp‘𝑌)(2nd ‘𝑦))(2nd ‘𝑓))〉)):((((Base‘𝑋) × (Base‘𝑌)) × ((Base‘𝑋) × (Base‘𝑌))) × ((Base‘𝑋) × (Base‘𝑌)))⟶((𝒫 ∪ ran ∪ ran (comp‘𝑋) × 𝒫 ∪ ran ∪ ran (comp‘𝑌)) ↑pm (∪ ran (Hom ‘𝑇) × ∪ ran
(Hom ‘𝑇))) |
| 127 | 126 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ (((Base‘𝑋) × (Base‘𝑌)) × ((Base‘𝑋) × (Base‘𝑌))), 𝑦 ∈ ((Base‘𝑋) × (Base‘𝑌)) ↦ (𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝑇)𝑦), 𝑓 ∈ ((Hom ‘𝑇)‘𝑥) ↦ 〈((1st ‘𝑔)(〈(1st
‘(1st ‘𝑥)), (1st ‘(2nd
‘𝑥))〉(comp‘𝑋)(1st ‘𝑦))(1st ‘𝑓)), ((2nd ‘𝑔)(〈(2nd
‘(1st ‘𝑥)), (2nd ‘(2nd
‘𝑥))〉(comp‘𝑌)(2nd ‘𝑦))(2nd ‘𝑓))〉)):((((Base‘𝑋) × (Base‘𝑌)) × ((Base‘𝑋) × (Base‘𝑌))) × ((Base‘𝑋) × (Base‘𝑌)))⟶((𝒫 ∪ ran ∪ ran (comp‘𝑋) × 𝒫 ∪ ran ∪ ran (comp‘𝑌)) ↑pm (∪ ran (Hom ‘𝑇) × ∪ ran
(Hom ‘𝑇)))) |
| 128 | 17, 58, 75, 127 | wunf 10767 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (((Base‘𝑋) × (Base‘𝑌)) × ((Base‘𝑋) × (Base‘𝑌))), 𝑦 ∈ ((Base‘𝑋) × (Base‘𝑌)) ↦ (𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝑇)𝑦), 𝑓 ∈ ((Hom ‘𝑇)‘𝑥) ↦ 〈((1st ‘𝑔)(〈(1st
‘(1st ‘𝑥)), (1st ‘(2nd
‘𝑥))〉(comp‘𝑋)(1st ‘𝑦))(1st ‘𝑓)), ((2nd ‘𝑔)(〈(2nd
‘(1st ‘𝑥)), (2nd ‘(2nd
‘𝑥))〉(comp‘𝑌)(2nd ‘𝑦))(2nd ‘𝑓))〉)) ∈ 𝑈) |
| 129 | 17, 57, 128 | wunop 10762 |
. . . . 5
⊢ (𝜑 → 〈(comp‘ndx),
(𝑥 ∈
(((Base‘𝑋) ×
(Base‘𝑌)) ×
((Base‘𝑋) ×
(Base‘𝑌))), 𝑦 ∈ ((Base‘𝑋) × (Base‘𝑌)) ↦ (𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝑇)𝑦), 𝑓 ∈ ((Hom ‘𝑇)‘𝑥) ↦ 〈((1st ‘𝑔)(〈(1st
‘(1st ‘𝑥)), (1st ‘(2nd
‘𝑥))〉(comp‘𝑋)(1st ‘𝑦))(1st ‘𝑓)), ((2nd ‘𝑔)(〈(2nd
‘(1st ‘𝑥)), (2nd ‘(2nd
‘𝑥))〉(comp‘𝑌)(2nd ‘𝑦))(2nd ‘𝑓))〉))〉 ∈ 𝑈) |
| 130 | 17, 27, 55, 129 | wuntp 10751 |
. . . 4
⊢ (𝜑 → {〈(Base‘ndx),
((Base‘𝑋) ×
(Base‘𝑌))〉,
〈(Hom ‘ndx), (Hom ‘𝑇)〉, 〈(comp‘ndx), (𝑥 ∈ (((Base‘𝑋) × (Base‘𝑌)) × ((Base‘𝑋) × (Base‘𝑌))), 𝑦 ∈ ((Base‘𝑋) × (Base‘𝑌)) ↦ (𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝑇)𝑦), 𝑓 ∈ ((Hom ‘𝑇)‘𝑥) ↦ 〈((1st ‘𝑔)(〈(1st
‘(1st ‘𝑥)), (1st ‘(2nd
‘𝑥))〉(comp‘𝑋)(1st ‘𝑦))(1st ‘𝑓)), ((2nd ‘𝑔)(〈(2nd
‘(1st ‘𝑥)), (2nd ‘(2nd
‘𝑥))〉(comp‘𝑌)(2nd ‘𝑦))(2nd ‘𝑓))〉))〉} ∈ 𝑈) |
| 131 | 16, 130 | eqeltrd 2841 |
. . 3
⊢ (𝜑 → 𝑇 ∈ 𝑈) |
| 132 | 22, 23, 17 | catcbas 18146 |
. . . . . 6
⊢ (𝜑 → 𝐵 = (𝑈 ∩ Cat)) |
| 133 | 8, 132 | eleqtrd 2843 |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ (𝑈 ∩ Cat)) |
| 134 | 133 | elin2d 4205 |
. . . 4
⊢ (𝜑 → 𝑋 ∈ Cat) |
| 135 | 9, 132 | eleqtrd 2843 |
. . . . 5
⊢ (𝜑 → 𝑌 ∈ (𝑈 ∩ Cat)) |
| 136 | 135 | elin2d 4205 |
. . . 4
⊢ (𝜑 → 𝑌 ∈ Cat) |
| 137 | 1, 134, 136 | xpccat 18235 |
. . 3
⊢ (𝜑 → 𝑇 ∈ Cat) |
| 138 | 131, 137 | elind 4200 |
. 2
⊢ (𝜑 → 𝑇 ∈ (𝑈 ∩ Cat)) |
| 139 | 138, 132 | eleqtrrd 2844 |
1
⊢ (𝜑 → 𝑇 ∈ 𝐵) |