Metamath Proof Explorer

Theorem r1wf

Description: Each stage in the cumulative hierarchy is well-founded. (Contributed by BTernaryTau, 19-Jan-2026)

Ref Expression
Assertion r1wf 
|- ( R1 ` A ) e. U. ( R1 " On )

Proof

Step Hyp Ref Expression
1 fvex 
 |-  ( R1 ` A ) e. _V
2 1 pwid 
 |-  ( R1 ` A ) e. ~P ( R1 ` A )
3 r1suc 
 |-  ( A e. On -> ( R1 ` suc A ) = ~P ( R1 ` A ) )
4 2 3 eleqtrrid 
 |-  ( A e. On -> ( R1 ` A ) e. ( R1 ` suc A ) )
5 r1elwf 
 |-  ( ( R1 ` A ) e. ( R1 ` suc A ) -> ( R1 ` A ) e. U. ( R1 " On ) )
6 4 5 syl 
 |-  ( A e. On -> ( R1 ` A ) e. U. ( R1 " On ) )
7 onwf 
 |-  On C_ U. ( R1 " On )
8 r1fnon 
 |-  R1 Fn On
9 8 fndmi 
 |-  dom R1 = On
10 9 eleq2i 
 |-  ( A e. dom R1 <-> A e. On )
11 ndmfv 
 |-  ( -. A e. dom R1 -> ( R1 ` A ) = (/) )
12 10 11 sylnbir 
 |-  ( -. A e. On -> ( R1 ` A ) = (/) )
13 0elon 
 |-  (/) e. On
14 12 13 eqeltrdi 
 |-  ( -. A e. On -> ( R1 ` A ) e. On )
15 7 14 sselid 
 |-  ( -. A e. On -> ( R1 ` A ) e. U. ( R1 " On ) )
16 6 15 pm2.61i 
 |-  ( R1 ` A ) e. U. ( R1 " On )