Metamath Proof Explorer

Theorem smfresal

Description: Given a sigma-measurable function, the subsets of RR 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)

Ref Expression
Hypotheses smfresal.s ⊢ ( 𝜑 → 𝑆 ∈ SAlg )
smfresal.f ⊢ ( 𝜑 → 𝐹 ∈ ( SMblFn ‘ 𝑆 ) )
smfresal.d ⊢ 𝐷 = dom 𝐹
smfresal.t ⊢ 𝑇 = { 𝑒 ∈ 𝒫 ℝ ∣ ( ◡ 𝐹 “ 𝑒 ) ∈ ( 𝑆 ↾t 𝐷 ) }
Assertion smfresal ( 𝜑 → 𝑇 ∈ SAlg )

Proof

Step Hyp Ref Expression
1 smfresal.s ⊢ ( 𝜑 → 𝑆 ∈ SAlg )
2 smfresal.f ⊢ ( 𝜑 → 𝐹 ∈ ( SMblFn ‘ 𝑆 ) )
3 smfresal.d ⊢ 𝐷 = dom 𝐹
4 smfresal.t ⊢ 𝑇 = { 𝑒 ∈ 𝒫 ℝ ∣ ( ◡ 𝐹 “ 𝑒 ) ∈ ( 𝑆 ↾t 𝐷 ) }
5 reex ⊢ ℝ ∈ V
6 5 pwex ⊢ 𝒫 ℝ ∈ V
7 4 6 rabex2 ⊢ 𝑇 ∈ V
8 7 a1i ⊢ ( 𝜑 → 𝑇 ∈ V )
9 0elpw ⊢ ∅ ∈ 𝒫 ℝ
10 9 a1i ⊢ ( 𝜑 → ∅ ∈ 𝒫 ℝ )
11 ima0 ⊢ ( ◡ 𝐹 “ ∅ ) = ∅
12 11 a1i ⊢ ( 𝜑 → ( ◡ 𝐹 “ ∅ ) = ∅ )
13 1 uniexd ⊢ ( 𝜑 → ∪ 𝑆 ∈ V )
14 1 2 3 smfdmss ⊢ ( 𝜑 → 𝐷 ⊆ ∪ 𝑆 )
15 13 14 ssexd ⊢ ( 𝜑 → 𝐷 ∈ V )
16 eqid ⊢ ( 𝑆 ↾t 𝐷 ) = ( 𝑆 ↾t 𝐷 )
17 1 15 16 subsalsal ⊢ ( 𝜑 → ( 𝑆 ↾t 𝐷 ) ∈ SAlg )
18 17 0sald ⊢ ( 𝜑 → ∅ ∈ ( 𝑆 ↾t 𝐷 ) )
19 12 18 eqeltrd ⊢ ( 𝜑 → ( ◡ 𝐹 “ ∅ ) ∈ ( 𝑆 ↾t 𝐷 ) )
20 10 19 jca ⊢ ( 𝜑 → ( ∅ ∈ 𝒫 ℝ ∧ ( ◡ 𝐹 “ ∅ ) ∈ ( 𝑆 ↾t 𝐷 ) ) )
21 imaeq2 ⊢ ( 𝑒 = ∅ → ( ◡ 𝐹 “ 𝑒 ) = ( ◡ 𝐹 “ ∅ ) )
22 21 eleq1d ⊢ ( 𝑒 = ∅ → ( ( ◡ 𝐹 “ 𝑒 ) ∈ ( 𝑆 ↾t 𝐷 ) ↔ ( ◡ 𝐹 “ ∅ ) ∈ ( 𝑆 ↾t 𝐷 ) ) )
23 22 4 elrab2 ⊢ ( ∅ ∈ 𝑇 ↔ ( ∅ ∈ 𝒫 ℝ ∧ ( ◡ 𝐹 “ ∅ ) ∈ ( 𝑆 ↾t 𝐷 ) ) )
24 20 23 sylibr ⊢ ( 𝜑 → ∅ ∈ 𝑇 )
25 eqid ⊢ ∪ 𝑇 = ∪ 𝑇
26 nfv ⊢ Ⅎ 𝑦 𝜑
27 nfcv ⊢ Ⅎ 𝑒 𝑦
28 nfrab1 ⊢ Ⅎ 𝑒 { 𝑒 ∈ 𝒫 ℝ ∣ ( ◡ 𝐹 “ 𝑒 ) ∈ ( 𝑆 ↾t 𝐷 ) }
29 4 28 nfcxfr ⊢ Ⅎ 𝑒 𝑇
30 27 29 eluni2f ⊢ ( 𝑦 ∈ ∪ 𝑇 ↔ ∃ 𝑒 ∈ 𝑇 𝑦 ∈ 𝑒 )
31 30 biimpi ⊢ ( 𝑦 ∈ ∪ 𝑇 → ∃ 𝑒 ∈ 𝑇 𝑦 ∈ 𝑒 )
32 31 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ∪ 𝑇 ) → ∃ 𝑒 ∈ 𝑇 𝑦 ∈ 𝑒 )
33 nfv ⊢ Ⅎ 𝑒 𝜑
34 29 nfuni ⊢ Ⅎ 𝑒 ∪ 𝑇
35 27 34 nfel ⊢ Ⅎ 𝑒 𝑦 ∈ ∪ 𝑇
36 33 35 nfan ⊢ Ⅎ 𝑒 ( 𝜑 ∧ 𝑦 ∈ ∪ 𝑇 )
37 27 nfel1 ⊢ Ⅎ 𝑒 𝑦 ∈ ℝ
38 4 eleq2i ⊢ ( 𝑒 ∈ 𝑇 ↔ 𝑒 ∈ { 𝑒 ∈ 𝒫 ℝ ∣ ( ◡ 𝐹 “ 𝑒 ) ∈ ( 𝑆 ↾t 𝐷 ) } )
39 38 biimpi ⊢ ( 𝑒 ∈ 𝑇 → 𝑒 ∈ { 𝑒 ∈ 𝒫 ℝ ∣ ( ◡ 𝐹 “ 𝑒 ) ∈ ( 𝑆 ↾t 𝐷 ) } )
40 rabidim1 ⊢ ( 𝑒 ∈ { 𝑒 ∈ 𝒫 ℝ ∣ ( ◡ 𝐹 “ 𝑒 ) ∈ ( 𝑆 ↾t 𝐷 ) } → 𝑒 ∈ 𝒫 ℝ )
41 39 40 syl ⊢ ( 𝑒 ∈ 𝑇 → 𝑒 ∈ 𝒫 ℝ )
42 elpwi ⊢ ( 𝑒 ∈ 𝒫 ℝ → 𝑒 ⊆ ℝ )
43 41 42 syl ⊢ ( 𝑒 ∈ 𝑇 → 𝑒 ⊆ ℝ )
44 43 adantr ⊢ ( ( 𝑒 ∈ 𝑇 ∧ 𝑦 ∈ 𝑒 ) → 𝑒 ⊆ ℝ )
45 simpr ⊢ ( ( 𝑒 ∈ 𝑇 ∧ 𝑦 ∈ 𝑒 ) → 𝑦 ∈ 𝑒 )
46 44 45 sseldd ⊢ ( ( 𝑒 ∈ 𝑇 ∧ 𝑦 ∈ 𝑒 ) → 𝑦 ∈ ℝ )
47 46 ex ⊢ ( 𝑒 ∈ 𝑇 → ( 𝑦 ∈ 𝑒 → 𝑦 ∈ ℝ ) )
48 47 a1i ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ∪ 𝑇 ) → ( 𝑒 ∈ 𝑇 → ( 𝑦 ∈ 𝑒 → 𝑦 ∈ ℝ ) ) )
49 36 37 48 rexlimd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ∪ 𝑇 ) → ( ∃ 𝑒 ∈ 𝑇 𝑦 ∈ 𝑒 → 𝑦 ∈ ℝ ) )
50 32 49 mpd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ∪ 𝑇 ) → 𝑦 ∈ ℝ )
51 50 ex ⊢ ( 𝜑 → ( 𝑦 ∈ ∪ 𝑇 → 𝑦 ∈ ℝ ) )
52 ovexd ⊢ ( 𝜑 → ( ( 𝑦 − 1 ) (,) ( 𝑦 + 1 ) ) ∈ V )
53 ioossre ⊢ ( ( 𝑦 − 1 ) (,) ( 𝑦 + 1 ) ) ⊆ ℝ
54 53 a1i ⊢ ( 𝜑 → ( ( 𝑦 − 1 ) (,) ( 𝑦 + 1 ) ) ⊆ ℝ )
55 52 54 elpwd ⊢ ( 𝜑 → ( ( 𝑦 − 1 ) (,) ( 𝑦 + 1 ) ) ∈ 𝒫 ℝ )
56 55 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ( 𝑦 − 1 ) (,) ( 𝑦 + 1 ) ) ∈ 𝒫 ℝ )
57 1 2 3 smff ⊢ ( 𝜑 → 𝐹 : 𝐷 ⟶ ℝ )
58 57 ffnd ⊢ ( 𝜑 → 𝐹 Fn 𝐷 )
59 fncnvima2 ⊢ ( 𝐹 Fn 𝐷 → ( ◡ 𝐹 “ ( ( 𝑦 − 1 ) (,) ( 𝑦 + 1 ) ) ) = { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) ∈ ( ( 𝑦 − 1 ) (,) ( 𝑦 + 1 ) ) } )
60 58 59 syl ⊢ ( 𝜑 → ( ◡ 𝐹 “ ( ( 𝑦 − 1 ) (,) ( 𝑦 + 1 ) ) ) = { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) ∈ ( ( 𝑦 − 1 ) (,) ( 𝑦 + 1 ) ) } )
61 60 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ◡ 𝐹 “ ( ( 𝑦 − 1 ) (,) ( 𝑦 + 1 ) ) ) = { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) ∈ ( ( 𝑦 − 1 ) (,) ( 𝑦 + 1 ) ) } )
62 nfv ⊢ Ⅎ 𝑥 ( 𝜑 ∧ 𝑦 ∈ ℝ )
63 1 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → 𝑆 ∈ SAlg )
64 15 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → 𝐷 ∈ V )
65 57 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝐹 : 𝐷 ⟶ ℝ )
66 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝑥 ∈ 𝐷 )
67 65 66 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
68 67 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ 𝐷 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
69 57 feqmptd ⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝑥 ) ) )
70 69 eqcomd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝑥 ) ) = 𝐹 )
71 70 2 eqeltrd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝑥 ) ) ∈ ( SMblFn ‘ 𝑆 ) )
72 71 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( 𝑥 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝑥 ) ) ∈ ( SMblFn ‘ 𝑆 ) )
73 peano2rem ⊢ ( 𝑦 ∈ ℝ → ( 𝑦 − 1 ) ∈ ℝ )
74 73 rexrd ⊢ ( 𝑦 ∈ ℝ → ( 𝑦 − 1 ) ∈ ℝ* )
75 74 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( 𝑦 − 1 ) ∈ ℝ* )
76 peano2re ⊢ ( 𝑦 ∈ ℝ → ( 𝑦 + 1 ) ∈ ℝ )
77 76 rexrd ⊢ ( 𝑦 ∈ ℝ → ( 𝑦 + 1 ) ∈ ℝ* )
78 77 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( 𝑦 + 1 ) ∈ ℝ* )
79 62 63 64 68 72 75 78 smfpimioompt ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) ∈ ( ( 𝑦 − 1 ) (,) ( 𝑦 + 1 ) ) } ∈ ( 𝑆 ↾t 𝐷 ) )
80 61 79 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ◡ 𝐹 “ ( ( 𝑦 − 1 ) (,) ( 𝑦 + 1 ) ) ) ∈ ( 𝑆 ↾t 𝐷 ) )
81 56 80 jca ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ( ( 𝑦 − 1 ) (,) ( 𝑦 + 1 ) ) ∈ 𝒫 ℝ ∧ ( ◡ 𝐹 “ ( ( 𝑦 − 1 ) (,) ( 𝑦 + 1 ) ) ) ∈ ( 𝑆 ↾t 𝐷 ) ) )
82 imaeq2 ⊢ ( 𝑒 = ( ( 𝑦 − 1 ) (,) ( 𝑦 + 1 ) ) → ( ◡ 𝐹 “ 𝑒 ) = ( ◡ 𝐹 “ ( ( 𝑦 − 1 ) (,) ( 𝑦 + 1 ) ) ) )
83 82 eleq1d ⊢ ( 𝑒 = ( ( 𝑦 − 1 ) (,) ( 𝑦 + 1 ) ) → ( ( ◡ 𝐹 “ 𝑒 ) ∈ ( 𝑆 ↾t 𝐷 ) ↔ ( ◡ 𝐹 “ ( ( 𝑦 − 1 ) (,) ( 𝑦 + 1 ) ) ) ∈ ( 𝑆 ↾t 𝐷 ) ) )
84 83 4 elrab2 ⊢ ( ( ( 𝑦 − 1 ) (,) ( 𝑦 + 1 ) ) ∈ 𝑇 ↔ ( ( ( 𝑦 − 1 ) (,) ( 𝑦 + 1 ) ) ∈ 𝒫 ℝ ∧ ( ◡ 𝐹 “ ( ( 𝑦 − 1 ) (,) ( 𝑦 + 1 ) ) ) ∈ ( 𝑆 ↾t 𝐷 ) ) )
85 81 84 sylibr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ( 𝑦 − 1 ) (,) ( 𝑦 + 1 ) ) ∈ 𝑇 )
86 id ⊢ ( 𝑦 ∈ ℝ → 𝑦 ∈ ℝ )
87 ltm1 ⊢ ( 𝑦 ∈ ℝ → ( 𝑦 − 1 ) < 𝑦 )
88 ltp1 ⊢ ( 𝑦 ∈ ℝ → 𝑦 < ( 𝑦 + 1 ) )
89 74 77 86 87 88 eliood ⊢ ( 𝑦 ∈ ℝ → 𝑦 ∈ ( ( 𝑦 − 1 ) (,) ( 𝑦 + 1 ) ) )
90 89 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → 𝑦 ∈ ( ( 𝑦 − 1 ) (,) ( 𝑦 + 1 ) ) )
91 nfv ⊢ Ⅎ 𝑒 𝑦 ∈ ( ( 𝑦 − 1 ) (,) ( 𝑦 + 1 ) )
92 nfcv ⊢ Ⅎ 𝑒 ( ( 𝑦 − 1 ) (,) ( 𝑦 + 1 ) )
93 eleq2 ⊢ ( 𝑒 = ( ( 𝑦 − 1 ) (,) ( 𝑦 + 1 ) ) → ( 𝑦 ∈ 𝑒 ↔ 𝑦 ∈ ( ( 𝑦 − 1 ) (,) ( 𝑦 + 1 ) ) ) )
94 91 92 29 93 rspcef ⊢ ( ( ( ( 𝑦 − 1 ) (,) ( 𝑦 + 1 ) ) ∈ 𝑇 ∧ 𝑦 ∈ ( ( 𝑦 − 1 ) (,) ( 𝑦 + 1 ) ) ) → ∃ 𝑒 ∈ 𝑇 𝑦 ∈ 𝑒 )
95 85 90 94 syl2anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ∃ 𝑒 ∈ 𝑇 𝑦 ∈ 𝑒 )
96 95 30 sylibr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → 𝑦 ∈ ∪ 𝑇 )
97 96 ex ⊢ ( 𝜑 → ( 𝑦 ∈ ℝ → 𝑦 ∈ ∪ 𝑇 ) )
98 51 97 impbid ⊢ ( 𝜑 → ( 𝑦 ∈ ∪ 𝑇 ↔ 𝑦 ∈ ℝ ) )
99 26 98 alrimi ⊢ ( 𝜑 → ∀ 𝑦 ( 𝑦 ∈ ∪ 𝑇 ↔ 𝑦 ∈ ℝ ) )
100 dfcleq ⊢ ( ∪ 𝑇 = ℝ ↔ ∀ 𝑦 ( 𝑦 ∈ ∪ 𝑇 ↔ 𝑦 ∈ ℝ ) )
101 99 100 sylibr ⊢ ( 𝜑 → ∪ 𝑇 = ℝ )
102 101 difeq1d ⊢ ( 𝜑 → ( ∪ 𝑇 ∖ 𝑥 ) = ( ℝ ∖ 𝑥 ) )
103 102 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑇 ) → ( ∪ 𝑇 ∖ 𝑥 ) = ( ℝ ∖ 𝑥 ) )
104 difss ⊢ ( ℝ ∖ 𝑥 ) ⊆ ℝ
105 5 104 ssexi ⊢ ( ℝ ∖ 𝑥 ) ∈ V
106 elpwg ⊢ ( ( ℝ ∖ 𝑥 ) ∈ V → ( ( ℝ ∖ 𝑥 ) ∈ 𝒫 ℝ ↔ ( ℝ ∖ 𝑥 ) ⊆ ℝ ) )
107 105 106 ax-mp ⊢ ( ( ℝ ∖ 𝑥 ) ∈ 𝒫 ℝ ↔ ( ℝ ∖ 𝑥 ) ⊆ ℝ )
108 104 107 mpbir ⊢ ( ℝ ∖ 𝑥 ) ∈ 𝒫 ℝ
109 108 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑇 ) → ( ℝ ∖ 𝑥 ) ∈ 𝒫 ℝ )
110 57 ffund ⊢ ( 𝜑 → Fun 𝐹 )
111 difpreima ⊢ ( Fun 𝐹 → ( ◡ 𝐹 “ ( ℝ ∖ 𝑥 ) ) = ( ( ◡ 𝐹 “ ℝ ) ∖ ( ◡ 𝐹 “ 𝑥 ) ) )
112 110 111 syl ⊢ ( 𝜑 → ( ◡ 𝐹 “ ( ℝ ∖ 𝑥 ) ) = ( ( ◡ 𝐹 “ ℝ ) ∖ ( ◡ 𝐹 “ 𝑥 ) ) )
113 fimacnv ⊢ ( 𝐹 : 𝐷 ⟶ ℝ → ( ◡ 𝐹 “ ℝ ) = 𝐷 )
114 57 113 syl ⊢ ( 𝜑 → ( ◡ 𝐹 “ ℝ ) = 𝐷 )
115 1 14 restuni4 ⊢ ( 𝜑 → ∪ ( 𝑆 ↾t 𝐷 ) = 𝐷 )
116 114 115 eqtr4d ⊢ ( 𝜑 → ( ◡ 𝐹 “ ℝ ) = ∪ ( 𝑆 ↾t 𝐷 ) )
117 116 difeq1d ⊢ ( 𝜑 → ( ( ◡ 𝐹 “ ℝ ) ∖ ( ◡ 𝐹 “ 𝑥 ) ) = ( ∪ ( 𝑆 ↾t 𝐷 ) ∖ ( ◡ 𝐹 “ 𝑥 ) ) )
118 112 117 eqtrd ⊢ ( 𝜑 → ( ◡ 𝐹 “ ( ℝ ∖ 𝑥 ) ) = ( ∪ ( 𝑆 ↾t 𝐷 ) ∖ ( ◡ 𝐹 “ 𝑥 ) ) )
119 118 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑇 ) → ( ◡ 𝐹 “ ( ℝ ∖ 𝑥 ) ) = ( ∪ ( 𝑆 ↾t 𝐷 ) ∖ ( ◡ 𝐹 “ 𝑥 ) ) )
120 17 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑇 ) → ( 𝑆 ↾t 𝐷 ) ∈ SAlg )
121 imaeq2 ⊢ ( 𝑒 = 𝑥 → ( ◡ 𝐹 “ 𝑒 ) = ( ◡ 𝐹 “ 𝑥 ) )
122 121 eleq1d ⊢ ( 𝑒 = 𝑥 → ( ( ◡ 𝐹 “ 𝑒 ) ∈ ( 𝑆 ↾t 𝐷 ) ↔ ( ◡ 𝐹 “ 𝑥 ) ∈ ( 𝑆 ↾t 𝐷 ) ) )
123 122 4 elrab2 ⊢ ( 𝑥 ∈ 𝑇 ↔ ( 𝑥 ∈ 𝒫 ℝ ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ ( 𝑆 ↾t 𝐷 ) ) )
124 123 biimpi ⊢ ( 𝑥 ∈ 𝑇 → ( 𝑥 ∈ 𝒫 ℝ ∧ ( ◡ 𝐹 “ 𝑥 ) ∈ ( 𝑆 ↾t 𝐷 ) ) )
125 124 simprd ⊢ ( 𝑥 ∈ 𝑇 → ( ◡ 𝐹 “ 𝑥 ) ∈ ( 𝑆 ↾t 𝐷 ) )
126 125 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑇 ) → ( ◡ 𝐹 “ 𝑥 ) ∈ ( 𝑆 ↾t 𝐷 ) )
127 120 126 saldifcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑇 ) → ( ∪ ( 𝑆 ↾t 𝐷 ) ∖ ( ◡ 𝐹 “ 𝑥 ) ) ∈ ( 𝑆 ↾t 𝐷 ) )
128 119 127 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑇 ) → ( ◡ 𝐹 “ ( ℝ ∖ 𝑥 ) ) ∈ ( 𝑆 ↾t 𝐷 ) )
129 109 128 jca ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑇 ) → ( ( ℝ ∖ 𝑥 ) ∈ 𝒫 ℝ ∧ ( ◡ 𝐹 “ ( ℝ ∖ 𝑥 ) ) ∈ ( 𝑆 ↾t 𝐷 ) ) )
130 imaeq2 ⊢ ( 𝑒 = ( ℝ ∖ 𝑥 ) → ( ◡ 𝐹 “ 𝑒 ) = ( ◡ 𝐹 “ ( ℝ ∖ 𝑥 ) ) )
131 130 eleq1d ⊢ ( 𝑒 = ( ℝ ∖ 𝑥 ) → ( ( ◡ 𝐹 “ 𝑒 ) ∈ ( 𝑆 ↾t 𝐷 ) ↔ ( ◡ 𝐹 “ ( ℝ ∖ 𝑥 ) ) ∈ ( 𝑆 ↾t 𝐷 ) ) )
132 131 4 elrab2 ⊢ ( ( ℝ ∖ 𝑥 ) ∈ 𝑇 ↔ ( ( ℝ ∖ 𝑥 ) ∈ 𝒫 ℝ ∧ ( ◡ 𝐹 “ ( ℝ ∖ 𝑥 ) ) ∈ ( 𝑆 ↾t 𝐷 ) ) )
133 129 132 sylibr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑇 ) → ( ℝ ∖ 𝑥 ) ∈ 𝑇 )
134 103 133 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑇 ) → ( ∪ 𝑇 ∖ 𝑥 ) ∈ 𝑇 )
135 nnex ⊢ ℕ ∈ V
136 fvex ⊢ ( 𝑔 ‘ 𝑛 ) ∈ V
137 135 136 iunex ⊢ ∪ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ∈ V
138 137 a1i ⊢ ( 𝑔 : ℕ ⟶ 𝑇 → ∪ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ∈ V )
139 ffvelcdm ⊢ ( ( 𝑔 : ℕ ⟶ 𝑇 ∧ 𝑛 ∈ ℕ ) → ( 𝑔 ‘ 𝑛 ) ∈ 𝑇 )
140 4 eleq2i ⊢ ( ( 𝑔 ‘ 𝑛 ) ∈ 𝑇 ↔ ( 𝑔 ‘ 𝑛 ) ∈ { 𝑒 ∈ 𝒫 ℝ ∣ ( ◡ 𝐹 “ 𝑒 ) ∈ ( 𝑆 ↾t 𝐷 ) } )
141 140 biimpi ⊢ ( ( 𝑔 ‘ 𝑛 ) ∈ 𝑇 → ( 𝑔 ‘ 𝑛 ) ∈ { 𝑒 ∈ 𝒫 ℝ ∣ ( ◡ 𝐹 “ 𝑒 ) ∈ ( 𝑆 ↾t 𝐷 ) } )
142 elrabi ⊢ ( ( 𝑔 ‘ 𝑛 ) ∈ { 𝑒 ∈ 𝒫 ℝ ∣ ( ◡ 𝐹 “ 𝑒 ) ∈ ( 𝑆 ↾t 𝐷 ) } → ( 𝑔 ‘ 𝑛 ) ∈ 𝒫 ℝ )
143 elpwi ⊢ ( ( 𝑔 ‘ 𝑛 ) ∈ 𝒫 ℝ → ( 𝑔 ‘ 𝑛 ) ⊆ ℝ )
144 139 141 142 143 4syl ⊢ ( ( 𝑔 : ℕ ⟶ 𝑇 ∧ 𝑛 ∈ ℕ ) → ( 𝑔 ‘ 𝑛 ) ⊆ ℝ )
145 144 iunssd ⊢ ( 𝑔 : ℕ ⟶ 𝑇 → ∪ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ⊆ ℝ )
146 138 145 elpwd ⊢ ( 𝑔 : ℕ ⟶ 𝑇 → ∪ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ∈ 𝒫 ℝ )
147 146 adantl ⊢ ( ( 𝜑 ∧ 𝑔 : ℕ ⟶ 𝑇 ) → ∪ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ∈ 𝒫 ℝ )
148 imaiun ⊢ ( ◡ 𝐹 “ ∪ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ) = ∪ 𝑛 ∈ ℕ ( ◡ 𝐹 “ ( 𝑔 ‘ 𝑛 ) )
149 148 a1i ⊢ ( ( 𝜑 ∧ 𝑔 : ℕ ⟶ 𝑇 ) → ( ◡ 𝐹 “ ∪ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ) = ∪ 𝑛 ∈ ℕ ( ◡ 𝐹 “ ( 𝑔 ‘ 𝑛 ) ) )
150 17 adantr ⊢ ( ( 𝜑 ∧ 𝑔 : ℕ ⟶ 𝑇 ) → ( 𝑆 ↾t 𝐷 ) ∈ SAlg )
151 nnct ⊢ ℕ ≼ ω
152 151 a1i ⊢ ( ( 𝜑 ∧ 𝑔 : ℕ ⟶ 𝑇 ) → ℕ ≼ ω )
153 imaeq2 ⊢ ( 𝑒 = ( 𝑔 ‘ 𝑛 ) → ( ◡ 𝐹 “ 𝑒 ) = ( ◡ 𝐹 “ ( 𝑔 ‘ 𝑛 ) ) )
154 153 eleq1d ⊢ ( 𝑒 = ( 𝑔 ‘ 𝑛 ) → ( ( ◡ 𝐹 “ 𝑒 ) ∈ ( 𝑆 ↾t 𝐷 ) ↔ ( ◡ 𝐹 “ ( 𝑔 ‘ 𝑛 ) ) ∈ ( 𝑆 ↾t 𝐷 ) ) )
155 154 4 elrab2 ⊢ ( ( 𝑔 ‘ 𝑛 ) ∈ 𝑇 ↔ ( ( 𝑔 ‘ 𝑛 ) ∈ 𝒫 ℝ ∧ ( ◡ 𝐹 “ ( 𝑔 ‘ 𝑛 ) ) ∈ ( 𝑆 ↾t 𝐷 ) ) )
156 155 biimpi ⊢ ( ( 𝑔 ‘ 𝑛 ) ∈ 𝑇 → ( ( 𝑔 ‘ 𝑛 ) ∈ 𝒫 ℝ ∧ ( ◡ 𝐹 “ ( 𝑔 ‘ 𝑛 ) ) ∈ ( 𝑆 ↾t 𝐷 ) ) )
157 156 simprd ⊢ ( ( 𝑔 ‘ 𝑛 ) ∈ 𝑇 → ( ◡ 𝐹 “ ( 𝑔 ‘ 𝑛 ) ) ∈ ( 𝑆 ↾t 𝐷 ) )
158 139 157 syl ⊢ ( ( 𝑔 : ℕ ⟶ 𝑇 ∧ 𝑛 ∈ ℕ ) → ( ◡ 𝐹 “ ( 𝑔 ‘ 𝑛 ) ) ∈ ( 𝑆 ↾t 𝐷 ) )
159 158 adantll ⊢ ( ( ( 𝜑 ∧ 𝑔 : ℕ ⟶ 𝑇 ) ∧ 𝑛 ∈ ℕ ) → ( ◡ 𝐹 “ ( 𝑔 ‘ 𝑛 ) ) ∈ ( 𝑆 ↾t 𝐷 ) )
160 150 152 159 saliuncl ⊢ ( ( 𝜑 ∧ 𝑔 : ℕ ⟶ 𝑇 ) → ∪ 𝑛 ∈ ℕ ( ◡ 𝐹 “ ( 𝑔 ‘ 𝑛 ) ) ∈ ( 𝑆 ↾t 𝐷 ) )
161 149 160 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑔 : ℕ ⟶ 𝑇 ) → ( ◡ 𝐹 “ ∪ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ) ∈ ( 𝑆 ↾t 𝐷 ) )
162 147 161 jca ⊢ ( ( 𝜑 ∧ 𝑔 : ℕ ⟶ 𝑇 ) → ( ∪ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ∈ 𝒫 ℝ ∧ ( ◡ 𝐹 “ ∪ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ) ∈ ( 𝑆 ↾t 𝐷 ) ) )
163 imaeq2 ⊢ ( 𝑒 = ∪ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) → ( ◡ 𝐹 “ 𝑒 ) = ( ◡ 𝐹 “ ∪ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ) )
164 163 eleq1d ⊢ ( 𝑒 = ∪ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) → ( ( ◡ 𝐹 “ 𝑒 ) ∈ ( 𝑆 ↾t 𝐷 ) ↔ ( ◡ 𝐹 “ ∪ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ) ∈ ( 𝑆 ↾t 𝐷 ) ) )
165 164 4 elrab2 ⊢ ( ∪ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ∈ 𝑇 ↔ ( ∪ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ∈ 𝒫 ℝ ∧ ( ◡ 𝐹 “ ∪ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ) ∈ ( 𝑆 ↾t 𝐷 ) ) )
166 162 165 sylibr ⊢ ( ( 𝜑 ∧ 𝑔 : ℕ ⟶ 𝑇 ) → ∪ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ∈ 𝑇 )
167 8 24 25 134 166 issalnnd ⊢ ( 𝜑 → 𝑇 ∈ SAlg )