difsnen

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

		Ref	Expression
	Assertion	difsnen	$⊢ (X \in V \land A \in X \land B \in X) \to (X ∖ \{A\}) \approx (X ∖ \{B\})$

Proof

Step	Hyp	Ref	Expression
1		difexg	$⊢ X \in V \to X ∖ \{A\} \in V$
2		enrefg	$⊢ X ∖ \{A\} \in V \to (X ∖ \{A\}) \approx (X ∖ \{A\})$
3	1 2	syl	$⊢ X \in V \to (X ∖ \{A\}) \approx (X ∖ \{A\})$
4	3	3ad2ant1	$⊢ (X \in V \land A \in X \land B \in X) \to (X ∖ \{A\}) \approx (X ∖ \{A\})$
5		sneq	$⊢ A = B \to \{A\} = \{B\}$
6	5	difeq2d	$⊢ A = B \to X ∖ \{A\} = X ∖ \{B\}$
7	6	breq2d	$⊢ A = B \to ((X ∖ \{A\}) \approx (X ∖ \{A\}) \leftrightarrow (X ∖ \{A\}) \approx (X ∖ \{B\}))$
8	4 7	syl5ibcom	$⊢ (X \in V \land A \in X \land B \in X) \to (A = B \to (X ∖ \{A\}) \approx (X ∖ \{B\}))$
9	8	imp	$⊢ ((X \in V \land A \in X \land B \in X) \land A = B) \to (X ∖ \{A\}) \approx (X ∖ \{B\})$
10		simpl1	$⊢ ((X \in V \land A \in X \land B \in X) \land A \neq B) \to X \in V$
11		difexg	$⊢ X ∖ \{A\} \in V \to (X ∖ \{A\}) ∖ \{B\} \in V$
12		enrefg	$⊢ (X ∖ \{A\}) ∖ \{B\} \in V \to ((X ∖ \{A\}) ∖ \{B\}) \approx ((X ∖ \{A\}) ∖ \{B\})$
13	10 1 11 12	4syl	$⊢ ((X \in V \land A \in X \land B \in X) \land A \neq B) \to ((X ∖ \{A\}) ∖ \{B\}) \approx ((X ∖ \{A\}) ∖ \{B\})$
14		dif32	$⊢ (X ∖ \{A\}) ∖ \{B\} = (X ∖ \{B\}) ∖ \{A\}$
15	13 14	breqtrdi	$⊢ ((X \in V \land A \in X \land B \in X) \land A \neq B) \to ((X ∖ \{A\}) ∖ \{B\}) \approx ((X ∖ \{B\}) ∖ \{A\})$
16		simpl3	$⊢ ((X \in V \land A \in X \land B \in X) \land A \neq B) \to B \in X$
17		simpl2	$⊢ ((X \in V \land A \in X \land B \in X) \land A \neq B) \to A \in X$
18		en2sn	$⊢ (B \in X \land A \in X) \to \{B\} \approx \{A\}$
19	16 17 18	syl2anc	$⊢ ((X \in V \land A \in X \land B \in X) \land A \neq B) \to \{B\} \approx \{A\}$
20		incom	$⊢ ((X ∖ \{A\}) ∖ \{B\}) \cap \{B\} = \{B\} \cap ((X ∖ \{A\}) ∖ \{B\})$
21		disjdif	$⊢ \{B\} \cap ((X ∖ \{A\}) ∖ \{B\}) = \emptyset$
22	20 21	eqtri	$⊢ ((X ∖ \{A\}) ∖ \{B\}) \cap \{B\} = \emptyset$
23	22	a1i	$⊢ ((X \in V \land A \in X \land B \in X) \land A \neq B) \to ((X ∖ \{A\}) ∖ \{B\}) \cap \{B\} = \emptyset$
24		incom	$⊢ ((X ∖ \{B\}) ∖ \{A\}) \cap \{A\} = \{A\} \cap ((X ∖ \{B\}) ∖ \{A\})$
25		disjdif	$⊢ \{A\} \cap ((X ∖ \{B\}) ∖ \{A\}) = \emptyset$
26	24 25	eqtri	$⊢ ((X ∖ \{B\}) ∖ \{A\}) \cap \{A\} = \emptyset$
27	26	a1i	$⊢ ((X \in V \land A \in X \land B \in X) \land A \neq B) \to ((X ∖ \{B\}) ∖ \{A\}) \cap \{A\} = \emptyset$
28		unen	$⊢ ((((X ∖ \{A\}) ∖ \{B\}) \approx ((X ∖ \{B\}) ∖ \{A\}) \land \{B\} \approx \{A\}) \land (((X ∖ \{A\}) ∖ \{B\}) \cap \{B\} = \emptyset \land ((X ∖ \{B\}) ∖ \{A\}) \cap \{A\} = \emptyset)) \to (((X ∖ \{A\}) ∖ \{B\}) \cup \{B\}) \approx (((X ∖ \{B\}) ∖ \{A\}) \cup \{A\})$
29	15 19 23 27 28	syl22anc	$⊢ ((X \in V \land A \in X \land B \in X) \land A \neq B) \to (((X ∖ \{A\}) ∖ \{B\}) \cup \{B\}) \approx (((X ∖ \{B\}) ∖ \{A\}) \cup \{A\})$
30		simpr	$⊢ ((X \in V \land A \in X \land B \in X) \land A \neq B) \to A \neq B$
31	30	necomd	$⊢ ((X \in V \land A \in X \land B \in X) \land A \neq B) \to B \neq A$
32		eldifsn	$⊢ B \in (X ∖ \{A\}) \leftrightarrow (B \in X \land B \neq A)$
33	16 31 32	sylanbrc	$⊢ ((X \in V \land A \in X \land B \in X) \land A \neq B) \to B \in (X ∖ \{A\})$
34		difsnid	$⊢ B \in (X ∖ \{A\}) \to ((X ∖ \{A\}) ∖ \{B\}) \cup \{B\} = X ∖ \{A\}$
35	33 34	syl	$⊢ ((X \in V \land A \in X \land B \in X) \land A \neq B) \to ((X ∖ \{A\}) ∖ \{B\}) \cup \{B\} = X ∖ \{A\}$
36		eldifsn	$⊢ A \in (X ∖ \{B\}) \leftrightarrow (A \in X \land A \neq B)$
37	17 30 36	sylanbrc	$⊢ ((X \in V \land A \in X \land B \in X) \land A \neq B) \to A \in (X ∖ \{B\})$
38		difsnid	$⊢ A \in (X ∖ \{B\}) \to ((X ∖ \{B\}) ∖ \{A\}) \cup \{A\} = X ∖ \{B\}$
39	37 38	syl	$⊢ ((X \in V \land A \in X \land B \in X) \land A \neq B) \to ((X ∖ \{B\}) ∖ \{A\}) \cup \{A\} = X ∖ \{B\}$
40	29 35 39	3brtr3d	$⊢ ((X \in V \land A \in X \land B \in X) \land A \neq B) \to (X ∖ \{A\}) \approx (X ∖ \{B\})$
41	9 40	pm2.61dane	$⊢ (X \in V \land A \in X \land B \in X) \to (X ∖ \{A\}) \approx (X ∖ \{B\})$

Metamath Proof Explorer

Theorem difsnen

Proof