Metamath Proof Explorer


Theorem iscnrm3r

Description: Lemma for iscnrm3 . If all subspaces of a topology are normal, i.e., two disjoint closed sets can be separated by open neighborhoods, then in the original topology two separated sets can be separated by open neighborhoods. (Contributed by Zhi Wang, 5-Sep-2024)

Ref Expression
Assertion iscnrm3r JTopz𝒫JcClsdJ𝑡zdClsdJ𝑡zcd=lJ𝑡zkJ𝑡zcldklk=S𝒫JT𝒫JSclsJT=clsJST=nJmJSnTmnm=

Proof

Step Hyp Ref Expression
1 oveq2 z=JclsJSclsJTJ𝑡z=J𝑡JclsJSclsJT
2 1 fveq2d z=JclsJSclsJTClsdJ𝑡z=ClsdJ𝑡JclsJSclsJT
3 1 rexeqdv z=JclsJSclsJTkJ𝑡zcldklk=kJ𝑡JclsJSclsJTcldklk=
4 1 3 rexeqbidv z=JclsJSclsJTlJ𝑡zkJ𝑡zcldklk=lJ𝑡JclsJSclsJTkJ𝑡JclsJSclsJTcldklk=
5 4 imbi2d z=JclsJSclsJTcd=lJ𝑡zkJ𝑡zcldklk=cd=lJ𝑡JclsJSclsJTkJ𝑡JclsJSclsJTcldklk=
6 2 5 raleqbidv z=JclsJSclsJTdClsdJ𝑡zcd=lJ𝑡zkJ𝑡zcldklk=dClsdJ𝑡JclsJSclsJTcd=lJ𝑡JclsJSclsJTkJ𝑡JclsJSclsJTcldklk=
7 2 6 raleqbidv z=JclsJSclsJTcClsdJ𝑡zdClsdJ𝑡zcd=lJ𝑡zkJ𝑡zcldklk=cClsdJ𝑡JclsJSclsJTdClsdJ𝑡JclsJSclsJTcd=lJ𝑡JclsJSclsJTkJ𝑡JclsJSclsJTcldklk=
8 7 rspcv JclsJSclsJT𝒫Jz𝒫JcClsdJ𝑡zdClsdJ𝑡zcd=lJ𝑡zkJ𝑡zcldklk=cClsdJ𝑡JclsJSclsJTdClsdJ𝑡JclsJSclsJTcd=lJ𝑡JclsJSclsJTkJ𝑡JclsJSclsJTcldklk=
9 8 3ad2ant1 JclsJSclsJT𝒫JclsJSclsJTClsdJ𝑡JclsJSclsJTclsJTclsJSClsdJ𝑡JclsJSclsJTz𝒫JcClsdJ𝑡zdClsdJ𝑡zcd=lJ𝑡zkJ𝑡zcldklk=cClsdJ𝑡JclsJSclsJTdClsdJ𝑡JclsJSclsJTcd=lJ𝑡JclsJSclsJTkJ𝑡JclsJSclsJTcldklk=
10 ineq12 c=clsJSclsJTd=clsJTclsJScd=clsJSclsJTclsJTclsJS
11 10 eqeq1d c=clsJSclsJTd=clsJTclsJScd=clsJSclsJTclsJTclsJS=
12 simpl c=clsJSclsJTd=clsJTclsJSc=clsJSclsJT
13 12 sseq1d c=clsJSclsJTd=clsJTclsJSclclsJSclsJTl
14 simpr c=clsJSclsJTd=clsJTclsJSd=clsJTclsJS
15 14 sseq1d c=clsJSclsJTd=clsJTclsJSdkclsJTclsJSk
16 13 15 3anbi12d c=clsJSclsJTd=clsJTclsJScldklk=clsJSclsJTlclsJTclsJSklk=
17 16 2rexbidv c=clsJSclsJTd=clsJTclsJSlJ𝑡JclsJSclsJTkJ𝑡JclsJSclsJTcldklk=lJ𝑡JclsJSclsJTkJ𝑡JclsJSclsJTclsJSclsJTlclsJTclsJSklk=
18 11 17 imbi12d c=clsJSclsJTd=clsJTclsJScd=lJ𝑡JclsJSclsJTkJ𝑡JclsJSclsJTcldklk=clsJSclsJTclsJTclsJS=lJ𝑡JclsJSclsJTkJ𝑡JclsJSclsJTclsJSclsJTlclsJTclsJSklk=
19 18 rspc2gv clsJSclsJTClsdJ𝑡JclsJSclsJTclsJTclsJSClsdJ𝑡JclsJSclsJTcClsdJ𝑡JclsJSclsJTdClsdJ𝑡JclsJSclsJTcd=lJ𝑡JclsJSclsJTkJ𝑡JclsJSclsJTcldklk=clsJSclsJTclsJTclsJS=lJ𝑡JclsJSclsJTkJ𝑡JclsJSclsJTclsJSclsJTlclsJTclsJSklk=
20 19 3adant1 JclsJSclsJT𝒫JclsJSclsJTClsdJ𝑡JclsJSclsJTclsJTclsJSClsdJ𝑡JclsJSclsJTcClsdJ𝑡JclsJSclsJTdClsdJ𝑡JclsJSclsJTcd=lJ𝑡JclsJSclsJTkJ𝑡JclsJSclsJTcldklk=clsJSclsJTclsJTclsJS=lJ𝑡JclsJSclsJTkJ𝑡JclsJSclsJTclsJSclsJTlclsJTclsJSklk=
21 9 20 syld JclsJSclsJT𝒫JclsJSclsJTClsdJ𝑡JclsJSclsJTclsJTclsJSClsdJ𝑡JclsJSclsJTz𝒫JcClsdJ𝑡zdClsdJ𝑡zcd=lJ𝑡zkJ𝑡zcldklk=clsJSclsJTclsJTclsJS=lJ𝑡JclsJSclsJTkJ𝑡JclsJSclsJTclsJSclsJTlclsJTclsJSklk=
22 iscnrm3rlem3 JTopS𝒫JT𝒫JJclsJSclsJT𝒫JclsJSclsJTClsdJ𝑡JclsJSclsJTclsJTclsJSClsdJ𝑡JclsJSclsJT
23 22 3adant3 JTopS𝒫JT𝒫JSclsJT=clsJST=JclsJSclsJT𝒫JclsJSclsJTClsdJ𝑡JclsJSclsJTclsJTclsJSClsdJ𝑡JclsJSclsJT
24 disjdifb clsJSclsJTclsJTclsJS=
25 24 a1i JTopS𝒫JT𝒫JSclsJT=clsJST=clsJSclsJTclsJTclsJS=
26 iscnrm3rlem8 JTopS𝒫JT𝒫JSclsJT=clsJST=lJ𝑡JclsJSclsJTkJ𝑡JclsJSclsJTclsJSclsJTlclsJTclsJSklk=nJmJSnTmnm=
27 25 26 embantd JTopS𝒫JT𝒫JSclsJT=clsJST=clsJSclsJTclsJTclsJS=lJ𝑡JclsJSclsJTkJ𝑡JclsJSclsJTclsJSclsJTlclsJTclsJSklk=nJmJSnTmnm=
28 21 23 27 iscnrm3lem4 JTopz𝒫JcClsdJ𝑡zdClsdJ𝑡zcd=lJ𝑡zkJ𝑡zcldklk=S𝒫JT𝒫JSclsJT=clsJST=nJmJSnTmnm=