noextend

Description: Extending a surreal by one sign value results in a new surreal. (Contributed by Scott Fenton, 22-Nov-2021)

		Ref	Expression
	Hypothesis	noextend.1	$⊢ X \in \{1_{𝑜}, 2_{𝑜}\}$
	Assertion	noextend	$⊢ A \in No \to A \cup \{⟨dom A, X⟩\} \in No$

Proof

Step	Hyp	Ref	Expression
1		noextend.1	$⊢ X \in \{1_{𝑜}, 2_{𝑜}\}$
2		nofun	$⊢ A \in No \to Fun A$
3		dmexg	$⊢ A \in No \to dom A \in V$
4		funsng	$⊢ (dom A \in V \land X \in \{1_{𝑜}, 2_{𝑜}\}) \to Fun \{⟨dom A, X⟩\}$
5	3 1 4	sylancl	$⊢ A \in No \to Fun \{⟨dom A, X⟩\}$
6	1	elexi	$⊢ X \in V$
7	6	dmsnop	$⊢ dom \{⟨dom A, X⟩\} = \{dom A\}$
8	7	ineq2i	$⊢ dom A \cap dom \{⟨dom A, X⟩\} = dom A \cap \{dom A\}$
9		nodmord	$⊢ A \in No \to Ord dom A$
10		ordirr	$⊢ Ord dom A \to \neg dom A \in dom A$
11	9 10	syl	$⊢ A \in No \to \neg dom A \in dom A$
12		disjsn	$⊢ dom A \cap \{dom A\} = \emptyset \leftrightarrow \neg dom A \in dom A$
13	11 12	sylibr	$⊢ A \in No \to dom A \cap \{dom A\} = \emptyset$
14	8 13	syl5eq	$⊢ A \in No \to dom A \cap dom \{⟨dom A, X⟩\} = \emptyset$
15		funun	$⊢ ((Fun A \land Fun \{⟨dom A, X⟩\}) \land dom A \cap dom \{⟨dom A, X⟩\} = \emptyset) \to Fun (A \cup \{⟨dom A, X⟩\})$
16	2 5 14 15	syl21anc	$⊢ A \in No \to Fun (A \cup \{⟨dom A, X⟩\})$
17	7	uneq2i	$⊢ dom A \cup dom \{⟨dom A, X⟩\} = dom A \cup \{dom A\}$
18		dmun	$⊢ dom (A \cup \{⟨dom A, X⟩\}) = dom A \cup dom \{⟨dom A, X⟩\}$
19		df-suc	$⊢ suc dom A = dom A \cup \{dom A\}$
20	17 18 19	3eqtr4i	$⊢ dom (A \cup \{⟨dom A, X⟩\}) = suc dom A$
21		nodmon	$⊢ A \in No \to dom A \in On$
22		suceloni	$⊢ dom A \in On \to suc dom A \in On$
23	21 22	syl	$⊢ A \in No \to suc dom A \in On$
24	20 23	eqeltrid	$⊢ A \in No \to dom (A \cup \{⟨dom A, X⟩\}) \in On$
25		rnun	$⊢ ran (A \cup \{⟨dom A, X⟩\}) = ran A \cup ran \{⟨dom A, X⟩\}$
26		rnsnopg	$⊢ dom A \in V \to ran \{⟨dom A, X⟩\} = \{X\}$
27	3 26	syl	$⊢ A \in No \to ran \{⟨dom A, X⟩\} = \{X\}$
28	27	uneq2d	$⊢ A \in No \to ran A \cup ran \{⟨dom A, X⟩\} = ran A \cup \{X\}$
29	25 28	syl5eq	$⊢ A \in No \to ran (A \cup \{⟨dom A, X⟩\}) = ran A \cup \{X\}$
30		norn	$⊢ A \in No \to ran A \subseteq \{1_{𝑜}, 2_{𝑜}\}$
31		snssi	$⊢ X \in \{1_{𝑜}, 2_{𝑜}\} \to \{X\} \subseteq \{1_{𝑜}, 2_{𝑜}\}$
32	1 31	mp1i	$⊢ A \in No \to \{X\} \subseteq \{1_{𝑜}, 2_{𝑜}\}$
33	30 32	unssd	$⊢ A \in No \to ran A \cup \{X\} \subseteq \{1_{𝑜}, 2_{𝑜}\}$
34	29 33	eqsstrd	$⊢ A \in No \to ran (A \cup \{⟨dom A, X⟩\}) \subseteq \{1_{𝑜}, 2_{𝑜}\}$
35		elno2	$⊢ A \cup \{⟨dom A, X⟩\} \in No \leftrightarrow (Fun (A \cup \{⟨dom A, X⟩\}) \land dom (A \cup \{⟨dom A, X⟩\}) \in On \land ran (A \cup \{⟨dom A, X⟩\}) \subseteq \{1_{𝑜}, 2_{𝑜}\})$
36	16 24 34 35	syl3anbrc	$⊢ A \in No \to A \cup \{⟨dom A, X⟩\} \in No$

Metamath Proof Explorer

Theorem noextend

Proof