Metamath Proof Explorer

Theorem nofv

Description: The function value of a surreal is either a sign or the empty set. (Contributed by Scott Fenton, 22-Jun-2011)

Ref Expression
Assertion nofv ⊢ A ∈ No → A ⁡ X = ∅ ∨ A ⁡ X = 1 𝑜 ∨ A ⁡ X = 2 𝑜

Proof

Step Hyp Ref Expression
1 pm2.1 ⊢ ¬ X ∈ dom ⁡ A ∨ X ∈ dom ⁡ A
2 ndmfv ⊢ ¬ X ∈ dom ⁡ A → A ⁡ X = ∅
3 2 a1i ⊢ A ∈ No → ¬ X ∈ dom ⁡ A → A ⁡ X = ∅
4 nofun ⊢ A ∈ No → Fun ⁡ A
5 norn ⊢ A ∈ No → ran ⁡ A ⊆ 1 𝑜 2 𝑜
6 fvelrn ⊢ Fun ⁡ A ∧ X ∈ dom ⁡ A → A ⁡ X ∈ ran ⁡ A
7 ssel ⊢ ran ⁡ A ⊆ 1 𝑜 2 𝑜 → A ⁡ X ∈ ran ⁡ A → A ⁡ X ∈ 1 𝑜 2 𝑜
8 6 7 syl5com ⊢ Fun ⁡ A ∧ X ∈ dom ⁡ A → ran ⁡ A ⊆ 1 𝑜 2 𝑜 → A ⁡ X ∈ 1 𝑜 2 𝑜
9 8 impancom ⊢ Fun ⁡ A ∧ ran ⁡ A ⊆ 1 𝑜 2 𝑜 → X ∈ dom ⁡ A → A ⁡ X ∈ 1 𝑜 2 𝑜
10 1oex ⊢ 1 𝑜 ∈ V
11 2on ⊢ 2 𝑜 ∈ On
12 11 elexi ⊢ 2 𝑜 ∈ V
13 10 12 elpr2 ⊢ A ⁡ X ∈ 1 𝑜 2 𝑜 ↔ A ⁡ X = 1 𝑜 ∨ A ⁡ X = 2 𝑜
14 9 13 imbitrdi ⊢ Fun ⁡ A ∧ ran ⁡ A ⊆ 1 𝑜 2 𝑜 → X ∈ dom ⁡ A → A ⁡ X = 1 𝑜 ∨ A ⁡ X = 2 𝑜
15 4 5 14 syl2anc ⊢ A ∈ No → X ∈ dom ⁡ A → A ⁡ X = 1 𝑜 ∨ A ⁡ X = 2 𝑜
16 3 15 orim12d ⊢ A ∈ No → ¬ X ∈ dom ⁡ A ∨ X ∈ dom ⁡ A → A ⁡ X = ∅ ∨ A ⁡ X = 1 𝑜 ∨ A ⁡ X = 2 𝑜
17 1 16 mpi ⊢ A ∈ No → A ⁡ X = ∅ ∨ A ⁡ X = 1 𝑜 ∨ A ⁡ X = 2 𝑜
18 3orass ⊢ A ⁡ X = ∅ ∨ A ⁡ X = 1 𝑜 ∨ A ⁡ X = 2 𝑜 ↔ A ⁡ X = ∅ ∨ A ⁡ X = 1 𝑜 ∨ A ⁡ X = 2 𝑜
19 17 18 sylibr ⊢ A ∈ No → A ⁡ X = ∅ ∨ A ⁡ X = 1 𝑜 ∨ A ⁡ X = 2 𝑜