Step | Hyp | Ref
| Expression |
1 | | catcxpccl.o |
. . . . 5
⊢ 𝑇 = (𝑋 ×_{c} 𝑌) |
2 | | eqid 2799 |
. . . . 5
⊢
(Base‘𝑋) =
(Base‘𝑋) |
3 | | eqid 2799 |
. . . . 5
⊢
(Base‘𝑌) =
(Base‘𝑌) |
4 | | eqid 2799 |
. . . . 5
⊢ (Hom
‘𝑋) = (Hom
‘𝑋) |
5 | | eqid 2799 |
. . . . 5
⊢ (Hom
‘𝑌) = (Hom
‘𝑌) |
6 | | eqid 2799 |
. . . . 5
⊢
(comp‘𝑋) =
(comp‘𝑋) |
7 | | eqid 2799 |
. . . . 5
⊢
(comp‘𝑌) =
(comp‘𝑌) |
8 | | catcxpccl.x |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
9 | | catcxpccl.y |
. . . . 5
⊢ (𝜑 → 𝑌 ∈ 𝐵) |
10 | | eqidd 2800 |
. . . . 5
⊢ (𝜑 → ((Base‘𝑋) × (Base‘𝑌)) = ((Base‘𝑋) × (Base‘𝑌))) |
11 | 1, 2, 3 | xpcbas 17133 |
. . . . . . 7
⊢
((Base‘𝑋)
× (Base‘𝑌)) =
(Base‘𝑇) |
12 | | eqid 2799 |
. . . . . . 7
⊢ (Hom
‘𝑇) = (Hom
‘𝑇) |
13 | 1, 11, 4, 5, 12 | xpchomfval 17134 |
. . . . . 6
⊢ (Hom
‘𝑇) = (𝑢 ∈ ((Base‘𝑋) × (Base‘𝑌)), 𝑣 ∈ ((Base‘𝑋) × (Base‘𝑌)) ↦ (((1^{st} ‘𝑢)(Hom ‘𝑋)(1^{st} ‘𝑣)) × ((2^{nd} ‘𝑢)(Hom ‘𝑌)(2^{nd} ‘𝑣)))) |
14 | 13 | a1i 11 |
. . . . 5
⊢ (𝜑 → (Hom ‘𝑇) = (𝑢 ∈ ((Base‘𝑋) × (Base‘𝑌)), 𝑣 ∈ ((Base‘𝑋) × (Base‘𝑌)) ↦ (((1^{st} ‘𝑢)(Hom ‘𝑋)(1^{st} ‘𝑣)) × ((2^{nd} ‘𝑢)(Hom ‘𝑌)(2^{nd} ‘𝑣))))) |
15 | | eqidd 2800 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (((Base‘𝑋) × (Base‘𝑌)) × ((Base‘𝑋) × (Base‘𝑌))), 𝑦 ∈ ((Base‘𝑋) × (Base‘𝑌)) ↦ (𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝑇)𝑦), 𝑓 ∈ ((Hom ‘𝑇)‘𝑥) ↦ ⟨((1^{st} ‘𝑔)(⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑋)(1^{st} ‘𝑦))(1^{st} ‘𝑓)), ((2^{nd} ‘𝑔)(⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑌)(2^{nd} ‘𝑦))(2^{nd} ‘𝑓))⟩)) = (𝑥 ∈ (((Base‘𝑋) × (Base‘𝑌)) × ((Base‘𝑋) × (Base‘𝑌))), 𝑦 ∈ ((Base‘𝑋) × (Base‘𝑌)) ↦ (𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝑇)𝑦), 𝑓 ∈ ((Hom ‘𝑇)‘𝑥) ↦ ⟨((1^{st} ‘𝑔)(⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑋)(1^{st} ‘𝑦))(1^{st} ‘𝑓)), ((2^{nd} ‘𝑔)(⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑌)(2^{nd} ‘𝑦))(2^{nd} ‘𝑓))⟩))) |
16 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
14, 15 | xpcval 17132 |
. . . 4
⊢ (𝜑 → 𝑇 = {⟨(Base‘ndx),
((Base‘𝑋) ×
(Base‘𝑌))⟩,
⟨(Hom ‘ndx), (Hom ‘𝑇)⟩, ⟨(comp‘ndx), (𝑥 ∈ (((Base‘𝑋) × (Base‘𝑌)) × ((Base‘𝑋) × (Base‘𝑌))), 𝑦 ∈ ((Base‘𝑋) × (Base‘𝑌)) ↦ (𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝑇)𝑦), 𝑓 ∈ ((Hom ‘𝑇)‘𝑥) ↦ ⟨((1^{st} ‘𝑔)(⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑋)(1^{st} ‘𝑦))(1^{st} ‘𝑓)), ((2^{nd} ‘𝑔)(⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑌)(2^{nd} ‘𝑦))(2^{nd} ‘𝑓))⟩))⟩}) |
17 | | catcxpccl.u |
. . . . 5
⊢ (𝜑 → 𝑈 ∈ WUni) |
18 | | df-base 16190 |
. . . . . . 7
⊢ Base =
Slot 1 |
19 | | catcxpccl.1 |
. . . . . . . 8
⊢ (𝜑 → ω ∈ 𝑈) |
20 | 17, 19 | wunndx 16205 |
. . . . . . 7
⊢ (𝜑 → ndx ∈ 𝑈) |
21 | 18, 17, 20 | wunstr 16208 |
. . . . . 6
⊢ (𝜑 → (Base‘ndx) ∈
𝑈) |
22 | | inss1 4028 |
. . . . . . . . 9
⊢ (𝑈 ∩ Cat) ⊆ 𝑈 |
23 | | catcxpccl.c |
. . . . . . . . . . 11
⊢ 𝐶 = (CatCat‘𝑈) |
24 | | catcxpccl.b |
. . . . . . . . . . 11
⊢ 𝐵 = (Base‘𝐶) |
25 | 23, 24, 17 | catcbas 17061 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 = (𝑈 ∩ Cat)) |
26 | 8, 25 | eleqtrd 2880 |
. . . . . . . . 9
⊢ (𝜑 → 𝑋 ∈ (𝑈 ∩ Cat)) |
27 | 22, 26 | sseldi 3796 |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ 𝑈) |
28 | 18, 17, 27 | wunstr 16208 |
. . . . . . 7
⊢ (𝜑 → (Base‘𝑋) ∈ 𝑈) |
29 | 9, 25 | eleqtrd 2880 |
. . . . . . . . 9
⊢ (𝜑 → 𝑌 ∈ (𝑈 ∩ Cat)) |
30 | 22, 29 | sseldi 3796 |
. . . . . . . 8
⊢ (𝜑 → 𝑌 ∈ 𝑈) |
31 | 18, 17, 30 | wunstr 16208 |
. . . . . . 7
⊢ (𝜑 → (Base‘𝑌) ∈ 𝑈) |
32 | 17, 28, 31 | wunxp 9834 |
. . . . . 6
⊢ (𝜑 → ((Base‘𝑋) × (Base‘𝑌)) ∈ 𝑈) |
33 | 17, 21, 32 | wunop 9832 |
. . . . 5
⊢ (𝜑 → ⟨(Base‘ndx),
((Base‘𝑋) ×
(Base‘𝑌))⟩
∈ 𝑈) |
34 | | df-hom 16291 |
. . . . . . 7
⊢ Hom =
Slot ;14 |
35 | 34, 17, 20 | wunstr 16208 |
. . . . . 6
⊢ (𝜑 → (Hom ‘ndx) ∈
𝑈) |
36 | 17, 32, 32 | wunxp 9834 |
. . . . . . . 8
⊢ (𝜑 → (((Base‘𝑋) × (Base‘𝑌)) × ((Base‘𝑋) × (Base‘𝑌))) ∈ 𝑈) |
37 | 34, 17, 27 | wunstr 16208 |
. . . . . . . . . . . 12
⊢ (𝜑 → (Hom ‘𝑋) ∈ 𝑈) |
38 | 17, 37 | wunrn 9839 |
. . . . . . . . . . 11
⊢ (𝜑 → ran (Hom ‘𝑋) ∈ 𝑈) |
39 | 17, 38 | wununi 9816 |
. . . . . . . . . 10
⊢ (𝜑 → ∪ ran (Hom ‘𝑋) ∈ 𝑈) |
40 | 34, 17, 30 | wunstr 16208 |
. . . . . . . . . . . 12
⊢ (𝜑 → (Hom ‘𝑌) ∈ 𝑈) |
41 | 17, 40 | wunrn 9839 |
. . . . . . . . . . 11
⊢ (𝜑 → ran (Hom ‘𝑌) ∈ 𝑈) |
42 | 17, 41 | wununi 9816 |
. . . . . . . . . 10
⊢ (𝜑 → ∪ ran (Hom ‘𝑌) ∈ 𝑈) |
43 | 17, 39, 42 | wunxp 9834 |
. . . . . . . . 9
⊢ (𝜑 → (∪ ran (Hom ‘𝑋) × ∪ ran
(Hom ‘𝑌)) ∈
𝑈) |
44 | 17, 43 | wunpw 9817 |
. . . . . . . 8
⊢ (𝜑 → 𝒫 (∪ ran (Hom ‘𝑋) × ∪ ran
(Hom ‘𝑌)) ∈
𝑈) |
45 | | ovssunirn 6913 |
. . . . . . . . . . . . 13
⊢
((1^{st} ‘𝑢)(Hom ‘𝑋)(1^{st} ‘𝑣)) ⊆ ∪ ran
(Hom ‘𝑋) |
46 | | ovssunirn 6913 |
. . . . . . . . . . . . 13
⊢
((2^{nd} ‘𝑢)(Hom ‘𝑌)(2^{nd} ‘𝑣)) ⊆ ∪ ran
(Hom ‘𝑌) |
47 | | xpss12 5327 |
. . . . . . . . . . . . 13
⊢
((((1^{st} ‘𝑢)(Hom ‘𝑋)(1^{st} ‘𝑣)) ⊆ ∪ ran
(Hom ‘𝑋) ∧
((2^{nd} ‘𝑢)(Hom ‘𝑌)(2^{nd} ‘𝑣)) ⊆ ∪ ran
(Hom ‘𝑌)) →
(((1^{st} ‘𝑢)(Hom ‘𝑋)(1^{st} ‘𝑣)) × ((2^{nd} ‘𝑢)(Hom ‘𝑌)(2^{nd} ‘𝑣))) ⊆ (∪ ran
(Hom ‘𝑋) ×
∪ ran (Hom ‘𝑌))) |
48 | 45, 46, 47 | mp2an 684 |
. . . . . . . . . . . 12
⊢
(((1^{st} ‘𝑢)(Hom ‘𝑋)(1^{st} ‘𝑣)) × ((2^{nd} ‘𝑢)(Hom ‘𝑌)(2^{nd} ‘𝑣))) ⊆ (∪ ran
(Hom ‘𝑋) ×
∪ ran (Hom ‘𝑌)) |
49 | | ovex 6910 |
. . . . . . . . . . . . . 14
⊢
((1^{st} ‘𝑢)(Hom ‘𝑋)(1^{st} ‘𝑣)) ∈ V |
50 | | ovex 6910 |
. . . . . . . . . . . . . 14
⊢
((2^{nd} ‘𝑢)(Hom ‘𝑌)(2^{nd} ‘𝑣)) ∈ V |
51 | 49, 50 | xpex 7196 |
. . . . . . . . . . . . 13
⊢
(((1^{st} ‘𝑢)(Hom ‘𝑋)(1^{st} ‘𝑣)) × ((2^{nd} ‘𝑢)(Hom ‘𝑌)(2^{nd} ‘𝑣))) ∈ V |
52 | 51 | elpw 4355 |
. . . . . . . . . . . 12
⊢
((((1^{st} ‘𝑢)(Hom ‘𝑋)(1^{st} ‘𝑣)) × ((2^{nd} ‘𝑢)(Hom ‘𝑌)(2^{nd} ‘𝑣))) ∈ 𝒫 (∪ ran (Hom ‘𝑋) × ∪ ran
(Hom ‘𝑌)) ↔
(((1^{st} ‘𝑢)(Hom ‘𝑋)(1^{st} ‘𝑣)) × ((2^{nd} ‘𝑢)(Hom ‘𝑌)(2^{nd} ‘𝑣))) ⊆ (∪ ran
(Hom ‘𝑋) ×
∪ ran (Hom ‘𝑌))) |
53 | 48, 52 | mpbir 223 |
. . . . . . . . . . 11
⊢
(((1^{st} ‘𝑢)(Hom ‘𝑋)(1^{st} ‘𝑣)) × ((2^{nd} ‘𝑢)(Hom ‘𝑌)(2^{nd} ‘𝑣))) ∈ 𝒫 (∪ ran (Hom ‘𝑋) × ∪ ran
(Hom ‘𝑌)) |
54 | 53 | rgen2w 3106 |
. . . . . . . . . 10
⊢
∀𝑢 ∈
((Base‘𝑋) ×
(Base‘𝑌))∀𝑣 ∈ ((Base‘𝑋) × (Base‘𝑌))(((1^{st} ‘𝑢)(Hom ‘𝑋)(1^{st} ‘𝑣)) × ((2^{nd} ‘𝑢)(Hom ‘𝑌)(2^{nd} ‘𝑣))) ∈ 𝒫 (∪ ran (Hom ‘𝑋) × ∪ ran
(Hom ‘𝑌)) |
55 | | eqid 2799 |
. . . . . . . . . . 11
⊢ (𝑢 ∈ ((Base‘𝑋) × (Base‘𝑌)), 𝑣 ∈ ((Base‘𝑋) × (Base‘𝑌)) ↦ (((1^{st} ‘𝑢)(Hom ‘𝑋)(1^{st} ‘𝑣)) × ((2^{nd} ‘𝑢)(Hom ‘𝑌)(2^{nd} ‘𝑣)))) = (𝑢 ∈ ((Base‘𝑋) × (Base‘𝑌)), 𝑣 ∈ ((Base‘𝑋) × (Base‘𝑌)) ↦ (((1^{st} ‘𝑢)(Hom ‘𝑋)(1^{st} ‘𝑣)) × ((2^{nd} ‘𝑢)(Hom ‘𝑌)(2^{nd} ‘𝑣)))) |
56 | 55 | fmpt2 7473 |
. . . . . . . . . 10
⊢
(∀𝑢 ∈
((Base‘𝑋) ×
(Base‘𝑌))∀𝑣 ∈ ((Base‘𝑋) × (Base‘𝑌))(((1^{st} ‘𝑢)(Hom ‘𝑋)(1^{st} ‘𝑣)) × ((2^{nd} ‘𝑢)(Hom ‘𝑌)(2^{nd} ‘𝑣))) ∈ 𝒫 (∪ ran (Hom ‘𝑋) × ∪ ran
(Hom ‘𝑌)) ↔
(𝑢 ∈
((Base‘𝑋) ×
(Base‘𝑌)), 𝑣 ∈ ((Base‘𝑋) × (Base‘𝑌)) ↦ (((1^{st}
‘𝑢)(Hom ‘𝑋)(1^{st} ‘𝑣)) × ((2^{nd}
‘𝑢)(Hom ‘𝑌)(2^{nd} ‘𝑣)))):(((Base‘𝑋) × (Base‘𝑌)) × ((Base‘𝑋) × (Base‘𝑌)))⟶𝒫 (∪ ran (Hom ‘𝑋) × ∪ ran
(Hom ‘𝑌))) |
57 | 54, 56 | mpbi 222 |
. . . . . . . . 9
⊢ (𝑢 ∈ ((Base‘𝑋) × (Base‘𝑌)), 𝑣 ∈ ((Base‘𝑋) × (Base‘𝑌)) ↦ (((1^{st} ‘𝑢)(Hom ‘𝑋)(1^{st} ‘𝑣)) × ((2^{nd} ‘𝑢)(Hom ‘𝑌)(2^{nd} ‘𝑣)))):(((Base‘𝑋) × (Base‘𝑌)) × ((Base‘𝑋) × (Base‘𝑌)))⟶𝒫 (∪ ran (Hom ‘𝑋) × ∪ ran
(Hom ‘𝑌)) |
58 | 57 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → (𝑢 ∈ ((Base‘𝑋) × (Base‘𝑌)), 𝑣 ∈ ((Base‘𝑋) × (Base‘𝑌)) ↦ (((1^{st} ‘𝑢)(Hom ‘𝑋)(1^{st} ‘𝑣)) × ((2^{nd} ‘𝑢)(Hom ‘𝑌)(2^{nd} ‘𝑣)))):(((Base‘𝑋) × (Base‘𝑌)) × ((Base‘𝑋) × (Base‘𝑌)))⟶𝒫 (∪ ran (Hom ‘𝑋) × ∪ ran
(Hom ‘𝑌))) |
59 | 17, 36, 44, 58 | wunf 9837 |
. . . . . . 7
⊢ (𝜑 → (𝑢 ∈ ((Base‘𝑋) × (Base‘𝑌)), 𝑣 ∈ ((Base‘𝑋) × (Base‘𝑌)) ↦ (((1^{st} ‘𝑢)(Hom ‘𝑋)(1^{st} ‘𝑣)) × ((2^{nd} ‘𝑢)(Hom ‘𝑌)(2^{nd} ‘𝑣)))) ∈ 𝑈) |
60 | 13, 59 | syl5eqel 2882 |
. . . . . 6
⊢ (𝜑 → (Hom ‘𝑇) ∈ 𝑈) |
61 | 17, 35, 60 | wunop 9832 |
. . . . 5
⊢ (𝜑 → ⟨(Hom ‘ndx),
(Hom ‘𝑇)⟩ ∈
𝑈) |
62 | | df-cco 16292 |
. . . . . . 7
⊢ comp =
Slot ;15 |
63 | 62, 17, 20 | wunstr 16208 |
. . . . . 6
⊢ (𝜑 → (comp‘ndx) ∈
𝑈) |
64 | 17, 36, 32 | wunxp 9834 |
. . . . . . 7
⊢ (𝜑 → ((((Base‘𝑋) × (Base‘𝑌)) × ((Base‘𝑋) × (Base‘𝑌))) × ((Base‘𝑋) × (Base‘𝑌))) ∈ 𝑈) |
65 | 62, 17, 27 | wunstr 16208 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (comp‘𝑋) ∈ 𝑈) |
66 | 17, 65 | wunrn 9839 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ran (comp‘𝑋) ∈ 𝑈) |
67 | 17, 66 | wununi 9816 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∪ ran (comp‘𝑋) ∈ 𝑈) |
68 | 17, 67 | wunrn 9839 |
. . . . . . . . . . 11
⊢ (𝜑 → ran ∪ ran (comp‘𝑋) ∈ 𝑈) |
69 | 17, 68 | wununi 9816 |
. . . . . . . . . 10
⊢ (𝜑 → ∪ ran ∪ ran (comp‘𝑋) ∈ 𝑈) |
70 | 17, 69 | wunpw 9817 |
. . . . . . . . 9
⊢ (𝜑 → 𝒫 ∪ ran ∪ ran (comp‘𝑋) ∈ 𝑈) |
71 | 62, 17, 30 | wunstr 16208 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (comp‘𝑌) ∈ 𝑈) |
72 | 17, 71 | wunrn 9839 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ran (comp‘𝑌) ∈ 𝑈) |
73 | 17, 72 | wununi 9816 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∪ ran (comp‘𝑌) ∈ 𝑈) |
74 | 17, 73 | wunrn 9839 |
. . . . . . . . . . 11
⊢ (𝜑 → ran ∪ ran (comp‘𝑌) ∈ 𝑈) |
75 | 17, 74 | wununi 9816 |
. . . . . . . . . 10
⊢ (𝜑 → ∪ ran ∪ ran (comp‘𝑌) ∈ 𝑈) |
76 | 17, 75 | wunpw 9817 |
. . . . . . . . 9
⊢ (𝜑 → 𝒫 ∪ ran ∪ ran (comp‘𝑌) ∈ 𝑈) |
77 | 17, 70, 76 | wunxp 9834 |
. . . . . . . 8
⊢ (𝜑 → (𝒫 ∪ ran ∪ ran (comp‘𝑋) × 𝒫 ∪ ran ∪ ran (comp‘𝑌)) ∈ 𝑈) |
78 | 17, 60 | wunrn 9839 |
. . . . . . . . . 10
⊢ (𝜑 → ran (Hom ‘𝑇) ∈ 𝑈) |
79 | 17, 78 | wununi 9816 |
. . . . . . . . 9
⊢ (𝜑 → ∪ ran (Hom ‘𝑇) ∈ 𝑈) |
80 | 17, 79, 79 | wunxp 9834 |
. . . . . . . 8
⊢ (𝜑 → (∪ ran (Hom ‘𝑇) × ∪ ran
(Hom ‘𝑇)) ∈
𝑈) |
81 | 17, 77, 80 | wunpm 9835 |
. . . . . . 7
⊢ (𝜑 → ((𝒫 ∪ ran ∪ ran (comp‘𝑋) × 𝒫 ∪ ran ∪ ran (comp‘𝑌)) ↑_{pm}
(∪ ran (Hom ‘𝑇) × ∪ ran
(Hom ‘𝑇))) ∈
𝑈) |
82 | | fvex 6424 |
. . . . . . . . . . . . . . . . 17
⊢
(comp‘𝑋)
∈ V |
83 | 82 | rnex 7335 |
. . . . . . . . . . . . . . . 16
⊢ ran
(comp‘𝑋) ∈
V |
84 | 83 | uniex 7187 |
. . . . . . . . . . . . . . 15
⊢ ∪ ran (comp‘𝑋) ∈ V |
85 | 84 | rnex 7335 |
. . . . . . . . . . . . . 14
⊢ ran ∪ ran (comp‘𝑋) ∈ V |
86 | 85 | uniex 7187 |
. . . . . . . . . . . . 13
⊢ ∪ ran ∪ ran (comp‘𝑋) ∈ V |
87 | 86 | pwex 5050 |
. . . . . . . . . . . 12
⊢ 𝒫
∪ ran ∪ ran
(comp‘𝑋) ∈
V |
88 | | fvex 6424 |
. . . . . . . . . . . . . . . . 17
⊢
(comp‘𝑌)
∈ V |
89 | 88 | rnex 7335 |
. . . . . . . . . . . . . . . 16
⊢ ran
(comp‘𝑌) ∈
V |
90 | 89 | uniex 7187 |
. . . . . . . . . . . . . . 15
⊢ ∪ ran (comp‘𝑌) ∈ V |
91 | 90 | rnex 7335 |
. . . . . . . . . . . . . 14
⊢ ran ∪ ran (comp‘𝑌) ∈ V |
92 | 91 | uniex 7187 |
. . . . . . . . . . . . 13
⊢ ∪ ran ∪ ran (comp‘𝑌) ∈ V |
93 | 92 | pwex 5050 |
. . . . . . . . . . . 12
⊢ 𝒫
∪ ran ∪ ran
(comp‘𝑌) ∈
V |
94 | 87, 93 | xpex 7196 |
. . . . . . . . . . 11
⊢
(𝒫 ∪ ran ∪
ran (comp‘𝑋) ×
𝒫 ∪ ran ∪ ran
(comp‘𝑌)) ∈
V |
95 | | fvex 6424 |
. . . . . . . . . . . . . 14
⊢ (Hom
‘𝑇) ∈
V |
96 | 95 | rnex 7335 |
. . . . . . . . . . . . 13
⊢ ran (Hom
‘𝑇) ∈
V |
97 | 96 | uniex 7187 |
. . . . . . . . . . . 12
⊢ ∪ ran (Hom ‘𝑇) ∈ V |
98 | 97, 97 | xpex 7196 |
. . . . . . . . . . 11
⊢ (∪ ran (Hom ‘𝑇) × ∪ ran
(Hom ‘𝑇)) ∈
V |
99 | | ovssunirn 6913 |
. . . . . . . . . . . . . . . 16
⊢
((1^{st} ‘𝑔)(⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑋)(1^{st} ‘𝑦))(1^{st} ‘𝑓)) ⊆ ∪ ran
(⟨(1^{st} ‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑋)(1^{st} ‘𝑦)) |
100 | | ovssunirn 6913 |
. . . . . . . . . . . . . . . . 17
⊢
(⟨(1^{st} ‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑋)(1^{st} ‘𝑦)) ⊆ ∪ ran
(comp‘𝑋) |
101 | | rnss 5557 |
. . . . . . . . . . . . . . . . 17
⊢
((⟨(1^{st} ‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑋)(1^{st} ‘𝑦)) ⊆ ∪ ran
(comp‘𝑋) → ran
(⟨(1^{st} ‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑋)(1^{st} ‘𝑦)) ⊆ ran ∪
ran (comp‘𝑋)) |
102 | | uniss 4651 |
. . . . . . . . . . . . . . . . 17
⊢ (ran
(⟨(1^{st} ‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑋)(1^{st} ‘𝑦)) ⊆ ran ∪
ran (comp‘𝑋) →
∪ ran (⟨(1^{st} ‘(1^{st}
‘𝑥)), (1^{st}
‘(2^{nd} ‘𝑥))⟩(comp‘𝑋)(1^{st} ‘𝑦)) ⊆ ∪ ran
∪ ran (comp‘𝑋)) |
103 | 100, 101,
102 | mp2b 10 |
. . . . . . . . . . . . . . . 16
⊢ ∪ ran (⟨(1^{st} ‘(1^{st}
‘𝑥)), (1^{st}
‘(2^{nd} ‘𝑥))⟩(comp‘𝑋)(1^{st} ‘𝑦)) ⊆ ∪ ran
∪ ran (comp‘𝑋) |
104 | 99, 103 | sstri 3807 |
. . . . . . . . . . . . . . 15
⊢
((1^{st} ‘𝑔)(⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑋)(1^{st} ‘𝑦))(1^{st} ‘𝑓)) ⊆ ∪ ran
∪ ran (comp‘𝑋) |
105 | | ovex 6910 |
. . . . . . . . . . . . . . . 16
⊢
((1^{st} ‘𝑔)(⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑋)(1^{st} ‘𝑦))(1^{st} ‘𝑓)) ∈ V |
106 | 105 | elpw 4355 |
. . . . . . . . . . . . . . 15
⊢
(((1^{st} ‘𝑔)(⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑋)(1^{st} ‘𝑦))(1^{st} ‘𝑓)) ∈ 𝒫 ∪ ran ∪ ran (comp‘𝑋) ↔ ((1^{st}
‘𝑔)(⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑋)(1^{st} ‘𝑦))(1^{st} ‘𝑓)) ⊆ ∪ ran
∪ ran (comp‘𝑋)) |
107 | 104, 106 | mpbir 223 |
. . . . . . . . . . . . . 14
⊢
((1^{st} ‘𝑔)(⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑋)(1^{st} ‘𝑦))(1^{st} ‘𝑓)) ∈ 𝒫 ∪ ran ∪ ran (comp‘𝑋) |
108 | | ovssunirn 6913 |
. . . . . . . . . . . . . . . 16
⊢
((2^{nd} ‘𝑔)(⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑌)(2^{nd} ‘𝑦))(2^{nd} ‘𝑓)) ⊆ ∪ ran
(⟨(2^{nd} ‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑌)(2^{nd} ‘𝑦)) |
109 | | ovssunirn 6913 |
. . . . . . . . . . . . . . . . 17
⊢
(⟨(2^{nd} ‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑌)(2^{nd} ‘𝑦)) ⊆ ∪ ran
(comp‘𝑌) |
110 | | rnss 5557 |
. . . . . . . . . . . . . . . . 17
⊢
((⟨(2^{nd} ‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑌)(2^{nd} ‘𝑦)) ⊆ ∪ ran
(comp‘𝑌) → ran
(⟨(2^{nd} ‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑌)(2^{nd} ‘𝑦)) ⊆ ran ∪
ran (comp‘𝑌)) |
111 | | uniss 4651 |
. . . . . . . . . . . . . . . . 17
⊢ (ran
(⟨(2^{nd} ‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑌)(2^{nd} ‘𝑦)) ⊆ ran ∪
ran (comp‘𝑌) →
∪ ran (⟨(2^{nd} ‘(1^{st}
‘𝑥)), (2^{nd}
‘(2^{nd} ‘𝑥))⟩(comp‘𝑌)(2^{nd} ‘𝑦)) ⊆ ∪ ran
∪ ran (comp‘𝑌)) |
112 | 109, 110,
111 | mp2b 10 |
. . . . . . . . . . . . . . . 16
⊢ ∪ ran (⟨(2^{nd} ‘(1^{st}
‘𝑥)), (2^{nd}
‘(2^{nd} ‘𝑥))⟩(comp‘𝑌)(2^{nd} ‘𝑦)) ⊆ ∪ ran
∪ ran (comp‘𝑌) |
113 | 108, 112 | sstri 3807 |
. . . . . . . . . . . . . . 15
⊢
((2^{nd} ‘𝑔)(⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑌)(2^{nd} ‘𝑦))(2^{nd} ‘𝑓)) ⊆ ∪ ran
∪ ran (comp‘𝑌) |
114 | | ovex 6910 |
. . . . . . . . . . . . . . . 16
⊢
((2^{nd} ‘𝑔)(⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑌)(2^{nd} ‘𝑦))(2^{nd} ‘𝑓)) ∈ V |
115 | 114 | elpw 4355 |
. . . . . . . . . . . . . . 15
⊢
(((2^{nd} ‘𝑔)(⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑌)(2^{nd} ‘𝑦))(2^{nd} ‘𝑓)) ∈ 𝒫 ∪ ran ∪ ran (comp‘𝑌) ↔ ((2^{nd}
‘𝑔)(⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑌)(2^{nd} ‘𝑦))(2^{nd} ‘𝑓)) ⊆ ∪ ran
∪ ran (comp‘𝑌)) |
116 | 113, 115 | mpbir 223 |
. . . . . . . . . . . . . 14
⊢
((2^{nd} ‘𝑔)(⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑌)(2^{nd} ‘𝑦))(2^{nd} ‘𝑓)) ∈ 𝒫 ∪ ran ∪ ran (comp‘𝑌) |
117 | | opelxpi 5349 |
. . . . . . . . . . . . . 14
⊢
((((1^{st} ‘𝑔)(⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑋)(1^{st} ‘𝑦))(1^{st} ‘𝑓)) ∈ 𝒫 ∪ ran ∪ ran (comp‘𝑋) ∧ ((2^{nd}
‘𝑔)(⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑌)(2^{nd} ‘𝑦))(2^{nd} ‘𝑓)) ∈ 𝒫 ∪ ran ∪ ran (comp‘𝑌)) → ⟨((1^{st}
‘𝑔)(⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑋)(1^{st} ‘𝑦))(1^{st} ‘𝑓)), ((2^{nd} ‘𝑔)(⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑌)(2^{nd} ‘𝑦))(2^{nd} ‘𝑓))⟩ ∈ (𝒫 ∪ ran ∪ ran (comp‘𝑋) × 𝒫 ∪ ran ∪ ran (comp‘𝑌))) |
118 | 107, 116,
117 | mp2an 684 |
. . . . . . . . . . . . 13
⊢
⟨((1^{st} ‘𝑔)(⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑋)(1^{st} ‘𝑦))(1^{st} ‘𝑓)), ((2^{nd} ‘𝑔)(⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑌)(2^{nd} ‘𝑦))(2^{nd} ‘𝑓))⟩ ∈ (𝒫 ∪ ran ∪ ran (comp‘𝑋) × 𝒫 ∪ ran ∪ ran (comp‘𝑌)) |
119 | 118 | rgen2w 3106 |
. . . . . . . . . . . 12
⊢
∀𝑔 ∈
((2^{nd} ‘𝑥)(Hom ‘𝑇)𝑦)∀𝑓 ∈ ((Hom ‘𝑇)‘𝑥)⟨((1^{st} ‘𝑔)(⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑋)(1^{st} ‘𝑦))(1^{st} ‘𝑓)), ((2^{nd} ‘𝑔)(⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑌)(2^{nd} ‘𝑦))(2^{nd} ‘𝑓))⟩ ∈ (𝒫 ∪ ran ∪ ran (comp‘𝑋) × 𝒫 ∪ ran ∪ ran (comp‘𝑌)) |
120 | | eqid 2799 |
. . . . . . . . . . . . 13
⊢ (𝑔 ∈ ((2^{nd}
‘𝑥)(Hom ‘𝑇)𝑦), 𝑓 ∈ ((Hom ‘𝑇)‘𝑥) ↦ ⟨((1^{st} ‘𝑔)(⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑋)(1^{st} ‘𝑦))(1^{st} ‘𝑓)), ((2^{nd} ‘𝑔)(⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑌)(2^{nd} ‘𝑦))(2^{nd} ‘𝑓))⟩) = (𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝑇)𝑦), 𝑓 ∈ ((Hom ‘𝑇)‘𝑥) ↦ ⟨((1^{st} ‘𝑔)(⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑋)(1^{st} ‘𝑦))(1^{st} ‘𝑓)), ((2^{nd} ‘𝑔)(⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑌)(2^{nd} ‘𝑦))(2^{nd} ‘𝑓))⟩) |
121 | 120 | fmpt2 7473 |
. . . . . . . . . . . 12
⊢
(∀𝑔 ∈
((2^{nd} ‘𝑥)(Hom ‘𝑇)𝑦)∀𝑓 ∈ ((Hom ‘𝑇)‘𝑥)⟨((1^{st} ‘𝑔)(⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑋)(1^{st} ‘𝑦))(1^{st} ‘𝑓)), ((2^{nd} ‘𝑔)(⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑌)(2^{nd} ‘𝑦))(2^{nd} ‘𝑓))⟩ ∈ (𝒫 ∪ ran ∪ ran (comp‘𝑋) × 𝒫 ∪ ran ∪ ran (comp‘𝑌)) ↔ (𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝑇)𝑦), 𝑓 ∈ ((Hom ‘𝑇)‘𝑥) ↦ ⟨((1^{st} ‘𝑔)(⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑋)(1^{st} ‘𝑦))(1^{st} ‘𝑓)), ((2^{nd} ‘𝑔)(⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑌)(2^{nd} ‘𝑦))(2^{nd} ‘𝑓))⟩):(((2^{nd} ‘𝑥)(Hom ‘𝑇)𝑦) × ((Hom ‘𝑇)‘𝑥))⟶(𝒫 ∪ ran ∪ ran (comp‘𝑋) × 𝒫 ∪ ran ∪ ran (comp‘𝑌))) |
122 | 119, 121 | mpbi 222 |
. . . . . . . . . . 11
⊢ (𝑔 ∈ ((2^{nd}
‘𝑥)(Hom ‘𝑇)𝑦), 𝑓 ∈ ((Hom ‘𝑇)‘𝑥) ↦ ⟨((1^{st} ‘𝑔)(⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑋)(1^{st} ‘𝑦))(1^{st} ‘𝑓)), ((2^{nd} ‘𝑔)(⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑌)(2^{nd} ‘𝑦))(2^{nd} ‘𝑓))⟩):(((2^{nd} ‘𝑥)(Hom ‘𝑇)𝑦) × ((Hom ‘𝑇)‘𝑥))⟶(𝒫 ∪ ran ∪ ran (comp‘𝑋) × 𝒫 ∪ ran ∪ ran (comp‘𝑌)) |
123 | | ovssunirn 6913 |
. . . . . . . . . . . 12
⊢
((2^{nd} ‘𝑥)(Hom ‘𝑇)𝑦) ⊆ ∪ ran
(Hom ‘𝑇) |
124 | | fvssunirn 6440 |
. . . . . . . . . . . 12
⊢ ((Hom
‘𝑇)‘𝑥) ⊆ ∪ ran (Hom ‘𝑇) |
125 | | xpss12 5327 |
. . . . . . . . . . . 12
⊢
((((2^{nd} ‘𝑥)(Hom ‘𝑇)𝑦) ⊆ ∪ ran
(Hom ‘𝑇) ∧ ((Hom
‘𝑇)‘𝑥) ⊆ ∪ ran (Hom ‘𝑇)) → (((2^{nd} ‘𝑥)(Hom ‘𝑇)𝑦) × ((Hom ‘𝑇)‘𝑥)) ⊆ (∪ ran
(Hom ‘𝑇) ×
∪ ran (Hom ‘𝑇))) |
126 | 123, 124,
125 | mp2an 684 |
. . . . . . . . . . 11
⊢
(((2^{nd} ‘𝑥)(Hom ‘𝑇)𝑦) × ((Hom ‘𝑇)‘𝑥)) ⊆ (∪ ran
(Hom ‘𝑇) ×
∪ ran (Hom ‘𝑇)) |
127 | | elpm2r 8113 |
. . . . . . . . . . 11
⊢
((((𝒫 ∪ ran ∪ ran (comp‘𝑋) × 𝒫 ∪ ran ∪ ran (comp‘𝑌)) ∈ V ∧ (∪ ran (Hom ‘𝑇) × ∪ ran
(Hom ‘𝑇)) ∈ V)
∧ ((𝑔 ∈
((2^{nd} ‘𝑥)(Hom ‘𝑇)𝑦), 𝑓 ∈ ((Hom ‘𝑇)‘𝑥) ↦ ⟨((1^{st} ‘𝑔)(⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑋)(1^{st} ‘𝑦))(1^{st} ‘𝑓)), ((2^{nd} ‘𝑔)(⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑌)(2^{nd} ‘𝑦))(2^{nd} ‘𝑓))⟩):(((2^{nd} ‘𝑥)(Hom ‘𝑇)𝑦) × ((Hom ‘𝑇)‘𝑥))⟶(𝒫 ∪ ran ∪ ran (comp‘𝑋) × 𝒫 ∪ ran ∪ ran (comp‘𝑌)) ∧ (((2^{nd}
‘𝑥)(Hom ‘𝑇)𝑦) × ((Hom ‘𝑇)‘𝑥)) ⊆ (∪ ran
(Hom ‘𝑇) ×
∪ ran (Hom ‘𝑇)))) → (𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝑇)𝑦), 𝑓 ∈ ((Hom ‘𝑇)‘𝑥) ↦ ⟨((1^{st} ‘𝑔)(⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑋)(1^{st} ‘𝑦))(1^{st} ‘𝑓)), ((2^{nd} ‘𝑔)(⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑌)(2^{nd} ‘𝑦))(2^{nd} ‘𝑓))⟩) ∈ ((𝒫 ∪ ran ∪ ran (comp‘𝑋) × 𝒫 ∪ ran ∪ ran (comp‘𝑌)) ↑_{pm}
(∪ ran (Hom ‘𝑇) × ∪ ran
(Hom ‘𝑇)))) |
128 | 94, 98, 122, 126, 127 | mp4an 685 |
. . . . . . . . . 10
⊢ (𝑔 ∈ ((2^{nd}
‘𝑥)(Hom ‘𝑇)𝑦), 𝑓 ∈ ((Hom ‘𝑇)‘𝑥) ↦ ⟨((1^{st} ‘𝑔)(⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑋)(1^{st} ‘𝑦))(1^{st} ‘𝑓)), ((2^{nd} ‘𝑔)(⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑌)(2^{nd} ‘𝑦))(2^{nd} ‘𝑓))⟩) ∈ ((𝒫 ∪ ran ∪ ran (comp‘𝑋) × 𝒫 ∪ ran ∪ ran (comp‘𝑌)) ↑_{pm}
(∪ ran (Hom ‘𝑇) × ∪ ran
(Hom ‘𝑇))) |
129 | 128 | rgen2w 3106 |
. . . . . . . . 9
⊢
∀𝑥 ∈
(((Base‘𝑋) ×
(Base‘𝑌)) ×
((Base‘𝑋) ×
(Base‘𝑌)))∀𝑦 ∈ ((Base‘𝑋) × (Base‘𝑌))(𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝑇)𝑦), 𝑓 ∈ ((Hom ‘𝑇)‘𝑥) ↦ ⟨((1^{st} ‘𝑔)(⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑋)(1^{st} ‘𝑦))(1^{st} ‘𝑓)), ((2^{nd} ‘𝑔)(⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑌)(2^{nd} ‘𝑦))(2^{nd} ‘𝑓))⟩) ∈ ((𝒫 ∪ ran ∪ ran (comp‘𝑋) × 𝒫 ∪ ran ∪ ran (comp‘𝑌)) ↑_{pm}
(∪ ran (Hom ‘𝑇) × ∪ ran
(Hom ‘𝑇))) |
130 | | eqid 2799 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (((Base‘𝑋) × (Base‘𝑌)) × ((Base‘𝑋) × (Base‘𝑌))), 𝑦 ∈ ((Base‘𝑋) × (Base‘𝑌)) ↦ (𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝑇)𝑦), 𝑓 ∈ ((Hom ‘𝑇)‘𝑥) ↦ ⟨((1^{st} ‘𝑔)(⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑋)(1^{st} ‘𝑦))(1^{st} ‘𝑓)), ((2^{nd} ‘𝑔)(⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑌)(2^{nd} ‘𝑦))(2^{nd} ‘𝑓))⟩)) = (𝑥 ∈ (((Base‘𝑋) × (Base‘𝑌)) × ((Base‘𝑋) × (Base‘𝑌))), 𝑦 ∈ ((Base‘𝑋) × (Base‘𝑌)) ↦ (𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝑇)𝑦), 𝑓 ∈ ((Hom ‘𝑇)‘𝑥) ↦ ⟨((1^{st} ‘𝑔)(⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑋)(1^{st} ‘𝑦))(1^{st} ‘𝑓)), ((2^{nd} ‘𝑔)(⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑌)(2^{nd} ‘𝑦))(2^{nd} ‘𝑓))⟩)) |
131 | 130 | fmpt2 7473 |
. . . . . . . . 9
⊢
(∀𝑥 ∈
(((Base‘𝑋) ×
(Base‘𝑌)) ×
((Base‘𝑋) ×
(Base‘𝑌)))∀𝑦 ∈ ((Base‘𝑋) × (Base‘𝑌))(𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝑇)𝑦), 𝑓 ∈ ((Hom ‘𝑇)‘𝑥) ↦ ⟨((1^{st} ‘𝑔)(⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑋)(1^{st} ‘𝑦))(1^{st} ‘𝑓)), ((2^{nd} ‘𝑔)(⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑌)(2^{nd} ‘𝑦))(2^{nd} ‘𝑓))⟩) ∈ ((𝒫 ∪ ran ∪ ran (comp‘𝑋) × 𝒫 ∪ ran ∪ ran (comp‘𝑌)) ↑_{pm}
(∪ ran (Hom ‘𝑇) × ∪ ran
(Hom ‘𝑇))) ↔
(𝑥 ∈
(((Base‘𝑋) ×
(Base‘𝑌)) ×
((Base‘𝑋) ×
(Base‘𝑌))), 𝑦 ∈ ((Base‘𝑋) × (Base‘𝑌)) ↦ (𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝑇)𝑦), 𝑓 ∈ ((Hom ‘𝑇)‘𝑥) ↦ ⟨((1^{st} ‘𝑔)(⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑋)(1^{st} ‘𝑦))(1^{st} ‘𝑓)), ((2^{nd} ‘𝑔)(⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑌)(2^{nd} ‘𝑦))(2^{nd} ‘𝑓))⟩)):((((Base‘𝑋) × (Base‘𝑌)) × ((Base‘𝑋) × (Base‘𝑌))) × ((Base‘𝑋) × (Base‘𝑌)))⟶((𝒫 ∪ ran ∪ ran (comp‘𝑋) × 𝒫 ∪ ran ∪ ran (comp‘𝑌)) ↑_{pm}
(∪ ran (Hom ‘𝑇) × ∪ ran
(Hom ‘𝑇)))) |
132 | 129, 131 | mpbi 222 |
. . . . . . . 8
⊢ (𝑥 ∈ (((Base‘𝑋) × (Base‘𝑌)) × ((Base‘𝑋) × (Base‘𝑌))), 𝑦 ∈ ((Base‘𝑋) × (Base‘𝑌)) ↦ (𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝑇)𝑦), 𝑓 ∈ ((Hom ‘𝑇)‘𝑥) ↦ ⟨((1^{st} ‘𝑔)(⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑋)(1^{st} ‘𝑦))(1^{st} ‘𝑓)), ((2^{nd} ‘𝑔)(⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑌)(2^{nd} ‘𝑦))(2^{nd} ‘𝑓))⟩)):((((Base‘𝑋) × (Base‘𝑌)) × ((Base‘𝑋) × (Base‘𝑌))) × ((Base‘𝑋) × (Base‘𝑌)))⟶((𝒫 ∪ ran ∪ ran (comp‘𝑋) × 𝒫 ∪ ran ∪ ran (comp‘𝑌)) ↑_{pm}
(∪ ran (Hom ‘𝑇) × ∪ ran
(Hom ‘𝑇))) |
133 | 132 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ (((Base‘𝑋) × (Base‘𝑌)) × ((Base‘𝑋) × (Base‘𝑌))), 𝑦 ∈ ((Base‘𝑋) × (Base‘𝑌)) ↦ (𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝑇)𝑦), 𝑓 ∈ ((Hom ‘𝑇)‘𝑥) ↦ ⟨((1^{st} ‘𝑔)(⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑋)(1^{st} ‘𝑦))(1^{st} ‘𝑓)), ((2^{nd} ‘𝑔)(⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑌)(2^{nd} ‘𝑦))(2^{nd} ‘𝑓))⟩)):((((Base‘𝑋) × (Base‘𝑌)) × ((Base‘𝑋) × (Base‘𝑌))) × ((Base‘𝑋) × (Base‘𝑌)))⟶((𝒫 ∪ ran ∪ ran (comp‘𝑋) × 𝒫 ∪ ran ∪ ran (comp‘𝑌)) ↑_{pm}
(∪ ran (Hom ‘𝑇) × ∪ ran
(Hom ‘𝑇)))) |
134 | 17, 64, 81, 133 | wunf 9837 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (((Base‘𝑋) × (Base‘𝑌)) × ((Base‘𝑋) × (Base‘𝑌))), 𝑦 ∈ ((Base‘𝑋) × (Base‘𝑌)) ↦ (𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝑇)𝑦), 𝑓 ∈ ((Hom ‘𝑇)‘𝑥) ↦ ⟨((1^{st} ‘𝑔)(⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑋)(1^{st} ‘𝑦))(1^{st} ‘𝑓)), ((2^{nd} ‘𝑔)(⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑌)(2^{nd} ‘𝑦))(2^{nd} ‘𝑓))⟩)) ∈ 𝑈) |
135 | 17, 63, 134 | wunop 9832 |
. . . . 5
⊢ (𝜑 → ⟨(comp‘ndx),
(𝑥 ∈
(((Base‘𝑋) ×
(Base‘𝑌)) ×
((Base‘𝑋) ×
(Base‘𝑌))), 𝑦 ∈ ((Base‘𝑋) × (Base‘𝑌)) ↦ (𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝑇)𝑦), 𝑓 ∈ ((Hom ‘𝑇)‘𝑥) ↦ ⟨((1^{st} ‘𝑔)(⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑋)(1^{st} ‘𝑦))(1^{st} ‘𝑓)), ((2^{nd} ‘𝑔)(⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑌)(2^{nd} ‘𝑦))(2^{nd} ‘𝑓))⟩))⟩ ∈ 𝑈) |
136 | 17, 33, 61, 135 | wuntp 9821 |
. . . 4
⊢ (𝜑 → {⟨(Base‘ndx),
((Base‘𝑋) ×
(Base‘𝑌))⟩,
⟨(Hom ‘ndx), (Hom ‘𝑇)⟩, ⟨(comp‘ndx), (𝑥 ∈ (((Base‘𝑋) × (Base‘𝑌)) × ((Base‘𝑋) × (Base‘𝑌))), 𝑦 ∈ ((Base‘𝑋) × (Base‘𝑌)) ↦ (𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝑇)𝑦), 𝑓 ∈ ((Hom ‘𝑇)‘𝑥) ↦ ⟨((1^{st} ‘𝑔)(⟨(1^{st}
‘(1^{st} ‘𝑥)), (1^{st} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑋)(1^{st} ‘𝑦))(1^{st} ‘𝑓)), ((2^{nd} ‘𝑔)(⟨(2^{nd}
‘(1^{st} ‘𝑥)), (2^{nd} ‘(2^{nd}
‘𝑥))⟩(comp‘𝑌)(2^{nd} ‘𝑦))(2^{nd} ‘𝑓))⟩))⟩} ∈ 𝑈) |
137 | 16, 136 | eqeltrd 2878 |
. . 3
⊢ (𝜑 → 𝑇 ∈ 𝑈) |
138 | | inss2 4029 |
. . . . 5
⊢ (𝑈 ∩ Cat) ⊆
Cat |
139 | 138, 26 | sseldi 3796 |
. . . 4
⊢ (𝜑 → 𝑋 ∈ Cat) |
140 | 138, 29 | sseldi 3796 |
. . . 4
⊢ (𝜑 → 𝑌 ∈ Cat) |
141 | 1, 139, 140 | xpccat 17145 |
. . 3
⊢ (𝜑 → 𝑇 ∈ Cat) |
142 | 137, 141 | elind 3996 |
. 2
⊢ (𝜑 → 𝑇 ∈ (𝑈 ∩ Cat)) |
143 | 142, 25 | eleqtrrd 2881 |
1
⊢ (𝜑 → 𝑇 ∈ 𝐵) |