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

Theorem smfpimcc 45459
Description: Given a countable set of sigma-measurable functions, and a Borel set 𝐴 there exists a choice function that, for each measurable function, chooses a measurable set that, when intersected with the function's domain, gives the preimage of 𝐴. This is a generalization of the observation at the beginning of the proof of Proposition 121F of [Fremlin1] p. 39 . The statement would also be provable for uncountable sets, but in most cases it will suffice to consider the countable case, and only the axiom of countable choice will be needed. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
Hypotheses
Ref Expression
smfpimcc.1 𝑛𝐹
smfpimcc.z 𝑍 = (ℤ𝑀)
smfpimcc.s (𝜑𝑆 ∈ SAlg)
smfpimcc.f (𝜑𝐹:𝑍⟶(SMblFn‘𝑆))
smfpimcc.j 𝐽 = (topGen‘ran (,))
smfpimcc.b 𝐵 = (SalGen‘𝐽)
smfpimcc.a (𝜑𝐴𝐵)
Assertion
Ref Expression
smfpimcc (𝜑 → ∃(:𝑍𝑆 ∧ ∀𝑛𝑍 ((𝐹𝑛) “ 𝐴) = ((𝑛) ∩ dom (𝐹𝑛))))
Distinct variable groups:   𝐴,,𝑛   ,𝐹   𝑆,   ,𝑍,𝑛
Allowed substitution hints:   𝜑(,𝑛)   𝐵(,𝑛)   𝑆(𝑛)   𝐹(𝑛)   𝐽(,𝑛)   𝑀(,𝑛)

