Mathbox for Glauco Siliprandi < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  smflimsuplem8 Structured version   Visualization version   GIF version

Theorem smflimsuplem8 40796
 Description: The superior limit of a sequence of sigma-measurable functions is sigma-measurable. Proposition 121F (d) of [Fremlin1] p. 39 . (Contributed by Glauco Siliprandi, 23-Oct-2021.)
Hypotheses
Ref Expression
smflimsuplem8.m (𝜑𝑀 ∈ ℤ)
smflimsuplem8.z 𝑍 = (ℤ𝑀)
smflimsuplem8.s (𝜑𝑆 ∈ SAlg)
smflimsuplem8.f (𝜑𝐹:𝑍⟶(SMblFn‘𝑆))
smflimsuplem8.d 𝐷 = {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ}
smflimsuplem8.g 𝐺 = (𝑥𝐷 ↦ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))))
smflimsuplem8.e 𝐸 = (𝑘𝑍 ↦ {𝑥 𝑚 ∈ (ℤ𝑘)dom (𝐹𝑚) ∣ sup(ran (𝑚 ∈ (ℤ𝑘) ↦ ((𝐹𝑚)‘𝑥)), ℝ*, < ) ∈ ℝ})
smflimsuplem8.h 𝐻 = (𝑘𝑍 ↦ (𝑥 ∈ (𝐸𝑘) ↦ sup(ran (𝑚 ∈ (ℤ𝑘) ↦ ((𝐹𝑚)‘𝑥)), ℝ*, < )))
Assertion
Ref Expression
smflimsuplem8 (𝜑𝐺 ∈ (SMblFn‘𝑆))
Distinct variable groups:   𝑥,𝑘   𝐷,𝑘,𝑚,𝑛   𝑘,𝐸,𝑥   𝑘,𝐹,𝑚,𝑛,𝑥   𝑘,𝐻,𝑚,𝑛,𝑥   𝑚,𝑀   𝑆,𝑘,𝑛   𝑘,𝑍,𝑚,𝑛,𝑥   𝜑,𝑘,𝑚,𝑛,𝑥
Allowed substitution hints:   𝐷(𝑥)   𝑆(𝑥,𝑚)   𝐸(𝑚,𝑛)   𝐺(𝑥,𝑘,𝑚,𝑛)   𝑀(𝑥,𝑘,𝑛)

