This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 𝐵 ) ≼ ( 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 ‘ 𝐽 ) ‘ 𝐴 ) ≼ 𝒫 𝐵 )