Proof of Theorem hauspwdom
Step | Hyp | Ref
| Expression |
1 | | hauspwdom.1 |
. . . 4
⊢ 𝑋 = ∪
𝐽 |
2 | 1 | hausmapdom 21113 |
. . 3
⊢ ((𝐽 ∈ Haus ∧ 𝐽 ∈ 1st𝜔
∧ 𝐴 ⊆ 𝑋) → ((cls‘𝐽)‘𝐴) ≼ (𝐴 ↑𝑚
ℕ)) |
3 | 2 | adantr 480 |
. 2
⊢ (((𝐽 ∈ Haus ∧ 𝐽 ∈ 1st𝜔
∧ 𝐴 ⊆ 𝑋) ∧ (𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵)) → ((cls‘𝐽)‘𝐴) ≼ (𝐴 ↑𝑚
ℕ)) |
4 | | simprr 792 |
. . . 4
⊢ (((𝐽 ∈ Haus ∧ 𝐽 ∈ 1st𝜔
∧ 𝐴 ⊆ 𝑋) ∧ (𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵)) → ℕ ≼ 𝐵) |
5 | | 1nn 10908 |
. . . . 5
⊢ 1 ∈
ℕ |
6 | | noel 3878 |
. . . . . . 7
⊢ ¬ 1
∈ ∅ |
7 | | eleq2 2677 |
. . . . . . 7
⊢ (ℕ
= ∅ → (1 ∈ ℕ ↔ 1 ∈ ∅)) |
8 | 6, 7 | mtbiri 316 |
. . . . . 6
⊢ (ℕ
= ∅ → ¬ 1 ∈ ℕ) |
9 | 8 | adantr 480 |
. . . . 5
⊢ ((ℕ
= ∅ ∧ 𝐴 =
∅) → ¬ 1 ∈ ℕ) |
10 | 5, 9 | mt2 190 |
. . . 4
⊢ ¬
(ℕ = ∅ ∧ 𝐴
= ∅) |
11 | | mapdom2 8016 |
. . . 4
⊢ ((ℕ
≼ 𝐵 ∧ ¬
(ℕ = ∅ ∧ 𝐴
= ∅)) → (𝐴
↑𝑚 ℕ) ≼ (𝐴 ↑𝑚 𝐵)) |
12 | 4, 10, 11 | sylancl 693 |
. . 3
⊢ (((𝐽 ∈ Haus ∧ 𝐽 ∈ 1st𝜔
∧ 𝐴 ⊆ 𝑋) ∧ (𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵)) → (𝐴 ↑𝑚 ℕ) ≼
(𝐴
↑𝑚 𝐵)) |
13 | | sdomdom 7869 |
. . . . . . 7
⊢ (𝐴 ≺ 2𝑜
→ 𝐴 ≼
2𝑜) |
14 | 13 | adantl 481 |
. . . . . 6
⊢ ((((𝐽 ∈ Haus ∧ 𝐽 ∈ 1st𝜔
∧ 𝐴 ⊆ 𝑋) ∧ (𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵)) ∧ 𝐴 ≺ 2𝑜) → 𝐴 ≼
2𝑜) |
15 | | mapdom1 8010 |
. . . . . 6
⊢ (𝐴 ≼ 2𝑜
→ (𝐴
↑𝑚 𝐵) ≼ (2𝑜
↑𝑚 𝐵)) |
16 | 14, 15 | syl 17 |
. . . . 5
⊢ ((((𝐽 ∈ Haus ∧ 𝐽 ∈ 1st𝜔
∧ 𝐴 ⊆ 𝑋) ∧ (𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵)) ∧ 𝐴 ≺ 2𝑜) →
(𝐴
↑𝑚 𝐵) ≼ (2𝑜
↑𝑚 𝐵)) |
17 | | reldom 7847 |
. . . . . . . . 9
⊢ Rel
≼ |
18 | 17 | brrelex2i 5083 |
. . . . . . . 8
⊢ (ℕ
≼ 𝐵 → 𝐵 ∈ V) |
19 | 18 | ad2antll 761 |
. . . . . . 7
⊢ (((𝐽 ∈ Haus ∧ 𝐽 ∈ 1st𝜔
∧ 𝐴 ⊆ 𝑋) ∧ (𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵)) → 𝐵 ∈ V) |
20 | | pw2eng 7951 |
. . . . . . 7
⊢ (𝐵 ∈ V → 𝒫 𝐵 ≈ (2𝑜
↑𝑚 𝐵)) |
21 | | ensym 7891 |
. . . . . . 7
⊢
(𝒫 𝐵 ≈
(2𝑜 ↑𝑚 𝐵) → (2𝑜
↑𝑚 𝐵) ≈ 𝒫 𝐵) |
22 | 19, 20, 21 | 3syl 18 |
. . . . . 6
⊢ (((𝐽 ∈ Haus ∧ 𝐽 ∈ 1st𝜔
∧ 𝐴 ⊆ 𝑋) ∧ (𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵)) → (2𝑜
↑𝑚 𝐵) ≈ 𝒫 𝐵) |
23 | 22 | adantr 480 |
. . . . 5
⊢ ((((𝐽 ∈ Haus ∧ 𝐽 ∈ 1st𝜔
∧ 𝐴 ⊆ 𝑋) ∧ (𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵)) ∧ 𝐴 ≺ 2𝑜) →
(2𝑜 ↑𝑚 𝐵) ≈ 𝒫 𝐵) |
24 | | domentr 7901 |
. . . . 5
⊢ (((𝐴 ↑𝑚
𝐵) ≼
(2𝑜 ↑𝑚 𝐵) ∧ (2𝑜
↑𝑚 𝐵) ≈ 𝒫 𝐵) → (𝐴 ↑𝑚 𝐵) ≼ 𝒫 𝐵) |
25 | 16, 23, 24 | syl2anc 691 |
. . . 4
⊢ ((((𝐽 ∈ Haus ∧ 𝐽 ∈ 1st𝜔
∧ 𝐴 ⊆ 𝑋) ∧ (𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵)) ∧ 𝐴 ≺ 2𝑜) →
(𝐴
↑𝑚 𝐵) ≼ 𝒫 𝐵) |
26 | | onfin2 8037 |
. . . . . . . . 9
⊢ ω =
(On ∩ Fin) |
27 | | inss2 3796 |
. . . . . . . . 9
⊢ (On ∩
Fin) ⊆ Fin |
28 | 26, 27 | eqsstri 3598 |
. . . . . . . 8
⊢ ω
⊆ Fin |
29 | | 2onn 7607 |
. . . . . . . 8
⊢
2𝑜 ∈ ω |
30 | 28, 29 | sselii 3565 |
. . . . . . 7
⊢
2𝑜 ∈ Fin |
31 | | simprl 790 |
. . . . . . . 8
⊢ (((𝐽 ∈ Haus ∧ 𝐽 ∈ 1st𝜔
∧ 𝐴 ⊆ 𝑋) ∧ (𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵)) → 𝐴 ≼ 𝒫 𝐵) |
32 | 17 | brrelexi 5082 |
. . . . . . . 8
⊢ (𝐴 ≼ 𝒫 𝐵 → 𝐴 ∈ V) |
33 | 31, 32 | syl 17 |
. . . . . . 7
⊢ (((𝐽 ∈ Haus ∧ 𝐽 ∈ 1st𝜔
∧ 𝐴 ⊆ 𝑋) ∧ (𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵)) → 𝐴 ∈ V) |
34 | | fidomtri 8702 |
. . . . . . 7
⊢
((2𝑜 ∈ Fin ∧ 𝐴 ∈ V) → (2𝑜
≼ 𝐴 ↔ ¬
𝐴 ≺
2𝑜)) |
35 | 30, 33, 34 | sylancr 694 |
. . . . . 6
⊢ (((𝐽 ∈ Haus ∧ 𝐽 ∈ 1st𝜔
∧ 𝐴 ⊆ 𝑋) ∧ (𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵)) → (2𝑜 ≼
𝐴 ↔ ¬ 𝐴 ≺
2𝑜)) |
36 | 35 | biimpar 501 |
. . . . 5
⊢ ((((𝐽 ∈ Haus ∧ 𝐽 ∈ 1st𝜔
∧ 𝐴 ⊆ 𝑋) ∧ (𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵)) ∧ ¬ 𝐴 ≺ 2𝑜) →
2𝑜 ≼ 𝐴) |
37 | | numth3 9175 |
. . . . . . . . 9
⊢ (𝐵 ∈ V → 𝐵 ∈ dom
card) |
38 | 19, 37 | syl 17 |
. . . . . . . 8
⊢ (((𝐽 ∈ Haus ∧ 𝐽 ∈ 1st𝜔
∧ 𝐴 ⊆ 𝑋) ∧ (𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵)) → 𝐵 ∈ dom card) |
39 | 38 | adantr 480 |
. . . . . . 7
⊢ ((((𝐽 ∈ Haus ∧ 𝐽 ∈ 1st𝜔
∧ 𝐴 ⊆ 𝑋) ∧ (𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵)) ∧ 2𝑜 ≼ 𝐴) → 𝐵 ∈ dom card) |
40 | | nnenom 12641 |
. . . . . . . . . 10
⊢ ℕ
≈ ω |
41 | 40 | ensymi 7892 |
. . . . . . . . 9
⊢ ω
≈ ℕ |
42 | | endomtr 7900 |
. . . . . . . . 9
⊢ ((ω
≈ ℕ ∧ ℕ ≼ 𝐵) → ω ≼ 𝐵) |
43 | 41, 4, 42 | sylancr 694 |
. . . . . . . 8
⊢ (((𝐽 ∈ Haus ∧ 𝐽 ∈ 1st𝜔
∧ 𝐴 ⊆ 𝑋) ∧ (𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵)) → ω ≼ 𝐵) |
44 | 43 | adantr 480 |
. . . . . . 7
⊢ ((((𝐽 ∈ Haus ∧ 𝐽 ∈ 1st𝜔
∧ 𝐴 ⊆ 𝑋) ∧ (𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵)) ∧ 2𝑜 ≼ 𝐴) → ω ≼ 𝐵) |
45 | | simpr 476 |
. . . . . . 7
⊢ ((((𝐽 ∈ Haus ∧ 𝐽 ∈ 1st𝜔
∧ 𝐴 ⊆ 𝑋) ∧ (𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵)) ∧ 2𝑜 ≼ 𝐴) → 2𝑜
≼ 𝐴) |
46 | 31 | adantr 480 |
. . . . . . 7
⊢ ((((𝐽 ∈ Haus ∧ 𝐽 ∈ 1st𝜔
∧ 𝐴 ⊆ 𝑋) ∧ (𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵)) ∧ 2𝑜 ≼ 𝐴) → 𝐴 ≼ 𝒫 𝐵) |
47 | | mappwen 8818 |
. . . . . . 7
⊢ (((𝐵 ∈ dom card ∧ ω
≼ 𝐵) ∧
(2𝑜 ≼ 𝐴 ∧ 𝐴 ≼ 𝒫 𝐵)) → (𝐴 ↑𝑚 𝐵) ≈ 𝒫 𝐵) |
48 | 39, 44, 45, 46, 47 | syl22anc 1319 |
. . . . . 6
⊢ ((((𝐽 ∈ Haus ∧ 𝐽 ∈ 1st𝜔
∧ 𝐴 ⊆ 𝑋) ∧ (𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵)) ∧ 2𝑜 ≼ 𝐴) → (𝐴 ↑𝑚 𝐵) ≈ 𝒫 𝐵) |
49 | | endom 7868 |
. . . . . 6
⊢ ((𝐴 ↑𝑚
𝐵) ≈ 𝒫 𝐵 → (𝐴 ↑𝑚 𝐵) ≼ 𝒫 𝐵) |
50 | 48, 49 | syl 17 |
. . . . 5
⊢ ((((𝐽 ∈ Haus ∧ 𝐽 ∈ 1st𝜔
∧ 𝐴 ⊆ 𝑋) ∧ (𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵)) ∧ 2𝑜 ≼ 𝐴) → (𝐴 ↑𝑚 𝐵) ≼ 𝒫 𝐵) |
51 | 36, 50 | syldan 486 |
. . . 4
⊢ ((((𝐽 ∈ Haus ∧ 𝐽 ∈ 1st𝜔
∧ 𝐴 ⊆ 𝑋) ∧ (𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵)) ∧ ¬ 𝐴 ≺ 2𝑜) →
(𝐴
↑𝑚 𝐵) ≼ 𝒫 𝐵) |
52 | 25, 51 | pm2.61dan 828 |
. . 3
⊢ (((𝐽 ∈ Haus ∧ 𝐽 ∈ 1st𝜔
∧ 𝐴 ⊆ 𝑋) ∧ (𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵)) → (𝐴 ↑𝑚 𝐵) ≼ 𝒫 𝐵) |
53 | | domtr 7895 |
. . 3
⊢ (((𝐴 ↑𝑚
ℕ) ≼ (𝐴
↑𝑚 𝐵) ∧ (𝐴 ↑𝑚 𝐵) ≼ 𝒫 𝐵) → (𝐴 ↑𝑚 ℕ) ≼
𝒫 𝐵) |
54 | 12, 52, 53 | syl2anc 691 |
. 2
⊢ (((𝐽 ∈ Haus ∧ 𝐽 ∈ 1st𝜔
∧ 𝐴 ⊆ 𝑋) ∧ (𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵)) → (𝐴 ↑𝑚 ℕ) ≼
𝒫 𝐵) |
55 | | domtr 7895 |
. 2
⊢
((((cls‘𝐽)‘𝐴) ≼ (𝐴 ↑𝑚 ℕ) ∧
(𝐴
↑𝑚 ℕ) ≼ 𝒫 𝐵) → ((cls‘𝐽)‘𝐴) ≼ 𝒫 𝐵) |
56 | 3, 54, 55 | syl2anc 691 |
1
⊢ (((𝐽 ∈ Haus ∧ 𝐽 ∈ 1st𝜔
∧ 𝐴 ⊆ 𝑋) ∧ (𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵)) → ((cls‘𝐽)‘𝐴) ≼ 𝒫 𝐵) |