dif1en

Description: If a set A is equinumerous to the successor of an ordinal 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) Avoid ax-pow . (Revised by BTernaryTau, 26-Aug-2024) Generalize to all ordinals. (Revised by BTernaryTau, 6-Jan-2025)

		Ref	Expression
	Assertion	dif1en	$⊢ (M \in On \land A \approx suc M \land X \in A) \to (A ∖ \{X\}) \approx M$

Proof

Step	Hyp	Ref	Expression
1		simp1	$⊢ (A \approx suc M \land X \in A \land M \in On) \to A \approx suc M$
2		encv	$⊢ A \approx suc M \to (A \in V \land suc M \in V)$
3	2	simpld	$⊢ A \approx suc M \to A \in V$
4	3	3anim1i	$⊢ (A \approx suc M \land X \in A \land M \in On) \to (A \in V \land X \in A \land M \in On)$
5		bren	$⊢ A \approx suc M \leftrightarrow \exists f f : A \underset{1-1 onto}{⟶} suc M$
6		sucidg	$⊢ M \in On \to M \in suc M$
7		f1ocnvdm	$⊢ (f : A \underset{1-1 onto}{⟶} suc M \land M \in suc M) \to f^{-1} (M) \in A$
8	7	3adant2	$⊢ (f : A \underset{1-1 onto}{⟶} suc M \land X \in A \land M \in suc M) \to f^{-1} (M) \in A$
9		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$
10	8 9	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$
11		f1ocnvfv2	$⊢ (f : A \underset{1-1 onto}{⟶} suc M \land M \in suc M) \to f (f^{-1} (M)) = M$
12	11	opeq2d	$⊢ (f : A \underset{1-1 onto}{⟶} suc M \land M \in suc M) \to ⟨X, f (f^{-1} (M))⟩ = ⟨X, M⟩$
13	12	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)⟩\}$
14	13	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)⟩\}$
15	14	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)$
16	15	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)$
17	10 16	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$
18	6 17	syl3an3	$⊢ (f : A \underset{1-1 onto}{⟶} suc M \land X \in A \land M \in On) \to (({f ↾}_{(A ∖ \{X, f^{-1} (M)\})}) \cup \{⟨X, M⟩, ⟨f^{-1} (M), f (X)⟩\}) : A \underset{1-1 onto}{⟶} suc M$
19	18	3adant3r1	$⊢ (f : A \underset{1-1 onto}{⟶} suc M \land (A \in V \land X \in A \land M \in On)) \to (({f ↾}_{(A ∖ \{X, f^{-1} (M)\})}) \cup \{⟨X, M⟩, ⟨f^{-1} (M), f (X)⟩\}) : A \underset{1-1 onto}{⟶} suc M$
20		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)⟩\})$
21		opex	$⊢ ⟨X, M⟩ \in V$
22	21	prid1	$⊢ ⟨X, M⟩ \in \{⟨X, M⟩, ⟨f^{-1} (M), f (X)⟩\}$
23		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)⟩\})$
24	22 23	ax-mp	$⊢ ⟨X, M⟩ \in (({f ↾}_{(A ∖ \{X, f^{-1} (M)\})}) \cup \{⟨X, M⟩, ⟨f^{-1} (M), f (X)⟩\})$
25		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)$
26	24 25	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$
27	19 20 26	3syl	$⊢ (f : A \underset{1-1 onto}{⟶} suc M \land (A \in V \land X \in A \land M \in On)) \to (({f ↾}_{(A ∖ \{X, f^{-1} (M)\})}) \cup \{⟨X, M⟩, ⟨f^{-1} (M), f (X)⟩\}) (X) = M$
28		simpr2	$⊢ (f : A \underset{1-1 onto}{⟶} suc M \land (A \in V \land X \in A \land M \in On)) \to X \in A$
29		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)$
30	19 28 29	syl2anc	$⊢ (f : A \underset{1-1 onto}{⟶} suc M \land (A \in V \land X \in A \land M \in On)) \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)$
31	27 30	mpd	$⊢ (f : A \underset{1-1 onto}{⟶} suc M \land (A \in V \land X \in A \land M \in On)) \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 (A \in V \land X \in A \land M \in On)) \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 (A \in V \land X \in A \land M \in On)) \to A ∖ \{{(({f ↾}_{(A ∖ \{X, f^{-1} (M)\})}) \cup \{⟨X, M⟩, ⟨f^{-1} (M), f (X)⟩\})}^{-1} (M)\} = A ∖ \{X\}$
34		simpr1	$⊢ (f : A \underset{1-1 onto}{⟶} suc M \land (A \in V \land X \in A \land M \in On)) \to A \in V$
35		3simpc	$⊢ (A \in V \land X \in A \land M \in On) \to (X \in A \land M \in On)$
36	35	anim2i	$⊢ (f : A \underset{1-1 onto}{⟶} suc M \land (A \in V \land X \in A \land M \in On)) \to (f : A \underset{1-1 onto}{⟶} suc M \land (X \in A \land M \in On))$
37		3anass	$⊢ (f : A \underset{1-1 onto}{⟶} suc M \land X \in A \land M \in On) \leftrightarrow (f : A \underset{1-1 onto}{⟶} suc M \land (X \in A \land M \in On))$
38	36 37	sylibr	$⊢ (f : A \underset{1-1 onto}{⟶} suc M \land (A \in V \land X \in A \land M \in On)) \to (f : A \underset{1-1 onto}{⟶} suc M \land X \in A \land M \in On)$
39	34 38	jca	$⊢ (f : A \underset{1-1 onto}{⟶} suc M \land (A \in V \land X \in A \land M \in On)) \to (A \in V \land (f : A \underset{1-1 onto}{⟶} suc M \land X \in A \land M \in On))$
40		simpl	$⊢ (A \in V \land (f : A \underset{1-1 onto}{⟶} suc M \land X \in A \land M \in On)) \to A \in V$
41		simpr3	$⊢ (A \in V \land (f : A \underset{1-1 onto}{⟶} suc M \land X \in A \land M \in On)) \to M \in On$
42	40 41	jca	$⊢ (A \in V \land (f : A \underset{1-1 onto}{⟶} suc M \land X \in A \land M \in On)) \to (A \in V \land M \in On)$
43		simpr	$⊢ (A \in V \land (f : A \underset{1-1 onto}{⟶} suc M \land X \in A \land M \in On)) \to (f : A \underset{1-1 onto}{⟶} suc M \land X \in A \land M \in On)$
44	42 43	jca	$⊢ (A \in V \land (f : A \underset{1-1 onto}{⟶} suc M \land X \in A \land M \in On)) \to ((A \in V \land M \in On) \land (f : A \underset{1-1 onto}{⟶} suc M \land X \in A \land M \in On))$
45		vex	$⊢ f \in V$
46	45	resex	$⊢ {f ↾}_{(A ∖ \{X, f^{-1} (M)\})} \in V$
47		prex	$⊢ \{⟨X, M⟩, ⟨f^{-1} (M), f (X)⟩\} \in V$
48	46 47	unex	$⊢ ({f ↾}_{(A ∖ \{X, f^{-1} (M)\})}) \cup \{⟨X, M⟩, ⟨f^{-1} (M), f (X)⟩\} \in V$
49		dif1enlem	$⊢ ((({f ↾}_{(A ∖ \{X, f^{-1} (M)\})}) \cup \{⟨X, M⟩, ⟨f^{-1} (M), f (X)⟩\} \in V \land A \in V \land M \in On) \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$
50	48 49	mp3anl1	$⊢ ((A \in V \land M \in On) \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$
51	18 50	sylan2	$⊢ ((A \in V \land M \in On) \land (f : A \underset{1-1 onto}{⟶} suc M \land X \in A \land M \in On)) \to (A ∖ \{{(({f ↾}_{(A ∖ \{X, f^{-1} (M)\})}) \cup \{⟨X, M⟩, ⟨f^{-1} (M), f (X)⟩\})}^{-1} (M)\}) \approx M$
52	39 44 51	3syl	$⊢ (f : A \underset{1-1 onto}{⟶} suc M \land (A \in V \land X \in A \land M \in On)) \to (A ∖ \{{(({f ↾}_{(A ∖ \{X, f^{-1} (M)\})}) \cup \{⟨X, M⟩, ⟨f^{-1} (M), f (X)⟩\})}^{-1} (M)\}) \approx M$
53	33 52	eqbrtrrd	$⊢ (f : A \underset{1-1 onto}{⟶} suc M \land (A \in V \land X \in A \land M \in On)) \to (A ∖ \{X\}) \approx M$
54	53	ex	$⊢ f : A \underset{1-1 onto}{⟶} suc M \to ((A \in V \land X \in A \land M \in On) \to (A ∖ \{X\}) \approx M)$
55	54	exlimiv	$⊢ \exists f f : A \underset{1-1 onto}{⟶} suc M \to ((A \in V \land X \in A \land M \in On) \to (A ∖ \{X\}) \approx M)$
56	5 55	sylbi	$⊢ A \approx suc M \to ((A \in V \land X \in A \land M \in On) \to (A ∖ \{X\}) \approx M)$
57	1 4 56	sylc	$⊢ (A \approx suc M \land X \in A \land M \in On) \to (A ∖ \{X\}) \approx M$
58	57	3comr	$⊢ (M \in On \land A \approx suc M \land X \in A) \to (A ∖ \{X\}) \approx M$

Metamath Proof Explorer

Theorem dif1en

Proof