rankdmr1

Description: A rank is a member of the cumulative hierarchy. (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		r1funlim	$⊢ (Fun R_{1} \land Lim dom R_{1})$
5	4	simpri	$⊢ Lim dom R_{1}$
6		limsuc	$⊢ Lim dom R_{1} \to (rank (A) \in dom R_{1} \leftrightarrow suc rank (A) \in dom R_{1})$
7	5 6	ax-mp	$⊢ rank (A) \in dom R_{1} \leftrightarrow suc rank (A) \in dom R_{1}$
8	3 7	sylibr	$⊢ A \in ⋃ R_{1} [On] \to rank (A) \in dom R_{1}$
9		rankvaln	$⊢ \neg A \in ⋃ R_{1} [On] \to rank (A) = \emptyset$
10		limomss	$⊢ Lim dom R_{1} \to ω \subseteq dom R_{1}$
11	5 10	ax-mp	$⊢ ω \subseteq dom R_{1}$
12		peano1	$⊢ \emptyset \in ω$
13	11 12	sselii	$⊢ \emptyset \in dom R_{1}$
14	9 13	eqeltrdi	$⊢ \neg A \in ⋃ R_{1} [On] \to rank (A) \in dom R_{1}$
15	8 14	pm2.61i	$⊢ rank (A) \in dom R_{1}$

Metamath Proof Explorer