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 ffvelrnd ( ( 𝜑𝑥𝐷 ) → ( 𝐹𝑥 ) ∈ ℝ )
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 ffvelrn ( ( 𝑔 : ℕ ⟶ 𝑇𝑛 ∈ ℕ ) → ( 𝑔𝑛 ) ∈ 𝑇 )
140 4 eleq2i ( ( 𝑔𝑛 ) ∈ 𝑇 ↔ ( 𝑔𝑛 ) ∈ { 𝑒 ∈ 𝒫 ℝ ∣ ( 𝐹𝑒 ) ∈ ( 𝑆t 𝐷 ) } )
141 140 biimpi ( ( 𝑔𝑛 ) ∈ 𝑇 → ( 𝑔𝑛 ) ∈ { 𝑒 ∈ 𝒫 ℝ ∣ ( 𝐹𝑒 ) ∈ ( 𝑆t 𝐷 ) } )
142 elrabi ( ( 𝑔𝑛 ) ∈ { 𝑒 ∈ 𝒫 ℝ ∣ ( 𝐹𝑒 ) ∈ ( 𝑆t 𝐷 ) } → ( 𝑔𝑛 ) ∈ 𝒫 ℝ )
143 141 142 syl ( ( 𝑔𝑛 ) ∈ 𝑇 → ( 𝑔𝑛 ) ∈ 𝒫 ℝ )
144 elpwi ( ( 𝑔𝑛 ) ∈ 𝒫 ℝ → ( 𝑔𝑛 ) ⊆ ℝ )
145 143 144 syl ( ( 𝑔𝑛 ) ∈ 𝑇 → ( 𝑔𝑛 ) ⊆ ℝ )
146 139 145 syl ( ( 𝑔 : ℕ ⟶ 𝑇𝑛 ∈ ℕ ) → ( 𝑔𝑛 ) ⊆ ℝ )
147 146 iunssd ( 𝑔 : ℕ ⟶ 𝑇 𝑛 ∈ ℕ ( 𝑔𝑛 ) ⊆ ℝ )
148 138 147 elpwd ( 𝑔 : ℕ ⟶ 𝑇 𝑛 ∈ ℕ ( 𝑔𝑛 ) ∈ 𝒫 ℝ )
149 148 adantl ( ( 𝜑𝑔 : ℕ ⟶ 𝑇 ) → 𝑛 ∈ ℕ ( 𝑔𝑛 ) ∈ 𝒫 ℝ )
150 imaiun ( 𝐹 𝑛 ∈ ℕ ( 𝑔𝑛 ) ) = 𝑛 ∈ ℕ ( 𝐹 “ ( 𝑔𝑛 ) )
151 150 a1i ( ( 𝜑𝑔 : ℕ ⟶ 𝑇 ) → ( 𝐹 𝑛 ∈ ℕ ( 𝑔𝑛 ) ) = 𝑛 ∈ ℕ ( 𝐹 “ ( 𝑔𝑛 ) ) )
152 17 adantr ( ( 𝜑𝑔 : ℕ ⟶ 𝑇 ) → ( 𝑆t 𝐷 ) ∈ SAlg )
153 nnct ℕ ≼ ω
154 153 a1i ( ( 𝜑𝑔 : ℕ ⟶ 𝑇 ) → ℕ ≼ ω )
155 imaeq2 ( 𝑒 = ( 𝑔𝑛 ) → ( 𝐹𝑒 ) = ( 𝐹 “ ( 𝑔𝑛 ) ) )
156 155 eleq1d ( 𝑒 = ( 𝑔𝑛 ) → ( ( 𝐹𝑒 ) ∈ ( 𝑆t 𝐷 ) ↔ ( 𝐹 “ ( 𝑔𝑛 ) ) ∈ ( 𝑆t 𝐷 ) ) )
157 156 4 elrab2 ( ( 𝑔𝑛 ) ∈ 𝑇 ↔ ( ( 𝑔𝑛 ) ∈ 𝒫 ℝ ∧ ( 𝐹 “ ( 𝑔𝑛 ) ) ∈ ( 𝑆t 𝐷 ) ) )
158 157 biimpi ( ( 𝑔𝑛 ) ∈ 𝑇 → ( ( 𝑔𝑛 ) ∈ 𝒫 ℝ ∧ ( 𝐹 “ ( 𝑔𝑛 ) ) ∈ ( 𝑆t 𝐷 ) ) )
159 158 simprd ( ( 𝑔𝑛 ) ∈ 𝑇 → ( 𝐹 “ ( 𝑔𝑛 ) ) ∈ ( 𝑆t 𝐷 ) )
160 139 159 syl ( ( 𝑔 : ℕ ⟶ 𝑇𝑛 ∈ ℕ ) → ( 𝐹 “ ( 𝑔𝑛 ) ) ∈ ( 𝑆t 𝐷 ) )
161 160 adantll ( ( ( 𝜑𝑔 : ℕ ⟶ 𝑇 ) ∧ 𝑛 ∈ ℕ ) → ( 𝐹 “ ( 𝑔𝑛 ) ) ∈ ( 𝑆t 𝐷 ) )
162 152 154 161 saliuncl ( ( 𝜑𝑔 : ℕ ⟶ 𝑇 ) → 𝑛 ∈ ℕ ( 𝐹 “ ( 𝑔𝑛 ) ) ∈ ( 𝑆t 𝐷 ) )
163 151 162 eqeltrd ( ( 𝜑𝑔 : ℕ ⟶ 𝑇 ) → ( 𝐹 𝑛 ∈ ℕ ( 𝑔𝑛 ) ) ∈ ( 𝑆t 𝐷 ) )
164 149 163 jca ( ( 𝜑𝑔 : ℕ ⟶ 𝑇 ) → ( 𝑛 ∈ ℕ ( 𝑔𝑛 ) ∈ 𝒫 ℝ ∧ ( 𝐹 𝑛 ∈ ℕ ( 𝑔𝑛 ) ) ∈ ( 𝑆t 𝐷 ) ) )
165 imaeq2 ( 𝑒 = 𝑛 ∈ ℕ ( 𝑔𝑛 ) → ( 𝐹𝑒 ) = ( 𝐹 𝑛 ∈ ℕ ( 𝑔𝑛 ) ) )
166 165 eleq1d ( 𝑒 = 𝑛 ∈ ℕ ( 𝑔𝑛 ) → ( ( 𝐹𝑒 ) ∈ ( 𝑆t 𝐷 ) ↔ ( 𝐹 𝑛 ∈ ℕ ( 𝑔𝑛 ) ) ∈ ( 𝑆t 𝐷 ) ) )
167 166 4 elrab2 ( 𝑛 ∈ ℕ ( 𝑔𝑛 ) ∈ 𝑇 ↔ ( 𝑛 ∈ ℕ ( 𝑔𝑛 ) ∈ 𝒫 ℝ ∧ ( 𝐹 𝑛 ∈ ℕ ( 𝑔𝑛 ) ) ∈ ( 𝑆t 𝐷 ) ) )
168 164 167 sylibr ( ( 𝜑𝑔 : ℕ ⟶ 𝑇 ) → 𝑛 ∈ ℕ ( 𝑔𝑛 ) ∈ 𝑇 )
169 8 24 25 134 168 issalnnd ( 𝜑𝑇 ∈ SAlg )