Proof of Theorem cnfldfunALT
Step | Hyp | Ref
| Expression |
1 | | cnfldstr 19748 |
. 2
ℂfld Struct ; |
2 | | structn0fun 15869 |
. . 3
ℂfld Struct
;
ℂfld |
3 | | fvex 6201 |
. . . . . . . . . . . . 13
|
4 | | cnex 10017 |
. . . . . . . . . . . . 13
|
5 | 3, 4 | opnzi 4943 |
. . . . . . . . . . . 12
|
6 | 5 | nesymi 2851 |
. . . . . . . . . . 11
|
7 | | fvex 6201 |
. . . . . . . . . . . . 13
|
8 | | addex 11830 |
. . . . . . . . . . . . 13
|
9 | 7, 8 | opnzi 4943 |
. . . . . . . . . . . 12
|
10 | 9 | nesymi 2851 |
. . . . . . . . . . 11
|
11 | | fvex 6201 |
. . . . . . . . . . . . 13
|
12 | | mulex 11831 |
. . . . . . . . . . . . 13
|
13 | 11, 12 | opnzi 4943 |
. . . . . . . . . . . 12
|
14 | 13 | nesymi 2851 |
. . . . . . . . . . 11
|
15 | | 3ioran 1056 |
. . . . . . . . . . . 12
|
16 | | 0ex 4790 |
. . . . . . . . . . . . 13
|
17 | 16 | eltp 4230 |
. . . . . . . . . . . 12
|
18 | 15, 17 | xchnxbir 323 |
. . . . . . . . . . 11
|
19 | 6, 10, 14, 18 | mpbir3an 1244 |
. . . . . . . . . 10
|
20 | | fvex 6201 |
. . . . . . . . . . . . 13
|
21 | | cjf 13844 |
. . . . . . . . . . . . . 14
|
22 | | fex 6490 |
. . . . . . . . . . . . . 14
|
23 | 21, 4, 22 | mp2an 708 |
. . . . . . . . . . . . 13
|
24 | 20, 23 | opnzi 4943 |
. . . . . . . . . . . 12
|
25 | 24 | necomi 2848 |
. . . . . . . . . . 11
|
26 | | nelsn 4212 |
. . . . . . . . . . 11
|
27 | 25, 26 | ax-mp 5 |
. . . . . . . . . 10
|
28 | 19, 27 | pm3.2i 471 |
. . . . . . . . 9
|
29 | | fvex 6201 |
. . . . . . . . . . . . . 14
TopSet
|
30 | | fvex 6201 |
. . . . . . . . . . . . . 14
|
31 | 29, 30 | opnzi 4943 |
. . . . . . . . . . . . 13
TopSet |
32 | 31 | nesymi 2851 |
. . . . . . . . . . . 12
TopSet |
33 | | fvex 6201 |
. . . . . . . . . . . . . 14
|
34 | | letsr 17227 |
. . . . . . . . . . . . . . 15
|
35 | 34 | elexi 3213 |
. . . . . . . . . . . . . 14
|
36 | 33, 35 | opnzi 4943 |
. . . . . . . . . . . . 13
|
37 | 36 | nesymi 2851 |
. . . . . . . . . . . 12
|
38 | | fvex 6201 |
. . . . . . . . . . . . . 14
|
39 | | absf 14077 |
. . . . . . . . . . . . . . . 16
|
40 | | fex 6490 |
. . . . . . . . . . . . . . . 16
|
41 | 39, 4, 40 | mp2an 708 |
. . . . . . . . . . . . . . 15
|
42 | | subf 10283 |
. . . . . . . . . . . . . . . 16
|
43 | 4, 4 | xpex 6962 |
. . . . . . . . . . . . . . . 16
|
44 | | fex 6490 |
. . . . . . . . . . . . . . . 16
|
45 | 42, 43, 44 | mp2an 708 |
. . . . . . . . . . . . . . 15
|
46 | 41, 45 | coex 7118 |
. . . . . . . . . . . . . 14
|
47 | 38, 46 | opnzi 4943 |
. . . . . . . . . . . . 13
|
48 | 47 | nesymi 2851 |
. . . . . . . . . . . 12
|
49 | | 3ioran 1056 |
. . . . . . . . . . . 12
TopSet
TopSet
|
50 | 32, 37, 48, 49 | mpbir3an 1244 |
. . . . . . . . . . 11
TopSet
|
51 | 16 | eltp 4230 |
. . . . . . . . . . 11
TopSet
TopSet |
52 | 50, 51 | mtbir 313 |
. . . . . . . . . 10
TopSet |
53 | | fvex 6201 |
. . . . . . . . . . . . 13
|
54 | | fvex 6201 |
. . . . . . . . . . . . 13
metUnif |
55 | 53, 54 | opnzi 4943 |
. . . . . . . . . . . 12
metUnif |
56 | 55 | necomi 2848 |
. . . . . . . . . . 11
metUnif |
57 | | nelsn 4212 |
. . . . . . . . . . 11
metUnif
metUnif |
58 | 56, 57 | ax-mp 5 |
. . . . . . . . . 10
metUnif |
59 | 52, 58 | pm3.2i 471 |
. . . . . . . . 9
TopSet metUnif |
60 | 28, 59 | pm3.2i 471 |
. . . . . . . 8
TopSet metUnif |
61 | | ioran 511 |
. . . . . . . . 9
TopSet
metUnif
TopSet metUnif |
62 | | ioran 511 |
. . . . . . . . . 10
|
63 | | ioran 511 |
. . . . . . . . . 10
TopSet metUnif
TopSet metUnif |
64 | 62, 63 | anbi12i 733 |
. . . . . . . . 9
TopSet metUnif
TopSet metUnif |
65 | 61, 64 | bitri 264 |
. . . . . . . 8
TopSet
metUnif
TopSet metUnif |
66 | 60, 65 | mpbir 221 |
. . . . . . 7
TopSet
metUnif |
67 | | df-cnfld 19747 |
. . . . . . . . 9
ℂfld
TopSet metUnif |
68 | 67 | eleq2i 2693 |
. . . . . . . 8
ℂfld TopSet metUnif |
69 | | elun 3753 |
. . . . . . . 8
TopSet metUnif
TopSet
metUnif |
70 | | elun 3753 |
. . . . . . . . 9
|
71 | | elun 3753 |
. . . . . . . . 9
TopSet metUnif
TopSet metUnif |
72 | 70, 71 | orbi12i 543 |
. . . . . . . 8
TopSet
metUnif
TopSet
metUnif |
73 | 68, 69, 72 | 3bitri 286 |
. . . . . . 7
ℂfld TopSet
metUnif |
74 | 66, 73 | mtbir 313 |
. . . . . 6
ℂfld |
75 | | disjsn 4246 |
. . . . . 6
ℂfld
ℂfld |
76 | 74, 75 | mpbir 221 |
. . . . 5
ℂfld |
77 | | disjdif2 4047 |
. . . . 5
ℂfld ℂfld ℂfld |
78 | 76, 77 | ax-mp 5 |
. . . 4
ℂfld
ℂfld |
79 | 78 | funeqi 5909 |
. . 3
ℂfld ℂfld |
80 | 2, 79 | sylib 208 |
. 2
ℂfld Struct
;
ℂfld |
81 | 1, 80 | ax-mp 5 |
1
ℂfld |