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	$⊢ (M \in ω \land A \approx suc M \land X \in A) \to (A ∖ \{X\}) \approx M$

Proof

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

Metamath Proof Explorer

Theorem dif1en

Proof