This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 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 ) )