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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | breq1 | |
|
2 | 1 | anbi1d | |
3 | 2 | imbi1d | |
4 | 3 | ralbidv | |
5 | breq2 | |
|
6 | 5 | anbi2d | |
7 | 6 | imbi1d | |
8 | 7 | ralbidv | |
9 | 4 8 | rspc2v | |
10 | breq2 | |
|
11 | breq1 | |
|
12 | 10 11 | anbi12d | |
13 | eleq1w | |
|
14 | 12 13 | imbi12d | |
15 | 14 | rspcv | |
16 | bdaydm | |
|
17 | 16 | sseq2i | |
18 | bdayfun | |
|
19 | funfvima2 | |
|
20 | 18 19 | mpan | |
21 | 17 20 | sylbir | |
22 | 21 | imp | |
23 | intss1 | |
|
24 | 22 23 | syl | |
25 | imassrn | |
|
26 | bdayrn | |
|
27 | 25 26 | sseqtri | |
28 | 22 | ne0d | |
29 | oninton | |
|
30 | 27 28 29 | sylancr | |
31 | bdayelon | |
|
32 | ontri1 | |
|
33 | 30 31 32 | sylancl | |
34 | 24 33 | mpbid | |
35 | 34 | ex | |
36 | eleq2 | |
|
37 | 36 | notbid | |
38 | 37 | biimprcd | |
39 | 35 38 | syl6 | |
40 | 39 | com3l | |
41 | 40 | adantrd | |
42 | 15 41 | syl8 | |
43 | 42 | com35 | |
44 | 43 | com4l | |
45 | 9 44 | syl6 | |
46 | 45 | com3l | |
47 | 46 | impcom | |
48 | 47 | imp42 | |
49 | 48 | con2d | |
50 | 3anass | |
|
51 | 50 | notbii | |
52 | imnan | |
|
53 | 51 52 | bitr4i | |
54 | 49 53 | sylibr | |
55 | 54 | nrexdv | |
56 | ssel | |
|
57 | ssel | |
|
58 | 56 57 | anim12d | |
59 | 58 | imp | |
60 | eqtr3 | |
|
61 | 59 60 | anim12i | |
62 | 61 | anasss | |
63 | 62 | adantlr | |
64 | nodense | |
|
65 | 64 | anassrs | |
66 | 63 65 | sylan | |
67 | 55 66 | mtand | |
68 | 67 | ex | |