This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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