Theorem smfpimbor1lem2

Description: Given a sigma-measurable function, the preimage of a Borel set belongs to the subspace sigma-algebra induced by the domain of the function. Proposition 121E (f) of Fremlin1 p. 37 . (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	smfpimbor1lem2.s	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
	smfpimbor1lem2.f	⊢ ( 𝜑 → 𝐹 ∈ ( SMblFn ‘ 𝑆 ) )
	smfpimbor1lem2.a	⊢ 𝐷 = dom 𝐹
	smfpimbor1lem2.j	⊢ 𝐽 = ( topGen ‘ ran (,) )
	smfpimbor1lem2.b	⊢ 𝐵 = ( SalGen ‘ 𝐽 )
	smfpimbor1lem2.e	⊢ ( 𝜑 → 𝐸 ∈ 𝐵 )
	smfpimbor1lem2.p	⊢ 𝑃 = ( ◡ 𝐹 “ 𝐸 )
	smfpimbor1lem2.t	⊢ 𝑇 = { 𝑒 ∈ 𝒫 ℝ ∣ ( ◡ 𝐹 “ 𝑒 ) ∈ ( 𝑆 ↾t 𝐷 ) }
Assertion	smfpimbor1lem2	⊢ ( 𝜑 → 𝑃 ∈ ( 𝑆 ↾t 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		smfpimbor1lem2.s	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
2		smfpimbor1lem2.f	⊢ ( 𝜑 → 𝐹 ∈ ( SMblFn ‘ 𝑆 ) )
3		smfpimbor1lem2.a	⊢ 𝐷 = dom 𝐹
4		smfpimbor1lem2.j	⊢ 𝐽 = ( topGen ‘ ran (,) )
5		smfpimbor1lem2.b	⊢ 𝐵 = ( SalGen ‘ 𝐽 )
6		smfpimbor1lem2.e	⊢ ( 𝜑 → 𝐸 ∈ 𝐵 )
7		smfpimbor1lem2.p	⊢ 𝑃 = ( ◡ 𝐹 “ 𝐸 )
8		smfpimbor1lem2.t	⊢ 𝑇 = { 𝑒 ∈ 𝒫 ℝ ∣ ( ◡ 𝐹 “ 𝑒 ) ∈ ( 𝑆 ↾t 𝐷 ) }
9		retop	⊢ ( topGen ‘ ran (,) ) ∈ Top
10	4 9	eqeltri	⊢ 𝐽 ∈ Top
11	10	a1i	⊢ ( 𝜑 → 𝐽 ∈ Top )
12	1 2 3 8	smfresal	⊢ ( 𝜑 → 𝑇 ∈ SAlg )
13	1	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐽 ) → 𝑆 ∈ SAlg )
14	2	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐽 ) → 𝐹 ∈ ( SMblFn ‘ 𝑆 ) )
15		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐽 ) → 𝑥 ∈ 𝐽 )
16	13 14 3 4 15 8	smfpimbor1lem1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐽 ) → 𝑥 ∈ 𝑇 )
17	16	ssd	⊢ ( 𝜑 → 𝐽 ⊆ 𝑇 )
18		nfcv	⊢ Ⅎ 𝑒 𝑥
19		nfrab1	⊢ Ⅎ 𝑒 { 𝑒 ∈ 𝒫 ℝ ∣ ( ◡ 𝐹 “ 𝑒 ) ∈ ( 𝑆 ↾t 𝐷 ) }
20	8 19	nfcxfr	⊢ Ⅎ 𝑒 𝑇
21	18 20	eluni2f	⊢ ( 𝑥 ∈ ∪ 𝑇 ↔ ∃ 𝑒 ∈ 𝑇 𝑥 ∈ 𝑒 )
22	21	biimpi	⊢ ( 𝑥 ∈ ∪ 𝑇 → ∃ 𝑒 ∈ 𝑇 𝑥 ∈ 𝑒 )
23	20	nfuni	⊢ Ⅎ 𝑒 ∪ 𝑇
24	18 23	nfel	⊢ Ⅎ 𝑒 𝑥 ∈ ∪ 𝑇
25		nfv	⊢ Ⅎ 𝑒 𝑥 ∈ ℝ
26	8	eleq2i	⊢ ( 𝑒 ∈ 𝑇 ↔ 𝑒 ∈ { 𝑒 ∈ 𝒫 ℝ ∣ ( ◡ 𝐹 “ 𝑒 ) ∈ ( 𝑆 ↾t 𝐷 ) } )
27	26	biimpi	⊢ ( 𝑒 ∈ 𝑇 → 𝑒 ∈ { 𝑒 ∈ 𝒫 ℝ ∣ ( ◡ 𝐹 “ 𝑒 ) ∈ ( 𝑆 ↾t 𝐷 ) } )
28		rabidim1	⊢ ( 𝑒 ∈ { 𝑒 ∈ 𝒫 ℝ ∣ ( ◡ 𝐹 “ 𝑒 ) ∈ ( 𝑆 ↾t 𝐷 ) } → 𝑒 ∈ 𝒫 ℝ )
29	27 28	syl	⊢ ( 𝑒 ∈ 𝑇 → 𝑒 ∈ 𝒫 ℝ )
30		elpwi	⊢ ( 𝑒 ∈ 𝒫 ℝ → 𝑒 ⊆ ℝ )
31	29 30	syl	⊢ ( 𝑒 ∈ 𝑇 → 𝑒 ⊆ ℝ )
32	31	adantr	⊢ ( ( 𝑒 ∈ 𝑇 ∧ 𝑥 ∈ 𝑒 ) → 𝑒 ⊆ ℝ )
33		simpr	⊢ ( ( 𝑒 ∈ 𝑇 ∧ 𝑥 ∈ 𝑒 ) → 𝑥 ∈ 𝑒 )
34	32 33	sseldd	⊢ ( ( 𝑒 ∈ 𝑇 ∧ 𝑥 ∈ 𝑒 ) → 𝑥 ∈ ℝ )
35	34	ex	⊢ ( 𝑒 ∈ 𝑇 → ( 𝑥 ∈ 𝑒 → 𝑥 ∈ ℝ ) )
36	35	a1i	⊢ ( 𝑥 ∈ ∪ 𝑇 → ( 𝑒 ∈ 𝑇 → ( 𝑥 ∈ 𝑒 → 𝑥 ∈ ℝ ) ) )
37	24 25 36	rexlimd	⊢ ( 𝑥 ∈ ∪ 𝑇 → ( ∃ 𝑒 ∈ 𝑇 𝑥 ∈ 𝑒 → 𝑥 ∈ ℝ ) )
38	22 37	mpd	⊢ ( 𝑥 ∈ ∪ 𝑇 → 𝑥 ∈ ℝ )
39	38	rgen	⊢ ∀ 𝑥 ∈ ∪ 𝑇 𝑥 ∈ ℝ
40		dfss3	⊢ ( ∪ 𝑇 ⊆ ℝ ↔ ∀ 𝑥 ∈ ∪ 𝑇 𝑥 ∈ ℝ )
41	39 40	mpbir	⊢ ∪ 𝑇 ⊆ ℝ
42	41	a1i	⊢ ( 𝜑 → ∪ 𝑇 ⊆ ℝ )
43		uniretop	⊢ ℝ = ∪ ( topGen ‘ ran (,) )
44	4	eqcomi	⊢ ( topGen ‘ ran (,) ) = 𝐽
45	44	unieqi	⊢ ∪ ( topGen ‘ ran (,) ) = ∪ 𝐽
46	43 45	eqtr2i	⊢ ∪ 𝐽 = ℝ
47	46	a1i	⊢ ( 𝜑 → ∪ 𝐽 = ℝ )
48	47	eqcomd	⊢ ( 𝜑 → ℝ = ∪ 𝐽 )
49	17	unissd	⊢ ( 𝜑 → ∪ 𝐽 ⊆ ∪ 𝑇 )
50	48 49	eqsstrd	⊢ ( 𝜑 → ℝ ⊆ ∪ 𝑇 )
51	42 50	eqssd	⊢ ( 𝜑 → ∪ 𝑇 = ℝ )
52	51 47	eqtr4d	⊢ ( 𝜑 → ∪ 𝑇 = ∪ 𝐽 )
53	11 5 12 17 52	salgenss	⊢ ( 𝜑 → 𝐵 ⊆ 𝑇 )
54	53 6	sseldd	⊢ ( 𝜑 → 𝐸 ∈ 𝑇 )
55		imaeq2	⊢ ( 𝑒 = 𝐸 → ( ◡ 𝐹 “ 𝑒 ) = ( ◡ 𝐹 “ 𝐸 ) )
56	55	eleq1d	⊢ ( 𝑒 = 𝐸 → ( ( ◡ 𝐹 “ 𝑒 ) ∈ ( 𝑆 ↾t 𝐷 ) ↔ ( ◡ 𝐹 “ 𝐸 ) ∈ ( 𝑆 ↾t 𝐷 ) ) )
57	56 8	elrab2	⊢ ( 𝐸 ∈ 𝑇 ↔ ( 𝐸 ∈ 𝒫 ℝ ∧ ( ◡ 𝐹 “ 𝐸 ) ∈ ( 𝑆 ↾t 𝐷 ) ) )
58	54 57	sylib	⊢ ( 𝜑 → ( 𝐸 ∈ 𝒫 ℝ ∧ ( ◡ 𝐹 “ 𝐸 ) ∈ ( 𝑆 ↾t 𝐷 ) ) )
59	58	simprd	⊢ ( 𝜑 → ( ◡ 𝐹 “ 𝐸 ) ∈ ( 𝑆 ↾t 𝐷 ) )
60	7 59	eqeltrid	⊢ ( 𝜑 → 𝑃 ∈ ( 𝑆 ↾t 𝐷 ) )