Metamath Proof Explorer

Theorem rankwflemb

Description: Two ways of expressing that a set is well-founded. (Contributed by NM, 11-Oct-2003) (Revised by Mario Carneiro, 16-Nov-2014) (Proof shortened by BJ, 29-Sep-2026)

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 r1fun 
 |-  Fun R1
17 fvelima 
 |-  ( ( Fun R1 /\ y e. ( R1 " On ) ) -> E. x e. On ( R1 ` x ) = y )
18 16 17 mpan 
 |-  ( y e. ( R1 " On ) -> E. x e. On ( R1 ` x ) = y )
19 15 18 impel 
 |-  ( ( A e. y /\ y e. ( R1 " On ) ) -> E. x e. On A e. ( R1 ` suc x ) )
20 19 exlimiv 
 |-  ( E. y ( A e. y /\ y e. ( R1 " On ) ) -> E. x e. On A e. ( R1 ` suc x ) )
21 1 20 sylbi 
 |-  ( A e. U. ( R1 " On ) -> E. x e. On A e. ( R1 ` suc x ) )
22 elfvdm 
 |-  ( A e. ( R1 ` suc x ) -> suc x e. dom R1 )
23 fvelrn 
 |-  ( ( Fun R1 /\ suc x e. dom R1 ) -> ( R1 ` suc x ) e. ran R1 )
24 16 22 23 sylancr 
 |-  ( A e. ( R1 ` suc x ) -> ( R1 ` suc x ) e. ran R1 )
25 rnr1 
 |-  ran R1 = ( R1 " On )
26 24 25 eleqtrdi 
 |-  ( A e. ( R1 ` suc x ) -> ( R1 ` suc x ) e. ( R1 " On ) )
27 elunii 
 |-  ( ( A e. ( R1 ` suc x ) /\ ( R1 ` suc x ) e. ( R1 " On ) ) -> A e. U. ( R1 " On ) )
28 26 27 mpdan 
 |-  ( A e. ( R1 ` suc x ) -> A e. U. ( R1 " On ) )
29 28 rexlimivw 
 |-  ( E. x e. On A e. ( R1 ` suc x ) -> A e. U. ( R1 " On ) )
30 21 29 impbii 
 |-  ( A e. U. ( R1 " On ) <-> E. x e. On A e. ( R1 ` suc x ) )