Metamath Proof Explorer


Theorem cnflddsOLD

Description: Obsolete version of cnfldds as of 27-Apr-2025. (Contributed by Mario Carneiro, 14-Aug-2015) (Revised by Mario Carneiro, 6-Oct-2015) (Revised by Thierry Arnoux, 17-Dec-2017) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion cnflddsOLD abs=distfld

Proof

Step Hyp Ref Expression
1 absf abs:
2 subf :×
3 fco abs::×abs:×
4 1 2 3 mp2an abs:×
5 cnex V
6 5 5 xpex ×V
7 reex V
8 fex2 abs:××VVabsV
9 4 6 7 8 mp3an absV
10 cnfldstrOLD fldStruct113
11 dsid dist=Slotdistndx
12 snsstp3 distndxabsTopSetndxMetOpenabsndxdistndxabs
13 ssun1 TopSetndxMetOpenabsndxdistndxabsTopSetndxMetOpenabsndxdistndxabsUnifSetndxmetUnifabs
14 ssun2 TopSetndxMetOpenabsndxdistndxabsUnifSetndxmetUnifabsBasendx+ndx+ndx×*ndx*TopSetndxMetOpenabsndxdistndxabsUnifSetndxmetUnifabs
15 dfcnfldOLD fld=Basendx+ndx+ndx×*ndx*TopSetndxMetOpenabsndxdistndxabsUnifSetndxmetUnifabs
16 14 15 sseqtrri TopSetndxMetOpenabsndxdistndxabsUnifSetndxmetUnifabsfld
17 13 16 sstri TopSetndxMetOpenabsndxdistndxabsfld
18 12 17 sstri distndxabsfld
19 10 11 18 strfv absVabs=distfld
20 9 19 ax-mp abs=distfld