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

Metamath Proof Explorer

Theorem rankdmr1

Description: A rank is a member of the cumulative hierarchy. (Contributed by Mario Carneiro, 17-Nov-2014)

Ref Expression
Assertion rankdmr1 ( rank ‘ 𝐴 ) ∈ dom 𝑅1

Proof

Step Hyp Ref Expression
1 rankidb ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → 𝐴 ∈ ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) )
2 elfvdm ⊢ ( 𝐴 ∈ ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) → suc ( rank ‘ 𝐴 ) ∈ dom 𝑅1 )
3 1 2 syl ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → suc ( rank ‘ 𝐴 ) ∈ dom 𝑅1 )
4 r1funlim ⊢ ( Fun 𝑅1 ∧ Lim dom 𝑅1 )
5 4 simpri ⊢ Lim dom 𝑅1
6 limsuc ⊢ ( Lim dom 𝑅1 → ( ( rank ‘ 𝐴 ) ∈ dom 𝑅1 ↔ suc ( rank ‘ 𝐴 ) ∈ dom 𝑅1 ) )
7 5 6 ax-mp ⊢ ( ( rank ‘ 𝐴 ) ∈ dom 𝑅1 ↔ suc ( rank ‘ 𝐴 ) ∈ dom 𝑅1 )
8 3 7 sylibr ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( rank ‘ 𝐴 ) ∈ dom 𝑅1 )
9 rankvaln ⊢ ( ¬ 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( rank ‘ 𝐴 ) = ∅ )
10 limomss ⊢ ( Lim dom 𝑅1 → ω ⊆ dom 𝑅1 )
11 5 10 ax-mp ⊢ ω ⊆ dom 𝑅1
12 peano1 ⊢ ∅ ∈ ω
13 11 12 sselii ⊢ ∅ ∈ dom 𝑅1
14 9 13 eqeltrdi ⊢ ( ¬ 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( rank ‘ 𝐴 ) ∈ dom 𝑅1 )
15 8 14 pm2.61i ⊢ ( rank ‘ 𝐴 ) ∈ dom 𝑅1