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 . For a proof with fewer symbols using ax-pow , see dif1enALT . (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Stefan O'Rear, 16-Aug-2015) Avoid ax-pow . (Revised by BTernaryTau, 26-Aug-2024)

		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		bren	$⊢ A \approx suc M \leftrightarrow \exists f f : A \underset{1-1 onto}{⟶} suc M$
2		19.41v	$⊢ \exists f (f : A \underset{1-1 onto}{⟶} suc M \land (X \in A \land M \in ω)) \leftrightarrow (\exists f f : A \underset{1-1 onto}{⟶} suc M \land (X \in A \land M \in ω))$
3		3anass	$⊢ (f : A \underset{1-1 onto}{⟶} suc M \land X \in A \land M \in ω) \leftrightarrow (f : A \underset{1-1 onto}{⟶} suc M \land (X \in A \land M \in ω))$
4	3	exbii	$⊢ \exists f (f : A \underset{1-1 onto}{⟶} suc M \land X \in A \land M \in ω) \leftrightarrow \exists f (f : A \underset{1-1 onto}{⟶} suc M \land (X \in A \land M \in ω))$
5		3anass	$⊢ (\exists f f : A \underset{1-1 onto}{⟶} suc M \land X \in A \land M \in ω) \leftrightarrow (\exists f f : A \underset{1-1 onto}{⟶} suc M \land (X \in A \land M \in ω))$
6	2 4 5	3bitr4i	$⊢ \exists f (f : A \underset{1-1 onto}{⟶} suc M \land X \in A \land M \in ω) \leftrightarrow (\exists f f : A \underset{1-1 onto}{⟶} suc M \land X \in A \land M \in ω)$
7		sucidg	$⊢ M \in ω \to M \in suc M$
8		f1ocnvdm	$⊢ (f : A \underset{1-1 onto}{⟶} suc M \land M \in suc M) \to f^{-1} (M) \in A$
9	8	3adant2	$⊢ (f : A \underset{1-1 onto}{⟶} suc M \land X \in A \land M \in suc M) \to f^{-1} (M) \in A$
10		f1ofvswap	$⊢ (f : A \underset{1-1 onto}{⟶} suc M \land X \in A \land f^{-1} (M) \in A) \to (({f ↾}_{(A ∖ \{X, f^{-1} (M)\})}) \cup \{⟨X, f (f^{-1} (M))⟩, ⟨f^{-1} (M), f (X)⟩\}) : A \underset{1-1 onto}{⟶} suc M$
11	9 10	syld3an3	$⊢ (f : A \underset{1-1 onto}{⟶} suc M \land X \in A \land M \in suc M) \to (({f ↾}_{(A ∖ \{X, f^{-1} (M)\})}) \cup \{⟨X, f (f^{-1} (M))⟩, ⟨f^{-1} (M), f (X)⟩\}) : A \underset{1-1 onto}{⟶} suc M$
12		f1ocnvfv2	$⊢ (f : A \underset{1-1 onto}{⟶} suc M \land M \in suc M) \to f (f^{-1} (M)) = M$
13	12	opeq2d	$⊢ (f : A \underset{1-1 onto}{⟶} suc M \land M \in suc M) \to ⟨X, f (f^{-1} (M))⟩ = ⟨X, M⟩$
14	13	preq1d	$⊢ (f : A \underset{1-1 onto}{⟶} suc M \land M \in suc M) \to \{⟨X, f (f^{-1} (M))⟩, ⟨f^{-1} (M), f (X)⟩\} = \{⟨X, M⟩, ⟨f^{-1} (M), f (X)⟩\}$
15	14	uneq2d	$⊢ (f : A \underset{1-1 onto}{⟶} suc M \land M \in suc M) \to ({f ↾}_{(A ∖ \{X, f^{-1} (M)\})}) \cup \{⟨X, f (f^{-1} (M))⟩, ⟨f^{-1} (M), f (X)⟩\} = ({f ↾}_{(A ∖ \{X, f^{-1} (M)\})}) \cup \{⟨X, M⟩, ⟨f^{-1} (M), f (X)⟩\}$
16	15	f1oeq1d	$⊢ (f : A \underset{1-1 onto}{⟶} suc M \land M \in suc M) \to ((({f ↾}_{(A ∖ \{X, f^{-1} (M)\})}) \cup \{⟨X, f (f^{-1} (M))⟩, ⟨f^{-1} (M), f (X)⟩\}) : A \underset{1-1 onto}{⟶} suc M \leftrightarrow (({f ↾}_{(A ∖ \{X, f^{-1} (M)\})}) \cup \{⟨X, M⟩, ⟨f^{-1} (M), f (X)⟩\}) : A \underset{1-1 onto}{⟶} suc M)$
17	16	3adant2	$⊢ (f : A \underset{1-1 onto}{⟶} suc M \land X \in A \land M \in suc M) \to ((({f ↾}_{(A ∖ \{X, f^{-1} (M)\})}) \cup \{⟨X, f (f^{-1} (M))⟩, ⟨f^{-1} (M), f (X)⟩\}) : A \underset{1-1 onto}{⟶} suc M \leftrightarrow (({f ↾}_{(A ∖ \{X, f^{-1} (M)\})}) \cup \{⟨X, M⟩, ⟨f^{-1} (M), f (X)⟩\}) : A \underset{1-1 onto}{⟶} suc M)$
18	11 17	mpbid	$⊢ (f : A \underset{1-1 onto}{⟶} suc M \land X \in A \land M \in suc M) \to (({f ↾}_{(A ∖ \{X, f^{-1} (M)\})}) \cup \{⟨X, M⟩, ⟨f^{-1} (M), f (X)⟩\}) : A \underset{1-1 onto}{⟶} suc M$
19		f1ofun	$⊢ (({f ↾}_{(A ∖ \{X, f^{-1} (M)\})}) \cup \{⟨X, M⟩, ⟨f^{-1} (M), f (X)⟩\}) : A \underset{1-1 onto}{⟶} suc M \to Fun (({f ↾}_{(A ∖ \{X, f^{-1} (M)\})}) \cup \{⟨X, M⟩, ⟨f^{-1} (M), f (X)⟩\})$
20		opex	$⊢ ⟨X, M⟩ \in V$
21	20	prid1	$⊢ ⟨X, M⟩ \in \{⟨X, M⟩, ⟨f^{-1} (M), f (X)⟩\}$
22		elun2	$⊢ ⟨X, M⟩ \in \{⟨X, M⟩, ⟨f^{-1} (M), f (X)⟩\} \to ⟨X, M⟩ \in (({f ↾}_{(A ∖ \{X, f^{-1} (M)\})}) \cup \{⟨X, M⟩, ⟨f^{-1} (M), f (X)⟩\})$
23	21 22	ax-mp	$⊢ ⟨X, M⟩ \in (({f ↾}_{(A ∖ \{X, f^{-1} (M)\})}) \cup \{⟨X, M⟩, ⟨f^{-1} (M), f (X)⟩\})$
24		funopfv	$⊢ Fun (({f ↾}_{(A ∖ \{X, f^{-1} (M)\})}) \cup \{⟨X, M⟩, ⟨f^{-1} (M), f (X)⟩\}) \to (⟨X, M⟩ \in (({f ↾}_{(A ∖ \{X, f^{-1} (M)\})}) \cup \{⟨X, M⟩, ⟨f^{-1} (M), f (X)⟩\}) \to (({f ↾}_{(A ∖ \{X, f^{-1} (M)\})}) \cup \{⟨X, M⟩, ⟨f^{-1} (M), f (X)⟩\}) (X) = M)$
25	23 24	mpi	$⊢ Fun (({f ↾}_{(A ∖ \{X, f^{-1} (M)\})}) \cup \{⟨X, M⟩, ⟨f^{-1} (M), f (X)⟩\}) \to (({f ↾}_{(A ∖ \{X, f^{-1} (M)\})}) \cup \{⟨X, M⟩, ⟨f^{-1} (M), f (X)⟩\}) (X) = M$
26	18 19 25	3syl	$⊢ (f : A \underset{1-1 onto}{⟶} suc M \land X \in A \land M \in suc M) \to (({f ↾}_{(A ∖ \{X, f^{-1} (M)\})}) \cup \{⟨X, M⟩, ⟨f^{-1} (M), f (X)⟩\}) (X) = M$
27		simp2	$⊢ (f : A \underset{1-1 onto}{⟶} suc M \land X \in A \land M \in suc M) \to X \in A$
28		f1ocnvfv	$⊢ ((({f ↾}_{(A ∖ \{X, f^{-1} (M)\})}) \cup \{⟨X, M⟩, ⟨f^{-1} (M), f (X)⟩\}) : A \underset{1-1 onto}{⟶} suc M \land X \in A) \to ((({f ↾}_{(A ∖ \{X, f^{-1} (M)\})}) \cup \{⟨X, M⟩, ⟨f^{-1} (M), f (X)⟩\}) (X) = M \to {(({f ↾}_{(A ∖ \{X, f^{-1} (M)\})}) \cup \{⟨X, M⟩, ⟨f^{-1} (M), f (X)⟩\})}^{-1} (M) = X)$
29	18 27 28	syl2anc	$⊢ (f : A \underset{1-1 onto}{⟶} suc M \land X \in A \land M \in suc M) \to ((({f ↾}_{(A ∖ \{X, f^{-1} (M)\})}) \cup \{⟨X, M⟩, ⟨f^{-1} (M), f (X)⟩\}) (X) = M \to {(({f ↾}_{(A ∖ \{X, f^{-1} (M)\})}) \cup \{⟨X, M⟩, ⟨f^{-1} (M), f (X)⟩\})}^{-1} (M) = X)$
30	26 29	mpd	$⊢ (f : A \underset{1-1 onto}{⟶} suc M \land X \in A \land M \in suc M) \to {(({f ↾}_{(A ∖ \{X, f^{-1} (M)\})}) \cup \{⟨X, M⟩, ⟨f^{-1} (M), f (X)⟩\})}^{-1} (M) = X$
31	7 30	syl3an3	$⊢ (f : A \underset{1-1 onto}{⟶} suc M \land X \in A \land M \in ω) \to {(({f ↾}_{(A ∖ \{X, f^{-1} (M)\})}) \cup \{⟨X, M⟩, ⟨f^{-1} (M), f (X)⟩\})}^{-1} (M) = X$
32	31	sneqd	$⊢ (f : A \underset{1-1 onto}{⟶} suc M \land X \in A \land M \in ω) \to \{{(({f ↾}_{(A ∖ \{X, f^{-1} (M)\})}) \cup \{⟨X, M⟩, ⟨f^{-1} (M), f (X)⟩\})}^{-1} (M)\} = \{X\}$
33	32	difeq2d	$⊢ (f : A \underset{1-1 onto}{⟶} suc M \land X \in A \land M \in ω) \to A ∖ \{{(({f ↾}_{(A ∖ \{X, f^{-1} (M)\})}) \cup \{⟨X, M⟩, ⟨f^{-1} (M), f (X)⟩\})}^{-1} (M)\} = A ∖ \{X\}$
34		vex	$⊢ f \in V$
35	34	resex	$⊢ {f ↾}_{(A ∖ \{X, f^{-1} (M)\})} \in V$
36		prex	$⊢ \{⟨X, M⟩, ⟨f^{-1} (M), f (X)⟩\} \in V$
37	35 36	unex	$⊢ ({f ↾}_{(A ∖ \{X, f^{-1} (M)\})}) \cup \{⟨X, M⟩, ⟨f^{-1} (M), f (X)⟩\} \in V$
38		simp3	$⊢ (f : A \underset{1-1 onto}{⟶} suc M \land X \in A \land M \in ω) \to M \in ω$
39	7 18	syl3an3	$⊢ (f : A \underset{1-1 onto}{⟶} suc M \land X \in A \land M \in ω) \to (({f ↾}_{(A ∖ \{X, f^{-1} (M)\})}) \cup \{⟨X, M⟩, ⟨f^{-1} (M), f (X)⟩\}) : A \underset{1-1 onto}{⟶} suc M$
40		dif1enlem	$⊢ (({f ↾}_{(A ∖ \{X, f^{-1} (M)\})}) \cup \{⟨X, M⟩, ⟨f^{-1} (M), f (X)⟩\} \in V \land M \in ω \land (({f ↾}_{(A ∖ \{X, f^{-1} (M)\})}) \cup \{⟨X, M⟩, ⟨f^{-1} (M), f (X)⟩\}) : A \underset{1-1 onto}{⟶} suc M) \to (A ∖ \{{(({f ↾}_{(A ∖ \{X, f^{-1} (M)\})}) \cup \{⟨X, M⟩, ⟨f^{-1} (M), f (X)⟩\})}^{-1} (M)\}) \approx M$
41	37 38 39 40	mp3an2i	$⊢ (f : A \underset{1-1 onto}{⟶} suc M \land X \in A \land M \in ω) \to (A ∖ \{{(({f ↾}_{(A ∖ \{X, f^{-1} (M)\})}) \cup \{⟨X, M⟩, ⟨f^{-1} (M), f (X)⟩\})}^{-1} (M)\}) \approx M$
42	33 41	eqbrtrrd	$⊢ (f : A \underset{1-1 onto}{⟶} suc M \land X \in A \land M \in ω) \to (A ∖ \{X\}) \approx M$
43	42	exlimiv	$⊢ \exists f (f : A \underset{1-1 onto}{⟶} suc M \land X \in A \land M \in ω) \to (A ∖ \{X\}) \approx M$
44	6 43	sylbir	$⊢ (\exists f f : A \underset{1-1 onto}{⟶} suc M \land X \in A \land M \in ω) \to (A ∖ \{X\}) \approx M$
45	1 44	syl3an1b	$⊢ (A \approx suc M \land X \in A \land M \in ω) \to (A ∖ \{X\}) \approx M$
46	45	3comr	$⊢ (M \in ω \land A \approx suc M \land X \in A) \to (A ∖ \{X\}) \approx M$

Metamath Proof Explorer

Theorem dif1en

Proof