Metamath Proof Explorer


Theorem 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 φ J Top
cnextf.4 φ K Haus
cnextf.5 φ F : A B
cnextf.a φ A C
cnextf.6 φ cls J A = C
cnextf.7 φ x C K fLimf nei J x 𝑡 A F
cnextcn.8 φ K Reg
cnextfres1.1 φ F J 𝑡 A Cn K
Assertion cnextfres1 φ J CnExt K F A = F

Proof

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