Metamath Proof Explorer

Theorem issmflem

Description: The predicate " F is a real-valued measurable function w.r.t. to the sigma-algebra S ". A function is measurable iff the preimages of all open intervals unbounded below are in the subspace sigma-algebra induced by its domain. The domain of F is required to be a subset of the underlying set of S . Definition 121C of Fremlin1 p. 36, and Proposition 121B (i) of Fremlin1 p. 35 . (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses issmflem.s ⊢ ( 𝜑 → 𝑆 ∈ SAlg )
issmflem.d ⊢ 𝐷 = dom 𝐹
Assertion issmflem ( 𝜑 → ( 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ↔ ( 𝐷 ⊆ ∪ 𝑆 ∧ 𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑎 ∈ ℝ { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } ∈ ( 𝑆 ↾t 𝐷 ) ) ) )

Proof

Step Hyp Ref Expression
1 issmflem.s ⊢ ( 𝜑 → 𝑆 ∈ SAlg )
2 issmflem.d ⊢ 𝐷 = dom 𝐹
3 simpr ⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) → 𝐹 ∈ ( SMblFn ‘ 𝑆 ) )
4 df-smblfn ⊢ SMblFn = ( 𝑠 ∈ SAlg ↦ { 𝑓 ∈ ( ℝ ↑pm ∪ 𝑠 ) ∣ ∀ 𝑎 ∈ ℝ ( ◡ 𝑓 “ ( -∞ (,) 𝑎 ) ) ∈ ( 𝑠 ↾t dom 𝑓 ) } )
5 unieq ⊢ ( 𝑠 = 𝑆 → ∪ 𝑠 = ∪ 𝑆 )
6 5 oveq2d ⊢ ( 𝑠 = 𝑆 → ( ℝ ↑pm ∪ 𝑠 ) = ( ℝ ↑pm ∪ 𝑆 ) )
7 6 rabeqdv ⊢ ( 𝑠 = 𝑆 → { 𝑓 ∈ ( ℝ ↑pm ∪ 𝑠 ) ∣ ∀ 𝑎 ∈ ℝ ( ◡ 𝑓 “ ( -∞ (,) 𝑎 ) ) ∈ ( 𝑠 ↾t dom 𝑓 ) } = { 𝑓 ∈ ( ℝ ↑pm ∪ 𝑆 ) ∣ ∀ 𝑎 ∈ ℝ ( ◡ 𝑓 “ ( -∞ (,) 𝑎 ) ) ∈ ( 𝑠 ↾t dom 𝑓 ) } )
8 oveq1 ⊢ ( 𝑠 = 𝑆 → ( 𝑠 ↾t dom 𝑓 ) = ( 𝑆 ↾t dom 𝑓 ) )
9 8 eleq2d ⊢ ( 𝑠 = 𝑆 → ( ( ◡ 𝑓 “ ( -∞ (,) 𝑎 ) ) ∈ ( 𝑠 ↾t dom 𝑓 ) ↔ ( ◡ 𝑓 “ ( -∞ (,) 𝑎 ) ) ∈ ( 𝑆 ↾t dom 𝑓 ) ) )
10 9 ralbidv ⊢ ( 𝑠 = 𝑆 → ( ∀ 𝑎 ∈ ℝ ( ◡ 𝑓 “ ( -∞ (,) 𝑎 ) ) ∈ ( 𝑠 ↾t dom 𝑓 ) ↔ ∀ 𝑎 ∈ ℝ ( ◡ 𝑓 “ ( -∞ (,) 𝑎 ) ) ∈ ( 𝑆 ↾t dom 𝑓 ) ) )
11 10 rabbidv ⊢ ( 𝑠 = 𝑆 → { 𝑓 ∈ ( ℝ ↑pm ∪ 𝑆 ) ∣ ∀ 𝑎 ∈ ℝ ( ◡ 𝑓 “ ( -∞ (,) 𝑎 ) ) ∈ ( 𝑠 ↾t dom 𝑓 ) } = { 𝑓 ∈ ( ℝ ↑pm ∪ 𝑆 ) ∣ ∀ 𝑎 ∈ ℝ ( ◡ 𝑓 “ ( -∞ (,) 𝑎 ) ) ∈ ( 𝑆 ↾t dom 𝑓 ) } )
12 7 11 eqtrd ⊢ ( 𝑠 = 𝑆 → { 𝑓 ∈ ( ℝ ↑pm ∪ 𝑠 ) ∣ ∀ 𝑎 ∈ ℝ ( ◡ 𝑓 “ ( -∞ (,) 𝑎 ) ) ∈ ( 𝑠 ↾t dom 𝑓 ) } = { 𝑓 ∈ ( ℝ ↑pm ∪ 𝑆 ) ∣ ∀ 𝑎 ∈ ℝ ( ◡ 𝑓 “ ( -∞ (,) 𝑎 ) ) ∈ ( 𝑆 ↾t dom 𝑓 ) } )
13 ovex ⊢ ( ℝ ↑pm ∪ 𝑆 ) ∈ V
14 13 rabex ⊢ { 𝑓 ∈ ( ℝ ↑pm ∪ 𝑆 ) ∣ ∀ 𝑎 ∈ ℝ ( ◡ 𝑓 “ ( -∞ (,) 𝑎 ) ) ∈ ( 𝑆 ↾t dom 𝑓 ) } ∈ V
15 14 a1i ⊢ ( 𝜑 → { 𝑓 ∈ ( ℝ ↑pm ∪ 𝑆 ) ∣ ∀ 𝑎 ∈ ℝ ( ◡ 𝑓 “ ( -∞ (,) 𝑎 ) ) ∈ ( 𝑆 ↾t dom 𝑓 ) } ∈ V )
16 4 12 1 15 fvmptd3 ⊢ ( 𝜑 → ( SMblFn ‘ 𝑆 ) = { 𝑓 ∈ ( ℝ ↑pm ∪ 𝑆 ) ∣ ∀ 𝑎 ∈ ℝ ( ◡ 𝑓 “ ( -∞ (,) 𝑎 ) ) ∈ ( 𝑆 ↾t dom 𝑓 ) } )
17 16 adantr ⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) → ( SMblFn ‘ 𝑆 ) = { 𝑓 ∈ ( ℝ ↑pm ∪ 𝑆 ) ∣ ∀ 𝑎 ∈ ℝ ( ◡ 𝑓 “ ( -∞ (,) 𝑎 ) ) ∈ ( 𝑆 ↾t dom 𝑓 ) } )
18 3 17 eleqtrd ⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) → 𝐹 ∈ { 𝑓 ∈ ( ℝ ↑pm ∪ 𝑆 ) ∣ ∀ 𝑎 ∈ ℝ ( ◡ 𝑓 “ ( -∞ (,) 𝑎 ) ) ∈ ( 𝑆 ↾t dom 𝑓 ) } )
19 elrabi ⊢ ( 𝐹 ∈ { 𝑓 ∈ ( ℝ ↑pm ∪ 𝑆 ) ∣ ∀ 𝑎 ∈ ℝ ( ◡ 𝑓 “ ( -∞ (,) 𝑎 ) ) ∈ ( 𝑆 ↾t dom 𝑓 ) } → 𝐹 ∈ ( ℝ ↑pm ∪ 𝑆 ) )
20 18 19 syl ⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) → 𝐹 ∈ ( ℝ ↑pm ∪ 𝑆 ) )
21 elpmi2 ⊢ ( 𝐹 ∈ ( ℝ ↑pm ∪ 𝑆 ) → dom 𝐹 ⊆ ∪ 𝑆 )
22 2 21 eqsstrid ⊢ ( 𝐹 ∈ ( ℝ ↑pm ∪ 𝑆 ) → 𝐷 ⊆ ∪ 𝑆 )
23 22 adantl ⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( ℝ ↑pm ∪ 𝑆 ) ) → 𝐷 ⊆ ∪ 𝑆 )
24 20 23 syldan ⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) → 𝐷 ⊆ ∪ 𝑆 )
25 elpmi ⊢ ( 𝐹 ∈ ( ℝ ↑pm ∪ 𝑆 ) → ( 𝐹 : dom 𝐹 ⟶ ℝ ∧ dom 𝐹 ⊆ ∪ 𝑆 ) )
26 20 25 syl ⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) → ( 𝐹 : dom 𝐹 ⟶ ℝ ∧ dom 𝐹 ⊆ ∪ 𝑆 ) )
27 26 simpld ⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) → 𝐹 : dom 𝐹 ⟶ ℝ )
28 2 feq2i ⊢ ( 𝐹 : 𝐷 ⟶ ℝ ↔ 𝐹 : dom 𝐹 ⟶ ℝ )
29 28 a1i ⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) → ( 𝐹 : 𝐷 ⟶ ℝ ↔ 𝐹 : dom 𝐹 ⟶ ℝ ) )
30 27 29 mpbird ⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) → 𝐹 : 𝐷 ⟶ ℝ )
31 cnveq ⊢ ( 𝑓 = 𝐹 → ◡ 𝑓 = ◡ 𝐹 )
32 31 imaeq1d ⊢ ( 𝑓 = 𝐹 → ( ◡ 𝑓 “ ( -∞ (,) 𝑎 ) ) = ( ◡ 𝐹 “ ( -∞ (,) 𝑎 ) ) )
33 dmeq ⊢ ( 𝑓 = 𝐹 → dom 𝑓 = dom 𝐹 )
34 33 oveq2d ⊢ ( 𝑓 = 𝐹 → ( 𝑆 ↾t dom 𝑓 ) = ( 𝑆 ↾t dom 𝐹 ) )
35 32 34 eleq12d ⊢ ( 𝑓 = 𝐹 → ( ( ◡ 𝑓 “ ( -∞ (,) 𝑎 ) ) ∈ ( 𝑆 ↾t dom 𝑓 ) ↔ ( ◡ 𝐹 “ ( -∞ (,) 𝑎 ) ) ∈ ( 𝑆 ↾t dom 𝐹 ) ) )
36 35 ralbidv ⊢ ( 𝑓 = 𝐹 → ( ∀ 𝑎 ∈ ℝ ( ◡ 𝑓 “ ( -∞ (,) 𝑎 ) ) ∈ ( 𝑆 ↾t dom 𝑓 ) ↔ ∀ 𝑎 ∈ ℝ ( ◡ 𝐹 “ ( -∞ (,) 𝑎 ) ) ∈ ( 𝑆 ↾t dom 𝐹 ) ) )
37 36 elrab ⊢ ( 𝐹 ∈ { 𝑓 ∈ ( ℝ ↑pm ∪ 𝑆 ) ∣ ∀ 𝑎 ∈ ℝ ( ◡ 𝑓 “ ( -∞ (,) 𝑎 ) ) ∈ ( 𝑆 ↾t dom 𝑓 ) } ↔ ( 𝐹 ∈ ( ℝ ↑pm ∪ 𝑆 ) ∧ ∀ 𝑎 ∈ ℝ ( ◡ 𝐹 “ ( -∞ (,) 𝑎 ) ) ∈ ( 𝑆 ↾t dom 𝐹 ) ) )
38 37 simprbi ⊢ ( 𝐹 ∈ { 𝑓 ∈ ( ℝ ↑pm ∪ 𝑆 ) ∣ ∀ 𝑎 ∈ ℝ ( ◡ 𝑓 “ ( -∞ (,) 𝑎 ) ) ∈ ( 𝑆 ↾t dom 𝑓 ) } → ∀ 𝑎 ∈ ℝ ( ◡ 𝐹 “ ( -∞ (,) 𝑎 ) ) ∈ ( 𝑆 ↾t dom 𝐹 ) )
39 18 38 syl ⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) → ∀ 𝑎 ∈ ℝ ( ◡ 𝐹 “ ( -∞ (,) 𝑎 ) ) ∈ ( 𝑆 ↾t dom 𝐹 ) )
40 39 adantr ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) ∧ 𝑎 ∈ ℝ ) → ∀ 𝑎 ∈ ℝ ( ◡ 𝐹 “ ( -∞ (,) 𝑎 ) ) ∈ ( 𝑆 ↾t dom 𝐹 ) )
41 simpr ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) ∧ 𝑎 ∈ ℝ ) → 𝑎 ∈ ℝ )
42 rspa ⊢ ( ( ∀ 𝑎 ∈ ℝ ( ◡ 𝐹 “ ( -∞ (,) 𝑎 ) ) ∈ ( 𝑆 ↾t dom 𝐹 ) ∧ 𝑎 ∈ ℝ ) → ( ◡ 𝐹 “ ( -∞ (,) 𝑎 ) ) ∈ ( 𝑆 ↾t dom 𝐹 ) )
43 40 41 42 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) ∧ 𝑎 ∈ ℝ ) → ( ◡ 𝐹 “ ( -∞ (,) 𝑎 ) ) ∈ ( 𝑆 ↾t dom 𝐹 ) )
44 30 adantr ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) ∧ 𝑎 ∈ ℝ ) → 𝐹 : 𝐷 ⟶ ℝ )
45 simpl ⊢ ( ( 𝐹 : 𝐷 ⟶ ℝ ∧ 𝑎 ∈ ℝ ) → 𝐹 : 𝐷 ⟶ ℝ )
46 simpr ⊢ ( ( 𝐹 : 𝐷 ⟶ ℝ ∧ 𝑎 ∈ ℝ ) → 𝑎 ∈ ℝ )
47 46 rexrd ⊢ ( ( 𝐹 : 𝐷 ⟶ ℝ ∧ 𝑎 ∈ ℝ ) → 𝑎 ∈ ℝ* )
48 45 47 preimaioomnf ⊢ ( ( 𝐹 : 𝐷 ⟶ ℝ ∧ 𝑎 ∈ ℝ ) → ( ◡ 𝐹 “ ( -∞ (,) 𝑎 ) ) = { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } )
49 48 eqcomd ⊢ ( ( 𝐹 : 𝐷 ⟶ ℝ ∧ 𝑎 ∈ ℝ ) → { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } = ( ◡ 𝐹 “ ( -∞ (,) 𝑎 ) ) )
50 44 41 49 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) ∧ 𝑎 ∈ ℝ ) → { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } = ( ◡ 𝐹 “ ( -∞ (,) 𝑎 ) ) )
51 2 oveq2i ⊢ ( 𝑆 ↾t 𝐷 ) = ( 𝑆 ↾t dom 𝐹 )
52 51 a1i ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) ∧ 𝑎 ∈ ℝ ) → ( 𝑆 ↾t 𝐷 ) = ( 𝑆 ↾t dom 𝐹 ) )
53 50 52 eleq12d ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) ∧ 𝑎 ∈ ℝ ) → ( { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } ∈ ( 𝑆 ↾t 𝐷 ) ↔ ( ◡ 𝐹 “ ( -∞ (,) 𝑎 ) ) ∈ ( 𝑆 ↾t dom 𝐹 ) ) )
54 43 53 mpbird ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) ∧ 𝑎 ∈ ℝ ) → { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } ∈ ( 𝑆 ↾t 𝐷 ) )
55 54 ralrimiva ⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) → ∀ 𝑎 ∈ ℝ { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } ∈ ( 𝑆 ↾t 𝐷 ) )
56 24 30 55 3jca ⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) → ( 𝐷 ⊆ ∪ 𝑆 ∧ 𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑎 ∈ ℝ { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } ∈ ( 𝑆 ↾t 𝐷 ) ) )
57 56 ex ⊢ ( 𝜑 → ( 𝐹 ∈ ( SMblFn ‘ 𝑆 ) → ( 𝐷 ⊆ ∪ 𝑆 ∧ 𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑎 ∈ ℝ { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } ∈ ( 𝑆 ↾t 𝐷 ) ) ) )
58 reex ⊢ ℝ ∈ V
59 58 a1i ⊢ ( ( 𝜑 ∧ ( 𝐷 ⊆ ∪ 𝑆 ∧ 𝐹 : 𝐷 ⟶ ℝ ) ) → ℝ ∈ V )
60 1 uniexd ⊢ ( 𝜑 → ∪ 𝑆 ∈ V )
61 60 adantr ⊢ ( ( 𝜑 ∧ ( 𝐷 ⊆ ∪ 𝑆 ∧ 𝐹 : 𝐷 ⟶ ℝ ) ) → ∪ 𝑆 ∈ V )
62 simprr ⊢ ( ( 𝜑 ∧ ( 𝐷 ⊆ ∪ 𝑆 ∧ 𝐹 : 𝐷 ⟶ ℝ ) ) → 𝐹 : 𝐷 ⟶ ℝ )
63 fssxp ⊢ ( 𝐹 : 𝐷 ⟶ ℝ → 𝐹 ⊆ ( 𝐷 × ℝ ) )
64 63 adantl ⊢ ( ( 𝐷 ⊆ ∪ 𝑆 ∧ 𝐹 : 𝐷 ⟶ ℝ ) → 𝐹 ⊆ ( 𝐷 × ℝ ) )
65 xpss1 ⊢ ( 𝐷 ⊆ ∪ 𝑆 → ( 𝐷 × ℝ ) ⊆ ( ∪ 𝑆 × ℝ ) )
66 65 adantr ⊢ ( ( 𝐷 ⊆ ∪ 𝑆 ∧ 𝐹 : 𝐷 ⟶ ℝ ) → ( 𝐷 × ℝ ) ⊆ ( ∪ 𝑆 × ℝ ) )
67 64 66 sstrd ⊢ ( ( 𝐷 ⊆ ∪ 𝑆 ∧ 𝐹 : 𝐷 ⟶ ℝ ) → 𝐹 ⊆ ( ∪ 𝑆 × ℝ ) )
68 67 adantl ⊢ ( ( 𝜑 ∧ ( 𝐷 ⊆ ∪ 𝑆 ∧ 𝐹 : 𝐷 ⟶ ℝ ) ) → 𝐹 ⊆ ( ∪ 𝑆 × ℝ ) )
69 dmss ⊢ ( 𝐹 ⊆ ( ∪ 𝑆 × ℝ ) → dom 𝐹 ⊆ dom ( ∪ 𝑆 × ℝ ) )
70 dmxpss ⊢ dom ( ∪ 𝑆 × ℝ ) ⊆ ∪ 𝑆
71 70 a1i ⊢ ( 𝐹 ⊆ ( ∪ 𝑆 × ℝ ) → dom ( ∪ 𝑆 × ℝ ) ⊆ ∪ 𝑆 )
72 69 71 sstrd ⊢ ( 𝐹 ⊆ ( ∪ 𝑆 × ℝ ) → dom 𝐹 ⊆ ∪ 𝑆 )
73 72 adantl ⊢ ( ( 𝜑 ∧ 𝐹 ⊆ ( ∪ 𝑆 × ℝ ) ) → dom 𝐹 ⊆ ∪ 𝑆 )
74 2 73 eqsstrid ⊢ ( ( 𝜑 ∧ 𝐹 ⊆ ( ∪ 𝑆 × ℝ ) ) → 𝐷 ⊆ ∪ 𝑆 )
75 68 74 syldan ⊢ ( ( 𝜑 ∧ ( 𝐷 ⊆ ∪ 𝑆 ∧ 𝐹 : 𝐷 ⟶ ℝ ) ) → 𝐷 ⊆ ∪ 𝑆 )
76 elpm2r ⊢ ( ( ( ℝ ∈ V ∧ ∪ 𝑆 ∈ V ) ∧ ( 𝐹 : 𝐷 ⟶ ℝ ∧ 𝐷 ⊆ ∪ 𝑆 ) ) → 𝐹 ∈ ( ℝ ↑pm ∪ 𝑆 ) )
77 59 61 62 75 76 syl22anc ⊢ ( ( 𝜑 ∧ ( 𝐷 ⊆ ∪ 𝑆 ∧ 𝐹 : 𝐷 ⟶ ℝ ) ) → 𝐹 ∈ ( ℝ ↑pm ∪ 𝑆 ) )
78 77 3adantr3 ⊢ ( ( 𝜑 ∧ ( 𝐷 ⊆ ∪ 𝑆 ∧ 𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑎 ∈ ℝ { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } ∈ ( 𝑆 ↾t 𝐷 ) ) ) → 𝐹 ∈ ( ℝ ↑pm ∪ 𝑆 ) )
79 2 a1i ⊢ ( ( 𝐹 : 𝐷 ⟶ ℝ ∧ 𝑎 ∈ ℝ ) → 𝐷 = dom 𝐹 )
80 79 oveq2d ⊢ ( ( 𝐹 : 𝐷 ⟶ ℝ ∧ 𝑎 ∈ ℝ ) → ( 𝑆 ↾t 𝐷 ) = ( 𝑆 ↾t dom 𝐹 ) )
81 49 80 eleq12d ⊢ ( ( 𝐹 : 𝐷 ⟶ ℝ ∧ 𝑎 ∈ ℝ ) → ( { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } ∈ ( 𝑆 ↾t 𝐷 ) ↔ ( ◡ 𝐹 “ ( -∞ (,) 𝑎 ) ) ∈ ( 𝑆 ↾t dom 𝐹 ) ) )
82 81 ralbidva ⊢ ( 𝐹 : 𝐷 ⟶ ℝ → ( ∀ 𝑎 ∈ ℝ { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } ∈ ( 𝑆 ↾t 𝐷 ) ↔ ∀ 𝑎 ∈ ℝ ( ◡ 𝐹 “ ( -∞ (,) 𝑎 ) ) ∈ ( 𝑆 ↾t dom 𝐹 ) ) )
83 82 biimpd ⊢ ( 𝐹 : 𝐷 ⟶ ℝ → ( ∀ 𝑎 ∈ ℝ { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } ∈ ( 𝑆 ↾t 𝐷 ) → ∀ 𝑎 ∈ ℝ ( ◡ 𝐹 “ ( -∞ (,) 𝑎 ) ) ∈ ( 𝑆 ↾t dom 𝐹 ) ) )
84 83 imp ⊢ ( ( 𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑎 ∈ ℝ { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } ∈ ( 𝑆 ↾t 𝐷 ) ) → ∀ 𝑎 ∈ ℝ ( ◡ 𝐹 “ ( -∞ (,) 𝑎 ) ) ∈ ( 𝑆 ↾t dom 𝐹 ) )
85 84 adantl ⊢ ( ( 𝜑 ∧ ( 𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑎 ∈ ℝ { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } ∈ ( 𝑆 ↾t 𝐷 ) ) ) → ∀ 𝑎 ∈ ℝ ( ◡ 𝐹 “ ( -∞ (,) 𝑎 ) ) ∈ ( 𝑆 ↾t dom 𝐹 ) )
86 85 3adantr1 ⊢ ( ( 𝜑 ∧ ( 𝐷 ⊆ ∪ 𝑆 ∧ 𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑎 ∈ ℝ { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } ∈ ( 𝑆 ↾t 𝐷 ) ) ) → ∀ 𝑎 ∈ ℝ ( ◡ 𝐹 “ ( -∞ (,) 𝑎 ) ) ∈ ( 𝑆 ↾t dom 𝐹 ) )
87 78 86 jca ⊢ ( ( 𝜑 ∧ ( 𝐷 ⊆ ∪ 𝑆 ∧ 𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑎 ∈ ℝ { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } ∈ ( 𝑆 ↾t 𝐷 ) ) ) → ( 𝐹 ∈ ( ℝ ↑pm ∪ 𝑆 ) ∧ ∀ 𝑎 ∈ ℝ ( ◡ 𝐹 “ ( -∞ (,) 𝑎 ) ) ∈ ( 𝑆 ↾t dom 𝐹 ) ) )
88 87 37 sylibr ⊢ ( ( 𝜑 ∧ ( 𝐷 ⊆ ∪ 𝑆 ∧ 𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑎 ∈ ℝ { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } ∈ ( 𝑆 ↾t 𝐷 ) ) ) → 𝐹 ∈ { 𝑓 ∈ ( ℝ ↑pm ∪ 𝑆 ) ∣ ∀ 𝑎 ∈ ℝ ( ◡ 𝑓 “ ( -∞ (,) 𝑎 ) ) ∈ ( 𝑆 ↾t dom 𝑓 ) } )
89 16 eqcomd ⊢ ( 𝜑 → { 𝑓 ∈ ( ℝ ↑pm ∪ 𝑆 ) ∣ ∀ 𝑎 ∈ ℝ ( ◡ 𝑓 “ ( -∞ (,) 𝑎 ) ) ∈ ( 𝑆 ↾t dom 𝑓 ) } = ( SMblFn ‘ 𝑆 ) )
90 89 adantr ⊢ ( ( 𝜑 ∧ ( 𝐷 ⊆ ∪ 𝑆 ∧ 𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑎 ∈ ℝ { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } ∈ ( 𝑆 ↾t 𝐷 ) ) ) → { 𝑓 ∈ ( ℝ ↑pm ∪ 𝑆 ) ∣ ∀ 𝑎 ∈ ℝ ( ◡ 𝑓 “ ( -∞ (,) 𝑎 ) ) ∈ ( 𝑆 ↾t dom 𝑓 ) } = ( SMblFn ‘ 𝑆 ) )
91 88 90 eleqtrd ⊢ ( ( 𝜑 ∧ ( 𝐷 ⊆ ∪ 𝑆 ∧ 𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑎 ∈ ℝ { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } ∈ ( 𝑆 ↾t 𝐷 ) ) ) → 𝐹 ∈ ( SMblFn ‘ 𝑆 ) )
92 91 ex ⊢ ( 𝜑 → ( ( 𝐷 ⊆ ∪ 𝑆 ∧ 𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑎 ∈ ℝ { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } ∈ ( 𝑆 ↾t 𝐷 ) ) → 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) )
93 57 92 impbid ⊢ ( 𝜑 → ( 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ↔ ( 𝐷 ⊆ ∪ 𝑆 ∧ 𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑎 ∈ ℝ { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑎 } ∈ ( 𝑆 ↾t 𝐷 ) ) ) )