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		oldno	⊢ ( 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) → 𝑥 ∈ No )
12		ltstrine	⊢ ( ( 𝑥 ∈ No ∧ 𝐴 ∈ No ) → ( 𝑥 ≠ 𝐴 ↔ ( 𝑥 <s 𝐴 ∨ 𝐴 <s 𝑥 ) ) )
13	12	ancoms	⊢ ( ( 𝐴 ∈ No ∧ 𝑥 ∈ No ) → ( 𝑥 ≠ 𝐴 ↔ ( 𝑥 <s 𝐴 ∨ 𝐴 <s 𝑥 ) ) )
14	11 13	sylan2	⊢ ( ( 𝐴 ∈ No ∧ 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ) → ( 𝑥 ≠ 𝐴 ↔ ( 𝑥 <s 𝐴 ∨ 𝐴 <s 𝑥 ) ) )
15	10 14	mpbid	⊢ ( ( 𝐴 ∈ No ∧ 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ) → ( 𝑥 <s 𝐴 ∨ 𝐴 <s 𝑥 ) )
16	15	rabeqcda	⊢ ( 𝐴 ∈ No → { 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ∣ ( 𝑥 <s 𝐴 ∨ 𝐴 <s 𝑥 ) } = ( O ‘ ( bday ‘ 𝐴 ) ) )
17	5 16	eqtrid	⊢ ( 𝐴 ∈ No → ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) = ( O ‘ ( bday ‘ 𝐴 ) ) )
18		un0	⊢ ( ∅ ∪ ∅ ) = ∅
19		leftf	⊢ L : No ⟶ 𝒫 No
20	19	fdmi	⊢ dom L = No
21	20	eleq2i	⊢ ( 𝐴 ∈ dom L ↔ 𝐴 ∈ No )
22		ndmfv	⊢ ( ¬ 𝐴 ∈ dom L → ( L ‘ 𝐴 ) = ∅ )
23	21 22	sylnbir	⊢ ( ¬ 𝐴 ∈ No → ( L ‘ 𝐴 ) = ∅ )
24		rightf	⊢ R : No ⟶ 𝒫 No
25	24	fdmi	⊢ dom R = No
26	25	eleq2i	⊢ ( 𝐴 ∈ dom R ↔ 𝐴 ∈ No )
27		ndmfv	⊢ ( ¬ 𝐴 ∈ dom R → ( R ‘ 𝐴 ) = ∅ )
28	26 27	sylnbir	⊢ ( ¬ 𝐴 ∈ No → ( R ‘ 𝐴 ) = ∅ )
29	23 28	uneq12d	⊢ ( ¬ 𝐴 ∈ No → ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) = ( ∅ ∪ ∅ ) )
30		bdaydm	⊢ dom bday = No
31	30	eleq2i	⊢ ( 𝐴 ∈ dom bday ↔ 𝐴 ∈ No )
32		ndmfv	⊢ ( ¬ 𝐴 ∈ dom bday → ( bday ‘ 𝐴 ) = ∅ )
33	31 32	sylnbir	⊢ ( ¬ 𝐴 ∈ No → ( bday ‘ 𝐴 ) = ∅ )
34	33	fveq2d	⊢ ( ¬ 𝐴 ∈ No → ( O ‘ ( bday ‘ 𝐴 ) ) = ( O ‘ ∅ ) )
35		old0	⊢ ( O ‘ ∅ ) = ∅
36	34 35	eqtrdi	⊢ ( ¬ 𝐴 ∈ No → ( O ‘ ( bday ‘ 𝐴 ) ) = ∅ )
37	18 29 36	3eqtr4a	⊢ ( ¬ 𝐴 ∈ No → ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) = ( O ‘ ( bday ‘ 𝐴 ) ) )
38	17 37	pm2.61i	⊢ ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) = ( O ‘ ( bday ‘ 𝐴 ) )