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

Metamath Proof Explorer

Theorem infdju1

Description: An infinite set is equinumerous to itself added with one. (Contributed by Mario Carneiro, 15-May-2015)

Ref Expression
Assertion infdju1 ( ω ≼ 𝐴 → ( 𝐴 ⊔ 1o ) ≈ 𝐴 )

Proof

Step Hyp Ref Expression
1 difun2 ⊢ ( ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 1o ) ) ∖ ( { 1o } × 1o ) ) = ( ( { ∅ } × 𝐴 ) ∖ ( { 1o } × 1o ) )
2 df-dju ⊢ ( 𝐴 ⊔ 1o ) = ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 1o ) )
3 df1o2 ⊢ 1o = { ∅ }
4 3 xpeq2i ⊢ ( { 1o } × 1o ) = ( { 1o } × { ∅ } )
5 1oex ⊢ 1o ∈ V
6 0ex ⊢ ∅ ∈ V
7 5 6 xpsn ⊢ ( { 1o } × { ∅ } ) = { ⟨ 1o , ∅ ⟩ }
8 4 7 eqtr2i ⊢ { ⟨ 1o , ∅ ⟩ } = ( { 1o } × 1o )
9 2 8 difeq12i ⊢ ( ( 𝐴 ⊔ 1o ) ∖ { ⟨ 1o , ∅ ⟩ } ) = ( ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 1o ) ) ∖ ( { 1o } × 1o ) )
10 xp01disjl ⊢ ( ( { ∅ } × 𝐴 ) ∩ ( { 1o } × 1o ) ) = ∅
11 disj3 ⊢ ( ( ( { ∅ } × 𝐴 ) ∩ ( { 1o } × 1o ) ) = ∅ ↔ ( { ∅ } × 𝐴 ) = ( ( { ∅ } × 𝐴 ) ∖ ( { 1o } × 1o ) ) )
12 10 11 mpbi ⊢ ( { ∅ } × 𝐴 ) = ( ( { ∅ } × 𝐴 ) ∖ ( { 1o } × 1o ) )
13 1 9 12 3eqtr4i ⊢ ( ( 𝐴 ⊔ 1o ) ∖ { ⟨ 1o , ∅ ⟩ } ) = ( { ∅ } × 𝐴 )
14 reldom ⊢ Rel ≼
15 14 brrelex2i ⊢ ( ω ≼ 𝐴 → 𝐴 ∈ V )
16 1on ⊢ 1o ∈ On
17 djudoml ⊢ ( ( 𝐴 ∈ V ∧ 1o ∈ On ) → 𝐴 ≼ ( 𝐴 ⊔ 1o ) )
18 15 16 17 sylancl ⊢ ( ω ≼ 𝐴 → 𝐴 ≼ ( 𝐴 ⊔ 1o ) )
19 domtr ⊢ ( ( ω ≼ 𝐴 ∧ 𝐴 ≼ ( 𝐴 ⊔ 1o ) ) → ω ≼ ( 𝐴 ⊔ 1o ) )
20 18 19 mpdan ⊢ ( ω ≼ 𝐴 → ω ≼ ( 𝐴 ⊔ 1o ) )
21 infdifsn ⊢ ( ω ≼ ( 𝐴 ⊔ 1o ) → ( ( 𝐴 ⊔ 1o ) ∖ { ⟨ 1o , ∅ ⟩ } ) ≈ ( 𝐴 ⊔ 1o ) )
22 20 21 syl ⊢ ( ω ≼ 𝐴 → ( ( 𝐴 ⊔ 1o ) ∖ { ⟨ 1o , ∅ ⟩ } ) ≈ ( 𝐴 ⊔ 1o ) )
23 13 22 eqbrtrrid ⊢ ( ω ≼ 𝐴 → ( { ∅ } × 𝐴 ) ≈ ( 𝐴 ⊔ 1o ) )
24 23 ensymd ⊢ ( ω ≼ 𝐴 → ( 𝐴 ⊔ 1o ) ≈ ( { ∅ } × 𝐴 ) )
25 xpsnen2g ⊢ ( ( ∅ ∈ V ∧ 𝐴 ∈ V ) → ( { ∅ } × 𝐴 ) ≈ 𝐴 )
26 6 15 25 sylancr ⊢ ( ω ≼ 𝐴 → ( { ∅ } × 𝐴 ) ≈ 𝐴 )
27 entr ⊢ ( ( ( 𝐴 ⊔ 1o ) ≈ ( { ∅ } × 𝐴 ) ∧ ( { ∅ } × 𝐴 ) ≈ 𝐴 ) → ( 𝐴 ⊔ 1o ) ≈ 𝐴 )
28 24 26 27 syl2anc ⊢ ( ω ≼ 𝐴 → ( 𝐴 ⊔ 1o ) ≈ 𝐴 )