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	$⊢ φ \to S \in SAlg$
	smfpimbor1lem2.f	$⊢ φ \to F \in SMblFn (S)$
	smfpimbor1lem2.a	$⊢ D = dom F$
	smfpimbor1lem2.j	$⊢ J = topGen (ran (.))$
	smfpimbor1lem2.b	$⊢ B = SalGen (J)$
	smfpimbor1lem2.e	$⊢ φ \to E \in B$
	smfpimbor1lem2.p	$⊢ P = F^{-1} [E]$
	smfpimbor1lem2.t	$⊢ T = \{e \in 𝒫 ℝ \| F^{-1} [e] \in (S ↾_{𝑡} D)\}$
Assertion	smfpimbor1lem2	$⊢ φ \to P \in (S ↾_{𝑡} D)$

Proof

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

Metamath Proof Explorer

Theorem smfpimbor1lem2

Proof