Description: The base set of the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014) (Revised by Mario Carneiro, 6-Oct-2015) (Revised by Thierry Arnoux, 17-Dec-2017)
Ref | Expression | ||
---|---|---|---|
Assertion | cnfldbas | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cnex | |
|
2 | cnfldstr | |
|
3 | baseid | |
|
4 | snsstp1 | |
|
5 | ssun1 | |
|
6 | ssun1 | |
|
7 | df-cnfld | |
|
8 | 6 7 | sseqtrri | |
9 | 5 8 | sstri | |
10 | 4 9 | sstri | |
11 | 2 3 10 | strfv | |
12 | 1 11 | ax-mp | |