Proof of Theorem smflimsuplem8
Dummy variables 𝑤 𝑧 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 smflimsuplem8.g . . . 4 𝐺 = (𝑥𝐷 ↦ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))))
21a1i 11 . . 3 (𝜑𝐺 = (𝑥𝐷 ↦ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)))))
3 smflimsuplem8.m . . . . 5 (𝜑𝑀 ∈ ℤ)
4 smflimsuplem8.z . . . . 5 𝑍 = (ℤ𝑀)
5 smflimsuplem8.s . . . . 5 (𝜑𝑆 ∈ SAlg)
6 smflimsuplem8.f . . . . 5 (𝜑𝐹:𝑍⟶(SMblFn‘𝑆))
7 smflimsuplem8.d . . . . 5 𝐷 = {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ}
8 smflimsuplem8.e . . . . 5 𝐸 = (𝑘𝑍 ↦ {𝑥 𝑚 ∈ (ℤ𝑘)dom (𝐹𝑚) ∣ sup(ran (𝑚 ∈ (ℤ𝑘) ↦ ((𝐹𝑚)‘𝑥)), ℝ*, < ) ∈ ℝ})
9 smflimsuplem8.h . . . . 5 𝐻 = (𝑘𝑍 ↦ (𝑥 ∈ (𝐸𝑘) ↦ sup(ran (𝑚 ∈ (ℤ𝑘) ↦ ((𝐹𝑚)‘𝑥)), ℝ*, < )))
103, 4, 5, 6, 7, 8, 9smflimsuplem7 40795 . . . 4 (𝜑𝐷 = {𝑥 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ∣ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ })
11 rabidim1 3112 . . . . . . . 8 (𝑥 ∈ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ} → 𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚))
12 eliun 4515 . . . . . . . 8 (𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ↔ ∃𝑛𝑍 𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚))
1311, 12sylib 208 . . . . . . 7 (𝑥 ∈ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ} → ∃𝑛𝑍 𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚))
1413, 7eleq2s 2717 . . . . . 6 (𝑥𝐷 → ∃𝑛𝑍 𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚))
1514adantl 482 . . . . 5 ((𝜑𝑥𝐷) → ∃𝑛𝑍 𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚))
16 nfv 1841 . . . . . 6 𝑛(𝜑𝑥𝐷)
17 nfv 1841 . . . . . 6 𝑛(lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) = ( ⇝ ‘(𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)))
18 nfv 1841 . . . . . . . . . . 11 𝑘((𝜑𝑥𝐷) ∧ 𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚))
19 nfv 1841 . . . . . . . . . . . 12 𝑚(𝜑𝑥𝐷)
20 nfv 1841 . . . . . . . . . . . 12 𝑚 𝑛𝑍
21 nfcv 2762 . . . . . . . . . . . . 13 𝑚𝑥
22 nfii1 4542 . . . . . . . . . . . . 13 𝑚 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)
2321, 22nfel 2774 . . . . . . . . . . . 12 𝑚 𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)
2419, 20, 23nf3an 1829 . . . . . . . . . . 11 𝑚((𝜑𝑥𝐷) ∧ 𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚))
253adantr 481 . . . . . . . . . . . 12 ((𝜑𝑥𝐷) → 𝑀 ∈ ℤ)
26253ad2ant1 1080 . . . . . . . . . . 11 (((𝜑𝑥𝐷) ∧ 𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) → 𝑀 ∈ ℤ)
275adantr 481 . . . . . . . . . . . 12 ((𝜑𝑥𝐷) → 𝑆 ∈ SAlg)
28273ad2ant1 1080 . . . . . . . . . . 11 (((𝜑𝑥𝐷) ∧ 𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) → 𝑆 ∈ SAlg)
296adantr 481 . . . . . . . . . . . 12 ((𝜑𝑥𝐷) → 𝐹:𝑍⟶(SMblFn‘𝑆))
30293ad2ant1 1080 . . . . . . . . . . 11 (((𝜑𝑥𝐷) ∧ 𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) → 𝐹:𝑍⟶(SMblFn‘𝑆))
31 rabidim2 39104 . . . . . . . . . . . . . . . 16 (𝑥 ∈ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ} → (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ)
3231, 7eleq2s 2717 . . . . . . . . . . . . . . 15 (𝑥𝐷 → (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ)
33 fveq2 6178 . . . . . . . . . . . . . . . . . . . 20 (𝑚 = 𝑦 → (𝐹𝑚) = (𝐹𝑦))
3433fveq1d 6180 . . . . . . . . . . . . . . . . . . 19 (𝑚 = 𝑦 → ((𝐹𝑚)‘𝑥) = ((𝐹𝑦)‘𝑥))
3534cbvmptv 4741 . . . . . . . . . . . . . . . . . 18 (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) = (𝑦𝑍 ↦ ((𝐹𝑦)‘𝑥))
36 fveq2 6178 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = 𝑦 → (𝐹𝑧) = (𝐹𝑦))
3736fveq1d 6180 . . . . . . . . . . . . . . . . . . 19 (𝑧 = 𝑦 → ((𝐹𝑧)‘𝑥) = ((𝐹𝑦)‘𝑥))
3837cbvmptv 4741 . . . . . . . . . . . . . . . . . 18 (𝑧𝑍 ↦ ((𝐹𝑧)‘𝑥)) = (𝑦𝑍 ↦ ((𝐹𝑦)‘𝑥))
39 fveq2 6178 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = 𝑤 → (𝐹𝑧) = (𝐹𝑤))
4039fveq1d 6180 . . . . . . . . . . . . . . . . . . 19 (𝑧 = 𝑤 → ((𝐹𝑧)‘𝑥) = ((𝐹𝑤)‘𝑥))
4140cbvmptv 4741 . . . . . . . . . . . . . . . . . 18 (𝑧𝑍 ↦ ((𝐹𝑧)‘𝑥)) = (𝑤𝑍 ↦ ((𝐹𝑤)‘𝑥))
4235, 38, 413eqtr2i 2648 . . . . . . . . . . . . . . . . 17 (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) = (𝑤𝑍 ↦ ((𝐹𝑤)‘𝑥))
4342fveq2i 6181 . . . . . . . . . . . . . . . 16 (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) = (lim sup‘(𝑤𝑍 ↦ ((𝐹𝑤)‘𝑥)))
4443eleq1i 2690 . . . . . . . . . . . . . . 15 ((lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ ↔ (lim sup‘(𝑤𝑍 ↦ ((𝐹𝑤)‘𝑥))) ∈ ℝ)
4532, 44sylib 208 . . . . . . . . . . . . . 14 (𝑥𝐷 → (lim sup‘(𝑤𝑍 ↦ ((𝐹𝑤)‘𝑥))) ∈ ℝ)
4645adantl 482 . . . . . . . . . . . . 13 ((𝜑𝑥𝐷) → (lim sup‘(𝑤𝑍 ↦ ((𝐹𝑤)‘𝑥))) ∈ ℝ)
47463ad2ant1 1080 . . . . . . . . . . . 12 (((𝜑𝑥𝐷) ∧ 𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) → (lim sup‘(𝑤𝑍 ↦ ((𝐹𝑤)‘𝑥))) ∈ ℝ)
4847, 44sylibr 224 . . . . . . . . . . 11 (((𝜑𝑥𝐷) ∧ 𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) → (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ)
49 simp2 1060 . . . . . . . . . . 11 (((𝜑𝑥𝐷) ∧ 𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) → 𝑛𝑍)
50 simp3 1061 . . . . . . . . . . 11 (((𝜑𝑥𝐷) ∧ 𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) → 𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚))
5118, 24, 26, 4, 28, 30, 8, 9, 48, 49, 50smflimsuplem5 40793 . . . . . . . . . 10 (((𝜑𝑥𝐷) ∧ 𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) → (𝑘 ∈ (ℤ𝑛) ↦ ((𝐻𝑘)‘𝑥)) ⇝ (lim sup‘(𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑥))))
52 fvexd 6190 . . . . . . . . . . 11 (((𝜑𝑥𝐷) ∧ 𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) → (ℤ𝑛) ∈ V)
534fvexi 6189 . . . . . . . . . . . 12 𝑍 ∈ V
5453a1i 11 . . . . . . . . . . 11 (((𝜑𝑥𝐷) ∧ 𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) → 𝑍 ∈ V)
554, 49eluzelz2d 39453 . . . . . . . . . . 11 (((𝜑𝑥𝐷) ∧ 𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) → 𝑛 ∈ ℤ)
56 eqid 2620 . . . . . . . . . . 11 (ℤ𝑛) = (ℤ𝑛)
5755uzidd 39444 . . . . . . . . . . . 12 (((𝜑𝑥𝐷) ∧ 𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) → 𝑛 ∈ (ℤ𝑛))
5857uzssd 39447 . . . . . . . . . . 11 (((𝜑𝑥𝐷) ∧ 𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) → (ℤ𝑛) ⊆ (ℤ𝑛))
594, 49uzssd2 39457 . . . . . . . . . . 11 (((𝜑𝑥𝐷) ∧ 𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) → (ℤ𝑛) ⊆ 𝑍)
60 fvexd 6190 . . . . . . . . . . 11 ((((𝜑𝑥𝐷) ∧ 𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) ∧ 𝑘 ∈ (ℤ𝑛)) → ((𝐻𝑘)‘𝑥) ∈ V)
6118, 52, 54, 55, 56, 58, 59, 60climeqmpt 39729 . . . . . . . . . 10 (((𝜑𝑥𝐷) ∧ 𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) → ((𝑘 ∈ (ℤ𝑛) ↦ ((𝐻𝑘)‘𝑥)) ⇝ (lim sup‘(𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑥))) ↔ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ⇝ (lim sup‘(𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑥)))))
6251, 61mpbid 222 . . . . . . . . 9 (((𝜑𝑥𝐷) ∧ 𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) → (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ⇝ (lim sup‘(𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑥))))
63 simp1l 1083 . . . . . . . . . 10 (((𝜑𝑥𝐷) ∧ 𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) → 𝜑)
64 nfv 1841 . . . . . . . . . . . 12 𝑚𝜑
6564, 20nfan 1826 . . . . . . . . . . 11 𝑚(𝜑𝑛𝑍)
664eluzelz2 39440 . . . . . . . . . . . 12 (𝑛𝑍𝑛 ∈ ℤ)
6766adantl 482 . . . . . . . . . . 11 ((𝜑𝑛𝑍) → 𝑛 ∈ ℤ)
683adantr 481 . . . . . . . . . . 11 ((𝜑𝑛𝑍) → 𝑀 ∈ ℤ)
69 fvexd 6190 . . . . . . . . . . 11 (((𝜑𝑛𝑍) ∧ 𝑚 ∈ (ℤ𝑛)) → ((𝐹𝑚)‘𝑥) ∈ V)
70 fvexd 6190 . . . . . . . . . . 11 (((𝜑𝑛𝑍) ∧ 𝑚𝑍) → ((𝐹𝑚)‘𝑥) ∈ V)
7165, 67, 68, 56, 4, 69, 70limsupequzmpt 39761 . . . . . . . . . 10 ((𝜑𝑛𝑍) → (lim sup‘(𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑥))) = (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))))
7263, 49, 71syl2anc 692 . . . . . . . . 9 (((𝜑𝑥𝐷) ∧ 𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) → (lim sup‘(𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑥))) = (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))))
7362, 72breqtrd 4670 . . . . . . . 8 (((𝜑𝑥𝐷) ∧ 𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) → (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ⇝ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))))
7473climfvd 39730 . . . . . . 7 (((𝜑𝑥𝐷) ∧ 𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) → (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) = ( ⇝ ‘(𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥))))
75743exp 1262 . . . . . 6 ((𝜑𝑥𝐷) → (𝑛𝑍 → (𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) → (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) = ( ⇝ ‘(𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥))))))
7616, 17, 75rexlimd 3022 . . . . 5 ((𝜑𝑥𝐷) → (∃𝑛𝑍 𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) → (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) = ( ⇝ ‘(𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)))))
7715, 76mpd 15 . . . 4 ((𝜑𝑥𝐷) → (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) = ( ⇝ ‘(𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥))))
7810, 77mpteq12dva 4723 . . 3 (𝜑 → (𝑥𝐷 ↦ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)))) = (𝑥 ∈ {𝑥 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ∣ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ } ↦ ( ⇝ ‘(𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)))))
792, 78eqtrd 2654 . 2 (𝜑𝐺 = (𝑥 ∈ {𝑥 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ∣ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ } ↦ ( ⇝ ‘(𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)))))
803, 4, 5, 6, 8, 9smflimsuplem3 40791 . 2 (𝜑 → (𝑥 ∈ {𝑥 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ∣ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ } ↦ ( ⇝ ‘(𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)))) ∈ (SMblFn‘𝑆))
8179, 80eqeltrd 2699 1 (𝜑𝐺 ∈ (SMblFn‘𝑆))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1036   = wceq 1481   ∈ wcel 1988  ∃wrex 2910  {crab 2913  Vcvv 3195  ∪ ciun 4511  ∩ ciin 4512   class class class wbr 4644   ↦ cmpt 4720  dom cdm 5104  ran crn 5105  ⟶wf 5872  ‘cfv 5876  supcsup 8331  ℝcr 9920  ℝ*cxr 10058   < clt 10059  ℤcz 11362  ℤ≥cuz 11672  lim supclsp 14182   ⇝ cli 14196  SAlgcsalg 40291  SMblFncsmblfn 40672 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-rep 4762  ax-sep 4772  ax-nul 4780  ax-pow 4834  ax-pr 4897  ax-un 6934  ax-inf2 8523  ax-cc 9242  ax-ac2 9270  ax-cnex 9977  ax-resscn 9978  ax-1cn 9979  ax-icn 9980  ax-addcl 9981  ax-addrcl 9982  ax-mulcl 9983  ax-mulrcl 9984  ax-mulcom 9985  ax-addass 9986  ax-mulass 9987  ax-distr 9988  ax-i2m1 9989  ax-1ne0 9990  ax-1rid 9991  ax-rnegex 9992  ax-rrecex 9993  ax-cnre 9994  ax-pre-lttri 9995  ax-pre-lttrn 9996  ax-pre-ltadd 9997  ax-pre-mulgt0 9998  ax-pre-sup 9999 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ne 2792  df-nel 2895  df-ral 2914  df-rex 2915  df-reu 2916  df-rmo 2917  df-rab 2918  df-v 3197  df-sbc 3430  df-csb 3527  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-pss 3583  df-nul 3908  df-if 4078  df-pw 4151  df-sn 4169  df-pr 4171  df-tp 4173  df-op 4175  df-uni 4428  df-int 4467  df-iun 4513  df-iin 4514  df-br 4645  df-opab 4704  df-mpt 4721  df-tr 4744  df-id 5014  df-eprel 5019  df-po 5025  df-so 5026  df-fr 5063  df-se 5064  df-we 5065  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-rn 5115  df-res 5116  df-ima 5117  df-pred 5668  df-ord 5714  df-on 5715  df-lim 5716  df-suc 5717  df-iota 5839  df-fun 5878  df-fn 5879  df-f 5880  df-f1 5881  df-fo 5882  df-f1o 5883  df-fv 5884  df-isom 5885  df-riota 6596  df-ov 6638  df-oprab 6639  df-mpt2 6640  df-om 7051  df-1st 7153  df-2nd 7154  df-wrecs 7392  df-recs 7453  df-rdg 7491  df-1o 7545  df-oadd 7549  df-omul 7550  df-er 7727  df-map 7844  df-pm 7845  df-en 7941  df-dom 7942  df-sdom 7943  df-fin 7944  df-sup 8333  df-inf 8334  df-oi 8400  df-card 8750  df-acn 8753  df-ac 8924  df-pnf 10061  df-mnf 10062  df-xr 10063  df-ltxr 10064  df-le 10065  df-sub 10253  df-neg 10254  df-div 10670  df-nn 11006  df-2 11064  df-3 11065  df-n0 11278  df-z 11363  df-uz 11673  df-q 11774  df-rp 11818  df-ioo 12164  df-ioc 12165  df-ico 12166  df-fz 12312  df-fl 12576  df-ceil 12577  df-seq 12785  df-exp 12844  df-cj 13820  df-re 13821  df-im 13822  df-sqrt 13956  df-abs 13957  df-limsup 14183  df-clim 14200  df-rlim 14201  df-rest 16064  df-topgen 16085  df-top 20680  df-bases 20731  df-salg 40292  df-salgen 40296  df-smblfn 40673 This theorem is referenced by:  smflimsup  40797
 Copyright terms: Public domain W3C validator