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 ( ( 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐴 ) → ( card ‘ 𝐴 ) = suc ( card ‘ ( 𝐴 ∖ { 𝑋 } ) ) )

Proof

Step Hyp Ref Expression
1 diffi ⊢ ( 𝐴 ∈ Fin → ( 𝐴 ∖ { 𝑋 } ) ∈ Fin )
2 isfi ⊢ ( ( 𝐴 ∖ { 𝑋 } ) ∈ Fin ↔ ∃ 𝑚 ∈ ω ( 𝐴 ∖ { 𝑋 } ) ≈ 𝑚 )
3 simp3 ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑚 ∈ ω ∧ ( 𝐴 ∖ { 𝑋 } ) ≈ 𝑚 ) → ( 𝐴 ∖ { 𝑋 } ) ≈ 𝑚 )
4 en2sn ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑚 ∈ ω ) → { 𝑋 } ≈ { 𝑚 } )
5 4 3adant3 ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑚 ∈ ω ∧ ( 𝐴 ∖ { 𝑋 } ) ≈ 𝑚 ) → { 𝑋 } ≈ { 𝑚 } )
6 incom ⊢ ( ( 𝐴 ∖ { 𝑋 } ) ∩ { 𝑋 } ) = ( { 𝑋 } ∩ ( 𝐴 ∖ { 𝑋 } ) )
7 disjdif ⊢ ( { 𝑋 } ∩ ( 𝐴 ∖ { 𝑋 } ) ) = ∅
8 6 7 eqtri ⊢ ( ( 𝐴 ∖ { 𝑋 } ) ∩ { 𝑋 } ) = ∅
9 8 a1i ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑚 ∈ ω ∧ ( 𝐴 ∖ { 𝑋 } ) ≈ 𝑚 ) → ( ( 𝐴 ∖ { 𝑋 } ) ∩ { 𝑋 } ) = ∅ )
10 nnord ⊢ ( 𝑚 ∈ ω → Ord 𝑚 )
11 ordirr ⊢ ( Ord 𝑚 → ¬ 𝑚 ∈ 𝑚 )
12 10 11 syl ⊢ ( 𝑚 ∈ ω → ¬ 𝑚 ∈ 𝑚 )
13 disjsn ⊢ ( ( 𝑚 ∩ { 𝑚 } ) = ∅ ↔ ¬ 𝑚 ∈ 𝑚 )
14 12 13 sylibr ⊢ ( 𝑚 ∈ ω → ( 𝑚 ∩ { 𝑚 } ) = ∅ )
15 14 3ad2ant2 ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑚 ∈ ω ∧ ( 𝐴 ∖ { 𝑋 } ) ≈ 𝑚 ) → ( 𝑚 ∩ { 𝑚 } ) = ∅ )
16 unen ⊢ ( ( ( ( 𝐴 ∖ { 𝑋 } ) ≈ 𝑚 ∧ { 𝑋 } ≈ { 𝑚 } ) ∧ ( ( ( 𝐴 ∖ { 𝑋 } ) ∩ { 𝑋 } ) = ∅ ∧ ( 𝑚 ∩ { 𝑚 } ) = ∅ ) ) → ( ( 𝐴 ∖ { 𝑋 } ) ∪ { 𝑋 } ) ≈ ( 𝑚 ∪ { 𝑚 } ) )
17 3 5 9 15 16 syl22anc ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑚 ∈ ω ∧ ( 𝐴 ∖ { 𝑋 } ) ≈ 𝑚 ) → ( ( 𝐴 ∖ { 𝑋 } ) ∪ { 𝑋 } ) ≈ ( 𝑚 ∪ { 𝑚 } ) )
18 difsnid ⊢ ( 𝑋 ∈ 𝐴 → ( ( 𝐴 ∖ { 𝑋 } ) ∪ { 𝑋 } ) = 𝐴 )
19 df-suc ⊢ suc 𝑚 = ( 𝑚 ∪ { 𝑚 } )
20 19 eqcomi ⊢ ( 𝑚 ∪ { 𝑚 } ) = suc 𝑚
21 20 a1i ⊢ ( 𝑋 ∈ 𝐴 → ( 𝑚 ∪ { 𝑚 } ) = suc 𝑚 )
22 18 21 breq12d ⊢ ( 𝑋 ∈ 𝐴 → ( ( ( 𝐴 ∖ { 𝑋 } ) ∪ { 𝑋 } ) ≈ ( 𝑚 ∪ { 𝑚 } ) ↔ 𝐴 ≈ suc 𝑚 ) )
23 22 3ad2ant1 ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑚 ∈ ω ∧ ( 𝐴 ∖ { 𝑋 } ) ≈ 𝑚 ) → ( ( ( 𝐴 ∖ { 𝑋 } ) ∪ { 𝑋 } ) ≈ ( 𝑚 ∪ { 𝑚 } ) ↔ 𝐴 ≈ suc 𝑚 ) )
24 17 23 mpbid ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑚 ∈ ω ∧ ( 𝐴 ∖ { 𝑋 } ) ≈ 𝑚 ) → 𝐴 ≈ suc 𝑚 )
25 peano2 ⊢ ( 𝑚 ∈ ω → suc 𝑚 ∈ ω )
26 25 3ad2ant2 ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑚 ∈ ω ∧ ( 𝐴 ∖ { 𝑋 } ) ≈ 𝑚 ) → suc 𝑚 ∈ ω )
27 cardennn ⊢ ( ( 𝐴 ≈ suc 𝑚 ∧ suc 𝑚 ∈ ω ) → ( card ‘ 𝐴 ) = suc 𝑚 )
28 24 26 27 syl2anc ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑚 ∈ ω ∧ ( 𝐴 ∖ { 𝑋 } ) ≈ 𝑚 ) → ( card ‘ 𝐴 ) = suc 𝑚 )
29 cardennn ⊢ ( ( ( 𝐴 ∖ { 𝑋 } ) ≈ 𝑚 ∧ 𝑚 ∈ ω ) → ( card ‘ ( 𝐴 ∖ { 𝑋 } ) ) = 𝑚 )
30 29 ancoms ⊢ ( ( 𝑚 ∈ ω ∧ ( 𝐴 ∖ { 𝑋 } ) ≈ 𝑚 ) → ( card ‘ ( 𝐴 ∖ { 𝑋 } ) ) = 𝑚 )
31 30 3adant1 ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑚 ∈ ω ∧ ( 𝐴 ∖ { 𝑋 } ) ≈ 𝑚 ) → ( card ‘ ( 𝐴 ∖ { 𝑋 } ) ) = 𝑚 )
32 suceq ⊢ ( ( card ‘ ( 𝐴 ∖ { 𝑋 } ) ) = 𝑚 → suc ( card ‘ ( 𝐴 ∖ { 𝑋 } ) ) = suc 𝑚 )
33 31 32 syl ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑚 ∈ ω ∧ ( 𝐴 ∖ { 𝑋 } ) ≈ 𝑚 ) → suc ( card ‘ ( 𝐴 ∖ { 𝑋 } ) ) = suc 𝑚 )
34 28 33 eqtr4d ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑚 ∈ ω ∧ ( 𝐴 ∖ { 𝑋 } ) ≈ 𝑚 ) → ( card ‘ 𝐴 ) = suc ( card ‘ ( 𝐴 ∖ { 𝑋 } ) ) )
35 34 3expib ⊢ ( 𝑋 ∈ 𝐴 → ( ( 𝑚 ∈ ω ∧ ( 𝐴 ∖ { 𝑋 } ) ≈ 𝑚 ) → ( card ‘ 𝐴 ) = suc ( card ‘ ( 𝐴 ∖ { 𝑋 } ) ) ) )
36 35 com12 ⊢ ( ( 𝑚 ∈ ω ∧ ( 𝐴 ∖ { 𝑋 } ) ≈ 𝑚 ) → ( 𝑋 ∈ 𝐴 → ( card ‘ 𝐴 ) = suc ( card ‘ ( 𝐴 ∖ { 𝑋 } ) ) ) )
37 36 rexlimiva ⊢ ( ∃ 𝑚 ∈ ω ( 𝐴 ∖ { 𝑋 } ) ≈ 𝑚 → ( 𝑋 ∈ 𝐴 → ( card ‘ 𝐴 ) = suc ( card ‘ ( 𝐴 ∖ { 𝑋 } ) ) ) )
38 2 37 sylbi ⊢ ( ( 𝐴 ∖ { 𝑋 } ) ∈ Fin → ( 𝑋 ∈ 𝐴 → ( card ‘ 𝐴 ) = suc ( card ‘ ( 𝐴 ∖ { 𝑋 } ) ) ) )
39 1 38 syl ⊢ ( 𝐴 ∈ Fin → ( 𝑋 ∈ 𝐴 → ( card ‘ 𝐴 ) = suc ( card ‘ ( 𝐴 ∖ { 𝑋 } ) ) ) )
40 39 imp ⊢ ( ( 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐴 ) → ( card ‘ 𝐴 ) = suc ( card ‘ ( 𝐴 ∖ { 𝑋 } ) ) )