Metamath Proof Explorer


Theorem nocvxminlem

Description: Lemma for nocvxmin . Given two birthday-minimal elements of a convex class of surreals, they are not comparable. (Contributed by Scott Fenton, 30-Jun-2011)

Ref Expression
Assertion nocvxminlem ANoxAyAzNox<szz<syzAXAYAbdayX=bdayAbdayY=bdayA¬X<sY

Proof

Step Hyp Ref Expression
1 breq1 x=Xx<szX<sz
2 1 anbi1d x=Xx<szz<syX<szz<sy
3 2 imbi1d x=Xx<szz<syzAX<szz<syzA
4 3 ralbidv x=XzNox<szz<syzAzNoX<szz<syzA
5 breq2 y=Yz<syz<sY
6 5 anbi2d y=YX<szz<syX<szz<sY
7 6 imbi1d y=YX<szz<syzAX<szz<sYzA
8 7 ralbidv y=YzNoX<szz<syzAzNoX<szz<sYzA
9 4 8 rspc2v XAYAxAyAzNox<szz<syzAzNoX<szz<sYzA
10 breq2 z=wX<szX<sw
11 breq1 z=wz<sYw<sY
12 10 11 anbi12d z=wX<szz<sYX<sww<sY
13 eleq1w z=wzAwA
14 12 13 imbi12d z=wX<szz<sYzAX<sww<sYwA
15 14 rspcv wNozNoX<szz<sYzAX<sww<sYwA
16 bdaydm dombday=No
17 16 sseq2i AdombdayANo
18 bdayfun Funbday
19 funfvima2 FunbdayAdombdaywAbdaywbdayA
20 18 19 mpan AdombdaywAbdaywbdayA
21 17 20 sylbir ANowAbdaywbdayA
22 21 imp ANowAbdaywbdayA
23 intss1 bdaywbdayAbdayAbdayw
24 22 23 syl ANowAbdayAbdayw
25 imassrn bdayAranbday
26 bdayrn ranbday=On
27 25 26 sseqtri bdayAOn
28 22 ne0d ANowAbdayA
29 oninton bdayAOnbdayAbdayAOn
30 27 28 29 sylancr ANowAbdayAOn
31 bdayelon bdaywOn
32 ontri1 bdayAOnbdaywOnbdayAbdayw¬bdaywbdayA
33 30 31 32 sylancl ANowAbdayAbdayw¬bdaywbdayA
34 24 33 mpbid ANowA¬bdaywbdayA
35 34 ex ANowA¬bdaywbdayA
36 eleq2 bdayX=bdayAbdaywbdayXbdaywbdayA
37 36 notbid bdayX=bdayA¬bdaywbdayX¬bdaywbdayA
38 37 biimprcd ¬bdaywbdayAbdayX=bdayA¬bdaywbdayX
39 35 38 syl6 ANowAbdayX=bdayA¬bdaywbdayX
40 39 com3l wAbdayX=bdayAANo¬bdaywbdayX
41 40 adantrd wAbdayX=bdayAbdayY=bdayAANo¬bdaywbdayX
42 15 41 syl8 wNozNoX<szz<sYzAX<sww<sYbdayX=bdayAbdayY=bdayAANo¬bdaywbdayX
43 42 com35 wNozNoX<szz<sYzAANobdayX=bdayAbdayY=bdayAX<sww<sY¬bdaywbdayX
44 43 com4l zNoX<szz<sYzAANobdayX=bdayAbdayY=bdayAwNoX<sww<sY¬bdaywbdayX
45 9 44 syl6 XAYAxAyAzNox<szz<syzAANobdayX=bdayAbdayY=bdayAwNoX<sww<sY¬bdaywbdayX
46 45 com3l xAyAzNox<szz<syzAANoXAYAbdayX=bdayAbdayY=bdayAwNoX<sww<sY¬bdaywbdayX
47 46 impcom ANoxAyAzNox<szz<syzAXAYAbdayX=bdayAbdayY=bdayAwNoX<sww<sY¬bdaywbdayX
48 47 imp42 ANoxAyAzNox<szz<syzAXAYAbdayX=bdayAbdayY=bdayAwNoX<sww<sY¬bdaywbdayX
49 48 con2d ANoxAyAzNox<szz<syzAXAYAbdayX=bdayAbdayY=bdayAwNobdaywbdayX¬X<sww<sY
50 3anass bdaywbdayXX<sww<sYbdaywbdayXX<sww<sY
51 50 notbii ¬bdaywbdayXX<sww<sY¬bdaywbdayXX<sww<sY
52 imnan bdaywbdayX¬X<sww<sY¬bdaywbdayXX<sww<sY
53 51 52 bitr4i ¬bdaywbdayXX<sww<sYbdaywbdayX¬X<sww<sY
54 49 53 sylibr ANoxAyAzNox<szz<syzAXAYAbdayX=bdayAbdayY=bdayAwNo¬bdaywbdayXX<sww<sY
55 54 nrexdv ANoxAyAzNox<szz<syzAXAYAbdayX=bdayAbdayY=bdayA¬wNobdaywbdayXX<sww<sY
56 ssel ANoXAXNo
57 ssel ANoYAYNo
58 56 57 anim12d ANoXAYAXNoYNo
59 58 imp ANoXAYAXNoYNo
60 eqtr3 bdayX=bdayAbdayY=bdayAbdayX=bdayY
61 59 60 anim12i ANoXAYAbdayX=bdayAbdayY=bdayAXNoYNobdayX=bdayY
62 61 anasss ANoXAYAbdayX=bdayAbdayY=bdayAXNoYNobdayX=bdayY
63 62 adantlr ANoxAyAzNox<szz<syzAXAYAbdayX=bdayAbdayY=bdayAXNoYNobdayX=bdayY
64 nodense XNoYNobdayX=bdayYX<sYwNobdaywbdayXX<sww<sY
65 64 anassrs XNoYNobdayX=bdayYX<sYwNobdaywbdayXX<sww<sY
66 63 65 sylan ANoxAyAzNox<szz<syzAXAYAbdayX=bdayAbdayY=bdayAX<sYwNobdaywbdayXX<sww<sY
67 55 66 mtand ANoxAyAzNox<szz<syzAXAYAbdayX=bdayAbdayY=bdayA¬X<sY
68 67 ex ANoxAyAzNox<szz<syzAXAYAbdayX=bdayAbdayY=bdayA¬X<sY