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	|- ( ( _L ` A ) u. ( _R ` A ) ) = ( _Old ` ( bday ` A ) )

Proof

Step	Hyp	Ref	Expression
1		leftval	|- ( _L ` A ) = { x e. ( _Old ` ( bday ` A ) ) | x
2		rightval	|- ( _R ` A ) = { x e. ( _Old ` ( bday ` A ) ) | A
3	1 2	uneq12i	|- ( ( _L ` A ) u. ( _R ` A ) ) = ( { x e. ( _Old ` ( bday ` A ) ) | x
4		unrab	|- ( { x e. ( _Old ` ( bday ` A ) ) | x
5	3 4	eqtri	|- ( ( _L ` A ) u. ( _R ` 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	syl5eq	|- ( A e. No -> ( ( _L ` A ) u. ( _R ` A ) ) = ( _Old ` ( bday ` A ) ) )
19		un0	|- ( (/) u. (/) ) = (/)
20		leftf	|- _L : No --> ~P No
21	20	fdmi	|- dom _L = No
22	21	eleq2i	|- ( A e. dom _L <-> A e. No )
23		ndmfv	|- ( -. A e. dom _L -> ( _L ` A ) = (/) )
24	22 23	sylnbir	|- ( -. A e. No -> ( _L ` A ) = (/) )
25		rightf	|- _R : No --> ~P No
26	25	fdmi	|- dom _R = No
27	26	eleq2i	|- ( A e. dom _R <-> A e. No )
28		ndmfv	|- ( -. A e. dom _R -> ( _R ` A ) = (/) )
29	27 28	sylnbir	|- ( -. A e. No -> ( _R ` A ) = (/) )
30	24 29	uneq12d	|- ( -. A e. No -> ( ( _L ` A ) u. ( _R ` 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 -> ( ( _L ` A ) u. ( _R ` A ) ) = ( _Old ` ( bday ` A ) ) )
39	18 38	pm2.61i	|- ( ( _L ` A ) u. ( _R ` A ) ) = ( _Old ` ( bday ` A ) )