Step | Hyp | Ref
| Expression |
1 | | pwfseq 9486 |
. 2
⊢ (ω
≼ 𝐴 → ¬
𝒫 𝐴 ≼
∪ 𝑛 ∈ ω (𝐴 ↑𝑚 𝑛)) |
2 | | reldom 7961 |
. . . . . . 7
⊢ Rel
≼ |
3 | 2 | brrelex2i 5159 |
. . . . . 6
⊢ (ω
≼ 𝐴 → 𝐴 ∈ V) |
4 | | oveq1 6657 |
. . . . . . . 8
⊢ (𝑥 = 𝐴 → (𝑥 ↑𝑚
1𝑜) = (𝐴
↑𝑚 1𝑜)) |
5 | | id 22 |
. . . . . . . 8
⊢ (𝑥 = 𝐴 → 𝑥 = 𝐴) |
6 | 4, 5 | breq12d 4666 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → ((𝑥 ↑𝑚
1𝑜) ≈ 𝑥 ↔ (𝐴 ↑𝑚
1𝑜) ≈ 𝐴)) |
7 | | df1o2 7572 |
. . . . . . . . 9
⊢
1𝑜 = {∅} |
8 | 7 | oveq2i 6661 |
. . . . . . . 8
⊢ (𝑥 ↑𝑚
1𝑜) = (𝑥
↑𝑚 {∅}) |
9 | | vex 3203 |
. . . . . . . . 9
⊢ 𝑥 ∈ V |
10 | | 0ex 4790 |
. . . . . . . . 9
⊢ ∅
∈ V |
11 | 9, 10 | mapsnen 8035 |
. . . . . . . 8
⊢ (𝑥 ↑𝑚
{∅}) ≈ 𝑥 |
12 | 8, 11 | eqbrtri 4674 |
. . . . . . 7
⊢ (𝑥 ↑𝑚
1𝑜) ≈ 𝑥 |
13 | 6, 12 | vtoclg 3266 |
. . . . . 6
⊢ (𝐴 ∈ V → (𝐴 ↑𝑚
1𝑜) ≈ 𝐴) |
14 | | ensym 8005 |
. . . . . 6
⊢ ((𝐴 ↑𝑚
1𝑜) ≈ 𝐴 → 𝐴 ≈ (𝐴 ↑𝑚
1𝑜)) |
15 | 3, 13, 14 | 3syl 18 |
. . . . 5
⊢ (ω
≼ 𝐴 → 𝐴 ≈ (𝐴 ↑𝑚
1𝑜)) |
16 | | map2xp 8130 |
. . . . . 6
⊢ (𝐴 ∈ V → (𝐴 ↑𝑚
2𝑜) ≈ (𝐴 × 𝐴)) |
17 | | ensym 8005 |
. . . . . 6
⊢ ((𝐴 ↑𝑚
2𝑜) ≈ (𝐴 × 𝐴) → (𝐴 × 𝐴) ≈ (𝐴 ↑𝑚
2𝑜)) |
18 | 3, 16, 17 | 3syl 18 |
. . . . 5
⊢ (ω
≼ 𝐴 → (𝐴 × 𝐴) ≈ (𝐴 ↑𝑚
2𝑜)) |
19 | | elmapi 7879 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (𝐴 ↑𝑚
1𝑜) → 𝑥:1𝑜⟶𝐴) |
20 | | fdm 6051 |
. . . . . . . . . . 11
⊢ (𝑥:1𝑜⟶𝐴 → dom 𝑥 = 1𝑜) |
21 | 19, 20 | syl 17 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (𝐴 ↑𝑚
1𝑜) → dom 𝑥 = 1𝑜) |
22 | 21 | adantr 481 |
. . . . . . . . 9
⊢ ((𝑥 ∈ (𝐴 ↑𝑚
1𝑜) ∧ 𝑥 ∈ (𝐴 ↑𝑚
2𝑜)) → dom 𝑥 = 1𝑜) |
23 | | 1onn 7719 |
. . . . . . . . . . . . . 14
⊢
1𝑜 ∈ ω |
24 | 23 | elexi 3213 |
. . . . . . . . . . . . 13
⊢
1𝑜 ∈ V |
25 | 24 | sucid 5804 |
. . . . . . . . . . . 12
⊢
1𝑜 ∈ suc 1𝑜 |
26 | | df-2o 7561 |
. . . . . . . . . . . 12
⊢
2𝑜 = suc 1𝑜 |
27 | 25, 26 | eleqtrri 2700 |
. . . . . . . . . . 11
⊢
1𝑜 ∈ 2𝑜 |
28 | | 1on 7567 |
. . . . . . . . . . . 12
⊢
1𝑜 ∈ On |
29 | 28 | onirri 5834 |
. . . . . . . . . . 11
⊢ ¬
1𝑜 ∈ 1𝑜 |
30 | | nelneq2 2726 |
. . . . . . . . . . 11
⊢
((1𝑜 ∈ 2𝑜 ∧ ¬
1𝑜 ∈ 1𝑜) → ¬
2𝑜 = 1𝑜) |
31 | 27, 29, 30 | mp2an 708 |
. . . . . . . . . 10
⊢ ¬
2𝑜 = 1𝑜 |
32 | | elmapi 7879 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (𝐴 ↑𝑚
2𝑜) → 𝑥:2𝑜⟶𝐴) |
33 | | fdm 6051 |
. . . . . . . . . . . . 13
⊢ (𝑥:2𝑜⟶𝐴 → dom 𝑥 = 2𝑜) |
34 | 32, 33 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (𝐴 ↑𝑚
2𝑜) → dom 𝑥 = 2𝑜) |
35 | 34 | adantl 482 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ (𝐴 ↑𝑚
1𝑜) ∧ 𝑥 ∈ (𝐴 ↑𝑚
2𝑜)) → dom 𝑥 = 2𝑜) |
36 | 35 | eqeq1d 2624 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ (𝐴 ↑𝑚
1𝑜) ∧ 𝑥 ∈ (𝐴 ↑𝑚
2𝑜)) → (dom 𝑥 = 1𝑜 ↔
2𝑜 = 1𝑜)) |
37 | 31, 36 | mtbiri 317 |
. . . . . . . . 9
⊢ ((𝑥 ∈ (𝐴 ↑𝑚
1𝑜) ∧ 𝑥 ∈ (𝐴 ↑𝑚
2𝑜)) → ¬ dom 𝑥 = 1𝑜) |
38 | 22, 37 | pm2.65i 185 |
. . . . . . . 8
⊢ ¬
(𝑥 ∈ (𝐴 ↑𝑚
1𝑜) ∧ 𝑥 ∈ (𝐴 ↑𝑚
2𝑜)) |
39 | | elin 3796 |
. . . . . . . 8
⊢ (𝑥 ∈ ((𝐴 ↑𝑚
1𝑜) ∩ (𝐴 ↑𝑚
2𝑜)) ↔ (𝑥 ∈ (𝐴 ↑𝑚
1𝑜) ∧ 𝑥 ∈ (𝐴 ↑𝑚
2𝑜))) |
40 | 38, 39 | mtbir 313 |
. . . . . . 7
⊢ ¬
𝑥 ∈ ((𝐴 ↑𝑚
1𝑜) ∩ (𝐴 ↑𝑚
2𝑜)) |
41 | 40 | a1i 11 |
. . . . . 6
⊢ (ω
≼ 𝐴 → ¬
𝑥 ∈ ((𝐴 ↑𝑚
1𝑜) ∩ (𝐴 ↑𝑚
2𝑜))) |
42 | 41 | eq0rdv 3979 |
. . . . 5
⊢ (ω
≼ 𝐴 → ((𝐴 ↑𝑚
1𝑜) ∩ (𝐴 ↑𝑚
2𝑜)) = ∅) |
43 | | cdaenun 8996 |
. . . . 5
⊢ ((𝐴 ≈ (𝐴 ↑𝑚
1𝑜) ∧ (𝐴 × 𝐴) ≈ (𝐴 ↑𝑚
2𝑜) ∧ ((𝐴 ↑𝑚
1𝑜) ∩ (𝐴 ↑𝑚
2𝑜)) = ∅) → (𝐴 +𝑐 (𝐴 × 𝐴)) ≈ ((𝐴 ↑𝑚
1𝑜) ∪ (𝐴 ↑𝑚
2𝑜))) |
44 | 15, 18, 42, 43 | syl3anc 1326 |
. . . 4
⊢ (ω
≼ 𝐴 → (𝐴 +𝑐 (𝐴 × 𝐴)) ≈ ((𝐴 ↑𝑚
1𝑜) ∪ (𝐴 ↑𝑚
2𝑜))) |
45 | | omex 8540 |
. . . . . 6
⊢ ω
∈ V |
46 | | ovex 6678 |
. . . . . 6
⊢ (𝐴 ↑𝑚
𝑛) ∈
V |
47 | 45, 46 | iunex 7147 |
. . . . 5
⊢ ∪ 𝑛 ∈ ω (𝐴 ↑𝑚 𝑛) ∈ V |
48 | | oveq2 6658 |
. . . . . . . 8
⊢ (𝑛 = 1𝑜 →
(𝐴
↑𝑚 𝑛) = (𝐴 ↑𝑚
1𝑜)) |
49 | 48 | ssiun2s 4564 |
. . . . . . 7
⊢
(1𝑜 ∈ ω → (𝐴 ↑𝑚
1𝑜) ⊆ ∪ 𝑛 ∈ ω (𝐴 ↑𝑚
𝑛)) |
50 | 23, 49 | ax-mp 5 |
. . . . . 6
⊢ (𝐴 ↑𝑚
1𝑜) ⊆ ∪ 𝑛 ∈ ω (𝐴 ↑𝑚
𝑛) |
51 | | 2onn 7720 |
. . . . . . 7
⊢
2𝑜 ∈ ω |
52 | | oveq2 6658 |
. . . . . . . 8
⊢ (𝑛 = 2𝑜 →
(𝐴
↑𝑚 𝑛) = (𝐴 ↑𝑚
2𝑜)) |
53 | 52 | ssiun2s 4564 |
. . . . . . 7
⊢
(2𝑜 ∈ ω → (𝐴 ↑𝑚
2𝑜) ⊆ ∪ 𝑛 ∈ ω (𝐴 ↑𝑚
𝑛)) |
54 | 51, 53 | ax-mp 5 |
. . . . . 6
⊢ (𝐴 ↑𝑚
2𝑜) ⊆ ∪ 𝑛 ∈ ω (𝐴 ↑𝑚
𝑛) |
55 | 50, 54 | unssi 3788 |
. . . . 5
⊢ ((𝐴 ↑𝑚
1𝑜) ∪ (𝐴 ↑𝑚
2𝑜)) ⊆ ∪ 𝑛 ∈ ω (𝐴 ↑𝑚
𝑛) |
56 | | ssdomg 8001 |
. . . . 5
⊢ (∪ 𝑛 ∈ ω (𝐴 ↑𝑚 𝑛) ∈ V → (((𝐴 ↑𝑚
1𝑜) ∪ (𝐴 ↑𝑚
2𝑜)) ⊆ ∪ 𝑛 ∈ ω (𝐴 ↑𝑚
𝑛) → ((𝐴 ↑𝑚
1𝑜) ∪ (𝐴 ↑𝑚
2𝑜)) ≼ ∪ 𝑛 ∈ ω (𝐴 ↑𝑚
𝑛))) |
57 | 47, 55, 56 | mp2 9 |
. . . 4
⊢ ((𝐴 ↑𝑚
1𝑜) ∪ (𝐴 ↑𝑚
2𝑜)) ≼ ∪ 𝑛 ∈ ω (𝐴 ↑𝑚
𝑛) |
58 | | endomtr 8014 |
. . . 4
⊢ (((𝐴 +𝑐 (𝐴 × 𝐴)) ≈ ((𝐴 ↑𝑚
1𝑜) ∪ (𝐴 ↑𝑚
2𝑜)) ∧ ((𝐴 ↑𝑚
1𝑜) ∪ (𝐴 ↑𝑚
2𝑜)) ≼ ∪ 𝑛 ∈ ω (𝐴 ↑𝑚
𝑛)) → (𝐴 +𝑐 (𝐴 × 𝐴)) ≼ ∪ 𝑛 ∈ ω (𝐴 ↑𝑚 𝑛)) |
59 | 44, 57, 58 | sylancl 694 |
. . 3
⊢ (ω
≼ 𝐴 → (𝐴 +𝑐 (𝐴 × 𝐴)) ≼ ∪ 𝑛 ∈ ω (𝐴 ↑𝑚 𝑛)) |
60 | | domtr 8009 |
. . . 4
⊢
((𝒫 𝐴
≼ (𝐴
+𝑐 (𝐴
× 𝐴)) ∧ (𝐴 +𝑐 (𝐴 × 𝐴)) ≼ ∪ 𝑛 ∈ ω (𝐴 ↑𝑚 𝑛)) → 𝒫 𝐴 ≼ ∪ 𝑛 ∈ ω (𝐴 ↑𝑚 𝑛)) |
61 | 60 | expcom 451 |
. . 3
⊢ ((𝐴 +𝑐 (𝐴 × 𝐴)) ≼ ∪ 𝑛 ∈ ω (𝐴 ↑𝑚 𝑛) → (𝒫 𝐴 ≼ (𝐴 +𝑐 (𝐴 × 𝐴)) → 𝒫 𝐴 ≼ ∪
𝑛 ∈ ω (𝐴 ↑𝑚
𝑛))) |
62 | 59, 61 | syl 17 |
. 2
⊢ (ω
≼ 𝐴 → (𝒫
𝐴 ≼ (𝐴 +𝑐 (𝐴 × 𝐴)) → 𝒫 𝐴 ≼ ∪
𝑛 ∈ ω (𝐴 ↑𝑚
𝑛))) |
63 | 1, 62 | mtod 189 |
1
⊢ (ω
≼ 𝐴 → ¬
𝒫 𝐴 ≼ (𝐴 +𝑐 (𝐴 × 𝐴))) |