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
|- A e. _V
unsnen.2
|- B e. _V
Assertion unsnen
|- ( -. B e. A -> ( A u. { B } ) ~~ suc ( card ` A ) )

Proof

Step Hyp Ref Expression
1 unsnen.1
 |-  A e. _V
2 unsnen.2
 |-  B e. _V
3 disjsn
 |-  ( ( A i^i { B } ) = (/) <-> -. B e. A )
4 cardon
 |-  ( card ` A ) e. On
5 4 onordi
 |-  Ord ( card ` A )
6 orddisj
 |-  ( Ord ( card ` A ) -> ( ( card ` A ) i^i { ( card ` A ) } ) = (/) )
7 5 6 ax-mp
 |-  ( ( card ` A ) i^i { ( card ` A ) } ) = (/)
8 1 cardid
 |-  ( card ` A ) ~~ A
9 8 ensymi
 |-  A ~~ ( card ` A )
10 fvex
 |-  ( card ` A ) e. _V
11 en2sn
 |-  ( ( B e. _V /\ ( card ` A ) e. _V ) -> { B } ~~ { ( card ` A ) } )
12 2 10 11 mp2an
 |-  { B } ~~ { ( card ` A ) }
13 unen
 |-  ( ( ( A ~~ ( card ` A ) /\ { B } ~~ { ( card ` A ) } ) /\ ( ( A i^i { B } ) = (/) /\ ( ( card ` A ) i^i { ( card ` A ) } ) = (/) ) ) -> ( A u. { B } ) ~~ ( ( card ` A ) u. { ( card ` A ) } ) )
14 9 12 13 mpanl12
 |-  ( ( ( A i^i { B } ) = (/) /\ ( ( card ` A ) i^i { ( card ` A ) } ) = (/) ) -> ( A u. { B } ) ~~ ( ( card ` A ) u. { ( card ` A ) } ) )
15 7 14 mpan2
 |-  ( ( A i^i { B } ) = (/) -> ( A u. { B } ) ~~ ( ( card ` A ) u. { ( card ` A ) } ) )
16 3 15 sylbir
 |-  ( -. B e. A -> ( A u. { B } ) ~~ ( ( card ` A ) u. { ( card ` A ) } ) )
17 df-suc
 |-  suc ( card ` A ) = ( ( card ` A ) u. { ( card ` A ) } )
18 16 17 breqtrrdi
 |-  ( -. B e. A -> ( A u. { B } ) ~~ suc ( card ` A ) )