Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  iscnp2 Structured version   Visualization version   Unicode version

Theorem iscnp2 20332
 Description: The predicate " is a continuous function from topology to topology at point ." Based on Theorem 7.2(g) of [Munkres] p. 107. (Contributed by Mario Carneiro, 21-Aug-2015.)
Hypotheses
Ref Expression
iscn.1
iscn.2
Assertion
Ref Expression
iscnp2
Distinct variable groups:   ,,   ,,   ,,   ,,   ,,   ,,

Proof of Theorem iscnp2
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 n0i 3727 . . . . . . 7
2 df-ov 6311 . . . . . . . . . 10
3 ndmfv 5903 . . . . . . . . . 10
42, 3syl5eq 2517 . . . . . . . . 9
54fveq1d 5881 . . . . . . . 8
6 0fv 5912 . . . . . . . 8
75, 6syl6eq 2521 . . . . . . 7
81, 7nsyl2 132 . . . . . 6
9 df-cnp 20321 . . . . . . 7
10 ssrab2 3500 . . . . . . . . . . 11
11 ovex 6336 . . . . . . . . . . . 12
1211elpw2 4565 . . . . . . . . . . 11
1310, 12mpbir 214 . . . . . . . . . 10
1413rgenw 2768 . . . . . . . . 9
15 eqid 2471 . . . . . . . . . 10
1615fmpt 6058 . . . . . . . . 9
1714, 16mpbi 213 . . . . . . . 8
18 vex 3034 . . . . . . . . 9
1918uniex 6606 . . . . . . . 8
2011pwex 4584 . . . . . . . 8
21 fex2 6767 . . . . . . . 8
2217, 19, 20, 21mp3an 1390 . . . . . . 7
239, 22dmmpt2 6882 . . . . . 6
248, 23syl6eleq 2559 . . . . 5
25 opelxp 4869 . . . . 5
2624, 25sylib 201 . . . 4
2726simpld 466 . . 3
2826simprd 470 . . 3
29 elfvdm 5905 . . . 4
30 iscn.1 . . . . . . . . 9
3130toptopon 20025 . . . . . . . 8 TopOn
32 iscn.2 . . . . . . . . 9
3332toptopon 20025 . . . . . . . 8 TopOn
34 cnpfval 20327 . . . . . . . 8 TopOn TopOn
3531, 33, 34syl2anb 487 . . . . . . 7
3626, 35syl 17 . . . . . 6
3736dmeqd 5042 . . . . 5
38 ovex 6336 . . . . . . . 8
3938rabex 4550 . . . . . . 7
4039rgenw 2768 . . . . . 6
41 dmmptg 5339 . . . . . 6
4240, 41ax-mp 5 . . . . 5
4337, 42syl6eq 2521 . . . 4
4429, 43eleqtrd 2551 . . 3
4527, 28, 443jca 1210 . 2
46 biid 244 . . 3
47 iscnp 20330 . . 3 TopOn TopOn
4831, 33, 46, 47syl3anb 1335 . 2