cnrest2 - Metamath Proof Explorer

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

Theorem cnrest2 23228

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 23182	. . . 4 ⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐽 ∈ Top)
2	1	a1i 11	. . 3 ⊢ ((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌) → (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐽 ∈ Top))
3		eqid 2734	. . . . . . . 8 ⊢ ∪ 𝐽 = ∪ 𝐽
4		eqid 2734	. . . . . . . 8 ⊢ ∪ 𝐾 = ∪ 𝐾
5	3, 4	cnf 23188	. . . . . . 7 ⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐹:∪ 𝐽⟶∪ 𝐾)
6	5	ffnd 6661	. . . . . 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 6494	. . . 4 ⊢ (𝐹:∪ 𝐽⟶𝐵 ↔ (𝐹 Fn ∪ 𝐽 ∧ ran 𝐹 ⊆ 𝐵))
11	9, 10	imbitrrdi 252	. . 3 ⊢ ((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌) → (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐹:∪ 𝐽⟶𝐵))
12	2, 11	jcad 512	. 2 ⊢ ((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌) → (𝐹 ∈ (𝐽 Cn 𝐾) → (𝐽 ∈ Top ∧ 𝐹:∪ 𝐽⟶𝐵)))
13		cntop1 23182	. . . . 5 ⊢ (𝐹 ∈ (𝐽 Cn (𝐾 ↾_t 𝐵)) → 𝐽 ∈ Top)
14	13	adantl 481	. . . 4 ⊢ (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ 𝐹 ∈ (𝐽 Cn (𝐾 ↾_t 𝐵))) → 𝐽 ∈ Top)
15		toptopon2 22860	. . . . . 6 ⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘∪ 𝐽))
16	14, 15	sylib 218	. . . . 5 ⊢ (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ 𝐹 ∈ (𝐽 Cn (𝐾 ↾_t 𝐵))) → 𝐽 ∈ (TopOn‘∪ 𝐽))
17		resttopon 23103	. . . . . . 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 23191	. . . . 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 3442	. . . . . . . . 9 ⊢ 𝑥 ∈ V
26	25	inex1 5260	. . . . . . . 8 ⊢ (𝑥 ∩ 𝐵) ∈ V
27	26	a1i 11	. . . . . . 7 ⊢ ((((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹:∪ 𝐽⟶𝐵)) ∧ 𝑥 ∈ 𝐾) → (𝑥 ∩ 𝐵) ∈ V)
28		simpl1 1192	. . . . . . . 8 ⊢ (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹:∪ 𝐽⟶𝐵)) → 𝐾 ∈ (TopOn‘𝑌))
29		toponmax 22868	. . . . . . . . . 10 ⊢ (𝐾 ∈ (TopOn‘𝑌) → 𝑌 ∈ 𝐾)
30	28, 29	syl 17	. . . . . . . . 9 ⊢ (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹:∪ 𝐽⟶𝐵)) → 𝑌 ∈ 𝐾)
31		simpl3 1194	. . . . . . . . 9 ⊢ (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹:∪ 𝐽⟶𝐵)) → 𝐵 ⊆ 𝑌)
32	30, 31	ssexd 5267	. . . . . . . 8 ⊢ (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹:∪ 𝐽⟶𝐵)) → 𝐵 ∈ V)
33		elrest 17345	. . . . . . . 8 ⊢ ((𝐾 ∈ (TopOn‘𝑌) ∧ 𝐵 ∈ V) → (𝑦 ∈ (𝐾 ↾_t 𝐵) ↔ ∃𝑥 ∈ 𝐾 𝑦 = (𝑥 ∩ 𝐵)))
34	28, 32, 33	syl2anc 584	. . . . . . 7 ⊢ (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹:∪ 𝐽⟶𝐵)) → (𝑦 ∈ (𝐾 ↾_t 𝐵) ↔ ∃𝑥 ∈ 𝐾 𝑦 = (𝑥 ∩ 𝐵)))
35		imaeq2 6013	. . . . . . . . 9 ⊢ (𝑦 = (𝑥 ∩ 𝐵) → (^◡𝐹 “ 𝑦) = (^◡𝐹 “ (𝑥 ∩ 𝐵)))
36	35	eleq1d 2819	. . . . . . . 8 ⊢ (𝑦 = (𝑥 ∩ 𝐵) → ((^◡𝐹 “ 𝑦) ∈ 𝐽 ↔ (^◡𝐹 “ (𝑥 ∩ 𝐵)) ∈ 𝐽))
37	36	adantl 481	. . . . . . 7 ⊢ ((((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹:∪ 𝐽⟶𝐵)) ∧ 𝑦 = (𝑥 ∩ 𝐵)) → ((^◡𝐹 “ 𝑦) ∈ 𝐽 ↔ (^◡𝐹 “ (𝑥 ∩ 𝐵)) ∈ 𝐽))
38	27, 34, 37	ralxfr2d 5353	. . . . . 6 ⊢ (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹:∪ 𝐽⟶𝐵)) → (∀𝑦 ∈ (𝐾 ↾_t 𝐵)(^◡𝐹 “ 𝑦) ∈ 𝐽 ↔ ∀𝑥 ∈ 𝐾 (^◡𝐹 “ (𝑥 ∩ 𝐵)) ∈ 𝐽))
39		simplrr 777	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹:∪ 𝐽⟶𝐵)) ∧ 𝑥 ∈ 𝐾) → 𝐹:∪ 𝐽⟶𝐵)
40		ffun 6663	. . . . . . . . . 10 ⊢ (𝐹:∪ 𝐽⟶𝐵 → Fun 𝐹)
41		inpreima 7007	. . . . . . . . . 10 ⊢ (Fun 𝐹 → (^◡𝐹 “ (𝑥 ∩ 𝐵)) = ((^◡𝐹 “ 𝑥) ∩ (^◡𝐹 “ 𝐵)))
42	39, 40, 41	3syl 18	. . . . . . . . 9 ⊢ ((((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹:∪ 𝐽⟶𝐵)) ∧ 𝑥 ∈ 𝐾) → (^◡𝐹 “ (𝑥 ∩ 𝐵)) = ((^◡𝐹 “ 𝑥) ∩ (^◡𝐹 “ 𝐵)))
43		cnvimass 6039	. . . . . . . . . . . 12 ⊢ (^◡𝐹 “ 𝑥) ⊆ dom 𝐹
44		cnvimarndm 6040	. . . . . . . . . . . 12 ⊢ (^◡𝐹 “ ran 𝐹) = dom 𝐹
45	43, 44	sseqtrri 3981	. . . . . . . . . . 11 ⊢ (^◡𝐹 “ 𝑥) ⊆ (^◡𝐹 “ ran 𝐹)
46		simpll2 1214	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹:∪ 𝐽⟶𝐵)) ∧ 𝑥 ∈ 𝐾) → ran 𝐹 ⊆ 𝐵)
47		imass2 6059	. . . . . . . . . . . 12 ⊢ (ran 𝐹 ⊆ 𝐵 → (^◡𝐹 “ ran 𝐹) ⊆ (^◡𝐹 “ 𝐵))
48	46, 47	syl 17	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹:∪ 𝐽⟶𝐵)) ∧ 𝑥 ∈ 𝐾) → (^◡𝐹 “ ran 𝐹) ⊆ (^◡𝐹 “ 𝐵))
49	45, 48	sstrid 3943	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹:∪ 𝐽⟶𝐵)) ∧ 𝑥 ∈ 𝐾) → (^◡𝐹 “ 𝑥) ⊆ (^◡𝐹 “ 𝐵))
50		dfss2 3917	. . . . . . . . . 10 ⊢ ((^◡𝐹 “ 𝑥) ⊆ (^◡𝐹 “ 𝐵) ↔ ((^◡𝐹 “ 𝑥) ∩ (^◡𝐹 “ 𝐵)) = (^◡𝐹 “ 𝑥))
51	49, 50	sylib 218	. . . . . . . . 9 ⊢ ((((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹:∪ 𝐽⟶𝐵)) ∧ 𝑥 ∈ 𝐾) → ((^◡𝐹 “ 𝑥) ∩ (^◡𝐹 “ 𝐵)) = (^◡𝐹 “ 𝑥))
52	42, 51	eqtrd 2769	. . . . . . . 8 ⊢ ((((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹:∪ 𝐽⟶𝐵)) ∧ 𝑥 ∈ 𝐾) → (^◡𝐹 “ (𝑥 ∩ 𝐵)) = (^◡𝐹 “ 𝑥))
53	52	eleq1d 2819	. . . . . . 7 ⊢ ((((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹:∪ 𝐽⟶𝐵)) ∧ 𝑥 ∈ 𝐾) → ((^◡𝐹 “ (𝑥 ∩ 𝐵)) ∈ 𝐽 ↔ (^◡𝐹 “ 𝑥) ∈ 𝐽))
54	53	ralbidva 3155	. . . . . 6 ⊢ (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹:∪ 𝐽⟶𝐵)) → (∀𝑥 ∈ 𝐾 (^◡𝐹 “ (𝑥 ∩ 𝐵)) ∈ 𝐽 ↔ ∀𝑥 ∈ 𝐾 (^◡𝐹 “ 𝑥) ∈ 𝐽))
55		simprr 772	. . . . . . . 8 ⊢ (((𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝑌) ∧ (𝐽 ∈ Top ∧ 𝐹:∪ 𝐽⟶𝐵)) → 𝐹:∪ 𝐽⟶𝐵)
56	55, 31	fssd 6677	. . . . . . 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 23177	. . . . 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 23177	. . . . 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 𝐵))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1541 ∈ wcel 2113 ∀wral 3049 ∃wrex 3058 Vcvv 3438 ∩ cin 3898 ⊆ wss 3899 ∪ cuni 4861 ^◡ccnv 5621 dom cdm 5622 ran crn 5623 “ cima 5625 Fun wfun 6484 Fn wfn 6485 ⟶wf 6486 ‘cfv 6490 (class class class)co 7356 ↾_t crest 17338 Topctop 22835 TopOnctopon 22852 Cn ccn 23166

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 2182 ax-ext 2706 ax-rep 5222 ax-sep 5239 ax-nul 5249 ax-pow 5308 ax-pr 5375 ax-un 7678

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 2537 df-eu 2567 df-clab 2713 df-cleq 2726 df-clel 2809 df-nfc 2883 df-ne 2931 df-ral 3050 df-rex 3059 df-reu 3349 df-rab 3398 df-v 3440 df-sbc 3739 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4284 df-if 4478 df-pw 4554 df-sn 4579 df-pr 4581 df-op 4585 df-uni 4862 df-int 4901 df-iun 4946 df-br 5097 df-opab 5159 df-mpt 5178 df-tr 5204 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 7359 df-oprab 7360 df-mpo 7361 df-om 7807 df-1st 7931 df-2nd 7932 df-map 8763 df-en 8882 df-fin 8885 df-fi 9312 df-rest 17340 df-topgen 17361 df-top 22836 df-topon 22853 df-bases 22888 df-cn 23169

This theorem is referenced by: cnrest2r 23229 rncmp 23338 connima 23367 conncn 23368 kgencn2 23499 kgencn3 23500 qtoprest 23659 hmeores 23713 efmndtmd 24043 submtmd 24046 subgtgp 24047 symgtgp 24048 metdcn2 24782 metdscn2 24800 cnmptre 24875 iimulcn 24888 iimulcnOLD 24889 icchmeo 24892 icchmeoOLD 24893 evth 24912 evth2 24913 lebnumlem2 24915 reparphti 24950 reparphtiOLD 24951 efrlim 26933 efrlimOLD 26934 rmulccn 34034 raddcn 34035 xrge0mulc1cn 34047 cvxpconn 35385 cvxsconn 35386 cvmliftmolem1 35424 cvmliftlem8 35435 cvmlift2lem9 35454 cvmlift3lem6 35467 ivthALT 36478 knoppcnlem10 36645 broucube 37794 areacirclem2 37849 cnres2 37903 cnresima 37904 refsumcn 45217 icccncfext 46073

W3C validator