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		r1dmlim	⊢ Lim dom 𝑅1
2		limord	⊢ ( Lim dom 𝑅1 → Ord dom 𝑅1 )
3		ordtr1	⊢ ( Ord dom 𝑅1 → ( ( 𝑥 ∈ 𝐴 ∧ 𝐴 ∈ dom 𝑅1 ) → 𝑥 ∈ dom 𝑅1 ) )
4	1 2 3	mp2b	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐴 ∈ dom 𝑅1 ) → 𝑥 ∈ dom 𝑅1 )
5	4	ancoms	⊢ ( ( 𝐴 ∈ dom 𝑅1 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ dom 𝑅1 )
6		rankonidlem	⊢ ( 𝑥 ∈ dom 𝑅1 → ( 𝑥 ∈ ∪ ( 𝑅1 “ On ) ∧ ( rank ‘ 𝑥 ) = 𝑥 ) )
7	5 6	syl	⊢ ( ( 𝐴 ∈ dom 𝑅1 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 ∈ ∪ ( 𝑅1 “ On ) ∧ ( rank ‘ 𝑥 ) = 𝑥 ) )
8	7	simprd	⊢ ( ( 𝐴 ∈ dom 𝑅1 ∧ 𝑥 ∈ 𝐴 ) → ( rank ‘ 𝑥 ) = 𝑥 )
9		simpr	⊢ ( ( 𝐴 ∈ dom 𝑅1 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
10	8 9	eqeltrd	⊢ ( ( 𝐴 ∈ dom 𝑅1 ∧ 𝑥 ∈ 𝐴 ) → ( rank ‘ 𝑥 ) ∈ 𝐴 )
11	7	simpld	⊢ ( ( 𝐴 ∈ dom 𝑅1 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ∪ ( 𝑅1 “ On ) )
12		simpl	⊢ ( ( 𝐴 ∈ dom 𝑅1 ∧ 𝑥 ∈ 𝐴 ) → 𝐴 ∈ dom 𝑅1 )
13		rankr1ag	⊢ ( ( 𝑥 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐴 ∈ dom 𝑅1 ) → ( 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ↔ ( rank ‘ 𝑥 ) ∈ 𝐴 ) )
14	11 12 13	syl2anc	⊢ ( ( 𝐴 ∈ dom 𝑅1 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ↔ ( rank ‘ 𝑥 ) ∈ 𝐴 ) )
15	10 14	mpbird	⊢ ( ( 𝐴 ∈ dom 𝑅1 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) )
16	15	ex	⊢ ( 𝐴 ∈ dom 𝑅1 → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ( 𝑅1 ‘ 𝐴 ) ) )
17	16	ssrdv	⊢ ( 𝐴 ∈ dom 𝑅1 → 𝐴 ⊆ ( 𝑅1 ‘ 𝐴 ) )