cnextfres

Description: F and its extension by continuity agree on the domain of F . (Contributed by Thierry Arnoux, 29-Aug-2020)

	Ref	Expression
Hypotheses	cnextfres.c	$⊢ C = ⋃ J$
	cnextfres.b	$⊢ B = ⋃ K$
	cnextfres.j	$⊢ φ \to J \in Top$
	cnextfres.k	$⊢ φ \to K \in Haus$
	cnextfres.a	$⊢ φ \to A \subseteq C$
	cnextfres.1	$⊢ φ \to F \in ((J ↾_{𝑡} A) Cn K)$
	cnextfres.x	$⊢ φ \to X \in A$
Assertion	cnextfres	$⊢ φ \to (J CnExt K) (F) (X) = F (X)$

Proof

Step	Hyp	Ref	Expression
1		cnextfres.c	$⊢ C = ⋃ J$
2		cnextfres.b	$⊢ B = ⋃ K$
3		cnextfres.j	$⊢ φ \to J \in Top$
4		cnextfres.k	$⊢ φ \to K \in Haus$
5		cnextfres.a	$⊢ φ \to A \subseteq C$
6		cnextfres.1	$⊢ φ \to F \in ((J ↾_{𝑡} A) Cn K)$
7		cnextfres.x	$⊢ φ \to X \in A$
8		eqid	$⊢ ⋃ (J ↾_{𝑡} A) = ⋃ (J ↾_{𝑡} A)$
9	8 2	cnf	$⊢ F \in ((J ↾_{𝑡} A) Cn K) \to F : ⋃ (J ↾_{𝑡} A) ⟶ B$
10	6 9	syl	$⊢ φ \to F : ⋃ (J ↾_{𝑡} A) ⟶ B$
11	1	restuni	$⊢ (J \in Top \land A \subseteq C) \to A = ⋃ (J ↾_{𝑡} A)$
12	3 5 11	syl2anc	$⊢ φ \to A = ⋃ (J ↾_{𝑡} A)$
13	12	feq2d	$⊢ φ \to (F : A ⟶ B \leftrightarrow F : ⋃ (J ↾_{𝑡} A) ⟶ B)$
14	10 13	mpbird	$⊢ φ \to F : A ⟶ B$
15	1 2	cnextfun	$⊢ ((J \in Top \land K \in Haus) \land (F : A ⟶ B \land A \subseteq C)) \to Fun (J CnExt K) (F)$
16	3 4 14 5 15	syl22anc	$⊢ φ \to Fun (J CnExt K) (F)$
17	1	sscls	$⊢ (J \in Top \land A \subseteq C) \to A \subseteq cls (J) (A)$
18	3 5 17	syl2anc	$⊢ φ \to A \subseteq cls (J) (A)$
19	18 7	sseldd	$⊢ φ \to X \in cls (J) (A)$
20	1 2 3 5 6 7	flfcntr	$⊢ φ \to F (X) \in (K fLimf (nei (J) (\{X\}) ↾_{𝑡} A)) (F)$
21		sneq	$⊢ x = X \to \{x\} = \{X\}$
22	21	fveq2d	$⊢ x = X \to nei (J) (\{x\}) = nei (J) (\{X\})$
23	22	oveq1d	$⊢ x = X \to nei (J) (\{x\}) ↾_{𝑡} A = nei (J) (\{X\}) ↾_{𝑡} A$
24	23	oveq2d	$⊢ x = X \to K fLimf (nei (J) (\{x\}) ↾_{𝑡} A) = K fLimf (nei (J) (\{X\}) ↾_{𝑡} A)$
25	24	fveq1d	$⊢ x = X \to (K fLimf (nei (J) (\{x\}) ↾_{𝑡} A)) (F) = (K fLimf (nei (J) (\{X\}) ↾_{𝑡} A)) (F)$
26	25	opeliunxp2	$⊢ ⟨X, F (X)⟩ \in ⋃_{x \in cls (J) (A)} (\{x\} \times (K fLimf (nei (J) (\{x\}) ↾_{𝑡} A)) (F)) \leftrightarrow (X \in cls (J) (A) \land F (X) \in (K fLimf (nei (J) (\{X\}) ↾_{𝑡} A)) (F))$
27	19 20 26	sylanbrc	$⊢ φ \to ⟨X, F (X)⟩ \in ⋃_{x \in cls (J) (A)} (\{x\} \times (K fLimf (nei (J) (\{x\}) ↾_{𝑡} A)) (F))$
28		haustop	$⊢ K \in Haus \to K \in Top$
29	4 28	syl	$⊢ φ \to K \in Top$
30	1 2	cnextfval	$⊢ ((J \in Top \land K \in Top) \land (F : A ⟶ B \land A \subseteq C)) \to (J CnExt K) (F) = ⋃_{x \in cls (J) (A)} (\{x\} \times (K fLimf (nei (J) (\{x\}) ↾_{𝑡} A)) (F))$
31	3 29 14 5 30	syl22anc	$⊢ φ \to (J CnExt K) (F) = ⋃_{x \in cls (J) (A)} (\{x\} \times (K fLimf (nei (J) (\{x\}) ↾_{𝑡} A)) (F))$
32	27 31	eleqtrrd	$⊢ φ \to ⟨X, F (X)⟩ \in (J CnExt K) (F)$
33		df-br	$⊢ X (J CnExt K) (F) F (X) \leftrightarrow ⟨X, F (X)⟩ \in (J CnExt K) (F)$
34	32 33	sylibr	$⊢ φ \to X (J CnExt K) (F) F (X)$
35		funbrfv	$⊢ Fun (J CnExt K) (F) \to (X (J CnExt K) (F) F (X) \to (J CnExt K) (F) (X) = F (X))$
36	16 34 35	sylc	$⊢ φ \to (J CnExt K) (F) (X) = F (X)$

Metamath Proof Explorer

Theorem cnextfres

Proof