cnextfres1

Description: F and its extension by continuity agree on the domain of F . (Contributed by Thierry Arnoux, 17-Jan-2018)

	Ref	Expression
Hypotheses	cnextf.1	$⊢ C = ⋃ J$
	cnextf.2	$⊢ B = ⋃ K$
	cnextf.3	$⊢ φ \to J \in Top$
	cnextf.4	$⊢ φ \to K \in Haus$
	cnextf.5	$⊢ φ \to F : A ⟶ B$
	cnextf.a	$⊢ φ \to A \subseteq C$
	cnextf.6	$⊢ φ \to cls (J) (A) = C$
	cnextf.7	$⊢ (φ \land x \in C) \to (K fLimf (nei (J) (\{x\}) ↾_{𝑡} A)) (F) \neq \emptyset$
	cnextcn.8	$⊢ φ \to K \in Reg$
	cnextfres1.1	$⊢ φ \to F \in ((J ↾_{𝑡} A) Cn K)$
Assertion	cnextfres1	$⊢ φ \to {(J CnExt K) (F) ↾}_{A} = F$

Proof

Step	Hyp	Ref	Expression
1		cnextf.1	$⊢ C = ⋃ J$
2		cnextf.2	$⊢ B = ⋃ K$
3		cnextf.3	$⊢ φ \to J \in Top$
4		cnextf.4	$⊢ φ \to K \in Haus$
5		cnextf.5	$⊢ φ \to F : A ⟶ B$
6		cnextf.a	$⊢ φ \to A \subseteq C$
7		cnextf.6	$⊢ φ \to cls (J) (A) = C$
8		cnextf.7	$⊢ (φ \land x \in C) \to (K fLimf (nei (J) (\{x\}) ↾_{𝑡} A)) (F) \neq \emptyset$
9		cnextcn.8	$⊢ φ \to K \in Reg$
10		cnextfres1.1	$⊢ φ \to F \in ((J ↾_{𝑡} A) Cn K)$
11	1 2 3 4 5 6 7 8	cnextf	$⊢ φ \to (J CnExt K) (F) : C ⟶ B$
12	11	ffnd	$⊢ φ \to (J CnExt K) (F) Fn C$
13		fnssres	$⊢ ((J CnExt K) (F) Fn C \land A \subseteq C) \to ({(J CnExt K) (F) ↾}_{A}) Fn A$
14	12 6 13	syl2anc	$⊢ φ \to ({(J CnExt K) (F) ↾}_{A}) Fn A$
15	5	ffnd	$⊢ φ \to F Fn A$
16		fvres	$⊢ y \in A \to ({(J CnExt K) (F) ↾}_{A}) (y) = (J CnExt K) (F) (y)$
17	16	adantl	$⊢ (φ \land y \in A) \to ({(J CnExt K) (F) ↾}_{A}) (y) = (J CnExt K) (F) (y)$
18	6	sselda	$⊢ (φ \land y \in A) \to y \in C$
19	1 2 3 4 5 6 7 8	cnextfvval	$⊢ (φ \land y \in C) \to (J CnExt K) (F) (y) = ⋃ (K fLimf (nei (J) (\{y\}) ↾_{𝑡} A)) (F)$
20	18 19	syldan	$⊢ (φ \land y \in A) \to (J CnExt K) (F) (y) = ⋃ (K fLimf (nei (J) (\{y\}) ↾_{𝑡} A)) (F)$
21	5	ffvelrnda	$⊢ (φ \land y \in A) \to F (y) \in B$
22		simpr	$⊢ (φ \land y \in A) \to y \in A$
23	1	restuni	$⊢ (J \in Top \land A \subseteq C) \to A = ⋃ (J ↾_{𝑡} A)$
24	3 6 23	syl2anc	$⊢ φ \to A = ⋃ (J ↾_{𝑡} A)$
25	24	adantr	$⊢ (φ \land y \in A) \to A = ⋃ (J ↾_{𝑡} A)$
26	22 25	eleqtrd	$⊢ (φ \land y \in A) \to y \in ⋃ (J ↾_{𝑡} A)$
27		fvex	$⊢ cls (J) (A) \in V$
28	7 27	eqeltrrdi	$⊢ φ \to C \in V$
29	28 6	ssexd	$⊢ φ \to A \in V$
30		resttop	$⊢ (J \in Top \land A \in V) \to J ↾_{𝑡} A \in Top$
31	3 29 30	syl2anc	$⊢ φ \to J ↾_{𝑡} A \in Top$
32		haustop	$⊢ K \in Haus \to K \in Top$
33	4 32	syl	$⊢ φ \to K \in Top$
34	24	feq2d	$⊢ φ \to (F : A ⟶ B \leftrightarrow F : ⋃ (J ↾_{𝑡} A) ⟶ B)$
35	5 34	mpbid	$⊢ φ \to F : ⋃ (J ↾_{𝑡} A) ⟶ B$
36		eqid	$⊢ ⋃ (J ↾_{𝑡} A) = ⋃ (J ↾_{𝑡} A)$
37	36 2	cnnei	$⊢ (J ↾_{𝑡} A \in Top \land K \in Top \land F : ⋃ (J ↾_{𝑡} A) ⟶ B) \to (F \in ((J ↾_{𝑡} A) Cn K) \leftrightarrow \forall y \in ⋃ (J ↾_{𝑡} A) \forall w \in nei (K) (\{F (y)\}) \exists v \in nei (J ↾_{𝑡} A) (\{y\}) F [v] \subseteq w)$
38	31 33 35 37	syl3anc	$⊢ φ \to (F \in ((J ↾_{𝑡} A) Cn K) \leftrightarrow \forall y \in ⋃ (J ↾_{𝑡} A) \forall w \in nei (K) (\{F (y)\}) \exists v \in nei (J ↾_{𝑡} A) (\{y\}) F [v] \subseteq w)$
39	10 38	mpbid	$⊢ φ \to \forall y \in ⋃ (J ↾_{𝑡} A) \forall w \in nei (K) (\{F (y)\}) \exists v \in nei (J ↾_{𝑡} A) (\{y\}) F [v] \subseteq w$
40	39	r19.21bi	$⊢ (φ \land y \in ⋃ (J ↾_{𝑡} A)) \to \forall w \in nei (K) (\{F (y)\}) \exists v \in nei (J ↾_{𝑡} A) (\{y\}) F [v] \subseteq w$
41	26 40	syldan	$⊢ (φ \land y \in A) \to \forall w \in nei (K) (\{F (y)\}) \exists v \in nei (J ↾_{𝑡} A) (\{y\}) F [v] \subseteq w$
42	41	r19.21bi	$⊢ ((φ \land y \in A) \land w \in nei (K) (\{F (y)\})) \to \exists v \in nei (J ↾_{𝑡} A) (\{y\}) F [v] \subseteq w$
43		snssi	$⊢ y \in A \to \{y\} \subseteq A$
44	1	neitr	$⊢ (J \in Top \land A \subseteq C \land \{y\} \subseteq A) \to nei (J ↾_{𝑡} A) (\{y\}) = nei (J) (\{y\}) ↾_{𝑡} A$
45	3 6 43 44	syl2an3an	$⊢ (φ \land y \in A) \to nei (J ↾_{𝑡} A) (\{y\}) = nei (J) (\{y\}) ↾_{𝑡} A$
46	45	rexeqdv	$⊢ (φ \land y \in A) \to (\exists v \in nei (J ↾_{𝑡} A) (\{y\}) F [v] \subseteq w \leftrightarrow \exists v \in (nei (J) (\{y\}) ↾_{𝑡} A) F [v] \subseteq w)$
47	46	adantr	$⊢ ((φ \land y \in A) \land w \in nei (K) (\{F (y)\})) \to (\exists v \in nei (J ↾_{𝑡} A) (\{y\}) F [v] \subseteq w \leftrightarrow \exists v \in (nei (J) (\{y\}) ↾_{𝑡} A) F [v] \subseteq w)$
48	42 47	mpbid	$⊢ ((φ \land y \in A) \land w \in nei (K) (\{F (y)\})) \to \exists v \in (nei (J) (\{y\}) ↾_{𝑡} A) F [v] \subseteq w$
49	48	ralrimiva	$⊢ (φ \land y \in A) \to \forall w \in nei (K) (\{F (y)\}) \exists v \in (nei (J) (\{y\}) ↾_{𝑡} A) F [v] \subseteq w$
50	4	adantr	$⊢ (φ \land y \in A) \to K \in Haus$
51	2	toptopon	$⊢ K \in Top \leftrightarrow K \in TopOn (B)$
52	51	biimpi	$⊢ K \in Top \to K \in TopOn (B)$
53	50 32 52	3syl	$⊢ (φ \land y \in A) \to K \in TopOn (B)$
54	7	adantr	$⊢ (φ \land y \in A) \to cls (J) (A) = C$
55	18 54	eleqtrrd	$⊢ (φ \land y \in A) \to y \in cls (J) (A)$
56	1	toptopon	$⊢ J \in Top \leftrightarrow J \in TopOn (C)$
57	3 56	sylib	$⊢ φ \to J \in TopOn (C)$
58	57	adantr	$⊢ (φ \land y \in A) \to J \in TopOn (C)$
59	6	adantr	$⊢ (φ \land y \in A) \to A \subseteq C$
60		trnei	$⊢ (J \in TopOn (C) \land A \subseteq C \land y \in C) \to (y \in cls (J) (A) \leftrightarrow nei (J) (\{y\}) ↾_{𝑡} A \in Fil (A))$
61	58 59 18 60	syl3anc	$⊢ (φ \land y \in A) \to (y \in cls (J) (A) \leftrightarrow nei (J) (\{y\}) ↾_{𝑡} A \in Fil (A))$
62	55 61	mpbid	$⊢ (φ \land y \in A) \to nei (J) (\{y\}) ↾_{𝑡} A \in Fil (A)$
63	5	adantr	$⊢ (φ \land y \in A) \to F : A ⟶ B$
64		flfnei	$⊢ (K \in TopOn (B) \land nei (J) (\{y\}) ↾_{𝑡} A \in Fil (A) \land F : A ⟶ B) \to (F (y) \in (K fLimf (nei (J) (\{y\}) ↾_{𝑡} A)) (F) \leftrightarrow (F (y) \in B \land \forall w \in nei (K) (\{F (y)\}) \exists v \in (nei (J) (\{y\}) ↾_{𝑡} A) F [v] \subseteq w))$
65	53 62 63 64	syl3anc	$⊢ (φ \land y \in A) \to (F (y) \in (K fLimf (nei (J) (\{y\}) ↾_{𝑡} A)) (F) \leftrightarrow (F (y) \in B \land \forall w \in nei (K) (\{F (y)\}) \exists v \in (nei (J) (\{y\}) ↾_{𝑡} A) F [v] \subseteq w))$
66	21 49 65	mpbir2and	$⊢ (φ \land y \in A) \to F (y) \in (K fLimf (nei (J) (\{y\}) ↾_{𝑡} A)) (F)$
67		eleq1w	$⊢ x = y \to (x \in C \leftrightarrow y \in C)$
68	67	anbi2d	$⊢ x = y \to ((φ \land x \in C) \leftrightarrow (φ \land y \in C))$
69		sneq	$⊢ x = y \to \{x\} = \{y\}$
70	69	fveq2d	$⊢ x = y \to nei (J) (\{x\}) = nei (J) (\{y\})$
71	70	oveq1d	$⊢ x = y \to nei (J) (\{x\}) ↾_{𝑡} A = nei (J) (\{y\}) ↾_{𝑡} A$
72	71	oveq2d	$⊢ x = y \to K fLimf (nei (J) (\{x\}) ↾_{𝑡} A) = K fLimf (nei (J) (\{y\}) ↾_{𝑡} A)$
73	72	fveq1d	$⊢ x = y \to (K fLimf (nei (J) (\{x\}) ↾_{𝑡} A)) (F) = (K fLimf (nei (J) (\{y\}) ↾_{𝑡} A)) (F)$
74	73	neeq1d	$⊢ x = y \to ((K fLimf (nei (J) (\{x\}) ↾_{𝑡} A)) (F) \neq \emptyset \leftrightarrow (K fLimf (nei (J) (\{y\}) ↾_{𝑡} A)) (F) \neq \emptyset)$
75	68 74	imbi12d	$⊢ x = y \to (((φ \land x \in C) \to (K fLimf (nei (J) (\{x\}) ↾_{𝑡} A)) (F) \neq \emptyset) \leftrightarrow ((φ \land y \in C) \to (K fLimf (nei (J) (\{y\}) ↾_{𝑡} A)) (F) \neq \emptyset))$
76	75 8	chvarvv	$⊢ (φ \land y \in C) \to (K fLimf (nei (J) (\{y\}) ↾_{𝑡} A)) (F) \neq \emptyset$
77	18 76	syldan	$⊢ (φ \land y \in A) \to (K fLimf (nei (J) (\{y\}) ↾_{𝑡} A)) (F) \neq \emptyset$
78	2	hausflf2	$⊢ ((K \in Haus \land nei (J) (\{y\}) ↾_{𝑡} A \in Fil (A) \land F : A ⟶ B) \land (K fLimf (nei (J) (\{y\}) ↾_{𝑡} A)) (F) \neq \emptyset) \to (K fLimf (nei (J) (\{y\}) ↾_{𝑡} A)) (F) \approx 1_{𝑜}$
79	50 62 63 77 78	syl31anc	$⊢ (φ \land y \in A) \to (K fLimf (nei (J) (\{y\}) ↾_{𝑡} A)) (F) \approx 1_{𝑜}$
80		en1eqsn	$⊢ (F (y) \in (K fLimf (nei (J) (\{y\}) ↾_{𝑡} A)) (F) \land (K fLimf (nei (J) (\{y\}) ↾_{𝑡} A)) (F) \approx 1_{𝑜}) \to (K fLimf (nei (J) (\{y\}) ↾_{𝑡} A)) (F) = \{F (y)\}$
81	66 79 80	syl2anc	$⊢ (φ \land y \in A) \to (K fLimf (nei (J) (\{y\}) ↾_{𝑡} A)) (F) = \{F (y)\}$
82	81	unieqd	$⊢ (φ \land y \in A) \to ⋃ (K fLimf (nei (J) (\{y\}) ↾_{𝑡} A)) (F) = ⋃ \{F (y)\}$
83		fvex	$⊢ F (y) \in V$
84	83	unisn	$⊢ ⋃ \{F (y)\} = F (y)$
85	82 84	eqtrdi	$⊢ (φ \land y \in A) \to ⋃ (K fLimf (nei (J) (\{y\}) ↾_{𝑡} A)) (F) = F (y)$
86	17 20 85	3eqtrd	$⊢ (φ \land y \in A) \to ({(J CnExt K) (F) ↾}_{A}) (y) = F (y)$
87	14 15 86	eqfnfvd	$⊢ φ \to {(J CnExt K) (F) ↾}_{A} = F$

Metamath Proof Explorer

Theorem cnextfres1

Proof