Metamath Proof Explorer

Theorem rankrelp

Description: The rank function preserves e. . (Contributed by Eric Schmidt, 11-Oct-2025)

Ref Expression
Assertion rankrelp 
|- rank RelPres _E , _E ( U. ( R1 " On ) , On )

Proof

Step Hyp Ref Expression
1 rankf 
 |-  rank : U. ( R1 " On ) --> On
2 rankelb 
 |-  ( y e. U. ( R1 " On ) -> ( x e. y -> ( rank ` x ) e. ( rank ` y ) ) )
3 epel 
 |-  ( x _E y <-> x e. y )
4 fvex 
 |-  ( rank ` y ) e. _V
5 4 epeli 
 |-  ( ( rank ` x ) _E ( rank ` y ) <-> ( rank ` x ) e. ( rank ` y ) )
6 2 3 5 3imtr4g 
 |-  ( y e. U. ( R1 " On ) -> ( x _E y -> ( rank ` x ) _E ( rank ` y ) ) )
7 6 rgen 
 |-  A. y e. U. ( R1 " On ) ( x _E y -> ( rank ` x ) _E ( rank ` y ) )
8 7 rgenw 
 |-  A. x e. U. ( R1 " On ) A. y e. U. ( R1 " On ) ( x _E y -> ( rank ` x ) _E ( rank ` y ) )
9 df-relp 
 |-  ( rank RelPres _E , _E ( U. ( R1 " On ) , On ) <-> ( rank : U. ( R1 " On ) --> On /\ A. x e. U. ( R1 " On ) A. y e. U. ( R1 " On ) ( x _E y -> ( rank ` x ) _E ( rank ` y ) ) ) )
10 1 8 9 mpbir2an 
 |-  rank RelPres _E , _E ( U. ( R1 " On ) , On )