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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | oveq2 | |
|
2 | 1 | fveq2d | |
3 | 1 | rexeqdv | |
4 | 1 3 | rexeqbidv | |
5 | 4 | imbi2d | |
6 | 2 5 | raleqbidv | |
7 | 2 6 | raleqbidv | |
8 | 7 | rspcv | |
9 | 8 | 3ad2ant1 | |
10 | ineq12 | |
|
11 | 10 | eqeq1d | |
12 | simpl | |
|
13 | 12 | sseq1d | |
14 | simpr | |
|
15 | 14 | sseq1d | |
16 | 13 15 | 3anbi12d | |
17 | 16 | 2rexbidv | |
18 | 11 17 | imbi12d | |
19 | 18 | rspc2gv | |
20 | 19 | 3adant1 | |
21 | 9 20 | syld | |
22 | iscnrm3rlem3 | |
|
23 | 22 | 3adant3 | |
24 | disjdifb | |
|
25 | 24 | a1i | |
26 | iscnrm3rlem8 | |
|
27 | 25 26 | embantd | |
28 | 21 23 27 | iscnrm3lem4 | |