Description: Lemma for nodense . Give a condition for surreal less-than when two surreals have the same birthday. (Contributed by Scott Fenton, 19-Jun-2011)
Ref | Expression | ||
---|---|---|---|
Assertion | nodenselem8 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nodenselem5 | |
|
2 | 1 | exp32 | |
3 | 2 | 3impia | |
4 | sltval2 | |
|
5 | 4 | 3adant3 | |
6 | fvex | |
|
7 | fvex | |
|
8 | 6 7 | brtp | |
9 | eleq2 | |
|
10 | 9 | biimpd | |
11 | nosgnn0 | |
|
12 | nofnbday | |
|
13 | fnfvelrn | |
|
14 | eleq1 | |
|
15 | 13 14 | syl5ibcom | |
16 | 12 15 | sylan | |
17 | norn | |
|
18 | 17 | sseld | |
19 | 18 | adantr | |
20 | 16 19 | syld | |
21 | 11 20 | mtoi | |
22 | 21 | ex | |
23 | 22 | adantl | |
24 | 10 23 | syl9r | |
25 | 24 | 3impia | |
26 | 25 | imp | |
27 | 26 | intnand | |
28 | nofnbday | |
|
29 | fnfvelrn | |
|
30 | eleq1 | |
|
31 | 29 30 | syl5ibcom | |
32 | 28 31 | sylan | |
33 | norn | |
|
34 | 33 | sseld | |
35 | 34 | adantr | |
36 | 32 35 | syld | |
37 | 11 36 | mtoi | |
38 | 37 | 3ad2antl1 | |
39 | 38 | intnanrd | |
40 | 3orel13 | |
|
41 | 27 39 40 | syl2anc | |
42 | 41 | ex | |
43 | 42 | com23 | |
44 | 8 43 | biimtrid | |
45 | 5 44 | sylbid | |
46 | 3 45 | mpdd | |
47 | 3mix2 | |
|
48 | 47 8 | sylibr | |
49 | 48 5 | imbitrrid | |
50 | 46 49 | impbid | |