r1rankcld

Description: Any rank of the cumulative hierarchy is closed under the rank function. (Contributed by Rohan Ridenour, 11-Aug-2023)

		Ref	Expression
	Hypothesis	r1rankcld.1	$⊢ φ \to A \in R_{1} (R)$
	Assertion	r1rankcld	$⊢ φ \to rank (A) \in R_{1} (R)$

Step	Hyp	Ref	Expression
1		r1rankcld.1	$⊢ φ \to A \in R_{1} (R)$
2		onssr1	$⊢ R \in dom R_{1} \to R \subseteq R_{1} (R)$
3	2	adantl	$⊢ (φ \land R \in dom R_{1}) \to R \subseteq R_{1} (R)$
4		rankr1ai	$⊢ A \in R_{1} (R) \to rank (A) \in R$
5	1 4	syl	$⊢ φ \to rank (A) \in R$
6	5	adantr	$⊢ (φ \land R \in dom R_{1}) \to rank (A) \in R$
7	3 6	sseldd	$⊢ (φ \land R \in dom R_{1}) \to rank (A) \in R_{1} (R)$
8	1	adantr	$⊢ (φ \land \neg R \in dom R_{1}) \to A \in R_{1} (R)$
9		noel	$⊢ \neg A \in \emptyset$
10	9	a1i	$⊢ \neg R \in dom R_{1} \to \neg A \in \emptyset$
11		ndmfv	$⊢ \neg R \in dom R_{1} \to R_{1} (R) = \emptyset$
12	10 11	neleqtrrd	$⊢ \neg R \in dom R_{1} \to \neg A \in R_{1} (R)$
13	12	adantl	$⊢ (φ \land \neg R \in dom R_{1}) \to \neg A \in R_{1} (R)$
14	8 13	pm2.21dd	$⊢ (φ \land \neg R \in dom R_{1}) \to rank (A) \in R_{1} (R)$
15	7 14	pm2.61dan	$⊢ φ \to rank (A) \in R_{1} (R)$

Metamath Proof Explorer