Theorem cnprest2 23233

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 23185	. . . 4 ⊢ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) → 𝐽 ∈ Top)
2		cnprest.1	. . . . 5 ⊢ 𝑋 = ∪ 𝐽
3	2	cnprcl 23188	. . . 4 ⊢ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) → 𝑃 ∈ 𝑋)
4	1, 3	jca 511	. . 3 ⊢ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) → (𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋))
5	4	a1i 11	. 2 ⊢ ((𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝐵 ∧ 𝐵 ⊆ 𝑌) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) → (𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋)))
6		cnptop1 23185	. . . 4 ⊢ (𝐹 ∈ ((𝐽 CnP (𝐾 ↾t 𝐵))‘𝑃) → 𝐽 ∈ Top)
7	2	cnprcl 23188	. . . 4 ⊢ (𝐹 ∈ ((𝐽 CnP (𝐾 ↾t 𝐵))‘𝑃) → 𝑃 ∈ 𝑋)
8	6, 7	jca 511	. . 3 ⊢ (𝐹 ∈ ((𝐽 CnP (𝐾 ↾t 𝐵))‘𝑃) → (𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋))
9	8	a1i 11	. 2 ⊢ ((𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝐵 ∧ 𝐵 ⊆ 𝑌) → (𝐹 ∈ ((𝐽 CnP (𝐾 ↾t 𝐵))‘𝑃) → (𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋)))
10		simpl2 1194	. . . . . . . . . 10 ⊢ (((𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋)) → 𝐹:𝑋⟶𝐵)
11		simprr 773	. . . . . . . . . 10 ⊢ (((𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋)) → 𝑃 ∈ 𝑋)
12	10, 11	ffvelcdmd 7029	. . . . . . . . 9 ⊢ (((𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋)) → (𝐹‘𝑃) ∈ 𝐵)
13	12	biantrud 531	. . . . . . . 8 ⊢ (((𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋)) → ((𝐹‘𝑃) ∈ 𝑥 ↔ ((𝐹‘𝑃) ∈ 𝑥 ∧ (𝐹‘𝑃) ∈ 𝐵)))
14		elin 3906	. . . . . . . 8 ⊢ ((𝐹‘𝑃) ∈ (𝑥 ∩ 𝐵) ↔ ((𝐹‘𝑃) ∈ 𝑥 ∧ (𝐹‘𝑃) ∈ 𝐵))
15	13, 14	bitr4di 289	. . . . . . 7 ⊢ (((𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋)) → ((𝐹‘𝑃) ∈ 𝑥 ↔ (𝐹‘𝑃) ∈ (𝑥 ∩ 𝐵)))
16		imassrn 6028	. . . . . . . . . . . 12 ⊢ (𝐹 “ 𝑦) ⊆ ran 𝐹
17	10	frnd 6668	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋)) → ran 𝐹 ⊆ 𝐵)
18	16, 17	sstrid 3934	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋)) → (𝐹 “ 𝑦) ⊆ 𝐵)
19	18	biantrud 531	. . . . . . . . . 10 ⊢ (((𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋)) → ((𝐹 “ 𝑦) ⊆ 𝑥 ↔ ((𝐹 “ 𝑦) ⊆ 𝑥 ∧ (𝐹 “ 𝑦) ⊆ 𝐵)))
20		ssin 4180	. . . . . . . . . 10 ⊢ (((𝐹 “ 𝑦) ⊆ 𝑥 ∧ (𝐹 “ 𝑦) ⊆ 𝐵) ↔ (𝐹 “ 𝑦) ⊆ (𝑥 ∩ 𝐵))
21	19, 20	bitrdi 287	. . . . . . . . 9 ⊢ (((𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋)) → ((𝐹 “ 𝑦) ⊆ 𝑥 ↔ (𝐹 “ 𝑦) ⊆ (𝑥 ∩ 𝐵)))
22	21	anbi2d 631	. . . . . . . 8 ⊢ (((𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋)) → ((𝑃 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑥) ↔ (𝑃 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ (𝑥 ∩ 𝐵))))
23	22	rexbidv 3162	. . . . . . 7 ⊢ (((𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋)) → (∃𝑦 ∈ 𝐽 (𝑃 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑥) ↔ ∃𝑦 ∈ 𝐽 (𝑃 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ (𝑥 ∩ 𝐵))))
24	15, 23	imbi12d 344	. . . . . 6 ⊢ (((𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋)) → (((𝐹‘𝑃) ∈ 𝑥 → ∃𝑦 ∈ 𝐽 (𝑃 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑥)) ↔ ((𝐹‘𝑃) ∈ (𝑥 ∩ 𝐵) → ∃𝑦 ∈ 𝐽 (𝑃 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ (𝑥 ∩ 𝐵)))))
25	24	ralbidv 3161	. . . . 5 ⊢ (((𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋)) → (∀𝑥 ∈ 𝐾 ((𝐹‘𝑃) ∈ 𝑥 → ∃𝑦 ∈ 𝐽 (𝑃 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑥)) ↔ ∀𝑥 ∈ 𝐾 ((𝐹‘𝑃) ∈ (𝑥 ∩ 𝐵) → ∃𝑦 ∈ 𝐽 (𝑃 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ (𝑥 ∩ 𝐵)))))
26		vex 3434	. . . . . . . 8 ⊢ 𝑥 ∈ V
27	26	inex1 5252	. . . . . . 7 ⊢ (𝑥 ∩ 𝐵) ∈ V
28	27	a1i 11	. . . . . 6 ⊢ ((((𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋)) ∧ 𝑥 ∈ 𝐾) → (𝑥 ∩ 𝐵) ∈ V)
29		simpl1 1193	. . . . . . 7 ⊢ (((𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋)) → 𝐾 ∈ Top)
30		cnprest.2	. . . . . . . . . 10 ⊢ 𝑌 = ∪ 𝐾
31		uniexg 7685	. . . . . . . . . 10 ⊢ (𝐾 ∈ Top → ∪ 𝐾 ∈ V)
32	30, 31	eqeltrid 2841	. . . . . . . . 9 ⊢ (𝐾 ∈ Top → 𝑌 ∈ V)
33	29, 32	syl 17	. . . . . . . 8 ⊢ (((𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋)) → 𝑌 ∈ V)
34		simpl3 1195	. . . . . . . 8 ⊢ (((𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋)) → 𝐵 ⊆ 𝑌)
35	33, 34	ssexd 5259	. . . . . . 7 ⊢ (((𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋)) → 𝐵 ∈ V)
36		elrest 17348	. . . . . . 7 ⊢ ((𝐾 ∈ Top ∧ 𝐵 ∈ V) → (𝑧 ∈ (𝐾 ↾t 𝐵) ↔ ∃𝑥 ∈ 𝐾 𝑧 = (𝑥 ∩ 𝐵)))
37	29, 35, 36	syl2anc 585	. . . . . 6 ⊢ (((𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋)) → (𝑧 ∈ (𝐾 ↾t 𝐵) ↔ ∃𝑥 ∈ 𝐾 𝑧 = (𝑥 ∩ 𝐵)))
38		eleq2 2826	. . . . . . . 8 ⊢ (𝑧 = (𝑥 ∩ 𝐵) → ((𝐹‘𝑃) ∈ 𝑧 ↔ (𝐹‘𝑃) ∈ (𝑥 ∩ 𝐵)))
39		sseq2 3949	. . . . . . . . . 10 ⊢ (𝑧 = (𝑥 ∩ 𝐵) → ((𝐹 “ 𝑦) ⊆ 𝑧 ↔ (𝐹 “ 𝑦) ⊆ (𝑥 ∩ 𝐵)))
40	39	anbi2d 631	. . . . . . . . 9 ⊢ (𝑧 = (𝑥 ∩ 𝐵) → ((𝑃 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑧) ↔ (𝑃 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ (𝑥 ∩ 𝐵))))
41	40	rexbidv 3162	. . . . . . . 8 ⊢ (𝑧 = (𝑥 ∩ 𝐵) → (∃𝑦 ∈ 𝐽 (𝑃 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑧) ↔ ∃𝑦 ∈ 𝐽 (𝑃 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ (𝑥 ∩ 𝐵))))
42	38, 41	imbi12d 344	. . . . . . 7 ⊢ (𝑧 = (𝑥 ∩ 𝐵) → (((𝐹‘𝑃) ∈ 𝑧 → ∃𝑦 ∈ 𝐽 (𝑃 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑧)) ↔ ((𝐹‘𝑃) ∈ (𝑥 ∩ 𝐵) → ∃𝑦 ∈ 𝐽 (𝑃 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ (𝑥 ∩ 𝐵)))))
43	42	adantl 481	. . . . . 6 ⊢ ((((𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋)) ∧ 𝑧 = (𝑥 ∩ 𝐵)) → (((𝐹‘𝑃) ∈ 𝑧 → ∃𝑦 ∈ 𝐽 (𝑃 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑧)) ↔ ((𝐹‘𝑃) ∈ (𝑥 ∩ 𝐵) → ∃𝑦 ∈ 𝐽 (𝑃 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ (𝑥 ∩ 𝐵)))))
44	28, 37, 43	ralxfr2d 5345	. . . . 5 ⊢ (((𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋)) → (∀𝑧 ∈ (𝐾 ↾t 𝐵)((𝐹‘𝑃) ∈ 𝑧 → ∃𝑦 ∈ 𝐽 (𝑃 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑧)) ↔ ∀𝑥 ∈ 𝐾 ((𝐹‘𝑃) ∈ (𝑥 ∩ 𝐵) → ∃𝑦 ∈ 𝐽 (𝑃 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ (𝑥 ∩ 𝐵)))))
45	25, 44	bitr4d 282	. . . 4 ⊢ (((𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋)) → (∀𝑥 ∈ 𝐾 ((𝐹‘𝑃) ∈ 𝑥 → ∃𝑦 ∈ 𝐽 (𝑃 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑥)) ↔ ∀𝑧 ∈ (𝐾 ↾t 𝐵)((𝐹‘𝑃) ∈ 𝑧 → ∃𝑦 ∈ 𝐽 (𝑃 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑧))))
46	10, 34	fssd 6677	. . . . 5 ⊢ (((𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋)) → 𝐹:𝑋⟶𝑌)
47		simprl 771	. . . . . 6 ⊢ (((𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋)) → 𝐽 ∈ Top)
48	2, 30	iscnp2 23182	. . . . . . 7 ⊢ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝑃 ∈ 𝑋) ∧ (𝐹:𝑋⟶𝑌 ∧ ∀𝑥 ∈ 𝐾 ((𝐹‘𝑃) ∈ 𝑥 → ∃𝑦 ∈ 𝐽 (𝑃 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑥)))))
49	48	baib 535	. . . . . 6 ⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝑃 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑥 ∈ 𝐾 ((𝐹‘𝑃) ∈ 𝑥 → ∃𝑦 ∈ 𝐽 (𝑃 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑥)))))
50	47, 29, 11, 49	syl3anc 1374	. . . . 5 ⊢ (((𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋)) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑥 ∈ 𝐾 ((𝐹‘𝑃) ∈ 𝑥 → ∃𝑦 ∈ 𝐽 (𝑃 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑥)))))
51	46, 50	mpbirand 708	. . . 4 ⊢ (((𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋)) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ ∀𝑥 ∈ 𝐾 ((𝐹‘𝑃) ∈ 𝑥 → ∃𝑦 ∈ 𝐽 (𝑃 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑥))))
52	2	toptopon 22860	. . . . . . 7 ⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋))
53	47, 52	sylib 218	. . . . . 6 ⊢ (((𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋)) → 𝐽 ∈ (TopOn‘𝑋))
54	30	toptopon 22860	. . . . . . . 8 ⊢ (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘𝑌))
55	29, 54	sylib 218	. . . . . . 7 ⊢ (((𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋)) → 𝐾 ∈ (TopOn‘𝑌))
56		resttopon 23104	. . . . . . 7 ⊢ ((𝐾 ∈ (TopOn‘𝑌) ∧ 𝐵 ⊆ 𝑌) → (𝐾 ↾t 𝐵) ∈ (TopOn‘𝐵))
57	55, 34, 56	syl2anc 585	. . . . . 6 ⊢ (((𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋)) → (𝐾 ↾t 𝐵) ∈ (TopOn‘𝐵))
58		iscnp 23180	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝐾 ↾t 𝐵) ∈ (TopOn‘𝐵) ∧ 𝑃 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP (𝐾 ↾t 𝐵))‘𝑃) ↔ (𝐹:𝑋⟶𝐵 ∧ ∀𝑧 ∈ (𝐾 ↾t 𝐵)((𝐹‘𝑃) ∈ 𝑧 → ∃𝑦 ∈ 𝐽 (𝑃 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑧)))))
59	53, 57, 11, 58	syl3anc 1374	. . . . 5 ⊢ (((𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋)) → (𝐹 ∈ ((𝐽 CnP (𝐾 ↾t 𝐵))‘𝑃) ↔ (𝐹:𝑋⟶𝐵 ∧ ∀𝑧 ∈ (𝐾 ↾t 𝐵)((𝐹‘𝑃) ∈ 𝑧 → ∃𝑦 ∈ 𝐽 (𝑃 ∈ 𝑦 ∧ (𝐹 “ 𝑦) ⊆ 𝑧)))))
60	10, 59	mpbirand 708	. . . 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 1087   = wceq 1542   ∈ wcel 2114  ∀wral 3052  ∃wrex 3062  Vcvv 3430   ∩ cin 3889   ⊆ wss 3890  ∪ cuni 4851  ran crn 5623   “ cima 5625  ⟶wf 6486  ‘cfv 6490  (class class class)co 7358   ↾_t crest 17341  Topctop 22836  TopOnctopon 22853   CnP ccnp 23168

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5212  ax-sep 5231  ax-nul 5241  ax-pow 5300  ax-pr 5368  ax-un 7680

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-int 4891  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5517  df-eprel 5522  df-po 5530  df-so 5531  df-fr 5575  df-we 5577  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-ord 6318  df-on 6319  df-lim 6320  df-suc 6321  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-f1 6495  df-fo 6496  df-f1o 6497  df-fv 6498  df-ov 7361  df-oprab 7362  df-mpo 7363  df-om 7809  df-1st 7933  df-2nd 7934  df-map 8766  df-en 8885  df-fin 8888  df-fi 9315  df-rest 17343  df-topgen 17364  df-top 22837  df-topon 22854  df-bases 22889  df-cnp 23171

This theorem is referenced by:  limccnp  25836  limccnp2  25837  dirkercncflem4  46538  dirkercncf  46539  fouriercnp  46658