nosupinfsep

Description: Given two sets of surreals, a surreal W separates them iff its restriction to the maximum of dom S and dom T separates them. Corollary 4.4 of Lipparini p. 7. (Contributed by Scott Fenton, 9-Aug-2024)

	Ref	Expression
Hypotheses	nosupinfsep.1	$⊢ S = if (\exists x \in A \forall y \in A \neg x <_{s} y, (ι x \in A \| \forall y \in A \neg x <_{s} y) \cup \{⟨dom (ι x \in A \| \forall y \in A \neg x <_{s} y), 2_{𝑜}⟩\}, (g \in \{y \| \exists u \in A (y \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc y} = {v ↾}_{suc y}))\} ⟼ (ι x \| \exists u \in A (g \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc g} = {v ↾}_{suc g}) \land u (g) = x))))$
	nosupinfsep.2	$⊢ T = if (\exists x \in B \forall y \in B \neg y <_{s} x, (ι x \in B \| \forall y \in B \neg y <_{s} x) \cup \{⟨dom (ι x \in B \| \forall y \in B \neg y <_{s} x), 1_{𝑜}⟩\}, (g \in \{y \| \exists u \in B (y \in dom u \land \forall v \in B (\neg u <_{s} v \to {u ↾}_{suc y} = {v ↾}_{suc y}))\} ⟼ (ι x \| \exists u \in B (g \in dom u \land \forall v \in B (\neg u <_{s} v \to {u ↾}_{suc g} = {v ↾}_{suc g}) \land u (g) = x))))$
Assertion	nosupinfsep	$⊢ ((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V) \land W \in No) \to ((\forall a \in A a <_{s} W \land \forall b \in B W <_{s} b) \leftrightarrow (\forall a \in A a <_{s} ({W ↾}_{(dom S \cup dom T)}) \land \forall b \in B ({W ↾}_{(dom S \cup dom T)}) <_{s} b))$

Proof

