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		oldno	$⊢ x \in Old (bday (A)) \to x \in No$
12		ltstrine	$⊢ (x \in No \land A \in No) \to (x \neq A \leftrightarrow (x <_{s} A \lor A <_{s} x))$
13	12	ancoms	$⊢ (A \in No \land x \in No) \to (x \neq A \leftrightarrow (x <_{s} A \lor A <_{s} x))$
14	11 13	sylan2	$⊢ (A \in No \land x \in Old (bday (A))) \to (x \neq A \leftrightarrow (x <_{s} A \lor A <_{s} x))$
15	10 14	mpbid	$⊢ (A \in No \land x \in Old (bday (A))) \to (x <_{s} A \lor A <_{s} x)$
16	15	rabeqcda	$⊢ A \in No \to \{x \in Old (bday (A)) \| (x <_{s} A \lor A <_{s} x)\} = Old (bday (A))$
17	5 16	eqtrid	$⊢ A \in No \to L (A) \cup R (A) = Old (bday (A))$
18		un0	$⊢ \emptyset \cup \emptyset = \emptyset$
19		leftf	$⊢ L : No ⟶ 𝒫 No$
20	19	fdmi	$⊢ dom L = No$
21	20	eleq2i	$⊢ A \in dom L \leftrightarrow A \in No$
22		ndmfv	$⊢ \neg A \in dom L \to L (A) = \emptyset$
23	21 22	sylnbir	$⊢ \neg A \in No \to L (A) = \emptyset$
24		rightf	$⊢ R : No ⟶ 𝒫 No$
25	24	fdmi	$⊢ dom R = No$
26	25	eleq2i	$⊢ A \in dom R \leftrightarrow A \in No$
27		ndmfv	$⊢ \neg A \in dom R \to R (A) = \emptyset$
28	26 27	sylnbir	$⊢ \neg A \in No \to R (A) = \emptyset$
29	23 28	uneq12d	$⊢ \neg A \in No \to L (A) \cup R (A) = \emptyset \cup \emptyset$
30		bdaydm	$⊢ dom bday = No$
31	30	eleq2i	$⊢ A \in dom bday \leftrightarrow A \in No$
32		ndmfv	$⊢ \neg A \in dom bday \to bday (A) = \emptyset$
33	31 32	sylnbir	$⊢ \neg A \in No \to bday (A) = \emptyset$
34	33	fveq2d	$⊢ \neg A \in No \to Old (bday (A)) = Old (\emptyset)$
35		old0	$⊢ Old (\emptyset) = \emptyset$
36	34 35	eqtrdi	$⊢ \neg A \in No \to Old (bday (A)) = \emptyset$
37	18 29 36	3eqtr4a	$⊢ \neg A \in No \to L (A) \cup R (A) = Old (bday (A))$
38	17 37	pm2.61i	$⊢ L (A) \cup R (A) = Old (bday (A))$

Metamath Proof Explorer

Theorem lrold

Proof