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

Metamath Proof Explorer

Theorem r1elwf

Description: Any member of the cumulative hierarchy is well-founded. (Contributed by Mario Carneiro, 28-May-2013) (Revised by Mario Carneiro, 16-Nov-2014)

Ref Expression
Assertion r1elwf 
|- ( A e. ( R1 ` B ) -> A e. U. ( R1 " On ) )

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 ordsson 
 |-  ( Ord dom R1 -> dom R1 C_ On )
5 2 3 4 mp2b 
 |-  dom R1 C_ On
6 elfvdm 
 |-  ( A e. ( R1 ` B ) -> B e. dom R1 )
7 5 6 sselid 
 |-  ( A e. ( R1 ` B ) -> B e. On )
8 r1tr 
 |-  Tr ( R1 ` B )
9 trss 
 |-  ( Tr ( R1 ` B ) -> ( A e. ( R1 ` B ) -> A C_ ( R1 ` B ) ) )
10 8 9 ax-mp 
 |-  ( A e. ( R1 ` B ) -> A C_ ( R1 ` B ) )
11 elpwg 
 |-  ( A e. ( R1 ` B ) -> ( A e. ~P ( R1 ` B ) <-> A C_ ( R1 ` B ) ) )
12 10 11 mpbird 
 |-  ( A e. ( R1 ` B ) -> A e. ~P ( R1 ` B ) )
13 r1sucg 
 |-  ( B e. dom R1 -> ( R1 ` suc B ) = ~P ( R1 ` B ) )
14 6 13 syl 
 |-  ( A e. ( R1 ` B ) -> ( R1 ` suc B ) = ~P ( R1 ` B ) )
15 12 14 eleqtrrd 
 |-  ( A e. ( R1 ` B ) -> A e. ( R1 ` suc B ) )
16 suceq 
 |-  ( x = B -> suc x = suc B )
17 16 fveq2d 
 |-  ( x = B -> ( R1 ` suc x ) = ( R1 ` suc B ) )
18 17 eleq2d 
 |-  ( x = B -> ( A e. ( R1 ` suc x ) <-> A e. ( R1 ` suc B ) ) )
19 18 rspcev 
 |-  ( ( B e. On /\ A e. ( R1 ` suc B ) ) -> E. x e. On A e. ( R1 ` suc x ) )
20 7 15 19 syl2anc 
 |-  ( A e. ( R1 ` B ) -> E. x e. On A e. ( R1 ` suc x ) )
21 rankwflemb 
 |-  ( A e. U. ( R1 " On ) <-> E. x e. On A e. ( R1 ` suc x ) )
22 20 21 sylibr 
 |-  ( A e. ( R1 ` B ) -> A e. U. ( R1 " On ) )