iscnp4

Description: The predicate "the class F is a continuous function from topology J to topology K at point P " in terms of neighborhoods. (Contributed by FL, 18-Jul-2011) (Revised by Mario Carneiro, 10-Sep-2015)

		Ref	Expression
	Assertion	iscnp4	$⊢ (J \in TopOn (X) \land K \in TopOn (Y) \land P \in X) \to (F \in (J CnP K) (P) \leftrightarrow (F : X ⟶ Y \land \forall y \in nei (K) (\{F (P)\}) \exists x \in nei (J) (\{P\}) F [x] \subseteq y))$

Proof

Step	Hyp	Ref	Expression
1		cnpf2	$⊢ (J \in TopOn (X) \land K \in TopOn (Y) \land F \in (J CnP K) (P)) \to F : X ⟶ Y$
2	1	3expa	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y)) \land F \in (J CnP K) (P)) \to F : X ⟶ Y$
3	2	3adantl3	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y) \land P \in X) \land F \in (J CnP K) (P)) \to F : X ⟶ Y$
4		simplr	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y) \land P \in X) \land F \in (J CnP K) (P)) \land y \in nei (K) (\{F (P)\})) \to F \in (J CnP K) (P)$
5		simpll2	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y) \land P \in X) \land F \in (J CnP K) (P)) \land y \in nei (K) (\{F (P)\})) \to K \in TopOn (Y)$
6		topontop	$⊢ K \in TopOn (Y) \to K \in Top$
7	5 6	syl	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y) \land P \in X) \land F \in (J CnP K) (P)) \land y \in nei (K) (\{F (P)\})) \to K \in Top$
8		eqid	$⊢ ⋃ K = ⋃ K$
9	8	neii1	$⊢ (K \in Top \land y \in nei (K) (\{F (P)\})) \to y \subseteq ⋃ K$
10	7 9	sylancom	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y) \land P \in X) \land F \in (J CnP K) (P)) \land y \in nei (K) (\{F (P)\})) \to y \subseteq ⋃ K$
11	8	ntropn	$⊢ (K \in Top \land y \subseteq ⋃ K) \to int (K) (y) \in K$
12	7 10 11	syl2anc	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y) \land P \in X) \land F \in (J CnP K) (P)) \land y \in nei (K) (\{F (P)\})) \to int (K) (y) \in K$
13		simpr	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y) \land P \in X) \land F \in (J CnP K) (P)) \land y \in nei (K) (\{F (P)\})) \to y \in nei (K) (\{F (P)\})$
14	3	adantr	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y) \land P \in X) \land F \in (J CnP K) (P)) \land y \in nei (K) (\{F (P)\})) \to F : X ⟶ Y$
15		simpll3	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y) \land P \in X) \land F \in (J CnP K) (P)) \land y \in nei (K) (\{F (P)\})) \to P \in X$
16	14 15	ffvelrnd	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y) \land P \in X) \land F \in (J CnP K) (P)) \land y \in nei (K) (\{F (P)\})) \to F (P) \in Y$
17		toponuni	$⊢ K \in TopOn (Y) \to Y = ⋃ K$
18	5 17	syl	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y) \land P \in X) \land F \in (J CnP K) (P)) \land y \in nei (K) (\{F (P)\})) \to Y = ⋃ K$
19	16 18	eleqtrd	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y) \land P \in X) \land F \in (J CnP K) (P)) \land y \in nei (K) (\{F (P)\})) \to F (P) \in ⋃ K$
20	19	snssd	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y) \land P \in X) \land F \in (J CnP K) (P)) \land y \in nei (K) (\{F (P)\})) \to \{F (P)\} \subseteq ⋃ K$
21	8	neiint	$⊢ (K \in Top \land \{F (P)\} \subseteq ⋃ K \land y \subseteq ⋃ K) \to (y \in nei (K) (\{F (P)\}) \leftrightarrow \{F (P)\} \subseteq int (K) (y))$
22	7 20 10 21	syl3anc	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y) \land P \in X) \land F \in (J CnP K) (P)) \land y \in nei (K) (\{F (P)\})) \to (y \in nei (K) (\{F (P)\}) \leftrightarrow \{F (P)\} \subseteq int (K) (y))$
23	13 22	mpbid	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y) \land P \in X) \land F \in (J CnP K) (P)) \land y \in nei (K) (\{F (P)\})) \to \{F (P)\} \subseteq int (K) (y)$
24		fvex	$⊢ F (P) \in V$
25	24	snss	$⊢ F (P) \in int (K) (y) \leftrightarrow \{F (P)\} \subseteq int (K) (y)$
26	23 25	sylibr	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y) \land P \in X) \land F \in (J CnP K) (P)) \land y \in nei (K) (\{F (P)\})) \to F (P) \in int (K) (y)$
27		cnpimaex	$⊢ (F \in (J CnP K) (P) \land int (K) (y) \in K \land F (P) \in int (K) (y)) \to \exists x \in J (P \in x \land F [x] \subseteq int (K) (y))$
28	4 12 26 27	syl3anc	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y) \land P \in X) \land F \in (J CnP K) (P)) \land y \in nei (K) (\{F (P)\})) \to \exists x \in J (P \in x \land F [x] \subseteq int (K) (y))$
29		simpl1	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y) \land P \in X) \land F \in (J CnP K) (P)) \to J \in TopOn (X)$
30	29	ad2antrr	$⊢ ((((J \in TopOn (X) \land K \in TopOn (Y) \land P \in X) \land F \in (J CnP K) (P)) \land y \in nei (K) (\{F (P)\})) \land (x \in J \land (P \in x \land F [x] \subseteq int (K) (y)))) \to J \in TopOn (X)$
31		topontop	$⊢ J \in TopOn (X) \to J \in Top$
32	30 31	syl	$⊢ ((((J \in TopOn (X) \land K \in TopOn (Y) \land P \in X) \land F \in (J CnP K) (P)) \land y \in nei (K) (\{F (P)\})) \land (x \in J \land (P \in x \land F [x] \subseteq int (K) (y)))) \to J \in Top$
33		simprl	$⊢ ((((J \in TopOn (X) \land K \in TopOn (Y) \land P \in X) \land F \in (J CnP K) (P)) \land y \in nei (K) (\{F (P)\})) \land (x \in J \land (P \in x \land F [x] \subseteq int (K) (y)))) \to x \in J$
34		simprrl	$⊢ ((((J \in TopOn (X) \land K \in TopOn (Y) \land P \in X) \land F \in (J CnP K) (P)) \land y \in nei (K) (\{F (P)\})) \land (x \in J \land (P \in x \land F [x] \subseteq int (K) (y)))) \to P \in x$
35		opnneip	$⊢ (J \in Top \land x \in J \land P \in x) \to x \in nei (J) (\{P\})$
36	32 33 34 35	syl3anc	$⊢ ((((J \in TopOn (X) \land K \in TopOn (Y) \land P \in X) \land F \in (J CnP K) (P)) \land y \in nei (K) (\{F (P)\})) \land (x \in J \land (P \in x \land F [x] \subseteq int (K) (y)))) \to x \in nei (J) (\{P\})$
37		simprrr	$⊢ ((((J \in TopOn (X) \land K \in TopOn (Y) \land P \in X) \land F \in (J CnP K) (P)) \land y \in nei (K) (\{F (P)\})) \land (x \in J \land (P \in x \land F [x] \subseteq int (K) (y)))) \to F [x] \subseteq int (K) (y)$
38	8	ntrss2	$⊢ (K \in Top \land y \subseteq ⋃ K) \to int (K) (y) \subseteq y$
39	7 10 38	syl2anc	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y) \land P \in X) \land F \in (J CnP K) (P)) \land y \in nei (K) (\{F (P)\})) \to int (K) (y) \subseteq y$
40	39	adantr	$⊢ ((((J \in TopOn (X) \land K \in TopOn (Y) \land P \in X) \land F \in (J CnP K) (P)) \land y \in nei (K) (\{F (P)\})) \land (x \in J \land (P \in x \land F [x] \subseteq int (K) (y)))) \to int (K) (y) \subseteq y$
41	37 40	sstrd	$⊢ ((((J \in TopOn (X) \land K \in TopOn (Y) \land P \in X) \land F \in (J CnP K) (P)) \land y \in nei (K) (\{F (P)\})) \land (x \in J \land (P \in x \land F [x] \subseteq int (K) (y)))) \to F [x] \subseteq y$
42	28 36 41	reximssdv	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y) \land P \in X) \land F \in (J CnP K) (P)) \land y \in nei (K) (\{F (P)\})) \to \exists x \in nei (J) (\{P\}) F [x] \subseteq y$
43	42	ralrimiva	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y) \land P \in X) \land F \in (J CnP K) (P)) \to \forall y \in nei (K) (\{F (P)\}) \exists x \in nei (J) (\{P\}) F [x] \subseteq y$
44	3 43	jca	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y) \land P \in X) \land F \in (J CnP K) (P)) \to (F : X ⟶ Y \land \forall y \in nei (K) (\{F (P)\}) \exists x \in nei (J) (\{P\}) F [x] \subseteq y)$
45	44	ex	$⊢ (J \in TopOn (X) \land K \in TopOn (Y) \land P \in X) \to (F \in (J CnP K) (P) \to (F : X ⟶ Y \land \forall y \in nei (K) (\{F (P)\}) \exists x \in nei (J) (\{P\}) F [x] \subseteq y))$
46		simpll2	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y) \land P \in X) \land F : X ⟶ Y) \land (y \in K \land F (P) \in y)) \to K \in TopOn (Y)$
47	46 6	syl	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y) \land P \in X) \land F : X ⟶ Y) \land (y \in K \land F (P) \in y)) \to K \in Top$
48		simprl	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y) \land P \in X) \land F : X ⟶ Y) \land (y \in K \land F (P) \in y)) \to y \in K$
49		simprr	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y) \land P \in X) \land F : X ⟶ Y) \land (y \in K \land F (P) \in y)) \to F (P) \in y$
50		opnneip	$⊢ (K \in Top \land y \in K \land F (P) \in y) \to y \in nei (K) (\{F (P)\})$
51	47 48 49 50	syl3anc	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y) \land P \in X) \land F : X ⟶ Y) \land (y \in K \land F (P) \in y)) \to y \in nei (K) (\{F (P)\})$
52		simpl1	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y) \land P \in X) \land F : X ⟶ Y) \to J \in TopOn (X)$
53	52	ad2antrr	$⊢ ((((J \in TopOn (X) \land K \in TopOn (Y) \land P \in X) \land F : X ⟶ Y) \land (y \in K \land F (P) \in y)) \land (x \in nei (J) (\{P\}) \land F [x] \subseteq y)) \to J \in TopOn (X)$
54	53 31	syl	$⊢ ((((J \in TopOn (X) \land K \in TopOn (Y) \land P \in X) \land F : X ⟶ Y) \land (y \in K \land F (P) \in y)) \land (x \in nei (J) (\{P\}) \land F [x] \subseteq y)) \to J \in Top$
55		simprl	$⊢ ((((J \in TopOn (X) \land K \in TopOn (Y) \land P \in X) \land F : X ⟶ Y) \land (y \in K \land F (P) \in y)) \land (x \in nei (J) (\{P\}) \land F [x] \subseteq y)) \to x \in nei (J) (\{P\})$
56		eqid	$⊢ ⋃ J = ⋃ J$
57	56	neii1	$⊢ (J \in Top \land x \in nei (J) (\{P\})) \to x \subseteq ⋃ J$
58	54 55 57	syl2anc	$⊢ ((((J \in TopOn (X) \land K \in TopOn (Y) \land P \in X) \land F : X ⟶ Y) \land (y \in K \land F (P) \in y)) \land (x \in nei (J) (\{P\}) \land F [x] \subseteq y)) \to x \subseteq ⋃ J$
59	56	ntropn	$⊢ (J \in Top \land x \subseteq ⋃ J) \to int (J) (x) \in J$
60	54 58 59	syl2anc	$⊢ ((((J \in TopOn (X) \land K \in TopOn (Y) \land P \in X) \land F : X ⟶ Y) \land (y \in K \land F (P) \in y)) \land (x \in nei (J) (\{P\}) \land F [x] \subseteq y)) \to int (J) (x) \in J$
61		simpll3	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y) \land P \in X) \land F : X ⟶ Y) \land (y \in K \land F (P) \in y)) \to P \in X$
62	61	adantr	$⊢ ((((J \in TopOn (X) \land K \in TopOn (Y) \land P \in X) \land F : X ⟶ Y) \land (y \in K \land F (P) \in y)) \land (x \in nei (J) (\{P\}) \land F [x] \subseteq y)) \to P \in X$
63		toponuni	$⊢ J \in TopOn (X) \to X = ⋃ J$
64	53 63	syl	$⊢ ((((J \in TopOn (X) \land K \in TopOn (Y) \land P \in X) \land F : X ⟶ Y) \land (y \in K \land F (P) \in y)) \land (x \in nei (J) (\{P\}) \land F [x] \subseteq y)) \to X = ⋃ J$
65	62 64	eleqtrd	$⊢ ((((J \in TopOn (X) \land K \in TopOn (Y) \land P \in X) \land F : X ⟶ Y) \land (y \in K \land F (P) \in y)) \land (x \in nei (J) (\{P\}) \land F [x] \subseteq y)) \to P \in ⋃ J$
66	65	snssd	$⊢ ((((J \in TopOn (X) \land K \in TopOn (Y) \land P \in X) \land F : X ⟶ Y) \land (y \in K \land F (P) \in y)) \land (x \in nei (J) (\{P\}) \land F [x] \subseteq y)) \to \{P\} \subseteq ⋃ J$
67	56	neiint	$⊢ (J \in Top \land \{P\} \subseteq ⋃ J \land x \subseteq ⋃ J) \to (x \in nei (J) (\{P\}) \leftrightarrow \{P\} \subseteq int (J) (x))$
68	54 66 58 67	syl3anc	$⊢ ((((J \in TopOn (X) \land K \in TopOn (Y) \land P \in X) \land F : X ⟶ Y) \land (y \in K \land F (P) \in y)) \land (x \in nei (J) (\{P\}) \land F [x] \subseteq y)) \to (x \in nei (J) (\{P\}) \leftrightarrow \{P\} \subseteq int (J) (x))$
69	55 68	mpbid	$⊢ ((((J \in TopOn (X) \land K \in TopOn (Y) \land P \in X) \land F : X ⟶ Y) \land (y \in K \land F (P) \in y)) \land (x \in nei (J) (\{P\}) \land F [x] \subseteq y)) \to \{P\} \subseteq int (J) (x)$
70		snssg	$⊢ P \in X \to (P \in int (J) (x) \leftrightarrow \{P\} \subseteq int (J) (x))$
71	62 70	syl	$⊢ ((((J \in TopOn (X) \land K \in TopOn (Y) \land P \in X) \land F : X ⟶ Y) \land (y \in K \land F (P) \in y)) \land (x \in nei (J) (\{P\}) \land F [x] \subseteq y)) \to (P \in int (J) (x) \leftrightarrow \{P\} \subseteq int (J) (x))$
72	69 71	mpbird	$⊢ ((((J \in TopOn (X) \land K \in TopOn (Y) \land P \in X) \land F : X ⟶ Y) \land (y \in K \land F (P) \in y)) \land (x \in nei (J) (\{P\}) \land F [x] \subseteq y)) \to P \in int (J) (x)$
73	56	ntrss2	$⊢ (J \in Top \land x \subseteq ⋃ J) \to int (J) (x) \subseteq x$
74	54 58 73	syl2anc	$⊢ ((((J \in TopOn (X) \land K \in TopOn (Y) \land P \in X) \land F : X ⟶ Y) \land (y \in K \land F (P) \in y)) \land (x \in nei (J) (\{P\}) \land F [x] \subseteq y)) \to int (J) (x) \subseteq x$
75		imass2	$⊢ int (J) (x) \subseteq x \to F [int (J) (x)] \subseteq F [x]$
76	74 75	syl	$⊢ ((((J \in TopOn (X) \land K \in TopOn (Y) \land P \in X) \land F : X ⟶ Y) \land (y \in K \land F (P) \in y)) \land (x \in nei (J) (\{P\}) \land F [x] \subseteq y)) \to F [int (J) (x)] \subseteq F [x]$
77		simprr	$⊢ ((((J \in TopOn (X) \land K \in TopOn (Y) \land P \in X) \land F : X ⟶ Y) \land (y \in K \land F (P) \in y)) \land (x \in nei (J) (\{P\}) \land F [x] \subseteq y)) \to F [x] \subseteq y$
78	76 77	sstrd	$⊢ ((((J \in TopOn (X) \land K \in TopOn (Y) \land P \in X) \land F : X ⟶ Y) \land (y \in K \land F (P) \in y)) \land (x \in nei (J) (\{P\}) \land F [x] \subseteq y)) \to F [int (J) (x)] \subseteq y$
79		eleq2	$⊢ z = int (J) (x) \to (P \in z \leftrightarrow P \in int (J) (x))$
80		imaeq2	$⊢ z = int (J) (x) \to F [z] = F [int (J) (x)]$
81	80	sseq1d	$⊢ z = int (J) (x) \to (F [z] \subseteq y \leftrightarrow F [int (J) (x)] \subseteq y)$
82	79 81	anbi12d	$⊢ z = int (J) (x) \to ((P \in z \land F [z] \subseteq y) \leftrightarrow (P \in int (J) (x) \land F [int (J) (x)] \subseteq y))$
83	82	rspcev	$⊢ (int (J) (x) \in J \land (P \in int (J) (x) \land F [int (J) (x)] \subseteq y)) \to \exists z \in J (P \in z \land F [z] \subseteq y)$
84	60 72 78 83	syl12anc	$⊢ ((((J \in TopOn (X) \land K \in TopOn (Y) \land P \in X) \land F : X ⟶ Y) \land (y \in K \land F (P) \in y)) \land (x \in nei (J) (\{P\}) \land F [x] \subseteq y)) \to \exists z \in J (P \in z \land F [z] \subseteq y)$
85	84	rexlimdvaa	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y) \land P \in X) \land F : X ⟶ Y) \land (y \in K \land F (P) \in y)) \to (\exists x \in nei (J) (\{P\}) F [x] \subseteq y \to \exists z \in J (P \in z \land F [z] \subseteq y))$
86	51 85	embantd	$⊢ (((J \in TopOn (X) \land K \in TopOn (Y) \land P \in X) \land F : X ⟶ Y) \land (y \in K \land F (P) \in y)) \to ((y \in nei (K) (\{F (P)\}) \to \exists x \in nei (J) (\{P\}) F [x] \subseteq y) \to \exists z \in J (P \in z \land F [z] \subseteq y))$
87	86	ex	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y) \land P \in X) \land F : X ⟶ Y) \to ((y \in K \land F (P) \in y) \to ((y \in nei (K) (\{F (P)\}) \to \exists x \in nei (J) (\{P\}) F [x] \subseteq y) \to \exists z \in J (P \in z \land F [z] \subseteq y)))$
88	87	com23	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y) \land P \in X) \land F : X ⟶ Y) \to ((y \in nei (K) (\{F (P)\}) \to \exists x \in nei (J) (\{P\}) F [x] \subseteq y) \to ((y \in K \land F (P) \in y) \to \exists z \in J (P \in z \land F [z] \subseteq y)))$
89	88	exp4a	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y) \land P \in X) \land F : X ⟶ Y) \to ((y \in nei (K) (\{F (P)\}) \to \exists x \in nei (J) (\{P\}) F [x] \subseteq y) \to (y \in K \to (F (P) \in y \to \exists z \in J (P \in z \land F [z] \subseteq y))))$
90	89	ralimdv2	$⊢ ((J \in TopOn (X) \land K \in TopOn (Y) \land P \in X) \land F : X ⟶ Y) \to (\forall y \in nei (K) (\{F (P)\}) \exists x \in nei (J) (\{P\}) F [x] \subseteq y \to \forall y \in K (F (P) \in y \to \exists z \in J (P \in z \land F [z] \subseteq y)))$
91	90	imdistanda	$⊢ (J \in TopOn (X) \land K \in TopOn (Y) \land P \in X) \to ((F : X ⟶ Y \land \forall y \in nei (K) (\{F (P)\}) \exists x \in nei (J) (\{P\}) F [x] \subseteq y) \to (F : X ⟶ Y \land \forall y \in K (F (P) \in y \to \exists z \in J (P \in z \land F [z] \subseteq y))))$
92		iscnp	$⊢ (J \in TopOn (X) \land K \in TopOn (Y) \land P \in X) \to (F \in (J CnP K) (P) \leftrightarrow (F : X ⟶ Y \land \forall y \in K (F (P) \in y \to \exists z \in J (P \in z \land F [z] \subseteq y))))$
93	91 92	sylibrd	$⊢ (J \in TopOn (X) \land K \in TopOn (Y) \land P \in X) \to ((F : X ⟶ Y \land \forall y \in nei (K) (\{F (P)\}) \exists x \in nei (J) (\{P\}) F [x] \subseteq y) \to F \in (J CnP K) (P))$
94	45 93	impbid	$⊢ (J \in TopOn (X) \land K \in TopOn (Y) \land P \in X) \to (F \in (J CnP K) (P) \leftrightarrow (F : X ⟶ Y \land \forall y \in nei (K) (\{F (P)\}) \exists x \in nei (J) (\{P\}) F [x] \subseteq y))$

Metamath Proof Explorer

Theorem iscnp4

Proof