Step |
Hyp |
Ref |
Expression |
1 |
|
hauspwdom.1 |
⊢ 𝑋 = ∪ 𝐽 |
2 |
1
|
hausmapdom |
⊢ ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴 ⊆ 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ≼ ( 𝐴 ↑m ℕ ) ) |
3 |
2
|
adantr |
⊢ ( ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵 ) ) → ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ≼ ( 𝐴 ↑m ℕ ) ) |
4 |
|
simprr |
⊢ ( ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵 ) ) → ℕ ≼ 𝐵 ) |
5 |
|
1nn |
⊢ 1 ∈ ℕ |
6 |
|
noel |
⊢ ¬ 1 ∈ ∅ |
7 |
|
eleq2 |
⊢ ( ℕ = ∅ → ( 1 ∈ ℕ ↔ 1 ∈ ∅ ) ) |
8 |
6 7
|
mtbiri |
⊢ ( ℕ = ∅ → ¬ 1 ∈ ℕ ) |
9 |
8
|
adantr |
⊢ ( ( ℕ = ∅ ∧ 𝐴 = ∅ ) → ¬ 1 ∈ ℕ ) |
10 |
5 9
|
mt2 |
⊢ ¬ ( ℕ = ∅ ∧ 𝐴 = ∅ ) |
11 |
|
mapdom2 |
⊢ ( ( ℕ ≼ 𝐵 ∧ ¬ ( ℕ = ∅ ∧ 𝐴 = ∅ ) ) → ( 𝐴 ↑m ℕ ) ≼ ( 𝐴 ↑m 𝐵 ) ) |
12 |
4 10 11
|
sylancl |
⊢ ( ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵 ) ) → ( 𝐴 ↑m ℕ ) ≼ ( 𝐴 ↑m 𝐵 ) ) |
13 |
|
sdomdom |
⊢ ( 𝐴 ≺ 2o → 𝐴 ≼ 2o ) |
14 |
13
|
adantl |
⊢ ( ( ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵 ) ) ∧ 𝐴 ≺ 2o ) → 𝐴 ≼ 2o ) |
15 |
|
mapdom1 |
⊢ ( 𝐴 ≼ 2o → ( 𝐴 ↑m 𝐵 ) ≼ ( 2o ↑m 𝐵 ) ) |
16 |
14 15
|
syl |
⊢ ( ( ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵 ) ) ∧ 𝐴 ≺ 2o ) → ( 𝐴 ↑m 𝐵 ) ≼ ( 2o ↑m 𝐵 ) ) |
17 |
|
reldom |
⊢ Rel ≼ |
18 |
17
|
brrelex2i |
⊢ ( ℕ ≼ 𝐵 → 𝐵 ∈ V ) |
19 |
18
|
ad2antll |
⊢ ( ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵 ) ) → 𝐵 ∈ V ) |
20 |
|
pw2eng |
⊢ ( 𝐵 ∈ V → 𝒫 𝐵 ≈ ( 2o ↑m 𝐵 ) ) |
21 |
|
ensym |
⊢ ( 𝒫 𝐵 ≈ ( 2o ↑m 𝐵 ) → ( 2o ↑m 𝐵 ) ≈ 𝒫 𝐵 ) |
22 |
19 20 21
|
3syl |
⊢ ( ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵 ) ) → ( 2o ↑m 𝐵 ) ≈ 𝒫 𝐵 ) |
23 |
22
|
adantr |
⊢ ( ( ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵 ) ) ∧ 𝐴 ≺ 2o ) → ( 2o ↑m 𝐵 ) ≈ 𝒫 𝐵 ) |
24 |
|
domentr |
⊢ ( ( ( 𝐴 ↑m 𝐵 ) ≼ ( 2o ↑m 𝐵 ) ∧ ( 2o ↑m 𝐵 ) ≈ 𝒫 𝐵 ) → ( 𝐴 ↑m 𝐵 ) ≼ 𝒫 𝐵 ) |
25 |
16 23 24
|
syl2anc |
⊢ ( ( ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵 ) ) ∧ 𝐴 ≺ 2o ) → ( 𝐴 ↑m 𝐵 ) ≼ 𝒫 𝐵 ) |
26 |
|
onfin2 |
⊢ ω = ( On ∩ Fin ) |
27 |
|
inss2 |
⊢ ( On ∩ Fin ) ⊆ Fin |
28 |
26 27
|
eqsstri |
⊢ ω ⊆ Fin |
29 |
|
2onn |
⊢ 2o ∈ ω |
30 |
28 29
|
sselii |
⊢ 2o ∈ Fin |
31 |
|
simprl |
⊢ ( ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵 ) ) → 𝐴 ≼ 𝒫 𝐵 ) |
32 |
17
|
brrelex1i |
⊢ ( 𝐴 ≼ 𝒫 𝐵 → 𝐴 ∈ V ) |
33 |
31 32
|
syl |
⊢ ( ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵 ) ) → 𝐴 ∈ V ) |
34 |
|
fidomtri |
⊢ ( ( 2o ∈ Fin ∧ 𝐴 ∈ V ) → ( 2o ≼ 𝐴 ↔ ¬ 𝐴 ≺ 2o ) ) |
35 |
30 33 34
|
sylancr |
⊢ ( ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵 ) ) → ( 2o ≼ 𝐴 ↔ ¬ 𝐴 ≺ 2o ) ) |
36 |
35
|
biimpar |
⊢ ( ( ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵 ) ) ∧ ¬ 𝐴 ≺ 2o ) → 2o ≼ 𝐴 ) |
37 |
|
numth3 |
⊢ ( 𝐵 ∈ V → 𝐵 ∈ dom card ) |
38 |
19 37
|
syl |
⊢ ( ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵 ) ) → 𝐵 ∈ dom card ) |
39 |
38
|
adantr |
⊢ ( ( ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵 ) ) ∧ 2o ≼ 𝐴 ) → 𝐵 ∈ dom card ) |
40 |
|
nnenom |
⊢ ℕ ≈ ω |
41 |
40
|
ensymi |
⊢ ω ≈ ℕ |
42 |
|
endomtr |
⊢ ( ( ω ≈ ℕ ∧ ℕ ≼ 𝐵 ) → ω ≼ 𝐵 ) |
43 |
41 4 42
|
sylancr |
⊢ ( ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵 ) ) → ω ≼ 𝐵 ) |
44 |
43
|
adantr |
⊢ ( ( ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵 ) ) ∧ 2o ≼ 𝐴 ) → ω ≼ 𝐵 ) |
45 |
|
simpr |
⊢ ( ( ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵 ) ) ∧ 2o ≼ 𝐴 ) → 2o ≼ 𝐴 ) |
46 |
31
|
adantr |
⊢ ( ( ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵 ) ) ∧ 2o ≼ 𝐴 ) → 𝐴 ≼ 𝒫 𝐵 ) |
47 |
|
mappwen |
⊢ ( ( ( 𝐵 ∈ dom card ∧ ω ≼ 𝐵 ) ∧ ( 2o ≼ 𝐴 ∧ 𝐴 ≼ 𝒫 𝐵 ) ) → ( 𝐴 ↑m 𝐵 ) ≈ 𝒫 𝐵 ) |
48 |
39 44 45 46 47
|
syl22anc |
⊢ ( ( ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵 ) ) ∧ 2o ≼ 𝐴 ) → ( 𝐴 ↑m 𝐵 ) ≈ 𝒫 𝐵 ) |
49 |
|
endom |
⊢ ( ( 𝐴 ↑m 𝐵 ) ≈ 𝒫 𝐵 → ( 𝐴 ↑m 𝐵 ) ≼ 𝒫 𝐵 ) |
50 |
48 49
|
syl |
⊢ ( ( ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵 ) ) ∧ 2o ≼ 𝐴 ) → ( 𝐴 ↑m 𝐵 ) ≼ 𝒫 𝐵 ) |
51 |
36 50
|
syldan |
⊢ ( ( ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵 ) ) ∧ ¬ 𝐴 ≺ 2o ) → ( 𝐴 ↑m 𝐵 ) ≼ 𝒫 𝐵 ) |
52 |
25 51
|
pm2.61dan |
⊢ ( ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵 ) ) → ( 𝐴 ↑m 𝐵 ) ≼ 𝒫 𝐵 ) |
53 |
|
domtr |
⊢ ( ( ( 𝐴 ↑m ℕ ) ≼ ( 𝐴 ↑m 𝐵 ) ∧ ( 𝐴 ↑m 𝐵 ) ≼ 𝒫 𝐵 ) → ( 𝐴 ↑m ℕ ) ≼ 𝒫 𝐵 ) |
54 |
12 52 53
|
syl2anc |
⊢ ( ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵 ) ) → ( 𝐴 ↑m ℕ ) ≼ 𝒫 𝐵 ) |
55 |
|
domtr |
⊢ ( ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ≼ ( 𝐴 ↑m ℕ ) ∧ ( 𝐴 ↑m ℕ ) ≼ 𝒫 𝐵 ) → ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ≼ 𝒫 𝐵 ) |
56 |
3 54 55
|
syl2anc |
⊢ ( ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴 ⊆ 𝑋 ) ∧ ( 𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵 ) ) → ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ≼ 𝒫 𝐵 ) |