lrold

Description: The union of the left and right options of a surreal make its old set. (Contributed by Scott Fenton, 9-Oct-2024)

		Ref	Expression
	Assertion	lrold	$⊢ L (A) \cup R (A) = Old (bday (A))$

Proof

Step	Hyp	Ref	Expression
1		leftval	$⊢ L (A) = \{x \in Old (bday (A)) \| x <_{s} A\}$
2		rightval	$⊢ R (A) = \{x \in Old (bday (A)) \| A <_{s} x\}$
3	1 2	uneq12i	$⊢ L (A) \cup R (A) = \{x \in Old (bday (A)) \| x <_{s} A\} \cup \{x \in Old (bday (A)) \| A <_{s} x\}$
4		unrab	$⊢ \{x \in Old (bday (A)) \| x <_{s} A\} \cup \{x \in Old (bday (A)) \| A <_{s} x\} = \{x \in Old (bday (A)) \| (x <_{s} A \lor A <_{s} x)\}$
5	3 4	eqtri	$⊢ L (A) \cup R (A) = \{x \in Old (bday (A)) \| (x <_{s} A \lor A <_{s} x)\}$
6		oldirr	$⊢ \neg A \in Old (bday (A))$
7		eleq1	$⊢ x = A \to (x \in Old (bday (A)) \leftrightarrow A \in Old (bday (A)))$
8	6 7	mtbiri	$⊢ x = A \to \neg x \in Old (bday (A))$
9	8	necon2ai	$⊢ x \in Old (bday (A)) \to x \neq A$
10	9	adantl	$⊢ (A \in No \land x \in Old (bday (A))) \to x \neq A$
11		oldssno	$⊢ Old (bday (A)) \subseteq No$
12	11	sseli	$⊢ x \in Old (bday (A)) \to x \in No$
13		slttrine	$⊢ (x \in No \land A \in No) \to (x \neq A \leftrightarrow (x <_{s} A \lor A <_{s} x))$
14	13	ancoms	$⊢ (A \in No \land x \in No) \to (x \neq A \leftrightarrow (x <_{s} A \lor A <_{s} x))$
15	12 14	sylan2	$⊢ (A \in No \land x \in Old (bday (A))) \to (x \neq A \leftrightarrow (x <_{s} A \lor A <_{s} x))$
16	10 15	mpbid	$⊢ (A \in No \land x \in Old (bday (A))) \to (x <_{s} A \lor A <_{s} x)$
17	16	rabeqcda	$⊢ A \in No \to \{x \in Old (bday (A)) \| (x <_{s} A \lor A <_{s} x)\} = Old (bday (A))$
18	5 17	eqtrid	$⊢ A \in No \to L (A) \cup R (A) = Old (bday (A))$
19		un0	$⊢ \emptyset \cup \emptyset = \emptyset$
20		leftf	$⊢ L : No ⟶ 𝒫 No$
21	20	fdmi	$⊢ dom L = No$
22	21	eleq2i	$⊢ A \in dom L \leftrightarrow A \in No$
23		ndmfv	$⊢ \neg A \in dom L \to L (A) = \emptyset$
24	22 23	sylnbir	$⊢ \neg A \in No \to L (A) = \emptyset$
25		rightf	$⊢ R : No ⟶ 𝒫 No$
26	25	fdmi	$⊢ dom R = No$
27	26	eleq2i	$⊢ A \in dom R \leftrightarrow A \in No$
28		ndmfv	$⊢ \neg A \in dom R \to R (A) = \emptyset$
29	27 28	sylnbir	$⊢ \neg A \in No \to R (A) = \emptyset$
30	24 29	uneq12d	$⊢ \neg A \in No \to L (A) \cup R (A) = \emptyset \cup \emptyset$
31		bdaydm	$⊢ dom bday = No$
32	31	eleq2i	$⊢ A \in dom bday \leftrightarrow A \in No$
33		ndmfv	$⊢ \neg A \in dom bday \to bday (A) = \emptyset$
34	32 33	sylnbir	$⊢ \neg A \in No \to bday (A) = \emptyset$
35	34	fveq2d	$⊢ \neg A \in No \to Old (bday (A)) = Old (\emptyset)$
36		old0	$⊢ Old (\emptyset) = \emptyset$
37	35 36	eqtrdi	$⊢ \neg A \in No \to Old (bday (A)) = \emptyset$
38	19 30 37	3eqtr4a	$⊢ \neg A \in No \to L (A) \cup R (A) = Old (bday (A))$
39	18 38	pm2.61i	$⊢ L (A) \cup R (A) = Old (bday (A))$

Metamath Proof Explorer

Theorem lrold

Proof