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 ‘ 𝐴 ) )