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

Theorem iscnp2 17303
 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 3633 . . . . . . 7
2 df-ov 6084 . . . . . . . . . 10
3 ndmfv 5755 . . . . . . . . . 10
42, 3syl5eq 2480 . . . . . . . . 9
54fveq1d 5730 . . . . . . . 8
6 fv01 5763 . . . . . . . 8
75, 6syl6eq 2484 . . . . . . 7
81, 7nsyl2 121 . . . . . 6
9 df-cnp 17292 . . . . . . 7
10 ssrab2 3428 . . . . . . . . . . 11
11 ovex 6106 . . . . . . . . . . . 12
1211elpw2 4364 . . . . . . . . . . 11
1310, 12mpbir 201 . . . . . . . . . 10
1413rgenw 2773 . . . . . . . . 9
15 eqid 2436 . . . . . . . . . 10
1615fmpt 5890 . . . . . . . . 9
1714, 16mpbi 200 . . . . . . . 8
18 vex 2959 . . . . . . . . 9
1918uniex 4705 . . . . . . . 8
2011pwex 4382 . . . . . . . 8
21 fex2 5603 . . . . . . . 8
2217, 19, 20, 21mp3an 1279 . . . . . . 7
239, 22dmmpt2 6421 . . . . . 6
248, 23syl6eleq 2526 . . . . 5
25 opelxp 4908 . . . . 5
2624, 25sylib 189 . . . 4
2726simpld 446 . . 3
2826simprd 450 . . 3
29 elfvdm 5757 . . . 4
30 iscn.1 . . . . . . . . 9
3130toptopon 16998 . . . . . . . 8 TopOn
32 iscn.2 . . . . . . . . 9
3332toptopon 16998 . . . . . . . 8 TopOn
34 cnpfval 17298 . . . . . . . 8 TopOn TopOn
3531, 33, 34syl2anb 466 . . . . . . 7
3626, 35syl 16 . . . . . 6
3736dmeqd 5072 . . . . 5
38 ovex 6106 . . . . . . . 8
3938rabex 4354 . . . . . . 7
4039rgenw 2773 . . . . . 6
41 dmmptg 5367 . . . . . 6
4240, 41ax-mp 8 . . . . 5
4337, 42syl6eq 2484 . . . 4
4429, 43eleqtrd 2512 . . 3
4527, 28, 443jca 1134 . 2
46 biid 228 . . 3
47 iscnp 17301 . . 3 TopOn TopOn
4831, 33, 46, 47syl3anb 1227 . 2