Metamath Proof Explorer

Theorem rexdif1en

Description: If a set is equinumerous to a nonzero finite 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)

		Ref	Expression
	Assertion	rexdif1en	$⊢ (M \in ω \land A \approx suc M) \to \exists x \in A (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.42v	$⊢ \exists f (M \in ω \land f : A \underset{1-1 onto}{⟶} suc M) \leftrightarrow (M \in ω \land \exists f f : A \underset{1-1 onto}{⟶} suc M)$
3		sucidg	$⊢ M \in ω \to M \in suc M$
4		f1ocnvdm	$⊢ (f : A \underset{1-1 onto}{⟶} suc M \land M \in suc M) \to f^{-1} (M) \in A$
5	4	ancoms	$⊢ (M \in suc M \land f : A \underset{1-1 onto}{⟶} suc M) \to f^{-1} (M) \in A$
6	3 5	sylan	$⊢ (M \in ω \land f : A \underset{1-1 onto}{⟶} suc M) \to f^{-1} (M) \in A$
7		vex	$⊢ f \in V$
8		dif1enlem	$⊢ (f \in V \land M \in ω \land f : A \underset{1-1 onto}{⟶} suc M) \to (A ∖ \{f^{-1} (M)\}) \approx M$
9	7 8	mp3an1	$⊢ (M \in ω \land f : A \underset{1-1 onto}{⟶} suc M) \to (A ∖ \{f^{-1} (M)\}) \approx M$
10		sneq	$⊢ x = f^{-1} (M) \to \{x\} = \{f^{-1} (M)\}$
11	10	difeq2d	$⊢ x = f^{-1} (M) \to A ∖ \{x\} = A ∖ \{f^{-1} (M)\}$
12	11	breq1d	$⊢ x = f^{-1} (M) \to ((A ∖ \{x\}) \approx M \leftrightarrow (A ∖ \{f^{-1} (M)\}) \approx M)$
13	12	rspcev	$⊢ (f^{-1} (M) \in A \land (A ∖ \{f^{-1} (M)\}) \approx M) \to \exists x \in A (A ∖ \{x\}) \approx M$
14	6 9 13	syl2anc	$⊢ (M \in ω \land f : A \underset{1-1 onto}{⟶} suc M) \to \exists x \in A (A ∖ \{x\}) \approx M$
15	14	exlimiv	$⊢ \exists f (M \in ω \land f : A \underset{1-1 onto}{⟶} suc M) \to \exists x \in A (A ∖ \{x\}) \approx M$
16	2 15	sylbir	$⊢ (M \in ω \land \exists f f : A \underset{1-1 onto}{⟶} suc M) \to \exists x \in A (A ∖ \{x\}) \approx M$
17	1 16	sylan2b	$⊢ (M \in ω \land A \approx suc M) \to \exists x \in A (A ∖ \{x\}) \approx M$