Metamath Proof Explorer

Theorem rankwflemb

Description: Two ways of saying a set is well-founded. (Contributed by NM, 11-Oct-2003) (Revised by Mario Carneiro, 16-Nov-2014)

Ref Expression
Assertion rankwflemb 
|- ( A e. U. ( R1 " On ) <-> E. x e. On A e. ( R1 ` suc x ) )

Proof

Step Hyp Ref Expression
1 eluni 
 |-  ( A e. U. ( R1 " On ) <-> E. y ( A e. y /\ y e. ( R1 " On ) ) )
2 eleq2 
 |-  ( ( R1 ` x ) = y -> ( A e. ( R1 ` x ) <-> A e. y ) )
3 2 biimprcd 
 |-  ( A e. y -> ( ( R1 ` x ) = y -> A e. ( R1 ` x ) ) )
4 r1tr 
 |-  Tr ( R1 ` x )
5 trss 
 |-  ( Tr ( R1 ` x ) -> ( A e. ( R1 ` x ) -> A C_ ( R1 ` x ) ) )
6 4 5 ax-mp 
 |-  ( A e. ( R1 ` x ) -> A C_ ( R1 ` x ) )
7 elpwg 
 |-  ( A e. ( R1 ` x ) -> ( A e. ~P ( R1 ` x ) <-> A C_ ( R1 ` x ) ) )
8 6 7 mpbird 
 |-  ( A e. ( R1 ` x ) -> A e. ~P ( R1 ` x ) )
9 elfvdm 
 |-  ( A e. ( R1 ` x ) -> x e. dom R1 )
10 r1sucg 
 |-  ( x e. dom R1 -> ( R1 ` suc x ) = ~P ( R1 ` x ) )
11 9 10 syl 
 |-  ( A e. ( R1 ` x ) -> ( R1 ` suc x ) = ~P ( R1 ` x ) )
12 8 11 eleqtrrd 
 |-  ( A e. ( R1 ` x ) -> A e. ( R1 ` suc x ) )
13 12 a1i 
 |-  ( x e. On -> ( A e. ( R1 ` x ) -> A e. ( R1 ` suc x ) ) )
14 3 13 syl9 
 |-  ( A e. y -> ( x e. On -> ( ( R1 ` x ) = y -> A e. ( R1 ` suc x ) ) ) )
15 14 reximdvai 
 |-  ( A e. y -> ( E. x e. On ( R1 ` x ) = y -> E. x e. On A e. ( R1 ` suc x ) ) )
16 r1funlim 
 |-  ( Fun R1 /\ Lim dom R1 )
17 16 simpli 
 |-  Fun R1
18 fvelima 
 |-  ( ( Fun R1 /\ y e. ( R1 " On ) ) -> E. x e. On ( R1 ` x ) = y )
19 17 18 mpan 
 |-  ( y e. ( R1 " On ) -> E. x e. On ( R1 ` x ) = y )
20 15 19 impel 
 |-  ( ( A e. y /\ y e. ( R1 " On ) ) -> E. x e. On A e. ( R1 ` suc x ) )
21 20 exlimiv 
 |-  ( E. y ( A e. y /\ y e. ( R1 " On ) ) -> E. x e. On A e. ( R1 ` suc x ) )
22 1 21 sylbi 
 |-  ( A e. U. ( R1 " On ) -> E. x e. On A e. ( R1 ` suc x ) )
23 elfvdm 
 |-  ( A e. ( R1 ` suc x ) -> suc x e. dom R1 )
24 fvelrn 
 |-  ( ( Fun R1 /\ suc x e. dom R1 ) -> ( R1 ` suc x ) e. ran R1 )
25 17 23 24 sylancr 
 |-  ( A e. ( R1 ` suc x ) -> ( R1 ` suc x ) e. ran R1 )
26 df-ima 
 |-  ( R1 " On ) = ran ( R1 |` On )
27 funrel 
 |-  ( Fun R1 -> Rel R1 )
28 17 27 ax-mp 
 |-  Rel R1
29 16 simpri 
 |-  Lim dom R1
30 limord 
 |-  ( Lim dom R1 -> Ord dom R1 )
31 ordsson 
 |-  ( Ord dom R1 -> dom R1 C_ On )
32 29 30 31 mp2b 
 |-  dom R1 C_ On
33 relssres 
 |-  ( ( Rel R1 /\ dom R1 C_ On ) -> ( R1 |` On ) = R1 )
34 28 32 33 mp2an 
 |-  ( R1 |` On ) = R1
35 34 rneqi 
 |-  ran ( R1 |` On ) = ran R1
36 26 35 eqtri 
 |-  ( R1 " On ) = ran R1
37 25 36 eleqtrrdi 
 |-  ( A e. ( R1 ` suc x ) -> ( R1 ` suc x ) e. ( R1 " On ) )
38 elunii 
 |-  ( ( A e. ( R1 ` suc x ) /\ ( R1 ` suc x ) e. ( R1 " On ) ) -> A e. U. ( R1 " On ) )
39 37 38 mpdan 
 |-  ( A e. ( R1 ` suc x ) -> A e. U. ( R1 " On ) )
40 39 rexlimivw 
 |-  ( E. x e. On A e. ( R1 ` suc x ) -> A e. U. ( R1 " On ) )
41 22 40 impbii 
 |-  ( A e. U. ( R1 " On ) <-> E. x e. On A e. ( R1 ` suc x ) )