Metamath Proof Explorer

Theorem r1ord3

Description: Ordering relation for the cumulative hierarchy of sets. Part of Theorem 3.3(i) of BellMachover p. 478. (Contributed by NM, 22-Sep-2003)

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

Proof

Step	Hyp	Ref	Expression
1		r1fnon	$⊢ R_{1} Fn On$
2		fndm	$⊢ R_{1} Fn On \to dom R_{1} = On$
3	1 2	ax-mp	$⊢ dom R_{1} = On$
4	3	eleq2i	$⊢ A \in dom R_{1} \leftrightarrow A \in On$
5	3	eleq2i	$⊢ B \in dom R_{1} \leftrightarrow B \in On$
6		r1ord3g	$⊢ (A \in dom R_{1} \land B \in dom R_{1}) \to (A \subseteq B \to R_{1} (A) \subseteq R_{1} (B))$
7	4 5 6	syl2anbr	$⊢ (A \in On \land B \in On) \to (A \subseteq B \to R_{1} (A) \subseteq R_{1} (B))$