unbnn

Description: Any unbounded subset of natural numbers is equinumerous to the set of all natural numbers. Part of the proof of Theorem 42 of Suppes p. 151. See unbnn3 for a stronger version without the first assumption. (Contributed by NM, 3-Dec-2003)

		Ref	Expression
	Assertion	unbnn	$⊢ (ω \in V \land A \subseteq ω \land \forall x \in ω \exists y \in A x \in y) \to A \approx ω$

Proof

Step	Hyp	Ref	Expression
1		ssdomg	$⊢ ω \in V \to (A \subseteq ω \to A ≼ ω)$
2	1	imp	$⊢ (ω \in V \land A \subseteq ω) \to A ≼ ω$
3	2	3adant3	$⊢ (ω \in V \land A \subseteq ω \land \forall x \in ω \exists y \in A x \in y) \to A ≼ ω$
4		simp1	$⊢ (ω \in V \land A \subseteq ω \land \forall x \in ω \exists y \in A x \in y) \to ω \in V$
5		ssexg	$⊢ (A \subseteq ω \land ω \in V) \to A \in V$
6	5	ancoms	$⊢ (ω \in V \land A \subseteq ω) \to A \in V$
7	6	3adant3	$⊢ (ω \in V \land A \subseteq ω \land \forall x \in ω \exists y \in A x \in y) \to A \in V$
8		eqid	$⊢ {rec ((z \in V ⟼ ⋂ (A ∖ suc z)), ⋂ A) ↾}_{ω} = {rec ((z \in V ⟼ ⋂ (A ∖ suc z)), ⋂ A) ↾}_{ω}$
9	8	unblem4	$⊢ (A \subseteq ω \land \forall x \in ω \exists y \in A x \in y) \to ({rec ((z \in V ⟼ ⋂ (A ∖ suc z)), ⋂ A) ↾}_{ω}) : ω \underset{1-1}{⟶} A$
10	9	3adant1	$⊢ (ω \in V \land A \subseteq ω \land \forall x \in ω \exists y \in A x \in y) \to ({rec ((z \in V ⟼ ⋂ (A ∖ suc z)), ⋂ A) ↾}_{ω}) : ω \underset{1-1}{⟶} A$
11		f1dom2g	$⊢ (ω \in V \land A \in V \land ({rec ((z \in V ⟼ ⋂ (A ∖ suc z)), ⋂ A) ↾}_{ω}) : ω \underset{1-1}{⟶} A) \to ω ≼ A$
12	4 7 10 11	syl3anc	$⊢ (ω \in V \land A \subseteq ω \land \forall x \in ω \exists y \in A x \in y) \to ω ≼ A$
13		sbth	$⊢ (A ≼ ω \land ω ≼ A) \to A \approx ω$
14	3 12 13	syl2anc	$⊢ (ω \in V \land A \subseteq ω \land \forall x \in ω \exists y \in A x \in y) \to A \approx ω$

Metamath Proof Explorer

Theorem unbnn

Proof