Theorem noreson

Description: The restriction of a surreal to an ordinal is still a surreal. (Contributed by Scott Fenton, 4-Sep-2011)

	Ref	Expression
Assertion	noreson	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ On ) → ( 𝐴 ↾ 𝐵 ) ∈ No )

Proof

Step	Hyp	Ref	Expression
1		elno	⊢ ( 𝐴 ∈ No ↔ ∃ 𝑥 ∈ On 𝐴 : 𝑥 ⟶ { 1o , 2o } )
2		onin	⊢ ( ( 𝑥 ∈ On ∧ 𝐵 ∈ On ) → ( 𝑥 ∩ 𝐵 ) ∈ On )
3		fresin	⊢ ( 𝐴 : 𝑥 ⟶ { 1o , 2o } → ( 𝐴 ↾ 𝐵 ) : ( 𝑥 ∩ 𝐵 ) ⟶ { 1o , 2o } )
4		feq2	⊢ ( 𝑦 = ( 𝑥 ∩ 𝐵 ) → ( ( 𝐴 ↾ 𝐵 ) : 𝑦 ⟶ { 1o , 2o } ↔ ( 𝐴 ↾ 𝐵 ) : ( 𝑥 ∩ 𝐵 ) ⟶ { 1o , 2o } ) )
5	4	rspcev	⊢ ( ( ( 𝑥 ∩ 𝐵 ) ∈ On ∧ ( 𝐴 ↾ 𝐵 ) : ( 𝑥 ∩ 𝐵 ) ⟶ { 1o , 2o } ) → ∃ 𝑦 ∈ On ( 𝐴 ↾ 𝐵 ) : 𝑦 ⟶ { 1o , 2o } )
6	2 3 5	syl2an	⊢ ( ( ( 𝑥 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐴 : 𝑥 ⟶ { 1o , 2o } ) → ∃ 𝑦 ∈ On ( 𝐴 ↾ 𝐵 ) : 𝑦 ⟶ { 1o , 2o } )
7	6	an32s	⊢ ( ( ( 𝑥 ∈ On ∧ 𝐴 : 𝑥 ⟶ { 1o , 2o } ) ∧ 𝐵 ∈ On ) → ∃ 𝑦 ∈ On ( 𝐴 ↾ 𝐵 ) : 𝑦 ⟶ { 1o , 2o } )
8	7	ex	⊢ ( ( 𝑥 ∈ On ∧ 𝐴 : 𝑥 ⟶ { 1o , 2o } ) → ( 𝐵 ∈ On → ∃ 𝑦 ∈ On ( 𝐴 ↾ 𝐵 ) : 𝑦 ⟶ { 1o , 2o } ) )
9	8	rexlimiva	⊢ ( ∃ 𝑥 ∈ On 𝐴 : 𝑥 ⟶ { 1o , 2o } → ( 𝐵 ∈ On → ∃ 𝑦 ∈ On ( 𝐴 ↾ 𝐵 ) : 𝑦 ⟶ { 1o , 2o } ) )
10	9	imp	⊢ ( ( ∃ 𝑥 ∈ On 𝐴 : 𝑥 ⟶ { 1o , 2o } ∧ 𝐵 ∈ On ) → ∃ 𝑦 ∈ On ( 𝐴 ↾ 𝐵 ) : 𝑦 ⟶ { 1o , 2o } )
11	1 10	sylanb	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ On ) → ∃ 𝑦 ∈ On ( 𝐴 ↾ 𝐵 ) : 𝑦 ⟶ { 1o , 2o } )
12		elno	⊢ ( ( 𝐴 ↾ 𝐵 ) ∈ No ↔ ∃ 𝑦 ∈ On ( 𝐴 ↾ 𝐵 ) : 𝑦 ⟶ { 1o , 2o } )
13	11 12	sylibr	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ On ) → ( 𝐴 ↾ 𝐵 ) ∈ No )