Theorem smfpimltxrmpt

Description: Given a function measurable w.r.t. to a sigma-algebra, the preimage of an open interval unbounded below is in the subspace sigma-algebra induced by its domain. (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	smfpimltxrmpt.x	⊢ Ⅎ 𝑥 𝜑
	smfpimltxrmpt.s	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
	smfpimltxrmpt.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
	smfpimltxrmpt.f	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ( SMblFn ‘ 𝑆 ) )
	smfpimltxrmpt.r	⊢ ( 𝜑 → 𝑅 ∈ ℝ* )
Assertion	smfpimltxrmpt	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅 } ∈ ( 𝑆 ↾t 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		smfpimltxrmpt.x	⊢ Ⅎ 𝑥 𝜑
2		smfpimltxrmpt.s	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
3		smfpimltxrmpt.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
4		smfpimltxrmpt.f	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ( SMblFn ‘ 𝑆 ) )
5		smfpimltxrmpt.r	⊢ ( 𝜑 → 𝑅 ∈ ℝ* )
6		nfmpt1	⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
7	6	nfdm	⊢ Ⅎ 𝑥 dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
8		nfcv	⊢ Ⅎ 𝑦 dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
9		nfv	⊢ Ⅎ 𝑦 ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) < 𝑅
10		nfcv	⊢ Ⅎ 𝑥 𝑦
11	6 10	nffv	⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 )
12		nfcv	⊢ Ⅎ 𝑥 <
13		nfcv	⊢ Ⅎ 𝑥 𝑅
14	11 12 13	nfbr	⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) < 𝑅
15		fveq2	⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) )
16	15	breq1d	⊢ ( 𝑥 = 𝑦 → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) < 𝑅 ↔ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) < 𝑅 ) )
17	7 8 9 14 16	cbvrabw	⊢ { 𝑥 ∈ dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∣ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) < 𝑅 } = { 𝑦 ∈ dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∣ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) < 𝑅 }
18	17	a1i	⊢ ( 𝜑 → { 𝑥 ∈ dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∣ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) < 𝑅 } = { 𝑦 ∈ dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∣ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) < 𝑅 } )
19		nfcv	⊢ Ⅎ 𝑦 ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
20		eqid	⊢ dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
21	19 2 4 20 5	smfpimltxr	⊢ ( 𝜑 → { 𝑦 ∈ dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∣ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) < 𝑅 } ∈ ( 𝑆 ↾t dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) )
22	18 21	eqeltrd	⊢ ( 𝜑 → { 𝑥 ∈ dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∣ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) < 𝑅 } ∈ ( 𝑆 ↾t dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) )
23		eqid	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
24	1 23 3	dmmptdf	⊢ ( 𝜑 → dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = 𝐴 )
25		nfcv	⊢ Ⅎ 𝑥 𝐴
26	7 25	rabeqf	⊢ ( dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = 𝐴 → { 𝑥 ∈ dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∣ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) < 𝑅 } = { 𝑥 ∈ 𝐴 ∣ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) < 𝑅 } )
27	24 26	syl	⊢ ( 𝜑 → { 𝑥 ∈ dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∣ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) < 𝑅 } = { 𝑥 ∈ 𝐴 ∣ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) < 𝑅 } )
28	23	a1i	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
29	28 3	fvmpt2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) = 𝐵 )
30	29	breq1d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) < 𝑅 ↔ 𝐵 < 𝑅 ) )
31	1 30	rabbida	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) < 𝑅 } = { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅 } )
32		eqidd	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅 } = { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅 } )
33	27 31 32	3eqtrrd	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅 } = { 𝑥 ∈ dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∣ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) < 𝑅 } )
34	24	eqcomd	⊢ ( 𝜑 → 𝐴 = dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
35	34	oveq2d	⊢ ( 𝜑 → ( 𝑆 ↾t 𝐴 ) = ( 𝑆 ↾t dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) )
36	33 35	eleq12d	⊢ ( 𝜑 → ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅 } ∈ ( 𝑆 ↾t 𝐴 ) ↔ { 𝑥 ∈ dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∣ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) < 𝑅 } ∈ ( 𝑆 ↾t dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ) )
37	22 36	mpbird	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑅 } ∈ ( 𝑆 ↾t 𝐴 ) )