| Step | Hyp | Ref
| Expression |
| 1 | | pwfseq 10704 |
. 2
⊢ (ω
≼ 𝐴 → ¬
𝒫 𝐴 ≼
∪ 𝑛 ∈ ω (𝐴 ↑m 𝑛)) |
| 2 | | reldom 8991 |
. . . . . . 7
⊢ Rel
≼ |
| 3 | 2 | brrelex2i 5742 |
. . . . . 6
⊢ (ω
≼ 𝐴 → 𝐴 ∈ V) |
| 4 | | df1o2 8513 |
. . . . . . . 8
⊢
1o = {∅} |
| 5 | 4 | oveq2i 7442 |
. . . . . . 7
⊢ (𝐴 ↑m
1o) = (𝐴
↑m {∅}) |
| 6 | | id 22 |
. . . . . . . 8
⊢ (𝐴 ∈ V → 𝐴 ∈ V) |
| 7 | | 0ex 5307 |
. . . . . . . . 9
⊢ ∅
∈ V |
| 8 | 7 | a1i 11 |
. . . . . . . 8
⊢ (𝐴 ∈ V → ∅ ∈
V) |
| 9 | 6, 8 | mapsnend 9076 |
. . . . . . 7
⊢ (𝐴 ∈ V → (𝐴 ↑m {∅})
≈ 𝐴) |
| 10 | 5, 9 | eqbrtrid 5178 |
. . . . . 6
⊢ (𝐴 ∈ V → (𝐴 ↑m
1o) ≈ 𝐴) |
| 11 | | ensym 9043 |
. . . . . 6
⊢ ((𝐴 ↑m
1o) ≈ 𝐴
→ 𝐴 ≈ (𝐴 ↑m
1o)) |
| 12 | 3, 10, 11 | 3syl 18 |
. . . . 5
⊢ (ω
≼ 𝐴 → 𝐴 ≈ (𝐴 ↑m
1o)) |
| 13 | | map2xp 9187 |
. . . . . 6
⊢ (𝐴 ∈ V → (𝐴 ↑m
2o) ≈ (𝐴
× 𝐴)) |
| 14 | | ensym 9043 |
. . . . . 6
⊢ ((𝐴 ↑m
2o) ≈ (𝐴
× 𝐴) → (𝐴 × 𝐴) ≈ (𝐴 ↑m
2o)) |
| 15 | 3, 13, 14 | 3syl 18 |
. . . . 5
⊢ (ω
≼ 𝐴 → (𝐴 × 𝐴) ≈ (𝐴 ↑m
2o)) |
| 16 | | elmapi 8889 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (𝐴 ↑m 1o) →
𝑥:1o⟶𝐴) |
| 17 | 16 | fdmd 6746 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (𝐴 ↑m 1o) →
dom 𝑥 =
1o) |
| 18 | 17 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑥 ∈ (𝐴 ↑m 1o) ∧
𝑥 ∈ (𝐴 ↑m 2o)) →
dom 𝑥 =
1o) |
| 19 | | 1oex 8516 |
. . . . . . . . . . . . 13
⊢
1o ∈ V |
| 20 | 19 | sucid 6466 |
. . . . . . . . . . . 12
⊢
1o ∈ suc 1o |
| 21 | | df-2o 8507 |
. . . . . . . . . . . 12
⊢
2o = suc 1o |
| 22 | 20, 21 | eleqtrri 2840 |
. . . . . . . . . . 11
⊢
1o ∈ 2o |
| 23 | | 1on 8518 |
. . . . . . . . . . . 12
⊢
1o ∈ On |
| 24 | 23 | onirri 6497 |
. . . . . . . . . . 11
⊢ ¬
1o ∈ 1o |
| 25 | | nelneq2 2866 |
. . . . . . . . . . 11
⊢
((1o ∈ 2o ∧ ¬ 1o ∈
1o) → ¬ 2o = 1o) |
| 26 | 22, 24, 25 | mp2an 692 |
. . . . . . . . . 10
⊢ ¬
2o = 1o |
| 27 | | elmapi 8889 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (𝐴 ↑m 2o) →
𝑥:2o⟶𝐴) |
| 28 | 27 | fdmd 6746 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (𝐴 ↑m 2o) →
dom 𝑥 =
2o) |
| 29 | 28 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ (𝐴 ↑m 1o) ∧
𝑥 ∈ (𝐴 ↑m 2o)) →
dom 𝑥 =
2o) |
| 30 | 29 | eqeq1d 2739 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ (𝐴 ↑m 1o) ∧
𝑥 ∈ (𝐴 ↑m 2o)) →
(dom 𝑥 = 1o
↔ 2o = 1o)) |
| 31 | 26, 30 | mtbiri 327 |
. . . . . . . . 9
⊢ ((𝑥 ∈ (𝐴 ↑m 1o) ∧
𝑥 ∈ (𝐴 ↑m 2o)) →
¬ dom 𝑥 =
1o) |
| 32 | 18, 31 | pm2.65i 194 |
. . . . . . . 8
⊢ ¬
(𝑥 ∈ (𝐴 ↑m
1o) ∧ 𝑥
∈ (𝐴
↑m 2o)) |
| 33 | | elin 3967 |
. . . . . . . 8
⊢ (𝑥 ∈ ((𝐴 ↑m 1o) ∩
(𝐴 ↑m
2o)) ↔ (𝑥
∈ (𝐴
↑m 1o) ∧ 𝑥 ∈ (𝐴 ↑m
2o))) |
| 34 | 32, 33 | mtbir 323 |
. . . . . . 7
⊢ ¬
𝑥 ∈ ((𝐴 ↑m
1o) ∩ (𝐴
↑m 2o)) |
| 35 | 34 | a1i 11 |
. . . . . 6
⊢ (ω
≼ 𝐴 → ¬
𝑥 ∈ ((𝐴 ↑m
1o) ∩ (𝐴
↑m 2o))) |
| 36 | 35 | eq0rdv 4407 |
. . . . 5
⊢ (ω
≼ 𝐴 → ((𝐴 ↑m
1o) ∩ (𝐴
↑m 2o)) = ∅) |
| 37 | | djuenun 10211 |
. . . . 5
⊢ ((𝐴 ≈ (𝐴 ↑m 1o) ∧
(𝐴 × 𝐴) ≈ (𝐴 ↑m 2o) ∧
((𝐴 ↑m
1o) ∩ (𝐴
↑m 2o)) = ∅) → (𝐴 ⊔ (𝐴 × 𝐴)) ≈ ((𝐴 ↑m 1o) ∪
(𝐴 ↑m
2o))) |
| 38 | 12, 15, 36, 37 | syl3anc 1373 |
. . . 4
⊢ (ω
≼ 𝐴 → (𝐴 ⊔ (𝐴 × 𝐴)) ≈ ((𝐴 ↑m 1o) ∪
(𝐴 ↑m
2o))) |
| 39 | | omex 9683 |
. . . . . 6
⊢ ω
∈ V |
| 40 | | ovex 7464 |
. . . . . 6
⊢ (𝐴 ↑m 𝑛) ∈ V |
| 41 | 39, 40 | iunex 7993 |
. . . . 5
⊢ ∪ 𝑛 ∈ ω (𝐴 ↑m 𝑛) ∈ V |
| 42 | | 1onn 8678 |
. . . . . . 7
⊢
1o ∈ ω |
| 43 | | oveq2 7439 |
. . . . . . . 8
⊢ (𝑛 = 1o → (𝐴 ↑m 𝑛) = (𝐴 ↑m
1o)) |
| 44 | 43 | ssiun2s 5048 |
. . . . . . 7
⊢
(1o ∈ ω → (𝐴 ↑m 1o) ⊆
∪ 𝑛 ∈ ω (𝐴 ↑m 𝑛)) |
| 45 | 42, 44 | ax-mp 5 |
. . . . . 6
⊢ (𝐴 ↑m
1o) ⊆ ∪ 𝑛 ∈ ω (𝐴 ↑m 𝑛) |
| 46 | | 2onn 8680 |
. . . . . . 7
⊢
2o ∈ ω |
| 47 | | oveq2 7439 |
. . . . . . . 8
⊢ (𝑛 = 2o → (𝐴 ↑m 𝑛) = (𝐴 ↑m
2o)) |
| 48 | 47 | ssiun2s 5048 |
. . . . . . 7
⊢
(2o ∈ ω → (𝐴 ↑m 2o) ⊆
∪ 𝑛 ∈ ω (𝐴 ↑m 𝑛)) |
| 49 | 46, 48 | ax-mp 5 |
. . . . . 6
⊢ (𝐴 ↑m
2o) ⊆ ∪ 𝑛 ∈ ω (𝐴 ↑m 𝑛) |
| 50 | 45, 49 | unssi 4191 |
. . . . 5
⊢ ((𝐴 ↑m
1o) ∪ (𝐴
↑m 2o)) ⊆ ∪
𝑛 ∈ ω (𝐴 ↑m 𝑛) |
| 51 | | ssdomg 9040 |
. . . . 5
⊢ (∪ 𝑛 ∈ ω (𝐴 ↑m 𝑛) ∈ V → (((𝐴 ↑m 1o) ∪
(𝐴 ↑m
2o)) ⊆ ∪ 𝑛 ∈ ω (𝐴 ↑m 𝑛) → ((𝐴 ↑m 1o) ∪
(𝐴 ↑m
2o)) ≼ ∪ 𝑛 ∈ ω (𝐴 ↑m 𝑛))) |
| 52 | 41, 50, 51 | mp2 9 |
. . . 4
⊢ ((𝐴 ↑m
1o) ∪ (𝐴
↑m 2o)) ≼ ∪
𝑛 ∈ ω (𝐴 ↑m 𝑛) |
| 53 | | endomtr 9052 |
. . . 4
⊢ (((𝐴 ⊔ (𝐴 × 𝐴)) ≈ ((𝐴 ↑m 1o) ∪
(𝐴 ↑m
2o)) ∧ ((𝐴
↑m 1o) ∪ (𝐴 ↑m 2o)) ≼
∪ 𝑛 ∈ ω (𝐴 ↑m 𝑛)) → (𝐴 ⊔ (𝐴 × 𝐴)) ≼ ∪ 𝑛 ∈ ω (𝐴 ↑m 𝑛)) |
| 54 | 38, 52, 53 | sylancl 586 |
. . 3
⊢ (ω
≼ 𝐴 → (𝐴 ⊔ (𝐴 × 𝐴)) ≼ ∪ 𝑛 ∈ ω (𝐴 ↑m 𝑛)) |
| 55 | | domtr 9047 |
. . . 4
⊢
((𝒫 𝐴
≼ (𝐴 ⊔ (𝐴 × 𝐴)) ∧ (𝐴 ⊔ (𝐴 × 𝐴)) ≼ ∪ 𝑛 ∈ ω (𝐴 ↑m 𝑛)) → 𝒫 𝐴 ≼ ∪
𝑛 ∈ ω (𝐴 ↑m 𝑛)) |
| 56 | 55 | expcom 413 |
. . 3
⊢ ((𝐴 ⊔ (𝐴 × 𝐴)) ≼ ∪ 𝑛 ∈ ω (𝐴 ↑m 𝑛) → (𝒫 𝐴 ≼ (𝐴 ⊔ (𝐴 × 𝐴)) → 𝒫 𝐴 ≼ ∪
𝑛 ∈ ω (𝐴 ↑m 𝑛))) |
| 57 | 54, 56 | syl 17 |
. 2
⊢ (ω
≼ 𝐴 → (𝒫
𝐴 ≼ (𝐴 ⊔ (𝐴 × 𝐴)) → 𝒫 𝐴 ≼ ∪
𝑛 ∈ ω (𝐴 ↑m 𝑛))) |
| 58 | 1, 57 | mtod 198 |
1
⊢ (ω
≼ 𝐴 → ¬
𝒫 𝐴 ≼ (𝐴 ⊔ (𝐴 × 𝐴))) |