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

Theorem limcres 25121
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 25109 . . . . . 6 (𝑥 ∈ ((𝐹𝐶) lim 𝐵) → ((𝐹𝐶):dom (𝐹𝐶)⟶ℂ ∧ dom (𝐹𝐶) ⊆ ℂ ∧ 𝐵 ∈ ℂ))
21simp3d 1143 . . . . 5 (𝑥 ∈ ((𝐹𝐶) lim 𝐵) → 𝐵 ∈ ℂ)
3 limccl 25110 . . . . . 6 ((𝐹𝐶) lim 𝐵) ⊆ ℂ
43sseli 3926 . . . . 5 (𝑥 ∈ ((𝐹𝐶) lim 𝐵) → 𝑥 ∈ ℂ)
52, 4jca 512 . . . 4 (𝑥 ∈ ((𝐹𝐶) lim 𝐵) → (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ))
65a1i 11 . . 3 (𝜑 → (𝑥 ∈ ((𝐹𝐶) lim 𝐵) → (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)))
7 limcrcl 25109 . . . . . 6 (𝑥 ∈ (𝐹 lim 𝐵) → (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ ∧ 𝐵 ∈ ℂ))
87simp3d 1143 . . . . 5 (𝑥 ∈ (𝐹 lim 𝐵) → 𝐵 ∈ ℂ)
9 limccl 25110 . . . . . 6 (𝐹 lim 𝐵) ⊆ ℂ
109sseli 3926 . . . . 5 (𝑥 ∈ (𝐹 lim 𝐵) → 𝑥 ∈ ℂ)
118, 10jca 512 . . . 4 (𝑥 ∈ (𝐹 lim 𝐵) → (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ))
1211a1i 11 . . 3 (𝜑 → (𝑥 ∈ (𝐹 lim 𝐵) → (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)))
13 limcres.j . . . . . . . 8 𝐽 = (𝐾t (𝐴 ∪ {𝐵}))
14 limcres.k . . . . . . . . . 10 𝐾 = (TopOpen‘ℂfld)
1514cnfldtopon 24017 . . . . . . . . 9 𝐾 ∈ (TopOn‘ℂ)
16 limcres.a . . . . . . . . . . 11 (𝜑𝐴 ⊆ ℂ)
1716adantr 481 . . . . . . . . . 10 ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → 𝐴 ⊆ ℂ)
18 simprl 768 . . . . . . . . . . 11 ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → 𝐵 ∈ ℂ)
1918snssd 4752 . . . . . . . . . 10 ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → {𝐵} ⊆ ℂ)
2017, 19unssd 4130 . . . . . . . . 9 ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝐴 ∪ {𝐵}) ⊆ ℂ)
21 resttopon 22383 . . . . . . . . 9 ((𝐾 ∈ (TopOn‘ℂ) ∧ (𝐴 ∪ {𝐵}) ⊆ ℂ) → (𝐾t (𝐴 ∪ {𝐵})) ∈ (TopOn‘(𝐴 ∪ {𝐵})))
2215, 20, 21sylancr 587 . . . . . . . 8 ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝐾t (𝐴 ∪ {𝐵})) ∈ (TopOn‘(𝐴 ∪ {𝐵})))
2313, 22eqeltrid 2842 . . . . . . 7 ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → 𝐽 ∈ (TopOn‘(𝐴 ∪ {𝐵})))
24 topontop 22133 . . . . . . 7 (𝐽 ∈ (TopOn‘(𝐴 ∪ {𝐵})) → 𝐽 ∈ Top)
2523, 24syl 17 . . . . . 6 ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → 𝐽 ∈ Top)
26 limcres.c . . . . . . . . 9 (𝜑𝐶𝐴)
2726adantr 481 . . . . . . . 8 ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → 𝐶𝐴)
28 unss1 4123 . . . . . . . 8 (𝐶𝐴 → (𝐶 ∪ {𝐵}) ⊆ (𝐴 ∪ {𝐵}))
2927, 28syl 17 . . . . . . 7 ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝐶 ∪ {𝐵}) ⊆ (𝐴 ∪ {𝐵}))
30 toponuni 22134 . . . . . . . 8 (𝐽 ∈ (TopOn‘(𝐴 ∪ {𝐵})) → (𝐴 ∪ {𝐵}) = 𝐽)
3123, 30syl 17 . . . . . . 7 ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝐴 ∪ {𝐵}) = 𝐽)
3229, 31sseqtrd 3970 . . . . . 6 ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝐶 ∪ {𝐵}) ⊆ 𝐽)
33 limcres.i . . . . . . 7 (𝜑𝐵 ∈ ((int‘𝐽)‘(𝐶 ∪ {𝐵})))
3433adantr 481 . . . . . 6 ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → 𝐵 ∈ ((int‘𝐽)‘(𝐶 ∪ {𝐵})))
35 elun 4093 . . . . . . . . 9 (𝑧 ∈ (𝐴 ∪ {𝐵}) ↔ (𝑧𝐴𝑧 ∈ {𝐵}))
36 simplrr 775 . . . . . . . . . . 11 (((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) ∧ 𝑧𝐴) → 𝑥 ∈ ℂ)
37 limcres.f . . . . . . . . . . . . 13 (𝜑𝐹:𝐴⟶ℂ)
3837adantr 481 . . . . . . . . . . . 12 ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → 𝐹:𝐴⟶ℂ)
3938ffvelcdmda 6998 . . . . . . . . . . 11 (((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) ∧ 𝑧𝐴) → (𝐹𝑧) ∈ ℂ)
4036, 39ifcld 4515 . . . . . . . . . 10 (((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) ∧ 𝑧𝐴) → if(𝑧 = 𝐵, 𝑥, (𝐹𝑧)) ∈ ℂ)
41 elsni 4586 . . . . . . . . . . . . 13 (𝑧 ∈ {𝐵} → 𝑧 = 𝐵)
4241adantl 482 . . . . . . . . . . . 12 (((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) ∧ 𝑧 ∈ {𝐵}) → 𝑧 = 𝐵)
4342iftrued 4477 . . . . . . . . . . 11 (((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) ∧ 𝑧 ∈ {𝐵}) → if(𝑧 = 𝐵, 𝑥, (𝐹𝑧)) = 𝑥)
44 simplrr 775 . . . . . . . . . . 11 (((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) ∧ 𝑧 ∈ {𝐵}) → 𝑥 ∈ ℂ)
4543, 44eqeltrd 2838 . . . . . . . . . 10 (((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) ∧ 𝑧 ∈ {𝐵}) → if(𝑧 = 𝐵, 𝑥, (𝐹𝑧)) ∈ ℂ)
4640, 45jaodan 955 . . . . . . . . 9 (((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) ∧ (𝑧𝐴𝑧 ∈ {𝐵})) → if(𝑧 = 𝐵, 𝑥, (𝐹𝑧)) ∈ ℂ)
4735, 46sylan2b 594 . . . . . . . 8 (((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) ∧ 𝑧 ∈ (𝐴 ∪ {𝐵})) → if(𝑧 = 𝐵, 𝑥, (𝐹𝑧)) ∈ ℂ)
4847fmpttd 7026 . . . . . . 7 ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑥, (𝐹𝑧))):(𝐴 ∪ {𝐵})⟶ℂ)
4931feq2d 6621 . . . . . . 7 ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑥, (𝐹𝑧))):(𝐴 ∪ {𝐵})⟶ℂ ↔ (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑥, (𝐹𝑧))): 𝐽⟶ℂ))
5048, 49mpbid 231 . . . . . 6 ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑥, (𝐹𝑧))): 𝐽⟶ℂ)
51 eqid 2737 . . . . . . 7 𝐽 = 𝐽
5215toponunii 22136 . . . . . . 7 ℂ = 𝐾
5351, 52cnprest 22511 . . . . . 6 (((𝐽 ∈ Top ∧ (𝐶 ∪ {𝐵}) ⊆ 𝐽) ∧ (𝐵 ∈ ((int‘𝐽)‘(𝐶 ∪ {𝐵})) ∧ (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑥, (𝐹𝑧))): 𝐽⟶ℂ)) → ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑥, (𝐹𝑧))) ∈ ((𝐽 CnP 𝐾)‘𝐵) ↔ ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑥, (𝐹𝑧))) ↾ (𝐶 ∪ {𝐵})) ∈ (((𝐽t (𝐶 ∪ {𝐵})) CnP 𝐾)‘𝐵)))
5425, 32, 34, 50, 53syl22anc 836 . . . . 5 ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑥, (𝐹𝑧))) ∈ ((𝐽 CnP 𝐾)‘𝐵) ↔ ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑥, (𝐹𝑧))) ↾ (𝐶 ∪ {𝐵})) ∈ (((𝐽t (𝐶 ∪ {𝐵})) CnP 𝐾)‘𝐵)))
55 eqid 2737 . . . . . 6 (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑥, (𝐹𝑧))) = (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑥, (𝐹𝑧)))
5613, 14, 55, 38, 17, 18ellimc 25108 . . . . 5 ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝑥 ∈ (𝐹 lim 𝐵) ↔ (𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑥, (𝐹𝑧))) ∈ ((𝐽 CnP 𝐾)‘𝐵)))
57 eqid 2737 . . . . . . 7 (𝐾t (𝐶 ∪ {𝐵})) = (𝐾t (𝐶 ∪ {𝐵}))
58 eqid 2737 . . . . . . 7 (𝑧 ∈ (𝐶 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑥, ((𝐹𝐶)‘𝑧))) = (𝑧 ∈ (𝐶 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑥, ((𝐹𝐶)‘𝑧)))
5938, 27fssresd 6676 . . . . . . 7 ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝐹𝐶):𝐶⟶ℂ)
6027, 17sstrd 3940 . . . . . . 7 ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → 𝐶 ⊆ ℂ)
6157, 14, 58, 59, 60, 18ellimc 25108 . . . . . 6 ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝑥 ∈ ((𝐹𝐶) lim 𝐵) ↔ (𝑧 ∈ (𝐶 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑥, ((𝐹𝐶)‘𝑧))) ∈ (((𝐾t (𝐶 ∪ {𝐵})) CnP 𝐾)‘𝐵)))
62 elun 4093 . . . . . . . . . . 11 (𝑧 ∈ (𝐶 ∪ {𝐵}) ↔ (𝑧𝐶𝑧 ∈ {𝐵}))
63 velsn 4585 . . . . . . . . . . . 12 (𝑧 ∈ {𝐵} ↔ 𝑧 = 𝐵)
6463orbi2i 910 . . . . . . . . . . 11 ((𝑧𝐶𝑧 ∈ {𝐵}) ↔ (𝑧𝐶𝑧 = 𝐵))
6562, 64bitri 274 . . . . . . . . . 10 (𝑧 ∈ (𝐶 ∪ {𝐵}) ↔ (𝑧𝐶𝑧 = 𝐵))
66 pm5.61 998 . . . . . . . . . . . 12 (((𝑧𝐶𝑧 = 𝐵) ∧ ¬ 𝑧 = 𝐵) ↔ (𝑧𝐶 ∧ ¬ 𝑧 = 𝐵))
67 fvres 6828 . . . . . . . . . . . . 13 (𝑧𝐶 → ((𝐹𝐶)‘𝑧) = (𝐹𝑧))
6867adantr 481 . . . . . . . . . . . 12 ((𝑧𝐶 ∧ ¬ 𝑧 = 𝐵) → ((𝐹𝐶)‘𝑧) = (𝐹𝑧))
6966, 68sylbi 216 . . . . . . . . . . 11 (((𝑧𝐶𝑧 = 𝐵) ∧ ¬ 𝑧 = 𝐵) → ((𝐹𝐶)‘𝑧) = (𝐹𝑧))
7069ifeq2da 4501 . . . . . . . . . 10 ((𝑧𝐶𝑧 = 𝐵) → if(𝑧 = 𝐵, 𝑥, ((𝐹𝐶)‘𝑧)) = if(𝑧 = 𝐵, 𝑥, (𝐹𝑧)))
7165, 70sylbi 216 . . . . . . . . 9 (𝑧 ∈ (𝐶 ∪ {𝐵}) → if(𝑧 = 𝐵, 𝑥, ((𝐹𝐶)‘𝑧)) = if(𝑧 = 𝐵, 𝑥, (𝐹𝑧)))
7271mpteq2ia 5188 . . . . . . . 8 (𝑧 ∈ (𝐶 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑥, ((𝐹𝐶)‘𝑧))) = (𝑧 ∈ (𝐶 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑥, (𝐹𝑧)))
7329resmptd 5965 . . . . . . . 8 ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑥, (𝐹𝑧))) ↾ (𝐶 ∪ {𝐵})) = (𝑧 ∈ (𝐶 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑥, (𝐹𝑧))))
7472, 73eqtr4id 2796 . . . . . . 7 ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝑧 ∈ (𝐶 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑥, ((𝐹𝐶)‘𝑧))) = ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑥, (𝐹𝑧))) ↾ (𝐶 ∪ {𝐵})))
7513oveq1i 7323 . . . . . . . . . 10 (𝐽t (𝐶 ∪ {𝐵})) = ((𝐾t (𝐴 ∪ {𝐵})) ↾t (𝐶 ∪ {𝐵}))
76 cnex 11022 . . . . . . . . . . . . 13 ℂ ∈ V
7776ssex 5258 . . . . . . . . . . . 12 ((𝐴 ∪ {𝐵}) ⊆ ℂ → (𝐴 ∪ {𝐵}) ∈ V)
7820, 77syl 17 . . . . . . . . . . 11 ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝐴 ∪ {𝐵}) ∈ V)
79 restabs 22387 . . . . . . . . . . 11 ((𝐾 ∈ (TopOn‘ℂ) ∧ (𝐶 ∪ {𝐵}) ⊆ (𝐴 ∪ {𝐵}) ∧ (𝐴 ∪ {𝐵}) ∈ V) → ((𝐾t (𝐴 ∪ {𝐵})) ↾t (𝐶 ∪ {𝐵})) = (𝐾t (𝐶 ∪ {𝐵})))
8015, 29, 78, 79mp3an2i 1465 . . . . . . . . . 10 ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → ((𝐾t (𝐴 ∪ {𝐵})) ↾t (𝐶 ∪ {𝐵})) = (𝐾t (𝐶 ∪ {𝐵})))
8175, 80eqtr2id 2790 . . . . . . . . 9 ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝐾t (𝐶 ∪ {𝐵})) = (𝐽t (𝐶 ∪ {𝐵})))
8281oveq1d 7328 . . . . . . . 8 ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → ((𝐾t (𝐶 ∪ {𝐵})) CnP 𝐾) = ((𝐽t (𝐶 ∪ {𝐵})) CnP 𝐾))
8382fveq1d 6811 . . . . . . 7 ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (((𝐾t (𝐶 ∪ {𝐵})) CnP 𝐾)‘𝐵) = (((𝐽t (𝐶 ∪ {𝐵})) CnP 𝐾)‘𝐵))
8474, 83eleq12d 2832 . . . . . 6 ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → ((𝑧 ∈ (𝐶 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑥, ((𝐹𝐶)‘𝑧))) ∈ (((𝐾t (𝐶 ∪ {𝐵})) CnP 𝐾)‘𝐵) ↔ ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑥, (𝐹𝑧))) ↾ (𝐶 ∪ {𝐵})) ∈ (((𝐽t (𝐶 ∪ {𝐵})) CnP 𝐾)‘𝐵)))
8561, 84bitrd 278 . . . . 5 ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝑥 ∈ ((𝐹𝐶) lim 𝐵) ↔ ((𝑧 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑥, (𝐹𝑧))) ↾ (𝐶 ∪ {𝐵})) ∈ (((𝐽t (𝐶 ∪ {𝐵})) CnP 𝐾)‘𝐵)))
8654, 56, 853bitr4rd 311 . . . 4 ((𝜑 ∧ (𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ)) → (𝑥 ∈ ((𝐹𝐶) lim 𝐵) ↔ 𝑥 ∈ (𝐹 lim 𝐵)))
8786ex 413 . . 3 (𝜑 → ((𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝑥 ∈ ((𝐹𝐶) lim 𝐵) ↔ 𝑥 ∈ (𝐹 lim 𝐵))))
886, 12, 87pm5.21ndd 380 . 2 (𝜑 → (𝑥 ∈ ((𝐹𝐶) lim 𝐵) ↔ 𝑥 ∈ (𝐹 lim 𝐵)))
8988eqrdv 2735 1 (𝜑 → ((𝐹𝐶) lim 𝐵) = (𝐹 lim 𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  wo 844   = wceq 1540  wcel 2105  Vcvv 3441  cun 3894  wss 3896  ifcif 4469  {csn 4569   cuni 4848  cmpt 5168  dom cdm 5605  cres 5607  wf 6459  cfv 6463  (class class class)co 7313  cc 10939  t crest 17198  TopOpenctopn 17199  fldccnfld 20668  Topctop 22113  TopOnctopon 22130  intcnt 22239   CnP ccnp 22447   lim climc 25097
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2708  ax-rep 5222  ax-sep 5236  ax-nul 5243  ax-pow 5301  ax-pr 5365  ax-un 7626  ax-cnex 10997  ax-resscn 10998  ax-1cn 10999  ax-icn 11000  ax-addcl 11001  ax-addrcl 11002  ax-mulcl 11003  ax-mulrcl 11004  ax-mulcom 11005  ax-addass 11006  ax-mulass 11007  ax-distr 11008  ax-i2m1 11009  ax-1ne0 11010  ax-1rid 11011  ax-rnegex 11012  ax-rrecex 11013  ax-cnre 11014  ax-pre-lttri 11015  ax-pre-lttrn 11016  ax-pre-ltadd 11017  ax-pre-mulgt0 11018  ax-pre-sup 11019
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3350  df-reu 3351  df-rab 3405  df-v 3443  df-sbc 3726  df-csb 3842  df-dif 3899  df-un 3901  df-in 3903  df-ss 3913  df-pss 3915  df-nul 4267  df-if 4470  df-pw 4545  df-sn 4570  df-pr 4572  df-tp 4574  df-op 4576  df-uni 4849  df-int 4891  df-iun 4937  df-br 5086  df-opab 5148  df-mpt 5169  df-tr 5203  df-id 5505  df-eprel 5511  df-po 5519  df-so 5520  df-fr 5560  df-we 5562  df-xp 5611  df-rel 5612  df-cnv 5613  df-co 5614  df-dm 5615  df-rn 5616  df-res 5617  df-ima 5618  df-pred 6222  df-ord 6289  df-on 6290  df-lim 6291  df-suc 6292  df-iota 6415  df-fun 6465  df-fn 6466  df-f 6467  df-f1 6468  df-fo 6469  df-f1o 6470  df-fv 6471  df-riota 7270  df-ov 7316  df-oprab 7317  df-mpo 7318  df-om 7756  df-1st 7874  df-2nd 7875  df-frecs 8142  df-wrecs 8173  df-recs 8247  df-rdg 8286  df-1o 8342  df-er 8544  df-map 8663  df-pm 8664  df-en 8780  df-dom 8781  df-sdom 8782  df-fin 8783  df-fi 9238  df-sup 9269  df-inf 9270  df-pnf 11081  df-mnf 11082  df-xr 11083  df-ltxr 11084  df-le 11085  df-sub 11277  df-neg 11278  df-div 11703  df-nn 12044  df-2 12106  df-3 12107  df-4 12108  df-5 12109  df-6 12110  df-7 12111  df-8 12112  df-9 12113  df-n0 12304  df-z 12390  df-dec 12508  df-uz 12653  df-q 12759  df-rp 12801  df-xneg 12918  df-xadd 12919  df-xmul 12920  df-fz 13310  df-seq 13792  df-exp 13853  df-cj 14879  df-re 14880  df-im 14881  df-sqrt 15015  df-abs 15016  df-struct 16915  df-slot 16950  df-ndx 16962  df-base 16980  df-plusg 17042  df-mulr 17043  df-starv 17044  df-tset 17048  df-ple 17049  df-ds 17051  df-unif 17052  df-rest 17200  df-topn 17201  df-topgen 17221  df-psmet 20660  df-xmet 20661  df-met 20662  df-bl 20663  df-mopn 20664  df-cnfld 20669  df-top 22114  df-topon 22131  df-topsp 22153  df-bases 22167  df-ntr 22242  df-cnp 22450  df-xms 23544  df-ms 23545  df-limc 25101
This theorem is referenced by:  dvreslem  25144  dvaddbr  25173  dvmulbr  25174  lhop2  25250  lhop  25251  limciccioolb  43406  limcicciooub  43422  limcresiooub  43427  limcresioolb  43428  ioccncflimc  43670  icocncflimc  43674  dirkercncflem3  43890  fourierdlem32  43924  fourierdlem33  43925  fourierdlem48  43939  fourierdlem49  43940  fourierdlem62  43953  fouriersw  44016
  Copyright terms: Public domain W3C validator