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

Theorem smflimsuplem8 41825
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 41824 . . . 4 (𝜑𝐷 = {𝑥 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ∣ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ })
11 rabidim1 3328 . . . . . . . 8 (𝑥 ∈ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ} → 𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚))
12 eliun 4746 . . . . . . . 8 (𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ↔ ∃𝑛𝑍 𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚))
1311, 12sylib 210 . . . . . . 7 (𝑥 ∈ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ} → ∃𝑛𝑍 𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚))
1413, 7eleq2s 2924 . . . . . 6 (𝑥𝐷 → ∃𝑛𝑍 𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚))
1514adantl 475 . . . . 5 ((𝜑𝑥𝐷) → ∃𝑛𝑍 𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚))
16 nfv 2013 . . . . . 6 𝑛(𝜑𝑥𝐷)
17 nfv 2013 . . . . . 6 𝑛(lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) = ( ⇝ ‘(𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)))
18 nfv 2013 . . . . . . . . . . 11 𝑘((𝜑𝑥𝐷) ∧ 𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚))
19 nfv 2013 . . . . . . . . . . . 12 𝑚(𝜑𝑥𝐷)
20 nfv 2013 . . . . . . . . . . . 12 𝑚 𝑛𝑍
21 nfcv 2969 . . . . . . . . . . . . 13 𝑚𝑥
22 nfii1 4773 . . . . . . . . . . . . 13 𝑚 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)
2321, 22nfel 2982 . . . . . . . . . . . 12 𝑚 𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)
2419, 20, 23nf3an 2004 . . . . . . . . . . 11 𝑚((𝜑𝑥𝐷) ∧ 𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚))
253adantr 474 . . . . . . . . . . . 12 ((𝜑𝑥𝐷) → 𝑀 ∈ ℤ)
26253ad2ant1 1167 . . . . . . . . . . 11 (((𝜑𝑥𝐷) ∧ 𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) → 𝑀 ∈ ℤ)
275adantr 474 . . . . . . . . . . . 12 ((𝜑𝑥𝐷) → 𝑆 ∈ SAlg)
28273ad2ant1 1167 . . . . . . . . . . 11 (((𝜑𝑥𝐷) ∧ 𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) → 𝑆 ∈ SAlg)
296adantr 474 . . . . . . . . . . . 12 ((𝜑𝑥𝐷) → 𝐹:𝑍⟶(SMblFn‘𝑆))
30293ad2ant1 1167 . . . . . . . . . . 11 (((𝜑𝑥𝐷) ∧ 𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) → 𝐹:𝑍⟶(SMblFn‘𝑆))
31 rabidim2 40099 . . . . . . . . . . . . . . . 16 (𝑥 ∈ {𝑥 𝑛𝑍 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) ∣ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ} → (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ)
3231, 7eleq2s 2924 . . . . . . . . . . . . . . 15 (𝑥𝐷 → (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ)
33 fveq2 6437 . . . . . . . . . . . . . . . . . . . 20 (𝑚 = 𝑦 → (𝐹𝑚) = (𝐹𝑦))
3433fveq1d 6439 . . . . . . . . . . . . . . . . . . 19 (𝑚 = 𝑦 → ((𝐹𝑚)‘𝑥) = ((𝐹𝑦)‘𝑥))
3534cbvmptv 4975 . . . . . . . . . . . . . . . . . 18 (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) = (𝑦𝑍 ↦ ((𝐹𝑦)‘𝑥))
36 fveq2 6437 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = 𝑦 → (𝐹𝑧) = (𝐹𝑦))
3736fveq1d 6439 . . . . . . . . . . . . . . . . . . 19 (𝑧 = 𝑦 → ((𝐹𝑧)‘𝑥) = ((𝐹𝑦)‘𝑥))
3837cbvmptv 4975 . . . . . . . . . . . . . . . . . 18 (𝑧𝑍 ↦ ((𝐹𝑧)‘𝑥)) = (𝑦𝑍 ↦ ((𝐹𝑦)‘𝑥))
39 fveq2 6437 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = 𝑤 → (𝐹𝑧) = (𝐹𝑤))
4039fveq1d 6439 . . . . . . . . . . . . . . . . . . 19 (𝑧 = 𝑤 → ((𝐹𝑧)‘𝑥) = ((𝐹𝑤)‘𝑥))
4140cbvmptv 4975 . . . . . . . . . . . . . . . . . 18 (𝑧𝑍 ↦ ((𝐹𝑧)‘𝑥)) = (𝑤𝑍 ↦ ((𝐹𝑤)‘𝑥))
4235, 38, 413eqtr2i 2855 . . . . . . . . . . . . . . . . 17 (𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)) = (𝑤𝑍 ↦ ((𝐹𝑤)‘𝑥))
4342fveq2i 6440 . . . . . . . . . . . . . . . 16 (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) = (lim sup‘(𝑤𝑍 ↦ ((𝐹𝑤)‘𝑥)))
4443eleq1i 2897 . . . . . . . . . . . . . . 15 ((lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ ↔ (lim sup‘(𝑤𝑍 ↦ ((𝐹𝑤)‘𝑥))) ∈ ℝ)
4532, 44sylib 210 . . . . . . . . . . . . . 14 (𝑥𝐷 → (lim sup‘(𝑤𝑍 ↦ ((𝐹𝑤)‘𝑥))) ∈ ℝ)
4645adantl 475 . . . . . . . . . . . . 13 ((𝜑𝑥𝐷) → (lim sup‘(𝑤𝑍 ↦ ((𝐹𝑤)‘𝑥))) ∈ ℝ)
47463ad2ant1 1167 . . . . . . . . . . . 12 (((𝜑𝑥𝐷) ∧ 𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) → (lim sup‘(𝑤𝑍 ↦ ((𝐹𝑤)‘𝑥))) ∈ ℝ)
4847, 44sylibr 226 . . . . . . . . . . 11 (((𝜑𝑥𝐷) ∧ 𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) → (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) ∈ ℝ)
49 simp2 1171 . . . . . . . . . . 11 (((𝜑𝑥𝐷) ∧ 𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) → 𝑛𝑍)
50 simp3 1172 . . . . . . . . . . 11 (((𝜑𝑥𝐷) ∧ 𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) → 𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚))
5118, 24, 26, 4, 28, 30, 8, 9, 48, 49, 50smflimsuplem5 41822 . . . . . . . . . 10 (((𝜑𝑥𝐷) ∧ 𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) → (𝑘 ∈ (ℤ𝑛) ↦ ((𝐻𝑘)‘𝑥)) ⇝ (lim sup‘(𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑥))))
52 fvexd 6452 . . . . . . . . . . 11 (((𝜑𝑥𝐷) ∧ 𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) → (ℤ𝑛) ∈ V)
534fvexi 6451 . . . . . . . . . . . 12 𝑍 ∈ V
5453a1i 11 . . . . . . . . . . 11 (((𝜑𝑥𝐷) ∧ 𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) → 𝑍 ∈ V)
554, 49eluzelz2d 40433 . . . . . . . . . . 11 (((𝜑𝑥𝐷) ∧ 𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) → 𝑛 ∈ ℤ)
56 eqid 2825 . . . . . . . . . . 11 (ℤ𝑛) = (ℤ𝑛)
5755uzidd 40424 . . . . . . . . . . . 12 (((𝜑𝑥𝐷) ∧ 𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) → 𝑛 ∈ (ℤ𝑛))
5857uzssd 40427 . . . . . . . . . . 11 (((𝜑𝑥𝐷) ∧ 𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) → (ℤ𝑛) ⊆ (ℤ𝑛))
594, 49uzssd2 40437 . . . . . . . . . . 11 (((𝜑𝑥𝐷) ∧ 𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) → (ℤ𝑛) ⊆ 𝑍)
60 fvexd 6452 . . . . . . . . . . 11 ((((𝜑𝑥𝐷) ∧ 𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) ∧ 𝑘 ∈ (ℤ𝑛)) → ((𝐻𝑘)‘𝑥) ∈ V)
6118, 52, 54, 55, 56, 58, 59, 60climeqmpt 40722 . . . . . . . . . 10 (((𝜑𝑥𝐷) ∧ 𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) → ((𝑘 ∈ (ℤ𝑛) ↦ ((𝐻𝑘)‘𝑥)) ⇝ (lim sup‘(𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑥))) ↔ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ⇝ (lim sup‘(𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑥)))))
6251, 61mpbid 224 . . . . . . . . 9 (((𝜑𝑥𝐷) ∧ 𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) → (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ⇝ (lim sup‘(𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑥))))
63 simp1l 1258 . . . . . . . . . 10 (((𝜑𝑥𝐷) ∧ 𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) → 𝜑)
64 nfv 2013 . . . . . . . . . . . 12 𝑚𝜑
6564, 20nfan 2002 . . . . . . . . . . 11 𝑚(𝜑𝑛𝑍)
664eluzelz2 40420 . . . . . . . . . . . 12 (𝑛𝑍𝑛 ∈ ℤ)
6766adantl 475 . . . . . . . . . . 11 ((𝜑𝑛𝑍) → 𝑛 ∈ ℤ)
683adantr 474 . . . . . . . . . . 11 ((𝜑𝑛𝑍) → 𝑀 ∈ ℤ)
69 fvexd 6452 . . . . . . . . . . 11 (((𝜑𝑛𝑍) ∧ 𝑚 ∈ (ℤ𝑛)) → ((𝐹𝑚)‘𝑥) ∈ V)
70 fvexd 6452 . . . . . . . . . . 11 (((𝜑𝑛𝑍) ∧ 𝑚𝑍) → ((𝐹𝑚)‘𝑥) ∈ V)
7165, 67, 68, 56, 4, 69, 70limsupequzmpt 40754 . . . . . . . . . 10 ((𝜑𝑛𝑍) → (lim sup‘(𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑥))) = (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))))
7263, 49, 71syl2anc 579 . . . . . . . . 9 (((𝜑𝑥𝐷) ∧ 𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) → (lim sup‘(𝑚 ∈ (ℤ𝑛) ↦ ((𝐹𝑚)‘𝑥))) = (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))))
7362, 72breqtrd 4901 . . . . . . . 8 (((𝜑𝑥𝐷) ∧ 𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) → (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ⇝ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))))
7473climfvd 40723 . . . . . . 7 (((𝜑𝑥𝐷) ∧ 𝑛𝑍𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚)) → (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) = ( ⇝ ‘(𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥))))
75743exp 1152 . . . . . 6 ((𝜑𝑥𝐷) → (𝑛𝑍 → (𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) → (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) = ( ⇝ ‘(𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥))))))
7616, 17, 75rexlimd 3235 . . . . 5 ((𝜑𝑥𝐷) → (∃𝑛𝑍 𝑥 𝑚 ∈ (ℤ𝑛)dom (𝐹𝑚) → (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) = ( ⇝ ‘(𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)))))
7715, 76mpd 15 . . . 4 ((𝜑𝑥𝐷) → (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥))) = ( ⇝ ‘(𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥))))
7810, 77mpteq12dva 4957 . . 3 (𝜑 → (𝑥𝐷 ↦ (lim sup‘(𝑚𝑍 ↦ ((𝐹𝑚)‘𝑥)))) = (𝑥 ∈ {𝑥 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ∣ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ } ↦ ( ⇝ ‘(𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)))))
792, 78eqtrd 2861 . 2 (𝜑𝐺 = (𝑥 ∈ {𝑥 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ∣ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ } ↦ ( ⇝ ‘(𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)))))
803, 4, 5, 6, 8, 9smflimsuplem3 41820 . 2 (𝜑 → (𝑥 ∈ {𝑥 𝑛𝑍 𝑘 ∈ (ℤ𝑛)dom (𝐻𝑘) ∣ (𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)) ∈ dom ⇝ } ↦ ( ⇝ ‘(𝑘𝑍 ↦ ((𝐻𝑘)‘𝑥)))) ∈ (SMblFn‘𝑆))
8179, 80eqeltrd 2906 1 (𝜑𝐺 ∈ (SMblFn‘𝑆))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 386  w3a 1111   = wceq 1656  wcel 2164  wrex 3118  {crab 3121  Vcvv 3414   ciun 4742   ciin 4743   class class class wbr 4875  cmpt 4954  dom cdm 5346  ran crn 5347  wf 6123  cfv 6127  supcsup 8621  cr 10258  *cxr 10397   < clt 10398  cz 11711  cuz 11975  lim supclsp 14585  cli 14599  SAlgcsalg 41317  SMblFncsmblfn 41701
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-8 2166  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-13 2389  ax-ext 2803  ax-rep 4996  ax-sep 5007  ax-nul 5015  ax-pow 5067  ax-pr 5129  ax-un 7214  ax-inf2 8822  ax-cc 9579  ax-ac2 9607  ax-cnex 10315  ax-resscn 10316  ax-1cn 10317  ax-icn 10318  ax-addcl 10319  ax-addrcl 10320  ax-mulcl 10321  ax-mulrcl 10322  ax-mulcom 10323  ax-addass 10324  ax-mulass 10325  ax-distr 10326  ax-i2m1 10327  ax-1ne0 10328  ax-1rid 10329  ax-rnegex 10330  ax-rrecex 10331  ax-cnre 10332  ax-pre-lttri 10333  ax-pre-lttrn 10334  ax-pre-ltadd 10335  ax-pre-mulgt0 10336  ax-pre-sup 10337
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-3or 1112  df-3an 1113  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ne 3000  df-nel 3103  df-ral 3122  df-rex 3123  df-reu 3124  df-rmo 3125  df-rab 3126  df-v 3416  df-sbc 3663  df-csb 3758  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-pss 3814  df-nul 4147  df-if 4309  df-pw 4382  df-sn 4400  df-pr 4402  df-tp 4404  df-op 4406  df-uni 4661  df-int 4700  df-iun 4744  df-iin 4745  df-br 4876  df-opab 4938  df-mpt 4955  df-tr 4978  df-id 5252  df-eprel 5257  df-po 5265  df-so 5266  df-fr 5305  df-se 5306  df-we 5307  df-xp 5352  df-rel 5353  df-cnv 5354  df-co 5355  df-dm 5356  df-rn 5357  df-res 5358  df-ima 5359  df-pred 5924  df-ord 5970  df-on 5971  df-lim 5972  df-suc 5973  df-iota 6090  df-fun 6129  df-fn 6130  df-f 6131  df-f1 6132  df-fo 6133  df-f1o 6134  df-fv 6135  df-isom 6136  df-riota 6871  df-ov 6913  df-oprab 6914  df-mpt2 6915  df-om 7332  df-1st 7433  df-2nd 7434  df-wrecs 7677  df-recs 7739  df-rdg 7777  df-1o 7831  df-oadd 7835  df-omul 7836  df-er 8014  df-map 8129  df-pm 8130  df-en 8229  df-dom 8230  df-sdom 8231  df-fin 8232  df-sup 8623  df-inf 8624  df-oi 8691  df-card 9085  df-acn 9088  df-ac 9259  df-pnf 10400  df-mnf 10401  df-xr 10402  df-ltxr 10403  df-le 10404  df-sub 10594  df-neg 10595  df-div 11017  df-nn 11358  df-2 11421  df-3 11422  df-n0 11626  df-z 11712  df-uz 11976  df-q 12079  df-rp 12120  df-ioo 12474  df-ioc 12475  df-ico 12476  df-fz 12627  df-fl 12895  df-ceil 12896  df-seq 13103  df-exp 13162  df-cj 14223  df-re 14224  df-im 14225  df-sqrt 14359  df-abs 14360  df-limsup 14586  df-clim 14603  df-rlim 14604  df-rest 16443  df-topgen 16464  df-top 21076  df-bases 21128  df-salg 41318  df-salgen 41322  df-smblfn 41702
This theorem is referenced by:  smflimsup  41826
  Copyright terms: Public domain W3C validator