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	13 3	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 Ord dom A$
15		ordirr	$⊢ Ord dom A \to \neg dom A \in dom A$
16		ndmfv	$⊢ \neg dom A \in dom A \to A (dom A) = \emptyset$
17	14 15 16	3syl	$⊢ ((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$
18	17	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))$
19		eqcom	$⊢ \emptyset = B (dom A) \leftrightarrow B (dom A) = \emptyset$
20	18 19	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)$
21		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$
22		nofun	$⊢ B \in No \to Fun B$
23	21 22	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$
24		nosgnn0	$⊢ \neg \emptyset \in \{1_{𝑜}, 2_{𝑜}\}$
25		norn	$⊢ B \in No \to ran B \subseteq \{1_{𝑜}, 2_{𝑜}\}$
26	21 25	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_{𝑜}\}$
27	26	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_{𝑜}\})$
28	24 27	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$
29		funeldmb	$⊢ (Fun B \land \neg \emptyset \in ran B) \to (dom A \in dom B \leftrightarrow B (dom A) \neq \emptyset)$
30	23 28 29	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)$
31	30	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)$
32		nodmord	$⊢ B \in No \to Ord dom B$
33	32	3ad2ant2	$⊢ (A \in No \land B \in No \land A \neq B) \to Ord dom B$
34		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)$
35	33 34	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)$
36	35	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)$
37	36	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)$
38	31 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 (B (dom A) = \emptyset \to \neg ⋂ \{x \in On \| A (x) \neq B (x)\} \in dom B)$
39	20 38	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)$
40	12 39	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$
41		ndmfv	$⊢ \neg ⋂ \{x \in On \| A (x) \neq B (x)\} \in dom B \to B (⋂ \{x \in On \| A (x) \neq B (x)\}) = \emptyset$
42	40 41	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$
43	11 42	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)\})$
44	2 43	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)\}$
45		nosepon	$⊢ (A \in No \land B \in No \land A \neq B) \to ⋂ \{x \in On \| A (x) \neq B (x)\} \in On$
46		nodmon	$⊢ A \in No \to dom A \in On$
47	46	3ad2ant1	$⊢ (A \in No \land B \in No \land A \neq B) \to dom A \in On$
48		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)\})$
49	45 47 48	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)\})$
50	44 49	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