noextendgt

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

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

Proof

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

Metamath Proof Explorer

Theorem noextendgt

Proof