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 ) )