Metamath Proof Explorer

Theorem r1ord2

Description: Ordering relation for the cumulative hierarchy of sets. Part of Proposition 9.10(2) of TakeutiZaring p. 77. (Contributed by NM, 22-Sep-2003)

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

Proof

Step	Hyp	Ref	Expression
1		r1tr	$⊢ Tr R_{1} (B)$
2		r1ord	$⊢ B \in On \to (A \in B \to R_{1} (A) \in R_{1} (B))$
3		trss	$⊢ Tr R_{1} (B) \to (R_{1} (A) \in R_{1} (B) \to R_{1} (A) \subseteq R_{1} (B))$
4	1 2 3	mpsylsyld	$⊢ B \in On \to (A \in B \to R_{1} (A) \subseteq R_{1} (B))$