nosepssdm

Description: Given two non-equal surreals, their separator is less-than or equal to the domain of one of them. Part of Lemma 2.1.1 of Lipparini p. 3. (Contributed by Scott Fenton, 6-Dec-2021)

		Ref	Expression
	Assertion	nosepssdm	$⊢ (A \in No \land B \in No \land A \neq B) \to ⋂ \{x \in On \| A (x) \neq B (x)\} \subseteq dom A$

Proof

Step	Hyp	Ref	Expression
1		nosepne	$⊢ (A \in No \land B \in No \land A \neq B) \to A (⋂ \{x \in On \| A (x) \neq B (x)\}) \neq B (⋂ \{x \in On \| A (x) \neq B (x)\})$
2	1	neneqd	$⊢ (A \in No \land B \in No \land A \neq B) \to \neg A (⋂ \{x \in On \| A (x) \neq B (x)\}) = B (⋂ \{x \in On \| A (x) \neq B (x)\})$
3		nodmord	$⊢ A \in No \to Ord dom A$
4	3	3ad2ant1	$⊢ (A \in No \land B \in No \land A \neq B) \to Ord dom A$
5		ordn2lp	$⊢ Ord dom A \to \neg (dom A \in ⋂ \{x \in On \| A (x) \neq B (x)\} \land ⋂ \{x \in On \| A (x) \neq B (x)\} \in dom A)$
6	4 5	syl	$⊢ (A \in No \land B \in No \land A \neq B) \to \neg (dom A \in ⋂ \{x \in On \| A (x) \neq B (x)\} \land ⋂ \{x \in On \| A (x) \neq B (x)\} \in dom A)$
7		imnan	$⊢ (dom A \in ⋂ \{x \in On \| A (x) \neq B (x)\} \to \neg ⋂ \{x \in On \| A (x) \neq B (x)\} \in dom A) \leftrightarrow \neg (dom A \in ⋂ \{x \in On \| A (x) \neq B (x)\} \land ⋂ \{x \in On \| A (x) \neq B (x)\} \in dom A)$
8	6 7	sylibr	$⊢ (A \in No \land B \in No \land A \neq B) \to (dom A \in ⋂ \{x \in On \| A (x) \neq B (x)\} \to \neg ⋂ \{x \in On \| A (x) \neq B (x)\} \in dom A)$
9	8	imp	$⊢ ((A \in No \land B \in No \land A \neq B) \land dom A \in ⋂ \{x \in On \| A (x) \neq B (x)\}) \to \neg ⋂ \{x \in On \| A (x) \neq B (x)\} \in dom A$
10		ndmfv	$⊢ \neg ⋂ \{x \in On \| A (x) \neq B (x)\} \in dom A \to A (⋂ \{x \in On \| A (x) \neq B (x)\}) = \emptyset$
11	9 10	syl	$⊢ ((A \in No \land B \in No \land A \neq B) \land dom A \in ⋂ \{x \in On \| A (x) \neq B (x)\}) \to A (⋂ \{x \in On \| A (x) \neq B (x)\}) = \emptyset$
12		nosepeq	$⊢ ((A \in No \land B \in No \land A \neq B) \land dom A \in ⋂ \{x \in On \| A (x) \neq B (x)\}) \to A (dom A) = B (dom A)$
13		simpl1	$⊢ ((A \in No \land B \in No \land A \neq B) \land dom A \in ⋂ \{x \in On \| A (x) \neq B (x)\}) \to A \in No$
14		ordirr	$⊢ Ord dom A \to \neg dom A \in dom A$
15		ndmfv	$⊢ \neg dom A \in dom A \to A (dom A) = \emptyset$
16	13 3 14 15	4syl	$⊢ ((A \in No \land B \in No \land A \neq B) \land dom A \in ⋂ \{x \in On \| A (x) \neq B (x)\}) \to A (dom A) = \emptyset$
17	16	eqeq1d	$⊢ ((A \in No \land B \in No \land A \neq B) \land dom A \in ⋂ \{x \in On \| A (x) \neq B (x)\}) \to (A (dom A) = B (dom A) \leftrightarrow \emptyset = B (dom A))$
18		eqcom	$⊢ \emptyset = B (dom A) \leftrightarrow B (dom A) = \emptyset$
19	17 18	bitrdi	$⊢ ((A \in No \land B \in No \land A \neq B) \land dom A \in ⋂ \{x \in On \| A (x) \neq B (x)\}) \to (A (dom A) = B (dom A) \leftrightarrow B (dom A) = \emptyset)$
20		simpl2	$⊢ ((A \in No \land B \in No \land A \neq B) \land dom A \in ⋂ \{x \in On \| A (x) \neq B (x)\}) \to B \in No$
21		nofun	$⊢ B \in No \to Fun B$
22	20 21	syl	$⊢ ((A \in No \land B \in No \land A \neq B) \land dom A \in ⋂ \{x \in On \| A (x) \neq B (x)\}) \to Fun B$
23		nosgnn0	$⊢ \neg \emptyset \in \{1_{𝑜}, 2_{𝑜}\}$
24		norn	$⊢ B \in No \to ran B \subseteq \{1_{𝑜}, 2_{𝑜}\}$
25	20 24	syl	$⊢ ((A \in No \land B \in No \land A \neq B) \land dom A \in ⋂ \{x \in On \| A (x) \neq B (x)\}) \to ran B \subseteq \{1_{𝑜}, 2_{𝑜}\}$
26	25	sseld	$⊢ ((A \in No \land B \in No \land A \neq B) \land dom A \in ⋂ \{x \in On \| A (x) \neq B (x)\}) \to (\emptyset \in ran B \to \emptyset \in \{1_{𝑜}, 2_{𝑜}\})$
27	23 26	mtoi	$⊢ ((A \in No \land B \in No \land A \neq B) \land dom A \in ⋂ \{x \in On \| A (x) \neq B (x)\}) \to \neg \emptyset \in ran B$
28		funeldmb	$⊢ (Fun B \land \neg \emptyset \in ran B) \to (dom A \in dom B \leftrightarrow B (dom A) \neq \emptyset)$
29	22 27 28	syl2anc	$⊢ ((A \in No \land B \in No \land A \neq B) \land dom A \in ⋂ \{x \in On \| A (x) \neq B (x)\}) \to (dom A \in dom B \leftrightarrow B (dom A) \neq \emptyset)$
30	29	necon2bbid	$⊢ ((A \in No \land B \in No \land A \neq B) \land dom A \in ⋂ \{x \in On \| A (x) \neq B (x)\}) \to (B (dom A) = \emptyset \leftrightarrow \neg dom A \in dom B)$
31		nodmord	$⊢ B \in No \to Ord dom B$
32	31	3ad2ant2	$⊢ (A \in No \land B \in No \land A \neq B) \to Ord dom B$
33		ordtr1	$⊢ Ord dom B \to ((dom A \in ⋂ \{x \in On \| A (x) \neq B (x)\} \land ⋂ \{x \in On \| A (x) \neq B (x)\} \in dom B) \to dom A \in dom B)$
34	32 33	syl	$⊢ (A \in No \land B \in No \land A \neq B) \to ((dom A \in ⋂ \{x \in On \| A (x) \neq B (x)\} \land ⋂ \{x \in On \| A (x) \neq B (x)\} \in dom B) \to dom A \in dom B)$
35	34	expdimp	$⊢ ((A \in No \land B \in No \land A \neq B) \land dom A \in ⋂ \{x \in On \| A (x) \neq B (x)\}) \to (⋂ \{x \in On \| A (x) \neq B (x)\} \in dom B \to dom A \in dom B)$
36	35	con3d	$⊢ ((A \in No \land B \in No \land A \neq B) \land dom A \in ⋂ \{x \in On \| A (x) \neq B (x)\}) \to (\neg dom A \in dom B \to \neg ⋂ \{x \in On \| A (x) \neq B (x)\} \in dom B)$
37	30 36	sylbid	$⊢ ((A \in No \land B \in No \land A \neq B) \land dom A \in ⋂ \{x \in On \| A (x) \neq B (x)\}) \to (B (dom A) = \emptyset \to \neg ⋂ \{x \in On \| A (x) \neq B (x)\} \in dom B)$
38	19 37	sylbid	$⊢ ((A \in No \land B \in No \land A \neq B) \land dom A \in ⋂ \{x \in On \| A (x) \neq B (x)\}) \to (A (dom A) = B (dom A) \to \neg ⋂ \{x \in On \| A (x) \neq B (x)\} \in dom B)$
39	12 38	mpd	$⊢ ((A \in No \land B \in No \land A \neq B) \land dom A \in ⋂ \{x \in On \| A (x) \neq B (x)\}) \to \neg ⋂ \{x \in On \| A (x) \neq B (x)\} \in dom B$
40		ndmfv	$⊢ \neg ⋂ \{x \in On \| A (x) \neq B (x)\} \in dom B \to B (⋂ \{x \in On \| A (x) \neq B (x)\}) = \emptyset$
41	39 40	syl	$⊢ ((A \in No \land B \in No \land A \neq B) \land dom A \in ⋂ \{x \in On \| A (x) \neq B (x)\}) \to B (⋂ \{x \in On \| A (x) \neq B (x)\}) = \emptyset$
42	11 41	eqtr4d	$⊢ ((A \in No \land B \in No \land A \neq B) \land dom A \in ⋂ \{x \in On \| A (x) \neq B (x)\}) \to A (⋂ \{x \in On \| A (x) \neq B (x)\}) = B (⋂ \{x \in On \| A (x) \neq B (x)\})$
43	2 42	mtand	$⊢ (A \in No \land B \in No \land A \neq B) \to \neg dom A \in ⋂ \{x \in On \| A (x) \neq B (x)\}$
44		nosepon	$⊢ (A \in No \land B \in No \land A \neq B) \to ⋂ \{x \in On \| A (x) \neq B (x)\} \in On$
45		nodmon	$⊢ A \in No \to dom A \in On$
46	45	3ad2ant1	$⊢ (A \in No \land B \in No \land A \neq B) \to dom A \in On$
47		ontri1	$⊢ (⋂ \{x \in On \| A (x) \neq B (x)\} \in On \land dom A \in On) \to (⋂ \{x \in On \| A (x) \neq B (x)\} \subseteq dom A \leftrightarrow \neg dom A \in ⋂ \{x \in On \| A (x) \neq B (x)\})$
48	44 46 47	syl2anc	$⊢ (A \in No \land B \in No \land A \neq B) \to (⋂ \{x \in On \| A (x) \neq B (x)\} \subseteq dom A \leftrightarrow \neg dom A \in ⋂ \{x \in On \| A (x) \neq B (x)\})$
49	43 48	mpbird	$⊢ (A \in No \land B \in No \land A \neq B) \to ⋂ \{x \in On \| A (x) \neq B (x)\} \subseteq dom A$

Metamath Proof Explorer

Theorem nosepssdm

Proof