Theorem lrold 28141

Description: The union of the left and right options of a surreal make its old set. (Contributed by Scott Fenton, 9-Oct-2024.)

Assertion

Ref	Expression
lrold	⊢ (( L ‘𝐴) ∪ ( R ‘𝐴)) = ( O ‘( bday ‘𝐴))

Proof of Theorem lrold

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		leftval 28093	. . . . 5 ⊢ ( L ‘𝐴) = {𝑥 ∈ ( O ‘( bday ‘𝐴)) ∣ 𝑥 <s 𝐴}
2		rightval 28094	. . . . 5 ⊢ ( R ‘𝐴) = {𝑥 ∈ ( O ‘( bday ‘𝐴)) ∣ 𝐴 <s 𝑥}
3	1, 2	uneq12i 4120	. . . 4 ⊢ (( L ‘𝐴) ∪ ( R ‘𝐴)) = ({𝑥 ∈ ( O ‘( bday ‘𝐴)) ∣ 𝑥 <s 𝐴} ∪ {𝑥 ∈ ( O ‘( bday ‘𝐴)) ∣ 𝐴 <s 𝑥})
4		unrab 4268	. . . 4 ⊢ ({𝑥 ∈ ( O ‘( bday ‘𝐴)) ∣ 𝑥 <s 𝐴} ∪ {𝑥 ∈ ( O ‘( bday ‘𝐴)) ∣ 𝐴 <s 𝑥}) = {𝑥 ∈ ( O ‘( bday ‘𝐴)) ∣ (𝑥 <s 𝐴 ∨ 𝐴 <s 𝑥)}
5	3, 4	eqtri 2788	. . 3 ⊢ (( L ‘𝐴) ∪ ( R ‘𝐴)) = {𝑥 ∈ ( O ‘( bday ‘𝐴)) ∣ (𝑥 <s 𝐴 ∨ 𝐴 <s 𝑥)}
6		oldirr 28134	. . . . . . . 8 ⊢ ¬ 𝐴 ∈ ( O ‘( bday ‘𝐴))
7		eleq1 2853	. . . . . . . 8 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ ( O ‘( bday ‘𝐴)) ↔ 𝐴 ∈ ( O ‘( bday ‘𝐴))))
8	6, 7	mtbiri 330	. . . . . . 7 ⊢ (𝑥 = 𝐴 → ¬ 𝑥 ∈ ( O ‘( bday ‘𝐴)))
9	8	necon2ai 2989	. . . . . 6 ⊢ (𝑥 ∈ ( O ‘( bday ‘𝐴)) → 𝑥 ≠ 𝐴)
10	9	adantl 487	. . . . 5 ⊢ ((𝐴 ∈ No ∧ 𝑥 ∈ ( O ‘( bday ‘𝐴))) → 𝑥 ≠ 𝐴)
11		oldno 28088	. . . . . 6 ⊢ (𝑥 ∈ ( O ‘( bday ‘𝐴)) → 𝑥 ∈ No )
12		ltstrine 27966	. . . . . . 7 ⊢ ((𝑥 ∈ No ∧ 𝐴 ∈ No ) → (𝑥 ≠ 𝐴 ↔ (𝑥 <s 𝐴 ∨ 𝐴 <s 𝑥)))
13	12	ancoms 464	. . . . . 6 ⊢ ((𝐴 ∈ No ∧ 𝑥 ∈ No ) → (𝑥 ≠ 𝐴 ↔ (𝑥 <s 𝐴 ∨ 𝐴 <s 𝑥)))
14	11, 13	sylan2 605	. . . . 5 ⊢ ((𝐴 ∈ No ∧ 𝑥 ∈ ( O ‘( bday ‘𝐴))) → (𝑥 ≠ 𝐴 ↔ (𝑥 <s 𝐴 ∨ 𝐴 <s 𝑥)))
15	10, 14	mpbid 235	. . . 4 ⊢ ((𝐴 ∈ No ∧ 𝑥 ∈ ( O ‘( bday ‘𝐴))) → (𝑥 <s 𝐴 ∨ 𝐴 <s 𝑥))
16	15	rabeqcda 3429	. . 3 ⊢ (𝐴 ∈ No → {𝑥 ∈ ( O ‘( bday ‘𝐴)) ∣ (𝑥 <s 𝐴 ∨ 𝐴 <s 𝑥)} = ( O ‘( bday ‘𝐴)))
17	5, 16	eqtrid 2812	. 2 ⊢ (𝐴 ∈ No → (( L ‘𝐴) ∪ ( R ‘𝐴)) = ( O ‘( bday ‘𝐴)))
18		un0 4351	. . 3 ⊢ (∅ ∪ ∅) = ∅
19		leftf 28099	. . . . . . 7 ⊢ L : No ⟶𝒫 No
20	19	fdmi 6721	. . . . . 6 ⊢ dom L = No
21	20	eleq2i 2857	. . . . 5 ⊢ (𝐴 ∈ dom L ↔ 𝐴 ∈ No )
22		ndmfv 6917	. . . . 5 ⊢ (¬ 𝐴 ∈ dom L → ( L ‘𝐴) = ∅)
23	21, 22	sylnbir 334	. . . 4 ⊢ (¬ 𝐴 ∈ No → ( L ‘𝐴) = ∅)
24		rightf 28100	. . . . . . 7 ⊢ R : No ⟶𝒫 No
25	24	fdmi 6721	. . . . . 6 ⊢ dom R = No
26	25	eleq2i 2857	. . . . 5 ⊢ (𝐴 ∈ dom R ↔ 𝐴 ∈ No )
27		ndmfv 6917	. . . . 5 ⊢ (¬ 𝐴 ∈ dom R → ( R ‘𝐴) = ∅)
28	26, 27	sylnbir 334	. . . 4 ⊢ (¬ 𝐴 ∈ No → ( R ‘𝐴) = ∅)
29	23, 28	uneq12d 4123	. . 3 ⊢ (¬ 𝐴 ∈ No → (( L ‘𝐴) ∪ ( R ‘𝐴)) = (∅ ∪ ∅))
30		bdaydm 27993	. . . . . . 7 ⊢ dom bday = No
31	30	eleq2i 2857	. . . . . 6 ⊢ (𝐴 ∈ dom bday ↔ 𝐴 ∈ No )
32		ndmfv 6917	. . . . . 6 ⊢ (¬ 𝐴 ∈ dom bday → ( bday ‘𝐴) = ∅)
33	31, 32	sylnbir 334	. . . . 5 ⊢ (¬ 𝐴 ∈ No → ( bday ‘𝐴) = ∅)
34	33	fveq2d 6889	. . . 4 ⊢ (¬ 𝐴 ∈ No → ( O ‘( bday ‘𝐴)) = ( O ‘∅))
35		old0 28083	. . . 4 ⊢ ( O ‘∅) = ∅
36	34, 35	eqtrdi 2816	. . 3 ⊢ (¬ 𝐴 ∈ No → ( O ‘( bday ‘𝐴)) = ∅)
37	18, 29, 36	3eqtr4a 2826	. 2 ⊢ (¬ 𝐴 ∈ No → (( L ‘𝐴) ∪ ( R ‘𝐴)) = ( O ‘( bday ‘𝐴)))
38	17, 37	pm2.61i 184	1 ⊢ (( L ‘𝐴) ∪ ( R ‘𝐴)) = ( O ‘( bday ‘𝐴))

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209   ∧ wa 401   ∨ wo 861   = wceq 1570   ∈ wcel 2146   ≠ wne 2960  {crab 3418   ∪ cun 3904  ∅c0 4286  𝒫 cpw 4564   class class class wbr 5111  dom cdm 5663  ‘cfv 6540   No csur 27855   <s clts 27856   bday cbday 27857   O cold 28067   L cleft 28069   R cright 28070

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-rep 5240  ax-sep 5259  ax-nul 5271  ax-pow 5338  ax-pr 5406  ax-un 7742

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3082  df-rex 3092  df-rmo 3371  df-reu 3372  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-tp 4596  df-op 4598  df-uni 4875  df-int 4915  df-iun 4960  df-br 5112  df-opab 5176  df-mpt 5195  df-tr 5221  df-id 5558  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-we 5618  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-pred 6306  df-ord 6367  df-on 6368  df-suc 6370  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7376  df-ov 7422  df-oprab 7423  df-mpo 7424  df-2nd 7993  df-frecs 8284  df-wrecs 8315  df-recs 8364  df-1o 8459  df-2o 8460  df-no 27858  df-lts 27859  df-bday 27860  df-slts 28002  df-cuts 28004  df-made 28071  df-old 28072  df-left 28074  df-right 28075

This theorem is used by:  lruneq  28151  bdayiun  28159  lrrecval2  28184  addbdaylem  28261  negbdaylem  28300  onleft  28504  ltonold  28505  oncutlt  28508