Metamath Proof Explorer


Theorem fprodsub2cncf

Description: F is continuous. (Contributed by Glauco Siliprandi, 8-Apr-2021)

Ref Expression
Hypotheses fprodsub2cncf.k kφ
fprodsub2cncf.a φAFin
fprodsub2cncf.b φkAB
fprodsub2cncf.f F=xkABx
Assertion fprodsub2cncf φF:cn

Proof

Step Hyp Ref Expression
1 fprodsub2cncf.k kφ
2 fprodsub2cncf.a φAFin
3 fprodsub2cncf.b φkAB
4 fprodsub2cncf.f F=xkABx
5 4 a1i φF=xkABx
6 eqid TopOpenfld=TopOpenfld
7 6 cnfldtopon TopOpenfldTopOn
8 7 a1i φTopOpenfldTopOn
9 eqid xBx=xBx
10 3 9 sub2cncfd φkAxBx:cn
11 6 cncfcn1 cn=TopOpenfldCnTopOpenfld
12 11 a1i φkAcn=TopOpenfldCnTopOpenfld
13 10 12 eleqtrd φkAxBxTopOpenfldCnTopOpenfld
14 1 6 8 2 13 fprodcn φxkABxTopOpenfldCnTopOpenfld
15 5 14 eqeltrd φFTopOpenfldCnTopOpenfld
16 11 a1i φcn=TopOpenfldCnTopOpenfld
17 16 eqcomd φTopOpenfldCnTopOpenfld=cn
18 15 17 eleqtrd φF:cn