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