Metamath Proof Explorer

Theorem nolt02olem

Description: Lemma for nolt02o . If A ( X ) is undefined with A surreal and X ordinal, then dom A C_ X . (Contributed by Scott Fenton, 6-Dec-2021)

		Ref	Expression
	Assertion	nolt02olem	$⊢ (A \in No \land X \in On \land A (X) = \emptyset) \to dom A \subseteq X$

Proof

Step	Hyp	Ref	Expression
1		nosgnn0	$⊢ \neg \emptyset \in \{1_{𝑜}, 2_{𝑜}\}$
2	1	a1i	$⊢ (A \in No \land X \in On \land A (X) = \emptyset) \to \neg \emptyset \in \{1_{𝑜}, 2_{𝑜}\}$
3		simpl3	$⊢ ((A \in No \land X \in On \land A (X) = \emptyset) \land X \in dom A) \to A (X) = \emptyset$
4		simpl1	$⊢ ((A \in No \land X \in On \land A (X) = \emptyset) \land X \in dom A) \to A \in No$
5		norn	$⊢ A \in No \to ran A \subseteq \{1_{𝑜}, 2_{𝑜}\}$
6	4 5	syl	$⊢ ((A \in No \land X \in On \land A (X) = \emptyset) \land X \in dom A) \to ran A \subseteq \{1_{𝑜}, 2_{𝑜}\}$
7		nofun	$⊢ A \in No \to Fun A$
8	7	3ad2ant1	$⊢ (A \in No \land X \in On \land A (X) = \emptyset) \to Fun A$
9		fvelrn	$⊢ (Fun A \land X \in dom A) \to A (X) \in ran A$
10	8 9	sylan	$⊢ ((A \in No \land X \in On \land A (X) = \emptyset) \land X \in dom A) \to A (X) \in ran A$
11	6 10	sseldd	$⊢ ((A \in No \land X \in On \land A (X) = \emptyset) \land X \in dom A) \to A (X) \in \{1_{𝑜}, 2_{𝑜}\}$
12	3 11	eqeltrrd	$⊢ ((A \in No \land X \in On \land A (X) = \emptyset) \land X \in dom A) \to \emptyset \in \{1_{𝑜}, 2_{𝑜}\}$
13	2 12	mtand	$⊢ (A \in No \land X \in On \land A (X) = \emptyset) \to \neg X \in dom A$
14		nodmon	$⊢ A \in No \to dom A \in On$
15	14	3ad2ant1	$⊢ (A \in No \land X \in On \land A (X) = \emptyset) \to dom A \in On$
16		simp2	$⊢ (A \in No \land X \in On \land A (X) = \emptyset) \to X \in On$
17		ontri1	$⊢ (dom A \in On \land X \in On) \to (dom A \subseteq X \leftrightarrow \neg X \in dom A)$
18	15 16 17	syl2anc	$⊢ (A \in No \land X \in On \land A (X) = \emptyset) \to (dom A \subseteq X \leftrightarrow \neg X \in dom A)$
19	13 18	mpbird	$⊢ (A \in No \land X \in On \land A (X) = \emptyset) \to dom A \subseteq X$