unbnn2

Description: Version of unbnn that does not require a strict upper bound. (Contributed by NM, 24-Apr-2004)

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

Step	Hyp	Ref	Expression
1		peano2	$⊢ z \in ω \to suc z \in ω$
2		sseq1	$⊢ x = suc z \to (x \subseteq y \leftrightarrow suc z \subseteq y)$
3	2	rexbidv	$⊢ x = suc z \to (\exists y \in A x \subseteq y \leftrightarrow \exists y \in A suc z \subseteq y)$
4	3	rspcv	$⊢ suc z \in ω \to (\forall x \in ω \exists y \in A x \subseteq y \to \exists y \in A suc z \subseteq y)$
5		sucssel	$⊢ z \in V \to (suc z \subseteq y \to z \in y)$
6	5	elv	$⊢ suc z \subseteq y \to z \in y$
7	6	reximi	$⊢ \exists y \in A suc z \subseteq y \to \exists y \in A z \in y$
8	4 7	syl6com	$⊢ \forall x \in ω \exists y \in A x \subseteq y \to (suc z \in ω \to \exists y \in A z \in y)$
9	1 8	syl5	$⊢ \forall x \in ω \exists y \in A x \subseteq y \to (z \in ω \to \exists y \in A z \in y)$
10	9	ralrimiv	$⊢ \forall x \in ω \exists y \in A x \subseteq y \to \forall z \in ω \exists y \in A z \in y$
11		unbnn	$⊢ (ω \in V \land A \subseteq ω \land \forall z \in ω \exists y \in A z \in y) \to A \approx ω$
12	10 11	syl3an3	$⊢ (ω \in V \land A \subseteq ω \land \forall x \in ω \exists y \in A x \subseteq y) \to A \approx ω$

Metamath Proof Explorer