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 ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) = ( O ‘ ( bday ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		leftval	⊢ ( L ‘ 𝐴 ) = { 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ∣ 𝑥 <s 𝐴 }
2		rightval	⊢ ( R ‘ 𝐴 ) = { 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ∣ 𝐴 <s 𝑥 }
3	1 2	uneq12i	⊢ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) = ( { 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ∣ 𝑥 <s 𝐴 } ∪ { 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ∣ 𝐴 <s 𝑥 } )
4		unrab	⊢ ( { 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ∣ 𝑥 <s 𝐴 } ∪ { 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ∣ 𝐴 <s 𝑥 } ) = { 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ∣ ( 𝑥 <s 𝐴 ∨ 𝐴 <s 𝑥 ) }
5	3 4	eqtri	⊢ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) = { 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ∣ ( 𝑥 <s 𝐴 ∨ 𝐴 <s 𝑥 ) }
6		oldirr	⊢ ¬ 𝐴 ∈ ( O ‘ ( bday ‘ 𝐴 ) )
7		eleq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ↔ 𝐴 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ) )
8	6 7	mtbiri	⊢ ( 𝑥 = 𝐴 → ¬ 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) )
9	8	necon2ai	⊢ ( 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) → 𝑥 ≠ 𝐴 )
10	9	adantl	⊢ ( ( 𝐴 ∈ No ∧ 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ) → 𝑥 ≠ 𝐴 )
11		oldssno	⊢ ( O ‘ ( bday ‘ 𝐴 ) ) ⊆ No
12	11	sseli	⊢ ( 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) → 𝑥 ∈ No )
13		slttrine	⊢ ( ( 𝑥 ∈ No ∧ 𝐴 ∈ No ) → ( 𝑥 ≠ 𝐴 ↔ ( 𝑥 <s 𝐴 ∨ 𝐴 <s 𝑥 ) ) )
14	13	ancoms	⊢ ( ( 𝐴 ∈ No ∧ 𝑥 ∈ No ) → ( 𝑥 ≠ 𝐴 ↔ ( 𝑥 <s 𝐴 ∨ 𝐴 <s 𝑥 ) ) )
15	12 14	sylan2	⊢ ( ( 𝐴 ∈ No ∧ 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ) → ( 𝑥 ≠ 𝐴 ↔ ( 𝑥 <s 𝐴 ∨ 𝐴 <s 𝑥 ) ) )
16	10 15	mpbid	⊢ ( ( 𝐴 ∈ No ∧ 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ) → ( 𝑥 <s 𝐴 ∨ 𝐴 <s 𝑥 ) )
17	16	rabeqcda	⊢ ( 𝐴 ∈ No → { 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ∣ ( 𝑥 <s 𝐴 ∨ 𝐴 <s 𝑥 ) } = ( O ‘ ( bday ‘ 𝐴 ) ) )
18	5 17	syl5eq	⊢ ( 𝐴 ∈ No → ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) = ( O ‘ ( bday ‘ 𝐴 ) ) )
19		un0	⊢ ( ∅ ∪ ∅ ) = ∅
20		leftf	⊢ L : No ⟶ 𝒫 No
21	20	fdmi	⊢ dom L = No
22	21	eleq2i	⊢ ( 𝐴 ∈ dom L ↔ 𝐴 ∈ No )
23		ndmfv	⊢ ( ¬ 𝐴 ∈ dom L → ( L ‘ 𝐴 ) = ∅ )
24	22 23	sylnbir	⊢ ( ¬ 𝐴 ∈ No → ( L ‘ 𝐴 ) = ∅ )
25		rightf	⊢ R : No ⟶ 𝒫 No
26	25	fdmi	⊢ dom R = No
27	26	eleq2i	⊢ ( 𝐴 ∈ dom R ↔ 𝐴 ∈ No )
28		ndmfv	⊢ ( ¬ 𝐴 ∈ dom R → ( R ‘ 𝐴 ) = ∅ )
29	27 28	sylnbir	⊢ ( ¬ 𝐴 ∈ No → ( R ‘ 𝐴 ) = ∅ )
30	24 29	uneq12d	⊢ ( ¬ 𝐴 ∈ No → ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) = ( ∅ ∪ ∅ ) )
31		bdaydm	⊢ dom bday = No
32	31	eleq2i	⊢ ( 𝐴 ∈ dom bday ↔ 𝐴 ∈ No )
33		ndmfv	⊢ ( ¬ 𝐴 ∈ dom bday → ( bday ‘ 𝐴 ) = ∅ )
34	32 33	sylnbir	⊢ ( ¬ 𝐴 ∈ No → ( bday ‘ 𝐴 ) = ∅ )
35	34	fveq2d	⊢ ( ¬ 𝐴 ∈ No → ( O ‘ ( bday ‘ 𝐴 ) ) = ( O ‘ ∅ ) )
36		old0	⊢ ( O ‘ ∅ ) = ∅
37	35 36	eqtrdi	⊢ ( ¬ 𝐴 ∈ No → ( O ‘ ( bday ‘ 𝐴 ) ) = ∅ )
38	19 30 37	3eqtr4a	⊢ ( ¬ 𝐴 ∈ No → ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) = ( O ‘ ( bday ‘ 𝐴 ) ) )
39	18 38	pm2.61i	⊢ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) = ( O ‘ ( bday ‘ 𝐴 ) )