noextendlt

Description: Extending a surreal with a negative sign results in a smaller surreal. (Contributed by Scott Fenton, 22-Nov-2021)

		Ref	Expression
	Assertion	noextendlt	$⊢ A \in No \to (A \cup \{⟨dom A, 1_{𝑜}⟩\}) <_{s} A$

Proof

Step	Hyp	Ref	Expression
1		nofun	$⊢ A \in No \to Fun A$
2		funfn	$⊢ Fun A \leftrightarrow A Fn dom A$
3	1 2	sylib	$⊢ A \in No \to A Fn dom A$
4		nodmon	$⊢ A \in No \to dom A \in On$
5		1on	$⊢ 1_{𝑜} \in On$
6		fnsng	$⊢ (dom A \in On \land 1_{𝑜} \in On) \to \{⟨dom A, 1_{𝑜}⟩\} Fn \{dom A\}$
7	4 5 6	sylancl	$⊢ A \in No \to \{⟨dom A, 1_{𝑜}⟩\} Fn \{dom A\}$
8		nodmord	$⊢ A \in No \to Ord dom A$
9		ordirr	$⊢ Ord dom A \to \neg dom A \in dom A$
10	8 9	syl	$⊢ A \in No \to \neg dom A \in dom A$
11		disjsn	$⊢ dom A \cap \{dom A\} = \emptyset \leftrightarrow \neg dom A \in dom A$
12	10 11	sylibr	$⊢ A \in No \to dom A \cap \{dom A\} = \emptyset$
13		snidg	$⊢ dom A \in On \to dom A \in \{dom A\}$
14	4 13	syl	$⊢ A \in No \to dom A \in \{dom A\}$
15		fvun2	$⊢ (A Fn dom A \land \{⟨dom A, 1_{𝑜}⟩\} Fn \{dom A\} \land (dom A \cap \{dom A\} = \emptyset \land dom A \in \{dom A\})) \to (A \cup \{⟨dom A, 1_{𝑜}⟩\}) (dom A) = \{⟨dom A, 1_{𝑜}⟩\} (dom A)$
16	3 7 12 14 15	syl112anc	$⊢ A \in No \to (A \cup \{⟨dom A, 1_{𝑜}⟩\}) (dom A) = \{⟨dom A, 1_{𝑜}⟩\} (dom A)$
17		fvsng	$⊢ (dom A \in On \land 1_{𝑜} \in On) \to \{⟨dom A, 1_{𝑜}⟩\} (dom A) = 1_{𝑜}$
18	4 5 17	sylancl	$⊢ A \in No \to \{⟨dom A, 1_{𝑜}⟩\} (dom A) = 1_{𝑜}$
19	16 18	eqtrd	$⊢ A \in No \to (A \cup \{⟨dom A, 1_{𝑜}⟩\}) (dom A) = 1_{𝑜}$
20		ndmfv	$⊢ \neg dom A \in dom A \to A (dom A) = \emptyset$
21	10 20	syl	$⊢ A \in No \to A (dom A) = \emptyset$
22	19 21	jca	$⊢ A \in No \to ((A \cup \{⟨dom A, 1_{𝑜}⟩\}) (dom A) = 1_{𝑜} \land A (dom A) = \emptyset)$
23	22	3mix1d	$⊢ A \in No \to (((A \cup \{⟨dom A, 1_{𝑜}⟩\}) (dom A) = 1_{𝑜} \land A (dom A) = \emptyset) \lor ((A \cup \{⟨dom A, 1_{𝑜}⟩\}) (dom A) = 1_{𝑜} \land A (dom A) = 2_{𝑜}) \lor ((A \cup \{⟨dom A, 1_{𝑜}⟩\}) (dom A) = \emptyset \land A (dom A) = 2_{𝑜}))$
24		fvex	$⊢ (A \cup \{⟨dom A, 1_{𝑜}⟩\}) (dom A) \in V$
25		fvex	$⊢ A (dom A) \in V$
26	24 25	brtp	$⊢ (A \cup \{⟨dom A, 1_{𝑜}⟩\}) (dom A) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} A (dom A) \leftrightarrow (((A \cup \{⟨dom A, 1_{𝑜}⟩\}) (dom A) = 1_{𝑜} \land A (dom A) = \emptyset) \lor ((A \cup \{⟨dom A, 1_{𝑜}⟩\}) (dom A) = 1_{𝑜} \land A (dom A) = 2_{𝑜}) \lor ((A \cup \{⟨dom A, 1_{𝑜}⟩\}) (dom A) = \emptyset \land A (dom A) = 2_{𝑜}))$
27	23 26	sylibr	$⊢ A \in No \to (A \cup \{⟨dom A, 1_{𝑜}⟩\}) (dom A) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} A (dom A)$
28		necom	$⊢ (A \cup \{⟨dom A, 1_{𝑜}⟩\}) (x) \neq A (x) \leftrightarrow A (x) \neq (A \cup \{⟨dom A, 1_{𝑜}⟩\}) (x)$
29	28	rabbii	$⊢ \{x \in On \| (A \cup \{⟨dom A, 1_{𝑜}⟩\}) (x) \neq A (x)\} = \{x \in On \| A (x) \neq (A \cup \{⟨dom A, 1_{𝑜}⟩\}) (x)\}$
30	29	inteqi	$⊢ ⋂ \{x \in On \| (A \cup \{⟨dom A, 1_{𝑜}⟩\}) (x) \neq A (x)\} = ⋂ \{x \in On \| A (x) \neq (A \cup \{⟨dom A, 1_{𝑜}⟩\}) (x)\}$
31		1oex	$⊢ 1_{𝑜} \in V$
32	31	prid1	$⊢ 1_{𝑜} \in \{1_{𝑜}, 2_{𝑜}\}$
33	32	noextenddif	$⊢ A \in No \to ⋂ \{x \in On \| A (x) \neq (A \cup \{⟨dom A, 1_{𝑜}⟩\}) (x)\} = dom A$
34	30 33	syl5eq	$⊢ A \in No \to ⋂ \{x \in On \| (A \cup \{⟨dom A, 1_{𝑜}⟩\}) (x) \neq A (x)\} = dom A$
35	34	fveq2d	$⊢ A \in No \to (A \cup \{⟨dom A, 1_{𝑜}⟩\}) (⋂ \{x \in On \| (A \cup \{⟨dom A, 1_{𝑜}⟩\}) (x) \neq A (x)\}) = (A \cup \{⟨dom A, 1_{𝑜}⟩\}) (dom A)$
36	34	fveq2d	$⊢ A \in No \to A (⋂ \{x \in On \| (A \cup \{⟨dom A, 1_{𝑜}⟩\}) (x) \neq A (x)\}) = A (dom A)$
37	27 35 36	3brtr4d	$⊢ A \in No \to (A \cup \{⟨dom A, 1_{𝑜}⟩\}) (⋂ \{x \in On \| (A \cup \{⟨dom A, 1_{𝑜}⟩\}) (x) \neq A (x)\}) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} A (⋂ \{x \in On \| (A \cup \{⟨dom A, 1_{𝑜}⟩\}) (x) \neq A (x)\})$
38	32	noextend	$⊢ A \in No \to A \cup \{⟨dom A, 1_{𝑜}⟩\} \in No$
39		sltval2	$⊢ (A \cup \{⟨dom A, 1_{𝑜}⟩\} \in No \land A \in No) \to ((A \cup \{⟨dom A, 1_{𝑜}⟩\}) <_{s} A \leftrightarrow (A \cup \{⟨dom A, 1_{𝑜}⟩\}) (⋂ \{x \in On \| (A \cup \{⟨dom A, 1_{𝑜}⟩\}) (x) \neq A (x)\}) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} A (⋂ \{x \in On \| (A \cup \{⟨dom A, 1_{𝑜}⟩\}) (x) \neq A (x)\}))$
40	38 39	mpancom	$⊢ A \in No \to ((A \cup \{⟨dom A, 1_{𝑜}⟩\}) <_{s} A \leftrightarrow (A \cup \{⟨dom A, 1_{𝑜}⟩\}) (⋂ \{x \in On \| (A \cup \{⟨dom A, 1_{𝑜}⟩\}) (x) \neq A (x)\}) \{⟨1_{𝑜}, \emptyset⟩, ⟨1_{𝑜}, 2_{𝑜}⟩, ⟨\emptyset, 2_{𝑜}⟩\} A (⋂ \{x \in On \| (A \cup \{⟨dom A, 1_{𝑜}⟩\}) (x) \neq A (x)\}))$
41	37 40	mpbird	$⊢ A \in No \to (A \cup \{⟨dom A, 1_{𝑜}⟩\}) <_{s} A$

Metamath Proof Explorer

Theorem noextendlt

Proof