This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem r1sssuc

Description: The value of the cumulative hierarchy of sets function is a subset of its value at the successor. JFM CLASSES1 Th. 39. (Contributed by FL, 20-Apr-2011)

		Ref	Expression
	Assertion	r1sssuc	$⊢ A \in On \to R_{1} (A) \subseteq R_{1} (suc A)$

Proof

Step	Hyp	Ref	Expression
1		r1tr	$⊢ Tr R_{1} (A)$
2		dftr4	$⊢ Tr R_{1} (A) \leftrightarrow R_{1} (A) \subseteq 𝒫 R_{1} (A)$
3	1 2	mpbi	$⊢ R_{1} (A) \subseteq 𝒫 R_{1} (A)$
4		r1suc	$⊢ A \in On \to R_{1} (suc A) = 𝒫 R_{1} (A)$
5	3 4	sseqtrrid	$⊢ A \in On \to R_{1} (A) \subseteq R_{1} (suc A)$