cnprest2

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)

	Ref	Expression
Hypotheses	cnprest.1	$⊢ X = ⋃ J$
	cnprest.2	$⊢ Y = ⋃ K$
Assertion	cnprest2	$⊢ (K \in Top \land F : X ⟶ B \land B \subseteq Y) \to (F \in (J CnP K) (P) \leftrightarrow F \in (J CnP (K ↾_{𝑡} B)) (P))$

Proof

Step	Hyp	Ref	Expression
1		cnprest.1	$⊢ X = ⋃ J$
2		cnprest.2	$⊢ Y = ⋃ K$
3		cnptop1	$⊢ F \in (J CnP K) (P) \to J \in Top$
4	1	cnprcl	$⊢ F \in (J CnP K) (P) \to P \in X$
5	3 4	jca	$⊢ F \in (J CnP K) (P) \to (J \in Top \land P \in X)$
6	5	a1i	$⊢ (K \in Top \land F : X ⟶ B \land B \subseteq Y) \to (F \in (J CnP K) (P) \to (J \in Top \land P \in X))$
7		cnptop1	$⊢ F \in (J CnP (K ↾_{𝑡} B)) (P) \to J \in Top$
8	1	cnprcl	$⊢ F \in (J CnP (K ↾_{𝑡} B)) (P) \to P \in X$
9	7 8	jca	$⊢ F \in (J CnP (K ↾_{𝑡} B)) (P) \to (J \in Top \land P \in X)$
10	9	a1i	$⊢ (K \in Top \land F : X ⟶ B \land B \subseteq Y) \to (F \in (J CnP (K ↾_{𝑡} B)) (P) \to (J \in Top \land P \in X))$
11		simpl2	$⊢ ((K \in Top \land F : X ⟶ B \land B \subseteq Y) \land (J \in Top \land P \in X)) \to F : X ⟶ B$
12		simprr	$⊢ ((K \in Top \land F : X ⟶ B \land B \subseteq Y) \land (J \in Top \land P \in X)) \to P \in X$
13	11 12	ffvelrnd	$⊢ ((K \in Top \land F : X ⟶ B \land B \subseteq Y) \land (J \in Top \land P \in X)) \to F (P) \in B$
14	13	biantrud	$⊢ ((K \in Top \land F : X ⟶ B \land B \subseteq Y) \land (J \in Top \land P \in X)) \to (F (P) \in x \leftrightarrow (F (P) \in x \land F (P) \in B))$
15		elin	$⊢ F (P) \in (x \cap B) \leftrightarrow (F (P) \in x \land F (P) \in B)$
16	14 15	bitr4di	$⊢ ((K \in Top \land F : X ⟶ B \land B \subseteq Y) \land (J \in Top \land P \in X)) \to (F (P) \in x \leftrightarrow F (P) \in (x \cap B))$
17		imassrn	$⊢ F [y] \subseteq ran F$
18	11	frnd	$⊢ ((K \in Top \land F : X ⟶ B \land B \subseteq Y) \land (J \in Top \land P \in X)) \to ran F \subseteq B$
19	17 18	sstrid	$⊢ ((K \in Top \land F : X ⟶ B \land B \subseteq Y) \land (J \in Top \land P \in X)) \to F [y] \subseteq B$
20	19	biantrud	$⊢ ((K \in Top \land F : X ⟶ B \land B \subseteq Y) \land (J \in Top \land P \in X)) \to (F [y] \subseteq x \leftrightarrow (F [y] \subseteq x \land F [y] \subseteq B))$
21		ssin	$⊢ (F [y] \subseteq x \land F [y] \subseteq B) \leftrightarrow F [y] \subseteq x \cap B$
22	20 21	bitrdi	$⊢ ((K \in Top \land F : X ⟶ B \land B \subseteq Y) \land (J \in Top \land P \in X)) \to (F [y] \subseteq x \leftrightarrow F [y] \subseteq x \cap B)$
23	22	anbi2d	$⊢ ((K \in Top \land F : X ⟶ B \land B \subseteq Y) \land (J \in Top \land P \in X)) \to ((P \in y \land F [y] \subseteq x) \leftrightarrow (P \in y \land F [y] \subseteq x \cap B))$
24	23	rexbidv	$⊢ ((K \in Top \land F : X ⟶ B \land B \subseteq Y) \land (J \in Top \land P \in X)) \to (\exists y \in J (P \in y \land F [y] \subseteq x) \leftrightarrow \exists y \in J (P \in y \land F [y] \subseteq x \cap B))$
25	16 24	imbi12d	$⊢ ((K \in Top \land F : X ⟶ B \land B \subseteq Y) \land (J \in Top \land P \in X)) \to ((F (P) \in x \to \exists y \in J (P \in y \land F [y] \subseteq x)) \leftrightarrow (F (P) \in (x \cap B) \to \exists y \in J (P \in y \land F [y] \subseteq x \cap B)))$
26	25	ralbidv	$⊢ ((K \in Top \land F : X ⟶ B \land B \subseteq Y) \land (J \in Top \land P \in X)) \to (\forall x \in K (F (P) \in x \to \exists y \in J (P \in y \land F [y] \subseteq x)) \leftrightarrow \forall x \in K (F (P) \in (x \cap B) \to \exists y \in J (P \in y \land F [y] \subseteq x \cap B)))$
27		vex	$⊢ x \in V$
28	27	inex1	$⊢ x \cap B \in V$
29	28	a1i	$⊢ (((K \in Top \land F : X ⟶ B \land B \subseteq Y) \land (J \in Top \land P \in X)) \land x \in K) \to x \cap B \in V$
30		simpl1	$⊢ ((K \in Top \land F : X ⟶ B \land B \subseteq Y) \land (J \in Top \land P \in X)) \to K \in Top$
31		uniexg	$⊢ K \in Top \to ⋃ K \in V$
32	2 31	eqeltrid	$⊢ K \in Top \to Y \in V$
33	30 32	syl	$⊢ ((K \in Top \land F : X ⟶ B \land B \subseteq Y) \land (J \in Top \land P \in X)) \to Y \in V$
34		simpl3	$⊢ ((K \in Top \land F : X ⟶ B \land B \subseteq Y) \land (J \in Top \land P \in X)) \to B \subseteq Y$
35	33 34	ssexd	$⊢ ((K \in Top \land F : X ⟶ B \land B \subseteq Y) \land (J \in Top \land P \in X)) \to B \in V$
36		elrest	$⊢ (K \in Top \land B \in V) \to (z \in (K ↾_{𝑡} B) \leftrightarrow \exists x \in K z = x \cap B)$
37	30 35 36	syl2anc	$⊢ ((K \in Top \land F : X ⟶ B \land B \subseteq Y) \land (J \in Top \land P \in X)) \to (z \in (K ↾_{𝑡} B) \leftrightarrow \exists x \in K z = x \cap B)$
38		eleq2	$⊢ z = x \cap B \to (F (P) \in z \leftrightarrow F (P) \in (x \cap B))$
39		sseq2	$⊢ z = x \cap B \to (F [y] \subseteq z \leftrightarrow F [y] \subseteq x \cap B)$
40	39	anbi2d	$⊢ z = x \cap B \to ((P \in y \land F [y] \subseteq z) \leftrightarrow (P \in y \land F [y] \subseteq x \cap B))$
41	40	rexbidv	$⊢ z = x \cap B \to (\exists y \in J (P \in y \land F [y] \subseteq z) \leftrightarrow \exists y \in J (P \in y \land F [y] \subseteq x \cap B))$
42	38 41	imbi12d	$⊢ z = x \cap B \to ((F (P) \in z \to \exists y \in J (P \in y \land F [y] \subseteq z)) \leftrightarrow (F (P) \in (x \cap B) \to \exists y \in J (P \in y \land F [y] \subseteq x \cap B)))$
43	42	adantl	$⊢ (((K \in Top \land F : X ⟶ B \land B \subseteq Y) \land (J \in Top \land P \in X)) \land z = x \cap B) \to ((F (P) \in z \to \exists y \in J (P \in y \land F [y] \subseteq z)) \leftrightarrow (F (P) \in (x \cap B) \to \exists y \in J (P \in y \land F [y] \subseteq x \cap B)))$
44	29 37 43	ralxfr2d	$⊢ ((K \in Top \land F : X ⟶ B \land B \subseteq Y) \land (J \in Top \land P \in X)) \to (\forall z \in (K ↾_{𝑡} B) (F (P) \in z \to \exists y \in J (P \in y \land F [y] \subseteq z)) \leftrightarrow \forall x \in K (F (P) \in (x \cap B) \to \exists y \in J (P \in y \land F [y] \subseteq x \cap B)))$
45	26 44	bitr4d	$⊢ ((K \in Top \land F : X ⟶ B \land B \subseteq Y) \land (J \in Top \land P \in X)) \to (\forall x \in K (F (P) \in x \to \exists y \in J (P \in y \land F [y] \subseteq x)) \leftrightarrow \forall z \in (K ↾_{𝑡} B) (F (P) \in z \to \exists y \in J (P \in y \land F [y] \subseteq z)))$
46	11 34	fssd	$⊢ ((K \in Top \land F : X ⟶ B \land B \subseteq Y) \land (J \in Top \land P \in X)) \to F : X ⟶ Y$
47		simprl	$⊢ ((K \in Top \land F : X ⟶ B \land B \subseteq Y) \land (J \in Top \land P \in X)) \to J \in Top$
48	1 2	iscnp2	$⊢ F \in (J CnP K) (P) \leftrightarrow ((J \in Top \land K \in Top \land P \in X) \land (F : X ⟶ Y \land \forall x \in K (F (P) \in x \to \exists y \in J (P \in y \land F [y] \subseteq x))))$
49	48	baib	$⊢ (J \in Top \land K \in Top \land P \in X) \to (F \in (J CnP K) (P) \leftrightarrow (F : X ⟶ Y \land \forall x \in K (F (P) \in x \to \exists y \in J (P \in y \land F [y] \subseteq x))))$
50	47 30 12 49	syl3anc	$⊢ ((K \in Top \land F : X ⟶ B \land B \subseteq Y) \land (J \in Top \land P \in X)) \to (F \in (J CnP K) (P) \leftrightarrow (F : X ⟶ Y \land \forall x \in K (F (P) \in x \to \exists y \in J (P \in y \land F [y] \subseteq x))))$
51	46 50	mpbirand	$⊢ ((K \in Top \land F : X ⟶ B \land B \subseteq Y) \land (J \in Top \land P \in X)) \to (F \in (J CnP K) (P) \leftrightarrow \forall x \in K (F (P) \in x \to \exists y \in J (P \in y \land F [y] \subseteq x)))$
52	1	toptopon	$⊢ J \in Top \leftrightarrow J \in TopOn (X)$
53	47 52	sylib	$⊢ ((K \in Top \land F : X ⟶ B \land B \subseteq Y) \land (J \in Top \land P \in X)) \to J \in TopOn (X)$
54	2	toptopon	$⊢ K \in Top \leftrightarrow K \in TopOn (Y)$
55	30 54	sylib	$⊢ ((K \in Top \land F : X ⟶ B \land B \subseteq Y) \land (J \in Top \land P \in X)) \to K \in TopOn (Y)$
56		resttopon	$⊢ (K \in TopOn (Y) \land B \subseteq Y) \to K ↾_{𝑡} B \in TopOn (B)$
57	55 34 56	syl2anc	$⊢ ((K \in Top \land F : X ⟶ B \land B \subseteq Y) \land (J \in Top \land P \in X)) \to K ↾_{𝑡} B \in TopOn (B)$
58		iscnp	$⊢ (J \in TopOn (X) \land K ↾_{𝑡} B \in TopOn (B) \land P \in X) \to (F \in (J CnP (K ↾_{𝑡} B)) (P) \leftrightarrow (F : X ⟶ B \land \forall z \in (K ↾_{𝑡} B) (F (P) \in z \to \exists y \in J (P \in y \land F [y] \subseteq z))))$
59	53 57 12 58	syl3anc	$⊢ ((K \in Top \land F : X ⟶ B \land B \subseteq Y) \land (J \in Top \land P \in X)) \to (F \in (J CnP (K ↾_{𝑡} B)) (P) \leftrightarrow (F : X ⟶ B \land \forall z \in (K ↾_{𝑡} B) (F (P) \in z \to \exists y \in J (P \in y \land F [y] \subseteq z))))$
60	11 59	mpbirand	$⊢ ((K \in Top \land F : X ⟶ B \land B \subseteq Y) \land (J \in Top \land P \in X)) \to (F \in (J CnP (K ↾_{𝑡} B)) (P) \leftrightarrow \forall z \in (K ↾_{𝑡} B) (F (P) \in z \to \exists y \in J (P \in y \land F [y] \subseteq z)))$
61	45 51 60	3bitr4d	$⊢ ((K \in Top \land F : X ⟶ B \land B \subseteq Y) \land (J \in Top \land P \in X)) \to (F \in (J CnP K) (P) \leftrightarrow F \in (J CnP (K ↾_{𝑡} B)) (P))$
62	61	ex	$⊢ (K \in Top \land F : X ⟶ B \land B \subseteq Y) \to ((J \in Top \land P \in X) \to (F \in (J CnP K) (P) \leftrightarrow F \in (J CnP (K ↾_{𝑡} B)) (P)))$
63	6 10 62	pm5.21ndd	$⊢ (K \in Top \land F : X ⟶ B \land B \subseteq Y) \to (F \in (J CnP K) (P) \leftrightarrow F \in (J CnP (K ↾_{𝑡} B)) (P))$

Metamath Proof Explorer

Theorem cnprest2

Proof