rexdif1en

Description: If a set is equinumerous to a nonzero ordinal, then there exists an element in that set such that removing it leaves the set equinumerous to the predecessor of that ordinal. (Contributed by BTernaryTau, 26-Aug-2024) Generalize to all ordinals and avoid ax-un . (Revised by BTernaryTau, 5-Jan-2025)

		Ref	Expression
	Assertion	rexdif1en	$⊢ (M \in On \land A \approx suc M) \to \exists x \in A (A ∖ \{x\}) \approx M$

Proof

Step	Hyp	Ref	Expression
1		encv	$⊢ A \approx suc M \to (A \in V \land suc M \in V)$
2	1	simpld	$⊢ A \approx suc M \to A \in V$
3		breng	$⊢ (A \in V \land suc M \in V) \to (A \approx suc M \leftrightarrow \exists f f : A \underset{1-1 onto}{⟶} suc M)$
4	1 3	syl	$⊢ A \approx suc M \to (A \approx suc M \leftrightarrow \exists f f : A \underset{1-1 onto}{⟶} suc M)$
5	4	ibi	$⊢ A \approx suc M \to \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	ancoms	$⊢ (M \in suc M \land f : A \underset{1-1 onto}{⟶} suc M) \to f^{-1} (M) \in A$
9	6 8	sylan	$⊢ (M \in On \land f : A \underset{1-1 onto}{⟶} suc M) \to f^{-1} (M) \in A$
10	9	adantll	$⊢ ((A \in V \land M \in On) \land f : A \underset{1-1 onto}{⟶} suc M) \to f^{-1} (M) \in A$
11		vex	$⊢ f \in V$
12		dif1enlem	$⊢ ((f \in V \land A \in V \land M \in On) \land f : A \underset{1-1 onto}{⟶} suc M) \to (A ∖ \{f^{-1} (M)\}) \approx M$
13	11 12	mp3anl1	$⊢ ((A \in V \land M \in On) \land f : A \underset{1-1 onto}{⟶} suc M) \to (A ∖ \{f^{-1} (M)\}) \approx M$
14		sneq	$⊢ x = f^{-1} (M) \to \{x\} = \{f^{-1} (M)\}$
15	14	difeq2d	$⊢ x = f^{-1} (M) \to A ∖ \{x\} = A ∖ \{f^{-1} (M)\}$
16	15	breq1d	$⊢ x = f^{-1} (M) \to ((A ∖ \{x\}) \approx M \leftrightarrow (A ∖ \{f^{-1} (M)\}) \approx M)$
17	16	rspcev	$⊢ (f^{-1} (M) \in A \land (A ∖ \{f^{-1} (M)\}) \approx M) \to \exists x \in A (A ∖ \{x\}) \approx M$
18	10 13 17	syl2anc	$⊢ ((A \in V \land M \in On) \land f : A \underset{1-1 onto}{⟶} suc M) \to \exists x \in A (A ∖ \{x\}) \approx M$
19	18	ex	$⊢ (A \in V \land M \in On) \to (f : A \underset{1-1 onto}{⟶} suc M \to \exists x \in A (A ∖ \{x\}) \approx M)$
20	19	exlimdv	$⊢ (A \in V \land M \in On) \to (\exists f f : A \underset{1-1 onto}{⟶} suc M \to \exists x \in A (A ∖ \{x\}) \approx M)$
21	5 20	syl5	$⊢ (A \in V \land M \in On) \to (A \approx suc M \to \exists x \in A (A ∖ \{x\}) \approx M)$
22	2 21	sylan	$⊢ (A \approx suc M \land M \in On) \to (A \approx suc M \to \exists x \in A (A ∖ \{x\}) \approx M)$
23	22	ancoms	$⊢ (M \in On \land A \approx suc M) \to (A \approx suc M \to \exists x \in A (A ∖ \{x\}) \approx M)$
24	23	syldbl2	$⊢ (M \in On \land A \approx suc M) \to \exists x \in A (A ∖ \{x\}) \approx M$

Metamath Proof Explorer

Theorem rexdif1en

Proof