Metamath Proof Explorer

Theorem issmfgt

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 left-open intervals unbounded above are in the subspace sigma-algebra induced by its domain. The domain of F is required to be b subset of the underlying set of S . Definition 121C of Fremlin1 p. 36, and Proposition 121B (iii) of Fremlin1 p. 35 . (Contributed by Glauco Siliprandi, 26-Jun-2021)

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

Proof

Step Hyp Ref Expression
1 issmfgt.s ⊢ ( 𝜑 → 𝑆 ∈ SAlg )
2 issmfgt.d ⊢ 𝐷 = dom 𝐹
3 1 adantr ⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) → 𝑆 ∈ SAlg )
4 simpr ⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) → 𝐹 ∈ ( SMblFn ‘ 𝑆 ) )
5 3 4 2 smfdmss ⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) → 𝐷 ⊆ ∪ 𝑆 )
6 3 4 2 smff ⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) → 𝐹 : 𝐷 ⟶ ℝ )
7 nfv ⊢ Ⅎ 𝑏 𝜑
8 nfv ⊢ Ⅎ 𝑏 𝐹 ∈ ( SMblFn ‘ 𝑆 )
9 7 8 nfan ⊢ Ⅎ 𝑏 ( 𝜑 ∧ 𝐹 ∈ ( SMblFn ‘ 𝑆 ) )
10 3 5 restuni4 ⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) → ∪ ( 𝑆 ↾t 𝐷 ) = 𝐷 )
11 10 eqcomd ⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) → 𝐷 = ∪ ( 𝑆 ↾t 𝐷 ) )
12 11 rabeqdv ⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) → { 𝑦 ∈ 𝐷 ∣ 𝑏 < ( 𝐹 ‘ 𝑦 ) } = { 𝑦 ∈ ∪ ( 𝑆 ↾t 𝐷 ) ∣ 𝑏 < ( 𝐹 ‘ 𝑦 ) } )
13 12 adantr ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) ∧ 𝑏 ∈ ℝ ) → { 𝑦 ∈ 𝐷 ∣ 𝑏 < ( 𝐹 ‘ 𝑦 ) } = { 𝑦 ∈ ∪ ( 𝑆 ↾t 𝐷 ) ∣ 𝑏 < ( 𝐹 ‘ 𝑦 ) } )
14 nfv ⊢ Ⅎ 𝑦 𝜑
15 nfv ⊢ Ⅎ 𝑦 𝐹 ∈ ( SMblFn ‘ 𝑆 )
16 14 15 nfan ⊢ Ⅎ 𝑦 ( 𝜑 ∧ 𝐹 ∈ ( SMblFn ‘ 𝑆 ) )
17 nfv ⊢ Ⅎ 𝑦 𝑏 ∈ ℝ
18 16 17 nfan ⊢ Ⅎ 𝑦 ( ( 𝜑 ∧ 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) ∧ 𝑏 ∈ ℝ )
19 nfv ⊢ Ⅎ 𝑐 ( ( 𝜑 ∧ 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) ∧ 𝑏 ∈ ℝ )
20 1 uniexd ⊢ ( 𝜑 → ∪ 𝑆 ∈ V )
21 20 adantr ⊢ ( ( 𝜑 ∧ 𝐷 ⊆ ∪ 𝑆 ) → ∪ 𝑆 ∈ V )
22 simpr ⊢ ( ( 𝜑 ∧ 𝐷 ⊆ ∪ 𝑆 ) → 𝐷 ⊆ ∪ 𝑆 )
23 21 22 ssexd ⊢ ( ( 𝜑 ∧ 𝐷 ⊆ ∪ 𝑆 ) → 𝐷 ∈ V )
24 5 23 syldan ⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) → 𝐷 ∈ V )
25 eqid ⊢ ( 𝑆 ↾t 𝐷 ) = ( 𝑆 ↾t 𝐷 )
26 3 24 25 subsalsal ⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) → ( 𝑆 ↾t 𝐷 ) ∈ SAlg )
27 26 adantr ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) ∧ 𝑏 ∈ ℝ ) → ( 𝑆 ↾t 𝐷 ) ∈ SAlg )
28 eqid ⊢ ∪ ( 𝑆 ↾t 𝐷 ) = ∪ ( 𝑆 ↾t 𝐷 )
29 6 adantr ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) ∧ 𝑦 ∈ ∪ ( 𝑆 ↾t 𝐷 ) ) → 𝐹 : 𝐷 ⟶ ℝ )
30 simpr ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) ∧ 𝑦 ∈ ∪ ( 𝑆 ↾t 𝐷 ) ) → 𝑦 ∈ ∪ ( 𝑆 ↾t 𝐷 ) )
31 10 adantr ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) ∧ 𝑦 ∈ ∪ ( 𝑆 ↾t 𝐷 ) ) → ∪ ( 𝑆 ↾t 𝐷 ) = 𝐷 )
32 30 31 eleqtrd ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) ∧ 𝑦 ∈ ∪ ( 𝑆 ↾t 𝐷 ) ) → 𝑦 ∈ 𝐷 )
33 29 32 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) ∧ 𝑦 ∈ ∪ ( 𝑆 ↾t 𝐷 ) ) → ( 𝐹 ‘ 𝑦 ) ∈ ℝ )
34 33 rexrd ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) ∧ 𝑦 ∈ ∪ ( 𝑆 ↾t 𝐷 ) ) → ( 𝐹 ‘ 𝑦 ) ∈ ℝ* )
35 34 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) ∧ 𝑏 ∈ ℝ ) ∧ 𝑦 ∈ ∪ ( 𝑆 ↾t 𝐷 ) ) → ( 𝐹 ‘ 𝑦 ) ∈ ℝ* )
36 3 2 issmfle ⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) → ( 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ↔ ( 𝐷 ⊆ ∪ 𝑆 ∧ 𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑐 ∈ ℝ { 𝑦 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑦 ) ≤ 𝑐 } ∈ ( 𝑆 ↾t 𝐷 ) ) ) )
37 4 36 mpbid ⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) → ( 𝐷 ⊆ ∪ 𝑆 ∧ 𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑐 ∈ ℝ { 𝑦 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑦 ) ≤ 𝑐 } ∈ ( 𝑆 ↾t 𝐷 ) ) )
38 37 simp3d ⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) → ∀ 𝑐 ∈ ℝ { 𝑦 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑦 ) ≤ 𝑐 } ∈ ( 𝑆 ↾t 𝐷 ) )
39 10 rabeqdv ⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) → { 𝑦 ∈ ∪ ( 𝑆 ↾t 𝐷 ) ∣ ( 𝐹 ‘ 𝑦 ) ≤ 𝑐 } = { 𝑦 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑦 ) ≤ 𝑐 } )
40 39 eleq1d ⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) → ( { 𝑦 ∈ ∪ ( 𝑆 ↾t 𝐷 ) ∣ ( 𝐹 ‘ 𝑦 ) ≤ 𝑐 } ∈ ( 𝑆 ↾t 𝐷 ) ↔ { 𝑦 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑦 ) ≤ 𝑐 } ∈ ( 𝑆 ↾t 𝐷 ) ) )
41 40 ralbidv ⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) → ( ∀ 𝑐 ∈ ℝ { 𝑦 ∈ ∪ ( 𝑆 ↾t 𝐷 ) ∣ ( 𝐹 ‘ 𝑦 ) ≤ 𝑐 } ∈ ( 𝑆 ↾t 𝐷 ) ↔ ∀ 𝑐 ∈ ℝ { 𝑦 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝑦 ) ≤ 𝑐 } ∈ ( 𝑆 ↾t 𝐷 ) ) )
42 38 41 mpbird ⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) → ∀ 𝑐 ∈ ℝ { 𝑦 ∈ ∪ ( 𝑆 ↾t 𝐷 ) ∣ ( 𝐹 ‘ 𝑦 ) ≤ 𝑐 } ∈ ( 𝑆 ↾t 𝐷 ) )
43 42 adantr ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) ∧ 𝑐 ∈ ℝ ) → ∀ 𝑐 ∈ ℝ { 𝑦 ∈ ∪ ( 𝑆 ↾t 𝐷 ) ∣ ( 𝐹 ‘ 𝑦 ) ≤ 𝑐 } ∈ ( 𝑆 ↾t 𝐷 ) )
44 simpr ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) ∧ 𝑐 ∈ ℝ ) → 𝑐 ∈ ℝ )
45 rspa ⊢ ( ( ∀ 𝑐 ∈ ℝ { 𝑦 ∈ ∪ ( 𝑆 ↾t 𝐷 ) ∣ ( 𝐹 ‘ 𝑦 ) ≤ 𝑐 } ∈ ( 𝑆 ↾t 𝐷 ) ∧ 𝑐 ∈ ℝ ) → { 𝑦 ∈ ∪ ( 𝑆 ↾t 𝐷 ) ∣ ( 𝐹 ‘ 𝑦 ) ≤ 𝑐 } ∈ ( 𝑆 ↾t 𝐷 ) )
46 43 44 45 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) ∧ 𝑐 ∈ ℝ ) → { 𝑦 ∈ ∪ ( 𝑆 ↾t 𝐷 ) ∣ ( 𝐹 ‘ 𝑦 ) ≤ 𝑐 } ∈ ( 𝑆 ↾t 𝐷 ) )
47 46 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) ∧ 𝑏 ∈ ℝ ) ∧ 𝑐 ∈ ℝ ) → { 𝑦 ∈ ∪ ( 𝑆 ↾t 𝐷 ) ∣ ( 𝐹 ‘ 𝑦 ) ≤ 𝑐 } ∈ ( 𝑆 ↾t 𝐷 ) )
48 simpr ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) ∧ 𝑏 ∈ ℝ ) → 𝑏 ∈ ℝ )
49 18 19 27 28 35 47 48 salpreimalegt ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) ∧ 𝑏 ∈ ℝ ) → { 𝑦 ∈ ∪ ( 𝑆 ↾t 𝐷 ) ∣ 𝑏 < ( 𝐹 ‘ 𝑦 ) } ∈ ( 𝑆 ↾t 𝐷 ) )
50 13 49 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) ∧ 𝑏 ∈ ℝ ) → { 𝑦 ∈ 𝐷 ∣ 𝑏 < ( 𝐹 ‘ 𝑦 ) } ∈ ( 𝑆 ↾t 𝐷 ) )
51 50 ex ⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) → ( 𝑏 ∈ ℝ → { 𝑦 ∈ 𝐷 ∣ 𝑏 < ( 𝐹 ‘ 𝑦 ) } ∈ ( 𝑆 ↾t 𝐷 ) ) )
52 9 51 ralrimi ⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) → ∀ 𝑏 ∈ ℝ { 𝑦 ∈ 𝐷 ∣ 𝑏 < ( 𝐹 ‘ 𝑦 ) } ∈ ( 𝑆 ↾t 𝐷 ) )
53 5 6 52 3jca ⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) → ( 𝐷 ⊆ ∪ 𝑆 ∧ 𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑏 ∈ ℝ { 𝑦 ∈ 𝐷 ∣ 𝑏 < ( 𝐹 ‘ 𝑦 ) } ∈ ( 𝑆 ↾t 𝐷 ) ) )
54 53 ex ⊢ ( 𝜑 → ( 𝐹 ∈ ( SMblFn ‘ 𝑆 ) → ( 𝐷 ⊆ ∪ 𝑆 ∧ 𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑏 ∈ ℝ { 𝑦 ∈ 𝐷 ∣ 𝑏 < ( 𝐹 ‘ 𝑦 ) } ∈ ( 𝑆 ↾t 𝐷 ) ) ) )
55 nfv ⊢ Ⅎ 𝑦 𝐷 ⊆ ∪ 𝑆
56 nfv ⊢ Ⅎ 𝑦 𝐹 : 𝐷 ⟶ ℝ
57 nfcv ⊢ Ⅎ 𝑦 ℝ
58 nfrab1 ⊢ Ⅎ 𝑦 { 𝑦 ∈ 𝐷 ∣ 𝑏 < ( 𝐹 ‘ 𝑦 ) }
59 nfcv ⊢ Ⅎ 𝑦 ( 𝑆 ↾t 𝐷 )
60 58 59 nfel ⊢ Ⅎ 𝑦 { 𝑦 ∈ 𝐷 ∣ 𝑏 < ( 𝐹 ‘ 𝑦 ) } ∈ ( 𝑆 ↾t 𝐷 )
61 57 60 nfralw ⊢ Ⅎ 𝑦 ∀ 𝑏 ∈ ℝ { 𝑦 ∈ 𝐷 ∣ 𝑏 < ( 𝐹 ‘ 𝑦 ) } ∈ ( 𝑆 ↾t 𝐷 )
62 55 56 61 nf3an ⊢ Ⅎ 𝑦 ( 𝐷 ⊆ ∪ 𝑆 ∧ 𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑏 ∈ ℝ { 𝑦 ∈ 𝐷 ∣ 𝑏 < ( 𝐹 ‘ 𝑦 ) } ∈ ( 𝑆 ↾t 𝐷 ) )
63 14 62 nfan ⊢ Ⅎ 𝑦 ( 𝜑 ∧ ( 𝐷 ⊆ ∪ 𝑆 ∧ 𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑏 ∈ ℝ { 𝑦 ∈ 𝐷 ∣ 𝑏 < ( 𝐹 ‘ 𝑦 ) } ∈ ( 𝑆 ↾t 𝐷 ) ) )
64 nfv ⊢ Ⅎ 𝑏 𝐷 ⊆ ∪ 𝑆
65 nfv ⊢ Ⅎ 𝑏 𝐹 : 𝐷 ⟶ ℝ
66 nfra1 ⊢ Ⅎ 𝑏 ∀ 𝑏 ∈ ℝ { 𝑦 ∈ 𝐷 ∣ 𝑏 < ( 𝐹 ‘ 𝑦 ) } ∈ ( 𝑆 ↾t 𝐷 )
67 64 65 66 nf3an ⊢ Ⅎ 𝑏 ( 𝐷 ⊆ ∪ 𝑆 ∧ 𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑏 ∈ ℝ { 𝑦 ∈ 𝐷 ∣ 𝑏 < ( 𝐹 ‘ 𝑦 ) } ∈ ( 𝑆 ↾t 𝐷 ) )
68 7 67 nfan ⊢ Ⅎ 𝑏 ( 𝜑 ∧ ( 𝐷 ⊆ ∪ 𝑆 ∧ 𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑏 ∈ ℝ { 𝑦 ∈ 𝐷 ∣ 𝑏 < ( 𝐹 ‘ 𝑦 ) } ∈ ( 𝑆 ↾t 𝐷 ) ) )
69 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝐷 ⊆ ∪ 𝑆 ∧ 𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑏 ∈ ℝ { 𝑦 ∈ 𝐷 ∣ 𝑏 < ( 𝐹 ‘ 𝑦 ) } ∈ ( 𝑆 ↾t 𝐷 ) ) ) → 𝑆 ∈ SAlg )
70 simpr1 ⊢ ( ( 𝜑 ∧ ( 𝐷 ⊆ ∪ 𝑆 ∧ 𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑏 ∈ ℝ { 𝑦 ∈ 𝐷 ∣ 𝑏 < ( 𝐹 ‘ 𝑦 ) } ∈ ( 𝑆 ↾t 𝐷 ) ) ) → 𝐷 ⊆ ∪ 𝑆 )
71 simpr2 ⊢ ( ( 𝜑 ∧ ( 𝐷 ⊆ ∪ 𝑆 ∧ 𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑏 ∈ ℝ { 𝑦 ∈ 𝐷 ∣ 𝑏 < ( 𝐹 ‘ 𝑦 ) } ∈ ( 𝑆 ↾t 𝐷 ) ) ) → 𝐹 : 𝐷 ⟶ ℝ )
72 simpr3 ⊢ ( ( 𝜑 ∧ ( 𝐷 ⊆ ∪ 𝑆 ∧ 𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑏 ∈ ℝ { 𝑦 ∈ 𝐷 ∣ 𝑏 < ( 𝐹 ‘ 𝑦 ) } ∈ ( 𝑆 ↾t 𝐷 ) ) ) → ∀ 𝑏 ∈ ℝ { 𝑦 ∈ 𝐷 ∣ 𝑏 < ( 𝐹 ‘ 𝑦 ) } ∈ ( 𝑆 ↾t 𝐷 ) )
73 63 68 69 2 70 71 72 issmfgtlem ⊢ ( ( 𝜑 ∧ ( 𝐷 ⊆ ∪ 𝑆 ∧ 𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑏 ∈ ℝ { 𝑦 ∈ 𝐷 ∣ 𝑏 < ( 𝐹 ‘ 𝑦 ) } ∈ ( 𝑆 ↾t 𝐷 ) ) ) → 𝐹 ∈ ( SMblFn ‘ 𝑆 ) )
74 73 ex ⊢ ( 𝜑 → ( ( 𝐷 ⊆ ∪ 𝑆 ∧ 𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑏 ∈ ℝ { 𝑦 ∈ 𝐷 ∣ 𝑏 < ( 𝐹 ‘ 𝑦 ) } ∈ ( 𝑆 ↾t 𝐷 ) ) → 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ) )
75 54 74 impbid ⊢ ( 𝜑 → ( 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ↔ ( 𝐷 ⊆ ∪ 𝑆 ∧ 𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑏 ∈ ℝ { 𝑦 ∈ 𝐷 ∣ 𝑏 < ( 𝐹 ‘ 𝑦 ) } ∈ ( 𝑆 ↾t 𝐷 ) ) ) )
76 breq1 ⊢ ( 𝑏 = 𝑎 → ( 𝑏 < ( 𝐹 ‘ 𝑦 ) ↔ 𝑎 < ( 𝐹 ‘ 𝑦 ) ) )
77 76 rabbidv ⊢ ( 𝑏 = 𝑎 → { 𝑦 ∈ 𝐷 ∣ 𝑏 < ( 𝐹 ‘ 𝑦 ) } = { 𝑦 ∈ 𝐷 ∣ 𝑎 < ( 𝐹 ‘ 𝑦 ) } )
78 fveq2 ⊢ ( 𝑦 = 𝑥 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) )
79 78 breq2d ⊢ ( 𝑦 = 𝑥 → ( 𝑎 < ( 𝐹 ‘ 𝑦 ) ↔ 𝑎 < ( 𝐹 ‘ 𝑥 ) ) )
80 79 cbvrabv ⊢ { 𝑦 ∈ 𝐷 ∣ 𝑎 < ( 𝐹 ‘ 𝑦 ) } = { 𝑥 ∈ 𝐷 ∣ 𝑎 < ( 𝐹 ‘ 𝑥 ) }
81 80 a1i ⊢ ( 𝑏 = 𝑎 → { 𝑦 ∈ 𝐷 ∣ 𝑎 < ( 𝐹 ‘ 𝑦 ) } = { 𝑥 ∈ 𝐷 ∣ 𝑎 < ( 𝐹 ‘ 𝑥 ) } )
82 77 81 eqtrd ⊢ ( 𝑏 = 𝑎 → { 𝑦 ∈ 𝐷 ∣ 𝑏 < ( 𝐹 ‘ 𝑦 ) } = { 𝑥 ∈ 𝐷 ∣ 𝑎 < ( 𝐹 ‘ 𝑥 ) } )
83 82 eleq1d ⊢ ( 𝑏 = 𝑎 → ( { 𝑦 ∈ 𝐷 ∣ 𝑏 < ( 𝐹 ‘ 𝑦 ) } ∈ ( 𝑆 ↾t 𝐷 ) ↔ { 𝑥 ∈ 𝐷 ∣ 𝑎 < ( 𝐹 ‘ 𝑥 ) } ∈ ( 𝑆 ↾t 𝐷 ) ) )
84 83 cbvralvw ⊢ ( ∀ 𝑏 ∈ ℝ { 𝑦 ∈ 𝐷 ∣ 𝑏 < ( 𝐹 ‘ 𝑦 ) } ∈ ( 𝑆 ↾t 𝐷 ) ↔ ∀ 𝑎 ∈ ℝ { 𝑥 ∈ 𝐷 ∣ 𝑎 < ( 𝐹 ‘ 𝑥 ) } ∈ ( 𝑆 ↾t 𝐷 ) )
85 84 3anbi3i ⊢ ( ( 𝐷 ⊆ ∪ 𝑆 ∧ 𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑏 ∈ ℝ { 𝑦 ∈ 𝐷 ∣ 𝑏 < ( 𝐹 ‘ 𝑦 ) } ∈ ( 𝑆 ↾t 𝐷 ) ) ↔ ( 𝐷 ⊆ ∪ 𝑆 ∧ 𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑎 ∈ ℝ { 𝑥 ∈ 𝐷 ∣ 𝑎 < ( 𝐹 ‘ 𝑥 ) } ∈ ( 𝑆 ↾t 𝐷 ) ) )
86 85 a1i ⊢ ( 𝜑 → ( ( 𝐷 ⊆ ∪ 𝑆 ∧ 𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑏 ∈ ℝ { 𝑦 ∈ 𝐷 ∣ 𝑏 < ( 𝐹 ‘ 𝑦 ) } ∈ ( 𝑆 ↾t 𝐷 ) ) ↔ ( 𝐷 ⊆ ∪ 𝑆 ∧ 𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑎 ∈ ℝ { 𝑥 ∈ 𝐷 ∣ 𝑎 < ( 𝐹 ‘ 𝑥 ) } ∈ ( 𝑆 ↾t 𝐷 ) ) ) )
87 75 86 bitrd ⊢ ( 𝜑 → ( 𝐹 ∈ ( SMblFn ‘ 𝑆 ) ↔ ( 𝐷 ⊆ ∪ 𝑆 ∧ 𝐹 : 𝐷 ⟶ ℝ ∧ ∀ 𝑎 ∈ ℝ { 𝑥 ∈ 𝐷 ∣ 𝑎 < ( 𝐹 ‘ 𝑥 ) } ∈ ( 𝑆 ↾t 𝐷 ) ) ) )