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 ∈ On A : 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 ∈ On A ↾ B : y ⟶ 1 𝑜 2 𝑜
6 2 3 5 syl2an ⊢ x ∈ On ∧ B ∈ On ∧ A : x ⟶ 1 𝑜 2 𝑜 → ∃ y ∈ On A ↾ B : y ⟶ 1 𝑜 2 𝑜
7 6 an32s ⊢ x ∈ On ∧ A : x ⟶ 1 𝑜 2 𝑜 ∧ B ∈ On → ∃ y ∈ On A ↾ B : y ⟶ 1 𝑜 2 𝑜
8 7 ex ⊢ x ∈ On ∧ A : x ⟶ 1 𝑜 2 𝑜 → B ∈ On → ∃ y ∈ On A ↾ B : y ⟶ 1 𝑜 2 𝑜
9 8 rexlimiva ⊢ ∃ x ∈ On A : x ⟶ 1 𝑜 2 𝑜 → B ∈ On → ∃ y ∈ On A ↾ B : y ⟶ 1 𝑜 2 𝑜
10 9 imp ⊢ ∃ x ∈ On A : x ⟶ 1 𝑜 2 𝑜 ∧ B ∈ On → ∃ y ∈ On A ↾ B : y ⟶ 1 𝑜 2 𝑜
11 1 10 sylanb ⊢ A ∈ No ∧ B ∈ On → ∃ y ∈ On A ↾ B : y ⟶ 1 𝑜 2 𝑜
12 elno ⊢ A ↾ B ∈ No ↔ ∃ y ∈ On A ↾ B : y ⟶ 1 𝑜 2 𝑜
13 11 12 sylibr ⊢ A ∈ No ∧ B ∈ On → A ↾ B ∈ No