Metamath Proof Explorer


Theorem nocvxmin

Description: Given a nonempty convex class of surreals, there is a unique birthday-minimal element of that class. Lemma 0 of Alling p. 185. (Contributed by Scott Fenton, 30-Jun-2011)

Ref Expression
Assertion nocvxmin A A No x A y A z No x < s z z < s y z A ∃! w A bday w = bday A

Proof

Step Hyp Ref Expression
1 imassrn bday A ran bday
2 bdayrn ran bday = On
3 1 2 sseqtri bday A On
4 bdaydm dom bday = No
5 4 sseq2i A dom bday A No
6 bdayfun Fun bday
7 funfvima2 Fun bday A dom bday x A bday x bday A
8 6 7 mpan A dom bday x A bday x bday A
9 5 8 sylbir A No x A bday x bday A
10 elex2 bday x bday A w w bday A
11 9 10 syl6 A No x A w w bday A
12 11 exlimdv A No x x A w w bday A
13 n0 A x x A
14 n0 bday A w w bday A
15 12 13 14 3imtr4g A No A bday A
16 15 impcom A A No bday A
17 onint bday A On bday A bday A bday A
18 3 16 17 sylancr A A No bday A bday A
19 bdayfn bday Fn No
20 fvelimab bday Fn No A No bday A bday A w A bday w = bday A
21 19 20 mpan A No bday A bday A w A bday w = bday A
22 21 adantl A A No bday A bday A w A bday w = bday A
23 18 22 mpbid A A No w A bday w = bday A
24 23 3adant3 A A No x A y A z No x < s z z < s y z A w A bday w = bday A
25 ssel A No w A w No
26 ssel A No t A t No
27 25 26 anim12d A No w A t A w No t No
28 27 imp A No w A t A w No t No
29 28 ad2ant2r A No x A y A z No x < s z z < s y z A w A t A bday w = bday A bday t = bday A w No t No
30 nocvxminlem A No x A y A z No x < s z z < s y z A w A t A bday w = bday A bday t = bday A ¬ w < s t
31 30 imp A No x A y A z No x < s z z < s y z A w A t A bday w = bday A bday t = bday A ¬ w < s t
32 ancom w A t A t A w A
33 ancom bday w = bday A bday t = bday A bday t = bday A bday w = bday A
34 32 33 anbi12i w A t A bday w = bday A bday t = bday A t A w A bday t = bday A bday w = bday A
35 nocvxminlem A No x A y A z No x < s z z < s y z A t A w A bday t = bday A bday w = bday A ¬ t < s w
36 34 35 syl5bi A No x A y A z No x < s z z < s y z A w A t A bday w = bday A bday t = bday A ¬ t < s w
37 36 imp A No x A y A z No x < s z z < s y z A w A t A bday w = bday A bday t = bday A ¬ t < s w
38 slttrieq2 w No t No w = t ¬ w < s t ¬ t < s w
39 38 biimpar w No t No ¬ w < s t ¬ t < s w w = t
40 29 31 37 39 syl12anc A No x A y A z No x < s z z < s y z A w A t A bday w = bday A bday t = bday A w = t
41 40 exp32 A No x A y A z No x < s z z < s y z A w A t A bday w = bday A bday t = bday A w = t
42 41 ralrimivv A No x A y A z No x < s z z < s y z A w A t A bday w = bday A bday t = bday A w = t
43 42 3adant1 A A No x A y A z No x < s z z < s y z A w A t A bday w = bday A bday t = bday A w = t
44 fveqeq2 w = t bday w = bday A bday t = bday A
45 44 reu4 ∃! w A bday w = bday A w A bday w = bday A w A t A bday w = bday A bday t = bday A w = t
46 24 43 45 sylanbrc A A No x A y A z No x < s z z < s y z A ∃! w A bday w = bday A