Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  limcres Structured version   Visualization version   GIF version

Theorem limcres 24530
 Description: If 𝐵 is an interior point of 𝐶 ∪ {𝐵} relative to the domain 𝐴, then a limit point of 𝐹 ↾ 𝐶 extends to a limit of 𝐹. (Contributed by Mario Carneiro, 27-Dec-2016.)
Hypotheses
Ref Expression
limcres.f (𝜑𝐹:𝐴⟶ℂ)
limcres.c (𝜑𝐶𝐴)
limcres.a (𝜑𝐴 ⊆ ℂ)
limcres.k 𝐾 = (TopOpen‘ℂfld)
limcres.j 𝐽 = (𝐾t (𝐴 ∪ {𝐵}))
limcres.i (𝜑𝐵 ∈ ((int‘𝐽)‘(𝐶 ∪ {𝐵})))
Assertion
Ref Expression
limcres (𝜑 → ((𝐹𝐶) lim 𝐵) = (𝐹 lim 𝐵))

Proof of Theorem limcres
Dummy variables 𝑧 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 limcrcl 24518 . . . . . 6 (𝑥 ∈ ((𝐹𝐶) lim 𝐵) → ((𝐹𝐶):dom (𝐹𝐶)⟶ℂ ∧ dom (𝐹𝐶) ⊆ ℂ ∧ 𝐵 ∈ ℂ))
21simp3d 1141 . . . . 5 (𝑥 ∈ ((𝐹𝐶) lim 𝐵) → 𝐵 ∈ ℂ)
3 limccl 24519 . . . . . 6 ((𝐹𝐶) lim 𝐵) ⊆ ℂ
43sseli 3913 . . . . 5 (𝑥 ∈ ((𝐹𝐶) lim 𝐵) → 𝑥 ∈ ℂ)
52, 4jca 515 . . . 4 (𝑥 ∈ ((𝐹𝐶) lim 𝐵) → (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ))
65a1i 11 . . 3 (𝜑 → (𝑥 ∈ ((𝐹𝐶) lim 𝐵) → (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)))
7 limcrcl 24518 . . . . . 6 (𝑥 ∈ (𝐹 lim 𝐵) → (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ ∧ 𝐵 ∈ ℂ))
87simp3d 1141 . . . . 5 (𝑥 ∈ (𝐹 lim 𝐵) → 𝐵 ∈ ℂ)
9 limccl 24519 . . . . . 6 (𝐹 lim 𝐵) ⊆ ℂ
109sseli 3913 . . . . 5 (𝑥 ∈ (𝐹 lim 𝐵) → 𝑥 ∈ ℂ)
118, 10jca 515 . . . 4 (𝑥 ∈ (𝐹 lim 𝐵) → (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ))
1211a1i 11 . . 3 (𝜑 → (𝑥 ∈ (𝐹 lim 𝐵) → (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)))
13 limcres.j . . . . . . . 8 𝐽 = (𝐾t (𝐴 ∪ {𝐵}))
14 limcres.k . . . . . . . . . 10 𝐾 = (TopOpen‘ℂfld)
1514cnfldtopon 23429 . . . . . . . . 9 𝐾 ∈ (TopOn‘ℂ)
16 limcres.a . . . . . . . . . . 11 (𝜑𝐴 ⊆ ℂ)
1716adantr 484 . . . . . . . . . 10 ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → 𝐴 ⊆ ℂ)
18 simprl 770 . . . . . . . . . . 11 ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → 𝐵 ∈ ℂ)
1918snssd 4705 . . . . . . . . . 10 ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → {𝐵} ⊆ ℂ)
2017, 19unssd 4116 . . . . . . . . 9 ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝐴 ∪ {𝐵}) ⊆ ℂ)
21 resttopon 21807 . . . . . . . . 9 ((𝐾 ∈ (TopOn‘ℂ) ∧ (𝐴 ∪ {𝐵}) ⊆ ℂ) → (𝐾t (𝐴 ∪ {𝐵})) ∈ (TopOn‘(𝐴 ∪ {𝐵})))
2215, 20, 21sylancr 590 . . . . . . . 8 ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝐾t (𝐴 ∪ {𝐵})) ∈ (TopOn‘(𝐴 ∪ {𝐵})))
2313, 22eqeltrid 2894 . . . . . . 7 ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → 𝐽 ∈ (TopOn‘(𝐴 ∪ {𝐵})))
24 topontop 21559 . . . . . . 7 (𝐽 ∈ (TopOn‘(𝐴 ∪ {𝐵})) → 𝐽 ∈ Top)
2523, 24syl 17 . . . . . 6 ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → 𝐽 ∈ Top)
26 limcres.c . . . . . . . . 9 (𝜑𝐶𝐴)
2726adantr 484 . . . . . . . 8 ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → 𝐶𝐴)
28 unss1 4109 . . . . . . . 8 (𝐶𝐴 → (𝐶 ∪ {𝐵}) ⊆ (𝐴 ∪ {𝐵}))
2927, 28syl 17 . . . . . . 7 ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝐶 ∪ {𝐵}) ⊆ (𝐴 ∪ {𝐵}))
30 toponuni 21560 . . . . . . . 8 (𝐽 ∈ (TopOn‘(𝐴 ∪ {𝐵})) → (𝐴 ∪ {𝐵}) = 𝐽)
3123, 30syl 17 . . . . . . 7 ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝐴 ∪ {𝐵}) = 𝐽)
3229, 31sseqtrd 3957 . . . . . 6 ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝐶 ∪ {𝐵}) ⊆ 𝐽)
33 limcres.i . . . . . . 7 (𝜑𝐵 ∈ ((int‘𝐽)‘(𝐶 ∪ {𝐵})))
3433adantr 484 . . . . . 6 ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → 𝐵 ∈ ((int‘𝐽)‘(𝐶 ∪ {𝐵})))
35 elun 4079 . . . . . . . . 9 (𝑧 ∈ (𝐴 ∪ {𝐵}) ↔ (𝑧𝐴𝑧 ∈ {𝐵}))
36 simplrr 777 . . . . . . . . . . 11 (((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) ∧ 𝑧𝐴) → 𝑥 ∈ ℂ)
37 limcres.f . . . . . . . . . . . . 13 (𝜑𝐹:𝐴⟶ℂ)
3837adantr 484 . . . . . . . . . . . 12 ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → 𝐹:𝐴⟶ℂ)
3938ffvelrnda 6838 . . . . . . . . . . 11 (((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) ∧ 𝑧𝐴) → (𝐹𝑧) ∈ ℂ)
4036, 39ifcld 4473 . . . . . . . . . 10 (((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) ∧ 𝑧𝐴) → if(𝑧 = 𝐵, 𝑥, (𝐹𝑧)) ∈ ℂ)
41 elsni 4545 . . . . . . . . . . . . 13 (𝑧 ∈ {𝐵} → 𝑧 = 𝐵)
4241adantl 485 . . . . . . . . . . . 12 (((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) ∧ 𝑧 ∈ {𝐵}) → 𝑧 = 𝐵)
4342iftrued 4436 . . . . . . . . . . 11 (((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) ∧ 𝑧 ∈ {𝐵}) → if(𝑧 = 𝐵, 𝑥, (𝐹𝑧)) = 𝑥)
44 simplrr 777 . . . . . . . . . . 11 (((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) ∧ 𝑧 ∈ {𝐵}) → 𝑥 ∈ ℂ)
4543, 44eqeltrd 2890 . . . . . . . . . 10 (((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) ∧ 𝑧 ∈ {𝐵}) → if(𝑧 = 𝐵, 𝑥, (𝐹𝑧)) ∈ ℂ)
4640, 45jaodan 955 . . . . . . . . 9 (((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) ∧ (𝑧𝐴𝑧 ∈ {𝐵})) → if(𝑧 = 𝐵, 𝑥, (𝐹𝑧)) ∈ ℂ)
4735, 46sylan2b 596 . . . . . . . 8 (((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) ∧ 𝑧 ∈ (𝐴 ∪ {𝐵})) → if(𝑧 = 𝐵, 𝑥, (𝐹𝑧)) ∈ ℂ)
4847fmpttd 6866 . . . . . . 7 ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑥, (𝐹𝑧))):(𝐴 ∪ {𝐵})⟶ℂ)
4931feq2d 6481 . . . . . . 7 ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑥, (𝐹𝑧))):(𝐴 ∪ {𝐵})⟶ℂ ↔ (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑥, (𝐹𝑧))): 𝐽⟶ℂ))
5048, 49mpbid 235 . . . . . 6 ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑥, (𝐹𝑧))): 𝐽⟶ℂ)
51 eqid 2798 . . . . . . 7 𝐽 = 𝐽
5215toponunii 21562 . . . . . . 7 ℂ = 𝐾
5351, 52cnprest 21935 . . . . . 6 (((𝐽 ∈ Top ∧ (𝐶 ∪ {𝐵}) ⊆ 𝐽) ∧ (𝐵 ∈ ((int‘𝐽)‘(𝐶 ∪ {𝐵})) ∧ (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑥, (𝐹𝑧))): 𝐽⟶ℂ)) → ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑥, (𝐹𝑧))) ∈ ((𝐽 CnP 𝐾)‘𝐵) ↔ ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑥, (𝐹𝑧))) ↾ (𝐶 ∪ {𝐵})) ∈ (((𝐽t (𝐶 ∪ {𝐵})) CnP 𝐾)‘𝐵)))
5425, 32, 34, 50, 53syl22anc 837 . . . . 5 ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑥, (𝐹𝑧))) ∈ ((𝐽 CnP 𝐾)‘𝐵) ↔ ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑥, (𝐹𝑧))) ↾ (𝐶 ∪ {𝐵})) ∈ (((𝐽t (𝐶 ∪ {𝐵})) CnP 𝐾)‘𝐵)))
55 eqid 2798 . . . . . 6 (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑥, (𝐹𝑧))) = (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑥, (𝐹𝑧)))
5613, 14, 55, 38, 17, 18ellimc 24517 . . . . 5 ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝑥 ∈ (𝐹 lim 𝐵) ↔ (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑥, (𝐹𝑧))) ∈ ((𝐽 CnP 𝐾)‘𝐵)))
57 eqid 2798 . . . . . . 7 (𝐾t (𝐶 ∪ {𝐵})) = (𝐾t (𝐶 ∪ {𝐵}))
58 eqid 2798 . . . . . . 7 (𝑧 ∈ (𝐶 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑥, ((𝐹𝐶)‘𝑧))) = (𝑧 ∈ (𝐶 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑥, ((𝐹𝐶)‘𝑧)))
5938, 27fssresd 6527 . . . . . . 7 ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝐹𝐶):𝐶⟶ℂ)
6027, 17sstrd 3927 . . . . . . 7 ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → 𝐶 ⊆ ℂ)
6157, 14, 58, 59, 60, 18ellimc 24517 . . . . . 6 ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝑥 ∈ ((𝐹𝐶) lim 𝐵) ↔ (𝑧 ∈ (𝐶 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑥, ((𝐹𝐶)‘𝑧))) ∈ (((𝐾t (𝐶 ∪ {𝐵})) CnP 𝐾)‘𝐵)))
62 elun 4079 . . . . . . . . . . 11 (𝑧 ∈ (𝐶 ∪ {𝐵}) ↔ (𝑧𝐶𝑧 ∈ {𝐵}))
63 velsn 4544 . . . . . . . . . . . 12 (𝑧 ∈ {𝐵} ↔ 𝑧 = 𝐵)
6463orbi2i 910 . . . . . . . . . . 11 ((𝑧𝐶𝑧 ∈ {𝐵}) ↔ (𝑧𝐶𝑧 = 𝐵))
6562, 64bitri 278 . . . . . . . . . 10 (𝑧 ∈ (𝐶 ∪ {𝐵}) ↔ (𝑧𝐶𝑧 = 𝐵))
66 pm5.61 998 . . . . . . . . . . . 12 (((𝑧𝐶𝑧 = 𝐵) ∧ ¬ 𝑧 = 𝐵) ↔ (𝑧𝐶 ∧ ¬ 𝑧 = 𝐵))
67 fvres 6674 . . . . . . . . . . . . 13 (𝑧𝐶 → ((𝐹𝐶)‘𝑧) = (𝐹𝑧))
6867adantr 484 . . . . . . . . . . . 12 ((𝑧𝐶 ∧ ¬ 𝑧 = 𝐵) → ((𝐹𝐶)‘𝑧) = (𝐹𝑧))
6966, 68sylbi 220 . . . . . . . . . . 11 (((𝑧𝐶𝑧 = 𝐵) ∧ ¬ 𝑧 = 𝐵) → ((𝐹𝐶)‘𝑧) = (𝐹𝑧))
7069ifeq2da 4459 . . . . . . . . . 10 ((𝑧𝐶𝑧 = 𝐵) → if(𝑧 = 𝐵, 𝑥, ((𝐹𝐶)‘𝑧)) = if(𝑧 = 𝐵, 𝑥, (𝐹𝑧)))
7165, 70sylbi 220 . . . . . . . . 9 (𝑧 ∈ (𝐶 ∪ {𝐵}) → if(𝑧 = 𝐵, 𝑥, ((𝐹𝐶)‘𝑧)) = if(𝑧 = 𝐵, 𝑥, (𝐹𝑧)))
7271mpteq2ia 5125 . . . . . . . 8 (𝑧 ∈ (𝐶 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑥, ((𝐹𝐶)‘𝑧))) = (𝑧 ∈ (𝐶 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑥, (𝐹𝑧)))
7329resmptd 5879 . . . . . . . 8 ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑥, (𝐹𝑧))) ↾ (𝐶 ∪ {𝐵})) = (𝑧 ∈ (𝐶 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑥, (𝐹𝑧))))
7472, 73eqtr4id 2852 . . . . . . 7 ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝑧 ∈ (𝐶 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑥, ((𝐹𝐶)‘𝑧))) = ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑥, (𝐹𝑧))) ↾ (𝐶 ∪ {𝐵})))
7513oveq1i 7155 . . . . . . . . . 10 (𝐽t (𝐶 ∪ {𝐵})) = ((𝐾t (𝐴 ∪ {𝐵})) ↾t (𝐶 ∪ {𝐵}))
76 cnex 10625 . . . . . . . . . . . . 13 ℂ ∈ V
7776ssex 5193 . . . . . . . . . . . 12 ((𝐴 ∪ {𝐵}) ⊆ ℂ → (𝐴 ∪ {𝐵}) ∈ V)
7820, 77syl 17 . . . . . . . . . . 11 ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝐴 ∪ {𝐵}) ∈ V)
79 restabs 21811 . . . . . . . . . . 11 ((𝐾 ∈ (TopOn‘ℂ) ∧ (𝐶 ∪ {𝐵}) ⊆ (𝐴 ∪ {𝐵}) ∧ (𝐴 ∪ {𝐵}) ∈ V) → ((𝐾t (𝐴 ∪ {𝐵})) ↾t (𝐶 ∪ {𝐵})) = (𝐾t (𝐶 ∪ {𝐵})))
8015, 29, 78, 79mp3an2i 1463 . . . . . . . . . 10 ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → ((𝐾t (𝐴 ∪ {𝐵})) ↾t (𝐶 ∪ {𝐵})) = (𝐾t (𝐶 ∪ {𝐵})))
8175, 80syl5req 2846 . . . . . . . . 9 ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝐾t (𝐶 ∪ {𝐵})) = (𝐽t (𝐶 ∪ {𝐵})))
8281oveq1d 7160 . . . . . . . 8 ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → ((𝐾t (𝐶 ∪ {𝐵})) CnP 𝐾) = ((𝐽t (𝐶 ∪ {𝐵})) CnP 𝐾))
8382fveq1d 6657 . . . . . . 7 ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (((𝐾t (𝐶 ∪ {𝐵})) CnP 𝐾)‘𝐵) = (((𝐽t (𝐶 ∪ {𝐵})) CnP 𝐾)‘𝐵))
8474, 83eleq12d 2884 . . . . . 6 ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → ((𝑧 ∈ (𝐶 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑥, ((𝐹𝐶)‘𝑧))) ∈ (((𝐾t (𝐶 ∪ {𝐵})) CnP 𝐾)‘𝐵) ↔ ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑥, (𝐹𝑧))) ↾ (𝐶 ∪ {𝐵})) ∈ (((𝐽t (𝐶 ∪ {𝐵})) CnP 𝐾)‘𝐵)))
8561, 84bitrd 282 . . . . 5 ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝑥 ∈ ((𝐹𝐶) lim 𝐵) ↔ ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑥, (𝐹𝑧))) ↾ (𝐶 ∪ {𝐵})) ∈ (((𝐽t (𝐶 ∪ {𝐵})) CnP 𝐾)‘𝐵)))
8654, 56, 853bitr4rd 315 . . . 4 ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝑥 ∈ ((𝐹𝐶) lim 𝐵) ↔ 𝑥 ∈ (𝐹 lim 𝐵)))
8786ex 416 . . 3 (𝜑 → ((𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝑥 ∈ ((𝐹𝐶) lim 𝐵) ↔ 𝑥 ∈ (𝐹 lim 𝐵))))
886, 12, 87pm5.21ndd 384 . 2 (𝜑 → (𝑥 ∈ ((𝐹𝐶) lim 𝐵) ↔ 𝑥 ∈ (𝐹 lim 𝐵)))
8988eqrdv 2796 1 (𝜑 → ((𝐹𝐶) lim 𝐵) = (𝐹 lim 𝐵))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∨ wo 844   = wceq 1538   ∈ wcel 2111  Vcvv 3442   ∪ cun 3881   ⊆ wss 3883  ifcif 4428  {csn 4528  ∪ cuni 4804   ↦ cmpt 5114  dom cdm 5523   ↾ cres 5525  ⟶wf 6328  ‘cfv 6332  (class class class)co 7145  ℂcc 10542   ↾t crest 16706  TopOpenctopn 16707  ℂfldccnfld 20112  Topctop 21539  TopOnctopon 21556  intcnt 21663   CnP ccnp 21871   limℂ climc 24506 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5158  ax-sep 5171  ax-nul 5178  ax-pow 5235  ax-pr 5299  ax-un 7454  ax-cnex 10600  ax-resscn 10601  ax-1cn 10602  ax-icn 10603  ax-addcl 10604  ax-addrcl 10605  ax-mulcl 10606  ax-mulrcl 10607  ax-mulcom 10608  ax-addass 10609  ax-mulass 10610  ax-distr 10611  ax-i2m1 10612  ax-1ne0 10613  ax-1rid 10614  ax-rnegex 10615  ax-rrecex 10616  ax-cnre 10617  ax-pre-lttri 10618  ax-pre-lttrn 10619  ax-pre-ltadd 10620  ax-pre-mulgt0 10621  ax-pre-sup 10622 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3444  df-sbc 3723  df-csb 3831  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-tp 4533  df-op 4535  df-uni 4805  df-int 4843  df-iun 4887  df-br 5035  df-opab 5097  df-mpt 5115  df-tr 5141  df-id 5429  df-eprel 5434  df-po 5442  df-so 5443  df-fr 5482  df-we 5484  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-pred 6123  df-ord 6169  df-on 6170  df-lim 6171  df-suc 6172  df-iota 6291  df-fun 6334  df-fn 6335  df-f 6336  df-f1 6337  df-fo 6338  df-f1o 6339  df-fv 6340  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-om 7574  df-1st 7684  df-2nd 7685  df-wrecs 7948  df-recs 8009  df-rdg 8047  df-1o 8103  df-oadd 8107  df-er 8290  df-map 8409  df-pm 8410  df-en 8511  df-dom 8512  df-sdom 8513  df-fin 8514  df-fi 8877  df-sup 8908  df-inf 8909  df-pnf 10684  df-mnf 10685  df-xr 10686  df-ltxr 10687  df-le 10688  df-sub 10879  df-neg 10880  df-div 11305  df-nn 11644  df-2 11706  df-3 11707  df-4 11708  df-5 11709  df-6 11710  df-7 11711  df-8 11712  df-9 11713  df-n0 11904  df-z 11990  df-dec 12107  df-uz 12252  df-q 12357  df-rp 12398  df-xneg 12515  df-xadd 12516  df-xmul 12517  df-fz 12906  df-seq 13385  df-exp 13446  df-cj 14470  df-re 14471  df-im 14472  df-sqrt 14606  df-abs 14607  df-struct 16497  df-ndx 16498  df-slot 16499  df-base 16501  df-plusg 16590  df-mulr 16591  df-starv 16592  df-tset 16596  df-ple 16597  df-ds 16599  df-unif 16600  df-rest 16708  df-topn 16709  df-topgen 16729  df-psmet 20104  df-xmet 20105  df-met 20106  df-bl 20107  df-mopn 20108  df-cnfld 20113  df-top 21540  df-topon 21557  df-topsp 21579  df-bases 21592  df-ntr 21666  df-cnp 21874  df-xms 22968  df-ms 22969  df-limc 24510 This theorem is referenced by:  dvreslem  24553  dvaddbr  24582  dvmulbr  24583  lhop2  24659  lhop  24660  limciccioolb  42431  limcicciooub  42447  limcresiooub  42452  limcresioolb  42453  ioccncflimc  42695  icocncflimc  42699  dirkercncflem3  42915  fourierdlem32  42949  fourierdlem33  42950  fourierdlem48  42964  fourierdlem49  42965  fourierdlem62  42978  fouriersw  43041
 Copyright terms: Public domain W3C validator