Metamath Proof Explorer

Theorem dif1en

Description: If a set A is equinumerous to the successor of a natural number M , then A with an element removed is equinumerous to M . (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Stefan O'Rear, 16-Aug-2015)

Ref Expression
Assertion dif1en ( ( 𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀 ∧ 𝑋 ∈ 𝐴 ) → ( 𝐴 ∖ { 𝑋 } ) ≈ 𝑀 )

Proof

Step Hyp Ref Expression
1 peano2 ⊢ ( 𝑀 ∈ ω → suc 𝑀 ∈ ω )
2 breq2 ⊢ ( 𝑥 = suc 𝑀 → ( 𝐴 ≈ 𝑥 ↔ 𝐴 ≈ suc 𝑀 ) )
3 2 rspcev ⊢ ( ( suc 𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀 ) → ∃ 𝑥 ∈ ω 𝐴 ≈ 𝑥 )
4 isfi ⊢ ( 𝐴 ∈ Fin ↔ ∃ 𝑥 ∈ ω 𝐴 ≈ 𝑥 )
5 3 4 sylibr ⊢ ( ( suc 𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀 ) → 𝐴 ∈ Fin )
6 1 5 sylan ⊢ ( ( 𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀 ) → 𝐴 ∈ Fin )
7 diffi ⊢ ( 𝐴 ∈ Fin → ( 𝐴 ∖ { 𝑋 } ) ∈ Fin )
8 isfi ⊢ ( ( 𝐴 ∖ { 𝑋 } ) ∈ Fin ↔ ∃ 𝑥 ∈ ω ( 𝐴 ∖ { 𝑋 } ) ≈ 𝑥 )
9 7 8 sylib ⊢ ( 𝐴 ∈ Fin → ∃ 𝑥 ∈ ω ( 𝐴 ∖ { 𝑋 } ) ≈ 𝑥 )
10 6 9 syl ⊢ ( ( 𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀 ) → ∃ 𝑥 ∈ ω ( 𝐴 ∖ { 𝑋 } ) ≈ 𝑥 )
11 10 3adant3 ⊢ ( ( 𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀 ∧ 𝑋 ∈ 𝐴 ) → ∃ 𝑥 ∈ ω ( 𝐴 ∖ { 𝑋 } ) ≈ 𝑥 )
12 en2sn ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑥 ∈ V ) → { 𝑋 } ≈ { 𝑥 } )
13 12 elvd ⊢ ( 𝑋 ∈ 𝐴 → { 𝑋 } ≈ { 𝑥 } )
14 nnord ⊢ ( 𝑥 ∈ ω → Ord 𝑥 )
15 orddisj ⊢ ( Ord 𝑥 → ( 𝑥 ∩ { 𝑥 } ) = ∅ )
16 14 15 syl ⊢ ( 𝑥 ∈ ω → ( 𝑥 ∩ { 𝑥 } ) = ∅ )
17 incom ⊢ ( ( 𝐴 ∖ { 𝑋 } ) ∩ { 𝑋 } ) = ( { 𝑋 } ∩ ( 𝐴 ∖ { 𝑋 } ) )
18 disjdif ⊢ ( { 𝑋 } ∩ ( 𝐴 ∖ { 𝑋 } ) ) = ∅
19 17 18 eqtri ⊢ ( ( 𝐴 ∖ { 𝑋 } ) ∩ { 𝑋 } ) = ∅
20 unen ⊢ ( ( ( ( 𝐴 ∖ { 𝑋 } ) ≈ 𝑥 ∧ { 𝑋 } ≈ { 𝑥 } ) ∧ ( ( ( 𝐴 ∖ { 𝑋 } ) ∩ { 𝑋 } ) = ∅ ∧ ( 𝑥 ∩ { 𝑥 } ) = ∅ ) ) → ( ( 𝐴 ∖ { 𝑋 } ) ∪ { 𝑋 } ) ≈ ( 𝑥 ∪ { 𝑥 } ) )
21 20 an4s ⊢ ( ( ( ( 𝐴 ∖ { 𝑋 } ) ≈ 𝑥 ∧ ( ( 𝐴 ∖ { 𝑋 } ) ∩ { 𝑋 } ) = ∅ ) ∧ ( { 𝑋 } ≈ { 𝑥 } ∧ ( 𝑥 ∩ { 𝑥 } ) = ∅ ) ) → ( ( 𝐴 ∖ { 𝑋 } ) ∪ { 𝑋 } ) ≈ ( 𝑥 ∪ { 𝑥 } ) )
22 19 21 mpanl2 ⊢ ( ( ( 𝐴 ∖ { 𝑋 } ) ≈ 𝑥 ∧ ( { 𝑋 } ≈ { 𝑥 } ∧ ( 𝑥 ∩ { 𝑥 } ) = ∅ ) ) → ( ( 𝐴 ∖ { 𝑋 } ) ∪ { 𝑋 } ) ≈ ( 𝑥 ∪ { 𝑥 } ) )
23 22 expcom ⊢ ( ( { 𝑋 } ≈ { 𝑥 } ∧ ( 𝑥 ∩ { 𝑥 } ) = ∅ ) → ( ( 𝐴 ∖ { 𝑋 } ) ≈ 𝑥 → ( ( 𝐴 ∖ { 𝑋 } ) ∪ { 𝑋 } ) ≈ ( 𝑥 ∪ { 𝑥 } ) ) )
24 13 16 23 syl2an ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑥 ∈ ω ) → ( ( 𝐴 ∖ { 𝑋 } ) ≈ 𝑥 → ( ( 𝐴 ∖ { 𝑋 } ) ∪ { 𝑋 } ) ≈ ( 𝑥 ∪ { 𝑥 } ) ) )
25 24 3ad2antl3 ⊢ ( ( ( 𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑥 ∈ ω ) → ( ( 𝐴 ∖ { 𝑋 } ) ≈ 𝑥 → ( ( 𝐴 ∖ { 𝑋 } ) ∪ { 𝑋 } ) ≈ ( 𝑥 ∪ { 𝑥 } ) ) )
26 difsnid ⊢ ( 𝑋 ∈ 𝐴 → ( ( 𝐴 ∖ { 𝑋 } ) ∪ { 𝑋 } ) = 𝐴 )
27 df-suc ⊢ suc 𝑥 = ( 𝑥 ∪ { 𝑥 } )
28 27 eqcomi ⊢ ( 𝑥 ∪ { 𝑥 } ) = suc 𝑥
29 28 a1i ⊢ ( 𝑋 ∈ 𝐴 → ( 𝑥 ∪ { 𝑥 } ) = suc 𝑥 )
30 26 29 breq12d ⊢ ( 𝑋 ∈ 𝐴 → ( ( ( 𝐴 ∖ { 𝑋 } ) ∪ { 𝑋 } ) ≈ ( 𝑥 ∪ { 𝑥 } ) ↔ 𝐴 ≈ suc 𝑥 ) )
31 30 3ad2ant3 ⊢ ( ( 𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀 ∧ 𝑋 ∈ 𝐴 ) → ( ( ( 𝐴 ∖ { 𝑋 } ) ∪ { 𝑋 } ) ≈ ( 𝑥 ∪ { 𝑥 } ) ↔ 𝐴 ≈ suc 𝑥 ) )
32 31 adantr ⊢ ( ( ( 𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑥 ∈ ω ) → ( ( ( 𝐴 ∖ { 𝑋 } ) ∪ { 𝑋 } ) ≈ ( 𝑥 ∪ { 𝑥 } ) ↔ 𝐴 ≈ suc 𝑥 ) )
33 ensym ⊢ ( 𝐴 ≈ suc 𝑀 → suc 𝑀 ≈ 𝐴 )
34 entr ⊢ ( ( suc 𝑀 ≈ 𝐴 ∧ 𝐴 ≈ suc 𝑥 ) → suc 𝑀 ≈ suc 𝑥 )
35 peano2 ⊢ ( 𝑥 ∈ ω → suc 𝑥 ∈ ω )
36 nneneq ⊢ ( ( suc 𝑀 ∈ ω ∧ suc 𝑥 ∈ ω ) → ( suc 𝑀 ≈ suc 𝑥 ↔ suc 𝑀 = suc 𝑥 ) )
37 35 36 sylan2 ⊢ ( ( suc 𝑀 ∈ ω ∧ 𝑥 ∈ ω ) → ( suc 𝑀 ≈ suc 𝑥 ↔ suc 𝑀 = suc 𝑥 ) )
38 34 37 syl5ib ⊢ ( ( suc 𝑀 ∈ ω ∧ 𝑥 ∈ ω ) → ( ( suc 𝑀 ≈ 𝐴 ∧ 𝐴 ≈ suc 𝑥 ) → suc 𝑀 = suc 𝑥 ) )
39 38 expd ⊢ ( ( suc 𝑀 ∈ ω ∧ 𝑥 ∈ ω ) → ( suc 𝑀 ≈ 𝐴 → ( 𝐴 ≈ suc 𝑥 → suc 𝑀 = suc 𝑥 ) ) )
40 33 39 syl5 ⊢ ( ( suc 𝑀 ∈ ω ∧ 𝑥 ∈ ω ) → ( 𝐴 ≈ suc 𝑀 → ( 𝐴 ≈ suc 𝑥 → suc 𝑀 = suc 𝑥 ) ) )
41 1 40 sylan ⊢ ( ( 𝑀 ∈ ω ∧ 𝑥 ∈ ω ) → ( 𝐴 ≈ suc 𝑀 → ( 𝐴 ≈ suc 𝑥 → suc 𝑀 = suc 𝑥 ) ) )
42 41 imp ⊢ ( ( ( 𝑀 ∈ ω ∧ 𝑥 ∈ ω ) ∧ 𝐴 ≈ suc 𝑀 ) → ( 𝐴 ≈ suc 𝑥 → suc 𝑀 = suc 𝑥 ) )
43 42 an32s ⊢ ( ( ( 𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀 ) ∧ 𝑥 ∈ ω ) → ( 𝐴 ≈ suc 𝑥 → suc 𝑀 = suc 𝑥 ) )
44 43 3adantl3 ⊢ ( ( ( 𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑥 ∈ ω ) → ( 𝐴 ≈ suc 𝑥 → suc 𝑀 = suc 𝑥 ) )
45 32 44 sylbid ⊢ ( ( ( 𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑥 ∈ ω ) → ( ( ( 𝐴 ∖ { 𝑋 } ) ∪ { 𝑋 } ) ≈ ( 𝑥 ∪ { 𝑥 } ) → suc 𝑀 = suc 𝑥 ) )
46 peano4 ⊢ ( ( 𝑀 ∈ ω ∧ 𝑥 ∈ ω ) → ( suc 𝑀 = suc 𝑥 ↔ 𝑀 = 𝑥 ) )
47 46 biimpd ⊢ ( ( 𝑀 ∈ ω ∧ 𝑥 ∈ ω ) → ( suc 𝑀 = suc 𝑥 → 𝑀 = 𝑥 ) )
48 47 3ad2antl1 ⊢ ( ( ( 𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑥 ∈ ω ) → ( suc 𝑀 = suc 𝑥 → 𝑀 = 𝑥 ) )
49 25 45 48 3syld ⊢ ( ( ( 𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑥 ∈ ω ) → ( ( 𝐴 ∖ { 𝑋 } ) ≈ 𝑥 → 𝑀 = 𝑥 ) )
50 breq2 ⊢ ( 𝑀 = 𝑥 → ( ( 𝐴 ∖ { 𝑋 } ) ≈ 𝑀 ↔ ( 𝐴 ∖ { 𝑋 } ) ≈ 𝑥 ) )
51 50 biimprcd ⊢ ( ( 𝐴 ∖ { 𝑋 } ) ≈ 𝑥 → ( 𝑀 = 𝑥 → ( 𝐴 ∖ { 𝑋 } ) ≈ 𝑀 ) )
52 49 51 sylcom ⊢ ( ( ( 𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑥 ∈ ω ) → ( ( 𝐴 ∖ { 𝑋 } ) ≈ 𝑥 → ( 𝐴 ∖ { 𝑋 } ) ≈ 𝑀 ) )
53 52 rexlimdva ⊢ ( ( 𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀 ∧ 𝑋 ∈ 𝐴 ) → ( ∃ 𝑥 ∈ ω ( 𝐴 ∖ { 𝑋 } ) ≈ 𝑥 → ( 𝐴 ∖ { 𝑋 } ) ≈ 𝑀 ) )
54 11 53 mpd ⊢ ( ( 𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀 ∧ 𝑋 ∈ 𝐴 ) → ( 𝐴 ∖ { 𝑋 } ) ≈ 𝑀 )