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, 12-Aug-2024)

Ref Expression
Assertion lrold ⊢ A ∈ No → L ⁡ A ∪ R ⁡ A = Old ⁡ bday ⁡ A

Proof

Step Hyp Ref Expression
1 leftval ⊢ A ∈ No → L ⁡ A = x ∈ Old ⁡ bday ⁡ A | x < s A
2 rightval ⊢ A ∈ No → R ⁡ A = x ∈ Old ⁡ bday ⁡ A | A < s x
3 1 2 uneq12d ⊢ A ∈ No → L ⁡ A ∪ R ⁡ A = x ∈ Old ⁡ bday ⁡ A | x < s A ∪ x ∈ Old ⁡ bday ⁡ A | A < s x
4 unrab ⊢ x ∈ Old ⁡ bday ⁡ A | x < s A ∪ x ∈ Old ⁡ bday ⁡ A | A < s x = x ∈ Old ⁡ bday ⁡ A | x < s A ∨ A < s x
5 3 4 eqtrdi ⊢ A ∈ No → L ⁡ A ∪ R ⁡ A = x ∈ Old ⁡ bday ⁡ A | x < s A ∨ A < s x
6 oldirr ⊢ ¬ A ∈ Old ⁡ bday ⁡ A
7 eleq1 ⊢ x = A → x ∈ Old ⁡ bday ⁡ A ↔ A ∈ Old ⁡ bday ⁡ A
8 6 7 mtbiri ⊢ x = A → ¬ x ∈ Old ⁡ bday ⁡ A
9 8 necon2ai ⊢ x ∈ Old ⁡ bday ⁡ A → x ≠ A
10 9 adantl ⊢ A ∈ No ∧ x ∈ Old ⁡ bday ⁡ A → x ≠ A
11 bdayelon ⊢ bday ⁡ A ∈ On
12 oldf ⊢ Old : On ⟶ 𝒫 No
13 12 ffvelrni ⊢ bday ⁡ A ∈ On → Old ⁡ bday ⁡ A ∈ 𝒫 No
14 13 elpwid ⊢ bday ⁡ A ∈ On → Old ⁡ bday ⁡ A ⊆ No
15 11 14 ax-mp ⊢ Old ⁡ bday ⁡ A ⊆ No
16 15 sseli ⊢ x ∈ Old ⁡ bday ⁡ A → x ∈ No
17 slttrine ⊢ x ∈ No ∧ A ∈ No → x ≠ A ↔ x < s A ∨ A < s x
18 17 ancoms ⊢ A ∈ No ∧ x ∈ No → x ≠ A ↔ x < s A ∨ A < s x
19 16 18 sylan2 ⊢ A ∈ No ∧ x ∈ Old ⁡ bday ⁡ A → x ≠ A ↔ x < s A ∨ A < s x
20 10 19 mpbid ⊢ A ∈ No ∧ x ∈ Old ⁡ bday ⁡ A → x < s A ∨ A < s x
21 20 rabeqcda ⊢ A ∈ No → x ∈ Old ⁡ bday ⁡ A | x < s A ∨ A < s x = Old ⁡ bday ⁡ A
22 5 21 eqtrd ⊢ A ∈ No → L ⁡ A ∪ R ⁡ A = Old ⁡ bday ⁡ A