Theorem cncnp 21885

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.

Step	Hyp	Ref	Expression
1		iscn 21840	. . . 4 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ 𝐾 (◡𝐹 “ 𝑦) ∈ 𝐽)))
2	1	simprbda 502	. . 3 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐹:𝑋⟶𝑌)
3		eqid 2798	. . . . . . 7 ⊢ ∪ 𝐽 = ∪ 𝐽
4	3	cncnpi 21883	. . . . . 6 ⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑥 ∈ ∪ 𝐽) → 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥))
5	4	ralrimiva 3149	. . . . 5 ⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → ∀𝑥 ∈ ∪ 𝐽𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥))
6	5	adantl 485	. . . 4 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → ∀𝑥 ∈ ∪ 𝐽𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥))
7		toponuni 21519	. . . . . 6 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝐽)
8	7	ad2antrr 725	. . . . 5 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝑋 = ∪ 𝐽)
9	8	raleqdv 3364	. . . 4 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (∀𝑥 ∈ 𝑋 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥) ↔ ∀𝑥 ∈ ∪ 𝐽𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥)))
10	6, 9	mpbird 260	. . 3 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → ∀𝑥 ∈ 𝑋 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥))
11	2, 10	jca 515	. 2 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (𝐹:𝑋⟶𝑌 ∧ ∀𝑥 ∈ 𝑋 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥)))
12		simprl 770	. . 3 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ (𝐹:𝑋⟶𝑌 ∧ ∀𝑥 ∈ 𝑋 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥))) → 𝐹:𝑋⟶𝑌)
13		cnvimass 5916	. . . . . . . . . 10 ⊢ (◡𝐹 “ 𝑦) ⊆ dom 𝐹
14		fdm 6495	. . . . . . . . . . 11 ⊢ (𝐹:𝑋⟶𝑌 → dom 𝐹 = 𝑋)
15	14	adantl 485	. . . . . . . . . 10 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝑦 ∈ 𝐾) ∧ 𝐹:𝑋⟶𝑌) → dom 𝐹 = 𝑋)
16	13, 15	sseqtrid 3967	. . . . . . . . 9 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝑦 ∈ 𝐾) ∧ 𝐹:𝑋⟶𝑌) → (◡𝐹 “ 𝑦) ⊆ 𝑋)
17		ssralv 3981	. . . . . . . . 9 ⊢ ((◡𝐹 “ 𝑦) ⊆ 𝑋 → (∀𝑥 ∈ 𝑋 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥) → ∀𝑥 ∈ (◡𝐹 “ 𝑦)𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥)))
18	16, 17	syl 17	. . . . . . . 8 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝑦 ∈ 𝐾) ∧ 𝐹:𝑋⟶𝑌) → (∀𝑥 ∈ 𝑋 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥) → ∀𝑥 ∈ (◡𝐹 “ 𝑦)𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥)))
19		simprr 772	. . . . . . . . . . . 12 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝑦 ∈ 𝐾) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑥 ∈ (◡𝐹 “ 𝑦) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥))) → 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥))
20		simpllr 775	. . . . . . . . . . . 12 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝑦 ∈ 𝐾) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑥 ∈ (◡𝐹 “ 𝑦) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥))) → 𝑦 ∈ 𝐾)
21		ffn 6487	. . . . . . . . . . . . . 14 ⊢ (𝐹:𝑋⟶𝑌 → 𝐹 Fn 𝑋)
22	21	ad2antlr 726	. . . . . . . . . . . . 13 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝑦 ∈ 𝐾) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑥 ∈ (◡𝐹 “ 𝑦) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥))) → 𝐹 Fn 𝑋)
23		simprl 770	. . . . . . . . . . . . 13 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝑦 ∈ 𝐾) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑥 ∈ (◡𝐹 “ 𝑦) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥))) → 𝑥 ∈ (◡𝐹 “ 𝑦))
24		elpreima 6805	. . . . . . . . . . . . . 14 ⊢ (𝐹 Fn 𝑋 → (𝑥 ∈ (◡𝐹 “ 𝑦) ↔ (𝑥 ∈ 𝑋 ∧ (𝐹‘𝑥) ∈ 𝑦)))
25	24	simplbda 503	. . . . . . . . . . . . 13 ⊢ ((𝐹 Fn 𝑋 ∧ 𝑥 ∈ (◡𝐹 “ 𝑦)) → (𝐹‘𝑥) ∈ 𝑦)
26	22, 23, 25	syl2anc 587	. . . . . . . . . . . 12 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝑦 ∈ 𝐾) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑥 ∈ (◡𝐹 “ 𝑦) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥))) → (𝐹‘𝑥) ∈ 𝑦)
27		cnpimaex 21861	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥) ∧ 𝑦 ∈ 𝐾 ∧ (𝐹‘𝑥) ∈ 𝑦) → ∃𝑢 ∈ 𝐽 (𝑥 ∈ 𝑢 ∧ (𝐹 “ 𝑢) ⊆ 𝑦))
28	19, 20, 26, 27	syl3anc 1368	. . . . . . . . . . 11 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝑦 ∈ 𝐾) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑥 ∈ (◡𝐹 “ 𝑦) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥))) → ∃𝑢 ∈ 𝐽 (𝑥 ∈ 𝑢 ∧ (𝐹 “ 𝑢) ⊆ 𝑦))
29		simpllr 775	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝑦 ∈ 𝐾) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑥 ∈ (◡𝐹 “ 𝑦) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥))) ∧ 𝑢 ∈ 𝐽) → 𝐹:𝑋⟶𝑌)
30	29	ffund 6491	. . . . . . . . . . . . . 14 ⊢ ((((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝑦 ∈ 𝐾) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑥 ∈ (◡𝐹 “ 𝑦) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥))) ∧ 𝑢 ∈ 𝐽) → Fun 𝐹)
31		simp-4l 782	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝑦 ∈ 𝐾) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑥 ∈ (◡𝐹 “ 𝑦) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥))) → 𝐽 ∈ (TopOn‘𝑋))
32		toponss 21532	. . . . . . . . . . . . . . . 16 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑢 ∈ 𝐽) → 𝑢 ⊆ 𝑋)
33	31, 32	sylan 583	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝑦 ∈ 𝐾) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑥 ∈ (◡𝐹 “ 𝑦) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥))) ∧ 𝑢 ∈ 𝐽) → 𝑢 ⊆ 𝑋)
34	29, 14	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝑦 ∈ 𝐾) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑥 ∈ (◡𝐹 “ 𝑦) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥))) ∧ 𝑢 ∈ 𝐽) → dom 𝐹 = 𝑋)
35	33, 34	sseqtrrd 3956	. . . . . . . . . . . . . 14 ⊢ ((((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝑦 ∈ 𝐾) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑥 ∈ (◡𝐹 “ 𝑦) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥))) ∧ 𝑢 ∈ 𝐽) → 𝑢 ⊆ dom 𝐹)
36		funimass3 6801	. . . . . . . . . . . . . 14 ⊢ ((Fun 𝐹 ∧ 𝑢 ⊆ dom 𝐹) → ((𝐹 “ 𝑢) ⊆ 𝑦 ↔ 𝑢 ⊆ (◡𝐹 “ 𝑦)))
37	30, 35, 36	syl2anc 587	. . . . . . . . . . . . 13 ⊢ ((((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝑦 ∈ 𝐾) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑥 ∈ (◡𝐹 “ 𝑦) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥))) ∧ 𝑢 ∈ 𝐽) → ((𝐹 “ 𝑢) ⊆ 𝑦 ↔ 𝑢 ⊆ (◡𝐹 “ 𝑦)))
38	37	anbi2d 631	. . . . . . . . . . . 12 ⊢ ((((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝑦 ∈ 𝐾) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑥 ∈ (◡𝐹 “ 𝑦) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥))) ∧ 𝑢 ∈ 𝐽) → ((𝑥 ∈ 𝑢 ∧ (𝐹 “ 𝑢) ⊆ 𝑦) ↔ (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ (◡𝐹 “ 𝑦))))
39	38	rexbidva 3255	. . . . . . . . . . 11 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝑦 ∈ 𝐾) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑥 ∈ (◡𝐹 “ 𝑦) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥))) → (∃𝑢 ∈ 𝐽 (𝑥 ∈ 𝑢 ∧ (𝐹 “ 𝑢) ⊆ 𝑦) ↔ ∃𝑢 ∈ 𝐽 (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ (◡𝐹 “ 𝑦))))
40	28, 39	mpbid 235	. . . . . . . . . 10 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝑦 ∈ 𝐾) ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑥 ∈ (◡𝐹 “ 𝑦) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥))) → ∃𝑢 ∈ 𝐽 (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ (◡𝐹 “ 𝑦)))
41	40	expr 460	. . . . . . . . 9 ⊢ (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝑦 ∈ 𝐾) ∧ 𝐹:𝑋⟶𝑌) ∧ 𝑥 ∈ (◡𝐹 “ 𝑦)) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥) → ∃𝑢 ∈ 𝐽 (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ (◡𝐹 “ 𝑦))))
42	41	ralimdva 3144	. . . . . . . 8 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝑦 ∈ 𝐾) ∧ 𝐹:𝑋⟶𝑌) → (∀𝑥 ∈ (◡𝐹 “ 𝑦)𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥) → ∀𝑥 ∈ (◡𝐹 “ 𝑦)∃𝑢 ∈ 𝐽 (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ (◡𝐹 “ 𝑦))))
43	18, 42	syld 47	. . . . . . 7 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝑦 ∈ 𝐾) ∧ 𝐹:𝑋⟶𝑌) → (∀𝑥 ∈ 𝑋 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥) → ∀𝑥 ∈ (◡𝐹 “ 𝑦)∃𝑢 ∈ 𝐽 (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ (◡𝐹 “ 𝑦))))
44	43	impr 458	. . . . . 6 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝑦 ∈ 𝐾) ∧ (𝐹:𝑋⟶𝑌 ∧ ∀𝑥 ∈ 𝑋 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥))) → ∀𝑥 ∈ (◡𝐹 “ 𝑦)∃𝑢 ∈ 𝐽 (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ (◡𝐹 “ 𝑦)))
45	44	an32s 651	. . . . 5 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ (𝐹:𝑋⟶𝑌 ∧ ∀𝑥 ∈ 𝑋 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥))) ∧ 𝑦 ∈ 𝐾) → ∀𝑥 ∈ (◡𝐹 “ 𝑦)∃𝑢 ∈ 𝐽 (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ (◡𝐹 “ 𝑦)))
46		topontop 21518	. . . . . . 7 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top)
47	46	ad3antrrr 729	. . . . . 6 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ (𝐹:𝑋⟶𝑌 ∧ ∀𝑥 ∈ 𝑋 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥))) ∧ 𝑦 ∈ 𝐾) → 𝐽 ∈ Top)
48		eltop2 21580	. . . . . 6 ⊢ (𝐽 ∈ Top → ((◡𝐹 “ 𝑦) ∈ 𝐽 ↔ ∀𝑥 ∈ (◡𝐹 “ 𝑦)∃𝑢 ∈ 𝐽 (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ (◡𝐹 “ 𝑦))))
49	47, 48	syl 17	. . . . 5 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ (𝐹:𝑋⟶𝑌 ∧ ∀𝑥 ∈ 𝑋 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥))) ∧ 𝑦 ∈ 𝐾) → ((◡𝐹 “ 𝑦) ∈ 𝐽 ↔ ∀𝑥 ∈ (◡𝐹 “ 𝑦)∃𝑢 ∈ 𝐽 (𝑥 ∈ 𝑢 ∧ 𝑢 ⊆ (◡𝐹 “ 𝑦))))
50	45, 49	mpbird 260	. . . 4 ⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ (𝐹:𝑋⟶𝑌 ∧ ∀𝑥 ∈ 𝑋 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥))) ∧ 𝑦 ∈ 𝐾) → (◡𝐹 “ 𝑦) ∈ 𝐽)
51	50	ralrimiva 3149	. . 3 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ (𝐹:𝑋⟶𝑌 ∧ ∀𝑥 ∈ 𝑋 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥))) → ∀𝑦 ∈ 𝐾 (◡𝐹 “ 𝑦) ∈ 𝐽)
52	1	adantr 484	. . 3 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ (𝐹:𝑋⟶𝑌 ∧ ∀𝑥 ∈ 𝑋 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥))) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ 𝐾 (◡𝐹 “ 𝑦) ∈ 𝐽)))
53	12, 51, 52	mpbir2and 712	. 2 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ (𝐹:𝑋⟶𝑌 ∧ ∀𝑥 ∈ 𝑋 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥))) → 𝐹 ∈ (𝐽 Cn 𝐾))
54	11, 53	impbida 800	1 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑥 ∈ 𝑋 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥))))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   ∈ wcel 2111  ∀wral 3106  ∃wrex 3107   ⊆ wss 3881  ∪ cuni 4800  ^◡ccnv 5518  dom cdm 5519   “ cima 5522  Fun wfun 6318   Fn wfn 6319  ⟶wf 6320  ‘cfv 6324  (class class class)co 7135  Topctop 21498  TopOnctopon 21515   Cn ccn 21829   CnP ccnp 21830

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-id 5425  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-fv 6332  df-ov 7138  df-oprab 7139  df-mpo 7140  df-1st 7671  df-2nd 7672  df-map 8391  df-topgen 16709  df-top 21499  df-topon 21516  df-cn 21832  df-cnp 21833

This theorem is referenced by:  cncnp2  21886  cnnei  21887  cnconst2  21888  1stccn  22068  ptcn  22232  cnflf  22607  cnfcf  22647  symgtgp  22711  ghmcnp  22720  metcn  23150  txmetcn  23155  cnlimc  24491  dvcn  24524  dvcnvre  24622  psercn  25021  abelth  25036  cxpcn3  25337  cvmlift2lem11  32673  cvmlift2lem12  32674  cvmlift3lem8  32686  ioccncflimc  42527  cncfuni  42528  icccncfext  42529  icocncflimc  42531  cncfiooicclem1  42535  dirkercncflem2  42746  dirkercncflem4  42748  dirkercncf  42749  fourierdlem32  42781  fourierdlem33  42782  fourierdlem62  42810  fourierdlem93  42841  fourierdlem101  42849