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

Metamath Proof Explorer

Theorem onssr1

Description: Initial segments of the ordinals are contained in initial segments of the cumulative hierarchy. (Contributed by FL, 20-Apr-2011) (Revised by Mario Carneiro, 17-Nov-2014)

Ref Expression
Assertion onssr1 ( 𝐴 ∈ dom 𝑅1 → 𝐴 ⊆ ( 𝑅1 ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 r1funlim ⊢ ( Fun 𝑅1 ∧ Lim dom 𝑅1 )
2 1 simpri ⊢ Lim dom 𝑅1
3 limord ⊢ ( Lim dom 𝑅1 → Ord dom 𝑅1 )
4 ordtr1 ⊢ ( Ord dom 𝑅1 → ( ( 𝑥 ∈ 𝐴 ∧ 𝐴 ∈ dom 𝑅1 ) → 𝑥 ∈ dom 𝑅1 ) )
5 2 3 4 mp2b ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐴 ∈ dom 𝑅1 ) → 𝑥 ∈ dom 𝑅1 )
6 5 ancoms ⊢ ( ( 𝐴 ∈ dom 𝑅1 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ dom 𝑅1 )
7 rankonidlem ⊢ ( 𝑥 ∈ dom 𝑅1 → ( 𝑥 ∈ ∪ ( 𝑅1 “ On ) ∧ ( rank ‘ 𝑥 ) = 𝑥 ) )
8 6 7 syl ⊢ ( ( 𝐴 ∈ dom 𝑅1 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 ∈ ∪ ( 𝑅1 “ On ) ∧ ( rank ‘ 𝑥 ) = 𝑥 ) )
9 8 simprd ⊢ ( ( 𝐴 ∈ dom 𝑅1 ∧ 𝑥 ∈ 𝐴 ) → ( rank ‘ 𝑥 ) = 𝑥 )
10 simpr ⊢ ( ( 𝐴 ∈ dom 𝑅1 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
11 9 10 eqeltrd ⊢ ( ( 𝐴 ∈ dom 𝑅1 ∧ 𝑥 ∈ 𝐴 ) → ( rank ‘ 𝑥 ) ∈ 𝐴 )
12 8 simpld ⊢ ( ( 𝐴 ∈ dom 𝑅1 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ∪ ( 𝑅1 “ On ) )
13 simpl ⊢ ( ( 𝐴 ∈ dom 𝑅1 ∧ 𝑥 ∈ 𝐴 ) → 𝐴 ∈ dom 𝑅1 )
14 rankr1ag ⊢ ( ( 𝑥 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐴 ∈ dom 𝑅1 ) → ( 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ↔ ( rank ‘ 𝑥 ) ∈ 𝐴 ) )
15 12 13 14 syl2anc ⊢ ( ( 𝐴 ∈ dom 𝑅1 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ↔ ( rank ‘ 𝑥 ) ∈ 𝐴 ) )
16 11 15 mpbird ⊢ ( ( 𝐴 ∈ dom 𝑅1 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) )
17 16 ex ⊢ ( 𝐴 ∈ dom 𝑅1 → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ) )
18 17 ssrdv ⊢ ( 𝐴 ∈ dom 𝑅1 → 𝐴 ⊆ ( 𝑅1 ‘ 𝐴 ) )