Theorem smfpimgtxrmpt

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

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

Proof

Step	Hyp	Ref	Expression
1		smfpimgtxrmpt.x	⊢ Ⅎ 𝑥 𝜑
2		smfpimgtxrmpt.s	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
3		smfpimgtxrmpt.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
4		smfpimgtxrmpt.f	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ( SMblFn ‘ 𝑆 ) )
5		smfpimgtxrmpt.l	⊢ ( 𝜑 → 𝐿 ∈ ℝ* )
6		nfmpt1	⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
7	6	nfdm	⊢ Ⅎ 𝑥 dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
8		nfcv	⊢ Ⅎ 𝑦 dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
9		nfv	⊢ Ⅎ 𝑦 𝐿 < ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 )
10		nfcv	⊢ Ⅎ 𝑥 𝐿
11		nfcv	⊢ Ⅎ 𝑥 <
12		nfcv	⊢ Ⅎ 𝑥 𝑦
13	6 12	nffv	⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 )
14	10 11 13	nfbr	⊢ Ⅎ 𝑥 𝐿 < ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 )
15		fveq2	⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) )
16	15	breq2d	⊢ ( 𝑥 = 𝑦 → ( 𝐿 < ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ↔ 𝐿 < ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) ) )
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	smfpimgtxr	⊢ ( 𝜑 → { 𝑦 ∈ 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	breq2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐿 < ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ↔ 𝐿 < 𝐵 ) )
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 𝐴 ) )