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 ( 𝐴𝐵 → ( rank ‘ 𝐴 ) = { 𝑥 ∈ On ∣ 𝐴 ⊆ ( 𝑅1𝑥 ) } )

Proof

Step Hyp Ref Expression
1 rankvalg ( 𝐴𝐵 → ( rank ‘ 𝐴 ) = { 𝑥 ∈ On ∣ 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) } )
2 r1suc ( 𝑥 ∈ On → ( 𝑅1 ‘ suc 𝑥 ) = 𝒫 ( 𝑅1𝑥 ) )
3 2 eleq2d ( 𝑥 ∈ On → ( 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) ↔ 𝐴 ∈ 𝒫 ( 𝑅1𝑥 ) ) )
4 fvex ( 𝑅1𝑥 ) ∈ V
5 4 elpw2 ( 𝐴 ∈ 𝒫 ( 𝑅1𝑥 ) ↔ 𝐴 ⊆ ( 𝑅1𝑥 ) )
6 3 5 bitrdi ( 𝑥 ∈ On → ( 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) ↔ 𝐴 ⊆ ( 𝑅1𝑥 ) ) )
7 6 rabbiia { 𝑥 ∈ On ∣ 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) } = { 𝑥 ∈ On ∣ 𝐴 ⊆ ( 𝑅1𝑥 ) }
8 7 inteqi { 𝑥 ∈ On ∣ 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) } = { 𝑥 ∈ On ∣ 𝐴 ⊆ ( 𝑅1𝑥 ) }
9 1 8 eqtrdi ( 𝐴𝐵 → ( rank ‘ 𝐴 ) = { 𝑥 ∈ On ∣ 𝐴 ⊆ ( 𝑅1𝑥 ) } )