cnrest2

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)

		Ref	Expression
	Assertion	cnrest2	$⊢ (K \in TopOn (Y) \land ran F \subseteq B \land B \subseteq Y) \to (F \in (J Cn K) \leftrightarrow F \in (J Cn (K ↾_{𝑡} B)))$

Proof

Step	Hyp	Ref	Expression
1		cntop1	$⊢ F \in (J Cn K) \to J \in Top$
2	1	a1i	$⊢ (K \in TopOn (Y) \land ran F \subseteq B \land B \subseteq Y) \to (F \in (J Cn K) \to J \in Top)$
3		eqid	$⊢ ⋃ J = ⋃ J$
4		eqid	$⊢ ⋃ K = ⋃ K$
5	3 4	cnf	$⊢ F \in (J Cn K) \to F : ⋃ J ⟶ ⋃ K$
6	5	ffnd	$⊢ F \in (J Cn K) \to F Fn ⋃ J$
7	6	a1i	$⊢ (K \in TopOn (Y) \land ran F \subseteq B \land B \subseteq Y) \to (F \in (J Cn K) \to F Fn ⋃ J)$
8		simp2	$⊢ (K \in TopOn (Y) \land ran F \subseteq B \land B \subseteq Y) \to ran F \subseteq B$
9	7 8	jctird	$⊢ (K \in TopOn (Y) \land ran F \subseteq B \land B \subseteq Y) \to (F \in (J Cn K) \to (F Fn ⋃ J \land ran F \subseteq B))$
10		df-f	$⊢ F : ⋃ J ⟶ B \leftrightarrow (F Fn ⋃ J \land ran F \subseteq B)$
11	9 10	syl6ibr	$⊢ (K \in TopOn (Y) \land ran F \subseteq B \land B \subseteq Y) \to (F \in (J Cn K) \to F : ⋃ J ⟶ B)$
12	2 11	jcad	$⊢ (K \in TopOn (Y) \land ran F \subseteq B \land B \subseteq Y) \to (F \in (J Cn K) \to (J \in Top \land F : ⋃ J ⟶ B))$
13		cntop1	$⊢ F \in (J Cn (K ↾_{𝑡} B)) \to J \in Top$
14	13	adantl	$⊢ ((K \in TopOn (Y) \land ran F \subseteq B \land B \subseteq Y) \land F \in (J Cn (K ↾_{𝑡} B))) \to J \in Top$
15		toptopon2	$⊢ J \in Top \leftrightarrow J \in TopOn (⋃ J)$
16	14 15	sylib	$⊢ ((K \in TopOn (Y) \land ran F \subseteq B \land B \subseteq Y) \land F \in (J Cn (K ↾_{𝑡} B))) \to J \in TopOn (⋃ J)$
17		resttopon	$⊢ (K \in TopOn (Y) \land B \subseteq Y) \to K ↾_{𝑡} B \in TopOn (B)$
18	17	3adant2	$⊢ (K \in TopOn (Y) \land ran F \subseteq B \land B \subseteq Y) \to K ↾_{𝑡} B \in TopOn (B)$
19	18	adantr	$⊢ ((K \in TopOn (Y) \land ran F \subseteq B \land B \subseteq Y) \land F \in (J Cn (K ↾_{𝑡} B))) \to K ↾_{𝑡} B \in TopOn (B)$
20		simpr	$⊢ ((K \in TopOn (Y) \land ran F \subseteq B \land B \subseteq Y) \land F \in (J Cn (K ↾_{𝑡} B))) \to F \in (J Cn (K ↾_{𝑡} B))$
21		cnf2	$⊢ (J \in TopOn (⋃ J) \land K ↾_{𝑡} B \in TopOn (B) \land F \in (J Cn (K ↾_{𝑡} B))) \to F : ⋃ J ⟶ B$
22	16 19 20 21	syl3anc	$⊢ ((K \in TopOn (Y) \land ran F \subseteq B \land B \subseteq Y) \land F \in (J Cn (K ↾_{𝑡} B))) \to F : ⋃ J ⟶ B$
23	14 22	jca	$⊢ ((K \in TopOn (Y) \land ran F \subseteq B \land B \subseteq Y) \land F \in (J Cn (K ↾_{𝑡} B))) \to (J \in Top \land F : ⋃ J ⟶ B)$
24	23	ex	$⊢ (K \in TopOn (Y) \land ran F \subseteq B \land B \subseteq Y) \to (F \in (J Cn (K ↾_{𝑡} B)) \to (J \in Top \land F : ⋃ J ⟶ B))$
25		vex	$⊢ x \in V$
26	25	inex1	$⊢ x \cap B \in V$
27	26	a1i	$⊢ (((K \in TopOn (Y) \land ran F \subseteq B \land B \subseteq Y) \land (J \in Top \land F : ⋃ J ⟶ B)) \land x \in K) \to x \cap B \in V$
28		simpl1	$⊢ ((K \in TopOn (Y) \land ran F \subseteq B \land B \subseteq Y) \land (J \in Top \land F : ⋃ J ⟶ B)) \to K \in TopOn (Y)$
29		toponmax	$⊢ K \in TopOn (Y) \to Y \in K$
30	28 29	syl	$⊢ ((K \in TopOn (Y) \land ran F \subseteq B \land B \subseteq Y) \land (J \in Top \land F : ⋃ J ⟶ B)) \to Y \in K$
31		simpl3	$⊢ ((K \in TopOn (Y) \land ran F \subseteq B \land B \subseteq Y) \land (J \in Top \land F : ⋃ J ⟶ B)) \to B \subseteq Y$
32	30 31	ssexd	$⊢ ((K \in TopOn (Y) \land ran F \subseteq B \land B \subseteq Y) \land (J \in Top \land F : ⋃ J ⟶ B)) \to B \in V$
33		elrest	$⊢ (K \in TopOn (Y) \land B \in V) \to (y \in (K ↾_{𝑡} B) \leftrightarrow \exists x \in K y = x \cap B)$
34	28 32 33	syl2anc	$⊢ ((K \in TopOn (Y) \land ran F \subseteq B \land B \subseteq Y) \land (J \in Top \land F : ⋃ J ⟶ B)) \to (y \in (K ↾_{𝑡} B) \leftrightarrow \exists x \in K y = x \cap B)$
35		imaeq2	$⊢ y = x \cap B \to F^{-1} [y] = F^{-1} [x \cap B]$
36	35	eleq1d	$⊢ y = x \cap B \to (F^{-1} [y] \in J \leftrightarrow F^{-1} [x \cap B] \in J)$
37	36	adantl	$⊢ (((K \in TopOn (Y) \land ran F \subseteq B \land B \subseteq Y) \land (J \in Top \land F : ⋃ J ⟶ B)) \land y = x \cap B) \to (F^{-1} [y] \in J \leftrightarrow F^{-1} [x \cap B] \in J)$
38	27 34 37	ralxfr2d	$⊢ ((K \in TopOn (Y) \land ran F \subseteq B \land B \subseteq Y) \land (J \in Top \land F : ⋃ J ⟶ B)) \to (\forall y \in (K ↾_{𝑡} B) F^{-1} [y] \in J \leftrightarrow \forall x \in K F^{-1} [x \cap B] \in J)$
39		simplrr	$⊢ (((K \in TopOn (Y) \land ran F \subseteq B \land B \subseteq Y) \land (J \in Top \land F : ⋃ J ⟶ B)) \land x \in K) \to F : ⋃ J ⟶ B$
40		ffun	$⊢ F : ⋃ J ⟶ B \to Fun F$
41		inpreima	$⊢ Fun F \to F^{-1} [x \cap B] = F^{-1} [x] \cap F^{-1} [B]$
42	39 40 41	3syl	$⊢ (((K \in TopOn (Y) \land ran F \subseteq B \land B \subseteq Y) \land (J \in Top \land F : ⋃ J ⟶ B)) \land x \in K) \to F^{-1} [x \cap B] = F^{-1} [x] \cap F^{-1} [B]$
43		cnvimass	$⊢ F^{-1} [x] \subseteq dom F$
44		cnvimarndm	$⊢ F^{-1} [ran F] = dom F$
45	43 44	sseqtrri	$⊢ F^{-1} [x] \subseteq F^{-1} [ran F]$
46		simpll2	$⊢ (((K \in TopOn (Y) \land ran F \subseteq B \land B \subseteq Y) \land (J \in Top \land F : ⋃ J ⟶ B)) \land x \in K) \to ran F \subseteq B$
47		imass2	$⊢ ran F \subseteq B \to F^{-1} [ran F] \subseteq F^{-1} [B]$
48	46 47	syl	$⊢ (((K \in TopOn (Y) \land ran F \subseteq B \land B \subseteq Y) \land (J \in Top \land F : ⋃ J ⟶ B)) \land x \in K) \to F^{-1} [ran F] \subseteq F^{-1} [B]$
49	45 48	sstrid	$⊢ (((K \in TopOn (Y) \land ran F \subseteq B \land B \subseteq Y) \land (J \in Top \land F : ⋃ J ⟶ B)) \land x \in K) \to F^{-1} [x] \subseteq F^{-1} [B]$
50		df-ss	$⊢ F^{-1} [x] \subseteq F^{-1} [B] \leftrightarrow F^{-1} [x] \cap F^{-1} [B] = F^{-1} [x]$
51	49 50	sylib	$⊢ (((K \in TopOn (Y) \land ran F \subseteq B \land B \subseteq Y) \land (J \in Top \land F : ⋃ J ⟶ B)) \land x \in K) \to F^{-1} [x] \cap F^{-1} [B] = F^{-1} [x]$
52	42 51	eqtrd	$⊢ (((K \in TopOn (Y) \land ran F \subseteq B \land B \subseteq Y) \land (J \in Top \land F : ⋃ J ⟶ B)) \land x \in K) \to F^{-1} [x \cap B] = F^{-1} [x]$
53	52	eleq1d	$⊢ (((K \in TopOn (Y) \land ran F \subseteq B \land B \subseteq Y) \land (J \in Top \land F : ⋃ J ⟶ B)) \land x \in K) \to (F^{-1} [x \cap B] \in J \leftrightarrow F^{-1} [x] \in J)$
54	53	ralbidva	$⊢ ((K \in TopOn (Y) \land ran F \subseteq B \land B \subseteq Y) \land (J \in Top \land F : ⋃ J ⟶ B)) \to (\forall x \in K F^{-1} [x \cap B] \in J \leftrightarrow \forall x \in K F^{-1} [x] \in J)$
55		simprr	$⊢ ((K \in TopOn (Y) \land ran F \subseteq B \land B \subseteq Y) \land (J \in Top \land F : ⋃ J ⟶ B)) \to F : ⋃ J ⟶ B$
56	55 31	fssd	$⊢ ((K \in TopOn (Y) \land ran F \subseteq B \land B \subseteq Y) \land (J \in Top \land F : ⋃ J ⟶ B)) \to F : ⋃ J ⟶ Y$
57	56	biantrurd	$⊢ ((K \in TopOn (Y) \land ran F \subseteq B \land B \subseteq Y) \land (J \in Top \land F : ⋃ J ⟶ B)) \to (\forall x \in K F^{-1} [x] \in J \leftrightarrow (F : ⋃ J ⟶ Y \land \forall x \in K F^{-1} [x] \in J))$
58	38 54 57	3bitrrd	$⊢ ((K \in TopOn (Y) \land ran F \subseteq B \land B \subseteq Y) \land (J \in Top \land F : ⋃ J ⟶ B)) \to ((F : ⋃ J ⟶ Y \land \forall x \in K F^{-1} [x] \in J) \leftrightarrow \forall y \in (K ↾_{𝑡} B) F^{-1} [y] \in J)$
59	55	biantrurd	$⊢ ((K \in TopOn (Y) \land ran F \subseteq B \land B \subseteq Y) \land (J \in Top \land F : ⋃ J ⟶ B)) \to (\forall y \in (K ↾_{𝑡} B) F^{-1} [y] \in J \leftrightarrow (F : ⋃ J ⟶ B \land \forall y \in (K ↾_{𝑡} B) F^{-1} [y] \in J))$
60	58 59	bitrd	$⊢ ((K \in TopOn (Y) \land ran F \subseteq B \land B \subseteq Y) \land (J \in Top \land F : ⋃ J ⟶ B)) \to ((F : ⋃ J ⟶ Y \land \forall x \in K F^{-1} [x] \in J) \leftrightarrow (F : ⋃ J ⟶ B \land \forall y \in (K ↾_{𝑡} B) F^{-1} [y] \in J))$
61		simprl	$⊢ ((K \in TopOn (Y) \land ran F \subseteq B \land B \subseteq Y) \land (J \in Top \land F : ⋃ J ⟶ B)) \to J \in Top$
62	61 15	sylib	$⊢ ((K \in TopOn (Y) \land ran F \subseteq B \land B \subseteq Y) \land (J \in Top \land F : ⋃ J ⟶ B)) \to J \in TopOn (⋃ J)$
63		iscn	$⊢ (J \in TopOn (⋃ J) \land K \in TopOn (Y)) \to (F \in (J Cn K) \leftrightarrow (F : ⋃ J ⟶ Y \land \forall x \in K F^{-1} [x] \in J))$
64	62 28 63	syl2anc	$⊢ ((K \in TopOn (Y) \land ran F \subseteq B \land B \subseteq Y) \land (J \in Top \land F : ⋃ J ⟶ B)) \to (F \in (J Cn K) \leftrightarrow (F : ⋃ J ⟶ Y \land \forall x \in K F^{-1} [x] \in J))$
65	18	adantr	$⊢ ((K \in TopOn (Y) \land ran F \subseteq B \land B \subseteq Y) \land (J \in Top \land F : ⋃ J ⟶ B)) \to K ↾_{𝑡} B \in TopOn (B)$
66		iscn	$⊢ (J \in TopOn (⋃ J) \land K ↾_{𝑡} B \in TopOn (B)) \to (F \in (J Cn (K ↾_{𝑡} B)) \leftrightarrow (F : ⋃ J ⟶ B \land \forall y \in (K ↾_{𝑡} B) F^{-1} [y] \in J))$
67	62 65 66	syl2anc	$⊢ ((K \in TopOn (Y) \land ran F \subseteq B \land B \subseteq Y) \land (J \in Top \land F : ⋃ J ⟶ B)) \to (F \in (J Cn (K ↾_{𝑡} B)) \leftrightarrow (F : ⋃ J ⟶ B \land \forall y \in (K ↾_{𝑡} B) F^{-1} [y] \in J))$
68	60 64 67	3bitr4d	$⊢ ((K \in TopOn (Y) \land ran F \subseteq B \land B \subseteq Y) \land (J \in Top \land F : ⋃ J ⟶ B)) \to (F \in (J Cn K) \leftrightarrow F \in (J Cn (K ↾_{𝑡} B)))$
69	68	ex	$⊢ (K \in TopOn (Y) \land ran F \subseteq B \land B \subseteq Y) \to ((J \in Top \land F : ⋃ J ⟶ B) \to (F \in (J Cn K) \leftrightarrow F \in (J Cn (K ↾_{𝑡} B))))$
70	12 24 69	pm5.21ndd	$⊢ (K \in TopOn (Y) \land ran F \subseteq B \land B \subseteq Y) \to (F \in (J Cn K) \leftrightarrow F \in (J Cn (K ↾_{𝑡} B)))$

Metamath Proof Explorer

Theorem cnrest2

Proof