Description: The set containing only 0 is an ideal. (Contributed by Jeff Madsen, 10-Jun-2010)
Ref | Expression | ||
---|---|---|---|
Hypotheses | 0idl.1 | |
|
0idl.2 | |
||
Assertion | 0idl | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 0idl.1 | |
|
2 | 0idl.2 | |
|
3 | eqid | |
|
4 | 1 3 2 | rngo0cl | |
5 | 4 | snssd | |
6 | 2 | fvexi | |
7 | 6 | snid | |
8 | 7 | a1i | |
9 | velsn | |
|
10 | velsn | |
|
11 | 1 3 2 | rngo0rid | |
12 | 4 11 | mpdan | |
13 | ovex | |
|
14 | 13 | elsn | |
15 | 12 14 | sylibr | |
16 | oveq2 | |
|
17 | 16 | eleq1d | |
18 | 15 17 | syl5ibrcom | |
19 | 10 18 | syl5bi | |
20 | 19 | ralrimiv | |
21 | eqid | |
|
22 | 2 3 1 21 | rngorz | |
23 | ovex | |
|
24 | 23 | elsn | |
25 | 22 24 | sylibr | |
26 | 2 3 1 21 | rngolz | |
27 | ovex | |
|
28 | 27 | elsn | |
29 | 26 28 | sylibr | |
30 | 25 29 | jca | |
31 | 30 | ralrimiva | |
32 | 20 31 | jca | |
33 | oveq1 | |
|
34 | 33 | eleq1d | |
35 | 34 | ralbidv | |
36 | oveq2 | |
|
37 | 36 | eleq1d | |
38 | oveq1 | |
|
39 | 38 | eleq1d | |
40 | 37 39 | anbi12d | |
41 | 40 | ralbidv | |
42 | 35 41 | anbi12d | |
43 | 32 42 | syl5ibrcom | |
44 | 9 43 | syl5bi | |
45 | 44 | ralrimiv | |
46 | 1 21 3 2 | isidl | |
47 | 5 8 45 46 | mpbir3and | |