Theorem cnprest2 23210

Description: Equivalence of point-continuity in the parent topology and point-continuity in a subspace. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 21-Aug-2015.)

Hypotheses

Ref	Expression
cnprest.1	⊢ 𝑋 = ∪ 𝐽
cnprest.2	⊢ 𝑌 = ∪ 𝐾

Assertion

Ref	Expression
cnprest2	⊢ ((𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝐵 ∧ 𝐵 ⊆ 𝑌) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ 𝐹 ∈ ((𝐽 CnP (𝐾 ↾t 𝐵))‘𝑃)))

Proof of Theorem cnprest2

Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		cnptop1 23162	. . . 4 ⊢ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) → 𝐽 ∈ Top)
2		cnprest.1	. . . . 5 ⊢ 𝑋 = ∪ 𝐽
3	2	cnprcl 23165	. . . 4 ⊢ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) → 𝑃 ∈ 𝑋)
4	1, 3	jca 511	. . 3 ⊢ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) → (𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋))
5	4	a1i 11	. 2 ⊢ ((𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝐵 ∧ 𝐵 ⊆ 𝑌) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) → (𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋)))
6		cnptop1 23162	. . . 4 ⊢ (𝐹 ∈ ((𝐽 CnP (𝐾 ↾t 𝐵))‘𝑃) → 𝐽 ∈ Top)
7	2	cnprcl 23165	. . . 4 ⊢ (𝐹 ∈ ((𝐽 CnP (𝐾 ↾t 𝐵))‘𝑃) → 𝑃 ∈ 𝑋)
8	6, 7	jca 511	. . 3 ⊢ (𝐹 ∈ ((𝐽 CnP (𝐾 ↾t 𝐵))‘𝑃) → (𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋))
9	8	a1i 11	. 2 ⊢ ((𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝐵 ∧ 𝐵 ⊆ 𝑌) → (𝐹 ∈ ((𝐽 CnP (𝐾 ↾t 𝐵))‘𝑃) → (𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋)))
10		simpl2 1193	. . . . . . . . . 10 ⊢ (((𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋)) → 𝐹:𝑋⟶𝐵)
11		simprr 772	. . . . . . . . . 10 ⊢ (((𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋)) → 𝑃 ∈ 𝑋)
12	10, 11	ffvelcdmd 7039	. . . . . . . . 9 ⊢ (((𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋)) → (𝐹‘𝑃) ∈ 𝐵)
13	12	biantrud 531	. . . . . . . 8 ⊢ (((𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋)) → ((𝐹‘𝑃) ∈ 𝑥 ↔ ((𝐹‘𝑃) ∈ 𝑥 ∧ (𝐹‘𝑃) ∈ 𝐵)))
14		elin 3927	. . . . . . . 8 ⊢ ((𝐹‘𝑃) ∈ (𝑥 ∩ 𝐵) ↔ ((𝐹‘𝑃) ∈ 𝑥 ∧ (𝐹‘𝑃) ∈ 𝐵))
15	13, 14	bitr4di 289	. . . . . . 7 ⊢ (((𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋)) → ((𝐹‘𝑃) ∈ 𝑥 ↔ (𝐹‘𝑃) ∈ (𝑥 ∩ 𝐵)))
16		imassrn 6031	. . . . . . . . . . . 12 ⊢ (𝐹 “ 𝑦) ⊆ ran 𝐹
17	10	frnd 6678	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋)) → ran 𝐹 ⊆ 𝐵)
18	16, 17	sstrid 3955	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋)) → (𝐹 “ 𝑦) ⊆ 𝐵)
19	18	biantrud 531	. . . . . . . . . 10 ⊢ (((𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋)) → ((𝐹 “ 𝑦) ⊆ 𝑥 ↔ ((𝐹 “ 𝑦) ⊆ 𝑥 ∧ (𝐹 “ 𝑦) ⊆ 𝐵)))
20		ssin 4198	. . . . . . . . . 10 ⊢ (((𝐹 “ 𝑦) ⊆ 𝑥 ∧ (𝐹 “ 𝑦) ⊆ 𝐵) ↔ (𝐹 “ 𝑦) ⊆ (𝑥 ∩ 𝐵))
21	19, 20	bitrdi 287	. . . . . . . . 9 ⊢ (((𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋)) → ((𝐹 “ 𝑦) ⊆ 𝑥 ↔ (𝐹 “ 𝑦) ⊆ (𝑥 ∩ 𝐵)))
22	21	anbi2d 630	. . . . . . . 8 ⊢ (((𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋)) → ((𝑃 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑥) ↔ (𝑃 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ (𝑥 ∩ 𝐵))))
23	22	rexbidv 3157	. . . . . . 7 ⊢ (((𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋)) → (∃𝑦 ∈ 𝐽 (𝑃 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑥) ↔ ∃𝑦 ∈ 𝐽 (𝑃 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ (𝑥 ∩ 𝐵))))
24	15, 23	imbi12d 344	. . . . . 6 ⊢ (((𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋)) → (((𝐹‘𝑃) ∈ 𝑥 → ∃𝑦 ∈ 𝐽 (𝑃 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑥)) ↔ ((𝐹‘𝑃) ∈ (𝑥 ∩ 𝐵) → ∃𝑦 ∈ 𝐽 (𝑃 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ (𝑥 ∩ 𝐵)))))
25	24	ralbidv 3156	. . . . 5 ⊢ (((𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋)) → (∀𝑥 ∈ 𝐾 ((𝐹‘𝑃) ∈ 𝑥 → ∃𝑦 ∈ 𝐽 (𝑃 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑥)) ↔ ∀𝑥 ∈ 𝐾 ((𝐹‘𝑃) ∈ (𝑥 ∩ 𝐵) → ∃𝑦 ∈ 𝐽 (𝑃 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ (𝑥 ∩ 𝐵)))))
26		vex 3448	. . . . . . . 8 ⊢ 𝑥 ∈ V
27	26	inex1 5267	. . . . . . 7 ⊢ (𝑥 ∩ 𝐵) ∈ V
28	27	a1i 11	. . . . . 6 ⊢ ((((𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋)) ∧ 𝑥 ∈ 𝐾) → (𝑥 ∩ 𝐵) ∈ V)
29		simpl1 1192	. . . . . . 7 ⊢ (((𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋)) → 𝐾 ∈ Top)
30		cnprest.2	. . . . . . . . . 10 ⊢ 𝑌 = ∪ 𝐾
31		uniexg 7696	. . . . . . . . . 10 ⊢ (𝐾 ∈ Top → ∪ 𝐾 ∈ V)
32	30, 31	eqeltrid 2832	. . . . . . . . 9 ⊢ (𝐾 ∈ Top → 𝑌 ∈ V)
33	29, 32	syl 17	. . . . . . . 8 ⊢ (((𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋)) → 𝑌 ∈ V)
34		simpl3 1194	. . . . . . . 8 ⊢ (((𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋)) → 𝐵 ⊆ 𝑌)
35	33, 34	ssexd 5274	. . . . . . 7 ⊢ (((𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋)) → 𝐵 ∈ V)
36		elrest 17366	. . . . . . 7 ⊢ ((𝐾 ∈ Top ∧ 𝐵 ∈ V) → (𝑧 ∈ (𝐾 ↾t 𝐵) ↔ ∃𝑥 ∈ 𝐾 𝑧 = (𝑥 ∩ 𝐵)))
37	29, 35, 36	syl2anc 584	. . . . . 6 ⊢ (((𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋)) → (𝑧 ∈ (𝐾 ↾t 𝐵) ↔ ∃𝑥 ∈ 𝐾 𝑧 = (𝑥 ∩ 𝐵)))
38		eleq2 2817	. . . . . . . 8 ⊢ (𝑧 = (𝑥 ∩ 𝐵) → ((𝐹‘𝑃) ∈ 𝑧 ↔ (𝐹‘𝑃) ∈ (𝑥 ∩ 𝐵)))
39		sseq2 3970	. . . . . . . . . 10 ⊢ (𝑧 = (𝑥 ∩ 𝐵) → ((𝐹 “ 𝑦) ⊆ 𝑧 ↔ (𝐹 “ 𝑦) ⊆ (𝑥 ∩ 𝐵)))
40	39	anbi2d 630	. . . . . . . . 9 ⊢ (𝑧 = (𝑥 ∩ 𝐵) → ((𝑃 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑧) ↔ (𝑃 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ (𝑥 ∩ 𝐵))))
41	40	rexbidv 3157	. . . . . . . 8 ⊢ (𝑧 = (𝑥 ∩ 𝐵) → (∃𝑦 ∈ 𝐽 (𝑃 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑧) ↔ ∃𝑦 ∈ 𝐽 (𝑃 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ (𝑥 ∩ 𝐵))))
42	38, 41	imbi12d 344	. . . . . . 7 ⊢ (𝑧 = (𝑥 ∩ 𝐵) → (((𝐹‘𝑃) ∈ 𝑧 → ∃𝑦 ∈ 𝐽 (𝑃 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑧)) ↔ ((𝐹‘𝑃) ∈ (𝑥 ∩ 𝐵) → ∃𝑦 ∈ 𝐽 (𝑃 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ (𝑥 ∩ 𝐵)))))
43	42	adantl 481	. . . . . 6 ⊢ ((((𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋)) ∧ 𝑧 = (𝑥 ∩ 𝐵)) → (((𝐹‘𝑃) ∈ 𝑧 → ∃𝑦 ∈ 𝐽 (𝑃 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑧)) ↔ ((𝐹‘𝑃) ∈ (𝑥 ∩ 𝐵) → ∃𝑦 ∈ 𝐽 (𝑃 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ (𝑥 ∩ 𝐵)))))
44	28, 37, 43	ralxfr2d 5360	. . . . 5 ⊢ (((𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋)) → (∀𝑧 ∈ (𝐾 ↾t 𝐵)((𝐹‘𝑃) ∈ 𝑧 → ∃𝑦 ∈ 𝐽 (𝑃 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑧)) ↔ ∀𝑥 ∈ 𝐾 ((𝐹‘𝑃) ∈ (𝑥 ∩ 𝐵) → ∃𝑦 ∈ 𝐽 (𝑃 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ (𝑥 ∩ 𝐵)))))
45	25, 44	bitr4d 282	. . . 4 ⊢ (((𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋)) → (∀𝑥 ∈ 𝐾 ((𝐹‘𝑃) ∈ 𝑥 → ∃𝑦 ∈ 𝐽 (𝑃 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑥)) ↔ ∀𝑧 ∈ (𝐾 ↾t 𝐵)((𝐹‘𝑃) ∈ 𝑧 → ∃𝑦 ∈ 𝐽 (𝑃 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑧))))
46	10, 34	fssd 6687	. . . . 5 ⊢ (((𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋)) → 𝐹:𝑋⟶𝑌)
47		simprl 770	. . . . . 6 ⊢ (((𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋)) → 𝐽 ∈ Top)
48	2, 30	iscnp2 23159	. . . . . . 7 ⊢ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝑃 ∈ 𝑋) ∧ (𝐹:𝑋⟶𝑌 ∧ ∀𝑥 ∈ 𝐾 ((𝐹‘𝑃) ∈ 𝑥 → ∃𝑦 ∈ 𝐽 (𝑃 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑥)))))
49	48	baib 535	. . . . . 6 ⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝑃 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑥 ∈ 𝐾 ((𝐹‘𝑃) ∈ 𝑥 → ∃𝑦 ∈ 𝐽 (𝑃 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑥)))))
50	47, 29, 11, 49	syl3anc 1373	. . . . 5 ⊢ (((𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋)) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑥 ∈ 𝐾 ((𝐹‘𝑃) ∈ 𝑥 → ∃𝑦 ∈ 𝐽 (𝑃 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑥)))))
51	46, 50	mpbirand 707	. . . 4 ⊢ (((𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋)) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ ∀𝑥 ∈ 𝐾 ((𝐹‘𝑃) ∈ 𝑥 → ∃𝑦 ∈ 𝐽 (𝑃 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑥))))
52	2	toptopon 22837	. . . . . . 7 ⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋))
53	47, 52	sylib 218	. . . . . 6 ⊢ (((𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋)) → 𝐽 ∈ (TopOn‘𝑋))
54	30	toptopon 22837	. . . . . . . 8 ⊢ (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘𝑌))
55	29, 54	sylib 218	. . . . . . 7 ⊢ (((𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋)) → 𝐾 ∈ (TopOn‘𝑌))
56		resttopon 23081	. . . . . . 7 ⊢ ((𝐾 ∈ (TopOn‘𝑌) ∧ 𝐵 ⊆ 𝑌) → (𝐾 ↾t 𝐵) ∈ (TopOn‘𝐵))
57	55, 34, 56	syl2anc 584	. . . . . 6 ⊢ (((𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋)) → (𝐾 ↾t 𝐵) ∈ (TopOn‘𝐵))
58		iscnp 23157	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝐾 ↾t 𝐵) ∈ (TopOn‘𝐵) ∧ 𝑃 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP (𝐾 ↾t 𝐵))‘𝑃) ↔ (𝐹:𝑋⟶𝐵 ∧ ∀𝑧 ∈ (𝐾 ↾t 𝐵)((𝐹‘𝑃) ∈ 𝑧 → ∃𝑦 ∈ 𝐽 (𝑃 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑧)))))
59	53, 57, 11, 58	syl3anc 1373	. . . . 5 ⊢ (((𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋)) → (𝐹 ∈ ((𝐽 CnP (𝐾 ↾t 𝐵))‘𝑃) ↔ (𝐹:𝑋⟶𝐵 ∧ ∀𝑧 ∈ (𝐾 ↾t 𝐵)((𝐹‘𝑃) ∈ 𝑧 → ∃𝑦 ∈ 𝐽 (𝑃 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑧)))))
60	10, 59	mpbirand 707	. . . 4 ⊢ (((𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋)) → (𝐹 ∈ ((𝐽 CnP (𝐾 ↾t 𝐵))‘𝑃) ↔ ∀𝑧 ∈ (𝐾 ↾t 𝐵)((𝐹‘𝑃) ∈ 𝑧 → ∃𝑦 ∈ 𝐽 (𝑃 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑧))))
61	45, 51, 60	3bitr4d 311	. . 3 ⊢ (((𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋)) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ 𝐹 ∈ ((𝐽 CnP (𝐾 ↾t 𝐵))‘𝑃)))
62	61	ex 412	. 2 ⊢ ((𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝐵 ∧ 𝐵 ⊆ 𝑌) → ((𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ 𝐹 ∈ ((𝐽 CnP (𝐾 ↾t 𝐵))‘𝑃))))
63	5, 9, 62	pm5.21ndd 379	1 ⊢ ((𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝐵 ∧ 𝐵 ⊆ 𝑌) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ 𝐹 ∈ ((𝐽 CnP (𝐾 ↾t 𝐵))‘𝑃)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109  ∀wral 3044  ∃wrex 3053  Vcvv 3444   ∩ cin 3910   ⊆ wss 3911  ∪ cuni 4867  ran crn 5632   “ cima 5634  ⟶wf 6495  ‘cfv 6499  (class class class)co 7369   ↾_t crest 17359  Topctop 22813  TopOnctopon 22830   CnP ccnp 23145

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-rep 5229  ax-sep 5246  ax-nul 5256  ax-pow 5315  ax-pr 5382  ax-un 7691

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-reu 3352  df-rab 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3931  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-int 4907  df-iun 4953  df-br 5103  df-opab 5165  df-mpt 5184  df-tr 5210  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-ord 6323  df-on 6324  df-lim 6325  df-suc 6326  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-ov 7372  df-oprab 7373  df-mpo 7374  df-om 7823  df-1st 7947  df-2nd 7948  df-map 8778  df-en 8896  df-fin 8899  df-fi 9338  df-rest 17361  df-topgen 17382  df-top 22814  df-topon 22831  df-bases 22866  df-cnp 23148

This theorem is referenced by:  limccnp  25825  limccnp2  25826  dirkercncflem4  46097  dirkercncf  46098  fouriercnp  46217