Metamath Proof Explorer

Theorem r1ord

Description: Ordering relation for the cumulative hierarchy of sets. Part of Proposition 9.10(2) of TakeutiZaring p. 77. (Contributed by NM, 8-Sep-2003) (Revised by Mario Carneiro, 16-Nov-2014)

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

Proof

Step	Hyp	Ref	Expression
1		r1fnon	$⊢ R_{1} Fn On$
2	1	fndmi	$⊢ dom R_{1} = On$
3	2	eleq2i	$⊢ B \in dom R_{1} \leftrightarrow B \in On$
4		r1ordg	$⊢ B \in dom R_{1} \to (A \in B \to R_{1} (A) \in R_{1} (B))$
5	3 4	sylbir	$⊢ B \in On \to (A \in B \to R_{1} (A) \in R_{1} (B))$