Mathbox for Scott Fenton < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  eqscut Structured version   Visualization version   GIF version

Theorem eqscut 33594
 Description: Condition for equality to a surreal cut. (Contributed by Scott Fenton, 8-Aug-2024.)
Assertion
Ref Expression
eqscut ((𝐿 <<s 𝑅𝑋 No ) → ((𝐿 |s 𝑅) = 𝑋 ↔ (𝐿 <<s {𝑋} ∧ {𝑋} <<s 𝑅 ∧ ( bday 𝑋) = ( bday “ {𝑦 No ∣ (𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅)}))))
Distinct variable groups:   𝑦,𝐿   𝑦,𝑅
Allowed substitution hint:   𝑋(𝑦)

Proof of Theorem eqscut
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 scutval 33589 . . . . 5 (𝐿 <<s 𝑅 → (𝐿 |s 𝑅) = (𝑥 ∈ {𝑦 No ∣ (𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅)} ( bday 𝑥) = ( bday “ {𝑦 No ∣ (𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅)})))
21adantr 484 . . . 4 ((𝐿 <<s 𝑅𝑋 No ) → (𝐿 |s 𝑅) = (𝑥 ∈ {𝑦 No ∣ (𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅)} ( bday 𝑥) = ( bday “ {𝑦 No ∣ (𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅)})))
3 sneq 4535 . . . . . . 7 (𝑥 = 𝑦 → {𝑥} = {𝑦})
43breq2d 5048 . . . . . 6 (𝑥 = 𝑦 → (𝐿 <<s {𝑥} ↔ 𝐿 <<s {𝑦}))
53breq1d 5046 . . . . . 6 (𝑥 = 𝑦 → ({𝑥} <<s 𝑅 ↔ {𝑦} <<s 𝑅))
64, 5anbi12d 633 . . . . 5 (𝑥 = 𝑦 → ((𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅) ↔ (𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅)))
76riotarab 33203 . . . 4 (𝑥 ∈ {𝑦 No ∣ (𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅)} ( bday 𝑥) = ( bday “ {𝑦 No ∣ (𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅)})) = (𝑥 No ((𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅) ∧ ( bday 𝑥) = ( bday “ {𝑦 No ∣ (𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅)})))
82, 7eqtrdi 2809 . . 3 ((𝐿 <<s 𝑅𝑋 No ) → (𝐿 |s 𝑅) = (𝑥 No ((𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅) ∧ ( bday 𝑥) = ( bday “ {𝑦 No ∣ (𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅)}))))
98eqeq1d 2760 . 2 ((𝐿 <<s 𝑅𝑋 No ) → ((𝐿 |s 𝑅) = 𝑋 ↔ (𝑥 No ((𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅) ∧ ( bday 𝑥) = ( bday “ {𝑦 No ∣ (𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅)}))) = 𝑋))
10 conway 33588 . . . 4 (𝐿 <<s 𝑅 → ∃!𝑥 ∈ {𝑦 No ∣ (𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅)} ( bday 𝑥) = ( bday “ {𝑦 No ∣ (𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅)}))
116reurab 33204 . . . 4 (∃!𝑥 ∈ {𝑦 No ∣ (𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅)} ( bday 𝑥) = ( bday “ {𝑦 No ∣ (𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅)}) ↔ ∃!𝑥 No ((𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅) ∧ ( bday 𝑥) = ( bday “ {𝑦 No ∣ (𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅)})))
1210, 11sylib 221 . . 3 (𝐿 <<s 𝑅 → ∃!𝑥 No ((𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅) ∧ ( bday 𝑥) = ( bday “ {𝑦 No ∣ (𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅)})))
13 df-3an 1086 . . . . . 6 ((𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅 ∧ ( bday 𝑥) = ( bday “ {𝑦 No ∣ (𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅)})) ↔ ((𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅) ∧ ( bday 𝑥) = ( bday “ {𝑦 No ∣ (𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅)})))
14 sneq 4535 . . . . . . . 8 (𝑥 = 𝑋 → {𝑥} = {𝑋})
1514breq2d 5048 . . . . . . 7 (𝑥 = 𝑋 → (𝐿 <<s {𝑥} ↔ 𝐿 <<s {𝑋}))
1614breq1d 5046 . . . . . . 7 (𝑥 = 𝑋 → ({𝑥} <<s 𝑅 ↔ {𝑋} <<s 𝑅))
17 fveqeq2 6672 . . . . . . 7 (𝑥 = 𝑋 → (( bday 𝑥) = ( bday “ {𝑦 No ∣ (𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅)}) ↔ ( bday 𝑋) = ( bday “ {𝑦 No ∣ (𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅)})))
1815, 16, 173anbi123d 1433 . . . . . 6 (𝑥 = 𝑋 → ((𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅 ∧ ( bday 𝑥) = ( bday “ {𝑦 No ∣ (𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅)})) ↔ (𝐿 <<s {𝑋} ∧ {𝑋} <<s 𝑅 ∧ ( bday 𝑋) = ( bday “ {𝑦 No ∣ (𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅)}))))
1913, 18bitr3id 288 . . . . 5 (𝑥 = 𝑋 → (((𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅) ∧ ( bday 𝑥) = ( bday “ {𝑦 No ∣ (𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅)})) ↔ (𝐿 <<s {𝑋} ∧ {𝑋} <<s 𝑅 ∧ ( bday 𝑋) = ( bday “ {𝑦 No ∣ (𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅)}))))
2019riota2 7139 . . . 4 ((𝑋 No ∧ ∃!𝑥 No ((𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅) ∧ ( bday 𝑥) = ( bday “ {𝑦 No ∣ (𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅)}))) → ((𝐿 <<s {𝑋} ∧ {𝑋} <<s 𝑅 ∧ ( bday 𝑋) = ( bday “ {𝑦 No ∣ (𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅)})) ↔ (𝑥 No ((𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅) ∧ ( bday 𝑥) = ( bday “ {𝑦 No ∣ (𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅)}))) = 𝑋))
2120ancoms 462 . . 3 ((∃!𝑥 No ((𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅) ∧ ( bday 𝑥) = ( bday “ {𝑦 No ∣ (𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅)})) ∧ 𝑋 No ) → ((𝐿 <<s {𝑋} ∧ {𝑋} <<s 𝑅 ∧ ( bday 𝑋) = ( bday “ {𝑦 No ∣ (𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅)})) ↔ (𝑥 No ((𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅) ∧ ( bday 𝑥) = ( bday “ {𝑦 No ∣ (𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅)}))) = 𝑋))
2212, 21sylan 583 . 2 ((𝐿 <<s 𝑅𝑋 No ) → ((𝐿 <<s {𝑋} ∧ {𝑋} <<s 𝑅 ∧ ( bday 𝑋) = ( bday “ {𝑦 No ∣ (𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅)})) ↔ (𝑥 No ((𝐿 <<s {𝑥} ∧ {𝑥} <<s 𝑅) ∧ ( bday 𝑥) = ( bday “ {𝑦 No ∣ (𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅)}))) = 𝑋))
239, 22bitr4d 285 1 ((𝐿 <<s 𝑅𝑋 No ) → ((𝐿 |s 𝑅) = 𝑋 ↔ (𝐿 <<s {𝑋} ∧ {𝑋} <<s 𝑅 ∧ ( bday 𝑋) = ( bday “ {𝑦 No ∣ (𝐿 <<s {𝑦} ∧ {𝑦} <<s 𝑅)}))))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111  ∃!wreu 3072  {crab 3074  {csn 4525  ∩ cint 4841   class class class wbr 5036   “ cima 5531  ‘cfv 6340  ℩crio 7113  (class class class)co 7156   No csur 33440   bday cbday 33442   <
 Copyright terms: Public domain W3C validator