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

Metamath Proof Explorer

Theorem pwdjundom

Description: The powerset of a Dedekind-infinite set does not inject into its cardinal sum with itself. (Contributed by Mario Carneiro, 31-May-2015)

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

Proof

Step Hyp Ref Expression
1 pwxpndom2 ⊢ ( ω ≼ 𝐴 → ¬ 𝒫 𝐴 ≼ ( 𝐴 ⊔ ( 𝐴 × 𝐴 ) ) )
2 df1o2 ⊢ 1o = { ∅ }
3 2 xpeq1i ⊢ ( 1o × 𝐴 ) = ( { ∅ } × 𝐴 )
4 0ex ⊢ ∅ ∈ V
5 reldom ⊢ Rel ≼
6 5 brrelex2i ⊢ ( ω ≼ 𝐴 → 𝐴 ∈ V )
7 xpsnen2g ⊢ ( ( ∅ ∈ V ∧ 𝐴 ∈ V ) → ( { ∅ } × 𝐴 ) ≈ 𝐴 )
8 4 6 7 sylancr ⊢ ( ω ≼ 𝐴 → ( { ∅ } × 𝐴 ) ≈ 𝐴 )
9 3 8 eqbrtrid ⊢ ( ω ≼ 𝐴 → ( 1o × 𝐴 ) ≈ 𝐴 )
10 9 ensymd ⊢ ( ω ≼ 𝐴 → 𝐴 ≈ ( 1o × 𝐴 ) )
11 omex ⊢ ω ∈ V
12 ordom ⊢ Ord ω
13 1onn ⊢ 1o ∈ ω
14 ordelss ⊢ ( ( Ord ω ∧ 1o ∈ ω ) → 1o ⊆ ω )
15 12 13 14 mp2an ⊢ 1o ⊆ ω
16 ssdomg ⊢ ( ω ∈ V → ( 1o ⊆ ω → 1o ≼ ω ) )
17 11 15 16 mp2 ⊢ 1o ≼ ω
18 domtr ⊢ ( ( 1o ≼ ω ∧ ω ≼ 𝐴 ) → 1o ≼ 𝐴 )
19 17 18 mpan ⊢ ( ω ≼ 𝐴 → 1o ≼ 𝐴 )
20 xpdom1g ⊢ ( ( 𝐴 ∈ V ∧ 1o ≼ 𝐴 ) → ( 1o × 𝐴 ) ≼ ( 𝐴 × 𝐴 ) )
21 6 19 20 syl2anc ⊢ ( ω ≼ 𝐴 → ( 1o × 𝐴 ) ≼ ( 𝐴 × 𝐴 ) )
22 endomtr ⊢ ( ( 𝐴 ≈ ( 1o × 𝐴 ) ∧ ( 1o × 𝐴 ) ≼ ( 𝐴 × 𝐴 ) ) → 𝐴 ≼ ( 𝐴 × 𝐴 ) )
23 10 21 22 syl2anc ⊢ ( ω ≼ 𝐴 → 𝐴 ≼ ( 𝐴 × 𝐴 ) )
24 djudom2 ⊢ ( ( 𝐴 ≼ ( 𝐴 × 𝐴 ) ∧ 𝐴 ∈ V ) → ( 𝐴 ⊔ 𝐴 ) ≼ ( 𝐴 ⊔ ( 𝐴 × 𝐴 ) ) )
25 23 6 24 syl2anc ⊢ ( ω ≼ 𝐴 → ( 𝐴 ⊔ 𝐴 ) ≼ ( 𝐴 ⊔ ( 𝐴 × 𝐴 ) ) )
26 domtr ⊢ ( ( 𝒫 𝐴 ≼ ( 𝐴 ⊔ 𝐴 ) ∧ ( 𝐴 ⊔ 𝐴 ) ≼ ( 𝐴 ⊔ ( 𝐴 × 𝐴 ) ) ) → 𝒫 𝐴 ≼ ( 𝐴 ⊔ ( 𝐴 × 𝐴 ) ) )
27 26 expcom ⊢ ( ( 𝐴 ⊔ 𝐴 ) ≼ ( 𝐴 ⊔ ( 𝐴 × 𝐴 ) ) → ( 𝒫 𝐴 ≼ ( 𝐴 ⊔ 𝐴 ) → 𝒫 𝐴 ≼ ( 𝐴 ⊔ ( 𝐴 × 𝐴 ) ) ) )
28 25 27 syl ⊢ ( ω ≼ 𝐴 → ( 𝒫 𝐴 ≼ ( 𝐴 ⊔ 𝐴 ) → 𝒫 𝐴 ≼ ( 𝐴 ⊔ ( 𝐴 × 𝐴 ) ) ) )
29 1 28 mtod ⊢ ( ω ≼ 𝐴 → ¬ 𝒫 𝐴 ≼ ( 𝐴 ⊔ 𝐴 ) )