rankdmr1

Description: A rank is a member of the cumulative hierarchy of sets. (Contributed by Mario Carneiro, 17-Nov-2014)

		Ref	Expression
	Assertion	rankdmr1	$⊢ rank (A) \in dom R_{1}$

Step	Hyp	Ref	Expression
1		rankidb	$⊢ A \in ⋃ R_{1} [On] \to A \in R_{1} (suc rank (A))$
2		elfvdm	$⊢ A \in R_{1} (suc rank (A)) \to suc rank (A) \in dom R_{1}$
3	1 2	syl	$⊢ A \in ⋃ R_{1} [On] \to suc rank (A) \in dom R_{1}$
4		r1dmlim	$⊢ Lim dom R_{1}$
5		limsuc	$⊢ Lim dom R_{1} \to (rank (A) \in dom R_{1} \leftrightarrow suc rank (A) \in dom R_{1})$
6	4 5	ax-mp	$⊢ rank (A) \in dom R_{1} \leftrightarrow suc rank (A) \in dom R_{1}$
7	3 6	sylibr	$⊢ A \in ⋃ R_{1} [On] \to rank (A) \in dom R_{1}$
8		rankvaln	$⊢ \neg A \in ⋃ R_{1} [On] \to rank (A) = \emptyset$
9		limomss	$⊢ Lim dom R_{1} \to ω \subseteq dom R_{1}$
10	4 9	ax-mp	$⊢ ω \subseteq dom R_{1}$
11		peano1	$⊢ \emptyset \in ω$
12	10 11	sselii	$⊢ \emptyset \in dom R_{1}$
13	8 12	eqeltrdi	$⊢ \neg A \in ⋃ R_{1} [On] \to rank (A) \in dom R_{1}$
14	7 13	pm2.61i	$⊢ rank (A) \in dom R_{1}$

Metamath Proof Explorer