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