Theorem lrold

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

	Ref	Expression
Assertion	lrold	|- ( A e. No -> ( ( _L ` A ) u. ( _R ` A ) ) = ( _Old ` ( bday ` A ) ) )

Proof

Step	Hyp	Ref	Expression
1		leftval	|- ( A e. No -> ( _L ` A ) = { x e. ( _Old ` ( bday ` A ) ) | x
2		rightval	|- ( A e. No -> ( _R ` A ) = { x e. ( _Old ` ( bday ` A ) ) | A
3	1 2	uneq12d	|- ( A e. No -> ( ( _L ` A ) u. ( _R ` A ) ) = ( { x e. ( _Old ` ( bday ` A ) ) | x
4		unrab	|- ( { x e. ( _Old ` ( bday ` A ) ) | x
5	3 4	eqtrdi	|- ( A e. No -> ( ( _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		bdayelon	|- ( bday ` A ) e. On
12		oldf	|- _Old : On --> ~P No
13	12	ffvelrni	|- ( ( bday ` A ) e. On -> ( _Old ` ( bday ` A ) ) e. ~P No )
14	13	elpwid	|- ( ( bday ` A ) e. On -> ( _Old ` ( bday ` A ) ) C_ No )
15	11 14	ax-mp	|- ( _Old ` ( bday ` A ) ) C_ No
16	15	sseli	|- ( x e. ( _Old ` ( bday ` A ) ) -> x e. No )
17		slttrine	|- ( ( x e. No /\ A e. No ) -> ( x =/= A <-> ( x
18	17	ancoms	|- ( ( A e. No /\ x e. No ) -> ( x =/= A <-> ( x
19	16 18	sylan2	|- ( ( A e. No /\ x e. ( _Old ` ( bday ` A ) ) ) -> ( x =/= A <-> ( x
20	10 19	mpbid	|- ( ( A e. No /\ x e. ( _Old ` ( bday ` A ) ) ) -> ( x
21	20	rabeqcda	|- ( A e. No -> { x e. ( _Old ` ( bday ` A ) ) | ( x
22	5 21	eqtrd	|- ( A e. No -> ( ( _L ` A ) u. ( _R ` A ) ) = ( _Old ` ( bday ` A ) ) )