Proof of Theorem smfpimcc
Dummy variables 𝑓 𝑚 𝑠 𝑤 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 smfpimcc.z . . . . . . 7 𝑍 = (ℤ𝑀)
21uzct 43683 . . . . . 6 𝑍 ≼ ω
32a1i 11 . . . . 5 (𝜑𝑍 ≼ ω)
4 mptct 10529 . . . . 5 (𝑍 ≼ ω → (𝑚𝑍 ↦ {𝑠𝑆 ∣ ((𝐹𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹𝑚))}) ≼ ω)
5 rnct 10516 . . . . 5 ((𝑚𝑍 ↦ {𝑠𝑆 ∣ ((𝐹𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹𝑚))}) ≼ ω → ran (𝑚𝑍 ↦ {𝑠𝑆 ∣ ((𝐹𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹𝑚))}) ≼ ω)
63, 4, 53syl 18 . . . 4 (𝜑 → ran (𝑚𝑍 ↦ {𝑠𝑆 ∣ ((𝐹𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹𝑚))}) ≼ ω)
7 vex 3479 . . . . . . . 8 𝑦 ∈ V
8 eqid 2733 . . . . . . . . 9 (𝑚𝑍 ↦ {𝑠𝑆 ∣ ((𝐹𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹𝑚))}) = (𝑚𝑍 ↦ {𝑠𝑆 ∣ ((𝐹𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹𝑚))})
98elrnmpt 5953 . . . . . . . 8 (𝑦 ∈ V → (𝑦 ∈ ran (𝑚𝑍 ↦ {𝑠𝑆 ∣ ((𝐹𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹𝑚))}) ↔ ∃𝑚𝑍 𝑦 = {𝑠𝑆 ∣ ((𝐹𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹𝑚))}))
107, 9ax-mp 5 . . . . . . 7 (𝑦 ∈ ran (𝑚𝑍 ↦ {𝑠𝑆 ∣ ((𝐹𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹𝑚))}) ↔ ∃𝑚𝑍 𝑦 = {𝑠𝑆 ∣ ((𝐹𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹𝑚))})
1110biimpi 215 . . . . . 6 (𝑦 ∈ ran (𝑚𝑍 ↦ {𝑠𝑆 ∣ ((𝐹𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹𝑚))}) → ∃𝑚𝑍 𝑦 = {𝑠𝑆 ∣ ((𝐹𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹𝑚))})
1211adantl 483 . . . . 5 ((𝜑𝑦 ∈ ran (𝑚𝑍 ↦ {𝑠𝑆 ∣ ((𝐹𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹𝑚))})) → ∃𝑚𝑍 𝑦 = {𝑠𝑆 ∣ ((𝐹𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹𝑚))})
13 simp3 1139 . . . . . . . . 9 ((𝜑𝑚𝑍𝑦 = {𝑠𝑆 ∣ ((𝐹𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹𝑚))}) → 𝑦 = {𝑠𝑆 ∣ ((𝐹𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹𝑚))})
14 smfpimcc.s . . . . . . . . . . . . . 14 (𝜑𝑆 ∈ SAlg)
1514adantr 482 . . . . . . . . . . . . 13 ((𝜑𝑚𝑍) → 𝑆 ∈ SAlg)
16 smfpimcc.f . . . . . . . . . . . . . 14 (𝜑𝐹:𝑍⟶(SMblFn‘𝑆))
1716ffvelcdmda 7082 . . . . . . . . . . . . 13 ((𝜑𝑚𝑍) → (𝐹𝑚) ∈ (SMblFn‘𝑆))
18 eqid 2733 . . . . . . . . . . . . 13 dom (𝐹𝑚) = dom (𝐹𝑚)
19 smfpimcc.j . . . . . . . . . . . . 13 𝐽 = (topGen‘ran (,))
20 smfpimcc.b . . . . . . . . . . . . 13 𝐵 = (SalGen‘𝐽)
21 smfpimcc.a . . . . . . . . . . . . . 14 (𝜑𝐴𝐵)
2221adantr 482 . . . . . . . . . . . . 13 ((𝜑𝑚𝑍) → 𝐴𝐵)
23 eqid 2733 . . . . . . . . . . . . 13 ((𝐹𝑚) “ 𝐴) = ((𝐹𝑚) “ 𝐴)
2415, 17, 18, 19, 20, 22, 23smfpimbor1 45451 . . . . . . . . . . . 12 ((𝜑𝑚𝑍) → ((𝐹𝑚) “ 𝐴) ∈ (𝑆t dom (𝐹𝑚)))
25 fvex 6901 . . . . . . . . . . . . . . . 16 (𝐹𝑚) ∈ V
2625dmex 7897 . . . . . . . . . . . . . . 15 dom (𝐹𝑚) ∈ V
2726a1i 11 . . . . . . . . . . . . . 14 (𝜑 → dom (𝐹𝑚) ∈ V)
28 elrest 17369 . . . . . . . . . . . . . 14 ((𝑆 ∈ SAlg ∧ dom (𝐹𝑚) ∈ V) → (((𝐹𝑚) “ 𝐴) ∈ (𝑆t dom (𝐹𝑚)) ↔ ∃𝑠𝑆 ((𝐹𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹𝑚))))
2914, 27, 28syl2anc 585 . . . . . . . . . . . . 13 (𝜑 → (((𝐹𝑚) “ 𝐴) ∈ (𝑆t dom (𝐹𝑚)) ↔ ∃𝑠𝑆 ((𝐹𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹𝑚))))
3029adantr 482 . . . . . . . . . . . 12 ((𝜑𝑚𝑍) → (((𝐹𝑚) “ 𝐴) ∈ (𝑆t dom (𝐹𝑚)) ↔ ∃𝑠𝑆 ((𝐹𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹𝑚))))
3124, 30mpbid 231 . . . . . . . . . . 11 ((𝜑𝑚𝑍) → ∃𝑠𝑆 ((𝐹𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹𝑚)))
32 rabn0 4384 . . . . . . . . . . 11 ({𝑠𝑆 ∣ ((𝐹𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹𝑚))} ≠ ∅ ↔ ∃𝑠𝑆 ((𝐹𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹𝑚)))
3331, 32sylibr 233 . . . . . . . . . 10 ((𝜑𝑚𝑍) → {𝑠𝑆 ∣ ((𝐹𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹𝑚))} ≠ ∅)
34333adant3 1133 . . . . . . . . 9 ((𝜑𝑚𝑍𝑦 = {𝑠𝑆 ∣ ((𝐹𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹𝑚))}) → {𝑠𝑆 ∣ ((𝐹𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹𝑚))} ≠ ∅)
3513, 34eqnetrd 3009 . . . . . . . 8 ((𝜑𝑚𝑍𝑦 = {𝑠𝑆 ∣ ((𝐹𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹𝑚))}) → 𝑦 ≠ ∅)
36353exp 1120 . . . . . . 7 (𝜑 → (𝑚𝑍 → (𝑦 = {𝑠𝑆 ∣ ((𝐹𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹𝑚))} → 𝑦 ≠ ∅)))
3736rexlimdv 3154 . . . . . 6 (𝜑 → (∃𝑚𝑍 𝑦 = {𝑠𝑆 ∣ ((𝐹𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹𝑚))} → 𝑦 ≠ ∅))
3837adantr 482 . . . . 5 ((𝜑𝑦 ∈ ran (𝑚𝑍 ↦ {𝑠𝑆 ∣ ((𝐹𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹𝑚))})) → (∃𝑚𝑍 𝑦 = {𝑠𝑆 ∣ ((𝐹𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹𝑚))} → 𝑦 ≠ ∅))
3912, 38mpd 15 . . . 4 ((𝜑𝑦 ∈ ran (𝑚𝑍 ↦ {𝑠𝑆 ∣ ((𝐹𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹𝑚))})) → 𝑦 ≠ ∅)
406, 39axccd2 43862 . . 3 (𝜑 → ∃𝑓𝑦 ∈ ran (𝑚𝑍 ↦ {𝑠𝑆 ∣ ((𝐹𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹𝑚))})(𝑓𝑦) ∈ 𝑦)
41 nfv 1918 . . . . . . 7 𝑚𝜑
42 nfmpt1 5255 . . . . . . . . 9 𝑚(𝑚𝑍 ↦ {𝑠𝑆 ∣ ((𝐹𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹𝑚))})
4342nfrn 5949 . . . . . . . 8 𝑚ran (𝑚𝑍 ↦ {𝑠𝑆 ∣ ((𝐹𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹𝑚))})
44 nfv 1918 . . . . . . . 8 𝑚(𝑓𝑦) ∈ 𝑦
4543, 44nfralw 3309 . . . . . . 7 𝑚𝑦 ∈ ran (𝑚𝑍 ↦ {𝑠𝑆 ∣ ((𝐹𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹𝑚))})(𝑓𝑦) ∈ 𝑦
4641, 45nfan 1903 . . . . . 6 𝑚(𝜑 ∧ ∀𝑦 ∈ ran (𝑚𝑍 ↦ {𝑠𝑆 ∣ ((𝐹𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹𝑚))})(𝑓𝑦) ∈ 𝑦)
471fvexi 6902 . . . . . 6 𝑍 ∈ V
4814adantr 482 . . . . . 6 ((𝜑 ∧ ∀𝑦 ∈ ran (𝑚𝑍 ↦ {𝑠𝑆 ∣ ((𝐹𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹𝑚))})(𝑓𝑦) ∈ 𝑦) → 𝑆 ∈ SAlg)
49 fveq2 6888 . . . . . . . . 9 (𝑦 = 𝑤 → (𝑓𝑦) = (𝑓𝑤))
50 id 22 . . . . . . . . 9 (𝑦 = 𝑤𝑦 = 𝑤)
5149, 50eleq12d 2828 . . . . . . . 8 (𝑦 = 𝑤 → ((𝑓𝑦) ∈ 𝑦 ↔ (𝑓𝑤) ∈ 𝑤))
5251rspccva 3611 . . . . . . 7 ((∀𝑦 ∈ ran (𝑚𝑍 ↦ {𝑠𝑆 ∣ ((𝐹𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹𝑚))})(𝑓𝑦) ∈ 𝑦𝑤 ∈ ran (𝑚𝑍 ↦ {𝑠𝑆 ∣ ((𝐹𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹𝑚))})) → (𝑓𝑤) ∈ 𝑤)
5352adantll 713 . . . . . 6 (((𝜑 ∧ ∀𝑦 ∈ ran (𝑚𝑍 ↦ {𝑠𝑆 ∣ ((𝐹𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹𝑚))})(𝑓𝑦) ∈ 𝑦) ∧ 𝑤 ∈ ran (𝑚𝑍 ↦ {𝑠𝑆 ∣ ((𝐹𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹𝑚))})) → (𝑓𝑤) ∈ 𝑤)
54 eqid 2733 . . . . . 6 (𝑚𝑍 ↦ (𝑓‘{𝑠𝑆 ∣ ((𝐹𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹𝑚))})) = (𝑚𝑍 ↦ (𝑓‘{𝑠𝑆 ∣ ((𝐹𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹𝑚))}))
5546, 47, 48, 53, 54smfpimcclem 45458 . . . . 5 ((𝜑 ∧ ∀𝑦 ∈ ran (𝑚𝑍 ↦ {𝑠𝑆 ∣ ((𝐹𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹𝑚))})(𝑓𝑦) ∈ 𝑦) → ∃(:𝑍𝑆 ∧ ∀𝑚𝑍 ((𝐹𝑚) “ 𝐴) = ((𝑚) ∩ dom (𝐹𝑚))))
5655ex 414 . . . 4 (𝜑 → (∀𝑦 ∈ ran (𝑚𝑍 ↦ {𝑠𝑆 ∣ ((𝐹𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹𝑚))})(𝑓𝑦) ∈ 𝑦 → ∃(:𝑍𝑆 ∧ ∀𝑚𝑍 ((𝐹𝑚) “ 𝐴) = ((𝑚) ∩ dom (𝐹𝑚)))))
5756exlimdv 1937 . . 3 (𝜑 → (∃𝑓𝑦 ∈ ran (𝑚𝑍 ↦ {𝑠𝑆 ∣ ((𝐹𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹𝑚))})(𝑓𝑦) ∈ 𝑦 → ∃(:𝑍𝑆 ∧ ∀𝑚𝑍 ((𝐹𝑚) “ 𝐴) = ((𝑚) ∩ dom (𝐹𝑚)))))
5840, 57mpd 15 . 2 (𝜑 → ∃(:𝑍𝑆 ∧ ∀𝑚𝑍 ((𝐹𝑚) “ 𝐴) = ((𝑚) ∩ dom (𝐹𝑚))))
59 smfpimcc.1 . . . . . . . . 9 𝑛𝐹
60 nfcv 2904 . . . . . . . . 9 𝑛𝑚
6159, 60nffv 6898 . . . . . . . 8 𝑛(𝐹𝑚)
6261nfcnv 5876 . . . . . . 7 𝑛(𝐹𝑚)
63 nfcv 2904 . . . . . . 7 𝑛𝐴
6462, 63nfima 6065 . . . . . 6 𝑛((𝐹𝑚) “ 𝐴)
65 nfcv 2904 . . . . . . 7 𝑛(𝑚)
6661nfdm 5948 . . . . . . 7 𝑛dom (𝐹𝑚)
6765, 66nfin 4215 . . . . . 6 𝑛((𝑚) ∩ dom (𝐹𝑚))
6864, 67nfeq 2917 . . . . 5 𝑛((𝐹𝑚) “ 𝐴) = ((𝑚) ∩ dom (𝐹𝑚))
69 nfv 1918 . . . . 5 𝑚((𝐹𝑛) “ 𝐴) = ((𝑛) ∩ dom (𝐹𝑛))
70 fveq2 6888 . . . . . . . 8 (𝑚 = 𝑛 → (𝐹𝑚) = (𝐹𝑛))
7170cnveqd 5873 . . . . . . 7 (𝑚 = 𝑛(𝐹𝑚) = (𝐹𝑛))
7271imaeq1d 6056 . . . . . 6 (𝑚 = 𝑛 → ((𝐹𝑚) “ 𝐴) = ((𝐹𝑛) “ 𝐴))
73 fveq2 6888 . . . . . . 7 (𝑚 = 𝑛 → (𝑚) = (𝑛))
7470dmeqd 5903 . . . . . . 7 (𝑚 = 𝑛 → dom (𝐹𝑚) = dom (𝐹𝑛))
7573, 74ineq12d 4212 . . . . . 6 (𝑚 = 𝑛 → ((𝑚) ∩ dom (𝐹𝑚)) = ((𝑛) ∩ dom (𝐹𝑛)))
7672, 75eqeq12d 2749 . . . . 5 (𝑚 = 𝑛 → (((𝐹𝑚) “ 𝐴) = ((𝑚) ∩ dom (𝐹𝑚)) ↔ ((𝐹𝑛) “ 𝐴) = ((𝑛) ∩ dom (𝐹𝑛))))
7768, 69, 76cbvralw 3304 . . . 4 (∀𝑚𝑍 ((𝐹𝑚) “ 𝐴) = ((𝑚) ∩ dom (𝐹𝑚)) ↔ ∀𝑛𝑍 ((𝐹𝑛) “ 𝐴) = ((𝑛) ∩ dom (𝐹𝑛)))
7877anbi2i 624 . . 3 ((:𝑍𝑆 ∧ ∀𝑚𝑍 ((𝐹𝑚) “ 𝐴) = ((𝑚) ∩ dom (𝐹𝑚))) ↔ (:𝑍𝑆 ∧ ∀𝑛𝑍 ((𝐹𝑛) “ 𝐴) = ((𝑛) ∩ dom (𝐹𝑛))))
7978exbii 1851 . 2 (∃(:𝑍𝑆 ∧ ∀𝑚𝑍 ((𝐹𝑚) “ 𝐴) = ((𝑚) ∩ dom (𝐹𝑚))) ↔ ∃(:𝑍𝑆 ∧ ∀𝑛𝑍 ((𝐹𝑛) “ 𝐴) = ((𝑛) ∩ dom (𝐹𝑛))))
8058, 79sylib 217 1 (𝜑 → ∃(:𝑍𝑆 ∧ ∀𝑛𝑍 ((𝐹𝑛) “ 𝐴) = ((𝑛) ∩ dom (𝐹𝑛))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397  w3a 1088   = wceq 1542  wex 1782  wcel 2107  wnfc 2884  wne 2941  wral 3062  wrex 3071  {crab 3433  Vcvv 3475  cin 3946  c0 4321   class class class wbr 5147  cmpt 5230  ccnv 5674  dom cdm 5675  ran crn 5676  cima 5678  wf 6536  cfv 6540  (class class class)co 7404  ωcom 7850  cdom 8933  cuz 12818  (,)cioo 13320  t crest 17362  topGenctg 17379  SAlgcsalg 44959  SalGencsalgen 44963  SMblFncsmblfn 45346
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7720  ax-inf2 9632  ax-cc 10426  ax-ac2 10454  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183  ax-pre-sup 11184
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-iin 4999  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-se 5631  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6297  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-isom 6549  df-riota 7360  df-ov 7407  df-oprab 7408  df-mpo 7409  df-om 7851  df-1st 7970  df-2nd 7971  df-frecs 8261  df-wrecs 8292  df-recs 8366  df-rdg 8405  df-1o 8461  df-oadd 8465  df-omul 8466  df-er 8699  df-map 8818  df-pm 8819  df-en 8936  df-dom 8937  df-sdom 8938  df-fin 8939  df-sup 9433  df-inf 9434  df-oi 9501  df-card 9930  df-acn 9933  df-ac 10107  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11442  df-neg 11443  df-div 11868  df-nn 12209  df-n0 12469  df-z 12555  df-uz 12819  df-q 12929  df-rp 12971  df-ioo 13324  df-ico 13326  df-fl 13753  df-rest 17364  df-topgen 17385  df-top 22378  df-bases 22431  df-salg 44960  df-salgen 44964  df-smblfn 45347
This theorem is referenced by:  smfsuplem2  45463
  Copyright terms: Public domain W3C validator