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