Metamath Proof Explorer


Theorem dif1card

Description: The cardinality of a nonempty finite set is one greater than the cardinality of the set with one element removed. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 2-Feb-2013)

Ref Expression
Assertion dif1card
|- ( ( A e. Fin /\ X e. A ) -> ( card ` A ) = suc ( card ` ( A \ { X } ) ) )

Proof

Step Hyp Ref Expression
1 diffi
 |-  ( A e. Fin -> ( A \ { X } ) e. Fin )
2 isfi
 |-  ( ( A \ { X } ) e. Fin <-> E. m e. _om ( A \ { X } ) ~~ m )
3 simp3
 |-  ( ( X e. A /\ m e. _om /\ ( A \ { X } ) ~~ m ) -> ( A \ { X } ) ~~ m )
4 en2sn
 |-  ( ( X e. A /\ m e. _om ) -> { X } ~~ { m } )
5 4 3adant3
 |-  ( ( X e. A /\ m e. _om /\ ( A \ { X } ) ~~ m ) -> { X } ~~ { m } )
6 disjdifr
 |-  ( ( A \ { X } ) i^i { X } ) = (/)
7 6 a1i
 |-  ( ( X e. A /\ m e. _om /\ ( A \ { X } ) ~~ m ) -> ( ( A \ { X } ) i^i { X } ) = (/) )
8 nnord
 |-  ( m e. _om -> Ord m )
9 ordirr
 |-  ( Ord m -> -. m e. m )
10 8 9 syl
 |-  ( m e. _om -> -. m e. m )
11 disjsn
 |-  ( ( m i^i { m } ) = (/) <-> -. m e. m )
12 10 11 sylibr
 |-  ( m e. _om -> ( m i^i { m } ) = (/) )
13 12 3ad2ant2
 |-  ( ( X e. A /\ m e. _om /\ ( A \ { X } ) ~~ m ) -> ( m i^i { m } ) = (/) )
14 unen
 |-  ( ( ( ( A \ { X } ) ~~ m /\ { X } ~~ { m } ) /\ ( ( ( A \ { X } ) i^i { X } ) = (/) /\ ( m i^i { m } ) = (/) ) ) -> ( ( A \ { X } ) u. { X } ) ~~ ( m u. { m } ) )
15 3 5 7 13 14 syl22anc
 |-  ( ( X e. A /\ m e. _om /\ ( A \ { X } ) ~~ m ) -> ( ( A \ { X } ) u. { X } ) ~~ ( m u. { m } ) )
16 difsnid
 |-  ( X e. A -> ( ( A \ { X } ) u. { X } ) = A )
17 df-suc
 |-  suc m = ( m u. { m } )
18 17 eqcomi
 |-  ( m u. { m } ) = suc m
19 18 a1i
 |-  ( X e. A -> ( m u. { m } ) = suc m )
20 16 19 breq12d
 |-  ( X e. A -> ( ( ( A \ { X } ) u. { X } ) ~~ ( m u. { m } ) <-> A ~~ suc m ) )
21 20 3ad2ant1
 |-  ( ( X e. A /\ m e. _om /\ ( A \ { X } ) ~~ m ) -> ( ( ( A \ { X } ) u. { X } ) ~~ ( m u. { m } ) <-> A ~~ suc m ) )
22 15 21 mpbid
 |-  ( ( X e. A /\ m e. _om /\ ( A \ { X } ) ~~ m ) -> A ~~ suc m )
23 peano2
 |-  ( m e. _om -> suc m e. _om )
24 23 3ad2ant2
 |-  ( ( X e. A /\ m e. _om /\ ( A \ { X } ) ~~ m ) -> suc m e. _om )
25 cardennn
 |-  ( ( A ~~ suc m /\ suc m e. _om ) -> ( card ` A ) = suc m )
26 22 24 25 syl2anc
 |-  ( ( X e. A /\ m e. _om /\ ( A \ { X } ) ~~ m ) -> ( card ` A ) = suc m )
27 cardennn
 |-  ( ( ( A \ { X } ) ~~ m /\ m e. _om ) -> ( card ` ( A \ { X } ) ) = m )
28 27 ancoms
 |-  ( ( m e. _om /\ ( A \ { X } ) ~~ m ) -> ( card ` ( A \ { X } ) ) = m )
29 28 3adant1
 |-  ( ( X e. A /\ m e. _om /\ ( A \ { X } ) ~~ m ) -> ( card ` ( A \ { X } ) ) = m )
30 suceq
 |-  ( ( card ` ( A \ { X } ) ) = m -> suc ( card ` ( A \ { X } ) ) = suc m )
31 29 30 syl
 |-  ( ( X e. A /\ m e. _om /\ ( A \ { X } ) ~~ m ) -> suc ( card ` ( A \ { X } ) ) = suc m )
32 26 31 eqtr4d
 |-  ( ( X e. A /\ m e. _om /\ ( A \ { X } ) ~~ m ) -> ( card ` A ) = suc ( card ` ( A \ { X } ) ) )
33 32 3expib
 |-  ( X e. A -> ( ( m e. _om /\ ( A \ { X } ) ~~ m ) -> ( card ` A ) = suc ( card ` ( A \ { X } ) ) ) )
34 33 com12
 |-  ( ( m e. _om /\ ( A \ { X } ) ~~ m ) -> ( X e. A -> ( card ` A ) = suc ( card ` ( A \ { X } ) ) ) )
35 34 rexlimiva
 |-  ( E. m e. _om ( A \ { X } ) ~~ m -> ( X e. A -> ( card ` A ) = suc ( card ` ( A \ { X } ) ) ) )
36 2 35 sylbi
 |-  ( ( A \ { X } ) e. Fin -> ( X e. A -> ( card ` A ) = suc ( card ` ( A \ { X } ) ) ) )
37 1 36 syl
 |-  ( A e. Fin -> ( X e. A -> ( card ` A ) = suc ( card ` ( A \ { X } ) ) ) )
38 37 imp
 |-  ( ( A e. Fin /\ X e. A ) -> ( card ` A ) = suc ( card ` ( A \ { X } ) ) )