Metamath Proof Explorer


Theorem rankrelp

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

Ref Expression
Assertion rankrelp Could not format assertion : No typesetting found for |- rank RelPres _E , _E ( U. ( R1 " On ) , On ) with typecode |-

Proof

Step Hyp Ref Expression
1 rankf rank : R1 On On
2 rankelb y R1 On x y rank x rank y
3 epel x E y x y
4 fvex rank y V
5 4 epeli rank x E rank y rank x rank y
6 2 3 5 3imtr4g y R1 On x E y rank x E rank y
7 6 rgen y R1 On x E y rank x E rank y
8 7 rgenw x R1 On y R1 On x E y rank x E rank y
9 df-relp Could not format ( 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 ) ) ) ) : No typesetting found for |- ( 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 ) ) ) ) with typecode |-
10 1 8 9 mpbir2an Could not format rank RelPres _E , _E ( U. ( R1 " On ) , On ) : No typesetting found for |- rank RelPres _E , _E ( U. ( R1 " On ) , On ) with typecode |-