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

Metamath Proof Explorer

Theorem ranksuc

Description: The rank of a successor. (Contributed by NM, 18-Sep-2006)

Ref Expression
Hypothesis rankr1b.1 ⊢ A ∈ V
Assertion ranksuc ⊢ rank ⁡ suc ⁡ A = suc ⁡ rank ⁡ A

Proof

Step Hyp Ref Expression
1 rankr1b.1 ⊢ A ∈ V
2 df-suc ⊢ suc ⁡ A = A ∪ A
3 2 fveq2i ⊢ rank ⁡ suc ⁡ A = rank ⁡ A ∪ A
4 snex ⊢ A ∈ V
5 1 4 rankun ⊢ rank ⁡ A ∪ A = rank ⁡ A ∪ rank ⁡ A
6 1 ranksn ⊢ rank ⁡ A = suc ⁡ rank ⁡ A
7 6 uneq2i ⊢ rank ⁡ A ∪ rank ⁡ A = rank ⁡ A ∪ suc ⁡ rank ⁡ A
8 sssucid ⊢ rank ⁡ A ⊆ suc ⁡ rank ⁡ A
9 ssequn1 ⊢ rank ⁡ A ⊆ suc ⁡ rank ⁡ A ↔ rank ⁡ A ∪ suc ⁡ rank ⁡ A = suc ⁡ rank ⁡ A
10 8 9 mpbi ⊢ rank ⁡ A ∪ suc ⁡ rank ⁡ A = suc ⁡ rank ⁡ A
11 7 10 eqtri ⊢ rank ⁡ A ∪ rank ⁡ A = suc ⁡ rank ⁡ A
12 5 11 eqtri ⊢ rank ⁡ A ∪ A = suc ⁡ rank ⁡ A
13 3 12 eqtri ⊢ rank ⁡ suc ⁡ A = suc ⁡ rank ⁡ A