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∈⋃R1On→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∈⋃R1On→∀y∈Arank⁡y∈x↔rank⁡A∈x
4 3 rabbidv ⊢A∈⋃R1On→x∈On|∀y∈Arank⁡y∈x=x∈On|rank⁡A∈x
5 4 inteqd ⊢A∈⋃R1On→⋂x∈On|∀y∈Arank⁡y∈x=⋂x∈On|rank⁡A∈x
6 snwf ⊢A∈⋃R1On→A∈⋃R1On
7 rankval3b ⊢A∈⋃R1On→rank⁡A=⋂x∈On|∀y∈Arank⁡y∈x
8 6 7 syl ⊢A∈⋃R1On→rank⁡A=⋂x∈On|∀y∈Arank⁡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∈⋃R1On→suc⁡rank⁡A=⋂x∈On|rank⁡A∈x
12 5 8 11 3eqtr4d ⊢A∈⋃R1On→rank⁡A=suc⁡rank⁡A