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	⊢ ( 𝐴 ∈ No → ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) = ( O ‘ ( bday ‘ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		leftval	⊢ ( 𝐴 ∈ No → ( L ‘ 𝐴 ) = { 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ∣ 𝑥 <s 𝐴 } )
2		rightval	⊢ ( 𝐴 ∈ No → ( R ‘ 𝐴 ) = { 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ∣ 𝐴 <s 𝑥 } )
3	1 2	uneq12d	⊢ ( 𝐴 ∈ No → ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) = ( { 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ∣ 𝑥 <s 𝐴 } ∪ { 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ∣ 𝐴 <s 𝑥 } ) )
4		unrab	⊢ ( { 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ∣ 𝑥 <s 𝐴 } ∪ { 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ∣ 𝐴 <s 𝑥 } ) = { 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ∣ ( 𝑥 <s 𝐴 ∨ 𝐴 <s 𝑥 ) }
5	3 4	eqtrdi	⊢ ( 𝐴 ∈ No → ( ( 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		bdayelon	⊢ ( bday ‘ 𝐴 ) ∈ On
12		oldf	⊢ O : On ⟶ 𝒫 No
13	12	ffvelrni	⊢ ( ( bday ‘ 𝐴 ) ∈ On → ( O ‘ ( bday ‘ 𝐴 ) ) ∈ 𝒫 No )
14	13	elpwid	⊢ ( ( bday ‘ 𝐴 ) ∈ On → ( O ‘ ( bday ‘ 𝐴 ) ) ⊆ No )
15	11 14	ax-mp	⊢ ( O ‘ ( bday ‘ 𝐴 ) ) ⊆ No
16	15	sseli	⊢ ( 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) → 𝑥 ∈ No )
17		slttrine	⊢ ( ( 𝑥 ∈ No ∧ 𝐴 ∈ No ) → ( 𝑥 ≠ 𝐴 ↔ ( 𝑥 <s 𝐴 ∨ 𝐴 <s 𝑥 ) ) )
18	17	ancoms	⊢ ( ( 𝐴 ∈ No ∧ 𝑥 ∈ No ) → ( 𝑥 ≠ 𝐴 ↔ ( 𝑥 <s 𝐴 ∨ 𝐴 <s 𝑥 ) ) )
19	16 18	sylan2	⊢ ( ( 𝐴 ∈ No ∧ 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ) → ( 𝑥 ≠ 𝐴 ↔ ( 𝑥 <s 𝐴 ∨ 𝐴 <s 𝑥 ) ) )
20	10 19	mpbid	⊢ ( ( 𝐴 ∈ No ∧ 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ) → ( 𝑥 <s 𝐴 ∨ 𝐴 <s 𝑥 ) )
21	20	rabeqcda	⊢ ( 𝐴 ∈ No → { 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ∣ ( 𝑥 <s 𝐴 ∨ 𝐴 <s 𝑥 ) } = ( O ‘ ( bday ‘ 𝐴 ) ) )
22	5 21	eqtrd	⊢ ( 𝐴 ∈ No → ( ( L ‘ 𝐴 ) ∪ ( R ‘ 𝐴 ) ) = ( O ‘ ( bday ‘ 𝐴 ) ) )