Metamath Proof Explorer

Theorem onssr1

Description: Initial segments of the ordinals are contained in initial segments of the cumulative hierarchy. (Contributed by FL, 20-Apr-2011) (Revised by Mario Carneiro, 17-Nov-2014)

		Ref	Expression
	Assertion	onssr1	$⊢ A \in dom R_{1} \to A \subseteq R_{1} (A)$

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		ordtr1	$⊢ Ord dom R_{1} \to ((x \in A \land A \in dom R_{1}) \to x \in dom R_{1})$
5	2 3 4	mp2b	$⊢ (x \in A \land A \in dom R_{1}) \to x \in dom R_{1}$
6	5	ancoms	$⊢ (A \in dom R_{1} \land x \in A) \to x \in dom R_{1}$
7		rankonidlem	$⊢ x \in dom R_{1} \to (x \in ⋃ R_{1} [On] \land rank (x) = x)$
8	6 7	syl	$⊢ (A \in dom R_{1} \land x \in A) \to (x \in ⋃ R_{1} [On] \land rank (x) = x)$
9	8	simprd	$⊢ (A \in dom R_{1} \land x \in A) \to rank (x) = x$
10		simpr	$⊢ (A \in dom R_{1} \land x \in A) \to x \in A$
11	9 10	eqeltrd	$⊢ (A \in dom R_{1} \land x \in A) \to rank (x) \in A$
12	8	simpld	$⊢ (A \in dom R_{1} \land x \in A) \to x \in ⋃ R_{1} [On]$
13		simpl	$⊢ (A \in dom R_{1} \land x \in A) \to A \in dom R_{1}$
14		rankr1ag	$⊢ (x \in ⋃ R_{1} [On] \land A \in dom R_{1}) \to (x \in R_{1} (A) \leftrightarrow rank (x) \in A)$
15	12 13 14	syl2anc	$⊢ (A \in dom R_{1} \land x \in A) \to (x \in R_{1} (A) \leftrightarrow rank (x) \in A)$
16	11 15	mpbird	$⊢ (A \in dom R_{1} \land x \in A) \to x \in R_{1} (A)$
17	16	ex	$⊢ A \in dom R_{1} \to (x \in A \to x \in R_{1} (A))$
18	17	ssrdv	$⊢ A \in dom R_{1} \to A \subseteq R_{1} (A)$