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

Theorem smfresal 43048
Description: Given a sigma-measurable function, the subsets of whose preimage is in the sigma-algebra induced by the function's domain, form a sigma-algebra. First part of the proof of Proposition 121E (f) of [Fremlin1] p. 38 . (Contributed by Glauco Siliprandi, 26-Jun-2021.)
Hypotheses
Ref Expression
smfresal.s (𝜑𝑆 ∈ SAlg)
smfresal.f (𝜑𝐹 ∈ (SMblFn‘𝑆))
smfresal.d 𝐷 = dom 𝐹
smfresal.t 𝑇 = {𝑒 ∈ 𝒫 ℝ ∣ (𝐹𝑒) ∈ (𝑆t 𝐷)}
Assertion
Ref Expression
smfresal (𝜑𝑇 ∈ SAlg)
Distinct variable groups:   𝐷,𝑒   𝑒,𝐹   𝑆,𝑒   𝜑,𝑒
Allowed substitution hint:   𝑇(𝑒)

Proof of Theorem smfresal
Dummy variables 𝑛 𝑥 𝑔 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 smfresal.t . . . 4 𝑇 = {𝑒 ∈ 𝒫 ℝ ∣ (𝐹𝑒) ∈ (𝑆t 𝐷)}
2 reex 10620 . . . . 5 ℝ ∈ V
32pwex 5272 . . . 4 𝒫 ℝ ∈ V
41, 3rabex2 5228 . . 3 𝑇 ∈ V
54a1i 11 . 2 (𝜑𝑇 ∈ V)
6 0elpw 5247 . . . . 5 ∅ ∈ 𝒫 ℝ
76a1i 11 . . . 4 (𝜑 → ∅ ∈ 𝒫 ℝ)
8 ima0 5938 . . . . . 6 (𝐹 “ ∅) = ∅
98a1i 11 . . . . 5 (𝜑 → (𝐹 “ ∅) = ∅)
10 smfresal.s . . . . . . 7 (𝜑𝑆 ∈ SAlg)
1110uniexd 7460 . . . . . . . 8 (𝜑 𝑆 ∈ V)
12 smfresal.f . . . . . . . . 9 (𝜑𝐹 ∈ (SMblFn‘𝑆))
13 smfresal.d . . . . . . . . 9 𝐷 = dom 𝐹
1410, 12, 13smfdmss 42995 . . . . . . . 8 (𝜑𝐷 𝑆)
1511, 14ssexd 5219 . . . . . . 7 (𝜑𝐷 ∈ V)
16 eqid 2819 . . . . . . 7 (𝑆t 𝐷) = (𝑆t 𝐷)
1710, 15, 16subsalsal 42627 . . . . . 6 (𝜑 → (𝑆t 𝐷) ∈ SAlg)
18170sald 42618 . . . . 5 (𝜑 → ∅ ∈ (𝑆t 𝐷))
199, 18eqeltrd 2911 . . . 4 (𝜑 → (𝐹 “ ∅) ∈ (𝑆t 𝐷))
207, 19jca 514 . . 3 (𝜑 → (∅ ∈ 𝒫 ℝ ∧ (𝐹 “ ∅) ∈ (𝑆t 𝐷)))
21 imaeq2 5918 . . . . 5 (𝑒 = ∅ → (𝐹𝑒) = (𝐹 “ ∅))
2221eleq1d 2895 . . . 4 (𝑒 = ∅ → ((𝐹𝑒) ∈ (𝑆t 𝐷) ↔ (𝐹 “ ∅) ∈ (𝑆t 𝐷)))
2322, 1elrab2 3681 . . 3 (∅ ∈ 𝑇 ↔ (∅ ∈ 𝒫 ℝ ∧ (𝐹 “ ∅) ∈ (𝑆t 𝐷)))
2420, 23sylibr 236 . 2 (𝜑 → ∅ ∈ 𝑇)
25 eqid 2819 . 2 𝑇 = 𝑇
26 nfv 1908 . . . . . . 7 𝑦𝜑
27 nfcv 2975 . . . . . . . . . . . . 13 𝑒𝑦
28 nfrab1 3383 . . . . . . . . . . . . . 14 𝑒{𝑒 ∈ 𝒫 ℝ ∣ (𝐹𝑒) ∈ (𝑆t 𝐷)}
291, 28nfcxfr 2973 . . . . . . . . . . . . 13 𝑒𝑇
3027, 29eluni2f 41354 . . . . . . . . . . . 12 (𝑦 𝑇 ↔ ∃𝑒𝑇 𝑦𝑒)
3130biimpi 218 . . . . . . . . . . 11 (𝑦 𝑇 → ∃𝑒𝑇 𝑦𝑒)
3231adantl 484 . . . . . . . . . 10 ((𝜑𝑦 𝑇) → ∃𝑒𝑇 𝑦𝑒)
33 nfv 1908 . . . . . . . . . . . 12 𝑒𝜑
3429nfuni 4837 . . . . . . . . . . . . 13 𝑒 𝑇
3527, 34nfel 2990 . . . . . . . . . . . 12 𝑒 𝑦 𝑇
3633, 35nfan 1893 . . . . . . . . . . 11 𝑒(𝜑𝑦 𝑇)
3727nfel1 2992 . . . . . . . . . . 11 𝑒 𝑦 ∈ ℝ
381eleq2i 2902 . . . . . . . . . . . . . . . . . 18 (𝑒𝑇𝑒 ∈ {𝑒 ∈ 𝒫 ℝ ∣ (𝐹𝑒) ∈ (𝑆t 𝐷)})
3938biimpi 218 . . . . . . . . . . . . . . . . 17 (𝑒𝑇𝑒 ∈ {𝑒 ∈ 𝒫 ℝ ∣ (𝐹𝑒) ∈ (𝑆t 𝐷)})
40 rabidim1 3379 . . . . . . . . . . . . . . . . 17 (𝑒 ∈ {𝑒 ∈ 𝒫 ℝ ∣ (𝐹𝑒) ∈ (𝑆t 𝐷)} → 𝑒 ∈ 𝒫 ℝ)
4139, 40syl 17 . . . . . . . . . . . . . . . 16 (𝑒𝑇𝑒 ∈ 𝒫 ℝ)
42 elpwi 4549 . . . . . . . . . . . . . . . 16 (𝑒 ∈ 𝒫 ℝ → 𝑒 ⊆ ℝ)
4341, 42syl 17 . . . . . . . . . . . . . . 15 (𝑒𝑇𝑒 ⊆ ℝ)
4443adantr 483 . . . . . . . . . . . . . 14 ((𝑒𝑇𝑦𝑒) → 𝑒 ⊆ ℝ)
45 simpr 487 . . . . . . . . . . . . . 14 ((𝑒𝑇𝑦𝑒) → 𝑦𝑒)
4644, 45sseldd 3966 . . . . . . . . . . . . 13 ((𝑒𝑇𝑦𝑒) → 𝑦 ∈ ℝ)
4746ex 415 . . . . . . . . . . . 12 (𝑒𝑇 → (𝑦𝑒𝑦 ∈ ℝ))
4847a1i 11 . . . . . . . . . . 11 ((𝜑𝑦 𝑇) → (𝑒𝑇 → (𝑦𝑒𝑦 ∈ ℝ)))
4936, 37, 48rexlimd 3315 . . . . . . . . . 10 ((𝜑𝑦 𝑇) → (∃𝑒𝑇 𝑦𝑒𝑦 ∈ ℝ))
5032, 49mpd 15 . . . . . . . . 9 ((𝜑𝑦 𝑇) → 𝑦 ∈ ℝ)
5150ex 415 . . . . . . . 8 (𝜑 → (𝑦 𝑇𝑦 ∈ ℝ))
52 ovexd 7183 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑦 − 1)(,)(𝑦 + 1)) ∈ V)
53 ioossre 12790 . . . . . . . . . . . . . . . 16 ((𝑦 − 1)(,)(𝑦 + 1)) ⊆ ℝ
5453a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑦 − 1)(,)(𝑦 + 1)) ⊆ ℝ)
5552, 54elpwd 4548 . . . . . . . . . . . . . 14 (𝜑 → ((𝑦 − 1)(,)(𝑦 + 1)) ∈ 𝒫 ℝ)
5655adantr 483 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ ℝ) → ((𝑦 − 1)(,)(𝑦 + 1)) ∈ 𝒫 ℝ)
5710, 12, 13smff 42994 . . . . . . . . . . . . . . . . 17 (𝜑𝐹:𝐷⟶ℝ)
5857ffnd 6508 . . . . . . . . . . . . . . . 16 (𝜑𝐹 Fn 𝐷)
59 fncnvima2 6824 . . . . . . . . . . . . . . . 16 (𝐹 Fn 𝐷 → (𝐹 “ ((𝑦 − 1)(,)(𝑦 + 1))) = {𝑥𝐷 ∣ (𝐹𝑥) ∈ ((𝑦 − 1)(,)(𝑦 + 1))})
6058, 59syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (𝐹 “ ((𝑦 − 1)(,)(𝑦 + 1))) = {𝑥𝐷 ∣ (𝐹𝑥) ∈ ((𝑦 − 1)(,)(𝑦 + 1))})
6160adantr 483 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ ℝ) → (𝐹 “ ((𝑦 − 1)(,)(𝑦 + 1))) = {𝑥𝐷 ∣ (𝐹𝑥) ∈ ((𝑦 − 1)(,)(𝑦 + 1))})
62 nfv 1908 . . . . . . . . . . . . . . 15 𝑥(𝜑𝑦 ∈ ℝ)
6310adantr 483 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ ℝ) → 𝑆 ∈ SAlg)
6415adantr 483 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ ℝ) → 𝐷 ∈ V)
6557adantr 483 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐷) → 𝐹:𝐷⟶ℝ)
66 simpr 487 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐷) → 𝑥𝐷)
6765, 66ffvelrnd 6845 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝐷) → (𝐹𝑥) ∈ ℝ)
6867adantlr 713 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ℝ) ∧ 𝑥𝐷) → (𝐹𝑥) ∈ ℝ)
6957feqmptd 6726 . . . . . . . . . . . . . . . . . 18 (𝜑𝐹 = (𝑥𝐷 ↦ (𝐹𝑥)))
7069eqcomd 2825 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑥𝐷 ↦ (𝐹𝑥)) = 𝐹)
7170, 12eqeltrd 2911 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑥𝐷 ↦ (𝐹𝑥)) ∈ (SMblFn‘𝑆))
7271adantr 483 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ ℝ) → (𝑥𝐷 ↦ (𝐹𝑥)) ∈ (SMblFn‘𝑆))
73 peano2rem 10945 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℝ → (𝑦 − 1) ∈ ℝ)
7473rexrd 10683 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℝ → (𝑦 − 1) ∈ ℝ*)
7574adantl 484 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ ℝ) → (𝑦 − 1) ∈ ℝ*)
76 peano2re 10805 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℝ → (𝑦 + 1) ∈ ℝ)
7776rexrd 10683 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℝ → (𝑦 + 1) ∈ ℝ*)
7877adantl 484 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ ℝ) → (𝑦 + 1) ∈ ℝ*)
7962, 63, 64, 68, 72, 75, 78smfpimioompt 43046 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ ℝ) → {𝑥𝐷 ∣ (𝐹𝑥) ∈ ((𝑦 − 1)(,)(𝑦 + 1))} ∈ (𝑆t 𝐷))
8061, 79eqeltrd 2911 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ ℝ) → (𝐹 “ ((𝑦 − 1)(,)(𝑦 + 1))) ∈ (𝑆t 𝐷))
8156, 80jca 514 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ ℝ) → (((𝑦 − 1)(,)(𝑦 + 1)) ∈ 𝒫 ℝ ∧ (𝐹 “ ((𝑦 − 1)(,)(𝑦 + 1))) ∈ (𝑆t 𝐷)))
82 imaeq2 5918 . . . . . . . . . . . . . 14 (𝑒 = ((𝑦 − 1)(,)(𝑦 + 1)) → (𝐹𝑒) = (𝐹 “ ((𝑦 − 1)(,)(𝑦 + 1))))
8382eleq1d 2895 . . . . . . . . . . . . 13 (𝑒 = ((𝑦 − 1)(,)(𝑦 + 1)) → ((𝐹𝑒) ∈ (𝑆t 𝐷) ↔ (𝐹 “ ((𝑦 − 1)(,)(𝑦 + 1))) ∈ (𝑆t 𝐷)))
8483, 1elrab2 3681 . . . . . . . . . . . 12 (((𝑦 − 1)(,)(𝑦 + 1)) ∈ 𝑇 ↔ (((𝑦 − 1)(,)(𝑦 + 1)) ∈ 𝒫 ℝ ∧ (𝐹 “ ((𝑦 − 1)(,)(𝑦 + 1))) ∈ (𝑆t 𝐷)))
8581, 84sylibr 236 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ℝ) → ((𝑦 − 1)(,)(𝑦 + 1)) ∈ 𝑇)
86 id 22 . . . . . . . . . . . . 13 (𝑦 ∈ ℝ → 𝑦 ∈ ℝ)
87 ltm1 11474 . . . . . . . . . . . . 13 (𝑦 ∈ ℝ → (𝑦 − 1) < 𝑦)
88 ltp1 11472 . . . . . . . . . . . . 13 (𝑦 ∈ ℝ → 𝑦 < (𝑦 + 1))
8974, 77, 86, 87, 88eliood 41757 . . . . . . . . . . . 12 (𝑦 ∈ ℝ → 𝑦 ∈ ((𝑦 − 1)(,)(𝑦 + 1)))
9089adantl 484 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ℝ) → 𝑦 ∈ ((𝑦 − 1)(,)(𝑦 + 1)))
91 nfv 1908 . . . . . . . . . . . 12 𝑒 𝑦 ∈ ((𝑦 − 1)(,)(𝑦 + 1))
92 nfcv 2975 . . . . . . . . . . . 12 𝑒((𝑦 − 1)(,)(𝑦 + 1))
93 eleq2 2899 . . . . . . . . . . . 12 (𝑒 = ((𝑦 − 1)(,)(𝑦 + 1)) → (𝑦𝑒𝑦 ∈ ((𝑦 − 1)(,)(𝑦 + 1))))
9491, 92, 29, 93rspcef 41319 . . . . . . . . . . 11 ((((𝑦 − 1)(,)(𝑦 + 1)) ∈ 𝑇𝑦 ∈ ((𝑦 − 1)(,)(𝑦 + 1))) → ∃𝑒𝑇 𝑦𝑒)
9585, 90, 94syl2anc 586 . . . . . . . . . 10 ((𝜑𝑦 ∈ ℝ) → ∃𝑒𝑇 𝑦𝑒)
9695, 30sylibr 236 . . . . . . . . 9 ((𝜑𝑦 ∈ ℝ) → 𝑦 𝑇)
9796ex 415 . . . . . . . 8 (𝜑 → (𝑦 ∈ ℝ → 𝑦 𝑇))
9851, 97impbid 214 . . . . . . 7 (𝜑 → (𝑦 𝑇𝑦 ∈ ℝ))
9926, 98alrimi 2205 . . . . . 6 (𝜑 → ∀𝑦(𝑦 𝑇𝑦 ∈ ℝ))
100 dfcleq 2813 . . . . . 6 ( 𝑇 = ℝ ↔ ∀𝑦(𝑦 𝑇𝑦 ∈ ℝ))
10199, 100sylibr 236 . . . . 5 (𝜑 𝑇 = ℝ)
102101difeq1d 4096 . . . 4 (𝜑 → ( 𝑇𝑥) = (ℝ ∖ 𝑥))
103102adantr 483 . . 3 ((𝜑𝑥𝑇) → ( 𝑇𝑥) = (ℝ ∖ 𝑥))
104 difss 4106 . . . . . . 7 (ℝ ∖ 𝑥) ⊆ ℝ
1052, 104ssexi 5217 . . . . . . . 8 (ℝ ∖ 𝑥) ∈ V
106 elpwg 4543 . . . . . . . 8 ((ℝ ∖ 𝑥) ∈ V → ((ℝ ∖ 𝑥) ∈ 𝒫 ℝ ↔ (ℝ ∖ 𝑥) ⊆ ℝ))
107105, 106ax-mp 5 . . . . . . 7 ((ℝ ∖ 𝑥) ∈ 𝒫 ℝ ↔ (ℝ ∖ 𝑥) ⊆ ℝ)
108104, 107mpbir 233 . . . . . 6 (ℝ ∖ 𝑥) ∈ 𝒫 ℝ
109108a1i 11 . . . . 5 ((𝜑𝑥𝑇) → (ℝ ∖ 𝑥) ∈ 𝒫 ℝ)
11057ffund 6511 . . . . . . . . 9 (𝜑 → Fun 𝐹)
111 difpreima 6828 . . . . . . . . 9 (Fun 𝐹 → (𝐹 “ (ℝ ∖ 𝑥)) = ((𝐹 “ ℝ) ∖ (𝐹𝑥)))
112110, 111syl 17 . . . . . . . 8 (𝜑 → (𝐹 “ (ℝ ∖ 𝑥)) = ((𝐹 “ ℝ) ∖ (𝐹𝑥)))
113 fimacnv 6832 . . . . . . . . . . 11 (𝐹:𝐷⟶ℝ → (𝐹 “ ℝ) = 𝐷)
11457, 113syl 17 . . . . . . . . . 10 (𝜑 → (𝐹 “ ℝ) = 𝐷)
11510, 14restuni4 41372 . . . . . . . . . 10 (𝜑 (𝑆t 𝐷) = 𝐷)
116114, 115eqtr4d 2857 . . . . . . . . 9 (𝜑 → (𝐹 “ ℝ) = (𝑆t 𝐷))
117116difeq1d 4096 . . . . . . . 8 (𝜑 → ((𝐹 “ ℝ) ∖ (𝐹𝑥)) = ( (𝑆t 𝐷) ∖ (𝐹𝑥)))
118112, 117eqtrd 2854 . . . . . . 7 (𝜑 → (𝐹 “ (ℝ ∖ 𝑥)) = ( (𝑆t 𝐷) ∖ (𝐹𝑥)))
119118adantr 483 . . . . . 6 ((𝜑𝑥𝑇) → (𝐹 “ (ℝ ∖ 𝑥)) = ( (𝑆t 𝐷) ∖ (𝐹𝑥)))
12017adantr 483 . . . . . . 7 ((𝜑𝑥𝑇) → (𝑆t 𝐷) ∈ SAlg)
121 imaeq2 5918 . . . . . . . . . . . 12 (𝑒 = 𝑥 → (𝐹𝑒) = (𝐹𝑥))
122121eleq1d 2895 . . . . . . . . . . 11 (𝑒 = 𝑥 → ((𝐹𝑒) ∈ (𝑆t 𝐷) ↔ (𝐹𝑥) ∈ (𝑆t 𝐷)))
123122, 1elrab2 3681 . . . . . . . . . 10 (𝑥𝑇 ↔ (𝑥 ∈ 𝒫 ℝ ∧ (𝐹𝑥) ∈ (𝑆t 𝐷)))
124123biimpi 218 . . . . . . . . 9 (𝑥𝑇 → (𝑥 ∈ 𝒫 ℝ ∧ (𝐹𝑥) ∈ (𝑆t 𝐷)))
125124simprd 498 . . . . . . . 8 (𝑥𝑇 → (𝐹𝑥) ∈ (𝑆t 𝐷))
126125adantl 484 . . . . . . 7 ((𝜑𝑥𝑇) → (𝐹𝑥) ∈ (𝑆t 𝐷))
127120, 126saldifcld 42615 . . . . . 6 ((𝜑𝑥𝑇) → ( (𝑆t 𝐷) ∖ (𝐹𝑥)) ∈ (𝑆t 𝐷))
128119, 127eqeltrd 2911 . . . . 5 ((𝜑𝑥𝑇) → (𝐹 “ (ℝ ∖ 𝑥)) ∈ (𝑆t 𝐷))
129109, 128jca 514 . . . 4 ((𝜑𝑥𝑇) → ((ℝ ∖ 𝑥) ∈ 𝒫 ℝ ∧ (𝐹 “ (ℝ ∖ 𝑥)) ∈ (𝑆t 𝐷)))
130 imaeq2 5918 . . . . . 6 (𝑒 = (ℝ ∖ 𝑥) → (𝐹𝑒) = (𝐹 “ (ℝ ∖ 𝑥)))
131130eleq1d 2895 . . . . 5 (𝑒 = (ℝ ∖ 𝑥) → ((𝐹𝑒) ∈ (𝑆t 𝐷) ↔ (𝐹 “ (ℝ ∖ 𝑥)) ∈ (𝑆t 𝐷)))
132131, 1elrab2 3681 . . . 4 ((ℝ ∖ 𝑥) ∈ 𝑇 ↔ ((ℝ ∖ 𝑥) ∈ 𝒫 ℝ ∧ (𝐹 “ (ℝ ∖ 𝑥)) ∈ (𝑆t 𝐷)))
133129, 132sylibr 236 . . 3 ((𝜑𝑥𝑇) → (ℝ ∖ 𝑥) ∈ 𝑇)
134103, 133eqeltrd 2911 . 2 ((𝜑𝑥𝑇) → ( 𝑇𝑥) ∈ 𝑇)
135 nnex 11636 . . . . . . . 8 ℕ ∈ V
136 fvex 6676 . . . . . . . 8 (𝑔𝑛) ∈ V
137135, 136iunex 7661 . . . . . . 7 𝑛 ∈ ℕ (𝑔𝑛) ∈ V
138137a1i 11 . . . . . 6 (𝑔:ℕ⟶𝑇 𝑛 ∈ ℕ (𝑔𝑛) ∈ V)
139 ffvelrn 6842 . . . . . . . 8 ((𝑔:ℕ⟶𝑇𝑛 ∈ ℕ) → (𝑔𝑛) ∈ 𝑇)
1401eleq2i 2902 . . . . . . . . . . 11 ((𝑔𝑛) ∈ 𝑇 ↔ (𝑔𝑛) ∈ {𝑒 ∈ 𝒫 ℝ ∣ (𝐹𝑒) ∈ (𝑆t 𝐷)})
141140biimpi 218 . . . . . . . . . 10 ((𝑔𝑛) ∈ 𝑇 → (𝑔𝑛) ∈ {𝑒 ∈ 𝒫 ℝ ∣ (𝐹𝑒) ∈ (𝑆t 𝐷)})
142 elrabi 3673 . . . . . . . . . 10 ((𝑔𝑛) ∈ {𝑒 ∈ 𝒫 ℝ ∣ (𝐹𝑒) ∈ (𝑆t 𝐷)} → (𝑔𝑛) ∈ 𝒫 ℝ)
143141, 142syl 17 . . . . . . . . 9 ((𝑔𝑛) ∈ 𝑇 → (𝑔𝑛) ∈ 𝒫 ℝ)
144 elpwi 4549 . . . . . . . . 9 ((𝑔𝑛) ∈ 𝒫 ℝ → (𝑔𝑛) ⊆ ℝ)
145143, 144syl 17 . . . . . . . 8 ((𝑔𝑛) ∈ 𝑇 → (𝑔𝑛) ⊆ ℝ)
146139, 145syl 17 . . . . . . 7 ((𝑔:ℕ⟶𝑇𝑛 ∈ ℕ) → (𝑔𝑛) ⊆ ℝ)
147146iunssd 4965 . . . . . 6 (𝑔:ℕ⟶𝑇 𝑛 ∈ ℕ (𝑔𝑛) ⊆ ℝ)
148138, 147elpwd 4548 . . . . 5 (𝑔:ℕ⟶𝑇 𝑛 ∈ ℕ (𝑔𝑛) ∈ 𝒫 ℝ)
149148adantl 484 . . . 4 ((𝜑𝑔:ℕ⟶𝑇) → 𝑛 ∈ ℕ (𝑔𝑛) ∈ 𝒫 ℝ)
150 imaiun 6996 . . . . . 6 (𝐹 𝑛 ∈ ℕ (𝑔𝑛)) = 𝑛 ∈ ℕ (𝐹 “ (𝑔𝑛))
151150a1i 11 . . . . 5 ((𝜑𝑔:ℕ⟶𝑇) → (𝐹 𝑛 ∈ ℕ (𝑔𝑛)) = 𝑛 ∈ ℕ (𝐹 “ (𝑔𝑛)))
15217adantr 483 . . . . . 6 ((𝜑𝑔:ℕ⟶𝑇) → (𝑆t 𝐷) ∈ SAlg)
153 nnct 13341 . . . . . . 7 ℕ ≼ ω
154153a1i 11 . . . . . 6 ((𝜑𝑔:ℕ⟶𝑇) → ℕ ≼ ω)
155 imaeq2 5918 . . . . . . . . . . . 12 (𝑒 = (𝑔𝑛) → (𝐹𝑒) = (𝐹 “ (𝑔𝑛)))
156155eleq1d 2895 . . . . . . . . . . 11 (𝑒 = (𝑔𝑛) → ((𝐹𝑒) ∈ (𝑆t 𝐷) ↔ (𝐹 “ (𝑔𝑛)) ∈ (𝑆t 𝐷)))
157156, 1elrab2 3681 . . . . . . . . . 10 ((𝑔𝑛) ∈ 𝑇 ↔ ((𝑔𝑛) ∈ 𝒫 ℝ ∧ (𝐹 “ (𝑔𝑛)) ∈ (𝑆t 𝐷)))
158157biimpi 218 . . . . . . . . 9 ((𝑔𝑛) ∈ 𝑇 → ((𝑔𝑛) ∈ 𝒫 ℝ ∧ (𝐹 “ (𝑔𝑛)) ∈ (𝑆t 𝐷)))
159158simprd 498 . . . . . . . 8 ((𝑔𝑛) ∈ 𝑇 → (𝐹 “ (𝑔𝑛)) ∈ (𝑆t 𝐷))
160139, 159syl 17 . . . . . . 7 ((𝑔:ℕ⟶𝑇𝑛 ∈ ℕ) → (𝐹 “ (𝑔𝑛)) ∈ (𝑆t 𝐷))
161160adantll 712 . . . . . 6 (((𝜑𝑔:ℕ⟶𝑇) ∧ 𝑛 ∈ ℕ) → (𝐹 “ (𝑔𝑛)) ∈ (𝑆t 𝐷))
162152, 154, 161saliuncl 42592 . . . . 5 ((𝜑𝑔:ℕ⟶𝑇) → 𝑛 ∈ ℕ (𝐹 “ (𝑔𝑛)) ∈ (𝑆t 𝐷))
163151, 162eqeltrd 2911 . . . 4 ((𝜑𝑔:ℕ⟶𝑇) → (𝐹 𝑛 ∈ ℕ (𝑔𝑛)) ∈ (𝑆t 𝐷))
164149, 163jca 514 . . 3 ((𝜑𝑔:ℕ⟶𝑇) → ( 𝑛 ∈ ℕ (𝑔𝑛) ∈ 𝒫 ℝ ∧ (𝐹 𝑛 ∈ ℕ (𝑔𝑛)) ∈ (𝑆t 𝐷)))
165 imaeq2 5918 . . . . 5 (𝑒 = 𝑛 ∈ ℕ (𝑔𝑛) → (𝐹𝑒) = (𝐹 𝑛 ∈ ℕ (𝑔𝑛)))
166165eleq1d 2895 . . . 4 (𝑒 = 𝑛 ∈ ℕ (𝑔𝑛) → ((𝐹𝑒) ∈ (𝑆t 𝐷) ↔ (𝐹 𝑛 ∈ ℕ (𝑔𝑛)) ∈ (𝑆t 𝐷)))
167166, 1elrab2 3681 . . 3 ( 𝑛 ∈ ℕ (𝑔𝑛) ∈ 𝑇 ↔ ( 𝑛 ∈ ℕ (𝑔𝑛) ∈ 𝒫 ℝ ∧ (𝐹 𝑛 ∈ ℕ (𝑔𝑛)) ∈ (𝑆t 𝐷)))
168164, 167sylibr 236 . 2 ((𝜑𝑔:ℕ⟶𝑇) → 𝑛 ∈ ℕ (𝑔𝑛) ∈ 𝑇)
1695, 24, 25, 134, 168issalnnd 42613 1 (𝜑𝑇 ∈ SAlg)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 208  wa 398  wal 1528   = wceq 1530  wcel 2107  wrex 3137  {crab 3140  Vcvv 3493  cdif 3931  wss 3934  c0 4289  𝒫 cpw 4537   cuni 4830   ciun 4910   class class class wbr 5057  cmpt 5137  ccnv 5547  dom cdm 5548  cima 5551  Fun wfun 6342   Fn wfn 6343  wf 6344  cfv 6348  (class class class)co 7148  ωcom 7572  cdom 8499  cr 10528  1c1 10530   + caddc 10532  *cxr 10666  cmin 10862  cn 11630  (,)cioo 12730  t crest 16686  SAlgcsalg 42578  SMblFncsmblfn 42962
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2791  ax-rep 5181  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7453  ax-inf2 9096  ax-cc 9849  ax-ac2 9877  ax-cnex 10585  ax-resscn 10586  ax-1cn 10587  ax-icn 10588  ax-addcl 10589  ax-addrcl 10590  ax-mulcl 10591  ax-mulrcl 10592  ax-mulcom 10593  ax-addass 10594  ax-mulass 10595  ax-distr 10596  ax-i2m1 10597  ax-1ne0 10598  ax-1rid 10599  ax-rnegex 10600  ax-rrecex 10601  ax-cnre 10602  ax-pre-lttri 10603  ax-pre-lttrn 10604  ax-pre-ltadd 10605  ax-pre-mulgt0 10606  ax-pre-sup 10607
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ne 3015  df-nel 3122  df-ral 3141  df-rex 3142  df-reu 3143  df-rmo 3144  df-rab 3145  df-v 3495  df-sbc 3771  df-csb 3882  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-pss 3952  df-nul 4290  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-tp 4564  df-op 4566  df-uni 4831  df-int 4868  df-iun 4912  df-iin 4913  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-se 5508  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-isom 6357  df-riota 7106  df-ov 7151  df-oprab 7152  df-mpo 7153  df-om 7573  df-1st 7681  df-2nd 7682  df-wrecs 7939  df-recs 8000  df-rdg 8038  df-1o 8094  df-oadd 8098  df-er 8281  df-map 8400  df-pm 8401  df-en 8502  df-dom 8503  df-sdom 8504  df-fin 8505  df-sup 8898  df-inf 8899  df-card 9360  df-acn 9363  df-ac 9534  df-pnf 10669  df-mnf 10670  df-xr 10671  df-ltxr 10672  df-le 10673  df-sub 10864  df-neg 10865  df-div 11290  df-nn 11631  df-n0 11890  df-z 11974  df-uz 12236  df-q 12341  df-rp 12382  df-ioo 12734  df-ico 12736  df-fl 13154  df-rest 16688  df-salg 42579  df-smblfn 42963
This theorem is referenced by:  smfpimbor1lem1  43058  smfpimbor1lem2  43059
  Copyright terms: Public domain W3C validator