infpssr

Description: Dedekind infinity implies existence of a denumerable subset: take a single point witnessing the proper subset relation and iterate the embedding. (Contributed by Stefan O'Rear, 30-Oct-2014) (Revised by Mario Carneiro, 16-May-2015)

		Ref	Expression
	Assertion	infpssr	$⊢ (X \subset A \land X \approx A) \to ω ≼ A$

Proof

Step	Hyp	Ref	Expression
1		pssnel	$⊢ X \subset A \to \exists y (y \in A \land \neg y \in X)$
2	1	adantr	$⊢ (X \subset A \land X \approx A) \to \exists y (y \in A \land \neg y \in X)$
3		eldif	$⊢ y \in (A ∖ X) \leftrightarrow (y \in A \land \neg y \in X)$
4		pssss	$⊢ X \subset A \to X \subseteq A$
5		bren	$⊢ X \approx A \leftrightarrow \exists f f : X \underset{1-1 onto}{⟶} A$
6		simpr	$⊢ ((y \in (A ∖ X) \land X \subseteq A) \land f : X \underset{1-1 onto}{⟶} A) \to f : X \underset{1-1 onto}{⟶} A$
7		f1ofo	$⊢ f : X \underset{1-1 onto}{⟶} A \to f : X \underset{onto}{⟶} A$
8		forn	$⊢ f : X \underset{onto}{⟶} A \to ran f = A$
9	6 7 8	3syl	$⊢ ((y \in (A ∖ X) \land X \subseteq A) \land f : X \underset{1-1 onto}{⟶} A) \to ran f = A$
10		vex	$⊢ f \in V$
11	10	rnex	$⊢ ran f \in V$
12	9 11	eqeltrrdi	$⊢ ((y \in (A ∖ X) \land X \subseteq A) \land f : X \underset{1-1 onto}{⟶} A) \to A \in V$
13		simplr	$⊢ ((y \in (A ∖ X) \land X \subseteq A) \land f : X \underset{1-1 onto}{⟶} A) \to X \subseteq A$
14		simpll	$⊢ ((y \in (A ∖ X) \land X \subseteq A) \land f : X \underset{1-1 onto}{⟶} A) \to y \in (A ∖ X)$
15		eqid	$⊢ {rec (f^{-1}, y) ↾}_{ω} = {rec (f^{-1}, y) ↾}_{ω}$
16	13 6 14 15	infpssrlem5	$⊢ ((y \in (A ∖ X) \land X \subseteq A) \land f : X \underset{1-1 onto}{⟶} A) \to (A \in V \to ω ≼ A)$
17	12 16	mpd	$⊢ ((y \in (A ∖ X) \land X \subseteq A) \land f : X \underset{1-1 onto}{⟶} A) \to ω ≼ A$
18	17	ex	$⊢ (y \in (A ∖ X) \land X \subseteq A) \to (f : X \underset{1-1 onto}{⟶} A \to ω ≼ A)$
19	18	exlimdv	$⊢ (y \in (A ∖ X) \land X \subseteq A) \to (\exists f f : X \underset{1-1 onto}{⟶} A \to ω ≼ A)$
20	5 19	biimtrid	$⊢ (y \in (A ∖ X) \land X \subseteq A) \to (X \approx A \to ω ≼ A)$
21	20	ex	$⊢ y \in (A ∖ X) \to (X \subseteq A \to (X \approx A \to ω ≼ A))$
22	4 21	syl5	$⊢ y \in (A ∖ X) \to (X \subset A \to (X \approx A \to ω ≼ A))$
23	22	impd	$⊢ y \in (A ∖ X) \to ((X \subset A \land X \approx A) \to ω ≼ A)$
24	3 23	sylbir	$⊢ (y \in A \land \neg y \in X) \to ((X \subset A \land X \approx A) \to ω ≼ A)$
25	24	exlimiv	$⊢ \exists y (y \in A \land \neg y \in X) \to ((X \subset A \land X \approx A) \to ω ≼ A)$
26	2 25	mpcom	$⊢ (X \subset A \land X \approx A) \to ω ≼ A$

Metamath Proof Explorer

Theorem infpssr

Proof