noextendseq

Description: Extend a surreal by a sequence of ordinals. (Contributed by Scott Fenton, 30-Nov-2021)

		Ref	Expression
	Hypothesis	noextend.1	$⊢ X \in \{1_{𝑜}, 2_{𝑜}\}$
	Assertion	noextendseq	$⊢ (A \in No \land B \in On) \to A \cup ((B ∖ dom A) \times \{X\}) \in No$

Proof

Step	Hyp	Ref	Expression
1		noextend.1	$⊢ X \in \{1_{𝑜}, 2_{𝑜}\}$
2		nofun	$⊢ A \in No \to Fun A$
3		fnconstg	$⊢ X \in \{1_{𝑜}, 2_{𝑜}\} \to ((B ∖ dom A) \times \{X\}) Fn (B ∖ dom A)$
4		fnfun	$⊢ ((B ∖ dom A) \times \{X\}) Fn (B ∖ dom A) \to Fun ((B ∖ dom A) \times \{X\})$
5	1 3 4	mp2b	$⊢ Fun ((B ∖ dom A) \times \{X\})$
6		snnzg	$⊢ X \in \{1_{𝑜}, 2_{𝑜}\} \to \{X\} \neq \emptyset$
7		dmxp	$⊢ \{X\} \neq \emptyset \to dom ((B ∖ dom A) \times \{X\}) = B ∖ dom A$
8	1 6 7	mp2b	$⊢ dom ((B ∖ dom A) \times \{X\}) = B ∖ dom A$
9	8	ineq2i	$⊢ dom A \cap dom ((B ∖ dom A) \times \{X\}) = dom A \cap (B ∖ dom A)$
10		disjdif	$⊢ dom A \cap (B ∖ dom A) = \emptyset$
11	9 10	eqtri	$⊢ dom A \cap dom ((B ∖ dom A) \times \{X\}) = \emptyset$
12		funun	$⊢ ((Fun A \land Fun ((B ∖ dom A) \times \{X\})) \land dom A \cap dom ((B ∖ dom A) \times \{X\}) = \emptyset) \to Fun (A \cup ((B ∖ dom A) \times \{X\}))$
13	11 12	mpan2	$⊢ (Fun A \land Fun ((B ∖ dom A) \times \{X\})) \to Fun (A \cup ((B ∖ dom A) \times \{X\}))$
14	2 5 13	sylancl	$⊢ A \in No \to Fun (A \cup ((B ∖ dom A) \times \{X\}))$
15	14	adantr	$⊢ (A \in No \land B \in On) \to Fun (A \cup ((B ∖ dom A) \times \{X\}))$
16		dmun	$⊢ dom (A \cup ((B ∖ dom A) \times \{X\})) = dom A \cup dom ((B ∖ dom A) \times \{X\})$
17	8	uneq2i	$⊢ dom A \cup dom ((B ∖ dom A) \times \{X\}) = dom A \cup (B ∖ dom A)$
18	16 17	eqtri	$⊢ dom (A \cup ((B ∖ dom A) \times \{X\})) = dom A \cup (B ∖ dom A)$
19		nodmon	$⊢ A \in No \to dom A \in On$
20		undif	$⊢ dom A \subseteq B \leftrightarrow dom A \cup (B ∖ dom A) = B$
21		eleq1a	$⊢ B \in On \to (dom A \cup (B ∖ dom A) = B \to dom A \cup (B ∖ dom A) \in On)$
22	21	adantl	$⊢ (dom A \in On \land B \in On) \to (dom A \cup (B ∖ dom A) = B \to dom A \cup (B ∖ dom A) \in On)$
23	20 22	biimtrid	$⊢ (dom A \in On \land B \in On) \to (dom A \subseteq B \to dom A \cup (B ∖ dom A) \in On)$
24		ssdif0	$⊢ B \subseteq dom A \leftrightarrow B ∖ dom A = \emptyset$
25		uneq2	$⊢ B ∖ dom A = \emptyset \to dom A \cup (B ∖ dom A) = dom A \cup \emptyset$
26		un0	$⊢ dom A \cup \emptyset = dom A$
27	25 26	eqtrdi	$⊢ B ∖ dom A = \emptyset \to dom A \cup (B ∖ dom A) = dom A$
28	27	eleq1d	$⊢ B ∖ dom A = \emptyset \to (dom A \cup (B ∖ dom A) \in On \leftrightarrow dom A \in On)$
29	28	biimprcd	$⊢ dom A \in On \to (B ∖ dom A = \emptyset \to dom A \cup (B ∖ dom A) \in On)$
30	29	adantr	$⊢ (dom A \in On \land B \in On) \to (B ∖ dom A = \emptyset \to dom A \cup (B ∖ dom A) \in On)$
31	24 30	biimtrid	$⊢ (dom A \in On \land B \in On) \to (B \subseteq dom A \to dom A \cup (B ∖ dom A) \in On)$
32		eloni	$⊢ dom A \in On \to Ord dom A$
33		eloni	$⊢ B \in On \to Ord B$
34		ordtri2or2	$⊢ (Ord dom A \land Ord B) \to (dom A \subseteq B \lor B \subseteq dom A)$
35	32 33 34	syl2an	$⊢ (dom A \in On \land B \in On) \to (dom A \subseteq B \lor B \subseteq dom A)$
36	23 31 35	mpjaod	$⊢ (dom A \in On \land B \in On) \to dom A \cup (B ∖ dom A) \in On$
37	19 36	sylan	$⊢ (A \in No \land B \in On) \to dom A \cup (B ∖ dom A) \in On$
38	18 37	eqeltrid	$⊢ (A \in No \land B \in On) \to dom (A \cup ((B ∖ dom A) \times \{X\})) \in On$
39		rnun	$⊢ ran (A \cup ((B ∖ dom A) \times \{X\})) = ran A \cup ran ((B ∖ dom A) \times \{X\})$
40		norn	$⊢ A \in No \to ran A \subseteq \{1_{𝑜}, 2_{𝑜}\}$
41	40	adantr	$⊢ (A \in No \land B \in On) \to ran A \subseteq \{1_{𝑜}, 2_{𝑜}\}$
42		rnxpss	$⊢ ran ((B ∖ dom A) \times \{X\}) \subseteq \{X\}$
43		snssi	$⊢ X \in \{1_{𝑜}, 2_{𝑜}\} \to \{X\} \subseteq \{1_{𝑜}, 2_{𝑜}\}$
44	1 43	ax-mp	$⊢ \{X\} \subseteq \{1_{𝑜}, 2_{𝑜}\}$
45	42 44	sstri	$⊢ ran ((B ∖ dom A) \times \{X\}) \subseteq \{1_{𝑜}, 2_{𝑜}\}$
46		unss	$⊢ (ran A \subseteq \{1_{𝑜}, 2_{𝑜}\} \land ran ((B ∖ dom A) \times \{X\}) \subseteq \{1_{𝑜}, 2_{𝑜}\}) \leftrightarrow ran A \cup ran ((B ∖ dom A) \times \{X\}) \subseteq \{1_{𝑜}, 2_{𝑜}\}$
47	41 45 46	sylanblc	$⊢ (A \in No \land B \in On) \to ran A \cup ran ((B ∖ dom A) \times \{X\}) \subseteq \{1_{𝑜}, 2_{𝑜}\}$
48	39 47	eqsstrid	$⊢ (A \in No \land B \in On) \to ran (A \cup ((B ∖ dom A) \times \{X\})) \subseteq \{1_{𝑜}, 2_{𝑜}\}$
49		elno2	$⊢ A \cup ((B ∖ dom A) \times \{X\}) \in No \leftrightarrow (Fun (A \cup ((B ∖ dom A) \times \{X\})) \land dom (A \cup ((B ∖ dom A) \times \{X\})) \in On \land ran (A \cup ((B ∖ dom A) \times \{X\})) \subseteq \{1_{𝑜}, 2_{𝑜}\})$
50	15 38 48 49	syl3anbrc	$⊢ (A \in No \land B \in On) \to A \cup ((B ∖ dom A) \times \{X\}) \in No$

Metamath Proof Explorer

Theorem noextendseq

Proof