Metamath Proof Explorer

Theorem difsnen

Description: All decrements of a set are equinumerous. (Contributed by Stefan O'Rear, 19-Feb-2015)

Ref Expression
Assertion difsnen ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑋 ∖ { 𝐴 } ) ≈ ( 𝑋 ∖ { 𝐵 } ) )

Proof

Step Hyp Ref Expression
1 difexg ⊢ ( 𝑋 ∈ 𝑉 → ( 𝑋 ∖ { 𝐴 } ) ∈ V )
2 enrefg ⊢ ( ( 𝑋 ∖ { 𝐴 } ) ∈ V → ( 𝑋 ∖ { 𝐴 } ) ≈ ( 𝑋 ∖ { 𝐴 } ) )
3 1 2 syl ⊢ ( 𝑋 ∈ 𝑉 → ( 𝑋 ∖ { 𝐴 } ) ≈ ( 𝑋 ∖ { 𝐴 } ) )
4 3 3ad2ant1 ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑋 ∖ { 𝐴 } ) ≈ ( 𝑋 ∖ { 𝐴 } ) )
5 sneq ⊢ ( 𝐴 = 𝐵 → { 𝐴 } = { 𝐵 } )
6 5 difeq2d ⊢ ( 𝐴 = 𝐵 → ( 𝑋 ∖ { 𝐴 } ) = ( 𝑋 ∖ { 𝐵 } ) )
7 6 breq2d ⊢ ( 𝐴 = 𝐵 → ( ( 𝑋 ∖ { 𝐴 } ) ≈ ( 𝑋 ∖ { 𝐴 } ) ↔ ( 𝑋 ∖ { 𝐴 } ) ≈ ( 𝑋 ∖ { 𝐵 } ) ) )
8 4 7 syl5ibcom ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 = 𝐵 → ( 𝑋 ∖ { 𝐴 } ) ≈ ( 𝑋 ∖ { 𝐵 } ) ) )
9 8 imp ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝐴 = 𝐵 ) → ( 𝑋 ∖ { 𝐴 } ) ≈ ( 𝑋 ∖ { 𝐵 } ) )
10 simpl1 ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝐴 ≠ 𝐵 ) → 𝑋 ∈ 𝑉 )
11 difexg ⊢ ( ( 𝑋 ∖ { 𝐴 } ) ∈ V → ( ( 𝑋 ∖ { 𝐴 } ) ∖ { 𝐵 } ) ∈ V )
12 enrefg ⊢ ( ( ( 𝑋 ∖ { 𝐴 } ) ∖ { 𝐵 } ) ∈ V → ( ( 𝑋 ∖ { 𝐴 } ) ∖ { 𝐵 } ) ≈ ( ( 𝑋 ∖ { 𝐴 } ) ∖ { 𝐵 } ) )
13 10 1 11 12 4syl ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝐴 ≠ 𝐵 ) → ( ( 𝑋 ∖ { 𝐴 } ) ∖ { 𝐵 } ) ≈ ( ( 𝑋 ∖ { 𝐴 } ) ∖ { 𝐵 } ) )
14 dif32 ⊢ ( ( 𝑋 ∖ { 𝐴 } ) ∖ { 𝐵 } ) = ( ( 𝑋 ∖ { 𝐵 } ) ∖ { 𝐴 } )
15 13 14 breqtrdi ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝐴 ≠ 𝐵 ) → ( ( 𝑋 ∖ { 𝐴 } ) ∖ { 𝐵 } ) ≈ ( ( 𝑋 ∖ { 𝐵 } ) ∖ { 𝐴 } ) )
16 simpl3 ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝐴 ≠ 𝐵 ) → 𝐵 ∈ 𝑋 )
17 simpl2 ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝐴 ≠ 𝐵 ) → 𝐴 ∈ 𝑋 )
18 en2sn ⊢ ( ( 𝐵 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → { 𝐵 } ≈ { 𝐴 } )
19 16 17 18 syl2anc ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝐴 ≠ 𝐵 ) → { 𝐵 } ≈ { 𝐴 } )
20 disjdifr ⊢ ( ( ( 𝑋 ∖ { 𝐴 } ) ∖ { 𝐵 } ) ∩ { 𝐵 } ) = ∅
21 20 a1i ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝐴 ≠ 𝐵 ) → ( ( ( 𝑋 ∖ { 𝐴 } ) ∖ { 𝐵 } ) ∩ { 𝐵 } ) = ∅ )
22 disjdifr ⊢ ( ( ( 𝑋 ∖ { 𝐵 } ) ∖ { 𝐴 } ) ∩ { 𝐴 } ) = ∅
23 22 a1i ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝐴 ≠ 𝐵 ) → ( ( ( 𝑋 ∖ { 𝐵 } ) ∖ { 𝐴 } ) ∩ { 𝐴 } ) = ∅ )
24 unen ⊢ ( ( ( ( ( 𝑋 ∖ { 𝐴 } ) ∖ { 𝐵 } ) ≈ ( ( 𝑋 ∖ { 𝐵 } ) ∖ { 𝐴 } ) ∧ { 𝐵 } ≈ { 𝐴 } ) ∧ ( ( ( ( 𝑋 ∖ { 𝐴 } ) ∖ { 𝐵 } ) ∩ { 𝐵 } ) = ∅ ∧ ( ( ( 𝑋 ∖ { 𝐵 } ) ∖ { 𝐴 } ) ∩ { 𝐴 } ) = ∅ ) ) → ( ( ( 𝑋 ∖ { 𝐴 } ) ∖ { 𝐵 } ) ∪ { 𝐵 } ) ≈ ( ( ( 𝑋 ∖ { 𝐵 } ) ∖ { 𝐴 } ) ∪ { 𝐴 } ) )
25 15 19 21 23 24 syl22anc ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝐴 ≠ 𝐵 ) → ( ( ( 𝑋 ∖ { 𝐴 } ) ∖ { 𝐵 } ) ∪ { 𝐵 } ) ≈ ( ( ( 𝑋 ∖ { 𝐵 } ) ∖ { 𝐴 } ) ∪ { 𝐴 } ) )
26 simpr ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝐴 ≠ 𝐵 ) → 𝐴 ≠ 𝐵 )
27 26 necomd ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝐴 ≠ 𝐵 ) → 𝐵 ≠ 𝐴 )
28 eldifsn ⊢ ( 𝐵 ∈ ( 𝑋 ∖ { 𝐴 } ) ↔ ( 𝐵 ∈ 𝑋 ∧ 𝐵 ≠ 𝐴 ) )
29 16 27 28 sylanbrc ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝐴 ≠ 𝐵 ) → 𝐵 ∈ ( 𝑋 ∖ { 𝐴 } ) )
30 difsnid ⊢ ( 𝐵 ∈ ( 𝑋 ∖ { 𝐴 } ) → ( ( ( 𝑋 ∖ { 𝐴 } ) ∖ { 𝐵 } ) ∪ { 𝐵 } ) = ( 𝑋 ∖ { 𝐴 } ) )
31 29 30 syl ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝐴 ≠ 𝐵 ) → ( ( ( 𝑋 ∖ { 𝐴 } ) ∖ { 𝐵 } ) ∪ { 𝐵 } ) = ( 𝑋 ∖ { 𝐴 } ) )
32 eldifsn ⊢ ( 𝐴 ∈ ( 𝑋 ∖ { 𝐵 } ) ↔ ( 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵 ) )
33 17 26 32 sylanbrc ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝐴 ≠ 𝐵 ) → 𝐴 ∈ ( 𝑋 ∖ { 𝐵 } ) )
34 difsnid ⊢ ( 𝐴 ∈ ( 𝑋 ∖ { 𝐵 } ) → ( ( ( 𝑋 ∖ { 𝐵 } ) ∖ { 𝐴 } ) ∪ { 𝐴 } ) = ( 𝑋 ∖ { 𝐵 } ) )
35 33 34 syl ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝐴 ≠ 𝐵 ) → ( ( ( 𝑋 ∖ { 𝐵 } ) ∖ { 𝐴 } ) ∪ { 𝐴 } ) = ( 𝑋 ∖ { 𝐵 } ) )
36 25 31 35 3brtr3d ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝐴 ≠ 𝐵 ) → ( 𝑋 ∖ { 𝐴 } ) ≈ ( 𝑋 ∖ { 𝐵 } ) )
37 9 36 pm2.61dane ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑋 ∖ { 𝐴 } ) ≈ ( 𝑋 ∖ { 𝐵 } ) )