Theorem smfres

Description: The restriction of sigma-measurable function is sigma-measurable. Proposition 121E (h) of Fremlin1 p. 37 . (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	smfres.s	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
	smfres.f	⊢ ( 𝜑 → 𝐹 ∈ ( SMblFn ‘ 𝑆 ) )
	smfres.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
Assertion	smfres	⊢ ( 𝜑 → ( 𝐹 ↾ 𝐴 ) ∈ ( SMblFn ‘ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		smfres.s	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
2		smfres.f	⊢ ( 𝜑 → 𝐹 ∈ ( SMblFn ‘ 𝑆 ) )
3		smfres.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
4		nfv	⊢ Ⅎ 𝑎 𝜑
5		inss1	⊢ ( dom 𝐹 ∩ 𝐴 ) ⊆ dom 𝐹
6	5	a1i	⊢ ( 𝜑 → ( dom 𝐹 ∩ 𝐴 ) ⊆ dom 𝐹 )
7		eqid	⊢ dom 𝐹 = dom 𝐹
8	1 2 7	smfdmss	⊢ ( 𝜑 → dom 𝐹 ⊆ ∪ 𝑆 )
9	6 8	sstrd	⊢ ( 𝜑 → ( dom 𝐹 ∩ 𝐴 ) ⊆ ∪ 𝑆 )
10	1 2 7	smff	⊢ ( 𝜑 → 𝐹 : dom 𝐹 ⟶ ℝ )
11		fresin	⊢ ( 𝐹 : dom 𝐹 ⟶ ℝ → ( 𝐹 ↾ 𝐴 ) : ( dom 𝐹 ∩ 𝐴 ) ⟶ ℝ )
12	10 11	syl	⊢ ( 𝜑 → ( 𝐹 ↾ 𝐴 ) : ( dom 𝐹 ∩ 𝐴 ) ⟶ ℝ )
13		ovexd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → ( 𝑆 ↾t dom 𝐹 ) ∈ V )
14	3	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → 𝐴 ∈ 𝑉 )
15	1	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → 𝑆 ∈ SAlg )
16	2	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → 𝐹 ∈ ( SMblFn ‘ 𝑆 ) )
17		mnfxr	⊢ -∞ ∈ ℝ*
18	17	a1i	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → -∞ ∈ ℝ* )
19		rexr	⊢ ( 𝑎 ∈ ℝ → 𝑎 ∈ ℝ* )
20	19	adantl	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → 𝑎 ∈ ℝ* )
21	15 16 7 18 20	smfpimioo	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → ( ◡ 𝐹 “ ( -∞ (,) 𝑎 ) ) ∈ ( 𝑆 ↾t dom 𝐹 ) )
22		eqid	⊢ ( ( ◡ 𝐹 “ ( -∞ (,) 𝑎 ) ) ∩ 𝐴 ) = ( ( ◡ 𝐹 “ ( -∞ (,) 𝑎 ) ) ∩ 𝐴 )
23	13 14 21 22	elrestd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → ( ( ◡ 𝐹 “ ( -∞ (,) 𝑎 ) ) ∩ 𝐴 ) ∈ ( ( 𝑆 ↾t dom 𝐹 ) ↾t 𝐴 ) )
24	10	ffund	⊢ ( 𝜑 → Fun 𝐹 )
25		respreima	⊢ ( Fun 𝐹 → ( ◡ ( 𝐹 ↾ 𝐴 ) “ ( -∞ (,) 𝑎 ) ) = ( ( ◡ 𝐹 “ ( -∞ (,) 𝑎 ) ) ∩ 𝐴 ) )
26	24 25	syl	⊢ ( 𝜑 → ( ◡ ( 𝐹 ↾ 𝐴 ) “ ( -∞ (,) 𝑎 ) ) = ( ( ◡ 𝐹 “ ( -∞ (,) 𝑎 ) ) ∩ 𝐴 ) )
27	26	eqcomd	⊢ ( 𝜑 → ( ( ◡ 𝐹 “ ( -∞ (,) 𝑎 ) ) ∩ 𝐴 ) = ( ◡ ( 𝐹 ↾ 𝐴 ) “ ( -∞ (,) 𝑎 ) ) )
28	27	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → ( ( ◡ 𝐹 “ ( -∞ (,) 𝑎 ) ) ∩ 𝐴 ) = ( ◡ ( 𝐹 ↾ 𝐴 ) “ ( -∞ (,) 𝑎 ) ) )
29	12	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → ( 𝐹 ↾ 𝐴 ) : ( dom 𝐹 ∩ 𝐴 ) ⟶ ℝ )
30	29 20	preimaioomnf	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → ( ◡ ( 𝐹 ↾ 𝐴 ) “ ( -∞ (,) 𝑎 ) ) = { 𝑥 ∈ ( dom 𝐹 ∩ 𝐴 ) ∣ ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) < 𝑎 } )
31	28 30	eqtr2d	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → { 𝑥 ∈ ( dom 𝐹 ∩ 𝐴 ) ∣ ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) < 𝑎 } = ( ( ◡ 𝐹 “ ( -∞ (,) 𝑎 ) ) ∩ 𝐴 ) )
32	2	dmexd	⊢ ( 𝜑 → dom 𝐹 ∈ V )
33		restco	⊢ ( ( 𝑆 ∈ SAlg ∧ dom 𝐹 ∈ V ∧ 𝐴 ∈ 𝑉 ) → ( ( 𝑆 ↾t dom 𝐹 ) ↾t 𝐴 ) = ( 𝑆 ↾t ( dom 𝐹 ∩ 𝐴 ) ) )
34	1 32 3 33	syl3anc	⊢ ( 𝜑 → ( ( 𝑆 ↾t dom 𝐹 ) ↾t 𝐴 ) = ( 𝑆 ↾t ( dom 𝐹 ∩ 𝐴 ) ) )
35	34	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → ( ( 𝑆 ↾t dom 𝐹 ) ↾t 𝐴 ) = ( 𝑆 ↾t ( dom 𝐹 ∩ 𝐴 ) ) )
36	35	eqcomd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → ( 𝑆 ↾t ( dom 𝐹 ∩ 𝐴 ) ) = ( ( 𝑆 ↾t dom 𝐹 ) ↾t 𝐴 ) )
37	31 36	eleq12d	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → ( { 𝑥 ∈ ( dom 𝐹 ∩ 𝐴 ) ∣ ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) < 𝑎 } ∈ ( 𝑆 ↾t ( dom 𝐹 ∩ 𝐴 ) ) ↔ ( ( ◡ 𝐹 “ ( -∞ (,) 𝑎 ) ) ∩ 𝐴 ) ∈ ( ( 𝑆 ↾t dom 𝐹 ) ↾t 𝐴 ) ) )
38	23 37	mpbird	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) → { 𝑥 ∈ ( dom 𝐹 ∩ 𝐴 ) ∣ ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) < 𝑎 } ∈ ( 𝑆 ↾t ( dom 𝐹 ∩ 𝐴 ) ) )
39	4 1 9 12 38	issmfd	⊢ ( 𝜑 → ( 𝐹 ↾ 𝐴 ) ∈ ( SMblFn ‘ 𝑆 ) )