Metamath Proof Explorer

Theorem rankvalb

Description: Value of the rank function. Definition 9.14 of TakeutiZaring p. 79 (proved as a theorem from our definition). This variant of rankval does not use the axiom of regularity, and so requires the assumption that A is in the range of R1 . (Contributed by NM, 11-Oct-2003) (Revised by Mario Carneiro, 10-Sep-2013)

Ref Expression
Assertion rankvalb ⊢ A ∈ ⋃ R1 On → rank ⁡ A = ⋂ x ∈ On | A ∈ R1 ⁡ suc ⁡ x

Proof

Step Hyp Ref Expression
1 df-rank ⊢ rank = y ∈ V ⟼ ⋂ x ∈ On | y ∈ R1 ⁡ suc ⁡ x
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 elex ⊢ A ∈ ⋃ R1 On → A ∈ V
6 rankwflemb ⊢ A ∈ ⋃ R1 On ↔ ∃ x ∈ On A ∈ R1 ⁡ suc ⁡ x
7 intexrab ⊢ ∃ x ∈ On A ∈ R1 ⁡ suc ⁡ x ↔ ⋂ x ∈ On | A ∈ R1 ⁡ suc ⁡ x ∈ V
8 6 7 sylbb ⊢ A ∈ ⋃ R1 On → ⋂ x ∈ On | A ∈ R1 ⁡ suc ⁡ x ∈ V
9 1 4 5 8 fvmptd3 ⊢ A ∈ ⋃ R1 On → rank ⁡ A = ⋂ x ∈ On | A ∈ R1 ⁡ suc ⁡ x