Metamath Proof Explorer


Theorem hauspwdom

Description: Simplify the cardinal A ^ NN of hausmapdom to ~P B = 2 ^ B when B is an infinite cardinal greater than A . (Contributed by Mario Carneiro, 9-Apr-2015) (Revised by Mario Carneiro, 30-Apr-2015)

Ref Expression
Hypothesis hauspwdom.1 𝑋 = 𝐽
Assertion hauspwdom ( ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴𝑋 ) ∧ ( 𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵 ) ) → ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ≼ 𝒫 𝐵 )

Proof

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 𝐵 ) ≼ ( 2om 𝐵 ) )
16 14 15 syl ( ( ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴𝑋 ) ∧ ( 𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵 ) ) ∧ 𝐴 ≺ 2o ) → ( 𝐴m 𝐵 ) ≼ ( 2om 𝐵 ) )
17 reldom Rel ≼
18 17 brrelex2i ( ℕ ≼ 𝐵𝐵 ∈ V )
19 18 ad2antll ( ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴𝑋 ) ∧ ( 𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵 ) ) → 𝐵 ∈ V )
20 pw2eng ( 𝐵 ∈ V → 𝒫 𝐵 ≈ ( 2om 𝐵 ) )
21 ensym ( 𝒫 𝐵 ≈ ( 2om 𝐵 ) → ( 2om 𝐵 ) ≈ 𝒫 𝐵 )
22 19 20 21 3syl ( ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴𝑋 ) ∧ ( 𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵 ) ) → ( 2om 𝐵 ) ≈ 𝒫 𝐵 )
23 22 adantr ( ( ( ( 𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴𝑋 ) ∧ ( 𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵 ) ) ∧ 𝐴 ≺ 2o ) → ( 2om 𝐵 ) ≈ 𝒫 𝐵 )
24 domentr ( ( ( 𝐴m 𝐵 ) ≼ ( 2om 𝐵 ) ∧ ( 2om 𝐵 ) ≈ 𝒫 𝐵 ) → ( 𝐴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 ‘ 𝐽 ) ‘ 𝐴 ) ≼ 𝒫 𝐵 )