Theorem 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	|- ( ( _Left ` A ) u. ( _Right ` A ) ) = ( _Old ` ( bday ` A ) )

Proof

Step	Hyp	Ref	Expression
1		leftval	|- ( _Left ` A ) = { x e. ( _Old ` ( bday ` A ) ) | x
2		rightval	|- ( _Right ` A ) = { x e. ( _Old ` ( bday ` A ) ) | A
3	1 2	uneq12i	|- ( ( _Left ` A ) u. ( _Right ` A ) ) = ( { x e. ( _Old ` ( bday ` A ) ) | x
4		unrab	|- ( { x e. ( _Old ` ( bday ` A ) ) | x
5	3 4	eqtri	|- ( ( _Left ` A ) u. ( _Right ` A ) ) = { x e. ( _Old ` ( bday ` A ) ) | ( x
6		oldirr	|- -. A e. ( _Old ` ( bday ` A ) )
7		eleq1	|- ( x = A -> ( x e. ( _Old ` ( bday ` A ) ) <-> A e. ( _Old ` ( bday ` A ) ) ) )
8	6 7	mtbiri	|- ( x = A -> -. x e. ( _Old ` ( bday ` A ) ) )
9	8	necon2ai	|- ( x e. ( _Old ` ( bday ` A ) ) -> x =/= A )
10	9	adantl	|- ( ( A e. No /\ x e. ( _Old ` ( bday ` A ) ) ) -> x =/= A )
11		oldno	|- ( x e. ( _Old ` ( bday ` A ) ) -> x e. No )
12		ltstrine	|- ( ( x e. No /\ A e. No ) -> ( x =/= A <-> ( x
13	12	ancoms	|- ( ( A e. No /\ x e. No ) -> ( x =/= A <-> ( x
14	11 13	sylan2	|- ( ( A e. No /\ x e. ( _Old ` ( bday ` A ) ) ) -> ( x =/= A <-> ( x
15	10 14	mpbid	|- ( ( A e. No /\ x e. ( _Old ` ( bday ` A ) ) ) -> ( x
16	15	rabeqcda	|- ( A e. No -> { x e. ( _Old ` ( bday ` A ) ) | ( x
17	5 16	eqtrid	|- ( A e. No -> ( ( _Left ` A ) u. ( _Right ` A ) ) = ( _Old ` ( bday ` A ) ) )
18		un0	|- ( (/) u. (/) ) = (/)
19		leftf	|- _Left : No --> ~P No
20	19	fdmi	|- dom _Left = No
21	20	eleq2i	|- ( A e. dom _Left <-> A e. No )
22		ndmfv	|- ( -. A e. dom _Left -> ( _Left ` A ) = (/) )
23	21 22	sylnbir	|- ( -. A e. No -> ( _Left ` A ) = (/) )
24		rightf	|- _Right : No --> ~P No
25	24	fdmi	|- dom _Right = No
26	25	eleq2i	|- ( A e. dom _Right <-> A e. No )
27		ndmfv	|- ( -. A e. dom _Right -> ( _Right ` A ) = (/) )
28	26 27	sylnbir	|- ( -. A e. No -> ( _Right ` A ) = (/) )
29	23 28	uneq12d	|- ( -. A e. No -> ( ( _Left ` A ) u. ( _Right ` A ) ) = ( (/) u. (/) ) )
30		bdaydm	|- dom bday = No
31	30	eleq2i	|- ( A e. dom bday <-> A e. No )
32		ndmfv	|- ( -. A e. dom bday -> ( bday ` A ) = (/) )
33	31 32	sylnbir	|- ( -. A e. No -> ( bday ` A ) = (/) )
34	33	fveq2d	|- ( -. A e. No -> ( _Old ` ( bday ` A ) ) = ( _Old ` (/) ) )
35		old0	|- ( _Old ` (/) ) = (/)
36	34 35	eqtrdi	|- ( -. A e. No -> ( _Old ` ( bday ` A ) ) = (/) )
37	18 29 36	3eqtr4a	|- ( -. A e. No -> ( ( _Left ` A ) u. ( _Right ` A ) ) = ( _Old ` ( bday ` A ) ) )
38	17 37	pm2.61i	|- ( ( _Left ` A ) u. ( _Right ` A ) ) = ( _Old ` ( bday ` A ) )