Metamath Proof Explorer


Theorem rankval2

Description: Value of an alternate definition of the rank function. Definition of BellMachover p. 478. (Contributed by NM, 8-Oct-2003)

Ref Expression
Assertion rankval2 A B rank A = x On | A R1 x

Proof

Step Hyp Ref Expression
1 rankvalg A B rank A = x On | A R1 suc x
2 r1suc x On R1 suc x = 𝒫 R1 x
3 2 eleq2d x On A R1 suc x A 𝒫 R1 x
4 fvex R1 x V
5 4 elpw2 A 𝒫 R1 x A R1 x
6 3 5 bitrdi x On A R1 suc x A R1 x
7 6 rabbiia x On | A R1 suc x = x On | A R1 x
8 7 inteqi x On | A R1 suc x = x On | A R1 x
9 1 8 eqtrdi A B rank A = x On | A R1 x