Metamath Proof Explorer


Theorem cnfldfunALT

Description: Alternate proof of cnfldfun (much shorter proof, using cnfldstr and structn0fun : in addition, it must be shown that (/) e/ CCfld ). (Contributed by AV, 18-Nov-2021) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion cnfldfunALT Fun fld

Proof

Step Hyp Ref Expression
1 cnfldstr fld Struct 1 13
2 structn0fun fld Struct 1 13 Fun fld
3 fvex Base ndx V
4 cnex V
5 3 4 opnzi Base ndx
6 5 nesymi ¬ = Base ndx
7 fvex + ndx V
8 addex + V
9 7 8 opnzi + ndx +
10 9 nesymi ¬ = + ndx +
11 fvex ndx V
12 mulex × V
13 11 12 opnzi ndx ×
14 13 nesymi ¬ = ndx ×
15 3ioran ¬ = Base ndx = + ndx + = ndx × ¬ = Base ndx ¬ = + ndx + ¬ = ndx ×
16 0ex V
17 16 eltp Base ndx + ndx + ndx × = Base ndx = + ndx + = ndx ×
18 15 17 xchnxbir ¬ Base ndx + ndx + ndx × ¬ = Base ndx ¬ = + ndx + ¬ = ndx ×
19 6 10 14 18 mpbir3an ¬ Base ndx + ndx + ndx ×
20 fvex * ndx V
21 cjf * :
22 fex * : V * V
23 21 4 22 mp2an * V
24 20 23 opnzi * ndx *
25 24 necomi * ndx *
26 nelsn * ndx * ¬ * ndx *
27 25 26 ax-mp ¬ * ndx *
28 19 27 pm3.2i ¬ Base ndx + ndx + ndx × ¬ * ndx *
29 fvex TopSet ndx V
30 fvex MetOpen abs V
31 29 30 opnzi TopSet ndx MetOpen abs
32 31 nesymi ¬ = TopSet ndx MetOpen abs
33 fvex ndx V
34 letsr TosetRel
35 34 elexi V
36 33 35 opnzi ndx
37 36 nesymi ¬ = ndx
38 fvex dist ndx V
39 absf abs :
40 fex abs : V abs V
41 39 4 40 mp2an abs V
42 subf : ×
43 4 4 xpex × V
44 fex : × × V V
45 42 43 44 mp2an V
46 41 45 coex abs V
47 38 46 opnzi dist ndx abs
48 47 nesymi ¬ = dist ndx abs
49 3ioran ¬ = TopSet ndx MetOpen abs = ndx = dist ndx abs ¬ = TopSet ndx MetOpen abs ¬ = ndx ¬ = dist ndx abs
50 32 37 48 49 mpbir3an ¬ = TopSet ndx MetOpen abs = ndx = dist ndx abs
51 16 eltp TopSet ndx MetOpen abs ndx dist ndx abs = TopSet ndx MetOpen abs = ndx = dist ndx abs
52 50 51 mtbir ¬ TopSet ndx MetOpen abs ndx dist ndx abs
53 fvex UnifSet ndx V
54 fvex metUnif abs V
55 53 54 opnzi UnifSet ndx metUnif abs
56 55 necomi UnifSet ndx metUnif abs
57 nelsn UnifSet ndx metUnif abs ¬ UnifSet ndx metUnif abs
58 56 57 ax-mp ¬ UnifSet ndx metUnif abs
59 52 58 pm3.2i ¬ TopSet ndx MetOpen abs ndx dist ndx abs ¬ UnifSet ndx metUnif abs
60 28 59 pm3.2i ¬ Base ndx + ndx + ndx × ¬ * ndx * ¬ TopSet ndx MetOpen abs ndx dist ndx abs ¬ UnifSet ndx metUnif abs
61 ioran ¬ Base ndx + ndx + ndx × * ndx * TopSet ndx MetOpen abs ndx dist ndx abs UnifSet ndx metUnif abs ¬ Base ndx + ndx + ndx × * ndx * ¬ TopSet ndx MetOpen abs ndx dist ndx abs UnifSet ndx metUnif abs
62 ioran ¬ Base ndx + ndx + ndx × * ndx * ¬ Base ndx + ndx + ndx × ¬ * ndx *
63 ioran ¬ TopSet ndx MetOpen abs ndx dist ndx abs UnifSet ndx metUnif abs ¬ TopSet ndx MetOpen abs ndx dist ndx abs ¬ UnifSet ndx metUnif abs
64 62 63 anbi12i ¬ Base ndx + ndx + ndx × * ndx * ¬ TopSet ndx MetOpen abs ndx dist ndx abs UnifSet ndx metUnif abs ¬ Base ndx + ndx + ndx × ¬ * ndx * ¬ TopSet ndx MetOpen abs ndx dist ndx abs ¬ UnifSet ndx metUnif abs
65 61 64 bitri ¬ Base ndx + ndx + ndx × * ndx * TopSet ndx MetOpen abs ndx dist ndx abs UnifSet ndx metUnif abs ¬ Base ndx + ndx + ndx × ¬ * ndx * ¬ TopSet ndx MetOpen abs ndx dist ndx abs ¬ UnifSet ndx metUnif abs
66 60 65 mpbir ¬ Base ndx + ndx + ndx × * ndx * TopSet ndx MetOpen abs ndx dist ndx abs UnifSet ndx metUnif abs
67 df-cnfld fld = Base ndx + ndx + ndx × * ndx * TopSet ndx MetOpen abs ndx dist ndx abs UnifSet ndx metUnif abs
68 67 eleq2i fld Base ndx + ndx + ndx × * ndx * TopSet ndx MetOpen abs ndx dist ndx abs UnifSet ndx metUnif abs
69 elun Base ndx + ndx + ndx × * ndx * TopSet ndx MetOpen abs ndx dist ndx abs UnifSet ndx metUnif abs Base ndx + ndx + ndx × * ndx * TopSet ndx MetOpen abs ndx dist ndx abs UnifSet ndx metUnif abs
70 elun Base ndx + ndx + ndx × * ndx * Base ndx + ndx + ndx × * ndx *
71 elun TopSet ndx MetOpen abs ndx dist ndx abs UnifSet ndx metUnif abs TopSet ndx MetOpen abs ndx dist ndx abs UnifSet ndx metUnif abs
72 70 71 orbi12i Base ndx + ndx + ndx × * ndx * TopSet ndx MetOpen abs ndx dist ndx abs UnifSet ndx metUnif abs Base ndx + ndx + ndx × * ndx * TopSet ndx MetOpen abs ndx dist ndx abs UnifSet ndx metUnif abs
73 68 69 72 3bitri fld Base ndx + ndx + ndx × * ndx * TopSet ndx MetOpen abs ndx dist ndx abs UnifSet ndx metUnif abs
74 66 73 mtbir ¬ fld
75 disjsn fld = ¬ fld
76 74 75 mpbir fld =
77 disjdif2 fld = fld = fld
78 76 77 ax-mp fld = fld
79 78 funeqi Fun fld Fun fld
80 2 79 sylib fld Struct 1 13 Fun fld
81 1 80 ax-mp Fun fld