bndrank

Description: Any class whose elements have bounded rank is a set. Proposition 9.19 of TakeutiZaring p. 80. (Contributed by NM, 13-Oct-2003)

		Ref	Expression
	Assertion	bndrank	$⊢ \exists x \in On \forall y \in A rank (y) \subseteq x \to A \in V$

Proof

Step	Hyp	Ref	Expression
1		rankon	$⊢ rank (y) \in On$
2	1	onordi	$⊢ Ord rank (y)$
3		eloni	$⊢ x \in On \to Ord x$
4		ordsucsssuc	$⊢ (Ord rank (y) \land Ord x) \to (rank (y) \subseteq x \leftrightarrow suc rank (y) \subseteq suc x)$
5	2 3 4	sylancr	$⊢ x \in On \to (rank (y) \subseteq x \leftrightarrow suc rank (y) \subseteq suc x)$
6	1	onsuci	$⊢ suc rank (y) \in On$
7		suceloni	$⊢ x \in On \to suc x \in On$
8		r1ord3	$⊢ (suc rank (y) \in On \land suc x \in On) \to (suc rank (y) \subseteq suc x \to R_{1} (suc rank (y)) \subseteq R_{1} (suc x))$
9	6 7 8	sylancr	$⊢ x \in On \to (suc rank (y) \subseteq suc x \to R_{1} (suc rank (y)) \subseteq R_{1} (suc x))$
10	5 9	sylbid	$⊢ x \in On \to (rank (y) \subseteq x \to R_{1} (suc rank (y)) \subseteq R_{1} (suc x))$
11		vex	$⊢ y \in V$
12	11	rankid	$⊢ y \in R_{1} (suc rank (y))$
13		ssel	$⊢ R_{1} (suc rank (y)) \subseteq R_{1} (suc x) \to (y \in R_{1} (suc rank (y)) \to y \in R_{1} (suc x))$
14	10 12 13	syl6mpi	$⊢ x \in On \to (rank (y) \subseteq x \to y \in R_{1} (suc x))$
15	14	ralimdv	$⊢ x \in On \to (\forall y \in A rank (y) \subseteq x \to \forall y \in A y \in R_{1} (suc x))$
16		dfss3	$⊢ A \subseteq R_{1} (suc x) \leftrightarrow \forall y \in A y \in R_{1} (suc x)$
17		fvex	$⊢ R_{1} (suc x) \in V$
18	17	ssex	$⊢ A \subseteq R_{1} (suc x) \to A \in V$
19	16 18	sylbir	$⊢ \forall y \in A y \in R_{1} (suc x) \to A \in V$
20	15 19	syl6	$⊢ x \in On \to (\forall y \in A rank (y) \subseteq x \to A \in V)$
21	20	rexlimiv	$⊢ \exists x \in On \forall y \in A rank (y) \subseteq x \to A \in V$

Metamath Proof Explorer

Theorem bndrank

Proof