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		r1funlim	$⊢ (Fun R_{1} \land Lim dom R_{1})$
2	1	simpri	$⊢ Lim dom R_{1}$
3		limord	$⊢ Lim dom R_{1} \to Ord dom R_{1}$
4		ordsson	$⊢ Ord dom R_{1} \to dom R_{1} \subseteq On$
5	2 3 4	mp2b	$⊢ dom R_{1} \subseteq On$
6	5	sseli	$⊢ A \in dom R_{1} \to A \in On$
7	5	sseli	$⊢ B \in dom R_{1} \to B \in On$
8		onsseleq	$⊢ (A \in On \land B \in On) \to (A \subseteq B \leftrightarrow (A \in B \lor A = B))$
9	6 7 8	syl2an	$⊢ (A \in dom R_{1} \land B \in dom R_{1}) \to (A \subseteq B \leftrightarrow (A \in B \lor A = B))$
10		r1tr	$⊢ Tr R_{1} (B)$
11		r1ordg	$⊢ B \in dom R_{1} \to (A \in B \to R_{1} (A) \in R_{1} (B))$
12	11	adantl	$⊢ (A \in dom R_{1} \land B \in dom R_{1}) \to (A \in B \to R_{1} (A) \in R_{1} (B))$
13		trss	$⊢ Tr R_{1} (B) \to (R_{1} (A) \in R_{1} (B) \to R_{1} (A) \subseteq R_{1} (B))$
14	10 12 13	mpsylsyld	$⊢ (A \in dom R_{1} \land B \in dom R_{1}) \to (A \in B \to R_{1} (A) \subseteq R_{1} (B))$
15		fveq2	$⊢ A = B \to R_{1} (A) = R_{1} (B)$
16		eqimss	$⊢ R_{1} (A) = R_{1} (B) \to R_{1} (A) \subseteq R_{1} (B)$
17	15 16	syl	$⊢ A = B \to R_{1} (A) \subseteq R_{1} (B)$
18	17	a1i	$⊢ (A \in dom R_{1} \land B \in dom R_{1}) \to (A = B \to R_{1} (A) \subseteq R_{1} (B))$
19	14 18	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))$
20	9 19	sylbid	$⊢ (A \in dom R_{1} \land B \in dom R_{1}) \to (A \subseteq B \to R_{1} (A) \subseteq R_{1} (B))$

Metamath Proof Explorer

Theorem r1ord3g

Proof