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 e. dom R1 -> A C_ ( R1 ` A ) )

Proof

Step	Hyp	Ref	Expression
1		r1dmlim	|- Lim dom R1
2		limord	|- ( Lim dom R1 -> Ord dom R1 )
3		ordtr1	|- ( Ord dom R1 -> ( ( x e. A /\ A e. dom R1 ) -> x e. dom R1 ) )
4	1 2 3	mp2b	|- ( ( x e. A /\ A e. dom R1 ) -> x e. dom R1 )
5	4	ancoms	|- ( ( A e. dom R1 /\ x e. A ) -> x e. dom R1 )
6		rankonidlem	|- ( x e. dom R1 -> ( x e. U. ( R1 " On ) /\ ( rank ` x ) = x ) )
7	5 6	syl	|- ( ( A e. dom R1 /\ x e. A ) -> ( x e. U. ( R1 " On ) /\ ( rank ` x ) = x ) )
8	7	simprd	|- ( ( A e. dom R1 /\ x e. A ) -> ( rank ` x ) = x )
9		simpr	|- ( ( A e. dom R1 /\ x e. A ) -> x e. A )
10	8 9	eqeltrd	|- ( ( A e. dom R1 /\ x e. A ) -> ( rank ` x ) e. A )
11	7	simpld	|- ( ( A e. dom R1 /\ x e. A ) -> x e. U. ( R1 " On ) )
12		simpl	|- ( ( A e. dom R1 /\ x e. A ) -> A e. dom R1 )
13		rankr1ag	|- ( ( x e. U. ( R1 " On ) /\ A e. dom R1 ) -> ( x e. ( R1 ` A ) <-> ( rank ` x ) e. A ) )
14	11 12 13	syl2anc	|- ( ( A e. dom R1 /\ x e. A ) -> ( x e. ( R1 ` A ) <-> ( rank ` x ) e. A ) )
15	10 14	mpbird	|- ( ( A e. dom R1 /\ x e. A ) -> x e. ( R1 ` A ) )
16	15	ex	|- ( A e. dom R1 -> ( x e. A -> x e. ( R1 ` A ) ) )
17	16	ssrdv	|- ( A e. dom R1 -> A C_ ( R1 ` A ) )