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 ⊢ A ∈ dom ⁡ R1 → A ⊆ R1 ⁡ A

Proof

Step Hyp Ref Expression
1 r1dmlim ⊢ Lim ⁡ dom ⁡ R1
2 limord ⊢ Lim ⁡ dom ⁡ R1 → Ord ⁡ dom ⁡ R1
3 ordtr1 ⊢ Ord ⁡ dom ⁡ R1 → x ∈ A ∧ A ∈ dom ⁡ R1 → x ∈ dom ⁡ R1
4 1 2 3 mp2b ⊢ x ∈ A ∧ A ∈ dom ⁡ R1 → x ∈ dom ⁡ R1
5 4 ancoms ⊢ A ∈ dom ⁡ R1 ∧ x ∈ A → x ∈ dom ⁡ R1
6 rankonidlem ⊢ x ∈ dom ⁡ R1 → x ∈ ⋃ R1 On ∧ rank ⁡ x = x
7 5 6 syl ⊢ A ∈ dom ⁡ R1 ∧ x ∈ A → x ∈ ⋃ R1 On ∧ rank ⁡ x = x
8 7 simprd ⊢ A ∈ dom ⁡ R1 ∧ x ∈ A → rank ⁡ x = x
9 simpr ⊢ A ∈ dom ⁡ R1 ∧ x ∈ A → x ∈ A
10 8 9 eqeltrd ⊢ A ∈ dom ⁡ R1 ∧ x ∈ A → rank ⁡ x ∈ A
11 7 simpld ⊢ A ∈ dom ⁡ R1 ∧ x ∈ A → x ∈ ⋃ R1 On
12 simpl ⊢ A ∈ dom ⁡ R1 ∧ x ∈ A → A ∈ dom ⁡ R1
13 rankr1ag ⊢ x ∈ ⋃ R1 On ∧ A ∈ dom ⁡ R1 → x ∈ R1 ⁡ A ↔ rank ⁡ x ∈ A
14 11 12 13 syl2anc ⊢ A ∈ dom ⁡ R1 ∧ x ∈ A → x ∈ R1 ⁡ A ↔ rank ⁡ x ∈ A
15 10 14 mpbird ⊢ A ∈ dom ⁡ R1 ∧ x ∈ A → x ∈ R1 ⁡ A
16 15 ex ⊢ A ∈ dom ⁡ R1 → x ∈ A → x ∈ R1 ⁡ A
17 16 ssrdv ⊢ A ∈ dom ⁡ R1 → A ⊆ R1 ⁡ A