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

Theorem cncnp 23304
Description: A continuous function is continuous at all points. Theorem 7.2(g) of [Munkres] p. 107. (Contributed by NM, 15-May-2007.) (Proof shortened by Mario Carneiro, 21-Aug-2015.)
Assertion
Ref Expression
cncnp ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:𝑋𝑌 ∧ ∀𝑥𝑋 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥))))
Distinct variable groups:   𝑥,𝐹   𝑥,𝐽   𝑥,𝐾   𝑥,𝑋   𝑥,𝑌

Proof of Theorem cncnp
Dummy variables 𝑢 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 iscn 23259 . . . 4 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:𝑋𝑌 ∧ ∀𝑦𝐾 (𝐹𝑦) ∈ 𝐽)))
21simprbda 498 . . 3 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐹:𝑋𝑌)
3 eqid 2735 . . . . . . 7 𝐽 = 𝐽
43cncnpi 23302 . . . . . 6 ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑥 𝐽) → 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥))
54ralrimiva 3144 . . . . 5 (𝐹 ∈ (𝐽 Cn 𝐾) → ∀𝑥 𝐽𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥))
65adantl 481 . . . 4 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → ∀𝑥 𝐽𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥))
7 toponuni 22936 . . . . 5 (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = 𝐽)
87ad2antrr 726 . . . 4 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝑋 = 𝐽)
96, 8raleqtrrdv 3328 . . 3 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → ∀𝑥𝑋 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥))
102, 9jca 511 . 2 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (𝐹:𝑋𝑌 ∧ ∀𝑥𝑋 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥)))
11 simprl 771 . . 3 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ (𝐹:𝑋𝑌 ∧ ∀𝑥𝑋 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥))) → 𝐹:𝑋𝑌)
12 cnvimass 6102 . . . . . . . . . 10 (𝐹𝑦) ⊆ dom 𝐹
13 fdm 6746 . . . . . . . . . . 11 (𝐹:𝑋𝑌 → dom 𝐹 = 𝑋)
1413adantl 481 . . . . . . . . . 10 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝑦𝐾) ∧ 𝐹:𝑋𝑌) → dom 𝐹 = 𝑋)
1512, 14sseqtrid 4048 . . . . . . . . 9 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝑦𝐾) ∧ 𝐹:𝑋𝑌) → (𝐹𝑦) ⊆ 𝑋)
16 ssralv 4064 . . . . . . . . 9 ((𝐹𝑦) ⊆ 𝑋 → (∀𝑥𝑋 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥) → ∀𝑥 ∈ (𝐹𝑦)𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥)))
1715, 16syl 17 . . . . . . . 8 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝑦𝐾) ∧ 𝐹:𝑋𝑌) → (∀𝑥𝑋 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥) → ∀𝑥 ∈ (𝐹𝑦)𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥)))
18 simprr 773 . . . . . . . . . . . 12 (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝑦𝐾) ∧ 𝐹:𝑋𝑌) ∧ (𝑥 ∈ (𝐹𝑦) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥))) → 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥))
19 simpllr 776 . . . . . . . . . . . 12 (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝑦𝐾) ∧ 𝐹:𝑋𝑌) ∧ (𝑥 ∈ (𝐹𝑦) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥))) → 𝑦𝐾)
20 ffn 6737 . . . . . . . . . . . . . 14 (𝐹:𝑋𝑌𝐹 Fn 𝑋)
2120ad2antlr 727 . . . . . . . . . . . . 13 (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝑦𝐾) ∧ 𝐹:𝑋𝑌) ∧ (𝑥 ∈ (𝐹𝑦) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥))) → 𝐹 Fn 𝑋)
22 simprl 771 . . . . . . . . . . . . 13 (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝑦𝐾) ∧ 𝐹:𝑋𝑌) ∧ (𝑥 ∈ (𝐹𝑦) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥))) → 𝑥 ∈ (𝐹𝑦))
23 elpreima 7078 . . . . . . . . . . . . . 14 (𝐹 Fn 𝑋 → (𝑥 ∈ (𝐹𝑦) ↔ (𝑥𝑋 ∧ (𝐹𝑥) ∈ 𝑦)))
2423simplbda 499 . . . . . . . . . . . . 13 ((𝐹 Fn 𝑋𝑥 ∈ (𝐹𝑦)) → (𝐹𝑥) ∈ 𝑦)
2521, 22, 24syl2anc 584 . . . . . . . . . . . 12 (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝑦𝐾) ∧ 𝐹:𝑋𝑌) ∧ (𝑥 ∈ (𝐹𝑦) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥))) → (𝐹𝑥) ∈ 𝑦)
26 cnpimaex 23280 . . . . . . . . . . . 12 ((𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥) ∧ 𝑦𝐾 ∧ (𝐹𝑥) ∈ 𝑦) → ∃𝑢𝐽 (𝑥𝑢 ∧ (𝐹𝑢) ⊆ 𝑦))
2718, 19, 25, 26syl3anc 1370 . . . . . . . . . . 11 (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝑦𝐾) ∧ 𝐹:𝑋𝑌) ∧ (𝑥 ∈ (𝐹𝑦) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥))) → ∃𝑢𝐽 (𝑥𝑢 ∧ (𝐹𝑢) ⊆ 𝑦))
28 simpllr 776 . . . . . . . . . . . . . . 15 ((((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝑦𝐾) ∧ 𝐹:𝑋𝑌) ∧ (𝑥 ∈ (𝐹𝑦) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥))) ∧ 𝑢𝐽) → 𝐹:𝑋𝑌)
2928ffund 6741 . . . . . . . . . . . . . 14 ((((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝑦𝐾) ∧ 𝐹:𝑋𝑌) ∧ (𝑥 ∈ (𝐹𝑦) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥))) ∧ 𝑢𝐽) → Fun 𝐹)
30 simp-4l 783 . . . . . . . . . . . . . . . 16 (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝑦𝐾) ∧ 𝐹:𝑋𝑌) ∧ (𝑥 ∈ (𝐹𝑦) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥))) → 𝐽 ∈ (TopOn‘𝑋))
31 toponss 22949 . . . . . . . . . . . . . . . 16 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑢𝐽) → 𝑢𝑋)
3230, 31sylan 580 . . . . . . . . . . . . . . 15 ((((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝑦𝐾) ∧ 𝐹:𝑋𝑌) ∧ (𝑥 ∈ (𝐹𝑦) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥))) ∧ 𝑢𝐽) → 𝑢𝑋)
3328, 13syl 17 . . . . . . . . . . . . . . 15 ((((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝑦𝐾) ∧ 𝐹:𝑋𝑌) ∧ (𝑥 ∈ (𝐹𝑦) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥))) ∧ 𝑢𝐽) → dom 𝐹 = 𝑋)
3432, 33sseqtrrd 4037 . . . . . . . . . . . . . 14 ((((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝑦𝐾) ∧ 𝐹:𝑋𝑌) ∧ (𝑥 ∈ (𝐹𝑦) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥))) ∧ 𝑢𝐽) → 𝑢 ⊆ dom 𝐹)
35 funimass3 7074 . . . . . . . . . . . . . 14 ((Fun 𝐹𝑢 ⊆ dom 𝐹) → ((𝐹𝑢) ⊆ 𝑦𝑢 ⊆ (𝐹𝑦)))
3629, 34, 35syl2anc 584 . . . . . . . . . . . . 13 ((((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝑦𝐾) ∧ 𝐹:𝑋𝑌) ∧ (𝑥 ∈ (𝐹𝑦) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥))) ∧ 𝑢𝐽) → ((𝐹𝑢) ⊆ 𝑦𝑢 ⊆ (𝐹𝑦)))
3736anbi2d 630 . . . . . . . . . . . 12 ((((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝑦𝐾) ∧ 𝐹:𝑋𝑌) ∧ (𝑥 ∈ (𝐹𝑦) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥))) ∧ 𝑢𝐽) → ((𝑥𝑢 ∧ (𝐹𝑢) ⊆ 𝑦) ↔ (𝑥𝑢𝑢 ⊆ (𝐹𝑦))))
3837rexbidva 3175 . . . . . . . . . . 11 (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝑦𝐾) ∧ 𝐹:𝑋𝑌) ∧ (𝑥 ∈ (𝐹𝑦) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥))) → (∃𝑢𝐽 (𝑥𝑢 ∧ (𝐹𝑢) ⊆ 𝑦) ↔ ∃𝑢𝐽 (𝑥𝑢𝑢 ⊆ (𝐹𝑦))))
3927, 38mpbid 232 . . . . . . . . . 10 (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝑦𝐾) ∧ 𝐹:𝑋𝑌) ∧ (𝑥 ∈ (𝐹𝑦) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥))) → ∃𝑢𝐽 (𝑥𝑢𝑢 ⊆ (𝐹𝑦)))
4039expr 456 . . . . . . . . 9 (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝑦𝐾) ∧ 𝐹:𝑋𝑌) ∧ 𝑥 ∈ (𝐹𝑦)) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥) → ∃𝑢𝐽 (𝑥𝑢𝑢 ⊆ (𝐹𝑦))))
4140ralimdva 3165 . . . . . . . 8 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝑦𝐾) ∧ 𝐹:𝑋𝑌) → (∀𝑥 ∈ (𝐹𝑦)𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥) → ∀𝑥 ∈ (𝐹𝑦)∃𝑢𝐽 (𝑥𝑢𝑢 ⊆ (𝐹𝑦))))
4217, 41syld 47 . . . . . . 7 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝑦𝐾) ∧ 𝐹:𝑋𝑌) → (∀𝑥𝑋 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥) → ∀𝑥 ∈ (𝐹𝑦)∃𝑢𝐽 (𝑥𝑢𝑢 ⊆ (𝐹𝑦))))
4342impr 454 . . . . . 6 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝑦𝐾) ∧ (𝐹:𝑋𝑌 ∧ ∀𝑥𝑋 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥))) → ∀𝑥 ∈ (𝐹𝑦)∃𝑢𝐽 (𝑥𝑢𝑢 ⊆ (𝐹𝑦)))
4443an32s 652 . . . . 5 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ (𝐹:𝑋𝑌 ∧ ∀𝑥𝑋 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥))) ∧ 𝑦𝐾) → ∀𝑥 ∈ (𝐹𝑦)∃𝑢𝐽 (𝑥𝑢𝑢 ⊆ (𝐹𝑦)))
45 topontop 22935 . . . . . . 7 (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top)
4645ad3antrrr 730 . . . . . 6 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ (𝐹:𝑋𝑌 ∧ ∀𝑥𝑋 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥))) ∧ 𝑦𝐾) → 𝐽 ∈ Top)
47 eltop2 22998 . . . . . 6 (𝐽 ∈ Top → ((𝐹𝑦) ∈ 𝐽 ↔ ∀𝑥 ∈ (𝐹𝑦)∃𝑢𝐽 (𝑥𝑢𝑢 ⊆ (𝐹𝑦))))
4846, 47syl 17 . . . . 5 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ (𝐹:𝑋𝑌 ∧ ∀𝑥𝑋 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥))) ∧ 𝑦𝐾) → ((𝐹𝑦) ∈ 𝐽 ↔ ∀𝑥 ∈ (𝐹𝑦)∃𝑢𝐽 (𝑥𝑢𝑢 ⊆ (𝐹𝑦))))
4944, 48mpbird 257 . . . 4 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ (𝐹:𝑋𝑌 ∧ ∀𝑥𝑋 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥))) ∧ 𝑦𝐾) → (𝐹𝑦) ∈ 𝐽)
5049ralrimiva 3144 . . 3 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ (𝐹:𝑋𝑌 ∧ ∀𝑥𝑋 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥))) → ∀𝑦𝐾 (𝐹𝑦) ∈ 𝐽)
511adantr 480 . . 3 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ (𝐹:𝑋𝑌 ∧ ∀𝑥𝑋 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥))) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:𝑋𝑌 ∧ ∀𝑦𝐾 (𝐹𝑦) ∈ 𝐽)))
5211, 50, 51mpbir2and 713 . 2 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ (𝐹:𝑋𝑌 ∧ ∀𝑥𝑋 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥))) → 𝐹 ∈ (𝐽 Cn 𝐾))
5310, 52impbida 801 1 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:𝑋𝑌 ∧ ∀𝑥𝑋 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1537  wcel 2106  wral 3059  wrex 3068  wss 3963   cuni 4912  ccnv 5688  dom cdm 5689  cima 5692  Fun wfun 6557   Fn wfn 6558  wf 6559  cfv 6563  (class class class)co 7431  Topctop 22915  TopOnctopon 22932   Cn ccn 23248   CnP ccnp 23249
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5583  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-fv 6571  df-ov 7434  df-oprab 7435  df-mpo 7436  df-1st 8013  df-2nd 8014  df-map 8867  df-topgen 17490  df-top 22916  df-topon 22933  df-cn 23251  df-cnp 23252
This theorem is referenced by:  cncnp2  23305  cnnei  23306  cnconst2  23307  1stccn  23487  ptcn  23651  cnflf  24026  cnfcf  24066  symgtgp  24130  ghmcnp  24139  metcn  24572  txmetcn  24577  cnlimc  25938  dvcn  25972  dvcnvre  26073  psercn  26485  abelth  26500  cxpcn3  26806  cvmlift2lem11  35298  cvmlift2lem12  35299  cvmlift3lem8  35311  ioccncflimc  45841  cncfuni  45842  icccncfext  45843  icocncflimc  45845  cncfiooicclem1  45849  dirkercncflem2  46060  dirkercncflem4  46062  dirkercncf  46063  fourierdlem32  46095  fourierdlem33  46096  fourierdlem62  46124  fourierdlem93  46155  fourierdlem101  46163
  Copyright terms: Public domain W3C validator