Metamath Proof Explorer

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 ⊢A∈No∧B∈On→A↾B∈No

Proof

Step Hyp Ref Expression
1 elno ⊢A∈No↔∃x∈OnA:x⟶1𝑜2𝑜
2 onin ⊢x∈On∧B∈On→x∩B∈On
3 fresin ⊢A:x⟶1𝑜2𝑜→A↾B:x∩B⟶1𝑜2𝑜
4 feq2 ⊢y=x∩B→A↾B:y⟶1𝑜2𝑜↔A↾B:x∩B⟶1𝑜2𝑜
5 4 rspcev ⊢x∩B∈On∧A↾B:x∩B⟶1𝑜2𝑜→∃y∈OnA↾B:y⟶1𝑜2𝑜
6 2 3 5 syl2an ⊢x∈On∧B∈On∧A:x⟶1𝑜2𝑜→∃y∈OnA↾B:y⟶1𝑜2𝑜
7 6 an32s ⊢x∈On∧A:x⟶1𝑜2𝑜∧B∈On→∃y∈OnA↾B:y⟶1𝑜2𝑜
8 7 ex ⊢x∈On∧A:x⟶1𝑜2𝑜→B∈On→∃y∈OnA↾B:y⟶1𝑜2𝑜
9 8 rexlimiva ⊢∃x∈OnA:x⟶1𝑜2𝑜→B∈On→∃y∈OnA↾B:y⟶1𝑜2𝑜
10 9 imp ⊢∃x∈OnA:x⟶1𝑜2𝑜∧B∈On→∃y∈OnA↾B:y⟶1𝑜2𝑜
11 1 10 sylanb ⊢A∈No∧B∈On→∃y∈OnA↾B:y⟶1𝑜2𝑜
12 elno ⊢A↾B∈No↔∃y∈OnA↾B:y⟶1𝑜2𝑜
13 11 12 sylibr ⊢A∈No∧B∈On→A↾B∈No