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 ⊢ A ∈ V → rank ⁡ A = ⋂ x ∈ On | A ∈ R1 ⁡ suc ⁡ x

Proof

Step Hyp Ref Expression
1 fveq2 ⊢ y = A → rank ⁡ y = rank ⁡ A
2 eleq1 ⊢ y = A → y ∈ R1 ⁡ suc ⁡ x ↔ A ∈ R1 ⁡ suc ⁡ x
3 2 rabbidv ⊢ y = A → x ∈ On | y ∈ R1 ⁡ suc ⁡ x = x ∈ On | A ∈ R1 ⁡ suc ⁡ x
4 3 inteqd ⊢ y = A → ⋂ x ∈ On | y ∈ R1 ⁡ suc ⁡ x = ⋂ x ∈ On | A ∈ R1 ⁡ suc ⁡ x
5 1 4 eqeq12d ⊢ y = A → rank ⁡ y = ⋂ x ∈ On | y ∈ R1 ⁡ suc ⁡ x ↔ rank ⁡ A = ⋂ x ∈ On | A ∈ R1 ⁡ suc ⁡ x
6 vex ⊢ y ∈ V
7 6 rankval ⊢ rank ⁡ y = ⋂ x ∈ On | y ∈ R1 ⁡ suc ⁡ x
8 5 7 vtoclg ⊢ A ∈ V → rank ⁡ A = ⋂ x ∈ On | A ∈ R1 ⁡ suc ⁡ x