This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 𝑥 ) } )