Step | Hyp | Ref
| Expression |
1 | | catcfuccl.o |
. . . . 5
⊢ 𝑄 = (𝑋 FuncCat 𝑌) |
2 | | eqid 2622 |
. . . . 5
⊢ (𝑋 Func 𝑌) = (𝑋 Func 𝑌) |
3 | | eqid 2622 |
. . . . 5
⊢ (𝑋 Nat 𝑌) = (𝑋 Nat 𝑌) |
4 | | eqid 2622 |
. . . . 5
⊢
(Base‘𝑋) =
(Base‘𝑋) |
5 | | eqid 2622 |
. . . . 5
⊢
(comp‘𝑌) =
(comp‘𝑌) |
6 | | inss2 3834 |
. . . . . 6
⊢ (𝑈 ∩ Cat) ⊆
Cat |
7 | | catcfuccl.x |
. . . . . . 7
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
8 | | catcfuccl.c |
. . . . . . . 8
⊢ 𝐶 = (CatCat‘𝑈) |
9 | | catcfuccl.b |
. . . . . . . 8
⊢ 𝐵 = (Base‘𝐶) |
10 | | catcfuccl.u |
. . . . . . . 8
⊢ (𝜑 → 𝑈 ∈ WUni) |
11 | 8, 9, 10 | catcbas 16747 |
. . . . . . 7
⊢ (𝜑 → 𝐵 = (𝑈 ∩ Cat)) |
12 | 7, 11 | eleqtrd 2703 |
. . . . . 6
⊢ (𝜑 → 𝑋 ∈ (𝑈 ∩ Cat)) |
13 | 6, 12 | sseldi 3601 |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ Cat) |
14 | | catcfuccl.y |
. . . . . . 7
⊢ (𝜑 → 𝑌 ∈ 𝐵) |
15 | 14, 11 | eleqtrd 2703 |
. . . . . 6
⊢ (𝜑 → 𝑌 ∈ (𝑈 ∩ Cat)) |
16 | 6, 15 | sseldi 3601 |
. . . . 5
⊢ (𝜑 → 𝑌 ∈ Cat) |
17 | | eqidd 2623 |
. . . . 5
⊢ (𝜑 → (𝑣 ∈ ((𝑋 Func 𝑌) × (𝑋 Func 𝑌)), ℎ ∈ (𝑋 Func 𝑌) ↦ ⦋(1st
‘𝑣) / 𝑓⦌⦋(2nd
‘𝑣) / 𝑔⦌(𝑏 ∈ (𝑔(𝑋 Nat 𝑌)ℎ), 𝑎 ∈ (𝑓(𝑋 Nat 𝑌)𝑔) ↦ (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏‘𝑥)(〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉(comp‘𝑌)((1st ‘ℎ)‘𝑥))(𝑎‘𝑥))))) = (𝑣 ∈ ((𝑋 Func 𝑌) × (𝑋 Func 𝑌)), ℎ ∈ (𝑋 Func 𝑌) ↦ ⦋(1st
‘𝑣) / 𝑓⦌⦋(2nd
‘𝑣) / 𝑔⦌(𝑏 ∈ (𝑔(𝑋 Nat 𝑌)ℎ), 𝑎 ∈ (𝑓(𝑋 Nat 𝑌)𝑔) ↦ (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏‘𝑥)(〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉(comp‘𝑌)((1st ‘ℎ)‘𝑥))(𝑎‘𝑥)))))) |
18 | 1, 2, 3, 4, 5, 13,
16, 17 | fucval 16618 |
. . . 4
⊢ (𝜑 → 𝑄 = {〈(Base‘ndx), (𝑋 Func 𝑌)〉, 〈(Hom ‘ndx), (𝑋 Nat 𝑌)〉, 〈(comp‘ndx), (𝑣 ∈ ((𝑋 Func 𝑌) × (𝑋 Func 𝑌)), ℎ ∈ (𝑋 Func 𝑌) ↦ ⦋(1st
‘𝑣) / 𝑓⦌⦋(2nd
‘𝑣) / 𝑔⦌(𝑏 ∈ (𝑔(𝑋 Nat 𝑌)ℎ), 𝑎 ∈ (𝑓(𝑋 Nat 𝑌)𝑔) ↦ (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏‘𝑥)(〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉(comp‘𝑌)((1st ‘ℎ)‘𝑥))(𝑎‘𝑥)))))〉}) |
19 | | df-base 15863 |
. . . . . . 7
⊢ Base =
Slot 1 |
20 | | catcfuccl.1 |
. . . . . . . 8
⊢ (𝜑 → ω ∈ 𝑈) |
21 | 10, 20 | wunndx 15878 |
. . . . . . 7
⊢ (𝜑 → ndx ∈ 𝑈) |
22 | 19, 10, 21 | wunstr 15881 |
. . . . . 6
⊢ (𝜑 → (Base‘ndx) ∈
𝑈) |
23 | | inss1 3833 |
. . . . . . . 8
⊢ (𝑈 ∩ Cat) ⊆ 𝑈 |
24 | 23, 12 | sseldi 3601 |
. . . . . . 7
⊢ (𝜑 → 𝑋 ∈ 𝑈) |
25 | 23, 15 | sseldi 3601 |
. . . . . . 7
⊢ (𝜑 → 𝑌 ∈ 𝑈) |
26 | 10, 24, 25 | wunfunc 16559 |
. . . . . 6
⊢ (𝜑 → (𝑋 Func 𝑌) ∈ 𝑈) |
27 | 10, 22, 26 | wunop 9544 |
. . . . 5
⊢ (𝜑 → 〈(Base‘ndx),
(𝑋 Func 𝑌)〉 ∈ 𝑈) |
28 | | df-hom 15966 |
. . . . . . 7
⊢ Hom =
Slot ;14 |
29 | 28, 10, 21 | wunstr 15881 |
. . . . . 6
⊢ (𝜑 → (Hom ‘ndx) ∈
𝑈) |
30 | 10, 24, 25 | wunnat 16616 |
. . . . . 6
⊢ (𝜑 → (𝑋 Nat 𝑌) ∈ 𝑈) |
31 | 10, 29, 30 | wunop 9544 |
. . . . 5
⊢ (𝜑 → 〈(Hom ‘ndx),
(𝑋 Nat 𝑌)〉 ∈ 𝑈) |
32 | | df-cco 15967 |
. . . . . . 7
⊢ comp =
Slot ;15 |
33 | 32, 10, 21 | wunstr 15881 |
. . . . . 6
⊢ (𝜑 → (comp‘ndx) ∈
𝑈) |
34 | 10, 26, 26 | wunxp 9546 |
. . . . . . . 8
⊢ (𝜑 → ((𝑋 Func 𝑌) × (𝑋 Func 𝑌)) ∈ 𝑈) |
35 | 10, 34, 26 | wunxp 9546 |
. . . . . . 7
⊢ (𝜑 → (((𝑋 Func 𝑌) × (𝑋 Func 𝑌)) × (𝑋 Func 𝑌)) ∈ 𝑈) |
36 | 32, 10, 25 | wunstr 15881 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (comp‘𝑌) ∈ 𝑈) |
37 | 10, 36 | wunrn 9551 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ran (comp‘𝑌) ∈ 𝑈) |
38 | 10, 37 | wununi 9528 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∪ ran (comp‘𝑌) ∈ 𝑈) |
39 | 10, 38 | wunrn 9551 |
. . . . . . . . . . 11
⊢ (𝜑 → ran ∪ ran (comp‘𝑌) ∈ 𝑈) |
40 | 10, 39 | wununi 9528 |
. . . . . . . . . 10
⊢ (𝜑 → ∪ ran ∪ ran (comp‘𝑌) ∈ 𝑈) |
41 | 10, 40 | wunpw 9529 |
. . . . . . . . 9
⊢ (𝜑 → 𝒫 ∪ ran ∪ ran (comp‘𝑌) ∈ 𝑈) |
42 | 19, 10, 24 | wunstr 15881 |
. . . . . . . . 9
⊢ (𝜑 → (Base‘𝑋) ∈ 𝑈) |
43 | 10, 41, 42 | wunmap 9548 |
. . . . . . . 8
⊢ (𝜑 → (𝒫 ∪ ran ∪ ran (comp‘𝑌) ↑𝑚
(Base‘𝑋)) ∈
𝑈) |
44 | 10, 30 | wunrn 9551 |
. . . . . . . . . 10
⊢ (𝜑 → ran (𝑋 Nat 𝑌) ∈ 𝑈) |
45 | 10, 44 | wununi 9528 |
. . . . . . . . 9
⊢ (𝜑 → ∪ ran (𝑋 Nat 𝑌) ∈ 𝑈) |
46 | 10, 45, 45 | wunxp 9546 |
. . . . . . . 8
⊢ (𝜑 → (∪ ran (𝑋 Nat 𝑌) × ∪ ran
(𝑋 Nat 𝑌)) ∈ 𝑈) |
47 | 10, 43, 46 | wunpm 9547 |
. . . . . . 7
⊢ (𝜑 → ((𝒫 ∪ ran ∪ ran (comp‘𝑌) ↑𝑚
(Base‘𝑋))
↑pm (∪ ran (𝑋 Nat 𝑌) × ∪ ran
(𝑋 Nat 𝑌))) ∈ 𝑈) |
48 | | fvex 6201 |
. . . . . . . . . . 11
⊢
(1st ‘𝑣) ∈ V |
49 | | fvex 6201 |
. . . . . . . . . . . . . 14
⊢
(2nd ‘𝑣) ∈ V |
50 | | ovex 6678 |
. . . . . . . . . . . . . . . . 17
⊢
(𝒫 ∪ ran ∪
ran (comp‘𝑌)
↑𝑚 (Base‘𝑋)) ∈ V |
51 | | ovex 6678 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑋 Nat 𝑌) ∈ V |
52 | 51 | rnex 7100 |
. . . . . . . . . . . . . . . . . . 19
⊢ ran
(𝑋 Nat 𝑌) ∈ V |
53 | 52 | uniex 6953 |
. . . . . . . . . . . . . . . . . 18
⊢ ∪ ran (𝑋 Nat 𝑌) ∈ V |
54 | 53, 53 | xpex 6962 |
. . . . . . . . . . . . . . . . 17
⊢ (∪ ran (𝑋 Nat 𝑌) × ∪ ran
(𝑋 Nat 𝑌)) ∈ V |
55 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏‘𝑥)(〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉(comp‘𝑌)((1st ‘ℎ)‘𝑥))(𝑎‘𝑥))) = (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏‘𝑥)(〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉(comp‘𝑌)((1st ‘ℎ)‘𝑥))(𝑎‘𝑥))) |
56 | | ovssunirn 6681 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑏‘𝑥)(〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉(comp‘𝑌)((1st ‘ℎ)‘𝑥))(𝑎‘𝑥)) ⊆ ∪ ran
(〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉(comp‘𝑌)((1st ‘ℎ)‘𝑥)) |
57 | | ovssunirn 6681 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉(comp‘𝑌)((1st ‘ℎ)‘𝑥)) ⊆ ∪ ran
(comp‘𝑌) |
58 | | rnss 5354 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉(comp‘𝑌)((1st ‘ℎ)‘𝑥)) ⊆ ∪ ran
(comp‘𝑌) → ran
(〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉(comp‘𝑌)((1st ‘ℎ)‘𝑥)) ⊆ ran ∪
ran (comp‘𝑌)) |
59 | | uniss 4458 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (ran
(〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉(comp‘𝑌)((1st ‘ℎ)‘𝑥)) ⊆ ran ∪
ran (comp‘𝑌) →
∪ ran (〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉(comp‘𝑌)((1st ‘ℎ)‘𝑥)) ⊆ ∪ ran
∪ ran (comp‘𝑌)) |
60 | 57, 58, 59 | mp2b 10 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ∪ ran (〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉(comp‘𝑌)((1st ‘ℎ)‘𝑥)) ⊆ ∪ ran
∪ ran (comp‘𝑌) |
61 | 56, 60 | sstri 3612 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑏‘𝑥)(〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉(comp‘𝑌)((1st ‘ℎ)‘𝑥))(𝑎‘𝑥)) ⊆ ∪ ran
∪ ran (comp‘𝑌) |
62 | | ovex 6678 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑏‘𝑥)(〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉(comp‘𝑌)((1st ‘ℎ)‘𝑥))(𝑎‘𝑥)) ∈ V |
63 | 62 | elpw 4164 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑏‘𝑥)(〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉(comp‘𝑌)((1st ‘ℎ)‘𝑥))(𝑎‘𝑥)) ∈ 𝒫 ∪ ran ∪ ran (comp‘𝑌) ↔ ((𝑏‘𝑥)(〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉(comp‘𝑌)((1st ‘ℎ)‘𝑥))(𝑎‘𝑥)) ⊆ ∪ ran
∪ ran (comp‘𝑌)) |
64 | 61, 63 | mpbir 221 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑏‘𝑥)(〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉(comp‘𝑌)((1st ‘ℎ)‘𝑥))(𝑎‘𝑥)) ∈ 𝒫 ∪ ran ∪ ran (comp‘𝑌) |
65 | 64 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ (Base‘𝑋) → ((𝑏‘𝑥)(〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉(comp‘𝑌)((1st ‘ℎ)‘𝑥))(𝑎‘𝑥)) ∈ 𝒫 ∪ ran ∪ ran (comp‘𝑌)) |
66 | 55, 65 | fmpti 6383 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏‘𝑥)(〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉(comp‘𝑌)((1st ‘ℎ)‘𝑥))(𝑎‘𝑥))):(Base‘𝑋)⟶𝒫 ∪ ran ∪ ran (comp‘𝑌) |
67 | | fvex 6201 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(comp‘𝑌)
∈ V |
68 | 67 | rnex 7100 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ran
(comp‘𝑌) ∈
V |
69 | 68 | uniex 6953 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ∪ ran (comp‘𝑌) ∈ V |
70 | 69 | rnex 7100 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ran ∪ ran (comp‘𝑌) ∈ V |
71 | 70 | uniex 6953 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ∪ ran ∪ ran (comp‘𝑌) ∈ V |
72 | 71 | pwex 4848 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝒫
∪ ran ∪ ran
(comp‘𝑌) ∈
V |
73 | | fvex 6201 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(Base‘𝑋)
∈ V |
74 | 72, 73 | elmap 7886 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ (Base‘𝑋) ↦ ((𝑏‘𝑥)(〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉(comp‘𝑌)((1st ‘ℎ)‘𝑥))(𝑎‘𝑥))) ∈ (𝒫 ∪ ran ∪ ran (comp‘𝑌) ↑𝑚
(Base‘𝑋)) ↔
(𝑥 ∈ (Base‘𝑋) ↦ ((𝑏‘𝑥)(〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉(comp‘𝑌)((1st ‘ℎ)‘𝑥))(𝑎‘𝑥))):(Base‘𝑋)⟶𝒫 ∪ ran ∪ ran (comp‘𝑌)) |
75 | 66, 74 | mpbir 221 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏‘𝑥)(〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉(comp‘𝑌)((1st ‘ℎ)‘𝑥))(𝑎‘𝑥))) ∈ (𝒫 ∪ ran ∪ ran (comp‘𝑌) ↑𝑚
(Base‘𝑋)) |
76 | 75 | rgen2w 2925 |
. . . . . . . . . . . . . . . . . 18
⊢
∀𝑏 ∈
(𝑔(𝑋 Nat 𝑌)ℎ)∀𝑎 ∈ (𝑓(𝑋 Nat 𝑌)𝑔)(𝑥 ∈ (Base‘𝑋) ↦ ((𝑏‘𝑥)(〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉(comp‘𝑌)((1st ‘ℎ)‘𝑥))(𝑎‘𝑥))) ∈ (𝒫 ∪ ran ∪ ran (comp‘𝑌) ↑𝑚
(Base‘𝑋)) |
77 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑏 ∈ (𝑔(𝑋 Nat 𝑌)ℎ), 𝑎 ∈ (𝑓(𝑋 Nat 𝑌)𝑔) ↦ (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏‘𝑥)(〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉(comp‘𝑌)((1st ‘ℎ)‘𝑥))(𝑎‘𝑥)))) = (𝑏 ∈ (𝑔(𝑋 Nat 𝑌)ℎ), 𝑎 ∈ (𝑓(𝑋 Nat 𝑌)𝑔) ↦ (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏‘𝑥)(〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉(comp‘𝑌)((1st ‘ℎ)‘𝑥))(𝑎‘𝑥)))) |
78 | 77 | fmpt2 7237 |
. . . . . . . . . . . . . . . . . 18
⊢
(∀𝑏 ∈
(𝑔(𝑋 Nat 𝑌)ℎ)∀𝑎 ∈ (𝑓(𝑋 Nat 𝑌)𝑔)(𝑥 ∈ (Base‘𝑋) ↦ ((𝑏‘𝑥)(〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉(comp‘𝑌)((1st ‘ℎ)‘𝑥))(𝑎‘𝑥))) ∈ (𝒫 ∪ ran ∪ ran (comp‘𝑌) ↑𝑚
(Base‘𝑋)) ↔
(𝑏 ∈ (𝑔(𝑋 Nat 𝑌)ℎ), 𝑎 ∈ (𝑓(𝑋 Nat 𝑌)𝑔) ↦ (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏‘𝑥)(〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉(comp‘𝑌)((1st ‘ℎ)‘𝑥))(𝑎‘𝑥)))):((𝑔(𝑋 Nat 𝑌)ℎ) × (𝑓(𝑋 Nat 𝑌)𝑔))⟶(𝒫 ∪ ran ∪ ran (comp‘𝑌) ↑𝑚
(Base‘𝑋))) |
79 | 76, 78 | mpbi 220 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 ∈ (𝑔(𝑋 Nat 𝑌)ℎ), 𝑎 ∈ (𝑓(𝑋 Nat 𝑌)𝑔) ↦ (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏‘𝑥)(〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉(comp‘𝑌)((1st ‘ℎ)‘𝑥))(𝑎‘𝑥)))):((𝑔(𝑋 Nat 𝑌)ℎ) × (𝑓(𝑋 Nat 𝑌)𝑔))⟶(𝒫 ∪ ran ∪ ran (comp‘𝑌) ↑𝑚
(Base‘𝑋)) |
80 | | ovssunirn 6681 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑔(𝑋 Nat 𝑌)ℎ) ⊆ ∪ ran
(𝑋 Nat 𝑌) |
81 | | ovssunirn 6681 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓(𝑋 Nat 𝑌)𝑔) ⊆ ∪ ran
(𝑋 Nat 𝑌) |
82 | | xpss12 5225 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑔(𝑋 Nat 𝑌)ℎ) ⊆ ∪ ran
(𝑋 Nat 𝑌) ∧ (𝑓(𝑋 Nat 𝑌)𝑔) ⊆ ∪ ran
(𝑋 Nat 𝑌)) → ((𝑔(𝑋 Nat 𝑌)ℎ) × (𝑓(𝑋 Nat 𝑌)𝑔)) ⊆ (∪ ran
(𝑋 Nat 𝑌) × ∪ ran
(𝑋 Nat 𝑌))) |
83 | 80, 81, 82 | mp2an 708 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑔(𝑋 Nat 𝑌)ℎ) × (𝑓(𝑋 Nat 𝑌)𝑔)) ⊆ (∪ ran
(𝑋 Nat 𝑌) × ∪ ran
(𝑋 Nat 𝑌)) |
84 | | elpm2r 7875 |
. . . . . . . . . . . . . . . . 17
⊢
((((𝒫 ∪ ran ∪ ran (comp‘𝑌) ↑𝑚
(Base‘𝑋)) ∈ V
∧ (∪ ran (𝑋 Nat 𝑌) × ∪ ran
(𝑋 Nat 𝑌)) ∈ V) ∧ ((𝑏 ∈ (𝑔(𝑋 Nat 𝑌)ℎ), 𝑎 ∈ (𝑓(𝑋 Nat 𝑌)𝑔) ↦ (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏‘𝑥)(〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉(comp‘𝑌)((1st ‘ℎ)‘𝑥))(𝑎‘𝑥)))):((𝑔(𝑋 Nat 𝑌)ℎ) × (𝑓(𝑋 Nat 𝑌)𝑔))⟶(𝒫 ∪ ran ∪ ran (comp‘𝑌) ↑𝑚
(Base‘𝑋)) ∧
((𝑔(𝑋 Nat 𝑌)ℎ) × (𝑓(𝑋 Nat 𝑌)𝑔)) ⊆ (∪ ran
(𝑋 Nat 𝑌) × ∪ ran
(𝑋 Nat 𝑌)))) → (𝑏 ∈ (𝑔(𝑋 Nat 𝑌)ℎ), 𝑎 ∈ (𝑓(𝑋 Nat 𝑌)𝑔) ↦ (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏‘𝑥)(〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉(comp‘𝑌)((1st ‘ℎ)‘𝑥))(𝑎‘𝑥)))) ∈ ((𝒫 ∪ ran ∪ ran (comp‘𝑌) ↑𝑚
(Base‘𝑋))
↑pm (∪ ran (𝑋 Nat 𝑌) × ∪ ran
(𝑋 Nat 𝑌)))) |
85 | 50, 54, 79, 83, 84 | mp4an 709 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 ∈ (𝑔(𝑋 Nat 𝑌)ℎ), 𝑎 ∈ (𝑓(𝑋 Nat 𝑌)𝑔) ↦ (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏‘𝑥)(〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉(comp‘𝑌)((1st ‘ℎ)‘𝑥))(𝑎‘𝑥)))) ∈ ((𝒫 ∪ ran ∪ ran (comp‘𝑌) ↑𝑚
(Base‘𝑋))
↑pm (∪ ran (𝑋 Nat 𝑌) × ∪ ran
(𝑋 Nat 𝑌))) |
86 | 85 | sbcth 3450 |
. . . . . . . . . . . . . . 15
⊢
((2nd ‘𝑣) ∈ V → [(2nd
‘𝑣) / 𝑔](𝑏 ∈ (𝑔(𝑋 Nat 𝑌)ℎ), 𝑎 ∈ (𝑓(𝑋 Nat 𝑌)𝑔) ↦ (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏‘𝑥)(〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉(comp‘𝑌)((1st ‘ℎ)‘𝑥))(𝑎‘𝑥)))) ∈ ((𝒫 ∪ ran ∪ ran (comp‘𝑌) ↑𝑚
(Base‘𝑋))
↑pm (∪ ran (𝑋 Nat 𝑌) × ∪ ran
(𝑋 Nat 𝑌)))) |
87 | | sbcel1g 3987 |
. . . . . . . . . . . . . . 15
⊢
((2nd ‘𝑣) ∈ V → ([(2nd
‘𝑣) / 𝑔](𝑏 ∈ (𝑔(𝑋 Nat 𝑌)ℎ), 𝑎 ∈ (𝑓(𝑋 Nat 𝑌)𝑔) ↦ (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏‘𝑥)(〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉(comp‘𝑌)((1st ‘ℎ)‘𝑥))(𝑎‘𝑥)))) ∈ ((𝒫 ∪ ran ∪ ran (comp‘𝑌) ↑𝑚
(Base‘𝑋))
↑pm (∪ ran (𝑋 Nat 𝑌) × ∪ ran
(𝑋 Nat 𝑌))) ↔ ⦋(2nd
‘𝑣) / 𝑔⦌(𝑏 ∈ (𝑔(𝑋 Nat 𝑌)ℎ), 𝑎 ∈ (𝑓(𝑋 Nat 𝑌)𝑔) ↦ (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏‘𝑥)(〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉(comp‘𝑌)((1st ‘ℎ)‘𝑥))(𝑎‘𝑥)))) ∈ ((𝒫 ∪ ran ∪ ran (comp‘𝑌) ↑𝑚
(Base‘𝑋))
↑pm (∪ ran (𝑋 Nat 𝑌) × ∪ ran
(𝑋 Nat 𝑌))))) |
88 | 86, 87 | mpbid 222 |
. . . . . . . . . . . . . 14
⊢
((2nd ‘𝑣) ∈ V →
⦋(2nd ‘𝑣) / 𝑔⦌(𝑏 ∈ (𝑔(𝑋 Nat 𝑌)ℎ), 𝑎 ∈ (𝑓(𝑋 Nat 𝑌)𝑔) ↦ (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏‘𝑥)(〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉(comp‘𝑌)((1st ‘ℎ)‘𝑥))(𝑎‘𝑥)))) ∈ ((𝒫 ∪ ran ∪ ran (comp‘𝑌) ↑𝑚
(Base‘𝑋))
↑pm (∪ ran (𝑋 Nat 𝑌) × ∪ ran
(𝑋 Nat 𝑌)))) |
89 | 49, 88 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢
⦋(2nd ‘𝑣) / 𝑔⦌(𝑏 ∈ (𝑔(𝑋 Nat 𝑌)ℎ), 𝑎 ∈ (𝑓(𝑋 Nat 𝑌)𝑔) ↦ (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏‘𝑥)(〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉(comp‘𝑌)((1st ‘ℎ)‘𝑥))(𝑎‘𝑥)))) ∈ ((𝒫 ∪ ran ∪ ran (comp‘𝑌) ↑𝑚
(Base‘𝑋))
↑pm (∪ ran (𝑋 Nat 𝑌) × ∪ ran
(𝑋 Nat 𝑌))) |
90 | 89 | sbcth 3450 |
. . . . . . . . . . . 12
⊢
((1st ‘𝑣) ∈ V → [(1st
‘𝑣) / 𝑓]⦋(2nd
‘𝑣) / 𝑔⦌(𝑏 ∈ (𝑔(𝑋 Nat 𝑌)ℎ), 𝑎 ∈ (𝑓(𝑋 Nat 𝑌)𝑔) ↦ (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏‘𝑥)(〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉(comp‘𝑌)((1st ‘ℎ)‘𝑥))(𝑎‘𝑥)))) ∈ ((𝒫 ∪ ran ∪ ran (comp‘𝑌) ↑𝑚
(Base‘𝑋))
↑pm (∪ ran (𝑋 Nat 𝑌) × ∪ ran
(𝑋 Nat 𝑌)))) |
91 | | sbcel1g 3987 |
. . . . . . . . . . . 12
⊢
((1st ‘𝑣) ∈ V → ([(1st
‘𝑣) / 𝑓]⦋(2nd
‘𝑣) / 𝑔⦌(𝑏 ∈ (𝑔(𝑋 Nat 𝑌)ℎ), 𝑎 ∈ (𝑓(𝑋 Nat 𝑌)𝑔) ↦ (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏‘𝑥)(〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉(comp‘𝑌)((1st ‘ℎ)‘𝑥))(𝑎‘𝑥)))) ∈ ((𝒫 ∪ ran ∪ ran (comp‘𝑌) ↑𝑚
(Base‘𝑋))
↑pm (∪ ran (𝑋 Nat 𝑌) × ∪ ran
(𝑋 Nat 𝑌))) ↔ ⦋(1st
‘𝑣) / 𝑓⦌⦋(2nd
‘𝑣) / 𝑔⦌(𝑏 ∈ (𝑔(𝑋 Nat 𝑌)ℎ), 𝑎 ∈ (𝑓(𝑋 Nat 𝑌)𝑔) ↦ (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏‘𝑥)(〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉(comp‘𝑌)((1st ‘ℎ)‘𝑥))(𝑎‘𝑥)))) ∈ ((𝒫 ∪ ran ∪ ran (comp‘𝑌) ↑𝑚
(Base‘𝑋))
↑pm (∪ ran (𝑋 Nat 𝑌) × ∪ ran
(𝑋 Nat 𝑌))))) |
92 | 90, 91 | mpbid 222 |
. . . . . . . . . . 11
⊢
((1st ‘𝑣) ∈ V →
⦋(1st ‘𝑣) / 𝑓⦌⦋(2nd
‘𝑣) / 𝑔⦌(𝑏 ∈ (𝑔(𝑋 Nat 𝑌)ℎ), 𝑎 ∈ (𝑓(𝑋 Nat 𝑌)𝑔) ↦ (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏‘𝑥)(〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉(comp‘𝑌)((1st ‘ℎ)‘𝑥))(𝑎‘𝑥)))) ∈ ((𝒫 ∪ ran ∪ ran (comp‘𝑌) ↑𝑚
(Base‘𝑋))
↑pm (∪ ran (𝑋 Nat 𝑌) × ∪ ran
(𝑋 Nat 𝑌)))) |
93 | 48, 92 | ax-mp 5 |
. . . . . . . . . 10
⊢
⦋(1st ‘𝑣) / 𝑓⦌⦋(2nd
‘𝑣) / 𝑔⦌(𝑏 ∈ (𝑔(𝑋 Nat 𝑌)ℎ), 𝑎 ∈ (𝑓(𝑋 Nat 𝑌)𝑔) ↦ (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏‘𝑥)(〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉(comp‘𝑌)((1st ‘ℎ)‘𝑥))(𝑎‘𝑥)))) ∈ ((𝒫 ∪ ran ∪ ran (comp‘𝑌) ↑𝑚
(Base‘𝑋))
↑pm (∪ ran (𝑋 Nat 𝑌) × ∪ ran
(𝑋 Nat 𝑌))) |
94 | 93 | rgen2w 2925 |
. . . . . . . . 9
⊢
∀𝑣 ∈
((𝑋 Func 𝑌) × (𝑋 Func 𝑌))∀ℎ ∈ (𝑋 Func 𝑌)⦋(1st ‘𝑣) / 𝑓⦌⦋(2nd
‘𝑣) / 𝑔⦌(𝑏 ∈ (𝑔(𝑋 Nat 𝑌)ℎ), 𝑎 ∈ (𝑓(𝑋 Nat 𝑌)𝑔) ↦ (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏‘𝑥)(〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉(comp‘𝑌)((1st ‘ℎ)‘𝑥))(𝑎‘𝑥)))) ∈ ((𝒫 ∪ ran ∪ ran (comp‘𝑌) ↑𝑚
(Base‘𝑋))
↑pm (∪ ran (𝑋 Nat 𝑌) × ∪ ran
(𝑋 Nat 𝑌))) |
95 | | eqid 2622 |
. . . . . . . . . 10
⊢ (𝑣 ∈ ((𝑋 Func 𝑌) × (𝑋 Func 𝑌)), ℎ ∈ (𝑋 Func 𝑌) ↦ ⦋(1st
‘𝑣) / 𝑓⦌⦋(2nd
‘𝑣) / 𝑔⦌(𝑏 ∈ (𝑔(𝑋 Nat 𝑌)ℎ), 𝑎 ∈ (𝑓(𝑋 Nat 𝑌)𝑔) ↦ (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏‘𝑥)(〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉(comp‘𝑌)((1st ‘ℎ)‘𝑥))(𝑎‘𝑥))))) = (𝑣 ∈ ((𝑋 Func 𝑌) × (𝑋 Func 𝑌)), ℎ ∈ (𝑋 Func 𝑌) ↦ ⦋(1st
‘𝑣) / 𝑓⦌⦋(2nd
‘𝑣) / 𝑔⦌(𝑏 ∈ (𝑔(𝑋 Nat 𝑌)ℎ), 𝑎 ∈ (𝑓(𝑋 Nat 𝑌)𝑔) ↦ (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏‘𝑥)(〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉(comp‘𝑌)((1st ‘ℎ)‘𝑥))(𝑎‘𝑥))))) |
96 | 95 | fmpt2 7237 |
. . . . . . . . 9
⊢
(∀𝑣 ∈
((𝑋 Func 𝑌) × (𝑋 Func 𝑌))∀ℎ ∈ (𝑋 Func 𝑌)⦋(1st ‘𝑣) / 𝑓⦌⦋(2nd
‘𝑣) / 𝑔⦌(𝑏 ∈ (𝑔(𝑋 Nat 𝑌)ℎ), 𝑎 ∈ (𝑓(𝑋 Nat 𝑌)𝑔) ↦ (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏‘𝑥)(〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉(comp‘𝑌)((1st ‘ℎ)‘𝑥))(𝑎‘𝑥)))) ∈ ((𝒫 ∪ ran ∪ ran (comp‘𝑌) ↑𝑚
(Base‘𝑋))
↑pm (∪ ran (𝑋 Nat 𝑌) × ∪ ran
(𝑋 Nat 𝑌))) ↔ (𝑣 ∈ ((𝑋 Func 𝑌) × (𝑋 Func 𝑌)), ℎ ∈ (𝑋 Func 𝑌) ↦ ⦋(1st
‘𝑣) / 𝑓⦌⦋(2nd
‘𝑣) / 𝑔⦌(𝑏 ∈ (𝑔(𝑋 Nat 𝑌)ℎ), 𝑎 ∈ (𝑓(𝑋 Nat 𝑌)𝑔) ↦ (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏‘𝑥)(〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉(comp‘𝑌)((1st ‘ℎ)‘𝑥))(𝑎‘𝑥))))):(((𝑋 Func 𝑌) × (𝑋 Func 𝑌)) × (𝑋 Func 𝑌))⟶((𝒫 ∪ ran ∪ ran (comp‘𝑌) ↑𝑚
(Base‘𝑋))
↑pm (∪ ran (𝑋 Nat 𝑌) × ∪ ran
(𝑋 Nat 𝑌)))) |
97 | 94, 96 | mpbi 220 |
. . . . . . . 8
⊢ (𝑣 ∈ ((𝑋 Func 𝑌) × (𝑋 Func 𝑌)), ℎ ∈ (𝑋 Func 𝑌) ↦ ⦋(1st
‘𝑣) / 𝑓⦌⦋(2nd
‘𝑣) / 𝑔⦌(𝑏 ∈ (𝑔(𝑋 Nat 𝑌)ℎ), 𝑎 ∈ (𝑓(𝑋 Nat 𝑌)𝑔) ↦ (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏‘𝑥)(〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉(comp‘𝑌)((1st ‘ℎ)‘𝑥))(𝑎‘𝑥))))):(((𝑋 Func 𝑌) × (𝑋 Func 𝑌)) × (𝑋 Func 𝑌))⟶((𝒫 ∪ ran ∪ ran (comp‘𝑌) ↑𝑚
(Base‘𝑋))
↑pm (∪ ran (𝑋 Nat 𝑌) × ∪ ran
(𝑋 Nat 𝑌))) |
98 | 97 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (𝑣 ∈ ((𝑋 Func 𝑌) × (𝑋 Func 𝑌)), ℎ ∈ (𝑋 Func 𝑌) ↦ ⦋(1st
‘𝑣) / 𝑓⦌⦋(2nd
‘𝑣) / 𝑔⦌(𝑏 ∈ (𝑔(𝑋 Nat 𝑌)ℎ), 𝑎 ∈ (𝑓(𝑋 Nat 𝑌)𝑔) ↦ (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏‘𝑥)(〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉(comp‘𝑌)((1st ‘ℎ)‘𝑥))(𝑎‘𝑥))))):(((𝑋 Func 𝑌) × (𝑋 Func 𝑌)) × (𝑋 Func 𝑌))⟶((𝒫 ∪ ran ∪ ran (comp‘𝑌) ↑𝑚
(Base‘𝑋))
↑pm (∪ ran (𝑋 Nat 𝑌) × ∪ ran
(𝑋 Nat 𝑌)))) |
99 | 10, 35, 47, 98 | wunf 9549 |
. . . . . 6
⊢ (𝜑 → (𝑣 ∈ ((𝑋 Func 𝑌) × (𝑋 Func 𝑌)), ℎ ∈ (𝑋 Func 𝑌) ↦ ⦋(1st
‘𝑣) / 𝑓⦌⦋(2nd
‘𝑣) / 𝑔⦌(𝑏 ∈ (𝑔(𝑋 Nat 𝑌)ℎ), 𝑎 ∈ (𝑓(𝑋 Nat 𝑌)𝑔) ↦ (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏‘𝑥)(〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉(comp‘𝑌)((1st ‘ℎ)‘𝑥))(𝑎‘𝑥))))) ∈ 𝑈) |
100 | 10, 33, 99 | wunop 9544 |
. . . . 5
⊢ (𝜑 → 〈(comp‘ndx),
(𝑣 ∈ ((𝑋 Func 𝑌) × (𝑋 Func 𝑌)), ℎ ∈ (𝑋 Func 𝑌) ↦ ⦋(1st
‘𝑣) / 𝑓⦌⦋(2nd
‘𝑣) / 𝑔⦌(𝑏 ∈ (𝑔(𝑋 Nat 𝑌)ℎ), 𝑎 ∈ (𝑓(𝑋 Nat 𝑌)𝑔) ↦ (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏‘𝑥)(〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉(comp‘𝑌)((1st ‘ℎ)‘𝑥))(𝑎‘𝑥)))))〉 ∈ 𝑈) |
101 | 10, 27, 31, 100 | wuntp 9533 |
. . . 4
⊢ (𝜑 → {〈(Base‘ndx),
(𝑋 Func 𝑌)〉, 〈(Hom ‘ndx), (𝑋 Nat 𝑌)〉, 〈(comp‘ndx), (𝑣 ∈ ((𝑋 Func 𝑌) × (𝑋 Func 𝑌)), ℎ ∈ (𝑋 Func 𝑌) ↦ ⦋(1st
‘𝑣) / 𝑓⦌⦋(2nd
‘𝑣) / 𝑔⦌(𝑏 ∈ (𝑔(𝑋 Nat 𝑌)ℎ), 𝑎 ∈ (𝑓(𝑋 Nat 𝑌)𝑔) ↦ (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏‘𝑥)(〈((1st ‘𝑓)‘𝑥), ((1st ‘𝑔)‘𝑥)〉(comp‘𝑌)((1st ‘ℎ)‘𝑥))(𝑎‘𝑥)))))〉} ∈ 𝑈) |
102 | 18, 101 | eqeltrd 2701 |
. . 3
⊢ (𝜑 → 𝑄 ∈ 𝑈) |
103 | 1, 13, 16 | fuccat 16630 |
. . 3
⊢ (𝜑 → 𝑄 ∈ Cat) |
104 | 102, 103 | elind 3798 |
. 2
⊢ (𝜑 → 𝑄 ∈ (𝑈 ∩ Cat)) |
105 | 104, 11 | eleqtrrd 2704 |
1
⊢ (𝜑 → 𝑄 ∈ 𝐵) |