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

Theorem nocvxmin 31589
 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 5441 . . . . . 6 ( bday 𝐴) ⊆ ran bday
2 bdayrn 31575 . . . . . 6 ran bday = On
31, 2sseqtri 3621 . . . . 5 ( bday 𝐴) ⊆ On
4 bdaydm 31576 . . . . . . . . . . 11 dom bday = No
54sseq2i 3614 . . . . . . . . . 10 (𝐴 ⊆ dom bday 𝐴 No )
6 bdayfun 31574 . . . . . . . . . . 11 Fun bday
7 funfvima2 6453 . . . . . . . . . . 11 ((Fun bday 𝐴 ⊆ dom bday ) → (𝑥𝐴 → ( bday 𝑥) ∈ ( bday 𝐴)))
86, 7mpan 705 . . . . . . . . . 10 (𝐴 ⊆ dom bday → (𝑥𝐴 → ( bday 𝑥) ∈ ( bday 𝐴)))
95, 8sylbir 225 . . . . . . . . 9 (𝐴 No → (𝑥𝐴 → ( bday 𝑥) ∈ ( bday 𝐴)))
10 elex2 3205 . . . . . . . . 9 (( bday 𝑥) ∈ ( bday 𝐴) → ∃𝑤 𝑤 ∈ ( bday 𝐴))
119, 10syl6 35 . . . . . . . 8 (𝐴 No → (𝑥𝐴 → ∃𝑤 𝑤 ∈ ( bday 𝐴)))
1211exlimdv 1858 . . . . . . 7 (𝐴 No → (∃𝑥 𝑥𝐴 → ∃𝑤 𝑤 ∈ ( bday 𝐴)))
13 n0 3912 . . . . . . 7 (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥𝐴)
14 n0 3912 . . . . . . 7 (( bday 𝐴) ≠ ∅ ↔ ∃𝑤 𝑤 ∈ ( bday 𝐴))
1512, 13, 143imtr4g 285 . . . . . 6 (𝐴 No → (𝐴 ≠ ∅ → ( bday 𝐴) ≠ ∅))
1615impcom 446 . . . . 5 ((𝐴 ≠ ∅ ∧ 𝐴 No ) → ( bday 𝐴) ≠ ∅)
17 onint 6949 . . . . 5 ((( bday 𝐴) ⊆ On ∧ ( bday 𝐴) ≠ ∅) → ( bday 𝐴) ∈ ( bday 𝐴))
183, 16, 17sylancr 694 . . . 4 ((𝐴 ≠ ∅ ∧ 𝐴 No ) → ( bday 𝐴) ∈ ( bday 𝐴))
19 bdayfn 31577 . . . . . 6 bday Fn No
20 fvelimab 6215 . . . . . 6 (( bday Fn No 𝐴 No ) → ( ( bday 𝐴) ∈ ( bday 𝐴) ↔ ∃𝑤𝐴 ( bday 𝑤) = ( bday 𝐴)))
2119, 20mpan 705 . . . . 5 (𝐴 No → ( ( bday 𝐴) ∈ ( bday 𝐴) ↔ ∃𝑤𝐴 ( bday 𝑤) = ( bday 𝐴)))
2221adantl 482 . . . 4 ((𝐴 ≠ ∅ ∧ 𝐴 No ) → ( ( bday 𝐴) ∈ ( bday 𝐴) ↔ ∃𝑤𝐴 ( bday 𝑤) = ( bday 𝐴)))
2318, 22mpbid 222 . . 3 ((𝐴 ≠ ∅ ∧ 𝐴 No ) → ∃𝑤𝐴 ( bday 𝑤) = ( bday 𝐴))
24233adant3 1079 . 2 ((𝐴 ≠ ∅ ∧ 𝐴 No ∧ ∀𝑥𝐴𝑦𝐴𝑧 No ((𝑥 <s 𝑧𝑧 <s 𝑦) → 𝑧𝐴)) → ∃𝑤𝐴 ( bday 𝑤) = ( bday 𝐴))
25 ssel 3581 . . . . . . . . 9 (𝐴 No → (𝑤𝐴𝑤 No ))
26 ssel 3581 . . . . . . . . 9 (𝐴 No → (𝑡𝐴𝑡 No ))
2725, 26anim12d 585 . . . . . . . 8 (𝐴 No → ((𝑤𝐴𝑡𝐴) → (𝑤 No 𝑡 No )))
2827imp 445 . . . . . . 7 ((𝐴 No ∧ (𝑤𝐴𝑡𝐴)) → (𝑤 No 𝑡 No ))
2928ad2ant2r 782 . . . . . 6 (((𝐴 No ∧ ∀𝑥𝐴𝑦𝐴𝑧 No ((𝑥 <s 𝑧𝑧 <s 𝑦) → 𝑧𝐴)) ∧ ((𝑤𝐴𝑡𝐴) ∧ (( bday 𝑤) = ( bday 𝐴) ∧ ( bday 𝑡) = ( bday 𝐴)))) → (𝑤 No 𝑡 No ))
30 nocvxminlem 31588 . . . . . . 7 ((𝐴 No ∧ ∀𝑥𝐴𝑦𝐴𝑧 No ((𝑥 <s 𝑧𝑧 <s 𝑦) → 𝑧𝐴)) → (((𝑤𝐴𝑡𝐴) ∧ (( bday 𝑤) = ( bday 𝐴) ∧ ( bday 𝑡) = ( bday 𝐴))) → ¬ 𝑤 <s 𝑡))
3130imp 445 . . . . . 6 (((𝐴 No ∧ ∀𝑥𝐴𝑦𝐴𝑧 No ((𝑥 <s 𝑧𝑧 <s 𝑦) → 𝑧𝐴)) ∧ ((𝑤𝐴𝑡𝐴) ∧ (( bday 𝑤) = ( bday 𝐴) ∧ ( bday 𝑡) = ( bday 𝐴)))) → ¬ 𝑤 <s 𝑡)
32 ancom 466 . . . . . . . . 9 ((𝑤𝐴𝑡𝐴) ↔ (𝑡𝐴𝑤𝐴))
33 ancom 466 . . . . . . . . 9 ((( bday 𝑤) = ( bday 𝐴) ∧ ( bday 𝑡) = ( bday 𝐴)) ↔ (( bday 𝑡) = ( bday 𝐴) ∧ ( bday 𝑤) = ( bday 𝐴)))
3432, 33anbi12i 732 . . . . . . . 8 (((𝑤𝐴𝑡𝐴) ∧ (( bday 𝑤) = ( bday 𝐴) ∧ ( bday 𝑡) = ( bday 𝐴))) ↔ ((𝑡𝐴𝑤𝐴) ∧ (( bday 𝑡) = ( bday 𝐴) ∧ ( bday 𝑤) = ( bday 𝐴))))
35 nocvxminlem 31588 . . . . . . . 8 ((𝐴 No ∧ ∀𝑥𝐴𝑦𝐴𝑧 No ((𝑥 <s 𝑧𝑧 <s 𝑦) → 𝑧𝐴)) → (((𝑡𝐴𝑤𝐴) ∧ (( bday 𝑡) = ( bday 𝐴) ∧ ( bday 𝑤) = ( bday 𝐴))) → ¬ 𝑡 <s 𝑤))
3634, 35syl5bi 232 . . . . . . 7 ((𝐴 No ∧ ∀𝑥𝐴𝑦𝐴𝑧 No ((𝑥 <s 𝑧𝑧 <s 𝑦) → 𝑧𝐴)) → (((𝑤𝐴𝑡𝐴) ∧ (( bday 𝑤) = ( bday 𝐴) ∧ ( bday 𝑡) = ( bday 𝐴))) → ¬ 𝑡 <s 𝑤))
3736imp 445 . . . . . 6 (((𝐴 No ∧ ∀𝑥𝐴𝑦𝐴𝑧 No ((𝑥 <s 𝑧𝑧 <s 𝑦) → 𝑧𝐴)) ∧ ((𝑤𝐴𝑡𝐴) ∧ (( bday 𝑤) = ( bday 𝐴) ∧ ( bday 𝑡) = ( bday 𝐴)))) → ¬ 𝑡 <s 𝑤)
38 slttrieq2 31569 . . . . . . 7 ((𝑤 No 𝑡 No ) → (𝑤 = 𝑡 ↔ (¬ 𝑤 <s 𝑡 ∧ ¬ 𝑡 <s 𝑤)))
3938biimpar 502 . . . . . 6 (((𝑤 No 𝑡 No ) ∧ (¬ 𝑤 <s 𝑡 ∧ ¬ 𝑡 <s 𝑤)) → 𝑤 = 𝑡)
4029, 31, 37, 39syl12anc 1321 . . . . 5 (((𝐴 No ∧ ∀𝑥𝐴𝑦𝐴𝑧 No ((𝑥 <s 𝑧𝑧 <s 𝑦) → 𝑧𝐴)) ∧ ((𝑤𝐴𝑡𝐴) ∧ (( bday 𝑤) = ( bday 𝐴) ∧ ( bday 𝑡) = ( bday 𝐴)))) → 𝑤 = 𝑡)
4140exp32 630 . . . 4 ((𝐴 No ∧ ∀𝑥𝐴𝑦𝐴𝑧 No ((𝑥 <s 𝑧𝑧 <s 𝑦) → 𝑧𝐴)) → ((𝑤𝐴𝑡𝐴) → ((( bday 𝑤) = ( bday 𝐴) ∧ ( bday 𝑡) = ( bday 𝐴)) → 𝑤 = 𝑡)))
4241ralrimivv 2965 . . 3 ((𝐴 No ∧ ∀𝑥𝐴𝑦𝐴𝑧 No ((𝑥 <s 𝑧𝑧 <s 𝑦) → 𝑧𝐴)) → ∀𝑤𝐴𝑡𝐴 ((( bday 𝑤) = ( bday 𝐴) ∧ ( bday 𝑡) = ( bday 𝐴)) → 𝑤 = 𝑡))
43423adant1 1077 . 2 ((𝐴 ≠ ∅ ∧ 𝐴 No ∧ ∀𝑥𝐴𝑦𝐴𝑧 No ((𝑥 <s 𝑧𝑧 <s 𝑦) → 𝑧𝐴)) → ∀𝑤𝐴𝑡𝐴 ((( bday 𝑤) = ( bday 𝐴) ∧ ( bday 𝑡) = ( bday 𝐴)) → 𝑤 = 𝑡))
44 fveq2 6153 . . . 4 (𝑤 = 𝑡 → ( bday 𝑤) = ( bday 𝑡))
4544eqeq1d 2623 . . 3 (𝑤 = 𝑡 → (( bday 𝑤) = ( bday 𝐴) ↔ ( bday 𝑡) = ( bday 𝐴)))
4645reu4 3386 . 2 (∃!𝑤𝐴 ( bday 𝑤) = ( bday 𝐴) ↔ (∃𝑤𝐴 ( bday 𝑤) = ( bday 𝐴) ∧ ∀𝑤𝐴𝑡𝐴 ((( bday 𝑤) = ( bday 𝐴) ∧ ( bday 𝑡) = ( bday 𝐴)) → 𝑤 = 𝑡)))
4724, 43, 46sylanbrc 697 1 ((𝐴 ≠ ∅ ∧ 𝐴 No ∧ ∀𝑥𝐴𝑦𝐴𝑧 No ((𝑥 <s 𝑧𝑧 <s 𝑦) → 𝑧𝐴)) → ∃!𝑤𝐴 ( bday 𝑤) = ( bday 𝐴))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 384   ∧ w3a 1036   = wceq 1480  ∃wex 1701   ∈ wcel 1987   ≠ wne 2790  ∀wral 2907  ∃wrex 2908  ∃!wreu 2909   ⊆ wss 3559  ∅c0 3896  ∩ cint 4445   class class class wbr 4618  dom cdm 5079  ran crn 5080   “ cima 5082  Oncon0 5687  Fun wfun 5846   Fn wfn 5847  ‘cfv 5852   No csur 31529
 Copyright terms: Public domain W3C validator