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		incom	⊢ ( ( ( 𝑋 ∖ { 𝐴 } ) ∖ { 𝐵 } ) ∩ { 𝐵 } ) = ( { 𝐵 } ∩ ( ( 𝑋 ∖ { 𝐴 } ) ∖ { 𝐵 } ) )
21		disjdif	⊢ ( { 𝐵 } ∩ ( ( 𝑋 ∖ { 𝐴 } ) ∖ { 𝐵 } ) ) = ∅
22	20 21	eqtri	⊢ ( ( ( 𝑋 ∖ { 𝐴 } ) ∖ { 𝐵 } ) ∩ { 𝐵 } ) = ∅
23	22	a1i	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝐴 ≠ 𝐵 ) → ( ( ( 𝑋 ∖ { 𝐴 } ) ∖ { 𝐵 } ) ∩ { 𝐵 } ) = ∅ )
24		incom	⊢ ( ( ( 𝑋 ∖ { 𝐵 } ) ∖ { 𝐴 } ) ∩ { 𝐴 } ) = ( { 𝐴 } ∩ ( ( 𝑋 ∖ { 𝐵 } ) ∖ { 𝐴 } ) )
25		disjdif	⊢ ( { 𝐴 } ∩ ( ( 𝑋 ∖ { 𝐵 } ) ∖ { 𝐴 } ) ) = ∅
26	24 25	eqtri	⊢ ( ( ( 𝑋 ∖ { 𝐵 } ) ∖ { 𝐴 } ) ∩ { 𝐴 } ) = ∅
27	26	a1i	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝐴 ≠ 𝐵 ) → ( ( ( 𝑋 ∖ { 𝐵 } ) ∖ { 𝐴 } ) ∩ { 𝐴 } ) = ∅ )
28		unen	⊢ ( ( ( ( ( 𝑋 ∖ { 𝐴 } ) ∖ { 𝐵 } ) ≈ ( ( 𝑋 ∖ { 𝐵 } ) ∖ { 𝐴 } ) ∧ { 𝐵 } ≈ { 𝐴 } ) ∧ ( ( ( ( 𝑋 ∖ { 𝐴 } ) ∖ { 𝐵 } ) ∩ { 𝐵 } ) = ∅ ∧ ( ( ( 𝑋 ∖ { 𝐵 } ) ∖ { 𝐴 } ) ∩ { 𝐴 } ) = ∅ ) ) → ( ( ( 𝑋 ∖ { 𝐴 } ) ∖ { 𝐵 } ) ∪ { 𝐵 } ) ≈ ( ( ( 𝑋 ∖ { 𝐵 } ) ∖ { 𝐴 } ) ∪ { 𝐴 } ) )
29	15 19 23 27 28	syl22anc	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝐴 ≠ 𝐵 ) → ( ( ( 𝑋 ∖ { 𝐴 } ) ∖ { 𝐵 } ) ∪ { 𝐵 } ) ≈ ( ( ( 𝑋 ∖ { 𝐵 } ) ∖ { 𝐴 } ) ∪ { 𝐴 } ) )
30		simpr	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝐴 ≠ 𝐵 ) → 𝐴 ≠ 𝐵 )
31	30	necomd	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝐴 ≠ 𝐵 ) → 𝐵 ≠ 𝐴 )
32		eldifsn	⊢ ( 𝐵 ∈ ( 𝑋 ∖ { 𝐴 } ) ↔ ( 𝐵 ∈ 𝑋 ∧ 𝐵 ≠ 𝐴 ) )
33	16 31 32	sylanbrc	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝐴 ≠ 𝐵 ) → 𝐵 ∈ ( 𝑋 ∖ { 𝐴 } ) )
34		difsnid	⊢ ( 𝐵 ∈ ( 𝑋 ∖ { 𝐴 } ) → ( ( ( 𝑋 ∖ { 𝐴 } ) ∖ { 𝐵 } ) ∪ { 𝐵 } ) = ( 𝑋 ∖ { 𝐴 } ) )
35	33 34	syl	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝐴 ≠ 𝐵 ) → ( ( ( 𝑋 ∖ { 𝐴 } ) ∖ { 𝐵 } ) ∪ { 𝐵 } ) = ( 𝑋 ∖ { 𝐴 } ) )
36		eldifsn	⊢ ( 𝐴 ∈ ( 𝑋 ∖ { 𝐵 } ) ↔ ( 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵 ) )
37	17 30 36	sylanbrc	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝐴 ≠ 𝐵 ) → 𝐴 ∈ ( 𝑋 ∖ { 𝐵 } ) )
38		difsnid	⊢ ( 𝐴 ∈ ( 𝑋 ∖ { 𝐵 } ) → ( ( ( 𝑋 ∖ { 𝐵 } ) ∖ { 𝐴 } ) ∪ { 𝐴 } ) = ( 𝑋 ∖ { 𝐵 } ) )
39	37 38	syl	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝐴 ≠ 𝐵 ) → ( ( ( 𝑋 ∖ { 𝐵 } ) ∖ { 𝐴 } ) ∪ { 𝐴 } ) = ( 𝑋 ∖ { 𝐵 } ) )
40	29 35 39	3brtr3d	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝐴 ≠ 𝐵 ) → ( 𝑋 ∖ { 𝐴 } ) ≈ ( 𝑋 ∖ { 𝐵 } ) )
41	9 40	pm2.61dane	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑋 ∖ { 𝐴 } ) ≈ ( 𝑋 ∖ { 𝐵 } ) )