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