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

Metamath Proof Explorer

Theorem ranksnb

Description: The rank of a singleton. Theorem 15.17(v) of Monk1 p. 112. (Contributed by Mario Carneiro, 10-Jun-2013)

Ref Expression
Assertion ranksnb ⊢ A ∈ ⋃ R1 On → rank ⁡ A = suc ⁡ rank ⁡ A

Proof

Step Hyp Ref Expression
1 fveq2 ⊢ y = A → rank ⁡ y = rank ⁡ A
2 1 eleq1d ⊢ y = A → rank ⁡ y ∈ x ↔ rank ⁡ A ∈ x
3 2 ralsng ⊢ A ∈ ⋃ R1 On → ∀ y ∈ A rank ⁡ y ∈ x ↔ rank ⁡ A ∈ x
4 3 rabbidv ⊢ A ∈ ⋃ R1 On → x ∈ On | ∀ y ∈ A rank ⁡ y ∈ x = x ∈ On | rank ⁡ A ∈ x
5 4 inteqd ⊢ A ∈ ⋃ R1 On → ⋂ x ∈ On | ∀ y ∈ A rank ⁡ y ∈ x = ⋂ x ∈ On | rank ⁡ A ∈ x
6 snwf ⊢ A ∈ ⋃ R1 On → A ∈ ⋃ R1 On
7 rankval3b ⊢ A ∈ ⋃ R1 On → rank ⁡ A = ⋂ x ∈ On | ∀ y ∈ A rank ⁡ y ∈ x
8 6 7 syl ⊢ A ∈ ⋃ R1 On → rank ⁡ A = ⋂ x ∈ On | ∀ y ∈ A rank ⁡ y ∈ x
9 rankon ⊢ rank ⁡ A ∈ On
10 onsucmin ⊢ rank ⁡ A ∈ On → suc ⁡ rank ⁡ A = ⋂ x ∈ On | rank ⁡ A ∈ x
11 9 10 mp1i ⊢ A ∈ ⋃ R1 On → suc ⁡ rank ⁡ A = ⋂ x ∈ On | rank ⁡ A ∈ x
12 5 8 11 3eqtr4d ⊢ A ∈ ⋃ R1 On → rank ⁡ A = suc ⁡ rank ⁡ A