unbndrank

Description: The elements of a proper class have unbounded rank. Exercise 2 of TakeutiZaring p. 80. (Contributed by NM, 13-Oct-2003)

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

Step	Hyp	Ref	Expression
1		rankon	$⊢ rank (y) \in On$
2		ontri1	$⊢ (rank (y) \in On \land x \in On) \to (rank (y) \subseteq x \leftrightarrow \neg x \in rank (y))$
3	1 2	mpan	$⊢ x \in On \to (rank (y) \subseteq x \leftrightarrow \neg x \in rank (y))$
4	3	ralbidv	$⊢ x \in On \to (\forall y \in A rank (y) \subseteq x \leftrightarrow \forall y \in A \neg x \in rank (y))$
5		ralnex	$⊢ \forall y \in A \neg x \in rank (y) \leftrightarrow \neg \exists y \in A x \in rank (y)$
6	4 5	bitrdi	$⊢ x \in On \to (\forall y \in A rank (y) \subseteq x \leftrightarrow \neg \exists y \in A x \in rank (y))$
7	6	rexbiia	$⊢ \exists x \in On \forall y \in A rank (y) \subseteq x \leftrightarrow \exists x \in On \neg \exists y \in A x \in rank (y)$
8		rexnal	$⊢ \exists x \in On \neg \exists y \in A x \in rank (y) \leftrightarrow \neg \forall x \in On \exists y \in A x \in rank (y)$
9	7 8	bitri	$⊢ \exists x \in On \forall y \in A rank (y) \subseteq x \leftrightarrow \neg \forall x \in On \exists y \in A x \in rank (y)$
10		bndrank	$⊢ \exists x \in On \forall y \in A rank (y) \subseteq x \to A \in V$
11	9 10	sylbir	$⊢ \neg \forall x \in On \exists y \in A x \in rank (y) \to A \in V$
12	11	con1i	$⊢ \neg A \in V \to \forall x \in On \exists y \in A x \in rank (y)$

Metamath Proof Explorer