Metamath Proof Explorer


Theorem dvreslem

Description: Lemma for dvres . (Contributed by Mario Carneiro, 8-Aug-2014) (Revised by Mario Carneiro, 28-Dec-2016) Commute the consequent and shorten proof. (Revised by Peter Mazsa, 2-Oct-2022)

Ref Expression
Hypotheses dvres.k K = TopOpen fld
dvres.t T = K 𝑡 S
dvres.g G = z A x F z F x z x
dvres.s φ S
dvres.f φ F : A
dvres.a φ A S
dvres.b φ B S
dvres.y φ y
Assertion dvreslem φ x F B S y x int T B x F S y

Proof

Step Hyp Ref Expression
1 dvres.k K = TopOpen fld
2 dvres.t T = K 𝑡 S
3 dvres.g G = z A x F z F x z x
4 dvres.s φ S
5 dvres.f φ F : A
6 dvres.a φ A S
7 dvres.b φ B S
8 dvres.y φ y
9 difss A B x A B
10 inss2 A B B
11 9 10 sstri A B x B
12 simpr φ x int T A B z A B x z A B x
13 11 12 sseldi φ x int T A B z A B x z B
14 13 fvresd φ x int T A B z A B x F B z = F z
15 1 cnfldtop K Top
16 cnex V
17 ssexg S V S V
18 4 16 17 sylancl φ S V
19 resttop K Top S V K 𝑡 S Top
20 15 18 19 sylancr φ K 𝑡 S Top
21 2 20 eqeltrid φ T Top
22 inss1 A B A
23 22 6 sstrid φ A B S
24 1 cnfldtopon K TopOn
25 resttopon K TopOn S K 𝑡 S TopOn S
26 24 4 25 sylancr φ K 𝑡 S TopOn S
27 2 26 eqeltrid φ T TopOn S
28 toponuni T TopOn S S = T
29 27 28 syl φ S = T
30 23 29 sseqtrd φ A B T
31 eqid T = T
32 31 ntrss2 T Top A B T int T A B A B
33 21 30 32 syl2anc φ int T A B A B
34 33 10 sstrdi φ int T A B B
35 34 sselda φ x int T A B x B
36 35 fvresd φ x int T A B F B x = F x
37 36 adantr φ x int T A B z A B x F B x = F x
38 14 37 oveq12d φ x int T A B z A B x F B z F B x = F z F x
39 38 oveq1d φ x int T A B z A B x F B z F B x z x = F z F x z x
40 39 mpteq2dva φ x int T A B z A B x F B z F B x z x = z A B x F z F x z x
41 3 reseq1i G A B x = z A x F z F x z x A B x
42 ssdif A B A A B x A x
43 resmpt A B x A x z A x F z F x z x A B x = z A B x F z F x z x
44 22 42 43 mp2b z A x F z F x z x A B x = z A B x F z F x z x
45 41 44 eqtri G A B x = z A B x F z F x z x
46 40 45 syl6eqr φ x int T A B z A B x F B z F B x z x = G A B x
47 46 oveq1d φ x int T A B z A B x F B z F B x z x lim x = G A B x lim x
48 5 adantr φ x int T A B F : A
49 6 4 sstrd φ A
50 49 adantr φ x int T A B A
51 33 22 sstrdi φ int T A B A
52 51 sselda φ x int T A B x A
53 48 50 52 dvlem φ x int T A B z A x F z F x z x
54 53 3 fmptd φ x int T A B G : A x
55 22 42 mp1i φ x int T A B A B x A x
56 difss A x A
57 56 50 sstrid φ x int T A B A x
58 eqid K 𝑡 A x x = K 𝑡 A x x
59 difssd φ T A T
60 30 59 unssd φ A B T A T
61 ssun1 A B A B T A
62 61 a1i φ A B A B T A
63 31 ntrss T Top A B T A T A B A B T A int T A B int T A B T A
64 21 60 62 63 syl3anc φ int T A B int T A B T A
65 64 51 ssind φ int T A B int T A B T A A
66 6 29 sseqtrd φ A T
67 22 a1i φ A B A
68 eqid T 𝑡 A = T 𝑡 A
69 31 68 restntr T Top A T A B A int T 𝑡 A A B = int T A B T A A
70 21 66 67 69 syl3anc φ int T 𝑡 A A B = int T A B T A A
71 2 oveq1i T 𝑡 A = K 𝑡 S 𝑡 A
72 15 a1i φ K Top
73 restabs K Top A S S V K 𝑡 S 𝑡 A = K 𝑡 A
74 72 6 18 73 syl3anc φ K 𝑡 S 𝑡 A = K 𝑡 A
75 71 74 syl5eq φ T 𝑡 A = K 𝑡 A
76 75 fveq2d φ int T 𝑡 A = int K 𝑡 A
77 76 fveq1d φ int T 𝑡 A A B = int K 𝑡 A A B
78 70 77 eqtr3d φ int T A B T A A = int K 𝑡 A A B
79 65 78 sseqtrd φ int T A B int K 𝑡 A A B
80 79 sselda φ x int T A B x int K 𝑡 A A B
81 undif1 A x x = A x
82 33 sselda φ x int T A B x A B
83 82 snssd φ x int T A B x A B
84 83 22 sstrdi φ x int T A B x A
85 ssequn2 x A A x = A
86 84 85 sylib φ x int T A B A x = A
87 81 86 syl5eq φ x int T A B A x x = A
88 87 oveq2d φ x int T A B K 𝑡 A x x = K 𝑡 A
89 88 fveq2d φ x int T A B int K 𝑡 A x x = int K 𝑡 A
90 undif1 A B x x = A B x
91 ssequn2 x A B A B x = A B
92 83 91 sylib φ x int T A B A B x = A B
93 90 92 syl5eq φ x int T A B A B x x = A B
94 89 93 fveq12d φ x int T A B int K 𝑡 A x x A B x x = int K 𝑡 A A B
95 80 94 eleqtrrd φ x int T A B x int K 𝑡 A x x A B x x
96 54 55 57 1 58 95 limcres φ x int T A B G A B x lim x = G lim x
97 47 96 eqtrd φ x int T A B z A B x F B z F B x z x lim x = G lim x
98 97 eleq2d φ x int T A B y z A B x F B z F B x z x lim x y G lim x
99 98 pm5.32da φ x int T A B y z A B x F B z F B x z x lim x x int T A B y G lim x
100 7 29 sseqtrd φ B T
101 31 ntrin T Top A T B T int T A B = int T A int T B
102 21 66 100 101 syl3anc φ int T A B = int T A int T B
103 102 eleq2d φ x int T A B x int T A int T B
104 elin x int T A int T B x int T A x int T B
105 103 104 syl6bb φ x int T A B x int T A x int T B
106 105 anbi1d φ x int T A B y G lim x x int T A x int T B y G lim x
107 99 106 bitrd φ x int T A B y z A B x F B z F B x z x lim x x int T A x int T B y G lim x
108 an32 x int T A x int T B y G lim x x int T A y G lim x x int T B
109 107 108 syl6bb φ x int T A B y z A B x F B z F B x z x lim x x int T A y G lim x x int T B
110 eqid z A B x F B z F B x z x = z A B x F B z F B x z x
111 fresin F : A F B : A B
112 5 111 syl φ F B : A B
113 2 1 110 4 112 23 eldv φ x F B S y x int T A B y z A B x F B z F B x z x lim x
114 2 1 3 4 5 6 eldv φ x F S y x int T A y G lim x
115 114 anbi1cd φ x int T B x F S y x int T A y G lim x x int T B
116 109 113 115 3bitr4d φ x F B S y x int T B x F S y