Metamath Proof Explorer


Theorem rankvalg

Description: Value of the rank function. Definition 9.14 of TakeutiZaring p. 79 (proved as a theorem from our definition). This variant of rankval expresses the class existence requirement as an antecedent instead of a hypothesis. (Contributed by NM, 5-Oct-2003)

Ref Expression
Assertion rankvalg ( 𝐴𝑉 → ( rank ‘ 𝐴 ) = { 𝑥 ∈ On ∣ 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) } )

Proof

Step Hyp Ref Expression
1 fveq2 ( 𝑦 = 𝐴 → ( rank ‘ 𝑦 ) = ( rank ‘ 𝐴 ) )
2 eleq1 ( 𝑦 = 𝐴 → ( 𝑦 ∈ ( 𝑅1 ‘ suc 𝑥 ) ↔ 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) ) )
3 2 rabbidv ( 𝑦 = 𝐴 → { 𝑥 ∈ On ∣ 𝑦 ∈ ( 𝑅1 ‘ suc 𝑥 ) } = { 𝑥 ∈ On ∣ 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) } )
4 3 inteqd ( 𝑦 = 𝐴 { 𝑥 ∈ On ∣ 𝑦 ∈ ( 𝑅1 ‘ suc 𝑥 ) } = { 𝑥 ∈ On ∣ 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) } )
5 1 4 eqeq12d ( 𝑦 = 𝐴 → ( ( rank ‘ 𝑦 ) = { 𝑥 ∈ On ∣ 𝑦 ∈ ( 𝑅1 ‘ suc 𝑥 ) } ↔ ( rank ‘ 𝐴 ) = { 𝑥 ∈ On ∣ 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) } ) )
6 vex 𝑦 ∈ V
7 6 rankval ( rank ‘ 𝑦 ) = { 𝑥 ∈ On ∣ 𝑦 ∈ ( 𝑅1 ‘ suc 𝑥 ) }
8 5 7 vtoclg ( 𝐴𝑉 → ( rank ‘ 𝐴 ) = { 𝑥 ∈ On ∣ 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) } )