Metamath Proof Explorer

Theorem r1ord3g

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	r1ord3g	$⊢ (A \in dom R_{1} \land B \in dom R_{1}) \to (A \subseteq B \to R_{1} (A) \subseteq R_{1} (B))$

Proof

Step	Hyp	Ref	Expression
1		r1dmlim	$⊢ Lim dom R_{1}$
2		limord	$⊢ Lim dom R_{1} \to Ord dom R_{1}$
3		ordsson	$⊢ Ord dom R_{1} \to dom R_{1} \subseteq On$
4	1 2 3	mp2b	$⊢ dom R_{1} \subseteq On$
5	4	sseli	$⊢ A \in dom R_{1} \to A \in On$
6	4	sseli	$⊢ B \in dom R_{1} \to B \in On$
7		onsseleq	$⊢ (A \in On \land B \in On) \to (A \subseteq B \leftrightarrow (A \in B \lor A = B))$
8	5 6 7	syl2an	$⊢ (A \in dom R_{1} \land B \in dom R_{1}) \to (A \subseteq B \leftrightarrow (A \in B \lor A = B))$
9		r1tr	$⊢ Tr R_{1} (B)$
10		r1ordg	$⊢ B \in dom R_{1} \to (A \in B \to R_{1} (A) \in R_{1} (B))$
11	10	adantl	$⊢ (A \in dom R_{1} \land B \in dom R_{1}) \to (A \in B \to R_{1} (A) \in R_{1} (B))$
12		trss	$⊢ Tr R_{1} (B) \to (R_{1} (A) \in R_{1} (B) \to R_{1} (A) \subseteq R_{1} (B))$
13	9 11 12	mpsylsyld	$⊢ (A \in dom R_{1} \land B \in dom R_{1}) \to (A \in B \to R_{1} (A) \subseteq R_{1} (B))$
14		fveq2	$⊢ A = B \to R_{1} (A) = R_{1} (B)$
15		eqimss	$⊢ R_{1} (A) = R_{1} (B) \to R_{1} (A) \subseteq R_{1} (B)$
16	14 15	syl	$⊢ A = B \to R_{1} (A) \subseteq R_{1} (B)$
17	16	a1i	$⊢ (A \in dom R_{1} \land B \in dom R_{1}) \to (A = B \to R_{1} (A) \subseteq R_{1} (B))$
18	13 17	jaod	$⊢ (A \in dom R_{1} \land B \in dom R_{1}) \to ((A \in B \lor A = B) \to R_{1} (A) \subseteq R_{1} (B))$
19	8 18	sylbid	$⊢ (A \in dom R_{1} \land B \in dom R_{1}) \to (A \subseteq B \to R_{1} (A) \subseteq R_{1} (B))$