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

Metamath Proof Explorer

Theorem r1rankid

Description: Any set is a subset of the hierarchy of its rank. (Contributed by NM, 14-Oct-2003) (Revised by Mario Carneiro, 17-Nov-2014)

Ref Expression
Assertion r1rankid ( 𝐴 ∈ 𝑉 → 𝐴 ⊆ ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 elex ⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ V )
2 unir1 ⊢ ∪ ( 𝑅1 “ On ) = V
3 1 2 eleqtrrdi ⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ ∪ ( 𝑅1 “ On ) )
4 r1rankidb ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → 𝐴 ⊆ ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) )
5 3 4 syl ⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ⊆ ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) )