Description: Variant of Zorn's lemma zorng in which (/) , the union of the empty chain, is not required to be an element of A . (Contributed by Jeff Madsen, 5-Jan-2011) (Revised by Mario Carneiro, 9-May-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | zornn0g | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp2 | |
|
2 | simp1 | |
|
3 | snfi | |
|
4 | finnum | |
|
5 | 3 4 | ax-mp | |
6 | unnum | |
|
7 | 2 5 6 | sylancl | |
8 | uncom | |
|
9 | 8 | sseq2i | |
10 | ssundif | |
|
11 | 9 10 | bitri | |
12 | difss | |
|
13 | soss | |
|
14 | 12 13 | ax-mp | |
15 | ssdif0 | |
|
16 | uni0b | |
|
17 | 16 | biimpri | |
18 | 17 | eleq1d | |
19 | 15 18 | sylbir | |
20 | 19 | imbi2d | |
21 | vex | |
|
22 | 21 | difexi | |
23 | sseq1 | |
|
24 | neeq1 | |
|
25 | soeq2 | |
|
26 | 23 24 25 | 3anbi123d | |
27 | unieq | |
|
28 | 27 | eleq1d | |
29 | 26 28 | imbi12d | |
30 | 22 29 | spcv | |
31 | 30 | com12 | |
32 | 31 | 3expa | |
33 | 32 | an32s | |
34 | unidif0 | |
|
35 | 34 | eleq1i | |
36 | elun1 | |
|
37 | 35 36 | sylbi | |
38 | 33 37 | syl6 | |
39 | 0ex | |
|
40 | 39 | snid | |
41 | elun2 | |
|
42 | 40 41 | ax-mp | |
43 | 42 | 2a1i | |
44 | 20 38 43 | pm2.61ne | |
45 | 14 44 | sylan2 | |
46 | 11 45 | sylanb | |
47 | 46 | com12 | |
48 | 47 | alrimiv | |
49 | 48 | 3ad2ant3 | |
50 | zorng | |
|
51 | 7 49 50 | syl2anc | |
52 | ssun1 | |
|
53 | ssralv | |
|
54 | 52 53 | ax-mp | |
55 | 54 | reximi | |
56 | rexun | |
|
57 | simpr | |
|
58 | simpr | |
|
59 | psseq1 | |
|
60 | 0pss | |
|
61 | 59 60 | bitrdi | |
62 | 61 | notbid | |
63 | nne | |
|
64 | 62 63 | bitrdi | |
65 | 64 | ralbidv | |
66 | 39 65 | rexsn | |
67 | eqsn | |
|
68 | 67 | biimpar | |
69 | 66 68 | sylan2b | |
70 | 69 | rexeqdv | |
71 | 58 70 | mpbird | |
72 | 57 71 | jaodan | |
73 | 56 72 | sylan2b | |
74 | 55 73 | sylan2 | |
75 | 1 51 74 | syl2anc | |