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 41904
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 10363 . . . . 5 ℝ ∈ V
32pwex 5092 . . . 4 𝒫 ℝ ∈ V
41, 3rabex2 5051 . . 3 𝑇 ∈ V
54a1i 11 . 2 (𝜑𝑇 ∈ V)
6 0elpw 5068 . . . . 5 ∅ ∈ 𝒫 ℝ
76a1i 11 . . . 4 (𝜑 → ∅ ∈ 𝒫 ℝ)
8 ima0 5735 . . . . . 6 (𝐹 “ ∅) = ∅
98a1i 11 . . . . 5 (𝜑 → (𝐹 “ ∅) = ∅)
10 smfresal.s . . . . . . 7 (𝜑𝑆 ∈ SAlg)
1110uniexd 40194 . . . . . . . 8 (𝜑 𝑆 ∈ V)
12 smfresal.f . . . . . . . . 9 (𝜑𝐹 ∈ (SMblFn‘𝑆))
13 smfresal.d . . . . . . . . 9 𝐷 = dom 𝐹
1410, 12, 13smfdmss 41851 . . . . . . . 8 (𝜑𝐷 𝑆)
1511, 14ssexd 5042 . . . . . . 7 (𝜑𝐷 ∈ V)
16 eqid 2777 . . . . . . 7 (𝑆t 𝐷) = (𝑆t 𝐷)
1710, 15, 16subsalsal 41483 . . . . . 6 (𝜑 → (𝑆t 𝐷) ∈ SAlg)
18170sald 41474 . . . . 5 (𝜑 → ∅ ∈ (𝑆t 𝐷))
199, 18eqeltrd 2858 . . . 4 (𝜑 → (𝐹 “ ∅) ∈ (𝑆t 𝐷))
207, 19jca 507 . . 3 (𝜑 → (∅ ∈ 𝒫 ℝ ∧ (𝐹 “ ∅) ∈ (𝑆t 𝐷)))
21 imaeq2 5716 . . . . 5 (𝑒 = ∅ → (𝐹𝑒) = (𝐹 “ ∅))
2221eleq1d 2843 . . . 4 (𝑒 = ∅ → ((𝐹𝑒) ∈ (𝑆t 𝐷) ↔ (𝐹 “ ∅) ∈ (𝑆t 𝐷)))
2322, 1elrab2 3575 . . 3 (∅ ∈ 𝑇 ↔ (∅ ∈ 𝒫 ℝ ∧ (𝐹 “ ∅) ∈ (𝑆t 𝐷)))
2420, 23sylibr 226 . 2 (𝜑 → ∅ ∈ 𝑇)
25 eqid 2777 . 2 𝑇 = 𝑇
26 nfv 1957 . . . . . . 7 𝑦𝜑
27 nfcv 2933 . . . . . . . . . . . . 13 𝑒𝑦
28 nfrab1 3308 . . . . . . . . . . . . . 14 𝑒{𝑒 ∈ 𝒫 ℝ ∣ (𝐹𝑒) ∈ (𝑆t 𝐷)}
291, 28nfcxfr 2931 . . . . . . . . . . . . 13 𝑒𝑇
3027, 29eluni2f 40197 . . . . . . . . . . . 12 (𝑦 𝑇 ↔ ∃𝑒𝑇 𝑦𝑒)
3130biimpi 208 . . . . . . . . . . 11 (𝑦 𝑇 → ∃𝑒𝑇 𝑦𝑒)
3231adantl 475 . . . . . . . . . 10 ((𝜑𝑦 𝑇) → ∃𝑒𝑇 𝑦𝑒)
33 nfv 1957 . . . . . . . . . . . 12 𝑒𝜑
3429nfuni 4677 . . . . . . . . . . . . 13 𝑒 𝑇
3527, 34nfel 2945 . . . . . . . . . . . 12 𝑒 𝑦 𝑇
3633, 35nfan 1946 . . . . . . . . . . 11 𝑒(𝜑𝑦 𝑇)
3727nfel1 2947 . . . . . . . . . . 11 𝑒 𝑦 ∈ ℝ
381eleq2i 2850 . . . . . . . . . . . . . . . . . 18 (𝑒𝑇𝑒 ∈ {𝑒 ∈ 𝒫 ℝ ∣ (𝐹𝑒) ∈ (𝑆t 𝐷)})
3938biimpi 208 . . . . . . . . . . . . . . . . 17 (𝑒𝑇𝑒 ∈ {𝑒 ∈ 𝒫 ℝ ∣ (𝐹𝑒) ∈ (𝑆t 𝐷)})
40 rabidim1 3303 . . . . . . . . . . . . . . . . 17 (𝑒 ∈ {𝑒 ∈ 𝒫 ℝ ∣ (𝐹𝑒) ∈ (𝑆t 𝐷)} → 𝑒 ∈ 𝒫 ℝ)
4139, 40syl 17 . . . . . . . . . . . . . . . 16 (𝑒𝑇𝑒 ∈ 𝒫 ℝ)
42 elpwi 4388 . . . . . . . . . . . . . . . 16 (𝑒 ∈ 𝒫 ℝ → 𝑒 ⊆ ℝ)
4341, 42syl 17 . . . . . . . . . . . . . . 15 (𝑒𝑇𝑒 ⊆ ℝ)
4443adantr 474 . . . . . . . . . . . . . 14 ((𝑒𝑇𝑦𝑒) → 𝑒 ⊆ ℝ)
45 simpr 479 . . . . . . . . . . . . . 14 ((𝑒𝑇𝑦𝑒) → 𝑦𝑒)
4644, 45sseldd 3821 . . . . . . . . . . . . 13 ((𝑒𝑇𝑦𝑒) → 𝑦 ∈ ℝ)
4746ex 403 . . . . . . . . . . . 12 (𝑒𝑇 → (𝑦𝑒𝑦 ∈ ℝ))
4847a1i 11 . . . . . . . . . . 11 ((𝜑𝑦 𝑇) → (𝑒𝑇 → (𝑦𝑒𝑦 ∈ ℝ)))
4936, 37, 48rexlimd 3207 . . . . . . . . . 10 ((𝜑𝑦 𝑇) → (∃𝑒𝑇 𝑦𝑒𝑦 ∈ ℝ))
5032, 49mpd 15 . . . . . . . . 9 ((𝜑𝑦 𝑇) → 𝑦 ∈ ℝ)
5150ex 403 . . . . . . . 8 (𝜑 → (𝑦 𝑇𝑦 ∈ ℝ))
52 ovexd 6956 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑦 − 1)(,)(𝑦 + 1)) ∈ V)
53 ioossre 12547 . . . . . . . . . . . . . . . 16 ((𝑦 − 1)(,)(𝑦 + 1)) ⊆ ℝ
5453a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑦 − 1)(,)(𝑦 + 1)) ⊆ ℝ)
5552, 54elpwd 4387 . . . . . . . . . . . . . 14 (𝜑 → ((𝑦 − 1)(,)(𝑦 + 1)) ∈ 𝒫 ℝ)
5655adantr 474 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ ℝ) → ((𝑦 − 1)(,)(𝑦 + 1)) ∈ 𝒫 ℝ)
5710, 12, 13smff 41850 . . . . . . . . . . . . . . . . 17 (𝜑𝐹:𝐷⟶ℝ)
5857ffnd 6292 . . . . . . . . . . . . . . . 16 (𝜑𝐹 Fn 𝐷)
59 fncnvima2 6603 . . . . . . . . . . . . . . . 16 (𝐹 Fn 𝐷 → (𝐹 “ ((𝑦 − 1)(,)(𝑦 + 1))) = {𝑥𝐷 ∣ (𝐹𝑥) ∈ ((𝑦 − 1)(,)(𝑦 + 1))})
6058, 59syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (𝐹 “ ((𝑦 − 1)(,)(𝑦 + 1))) = {𝑥𝐷 ∣ (𝐹𝑥) ∈ ((𝑦 − 1)(,)(𝑦 + 1))})
6160adantr 474 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ ℝ) → (𝐹 “ ((𝑦 − 1)(,)(𝑦 + 1))) = {𝑥𝐷 ∣ (𝐹𝑥) ∈ ((𝑦 − 1)(,)(𝑦 + 1))})
62 nfv 1957 . . . . . . . . . . . . . . 15 𝑥(𝜑𝑦 ∈ ℝ)
6310adantr 474 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ ℝ) → 𝑆 ∈ SAlg)
6415adantr 474 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ ℝ) → 𝐷 ∈ V)
6557adantr 474 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐷) → 𝐹:𝐷⟶ℝ)
66 simpr 479 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥𝐷) → 𝑥𝐷)
6765, 66ffvelrnd 6624 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝐷) → (𝐹𝑥) ∈ ℝ)
6867adantlr 705 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ℝ) ∧ 𝑥𝐷) → (𝐹𝑥) ∈ ℝ)
6957feqmptd 6509 . . . . . . . . . . . . . . . . . 18 (𝜑𝐹 = (𝑥𝐷 ↦ (𝐹𝑥)))
7069eqcomd 2783 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑥𝐷 ↦ (𝐹𝑥)) = 𝐹)
7170, 12eqeltrd 2858 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑥𝐷 ↦ (𝐹𝑥)) ∈ (SMblFn‘𝑆))
7271adantr 474 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ ℝ) → (𝑥𝐷 ↦ (𝐹𝑥)) ∈ (SMblFn‘𝑆))
73 peano2rem 10690 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℝ → (𝑦 − 1) ∈ ℝ)
7473rexrd 10426 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℝ → (𝑦 − 1) ∈ ℝ*)
7574adantl 475 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ ℝ) → (𝑦 − 1) ∈ ℝ*)
76 peano2re 10549 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℝ → (𝑦 + 1) ∈ ℝ)
7776rexrd 10426 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℝ → (𝑦 + 1) ∈ ℝ*)
7877adantl 475 . . . . . . . . . . . . . . 15 ((𝜑𝑦 ∈ ℝ) → (𝑦 + 1) ∈ ℝ*)
7962, 63, 64, 68, 72, 75, 78smfpimioompt 41902 . . . . . . . . . . . . . 14 ((𝜑𝑦 ∈ ℝ) → {𝑥𝐷 ∣ (𝐹𝑥) ∈ ((𝑦 − 1)(,)(𝑦 + 1))} ∈ (𝑆t 𝐷))
8061, 79eqeltrd 2858 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ ℝ) → (𝐹 “ ((𝑦 − 1)(,)(𝑦 + 1))) ∈ (𝑆t 𝐷))
8156, 80jca 507 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ ℝ) → (((𝑦 − 1)(,)(𝑦 + 1)) ∈ 𝒫 ℝ ∧ (𝐹 “ ((𝑦 − 1)(,)(𝑦 + 1))) ∈ (𝑆t 𝐷)))
82 imaeq2 5716 . . . . . . . . . . . . . 14 (𝑒 = ((𝑦 − 1)(,)(𝑦 + 1)) → (𝐹𝑒) = (𝐹 “ ((𝑦 − 1)(,)(𝑦 + 1))))
8382eleq1d 2843 . . . . . . . . . . . . 13 (𝑒 = ((𝑦 − 1)(,)(𝑦 + 1)) → ((𝐹𝑒) ∈ (𝑆t 𝐷) ↔ (𝐹 “ ((𝑦 − 1)(,)(𝑦 + 1))) ∈ (𝑆t 𝐷)))
8483, 1elrab2 3575 . . . . . . . . . . . 12 (((𝑦 − 1)(,)(𝑦 + 1)) ∈ 𝑇 ↔ (((𝑦 − 1)(,)(𝑦 + 1)) ∈ 𝒫 ℝ ∧ (𝐹 “ ((𝑦 − 1)(,)(𝑦 + 1))) ∈ (𝑆t 𝐷)))
8581, 84sylibr 226 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ℝ) → ((𝑦 − 1)(,)(𝑦 + 1)) ∈ 𝑇)
86 id 22 . . . . . . . . . . . . 13 (𝑦 ∈ ℝ → 𝑦 ∈ ℝ)
87 ltm1 11217 . . . . . . . . . . . . 13 (𝑦 ∈ ℝ → (𝑦 − 1) < 𝑦)
88 ltp1 11215 . . . . . . . . . . . . 13 (𝑦 ∈ ℝ → 𝑦 < (𝑦 + 1))
8974, 77, 86, 87, 88eliood 40614 . . . . . . . . . . . 12 (𝑦 ∈ ℝ → 𝑦 ∈ ((𝑦 − 1)(,)(𝑦 + 1)))
9089adantl 475 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ℝ) → 𝑦 ∈ ((𝑦 − 1)(,)(𝑦 + 1)))
91 nfv 1957 . . . . . . . . . . . 12 𝑒 𝑦 ∈ ((𝑦 − 1)(,)(𝑦 + 1))
92 nfcv 2933 . . . . . . . . . . . 12 𝑒((𝑦 − 1)(,)(𝑦 + 1))
93 eleq2 2847 . . . . . . . . . . . 12 (𝑒 = ((𝑦 − 1)(,)(𝑦 + 1)) → (𝑦𝑒𝑦 ∈ ((𝑦 − 1)(,)(𝑦 + 1))))
9491, 92, 29, 93rspcef 40154 . . . . . . . . . . 11 ((((𝑦 − 1)(,)(𝑦 + 1)) ∈ 𝑇𝑦 ∈ ((𝑦 − 1)(,)(𝑦 + 1))) → ∃𝑒𝑇 𝑦𝑒)
9585, 90, 94syl2anc 579 . . . . . . . . . 10 ((𝜑𝑦 ∈ ℝ) → ∃𝑒𝑇 𝑦𝑒)
9695, 30sylibr 226 . . . . . . . . 9 ((𝜑𝑦 ∈ ℝ) → 𝑦 𝑇)
9796ex 403 . . . . . . . 8 (𝜑 → (𝑦 ∈ ℝ → 𝑦 𝑇))
9851, 97impbid 204 . . . . . . 7 (𝜑 → (𝑦 𝑇𝑦 ∈ ℝ))
9926, 98alrimi 2198 . . . . . 6 (𝜑 → ∀𝑦(𝑦 𝑇𝑦 ∈ ℝ))
100 dfcleq 2770 . . . . . 6 ( 𝑇 = ℝ ↔ ∀𝑦(𝑦 𝑇𝑦 ∈ ℝ))
10199, 100sylibr 226 . . . . 5 (𝜑 𝑇 = ℝ)
102101difeq1d 3949 . . . 4 (𝜑 → ( 𝑇𝑥) = (ℝ ∖ 𝑥))
103102adantr 474 . . 3 ((𝜑𝑥𝑇) → ( 𝑇𝑥) = (ℝ ∖ 𝑥))
104 difss 3959 . . . . . . 7 (ℝ ∖ 𝑥) ⊆ ℝ
1052, 104ssexi 5040 . . . . . . . 8 (ℝ ∖ 𝑥) ∈ V
106 elpwg 4386 . . . . . . . 8 ((ℝ ∖ 𝑥) ∈ V → ((ℝ ∖ 𝑥) ∈ 𝒫 ℝ ↔ (ℝ ∖ 𝑥) ⊆ ℝ))
107105, 106ax-mp 5 . . . . . . 7 ((ℝ ∖ 𝑥) ∈ 𝒫 ℝ ↔ (ℝ ∖ 𝑥) ⊆ ℝ)
108104, 107mpbir 223 . . . . . 6 (ℝ ∖ 𝑥) ∈ 𝒫 ℝ
109108a1i 11 . . . . 5 ((𝜑𝑥𝑇) → (ℝ ∖ 𝑥) ∈ 𝒫 ℝ)
11057ffund 6295 . . . . . . . . 9 (𝜑 → Fun 𝐹)
111 difpreima 6607 . . . . . . . . 9 (Fun 𝐹 → (𝐹 “ (ℝ ∖ 𝑥)) = ((𝐹 “ ℝ) ∖ (𝐹𝑥)))
112110, 111syl 17 . . . . . . . 8 (𝜑 → (𝐹 “ (ℝ ∖ 𝑥)) = ((𝐹 “ ℝ) ∖ (𝐹𝑥)))
113 fimacnv 6611 . . . . . . . . . . 11 (𝐹:𝐷⟶ℝ → (𝐹 “ ℝ) = 𝐷)
11457, 113syl 17 . . . . . . . . . 10 (𝜑 → (𝐹 “ ℝ) = 𝐷)
11510, 14restuni4 40215 . . . . . . . . . 10 (𝜑 (𝑆t 𝐷) = 𝐷)
116114, 115eqtr4d 2816 . . . . . . . . 9 (𝜑 → (𝐹 “ ℝ) = (𝑆t 𝐷))
117116difeq1d 3949 . . . . . . . 8 (𝜑 → ((𝐹 “ ℝ) ∖ (𝐹𝑥)) = ( (𝑆t 𝐷) ∖ (𝐹𝑥)))
118112, 117eqtrd 2813 . . . . . . 7 (𝜑 → (𝐹 “ (ℝ ∖ 𝑥)) = ( (𝑆t 𝐷) ∖ (𝐹𝑥)))
119118adantr 474 . . . . . 6 ((𝜑𝑥𝑇) → (𝐹 “ (ℝ ∖ 𝑥)) = ( (𝑆t 𝐷) ∖ (𝐹𝑥)))
12017adantr 474 . . . . . . 7 ((𝜑𝑥𝑇) → (𝑆t 𝐷) ∈ SAlg)
121 imaeq2 5716 . . . . . . . . . . . 12 (𝑒 = 𝑥 → (𝐹𝑒) = (𝐹𝑥))
122121eleq1d 2843 . . . . . . . . . . 11 (𝑒 = 𝑥 → ((𝐹𝑒) ∈ (𝑆t 𝐷) ↔ (𝐹𝑥) ∈ (𝑆t 𝐷)))
123122, 1elrab2 3575 . . . . . . . . . 10 (𝑥𝑇 ↔ (𝑥 ∈ 𝒫 ℝ ∧ (𝐹𝑥) ∈ (𝑆t 𝐷)))
124123biimpi 208 . . . . . . . . 9 (𝑥𝑇 → (𝑥 ∈ 𝒫 ℝ ∧ (𝐹𝑥) ∈ (𝑆t 𝐷)))
125124simprd 491 . . . . . . . 8 (𝑥𝑇 → (𝐹𝑥) ∈ (𝑆t 𝐷))
126125adantl 475 . . . . . . 7 ((𝜑𝑥𝑇) → (𝐹𝑥) ∈ (𝑆t 𝐷))
127120, 126saldifcld 41471 . . . . . 6 ((𝜑𝑥𝑇) → ( (𝑆t 𝐷) ∖ (𝐹𝑥)) ∈ (𝑆t 𝐷))
128119, 127eqeltrd 2858 . . . . 5 ((𝜑𝑥𝑇) → (𝐹 “ (ℝ ∖ 𝑥)) ∈ (𝑆t 𝐷))
129109, 128jca 507 . . . 4 ((𝜑𝑥𝑇) → ((ℝ ∖ 𝑥) ∈ 𝒫 ℝ ∧ (𝐹 “ (ℝ ∖ 𝑥)) ∈ (𝑆t 𝐷)))
130 imaeq2 5716 . . . . . 6 (𝑒 = (ℝ ∖ 𝑥) → (𝐹𝑒) = (𝐹 “ (ℝ ∖ 𝑥)))
131130eleq1d 2843 . . . . 5 (𝑒 = (ℝ ∖ 𝑥) → ((𝐹𝑒) ∈ (𝑆t 𝐷) ↔ (𝐹 “ (ℝ ∖ 𝑥)) ∈ (𝑆t 𝐷)))
132131, 1elrab2 3575 . . . 4 ((ℝ ∖ 𝑥) ∈ 𝑇 ↔ ((ℝ ∖ 𝑥) ∈ 𝒫 ℝ ∧ (𝐹 “ (ℝ ∖ 𝑥)) ∈ (𝑆t 𝐷)))
133129, 132sylibr 226 . . 3 ((𝜑𝑥𝑇) → (ℝ ∖ 𝑥) ∈ 𝑇)
134103, 133eqeltrd 2858 . 2 ((𝜑𝑥𝑇) → ( 𝑇𝑥) ∈ 𝑇)
135 nnex 11381 . . . . . . . 8 ℕ ∈ V
136 fvex 6459 . . . . . . . 8 (𝑔𝑛) ∈ V
137135, 136iunex 7425 . . . . . . 7 𝑛 ∈ ℕ (𝑔𝑛) ∈ V
138137a1i 11 . . . . . 6 (𝑔:ℕ⟶𝑇 𝑛 ∈ ℕ (𝑔𝑛) ∈ V)
139 ffvelrn 6621 . . . . . . . 8 ((𝑔:ℕ⟶𝑇𝑛 ∈ ℕ) → (𝑔𝑛) ∈ 𝑇)
1401eleq2i 2850 . . . . . . . . . . 11 ((𝑔𝑛) ∈ 𝑇 ↔ (𝑔𝑛) ∈ {𝑒 ∈ 𝒫 ℝ ∣ (𝐹𝑒) ∈ (𝑆t 𝐷)})
141140biimpi 208 . . . . . . . . . 10 ((𝑔𝑛) ∈ 𝑇 → (𝑔𝑛) ∈ {𝑒 ∈ 𝒫 ℝ ∣ (𝐹𝑒) ∈ (𝑆t 𝐷)})
142 elrabi 3566 . . . . . . . . . 10 ((𝑔𝑛) ∈ {𝑒 ∈ 𝒫 ℝ ∣ (𝐹𝑒) ∈ (𝑆t 𝐷)} → (𝑔𝑛) ∈ 𝒫 ℝ)
143141, 142syl 17 . . . . . . . . 9 ((𝑔𝑛) ∈ 𝑇 → (𝑔𝑛) ∈ 𝒫 ℝ)
144 elpwi 4388 . . . . . . . . 9 ((𝑔𝑛) ∈ 𝒫 ℝ → (𝑔𝑛) ⊆ ℝ)
145143, 144syl 17 . . . . . . . 8 ((𝑔𝑛) ∈ 𝑇 → (𝑔𝑛) ⊆ ℝ)
146139, 145syl 17 . . . . . . 7 ((𝑔:ℕ⟶𝑇𝑛 ∈ ℕ) → (𝑔𝑛) ⊆ ℝ)
147146iunssd 40184 . . . . . 6 (𝑔:ℕ⟶𝑇 𝑛 ∈ ℕ (𝑔𝑛) ⊆ ℝ)
148138, 147elpwd 4387 . . . . 5 (𝑔:ℕ⟶𝑇 𝑛 ∈ ℕ (𝑔𝑛) ∈ 𝒫 ℝ)
149148adantl 475 . . . 4 ((𝜑𝑔:ℕ⟶𝑇) → 𝑛 ∈ ℕ (𝑔𝑛) ∈ 𝒫 ℝ)
150 imaiun 6775 . . . . . 6 (𝐹 𝑛 ∈ ℕ (𝑔𝑛)) = 𝑛 ∈ ℕ (𝐹 “ (𝑔𝑛))
151150a1i 11 . . . . 5 ((𝜑𝑔:ℕ⟶𝑇) → (𝐹 𝑛 ∈ ℕ (𝑔𝑛)) = 𝑛 ∈ ℕ (𝐹 “ (𝑔𝑛)))
15217adantr 474 . . . . . 6 ((𝜑𝑔:ℕ⟶𝑇) → (𝑆t 𝐷) ∈ SAlg)
153 nnct 13099 . . . . . . 7 ℕ ≼ ω
154153a1i 11 . . . . . 6 ((𝜑𝑔:ℕ⟶𝑇) → ℕ ≼ ω)
155 imaeq2 5716 . . . . . . . . . . . 12 (𝑒 = (𝑔𝑛) → (𝐹𝑒) = (𝐹 “ (𝑔𝑛)))
156155eleq1d 2843 . . . . . . . . . . 11 (𝑒 = (𝑔𝑛) → ((𝐹𝑒) ∈ (𝑆t 𝐷) ↔ (𝐹 “ (𝑔𝑛)) ∈ (𝑆t 𝐷)))
157156, 1elrab2 3575 . . . . . . . . . 10 ((𝑔𝑛) ∈ 𝑇 ↔ ((𝑔𝑛) ∈ 𝒫 ℝ ∧ (𝐹 “ (𝑔𝑛)) ∈ (𝑆t 𝐷)))
158157biimpi 208 . . . . . . . . 9 ((𝑔𝑛) ∈ 𝑇 → ((𝑔𝑛) ∈ 𝒫 ℝ ∧ (𝐹 “ (𝑔𝑛)) ∈ (𝑆t 𝐷)))
159158simprd 491 . . . . . . . 8 ((𝑔𝑛) ∈ 𝑇 → (𝐹 “ (𝑔𝑛)) ∈ (𝑆t 𝐷))
160139, 159syl 17 . . . . . . 7 ((𝑔:ℕ⟶𝑇𝑛 ∈ ℕ) → (𝐹 “ (𝑔𝑛)) ∈ (𝑆t 𝐷))
161160adantll 704 . . . . . 6 (((𝜑𝑔:ℕ⟶𝑇) ∧ 𝑛 ∈ ℕ) → (𝐹 “ (𝑔𝑛)) ∈ (𝑆t 𝐷))
162152, 154, 161saliuncl 41448 . . . . 5 ((𝜑𝑔:ℕ⟶𝑇) → 𝑛 ∈ ℕ (𝐹 “ (𝑔𝑛)) ∈ (𝑆t 𝐷))
163151, 162eqeltrd 2858 . . . 4 ((𝜑𝑔:ℕ⟶𝑇) → (𝐹 𝑛 ∈ ℕ (𝑔𝑛)) ∈ (𝑆t 𝐷))
164149, 163jca 507 . . 3 ((𝜑𝑔:ℕ⟶𝑇) → ( 𝑛 ∈ ℕ (𝑔𝑛) ∈ 𝒫 ℝ ∧ (𝐹 𝑛 ∈ ℕ (𝑔𝑛)) ∈ (𝑆t 𝐷)))
165 imaeq2 5716 . . . . 5 (𝑒 = 𝑛 ∈ ℕ (𝑔𝑛) → (𝐹𝑒) = (𝐹 𝑛 ∈ ℕ (𝑔𝑛)))
166165eleq1d 2843 . . . 4 (𝑒 = 𝑛 ∈ ℕ (𝑔𝑛) → ((𝐹𝑒) ∈ (𝑆t 𝐷) ↔ (𝐹 𝑛 ∈ ℕ (𝑔𝑛)) ∈ (𝑆t 𝐷)))
167166, 1elrab2 3575 . . 3 ( 𝑛 ∈ ℕ (𝑔𝑛) ∈ 𝑇 ↔ ( 𝑛 ∈ ℕ (𝑔𝑛) ∈ 𝒫 ℝ ∧ (𝐹 𝑛 ∈ ℕ (𝑔𝑛)) ∈ (𝑆t 𝐷)))
168164, 167sylibr 226 . 2 ((𝜑𝑔:ℕ⟶𝑇) → 𝑛 ∈ ℕ (𝑔𝑛) ∈ 𝑇)
1695, 24, 25, 134, 168issalnnd 41469 1 (𝜑𝑇 ∈ SAlg)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 386  wal 1599   = wceq 1601  wcel 2106  wrex 3090  {crab 3093  Vcvv 3397  cdif 3788  wss 3791  c0 4140  𝒫 cpw 4378   cuni 4671   ciun 4753   class class class wbr 4886  cmpt 4965  ccnv 5354  dom cdm 5355  cima 5358  Fun wfun 6129   Fn wfn 6130  wf 6131  cfv 6135  (class class class)co 6922  ωcom 7343  cdom 8239  cr 10271  1c1 10273   + caddc 10275  *cxr 10410  cmin 10606  cn 11374  (,)cioo 12487  t crest 16467  SAlgcsalg 41434  SMblFncsmblfn 41818
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2054  ax-8 2108  ax-9 2115  ax-10 2134  ax-11 2149  ax-12 2162  ax-13 2333  ax-ext 2753  ax-rep 5006  ax-sep 5017  ax-nul 5025  ax-pow 5077  ax-pr 5138  ax-un 7226  ax-inf2 8835  ax-cc 9592  ax-ac2 9620  ax-cnex 10328  ax-resscn 10329  ax-1cn 10330  ax-icn 10331  ax-addcl 10332  ax-addrcl 10333  ax-mulcl 10334  ax-mulrcl 10335  ax-mulcom 10336  ax-addass 10337  ax-mulass 10338  ax-distr 10339  ax-i2m1 10340  ax-1ne0 10341  ax-1rid 10342  ax-rnegex 10343  ax-rrecex 10344  ax-cnre 10345  ax-pre-lttri 10346  ax-pre-lttrn 10347  ax-pre-ltadd 10348  ax-pre-mulgt0 10349  ax-pre-sup 10350
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2550  df-eu 2586  df-clab 2763  df-cleq 2769  df-clel 2773  df-nfc 2920  df-ne 2969  df-nel 3075  df-ral 3094  df-rex 3095  df-reu 3096  df-rmo 3097  df-rab 3098  df-v 3399  df-sbc 3652  df-csb 3751  df-dif 3794  df-un 3796  df-in 3798  df-ss 3805  df-pss 3807  df-nul 4141  df-if 4307  df-pw 4380  df-sn 4398  df-pr 4400  df-tp 4402  df-op 4404  df-uni 4672  df-int 4711  df-iun 4755  df-iin 4756  df-br 4887  df-opab 4949  df-mpt 4966  df-tr 4988  df-id 5261  df-eprel 5266  df-po 5274  df-so 5275  df-fr 5314  df-se 5315  df-we 5316  df-xp 5361  df-rel 5362  df-cnv 5363  df-co 5364  df-dm 5365  df-rn 5366  df-res 5367  df-ima 5368  df-pred 5933  df-ord 5979  df-on 5980  df-lim 5981  df-suc 5982  df-iota 6099  df-fun 6137  df-fn 6138  df-f 6139  df-f1 6140  df-fo 6141  df-f1o 6142  df-fv 6143  df-isom 6144  df-riota 6883  df-ov 6925  df-oprab 6926  df-mpt2 6927  df-om 7344  df-1st 7445  df-2nd 7446  df-wrecs 7689  df-recs 7751  df-rdg 7789  df-1o 7843  df-oadd 7847  df-er 8026  df-map 8142  df-pm 8143  df-en 8242  df-dom 8243  df-sdom 8244  df-fin 8245  df-sup 8636  df-inf 8637  df-card 9098  df-acn 9101  df-ac 9272  df-pnf 10413  df-mnf 10414  df-xr 10415  df-ltxr 10416  df-le 10417  df-sub 10608  df-neg 10609  df-div 11033  df-nn 11375  df-n0 11643  df-z 11729  df-uz 11993  df-q 12096  df-rp 12138  df-ioo 12491  df-ico 12493  df-fl 12912  df-rest 16469  df-salg 41435  df-smblfn 41819
This theorem is referenced by:  smfpimbor1lem1  41914  smfpimbor1lem2  41915
  Copyright terms: Public domain W3C validator