Proof of Theorem hauspwdom
| Step | Hyp | Ref
| Expression |
| 1 | | hauspwdom.1 |
. . . 4
⊢ 𝑋 = ∪
𝐽 |
| 2 | 1 | hausmapdom 23508 |
. . 3
⊢ ((𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω
∧ 𝐴 ⊆ 𝑋) → ((cls‘𝐽)‘𝐴) ≼ (𝐴 ↑m
ℕ)) |
| 3 | 2 | adantr 480 |
. 2
⊢ (((𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω
∧ 𝐴 ⊆ 𝑋) ∧ (𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵)) → ((cls‘𝐽)‘𝐴) ≼ (𝐴 ↑m
ℕ)) |
| 4 | | simprr 773 |
. . . 4
⊢ (((𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω
∧ 𝐴 ⊆ 𝑋) ∧ (𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵)) → ℕ ≼ 𝐵) |
| 5 | | 1nn 12277 |
. . . . 5
⊢ 1 ∈
ℕ |
| 6 | | noel 4338 |
. . . . . . 7
⊢ ¬ 1
∈ ∅ |
| 7 | | eleq2 2830 |
. . . . . . 7
⊢ (ℕ
= ∅ → (1 ∈ ℕ ↔ 1 ∈ ∅)) |
| 8 | 6, 7 | mtbiri 327 |
. . . . . 6
⊢ (ℕ
= ∅ → ¬ 1 ∈ ℕ) |
| 9 | 8 | adantr 480 |
. . . . 5
⊢ ((ℕ
= ∅ ∧ 𝐴 =
∅) → ¬ 1 ∈ ℕ) |
| 10 | 5, 9 | mt2 200 |
. . . 4
⊢ ¬
(ℕ = ∅ ∧ 𝐴
= ∅) |
| 11 | | mapdom2 9188 |
. . . 4
⊢ ((ℕ
≼ 𝐵 ∧ ¬
(ℕ = ∅ ∧ 𝐴
= ∅)) → (𝐴
↑m ℕ) ≼ (𝐴 ↑m 𝐵)) |
| 12 | 4, 10, 11 | sylancl 586 |
. . 3
⊢ (((𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω
∧ 𝐴 ⊆ 𝑋) ∧ (𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵)) → (𝐴 ↑m ℕ) ≼ (𝐴 ↑m 𝐵)) |
| 13 | | sdomdom 9020 |
. . . . . . 7
⊢ (𝐴 ≺ 2o →
𝐴 ≼
2o) |
| 14 | 13 | adantl 481 |
. . . . . 6
⊢ ((((𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω
∧ 𝐴 ⊆ 𝑋) ∧ (𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵)) ∧ 𝐴 ≺ 2o) → 𝐴 ≼
2o) |
| 15 | | mapdom1 9182 |
. . . . . 6
⊢ (𝐴 ≼ 2o →
(𝐴 ↑m 𝐵) ≼ (2o
↑m 𝐵)) |
| 16 | 14, 15 | syl 17 |
. . . . 5
⊢ ((((𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω
∧ 𝐴 ⊆ 𝑋) ∧ (𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵)) ∧ 𝐴 ≺ 2o) → (𝐴 ↑m 𝐵) ≼ (2o
↑m 𝐵)) |
| 17 | | reldom 8991 |
. . . . . . . . 9
⊢ Rel
≼ |
| 18 | 17 | brrelex2i 5742 |
. . . . . . . 8
⊢ (ℕ
≼ 𝐵 → 𝐵 ∈ V) |
| 19 | 18 | ad2antll 729 |
. . . . . . 7
⊢ (((𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω
∧ 𝐴 ⊆ 𝑋) ∧ (𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵)) → 𝐵 ∈ V) |
| 20 | | pw2eng 9118 |
. . . . . . 7
⊢ (𝐵 ∈ V → 𝒫 𝐵 ≈ (2o
↑m 𝐵)) |
| 21 | | ensym 9043 |
. . . . . . 7
⊢
(𝒫 𝐵 ≈
(2o ↑m 𝐵) → (2o ↑m
𝐵) ≈ 𝒫 𝐵) |
| 22 | 19, 20, 21 | 3syl 18 |
. . . . . 6
⊢ (((𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω
∧ 𝐴 ⊆ 𝑋) ∧ (𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵)) → (2o ↑m
𝐵) ≈ 𝒫 𝐵) |
| 23 | 22 | adantr 480 |
. . . . 5
⊢ ((((𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω
∧ 𝐴 ⊆ 𝑋) ∧ (𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵)) ∧ 𝐴 ≺ 2o) →
(2o ↑m 𝐵) ≈ 𝒫 𝐵) |
| 24 | | domentr 9053 |
. . . . 5
⊢ (((𝐴 ↑m 𝐵) ≼ (2o
↑m 𝐵) ∧
(2o ↑m 𝐵) ≈ 𝒫 𝐵) → (𝐴 ↑m 𝐵) ≼ 𝒫 𝐵) |
| 25 | 16, 23, 24 | syl2anc 584 |
. . . 4
⊢ ((((𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω
∧ 𝐴 ⊆ 𝑋) ∧ (𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵)) ∧ 𝐴 ≺ 2o) → (𝐴 ↑m 𝐵) ≼ 𝒫 𝐵) |
| 26 | | onfin2 9268 |
. . . . . . . . 9
⊢ ω =
(On ∩ Fin) |
| 27 | | inss2 4238 |
. . . . . . . . 9
⊢ (On ∩
Fin) ⊆ Fin |
| 28 | 26, 27 | eqsstri 4030 |
. . . . . . . 8
⊢ ω
⊆ Fin |
| 29 | | 2onn 8680 |
. . . . . . . 8
⊢
2o ∈ ω |
| 30 | 28, 29 | sselii 3980 |
. . . . . . 7
⊢
2o ∈ Fin |
| 31 | | simprl 771 |
. . . . . . . 8
⊢ (((𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω
∧ 𝐴 ⊆ 𝑋) ∧ (𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵)) → 𝐴 ≼ 𝒫 𝐵) |
| 32 | 17 | brrelex1i 5741 |
. . . . . . . 8
⊢ (𝐴 ≼ 𝒫 𝐵 → 𝐴 ∈ V) |
| 33 | 31, 32 | syl 17 |
. . . . . . 7
⊢ (((𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω
∧ 𝐴 ⊆ 𝑋) ∧ (𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵)) → 𝐴 ∈ V) |
| 34 | | fidomtri 10033 |
. . . . . . 7
⊢
((2o ∈ Fin ∧ 𝐴 ∈ V) → (2o ≼
𝐴 ↔ ¬ 𝐴 ≺
2o)) |
| 35 | 30, 33, 34 | sylancr 587 |
. . . . . 6
⊢ (((𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω
∧ 𝐴 ⊆ 𝑋) ∧ (𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵)) → (2o ≼ 𝐴 ↔ ¬ 𝐴 ≺ 2o)) |
| 36 | 35 | biimpar 477 |
. . . . 5
⊢ ((((𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω
∧ 𝐴 ⊆ 𝑋) ∧ (𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵)) ∧ ¬ 𝐴 ≺ 2o) → 2o
≼ 𝐴) |
| 37 | | numth3 10510 |
. . . . . . . . 9
⊢ (𝐵 ∈ V → 𝐵 ∈ dom
card) |
| 38 | 19, 37 | syl 17 |
. . . . . . . 8
⊢ (((𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω
∧ 𝐴 ⊆ 𝑋) ∧ (𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵)) → 𝐵 ∈ dom card) |
| 39 | 38 | adantr 480 |
. . . . . . 7
⊢ ((((𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω
∧ 𝐴 ⊆ 𝑋) ∧ (𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵)) ∧ 2o ≼ 𝐴) → 𝐵 ∈ dom card) |
| 40 | | nnenom 14021 |
. . . . . . . . . 10
⊢ ℕ
≈ ω |
| 41 | 40 | ensymi 9044 |
. . . . . . . . 9
⊢ ω
≈ ℕ |
| 42 | | endomtr 9052 |
. . . . . . . . 9
⊢ ((ω
≈ ℕ ∧ ℕ ≼ 𝐵) → ω ≼ 𝐵) |
| 43 | 41, 4, 42 | sylancr 587 |
. . . . . . . 8
⊢ (((𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω
∧ 𝐴 ⊆ 𝑋) ∧ (𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵)) → ω ≼ 𝐵) |
| 44 | 43 | adantr 480 |
. . . . . . 7
⊢ ((((𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω
∧ 𝐴 ⊆ 𝑋) ∧ (𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵)) ∧ 2o ≼ 𝐴) → ω ≼ 𝐵) |
| 45 | | simpr 484 |
. . . . . . 7
⊢ ((((𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω
∧ 𝐴 ⊆ 𝑋) ∧ (𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵)) ∧ 2o ≼ 𝐴) → 2o ≼
𝐴) |
| 46 | 31 | adantr 480 |
. . . . . . 7
⊢ ((((𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω
∧ 𝐴 ⊆ 𝑋) ∧ (𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵)) ∧ 2o ≼ 𝐴) → 𝐴 ≼ 𝒫 𝐵) |
| 47 | | mappwen 10152 |
. . . . . . 7
⊢ (((𝐵 ∈ dom card ∧ ω
≼ 𝐵) ∧
(2o ≼ 𝐴
∧ 𝐴 ≼ 𝒫
𝐵)) → (𝐴 ↑m 𝐵) ≈ 𝒫 𝐵) |
| 48 | 39, 44, 45, 46, 47 | syl22anc 839 |
. . . . . 6
⊢ ((((𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω
∧ 𝐴 ⊆ 𝑋) ∧ (𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵)) ∧ 2o ≼ 𝐴) → (𝐴 ↑m 𝐵) ≈ 𝒫 𝐵) |
| 49 | | endom 9019 |
. . . . . 6
⊢ ((𝐴 ↑m 𝐵) ≈ 𝒫 𝐵 → (𝐴 ↑m 𝐵) ≼ 𝒫 𝐵) |
| 50 | 48, 49 | syl 17 |
. . . . 5
⊢ ((((𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω
∧ 𝐴 ⊆ 𝑋) ∧ (𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵)) ∧ 2o ≼ 𝐴) → (𝐴 ↑m 𝐵) ≼ 𝒫 𝐵) |
| 51 | 36, 50 | syldan 591 |
. . . 4
⊢ ((((𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω
∧ 𝐴 ⊆ 𝑋) ∧ (𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵)) ∧ ¬ 𝐴 ≺ 2o) → (𝐴 ↑m 𝐵) ≼ 𝒫 𝐵) |
| 52 | 25, 51 | pm2.61dan 813 |
. . 3
⊢ (((𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω
∧ 𝐴 ⊆ 𝑋) ∧ (𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵)) → (𝐴 ↑m 𝐵) ≼ 𝒫 𝐵) |
| 53 | | domtr 9047 |
. . 3
⊢ (((𝐴 ↑m ℕ)
≼ (𝐴
↑m 𝐵) ∧
(𝐴 ↑m 𝐵) ≼ 𝒫 𝐵) → (𝐴 ↑m ℕ) ≼
𝒫 𝐵) |
| 54 | 12, 52, 53 | syl2anc 584 |
. 2
⊢ (((𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω
∧ 𝐴 ⊆ 𝑋) ∧ (𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵)) → (𝐴 ↑m ℕ) ≼
𝒫 𝐵) |
| 55 | | domtr 9047 |
. 2
⊢
((((cls‘𝐽)‘𝐴) ≼ (𝐴 ↑m ℕ) ∧ (𝐴 ↑m ℕ)
≼ 𝒫 𝐵) →
((cls‘𝐽)‘𝐴) ≼ 𝒫 𝐵) |
| 56 | 3, 54, 55 | syl2anc 584 |
1
⊢ (((𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω
∧ 𝐴 ⊆ 𝑋) ∧ (𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵)) → ((cls‘𝐽)‘𝐴) ≼ 𝒫 𝐵) |