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

Theorem nocvxmin 32422
Description: Given a nonempty convex class of surreals, there is a unique birthday-minimal element of that class. (Contributed by Scott Fenton, 30-Jun-2011.)
Assertion
Ref Expression
nocvxmin ((𝐴 ≠ ∅ ∧ 𝐴 No ∧ ∀𝑥𝐴𝑦𝐴𝑧 No ((𝑥 <s 𝑧𝑧 <s 𝑦) → 𝑧𝐴)) → ∃!𝑤𝐴 ( bday 𝑤) = ( bday 𝐴))
Distinct variable group:   𝑤,𝐴,𝑥,𝑦,𝑧

Proof of Theorem nocvxmin
Dummy variable 𝑡 is distinct from all other variables.
StepHypRef Expression
1 imassrn 5718 . . . . . 6 ( bday 𝐴) ⊆ ran bday
2 bdayrn 32419 . . . . . 6 ran bday = On
31, 2sseqtri 3862 . . . . 5 ( bday 𝐴) ⊆ On
4 bdaydm 32418 . . . . . . . . . . 11 dom bday = No
54sseq2i 3855 . . . . . . . . . 10 (𝐴 ⊆ dom bday 𝐴 No )
6 bdayfun 32416 . . . . . . . . . . 11 Fun bday
7 funfvima2 6749 . . . . . . . . . . 11 ((Fun bday 𝐴 ⊆ dom bday ) → (𝑥𝐴 → ( bday 𝑥) ∈ ( bday 𝐴)))
86, 7mpan 681 . . . . . . . . . 10 (𝐴 ⊆ dom bday → (𝑥𝐴 → ( bday 𝑥) ∈ ( bday 𝐴)))
95, 8sylbir 227 . . . . . . . . 9 (𝐴 No → (𝑥𝐴 → ( bday 𝑥) ∈ ( bday 𝐴)))
10 elex2 3433 . . . . . . . . 9 (( bday 𝑥) ∈ ( bday 𝐴) → ∃𝑤 𝑤 ∈ ( bday 𝐴))
119, 10syl6 35 . . . . . . . 8 (𝐴 No → (𝑥𝐴 → ∃𝑤 𝑤 ∈ ( bday 𝐴)))
1211exlimdv 2032 . . . . . . 7 (𝐴 No → (∃𝑥 𝑥𝐴 → ∃𝑤 𝑤 ∈ ( bday 𝐴)))
13 n0 4160 . . . . . . 7 (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥𝐴)
14 n0 4160 . . . . . . 7 (( bday 𝐴) ≠ ∅ ↔ ∃𝑤 𝑤 ∈ ( bday 𝐴))
1512, 13, 143imtr4g 288 . . . . . 6 (𝐴 No → (𝐴 ≠ ∅ → ( bday 𝐴) ≠ ∅))
1615impcom 398 . . . . 5 ((𝐴 ≠ ∅ ∧ 𝐴 No ) → ( bday 𝐴) ≠ ∅)
17 onint 7256 . . . . 5 ((( bday 𝐴) ⊆ On ∧ ( bday 𝐴) ≠ ∅) → ( bday 𝐴) ∈ ( bday 𝐴))
183, 16, 17sylancr 581 . . . 4 ((𝐴 ≠ ∅ ∧ 𝐴 No ) → ( bday 𝐴) ∈ ( bday 𝐴))
19 bdayfn 32417 . . . . . 6 bday Fn No
20 fvelimab 6500 . . . . . 6 (( bday Fn No 𝐴 No ) → ( ( bday 𝐴) ∈ ( bday 𝐴) ↔ ∃𝑤𝐴 ( bday 𝑤) = ( bday 𝐴)))
2119, 20mpan 681 . . . . 5 (𝐴 No → ( ( bday 𝐴) ∈ ( bday 𝐴) ↔ ∃𝑤𝐴 ( bday 𝑤) = ( bday 𝐴)))
2221adantl 475 . . . 4 ((𝐴 ≠ ∅ ∧ 𝐴 No ) → ( ( bday 𝐴) ∈ ( bday 𝐴) ↔ ∃𝑤𝐴 ( bday 𝑤) = ( bday 𝐴)))
2318, 22mpbid 224 . . 3 ((𝐴 ≠ ∅ ∧ 𝐴 No ) → ∃𝑤𝐴 ( bday 𝑤) = ( bday 𝐴))
24233adant3 1166 . 2 ((𝐴 ≠ ∅ ∧ 𝐴 No ∧ ∀𝑥𝐴𝑦𝐴𝑧 No ((𝑥 <s 𝑧𝑧 <s 𝑦) → 𝑧𝐴)) → ∃𝑤𝐴 ( bday 𝑤) = ( bday 𝐴))
25 ssel 3821 . . . . . . . . 9 (𝐴 No → (𝑤𝐴𝑤 No ))
26 ssel 3821 . . . . . . . . 9 (𝐴 No → (𝑡𝐴𝑡 No ))
2725, 26anim12d 602 . . . . . . . 8 (𝐴 No → ((𝑤𝐴𝑡𝐴) → (𝑤 No 𝑡 No )))
2827imp 397 . . . . . . 7 ((𝐴 No ∧ (𝑤𝐴𝑡𝐴)) → (𝑤 No 𝑡 No ))
2928ad2ant2r 753 . . . . . 6 (((𝐴 No ∧ ∀𝑥𝐴𝑦𝐴𝑧 No ((𝑥 <s 𝑧𝑧 <s 𝑦) → 𝑧𝐴)) ∧ ((𝑤𝐴𝑡𝐴) ∧ (( bday 𝑤) = ( bday 𝐴) ∧ ( bday 𝑡) = ( bday 𝐴)))) → (𝑤 No 𝑡 No ))
30 nocvxminlem 32421 . . . . . . 7 ((𝐴 No ∧ ∀𝑥𝐴𝑦𝐴𝑧 No ((𝑥 <s 𝑧𝑧 <s 𝑦) → 𝑧𝐴)) → (((𝑤𝐴𝑡𝐴) ∧ (( bday 𝑤) = ( bday 𝐴) ∧ ( bday 𝑡) = ( bday 𝐴))) → ¬ 𝑤 <s 𝑡))
3130imp 397 . . . . . 6 (((𝐴 No ∧ ∀𝑥𝐴𝑦𝐴𝑧 No ((𝑥 <s 𝑧𝑧 <s 𝑦) → 𝑧𝐴)) ∧ ((𝑤𝐴𝑡𝐴) ∧ (( bday 𝑤) = ( bday 𝐴) ∧ ( bday 𝑡) = ( bday 𝐴)))) → ¬ 𝑤 <s 𝑡)
32 ancom 454 . . . . . . . . 9 ((𝑤𝐴𝑡𝐴) ↔ (𝑡𝐴𝑤𝐴))
33 ancom 454 . . . . . . . . 9 ((( bday 𝑤) = ( bday 𝐴) ∧ ( bday 𝑡) = ( bday 𝐴)) ↔ (( bday 𝑡) = ( bday 𝐴) ∧ ( bday 𝑤) = ( bday 𝐴)))
3432, 33anbi12i 620 . . . . . . . 8 (((𝑤𝐴𝑡𝐴) ∧ (( bday 𝑤) = ( bday 𝐴) ∧ ( bday 𝑡) = ( bday 𝐴))) ↔ ((𝑡𝐴𝑤𝐴) ∧ (( bday 𝑡) = ( bday 𝐴) ∧ ( bday 𝑤) = ( bday 𝐴))))
35 nocvxminlem 32421 . . . . . . . 8 ((𝐴 No ∧ ∀𝑥𝐴𝑦𝐴𝑧 No ((𝑥 <s 𝑧𝑧 <s 𝑦) → 𝑧𝐴)) → (((𝑡𝐴𝑤𝐴) ∧ (( bday 𝑡) = ( bday 𝐴) ∧ ( bday 𝑤) = ( bday 𝐴))) → ¬ 𝑡 <s 𝑤))
3634, 35syl5bi 234 . . . . . . 7 ((𝐴 No ∧ ∀𝑥𝐴𝑦𝐴𝑧 No ((𝑥 <s 𝑧𝑧 <s 𝑦) → 𝑧𝐴)) → (((𝑤𝐴𝑡𝐴) ∧ (( bday 𝑤) = ( bday 𝐴) ∧ ( bday 𝑡) = ( bday 𝐴))) → ¬ 𝑡 <s 𝑤))
3736imp 397 . . . . . 6 (((𝐴 No ∧ ∀𝑥𝐴𝑦𝐴𝑧 No ((𝑥 <s 𝑧𝑧 <s 𝑦) → 𝑧𝐴)) ∧ ((𝑤𝐴𝑡𝐴) ∧ (( bday 𝑤) = ( bday 𝐴) ∧ ( bday 𝑡) = ( bday 𝐴)))) → ¬ 𝑡 <s 𝑤)
38 slttrieq2 32403 . . . . . . 7 ((𝑤 No 𝑡 No ) → (𝑤 = 𝑡 ↔ (¬ 𝑤 <s 𝑡 ∧ ¬ 𝑡 <s 𝑤)))
3938biimpar 471 . . . . . 6 (((𝑤 No 𝑡 No ) ∧ (¬ 𝑤 <s 𝑡 ∧ ¬ 𝑡 <s 𝑤)) → 𝑤 = 𝑡)
4029, 31, 37, 39syl12anc 870 . . . . 5 (((𝐴 No ∧ ∀𝑥𝐴𝑦𝐴𝑧 No ((𝑥 <s 𝑧𝑧 <s 𝑦) → 𝑧𝐴)) ∧ ((𝑤𝐴𝑡𝐴) ∧ (( bday 𝑤) = ( bday 𝐴) ∧ ( bday 𝑡) = ( bday 𝐴)))) → 𝑤 = 𝑡)
4140exp32 413 . . . 4 ((𝐴 No ∧ ∀𝑥𝐴𝑦𝐴𝑧 No ((𝑥 <s 𝑧𝑧 <s 𝑦) → 𝑧𝐴)) → ((𝑤𝐴𝑡𝐴) → ((( bday 𝑤) = ( bday 𝐴) ∧ ( bday 𝑡) = ( bday 𝐴)) → 𝑤 = 𝑡)))
4241ralrimivv 3179 . . 3 ((𝐴 No ∧ ∀𝑥𝐴𝑦𝐴𝑧 No ((𝑥 <s 𝑧𝑧 <s 𝑦) → 𝑧𝐴)) → ∀𝑤𝐴𝑡𝐴 ((( bday 𝑤) = ( bday 𝐴) ∧ ( bday 𝑡) = ( bday 𝐴)) → 𝑤 = 𝑡))
43423adant1 1164 . 2 ((𝐴 ≠ ∅ ∧ 𝐴 No ∧ ∀𝑥𝐴𝑦𝐴𝑧 No ((𝑥 <s 𝑧𝑧 <s 𝑦) → 𝑧𝐴)) → ∀𝑤𝐴𝑡𝐴 ((( bday 𝑤) = ( bday 𝐴) ∧ ( bday 𝑡) = ( bday 𝐴)) → 𝑤 = 𝑡))
44 fveqeq2 6442 . . 3 (𝑤 = 𝑡 → (( bday 𝑤) = ( bday 𝐴) ↔ ( bday 𝑡) = ( bday 𝐴)))
4544reu4 3625 . 2 (∃!𝑤𝐴 ( bday 𝑤) = ( bday 𝐴) ↔ (∃𝑤𝐴 ( bday 𝑤) = ( bday 𝐴) ∧ ∀𝑤𝐴𝑡𝐴 ((( bday 𝑤) = ( bday 𝐴) ∧ ( bday 𝑡) = ( bday 𝐴)) → 𝑤 = 𝑡)))
4624, 43, 45sylanbrc 578 1 ((𝐴 ≠ ∅ ∧ 𝐴 No ∧ ∀𝑥𝐴𝑦𝐴𝑧 No ((𝑥 <s 𝑧𝑧 <s 𝑦) → 𝑧𝐴)) → ∃!𝑤𝐴 ( bday 𝑤) = ( bday 𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wa 386  w3a 1111   = wceq 1656  wex 1878  wcel 2164  wne 2999  wral 3117  wrex 3118  ∃!wreu 3119  wss 3798  c0 4144   cint 4697   class class class wbr 4873  dom cdm 5342  ran crn 5343  cima 5345  Oncon0 5963  Fun wfun 6117   Fn wfn 6118  cfv 6123   No csur 32321   <s cslt 32322   bday cbday 32323
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-8 2166  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-13 2389  ax-ext 2803  ax-rep 4994  ax-sep 5005  ax-nul 5013  ax-pow 5065  ax-pr 5127  ax-un 7209
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-3or 1112  df-3an 1113  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ne 3000  df-ral 3122  df-rex 3123  df-reu 3124  df-rmo 3125  df-rab 3126  df-v 3416  df-sbc 3663  df-csb 3758  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-pss 3814  df-nul 4145  df-if 4307  df-pw 4380  df-sn 4398  df-pr 4400  df-tp 4402  df-op 4404  df-uni 4659  df-int 4698  df-iun 4742  df-br 4874  df-opab 4936  df-mpt 4953  df-tr 4976  df-id 5250  df-eprel 5255  df-po 5263  df-so 5264  df-fr 5301  df-we 5303  df-xp 5348  df-rel 5349  df-cnv 5350  df-co 5351  df-dm 5352  df-rn 5353  df-res 5354  df-ima 5355  df-ord 5966  df-on 5967  df-suc 5969  df-iota 6086  df-fun 6125  df-fn 6126  df-f 6127  df-f1 6128  df-fo 6129  df-f1o 6130  df-fv 6131  df-1o 7826  df-2o 7827  df-no 32324  df-slt 32325  df-bday 32326
This theorem is referenced by:  conway  32438
  Copyright terms: Public domain W3C validator