Step	Hyp	Ref	Expression
1		nosupinfsep.1	$⊢ S = if (\exists x \in A \forall y \in A \neg x <_{s} y, (ι x \in A \| \forall y \in A \neg x <_{s} y) \cup \{⟨dom (ι x \in A \| \forall y \in A \neg x <_{s} y), 2_{𝑜}⟩\}, (g \in \{y \| \exists u \in A (y \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc y} = {v ↾}_{suc y}))\} ⟼ (ι x \| \exists u \in A (g \in dom u \land \forall v \in A (\neg v <_{s} u \to {u ↾}_{suc g} = {v ↾}_{suc g}) \land u (g) = x))))$
2		nosupinfsep.2	$⊢ T = if (\exists x \in B \forall y \in B \neg y <_{s} x, (ι x \in B \| \forall y \in B \neg y <_{s} x) \cup \{⟨dom (ι x \in B \| \forall y \in B \neg y <_{s} x), 1_{𝑜}⟩\}, (g \in \{y \| \exists u \in B (y \in dom u \land \forall v \in B (\neg u <_{s} v \to {u ↾}_{suc y} = {v ↾}_{suc y}))\} ⟼ (ι x \| \exists u \in B (g \in dom u \land \forall v \in B (\neg u <_{s} v \to {u ↾}_{suc g} = {v ↾}_{suc g}) \land u (g) = x))))$
3		ssun1	$⊢ dom S \subseteq dom S \cup dom T$
4		resabs1	$⊢ dom S \subseteq dom S \cup dom T \to {({W ↾}_{(dom S \cup dom T)}) ↾}_{dom S} = {W ↾}_{dom S}$
5	3 4	ax-mp	$⊢ {({W ↾}_{(dom S \cup dom T)}) ↾}_{dom S} = {W ↾}_{dom S}$
6	5	breq1i	$⊢ ({({W ↾}_{(dom S \cup dom T)}) ↾}_{dom S}) <_{s} S \leftrightarrow ({W ↾}_{dom S}) <_{s} S$
7	6	notbii	$⊢ \neg ({({W ↾}_{(dom S \cup dom T)}) ↾}_{dom S}) <_{s} S \leftrightarrow \neg ({W ↾}_{dom S}) <_{s} S$
8		ssun2	$⊢ dom T \subseteq dom S \cup dom T$
9		resabs1	$⊢ dom T \subseteq dom S \cup dom T \to {({W ↾}_{(dom S \cup dom T)}) ↾}_{dom T} = {W ↾}_{dom T}$
10	8 9	ax-mp	$⊢ {({W ↾}_{(dom S \cup dom T)}) ↾}_{dom T} = {W ↾}_{dom T}$
11	10	breq2i	$⊢ T <_{s} ({({W ↾}_{(dom S \cup dom T)}) ↾}_{dom T}) \leftrightarrow T <_{s} ({W ↾}_{dom T})$
12	11	notbii	$⊢ \neg T <_{s} ({({W ↾}_{(dom S \cup dom T)}) ↾}_{dom T}) \leftrightarrow \neg T <_{s} ({W ↾}_{dom T})$
13	7 12	anbi12i	$⊢ (\neg ({({W ↾}_{(dom S \cup dom T)}) ↾}_{dom S}) <_{s} S \land \neg T <_{s} ({({W ↾}_{(dom S \cup dom T)}) ↾}_{dom T})) \leftrightarrow (\neg ({W ↾}_{dom S}) <_{s} S \land \neg T <_{s} ({W ↾}_{dom T}))$
14	13	bicomi	$⊢ (\neg ({W ↾}_{dom S}) <_{s} S \land \neg T <_{s} ({W ↾}_{dom T})) \leftrightarrow (\neg ({({W ↾}_{(dom S \cup dom T)}) ↾}_{dom S}) <_{s} S \land \neg T <_{s} ({({W ↾}_{(dom S \cup dom T)}) ↾}_{dom T}))$
15	14	a1i	$⊢ ((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V) \land W \in No) \to ((\neg ({W ↾}_{dom S}) <_{s} S \land \neg T <_{s} ({W ↾}_{dom T})) \leftrightarrow (\neg ({({W ↾}_{(dom S \cup dom T)}) ↾}_{dom S}) <_{s} S \land \neg T <_{s} ({({W ↾}_{(dom S \cup dom T)}) ↾}_{dom T})))$
16		simp1l	$⊢ ((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V) \land W \in No) \to A \subseteq No$
17		simp1r	$⊢ ((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V) \land W \in No) \to A \in V$
18		simp3	$⊢ ((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V) \land W \in No) \to W \in No$
19	1	nosupbnd2	$⊢ (A \subseteq No \land A \in V \land W \in No) \to (\forall a \in A a <_{s} W \leftrightarrow \neg ({W ↾}_{dom S}) <_{s} S)$
20	16 17 18 19	syl3anc	$⊢ ((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V) \land W \in No) \to (\forall a \in A a <_{s} W \leftrightarrow \neg ({W ↾}_{dom S}) <_{s} S)$
21		simp2l	$⊢ ((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V) \land W \in No) \to B \subseteq No$
22		simp2r	$⊢ ((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V) \land W \in No) \to B \in V$
23	2	noinfbnd2	$⊢ (B \subseteq No \land B \in V \land W \in No) \to (\forall b \in B W <_{s} b \leftrightarrow \neg T <_{s} ({W ↾}_{dom T}))$
24	21 22 18 23	syl3anc	$⊢ ((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V) \land W \in No) \to (\forall b \in B W <_{s} b \leftrightarrow \neg T <_{s} ({W ↾}_{dom T}))$
25	20 24	anbi12d	$⊢ ((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V) \land W \in No) \to ((\forall a \in A a <_{s} W \land \forall b \in B W <_{s} b) \leftrightarrow (\neg ({W ↾}_{dom S}) <_{s} S \land \neg T <_{s} ({W ↾}_{dom T})))$
26	1	nosupno	$⊢ (A \subseteq No \land A \in V) \to S \in No$
27		nodmon	$⊢ S \in No \to dom S \in On$
28	26 27	syl	$⊢ (A \subseteq No \land A \in V) \to dom S \in On$
29	28	3ad2ant1	$⊢ ((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V) \land W \in No) \to dom S \in On$
30	2	noinfno	$⊢ (B \subseteq No \land B \in V) \to T \in No$
31		nodmon	$⊢ T \in No \to dom T \in On$
32	30 31	syl	$⊢ (B \subseteq No \land B \in V) \to dom T \in On$
33	32	3ad2ant2	$⊢ ((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V) \land W \in No) \to dom T \in On$
34		onun2	$⊢ (dom S \in On \land dom T \in On) \to dom S \cup dom T \in On$
35	29 33 34	syl2anc	$⊢ ((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V) \land W \in No) \to dom S \cup dom T \in On$
36		noreson	$⊢ (W \in No \land dom S \cup dom T \in On) \to {W ↾}_{(dom S \cup dom T)} \in No$
37	18 35 36	syl2anc	$⊢ ((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V) \land W \in No) \to {W ↾}_{(dom S \cup dom T)} \in No$
38	1	nosupbnd2	$⊢ (A \subseteq No \land A \in V \land {W ↾}_{(dom S \cup dom T)} \in No) \to (\forall a \in A a <_{s} ({W ↾}_{(dom S \cup dom T)}) \leftrightarrow \neg ({({W ↾}_{(dom S \cup dom T)}) ↾}_{dom S}) <_{s} S)$
39	16 17 37 38	syl3anc	$⊢ ((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V) \land W \in No) \to (\forall a \in A a <_{s} ({W ↾}_{(dom S \cup dom T)}) \leftrightarrow \neg ({({W ↾}_{(dom S \cup dom T)}) ↾}_{dom S}) <_{s} S)$
40	21 22 37	3jca	$⊢ ((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V) \land W \in No) \to (B \subseteq No \land B \in V \land {W ↾}_{(dom S \cup dom T)} \in No)$
41	2	noinfbnd2	$⊢ (B \subseteq No \land B \in V \land {W ↾}_{(dom S \cup dom T)} \in No) \to (\forall b \in B ({W ↾}_{(dom S \cup dom T)}) <_{s} b \leftrightarrow \neg T <_{s} ({({W ↾}_{(dom S \cup dom T)}) ↾}_{dom T}))$
42	40 41	syl	$⊢ ((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V) \land W \in No) \to (\forall b \in B ({W ↾}_{(dom S \cup dom T)}) <_{s} b \leftrightarrow \neg T <_{s} ({({W ↾}_{(dom S \cup dom T)}) ↾}_{dom T}))$
43	39 42	anbi12d	$⊢ ((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V) \land W \in No) \to ((\forall a \in A a <_{s} ({W ↾}_{(dom S \cup dom T)}) \land \forall b \in B ({W ↾}_{(dom S \cup dom T)}) <_{s} b) \leftrightarrow (\neg ({({W ↾}_{(dom S \cup dom T)}) ↾}_{dom S}) <_{s} S \land \neg T <_{s} ({({W ↾}_{(dom S \cup dom T)}) ↾}_{dom T})))$
44	15 25 43	3bitr4d	$⊢ ((A \subseteq No \land A \in V) \land (B \subseteq No \land B \in V) \land W \in No) \to ((\forall a \in A a <_{s} W \land \forall b \in B W <_{s} b) \leftrightarrow (\forall a \in A a <_{s} ({W ↾}_{(dom S \cup dom T)}) \land \forall b \in B ({W ↾}_{(dom S \cup dom T)}) <_{s} b))$

Metamath Proof Explorer

Theorem nosupinfsep

Proof