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 \in No \to (A (X) = \emptyset \lor A (X) = 1_{𝑜} \lor A (X) = 2_{𝑜})$

Proof

Step	Hyp	Ref	Expression
1		pm2.1	$⊢ (\neg X \in dom A \lor X \in dom A)$
2		ndmfv	$⊢ \neg X \in dom A \to A (X) = \emptyset$
3	2	a1i	$⊢ A \in No \to (\neg X \in dom A \to A (X) = \emptyset)$
4		nofun	$⊢ A \in No \to Fun A$
5		norn	$⊢ A \in No \to ran A \subseteq \{1_{𝑜}, 2_{𝑜}\}$
6		fvelrn	$⊢ (Fun A \land X \in dom A) \to A (X) \in ran A$
7		ssel	$⊢ ran A \subseteq \{1_{𝑜}, 2_{𝑜}\} \to (A (X) \in ran A \to A (X) \in \{1_{𝑜}, 2_{𝑜}\})$
8	6 7	syl5com	$⊢ (Fun A \land X \in dom A) \to (ran A \subseteq \{1_{𝑜}, 2_{𝑜}\} \to A (X) \in \{1_{𝑜}, 2_{𝑜}\})$
9	8	impancom	$⊢ (Fun A \land ran A \subseteq \{1_{𝑜}, 2_{𝑜}\}) \to (X \in dom A \to A (X) \in \{1_{𝑜}, 2_{𝑜}\})$
10		1oex	$⊢ 1_{𝑜} \in V$
11		2on	$⊢ 2_{𝑜} \in On$
12	11	elexi	$⊢ 2_{𝑜} \in V$
13	10 12	elpr2	$⊢ A (X) \in \{1_{𝑜}, 2_{𝑜}\} \leftrightarrow (A (X) = 1_{𝑜} \lor A (X) = 2_{𝑜})$
14	9 13	imbitrdi	$⊢ (Fun A \land ran A \subseteq \{1_{𝑜}, 2_{𝑜}\}) \to (X \in dom A \to (A (X) = 1_{𝑜} \lor A (X) = 2_{𝑜}))$
15	4 5 14	syl2anc	$⊢ A \in No \to (X \in dom A \to (A (X) = 1_{𝑜} \lor A (X) = 2_{𝑜}))$
16	3 15	orim12d	$⊢ A \in No \to ((\neg X \in dom A \lor X \in dom A) \to (A (X) = \emptyset \lor (A (X) = 1_{𝑜} \lor A (X) = 2_{𝑜})))$
17	1 16	mpi	$⊢ A \in No \to (A (X) = \emptyset \lor (A (X) = 1_{𝑜} \lor A (X) = 2_{𝑜}))$
18		3orass	$⊢ (A (X) = \emptyset \lor A (X) = 1_{𝑜} \lor A (X) = 2_{𝑜}) \leftrightarrow (A (X) = \emptyset \lor (A (X) = 1_{𝑜} \lor A (X) = 2_{𝑜}))$
19	17 18	sylibr	$⊢ A \in No \to (A (X) = \emptyset \lor A (X) = 1_{𝑜} \lor A (X) = 2_{𝑜})$