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		oldssno	|- ( _Old ` ( bday ` A ) ) C_ No
12	11	sseli	|- ( x e. ( _Old ` ( bday ` A ) ) -> x e. No )
13		slttrine	|- ( ( x e. No /\ A e. No ) -> ( x =/= A <-> ( x
14	13	ancoms	|- ( ( A e. No /\ x e. No ) -> ( x =/= A <-> ( x
15	12 14	sylan2	|- ( ( A e. No /\ x e. ( _Old ` ( bday ` A ) ) ) -> ( x =/= A <-> ( x
16	10 15	mpbid	|- ( ( A e. No /\ x e. ( _Old ` ( bday ` A ) ) ) -> ( x
17	16	rabeqcda	|- ( A e. No -> { x e. ( _Old ` ( bday ` A ) ) | ( x
18	5 17	eqtrid	|- ( A e. No -> ( ( _Left ` A ) u. ( _Right ` A ) ) = ( _Old ` ( bday ` A ) ) )
19		un0	|- ( (/) u. (/) ) = (/)
20		leftf	|- _Left : No --> ~P No
21	20	fdmi	|- dom _Left = No
22	21	eleq2i	|- ( A e. dom _Left <-> A e. No )
23		ndmfv	|- ( -. A e. dom _Left -> ( _Left ` A ) = (/) )
24	22 23	sylnbir	|- ( -. A e. No -> ( _Left ` A ) = (/) )
25		rightf	|- _Right : No --> ~P No
26	25	fdmi	|- dom _Right = No
27	26	eleq2i	|- ( A e. dom _Right <-> A e. No )
28		ndmfv	|- ( -. A e. dom _Right -> ( _Right ` A ) = (/) )
29	27 28	sylnbir	|- ( -. A e. No -> ( _Right ` A ) = (/) )
30	24 29	uneq12d	|- ( -. A e. No -> ( ( _Left ` A ) u. ( _Right ` A ) ) = ( (/) u. (/) ) )
31		bdaydm	|- dom bday = No
32	31	eleq2i	|- ( A e. dom bday <-> A e. No )
33		ndmfv	|- ( -. A e. dom bday -> ( bday ` A ) = (/) )
34	32 33	sylnbir	|- ( -. A e. No -> ( bday ` A ) = (/) )
35	34	fveq2d	|- ( -. A e. No -> ( _Old ` ( bday ` A ) ) = ( _Old ` (/) ) )
36		old0	|- ( _Old ` (/) ) = (/)
37	35 36	eqtrdi	|- ( -. A e. No -> ( _Old ` ( bday ` A ) ) = (/) )
38	19 30 37	3eqtr4a	|- ( -. A e. No -> ( ( _Left ` A ) u. ( _Right ` A ) ) = ( _Old ` ( bday ` A ) ) )
39	18 38	pm2.61i	|- ( ( _Left ` A ) u. ( _Right ` A ) ) = ( _Old ` ( bday ` A ) )