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

Metamath Proof Explorer

Theorem pwxpndom2

Description: The powerset of a Dedekind-infinite set does not inject into its Cartesian product with itself. (Contributed by Mario Carneiro, 31-May-2015) (Proof shortened by AV, 18-Jul-2022)

Ref Expression
Assertion pwxpndom2 ( ω ≼ 𝐴 → ¬ 𝒫 𝐴 ≼ ( 𝐴 ⊔ ( 𝐴 × 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 pwfseq ⊢ ( ω ≼ 𝐴 → ¬ 𝒫 𝐴 ≼ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) )
2 reldom ⊢ Rel ≼
3 2 brrelex2i ⊢ ( ω ≼ 𝐴 → 𝐴 ∈ V )
4 df1o2 ⊢ 1o = { ∅ }
5 4 oveq2i ⊢ ( 𝐴 ↑m 1o ) = ( 𝐴 ↑m { ∅ } )
6 id ⊢ ( 𝐴 ∈ V → 𝐴 ∈ V )
7 0ex ⊢ ∅ ∈ V
8 7 a1i ⊢ ( 𝐴 ∈ V → ∅ ∈ V )
9 6 8 mapsnend ⊢ ( 𝐴 ∈ V → ( 𝐴 ↑m { ∅ } ) ≈ 𝐴 )
10 5 9 eqbrtrid ⊢ ( 𝐴 ∈ V → ( 𝐴 ↑m 1o ) ≈ 𝐴 )
11 ensym ⊢ ( ( 𝐴 ↑m 1o ) ≈ 𝐴 → 𝐴 ≈ ( 𝐴 ↑m 1o ) )
12 3 10 11 3syl ⊢ ( ω ≼ 𝐴 → 𝐴 ≈ ( 𝐴 ↑m 1o ) )
13 map2xp ⊢ ( 𝐴 ∈ V → ( 𝐴 ↑m 2o ) ≈ ( 𝐴 × 𝐴 ) )
14 ensym ⊢ ( ( 𝐴 ↑m 2o ) ≈ ( 𝐴 × 𝐴 ) → ( 𝐴 × 𝐴 ) ≈ ( 𝐴 ↑m 2o ) )
15 3 13 14 3syl ⊢ ( ω ≼ 𝐴 → ( 𝐴 × 𝐴 ) ≈ ( 𝐴 ↑m 2o ) )
16 elmapi ⊢ ( 𝑥 ∈ ( 𝐴 ↑m 1o ) → 𝑥 : 1o ⟶ 𝐴 )
17 16 fdmd ⊢ ( 𝑥 ∈ ( 𝐴 ↑m 1o ) → dom 𝑥 = 1o )
18 17 adantr ⊢ ( ( 𝑥 ∈ ( 𝐴 ↑m 1o ) ∧ 𝑥 ∈ ( 𝐴 ↑m 2o ) ) → dom 𝑥 = 1o )
19 1oex ⊢ 1o ∈ V
20 19 sucid ⊢ 1o ∈ suc 1o
21 df-2o ⊢ 2o = suc 1o
22 20 21 eleqtrri ⊢ 1o ∈ 2o
23 1on ⊢ 1o ∈ On
24 23 onirri ⊢ ¬ 1o ∈ 1o
25 nelneq2 ⊢ ( ( 1o ∈ 2o ∧ ¬ 1o ∈ 1o ) → ¬ 2o = 1o )
26 22 24 25 mp2an ⊢ ¬ 2o = 1o
27 elmapi ⊢ ( 𝑥 ∈ ( 𝐴 ↑m 2o ) → 𝑥 : 2o ⟶ 𝐴 )
28 27 fdmd ⊢ ( 𝑥 ∈ ( 𝐴 ↑m 2o ) → dom 𝑥 = 2o )
29 28 adantl ⊢ ( ( 𝑥 ∈ ( 𝐴 ↑m 1o ) ∧ 𝑥 ∈ ( 𝐴 ↑m 2o ) ) → dom 𝑥 = 2o )
30 29 eqeq1d ⊢ ( ( 𝑥 ∈ ( 𝐴 ↑m 1o ) ∧ 𝑥 ∈ ( 𝐴 ↑m 2o ) ) → ( dom 𝑥 = 1o ↔ 2o = 1o ) )
31 26 30 mtbiri ⊢ ( ( 𝑥 ∈ ( 𝐴 ↑m 1o ) ∧ 𝑥 ∈ ( 𝐴 ↑m 2o ) ) → ¬ dom 𝑥 = 1o )
32 18 31 pm2.65i ⊢ ¬ ( 𝑥 ∈ ( 𝐴 ↑m 1o ) ∧ 𝑥 ∈ ( 𝐴 ↑m 2o ) )
33 elin ⊢ ( 𝑥 ∈ ( ( 𝐴 ↑m 1o ) ∩ ( 𝐴 ↑m 2o ) ) ↔ ( 𝑥 ∈ ( 𝐴 ↑m 1o ) ∧ 𝑥 ∈ ( 𝐴 ↑m 2o ) ) )
34 32 33 mtbir ⊢ ¬ 𝑥 ∈ ( ( 𝐴 ↑m 1o ) ∩ ( 𝐴 ↑m 2o ) )
35 34 a1i ⊢ ( ω ≼ 𝐴 → ¬ 𝑥 ∈ ( ( 𝐴 ↑m 1o ) ∩ ( 𝐴 ↑m 2o ) ) )
36 35 eq0rdv ⊢ ( ω ≼ 𝐴 → ( ( 𝐴 ↑m 1o ) ∩ ( 𝐴 ↑m 2o ) ) = ∅ )
37 djuenun ⊢ ( ( 𝐴 ≈ ( 𝐴 ↑m 1o ) ∧ ( 𝐴 × 𝐴 ) ≈ ( 𝐴 ↑m 2o ) ∧ ( ( 𝐴 ↑m 1o ) ∩ ( 𝐴 ↑m 2o ) ) = ∅ ) → ( 𝐴 ⊔ ( 𝐴 × 𝐴 ) ) ≈ ( ( 𝐴 ↑m 1o ) ∪ ( 𝐴 ↑m 2o ) ) )
38 12 15 36 37 syl3anc ⊢ ( ω ≼ 𝐴 → ( 𝐴 ⊔ ( 𝐴 × 𝐴 ) ) ≈ ( ( 𝐴 ↑m 1o ) ∪ ( 𝐴 ↑m 2o ) ) )
39 omex ⊢ ω ∈ V
40 ovex ⊢ ( 𝐴 ↑m 𝑛 ) ∈ V
41 39 40 iunex ⊢ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ∈ V
42 1onn ⊢ 1o ∈ ω
43 oveq2 ⊢ ( 𝑛 = 1o → ( 𝐴 ↑m 𝑛 ) = ( 𝐴 ↑m 1o ) )
44 43 ssiun2s ⊢ ( 1o ∈ ω → ( 𝐴 ↑m 1o ) ⊆ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) )
45 42 44 ax-mp ⊢ ( 𝐴 ↑m 1o ) ⊆ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 )
46 2onn ⊢ 2o ∈ ω
47 oveq2 ⊢ ( 𝑛 = 2o → ( 𝐴 ↑m 𝑛 ) = ( 𝐴 ↑m 2o ) )
48 47 ssiun2s ⊢ ( 2o ∈ ω → ( 𝐴 ↑m 2o ) ⊆ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) )
49 46 48 ax-mp ⊢ ( 𝐴 ↑m 2o ) ⊆ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 )
50 45 49 unssi ⊢ ( ( 𝐴 ↑m 1o ) ∪ ( 𝐴 ↑m 2o ) ) ⊆ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 )
51 ssdomg ⊢ ( ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ∈ V → ( ( ( 𝐴 ↑m 1o ) ∪ ( 𝐴 ↑m 2o ) ) ⊆ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) → ( ( 𝐴 ↑m 1o ) ∪ ( 𝐴 ↑m 2o ) ) ≼ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ) )
52 41 50 51 mp2 ⊢ ( ( 𝐴 ↑m 1o ) ∪ ( 𝐴 ↑m 2o ) ) ≼ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 )
53 endomtr ⊢ ( ( ( 𝐴 ⊔ ( 𝐴 × 𝐴 ) ) ≈ ( ( 𝐴 ↑m 1o ) ∪ ( 𝐴 ↑m 2o ) ) ∧ ( ( 𝐴 ↑m 1o ) ∪ ( 𝐴 ↑m 2o ) ) ≼ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ) → ( 𝐴 ⊔ ( 𝐴 × 𝐴 ) ) ≼ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) )
54 38 52 53 sylancl ⊢ ( ω ≼ 𝐴 → ( 𝐴 ⊔ ( 𝐴 × 𝐴 ) ) ≼ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) )
55 domtr ⊢ ( ( 𝒫 𝐴 ≼ ( 𝐴 ⊔ ( 𝐴 × 𝐴 ) ) ∧ ( 𝐴 ⊔ ( 𝐴 × 𝐴 ) ) ≼ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ) → 𝒫 𝐴 ≼ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) )
56 55 expcom ⊢ ( ( 𝐴 ⊔ ( 𝐴 × 𝐴 ) ) ≼ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) → ( 𝒫 𝐴 ≼ ( 𝐴 ⊔ ( 𝐴 × 𝐴 ) ) → 𝒫 𝐴 ≼ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ) )
57 54 56 syl ⊢ ( ω ≼ 𝐴 → ( 𝒫 𝐴 ≼ ( 𝐴 ⊔ ( 𝐴 × 𝐴 ) ) → 𝒫 𝐴 ≼ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ) )
58 1 57 mtod ⊢ ( ω ≼ 𝐴 → ¬ 𝒫 𝐴 ≼ ( 𝐴 ⊔ ( 𝐴 × 𝐴 ) ) )