Theorem smfpimgtxrmptf

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, 20-Dec-2024)

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

Proof

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