Theorem smfpimltxrmptf

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

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

Proof

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