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

Metamath Proof Explorer

Theorem unsnen

Description: Equinumerosity of a set with a new element added. (Contributed by NM, 7-Nov-2008)

Ref Expression
Hypotheses unsnen.1 ⊢ 𝐴 ∈ V
unsnen.2 ⊢ 𝐵 ∈ V
Assertion unsnen ( ¬ 𝐵 ∈ 𝐴 → ( 𝐴 ∪ { 𝐵 } ) ≈ suc ( card ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 unsnen.1 ⊢ 𝐴 ∈ V
2 unsnen.2 ⊢ 𝐵 ∈ V
3 disjsn ⊢ ( ( 𝐴 ∩ { 𝐵 } ) = ∅ ↔ ¬ 𝐵 ∈ 𝐴 )
4 cardon ⊢ ( card ‘ 𝐴 ) ∈ On
5 4 onordi ⊢ Ord ( card ‘ 𝐴 )
6 orddisj ⊢ ( Ord ( card ‘ 𝐴 ) → ( ( card ‘ 𝐴 ) ∩ { ( card ‘ 𝐴 ) } ) = ∅ )
7 5 6 ax-mp ⊢ ( ( card ‘ 𝐴 ) ∩ { ( card ‘ 𝐴 ) } ) = ∅
8 1 cardid ⊢ ( card ‘ 𝐴 ) ≈ 𝐴
9 8 ensymi ⊢ 𝐴 ≈ ( card ‘ 𝐴 )
10 fvex ⊢ ( card ‘ 𝐴 ) ∈ V
11 en2sn ⊢ ( ( 𝐵 ∈ V ∧ ( card ‘ 𝐴 ) ∈ V ) → { 𝐵 } ≈ { ( card ‘ 𝐴 ) } )
12 2 10 11 mp2an ⊢ { 𝐵 } ≈ { ( card ‘ 𝐴 ) }
13 unen ⊢ ( ( ( 𝐴 ≈ ( card ‘ 𝐴 ) ∧ { 𝐵 } ≈ { ( card ‘ 𝐴 ) } ) ∧ ( ( 𝐴 ∩ { 𝐵 } ) = ∅ ∧ ( ( card ‘ 𝐴 ) ∩ { ( card ‘ 𝐴 ) } ) = ∅ ) ) → ( 𝐴 ∪ { 𝐵 } ) ≈ ( ( card ‘ 𝐴 ) ∪ { ( card ‘ 𝐴 ) } ) )
14 9 12 13 mpanl12 ⊢ ( ( ( 𝐴 ∩ { 𝐵 } ) = ∅ ∧ ( ( card ‘ 𝐴 ) ∩ { ( card ‘ 𝐴 ) } ) = ∅ ) → ( 𝐴 ∪ { 𝐵 } ) ≈ ( ( card ‘ 𝐴 ) ∪ { ( card ‘ 𝐴 ) } ) )
15 7 14 mpan2 ⊢ ( ( 𝐴 ∩ { 𝐵 } ) = ∅ → ( 𝐴 ∪ { 𝐵 } ) ≈ ( ( card ‘ 𝐴 ) ∪ { ( card ‘ 𝐴 ) } ) )
16 3 15 sylbir ⊢ ( ¬ 𝐵 ∈ 𝐴 → ( 𝐴 ∪ { 𝐵 } ) ≈ ( ( card ‘ 𝐴 ) ∪ { ( card ‘ 𝐴 ) } ) )
17 df-suc ⊢ suc ( card ‘ 𝐴 ) = ( ( card ‘ 𝐴 ) ∪ { ( card ‘ 𝐴 ) } )
18 16 17 breqtrrdi ⊢ ( ¬ 𝐵 ∈ 𝐴 → ( 𝐴 ∪ { 𝐵 } ) ≈ suc ( card ‘ 𝐴 ) )