Theorem cnrest2 23232

Description: Equivalence of continuity in the parent topology and continuity in a subspace. (Contributed by Jeff Hankins, 10-Jul-2009.) (Proof shortened by Mario Carneiro, 21-Aug-2015.)

Assertion

Ref	Expression
cnrest2	⊢ ((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ 𝐹 ∈ (𝐽 Cn (𝐾 ↾t 𝐵))))

Proof of Theorem cnrest2

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

Step	Hyp	Ref	Expression
1		cntop1 23186	. . . 4 ⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐽 ∈ Top)
2	1	a1i 11	. . 3 ⊢ ((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌) → (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐽 ∈ Top))
3		eqid 2736	. . . . . . . 8 ⊢ ∪ 𝐽 = ∪ 𝐽
4		eqid 2736	. . . . . . . 8 ⊢ ∪ 𝐾 = ∪ 𝐾
5	3, 4	cnf 23192	. . . . . . 7 ⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐹:∪ 𝐽⟶∪ 𝐾)
6	5	ffnd 6663	. . . . . 6 ⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐹 Fn ∪ 𝐽)
7	6	a1i 11	. . . . 5 ⊢ ((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌) → (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐹 Fn ∪ 𝐽))
8		simp2 1137	. . . . 5 ⊢ ((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌) → ran 𝐹 ⊆ 𝐵)
9	7, 8	jctird 526	. . . 4 ⊢ ((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌) → (𝐹 ∈ (𝐽 Cn 𝐾) → (𝐹 Fn ∪ 𝐽 ∧ ran 𝐹 ⊆ 𝐵)))
10		df-f 6496	. . . 4 ⊢ (𝐹:∪ 𝐽⟶𝐵 ↔ (𝐹 Fn ∪ 𝐽 ∧ ran 𝐹 ⊆ 𝐵))
11	9, 10	imbitrrdi 252	. . 3 ⊢ ((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌) → (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐹:∪ 𝐽⟶𝐵))
12	2, 11	jcad 512	. 2 ⊢ ((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌) → (𝐹 ∈ (𝐽 Cn 𝐾) → (𝐽 ∈ Top ∧ 𝐹:∪ 𝐽⟶𝐵)))
13		cntop1 23186	. . . . 5 ⊢ (𝐹 ∈ (𝐽 Cn (𝐾 ↾t 𝐵)) → 𝐽 ∈ Top)
14	13	adantl 481	. . . 4 ⊢ (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ 𝐹 ∈ (𝐽 Cn (𝐾 ↾t 𝐵))) → 𝐽 ∈ Top)
15		toptopon2 22864	. . . . . 6 ⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘∪ 𝐽))
16	14, 15	sylib 218	. . . . 5 ⊢ (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ 𝐹 ∈ (𝐽 Cn (𝐾 ↾t 𝐵))) → 𝐽 ∈ (TopOn‘∪ 𝐽))
17		resttopon 23107	. . . . . . 7 ⊢ ((𝐾 ∈ (TopOn‘𝑌) ∧ 𝐵 ⊆ 𝑌) → (𝐾 ↾t 𝐵) ∈ (TopOn‘𝐵))
18	17	3adant2 1131	. . . . . 6 ⊢ ((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌) → (𝐾 ↾t 𝐵) ∈ (TopOn‘𝐵))
19	18	adantr 480	. . . . 5 ⊢ (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ 𝐹 ∈ (𝐽 Cn (𝐾 ↾t 𝐵))) → (𝐾 ↾t 𝐵) ∈ (TopOn‘𝐵))
20		simpr 484	. . . . 5 ⊢ (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ 𝐹 ∈ (𝐽 Cn (𝐾 ↾t 𝐵))) → 𝐹 ∈ (𝐽 Cn (𝐾 ↾t 𝐵)))
21		cnf2 23195	. . . . 5 ⊢ ((𝐽 ∈ (TopOn‘∪ 𝐽) ∧ (𝐾 ↾t 𝐵) ∈ (TopOn‘𝐵) ∧ 𝐹 ∈ (𝐽 Cn (𝐾 ↾t 𝐵))) → 𝐹:∪ 𝐽⟶𝐵)
22	16, 19, 20, 21	syl3anc 1373	. . . 4 ⊢ (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ 𝐹 ∈ (𝐽 Cn (𝐾 ↾t 𝐵))) → 𝐹:∪ 𝐽⟶𝐵)
23	14, 22	jca 511	. . 3 ⊢ (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ 𝐹 ∈ (𝐽 Cn (𝐾 ↾t 𝐵))) → (𝐽 ∈ Top ∧ 𝐹:∪ 𝐽⟶𝐵))
24	23	ex 412	. 2 ⊢ ((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌) → (𝐹 ∈ (𝐽 Cn (𝐾 ↾t 𝐵)) → (𝐽 ∈ Top ∧ 𝐹:∪ 𝐽⟶𝐵)))
25		vex 3444	. . . . . . . . 9 ⊢ 𝑥 ∈ V
26	25	inex1 5262	. . . . . . . 8 ⊢ (𝑥 ∩ 𝐵) ∈ V
27	26	a1i 11	. . . . . . 7 ⊢ ((((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹:∪ 𝐽⟶𝐵)) ∧ 𝑥 ∈ 𝐾) → (𝑥 ∩ 𝐵) ∈ V)
28		simpl1 1192	. . . . . . . 8 ⊢ (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹:∪ 𝐽⟶𝐵)) → 𝐾 ∈ (TopOn‘𝑌))
29		toponmax 22872	. . . . . . . . . 10 ⊢ (𝐾 ∈ (TopOn‘𝑌) → 𝑌 ∈ 𝐾)
30	28, 29	syl 17	. . . . . . . . 9 ⊢ (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹:∪ 𝐽⟶𝐵)) → 𝑌 ∈ 𝐾)
31		simpl3 1194	. . . . . . . . 9 ⊢ (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹:∪ 𝐽⟶𝐵)) → 𝐵 ⊆ 𝑌)
32	30, 31	ssexd 5269	. . . . . . . 8 ⊢ (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹:∪ 𝐽⟶𝐵)) → 𝐵 ∈ V)
33		elrest 17349	. . . . . . . 8 ⊢ ((𝐾 ∈ (TopOn‘𝑌) ∧ 𝐵 ∈ V) → (𝑦 ∈ (𝐾 ↾t 𝐵) ↔ ∃𝑥 ∈ 𝐾 𝑦 = (𝑥 ∩ 𝐵)))
34	28, 32, 33	syl2anc 584	. . . . . . 7 ⊢ (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹:∪ 𝐽⟶𝐵)) → (𝑦 ∈ (𝐾 ↾t 𝐵) ↔ ∃𝑥 ∈ 𝐾 𝑦 = (𝑥 ∩ 𝐵)))
35		imaeq2 6015	. . . . . . . . 9 ⊢ (𝑦 = (𝑥 ∩ 𝐵) → (◡𝐹 “ 𝑦) = (◡𝐹 “ (𝑥 ∩ 𝐵)))
36	35	eleq1d 2821	. . . . . . . 8 ⊢ (𝑦 = (𝑥 ∩ 𝐵) → ((◡𝐹 “ 𝑦) ∈ 𝐽 ↔ (◡𝐹 “ (𝑥 ∩ 𝐵)) ∈ 𝐽))
37	36	adantl 481	. . . . . . 7 ⊢ ((((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹:∪ 𝐽⟶𝐵)) ∧ 𝑦 = (𝑥 ∩ 𝐵)) → ((◡𝐹 “ 𝑦) ∈ 𝐽 ↔ (◡𝐹 “ (𝑥 ∩ 𝐵)) ∈ 𝐽))
38	27, 34, 37	ralxfr2d 5355	. . . . . 6 ⊢ (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹:∪ 𝐽⟶𝐵)) → (∀𝑦 ∈ (𝐾 ↾t 𝐵)(◡𝐹 “ 𝑦) ∈ 𝐽 ↔ ∀𝑥 ∈ 𝐾 (◡𝐹 “ (𝑥 ∩ 𝐵)) ∈ 𝐽))
39		simplrr 777	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹:∪ 𝐽⟶𝐵)) ∧ 𝑥 ∈ 𝐾) → 𝐹:∪ 𝐽⟶𝐵)
40		ffun 6665	. . . . . . . . . 10 ⊢ (𝐹:∪ 𝐽⟶𝐵 → Fun 𝐹)
41		inpreima 7009	. . . . . . . . . 10 ⊢ (Fun 𝐹 → (◡𝐹 “ (𝑥 ∩ 𝐵)) = ((◡𝐹 “ 𝑥) ∩ (◡𝐹 “ 𝐵)))
42	39, 40, 41	3syl 18	. . . . . . . . 9 ⊢ ((((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹:∪ 𝐽⟶𝐵)) ∧ 𝑥 ∈ 𝐾) → (◡𝐹 “ (𝑥 ∩ 𝐵)) = ((◡𝐹 “ 𝑥) ∩ (◡𝐹 “ 𝐵)))
43		cnvimass 6041	. . . . . . . . . . . 12 ⊢ (◡𝐹 “ 𝑥) ⊆ dom 𝐹
44		cnvimarndm 6042	. . . . . . . . . . . 12 ⊢ (◡𝐹 “ ran 𝐹) = dom 𝐹
45	43, 44	sseqtrri 3983	. . . . . . . . . . 11 ⊢ (◡𝐹 “ 𝑥) ⊆ (◡𝐹 “ ran 𝐹)
46		simpll2 1214	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹:∪ 𝐽⟶𝐵)) ∧ 𝑥 ∈ 𝐾) → ran 𝐹 ⊆ 𝐵)
47		imass2 6061	. . . . . . . . . . . 12 ⊢ (ran 𝐹 ⊆ 𝐵 → (◡𝐹 “ ran 𝐹) ⊆ (◡𝐹 “ 𝐵))
48	46, 47	syl 17	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹:∪ 𝐽⟶𝐵)) ∧ 𝑥 ∈ 𝐾) → (◡𝐹 “ ran 𝐹) ⊆ (◡𝐹 “ 𝐵))
49	45, 48	sstrid 3945	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹:∪ 𝐽⟶𝐵)) ∧ 𝑥 ∈ 𝐾) → (◡𝐹 “ 𝑥) ⊆ (◡𝐹 “ 𝐵))
50		dfss2 3919	. . . . . . . . . 10 ⊢ ((◡𝐹 “ 𝑥) ⊆ (◡𝐹 “ 𝐵) ↔ ((◡𝐹 “ 𝑥) ∩ (◡𝐹 “ 𝐵)) = (◡𝐹 “ 𝑥))
51	49, 50	sylib 218	. . . . . . . . 9 ⊢ ((((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹:∪ 𝐽⟶𝐵)) ∧ 𝑥 ∈ 𝐾) → ((◡𝐹 “ 𝑥) ∩ (◡𝐹 “ 𝐵)) = (◡𝐹 “ 𝑥))
52	42, 51	eqtrd 2771	. . . . . . . 8 ⊢ ((((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹:∪ 𝐽⟶𝐵)) ∧ 𝑥 ∈ 𝐾) → (◡𝐹 “ (𝑥 ∩ 𝐵)) = (◡𝐹 “ 𝑥))
53	52	eleq1d 2821	. . . . . . 7 ⊢ ((((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹:∪ 𝐽⟶𝐵)) ∧ 𝑥 ∈ 𝐾) → ((◡𝐹 “ (𝑥 ∩ 𝐵)) ∈ 𝐽 ↔ (◡𝐹 “ 𝑥) ∈ 𝐽))
54	53	ralbidva 3157	. . . . . 6 ⊢ (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹:∪ 𝐽⟶𝐵)) → (∀𝑥 ∈ 𝐾 (◡𝐹 “ (𝑥 ∩ 𝐵)) ∈ 𝐽 ↔ ∀𝑥 ∈ 𝐾 (◡𝐹 “ 𝑥) ∈ 𝐽))
55		simprr 772	. . . . . . . 8 ⊢ (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹:∪ 𝐽⟶𝐵)) → 𝐹:∪ 𝐽⟶𝐵)
56	55, 31	fssd 6679	. . . . . . 7 ⊢ (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹:∪ 𝐽⟶𝐵)) → 𝐹:∪ 𝐽⟶𝑌)
57	56	biantrurd 532	. . . . . 6 ⊢ (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹:∪ 𝐽⟶𝐵)) → (∀𝑥 ∈ 𝐾 (◡𝐹 “ 𝑥) ∈ 𝐽 ↔ (𝐹:∪ 𝐽⟶𝑌 ∧ ∀𝑥 ∈ 𝐾 (◡𝐹 “ 𝑥) ∈ 𝐽)))
58	38, 54, 57	3bitrrd 306	. . . . 5 ⊢ (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹:∪ 𝐽⟶𝐵)) → ((𝐹:∪ 𝐽⟶𝑌 ∧ ∀𝑥 ∈ 𝐾 (◡𝐹 “ 𝑥) ∈ 𝐽) ↔ ∀𝑦 ∈ (𝐾 ↾t 𝐵)(◡𝐹 “ 𝑦) ∈ 𝐽))
59	55	biantrurd 532	. . . . 5 ⊢ (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹:∪ 𝐽⟶𝐵)) → (∀𝑦 ∈ (𝐾 ↾t 𝐵)(◡𝐹 “ 𝑦) ∈ 𝐽 ↔ (𝐹:∪ 𝐽⟶𝐵 ∧ ∀𝑦 ∈ (𝐾 ↾t 𝐵)(◡𝐹 “ 𝑦) ∈ 𝐽)))
60	58, 59	bitrd 279	. . . 4 ⊢ (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹:∪ 𝐽⟶𝐵)) → ((𝐹:∪ 𝐽⟶𝑌 ∧ ∀𝑥 ∈ 𝐾 (◡𝐹 “ 𝑥) ∈ 𝐽) ↔ (𝐹:∪ 𝐽⟶𝐵 ∧ ∀𝑦 ∈ (𝐾 ↾t 𝐵)(◡𝐹 “ 𝑦) ∈ 𝐽)))
61		simprl 770	. . . . . 6 ⊢ (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹:∪ 𝐽⟶𝐵)) → 𝐽 ∈ Top)
62	61, 15	sylib 218	. . . . 5 ⊢ (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹:∪ 𝐽⟶𝐵)) → 𝐽 ∈ (TopOn‘∪ 𝐽))
63		iscn 23181	. . . . 5 ⊢ ((𝐽 ∈ (TopOn‘∪ 𝐽) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:∪ 𝐽⟶𝑌 ∧ ∀𝑥 ∈ 𝐾 (◡𝐹 “ 𝑥) ∈ 𝐽)))
64	62, 28, 63	syl2anc 584	. . . 4 ⊢ (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹:∪ 𝐽⟶𝐵)) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:∪ 𝐽⟶𝑌 ∧ ∀𝑥 ∈ 𝐾 (◡𝐹 “ 𝑥) ∈ 𝐽)))
65	18	adantr 480	. . . . 5 ⊢ (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹:∪ 𝐽⟶𝐵)) → (𝐾 ↾t 𝐵) ∈ (TopOn‘𝐵))
66		iscn 23181	. . . . 5 ⊢ ((𝐽 ∈ (TopOn‘∪ 𝐽) ∧ (𝐾 ↾t 𝐵) ∈ (TopOn‘𝐵)) → (𝐹 ∈ (𝐽 Cn (𝐾 ↾t 𝐵)) ↔ (𝐹:∪ 𝐽⟶𝐵 ∧ ∀𝑦 ∈ (𝐾 ↾t 𝐵)(◡𝐹 “ 𝑦) ∈ 𝐽)))
67	62, 65, 66	syl2anc 584	. . . 4 ⊢ (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹:∪ 𝐽⟶𝐵)) → (𝐹 ∈ (𝐽 Cn (𝐾 ↾t 𝐵)) ↔ (𝐹:∪ 𝐽⟶𝐵 ∧ ∀𝑦 ∈ (𝐾 ↾t 𝐵)(◡𝐹 “ 𝑦) ∈ 𝐽)))
68	60, 64, 67	3bitr4d 311	. . 3 ⊢ (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹:∪ 𝐽⟶𝐵)) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ 𝐹 ∈ (𝐽 Cn (𝐾 ↾t 𝐵))))
69	68	ex 412	. 2 ⊢ ((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌) → ((𝐽 ∈ Top ∧ 𝐹:∪ 𝐽⟶𝐵) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ 𝐹 ∈ (𝐽 Cn (𝐾 ↾t 𝐵)))))
70	12, 24, 69	pm5.21ndd 379	1 ⊢ ((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ 𝐹 ∈ (𝐽 Cn (𝐾 ↾t 𝐵))))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1541   ∈ wcel 2113  ∀wral 3051  ∃wrex 3060  Vcvv 3440   ∩ cin 3900   ⊆ wss 3901  ∪ cuni 4863  ^◡ccnv 5623  dom cdm 5624  ran crn 5625   “ cima 5627  Fun wfun 6486   Fn wfn 6487  ⟶wf 6488  ‘cfv 6492  (class class class)co 7358   ↾_t crest 17342  Topctop 22839  TopOnctopon 22856   Cn ccn 23170

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-rep 5224  ax-sep 5241  ax-nul 5251  ax-pow 5310  ax-pr 5377  ax-un 7680

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-reu 3351  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-pss 3921  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-int 4903  df-iun 4948  df-br 5099  df-opab 5161  df-mpt 5180  df-tr 5206  df-id 5519  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-ov 7361  df-oprab 7362  df-mpo 7363  df-om 7809  df-1st 7933  df-2nd 7934  df-map 8767  df-en 8886  df-fin 8889  df-fi 9316  df-rest 17344  df-topgen 17365  df-top 22840  df-topon 22857  df-bases 22892  df-cn 23173

This theorem is referenced by:  cnrest2r  23233  rncmp  23342  connima  23371  conncn  23372  kgencn2  23503  kgencn3  23504  qtoprest  23663  hmeores  23717  efmndtmd  24047  submtmd  24050  subgtgp  24051  symgtgp  24052  metdcn2  24786  metdscn2  24804  cnmptre  24879  iimulcn  24892  iimulcnOLD  24893  icchmeo  24896  icchmeoOLD  24897  evth  24916  evth2  24917  lebnumlem2  24919  reparphti  24954  reparphtiOLD  24955  efrlim  26937  efrlimOLD  26938  rmulccn  34087  raddcn  34088  xrge0mulc1cn  34100  cvxpconn  35438  cvxsconn  35439  cvmliftmolem1  35477  cvmliftlem8  35488  cvmlift2lem9  35507  cvmlift3lem6  35520  ivthALT  36531  knoppcnlem10  36704  broucube  37857  areacirclem2  37912  cnres2  37966  cnresima  37967  refsumcn  45296  icccncfext  46152