Metamath Proof Explorer


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 eqtrid ( 𝐴 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 𝐴 ) )