# Metamath Proof Explorer

## 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 $⊢ φ → S ∈ SAlg$
smfpimbor1lem2.f $⊢ φ → F ∈ SMblFn ⁡ S$
smfpimbor1lem2.a $⊢ D = dom ⁡ F$
smfpimbor1lem2.j $⊢ J = topGen ⁡ ran ⁡ .$
smfpimbor1lem2.b $⊢ B = SalGen ⁡ J$
smfpimbor1lem2.e $⊢ φ → E ∈ B$
smfpimbor1lem2.p $⊢ P = F -1 E$
smfpimbor1lem2.t $⊢ T = e ∈ 𝒫 ℝ | F -1 e ∈ S ↾ 𝑡 D$
Assertion smfpimbor1lem2 $⊢ φ → P ∈ S ↾ 𝑡 D$

### Proof

Step Hyp Ref Expression
1 smfpimbor1lem2.s $⊢ φ → S ∈ SAlg$
2 smfpimbor1lem2.f $⊢ φ → F ∈ SMblFn ⁡ S$
3 smfpimbor1lem2.a $⊢ D = dom ⁡ F$
4 smfpimbor1lem2.j $⊢ J = topGen ⁡ ran ⁡ .$
5 smfpimbor1lem2.b $⊢ B = SalGen ⁡ J$
6 smfpimbor1lem2.e $⊢ φ → E ∈ B$
7 smfpimbor1lem2.p $⊢ P = F -1 E$
8 smfpimbor1lem2.t $⊢ T = e ∈ 𝒫 ℝ | F -1 e ∈ S ↾ 𝑡 D$
9 retop $⊢ topGen ⁡ ran ⁡ . ∈ Top$
10 4 9 eqeltri $⊢ J ∈ Top$
11 10 a1i $⊢ φ → J ∈ Top$
12 1 2 3 8 smfresal $⊢ φ → T ∈ SAlg$
13 1 adantr $⊢ φ ∧ x ∈ J → S ∈ SAlg$
14 2 adantr $⊢ φ ∧ x ∈ J → F ∈ SMblFn ⁡ S$
15 simpr $⊢ φ ∧ x ∈ J → x ∈ J$
16 13 14 3 4 15 8 smfpimbor1lem1 $⊢ φ ∧ x ∈ J → x ∈ T$
17 16 ssd $⊢ φ → J ⊆ T$
18 nfcv $⊢ Ⅎ _ e x$
19 nfrab1 $⊢ Ⅎ _ e e ∈ 𝒫 ℝ | F -1 e ∈ S ↾ 𝑡 D$
20 8 19 nfcxfr $⊢ Ⅎ _ e T$
21 18 20 eluni2f $⊢ x ∈ ⋃ T ↔ ∃ e ∈ T x ∈ e$
22 21 biimpi $⊢ x ∈ ⋃ T → ∃ e ∈ T x ∈ e$
23 20 nfuni $⊢ Ⅎ _ e ⋃ T$
24 18 23 nfel $⊢ Ⅎ e x ∈ ⋃ T$
25 nfv $⊢ Ⅎ e x ∈ ℝ$
26 8 eleq2i $⊢ e ∈ T ↔ e ∈ e ∈ 𝒫 ℝ | F -1 e ∈ S ↾ 𝑡 D$
27 26 biimpi $⊢ e ∈ T → e ∈ e ∈ 𝒫 ℝ | F -1 e ∈ S ↾ 𝑡 D$
28 rabidim1 $⊢ e ∈ e ∈ 𝒫 ℝ | F -1 e ∈ S ↾ 𝑡 D → e ∈ 𝒫 ℝ$
29 27 28 syl $⊢ e ∈ T → e ∈ 𝒫 ℝ$
30 elpwi $⊢ e ∈ 𝒫 ℝ → e ⊆ ℝ$
31 29 30 syl $⊢ e ∈ T → e ⊆ ℝ$
32 31 adantr $⊢ e ∈ T ∧ x ∈ e → e ⊆ ℝ$
33 simpr $⊢ e ∈ T ∧ x ∈ e → x ∈ e$
34 32 33 sseldd $⊢ e ∈ T ∧ x ∈ e → x ∈ ℝ$
35 34 ex $⊢ e ∈ T → x ∈ e → x ∈ ℝ$
36 35 a1i $⊢ x ∈ ⋃ T → e ∈ T → x ∈ e → x ∈ ℝ$
37 24 25 36 rexlimd $⊢ x ∈ ⋃ T → ∃ e ∈ T x ∈ e → x ∈ ℝ$
38 22 37 mpd $⊢ x ∈ ⋃ T → x ∈ ℝ$
39 38 rgen $⊢ ∀ x ∈ ⋃ T x ∈ ℝ$
40 dfss3 $⊢ ⋃ T ⊆ ℝ ↔ ∀ x ∈ ⋃ T x ∈ ℝ$
41 39 40 mpbir $⊢ ⋃ T ⊆ ℝ$
42 41 a1i $⊢ φ → ⋃ T ⊆ ℝ$
43 uniretop $⊢ ℝ = ⋃ topGen ⁡ ran ⁡ .$
44 4 eqcomi $⊢ topGen ⁡ ran ⁡ . = J$
45 44 unieqi $⊢ ⋃ topGen ⁡ ran ⁡ . = ⋃ J$
46 43 45 eqtr2i $⊢ ⋃ J = ℝ$
47 46 a1i $⊢ φ → ⋃ J = ℝ$
48 47 eqcomd $⊢ φ → ℝ = ⋃ J$
49 17 unissd $⊢ φ → ⋃ J ⊆ ⋃ T$
50 48 49 eqsstrd $⊢ φ → ℝ ⊆ ⋃ T$
51 42 50 eqssd $⊢ φ → ⋃ T = ℝ$
52 51 47 eqtr4d $⊢ φ → ⋃ T = ⋃ J$
53 11 5 12 17 52 salgenss $⊢ φ → B ⊆ T$
54 53 6 sseldd $⊢ φ → E ∈ T$
55 imaeq2 $⊢ e = E → F -1 e = F -1 E$
56 55 eleq1d $⊢ e = E → F -1 e ∈ S ↾ 𝑡 D ↔ F -1 E ∈ S ↾ 𝑡 D$
57 56 8 elrab2 $⊢ E ∈ T ↔ E ∈ 𝒫 ℝ ∧ F -1 E ∈ S ↾ 𝑡 D$
58 54 57 sylib $⊢ φ → E ∈ 𝒫 ℝ ∧ F -1 E ∈ S ↾ 𝑡 D$
59 58 simprd $⊢ φ → F -1 E ∈ S ↾ 𝑡 D$
60 7 59 eqeltrid $⊢ φ → P ∈ S ↾ 𝑡 D$