smfresal

Description: Given a sigma-measurable function, the subsets of RR whose preimage is in the sigma-algebra induced by the function's domain, form a sigma-algebra. First part of the proof of Proposition 121E (f) of Fremlin1 p. 38 . (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	smfresal.s	$⊢ φ \to S \in SAlg$
	smfresal.f	$⊢ φ \to F \in SMblFn (S)$
	smfresal.d	$⊢ D = dom F$
	smfresal.t	$⊢ T = \{e \in 𝒫 ℝ \| F^{-1} [e] \in (S ↾_{𝑡} D)\}$
Assertion	smfresal	$⊢ φ \to T \in SAlg$

Proof

Step	Hyp	Ref	Expression
1		smfresal.s	$⊢ φ \to S \in SAlg$
2		smfresal.f	$⊢ φ \to F \in SMblFn (S)$
3		smfresal.d	$⊢ D = dom F$
4		smfresal.t	$⊢ T = \{e \in 𝒫 ℝ \| F^{-1} [e] \in (S ↾_{𝑡} D)\}$
5		reex	$⊢ ℝ \in V$
6	5	pwex	$⊢ 𝒫 ℝ \in V$
7	4 6	rabex2	$⊢ T \in V$
8	7	a1i	$⊢ φ \to T \in V$
9		0elpw	$⊢ \emptyset \in 𝒫 ℝ$
10	9	a1i	$⊢ φ \to \emptyset \in 𝒫 ℝ$
11		ima0	$⊢ F^{-1} [\emptyset] = \emptyset$
12	11	a1i	$⊢ φ \to F^{-1} [\emptyset] = \emptyset$
13	1	uniexd	$⊢ φ \to ⋃ S \in V$
14	1 2 3	smfdmss	$⊢ φ \to D \subseteq ⋃ S$
15	13 14	ssexd	$⊢ φ \to D \in V$
16		eqid	$⊢ S ↾_{𝑡} D = S ↾_{𝑡} D$
17	1 15 16	subsalsal	$⊢ φ \to S ↾_{𝑡} D \in SAlg$
18	17	0sald	$⊢ φ \to \emptyset \in (S ↾_{𝑡} D)$
19	12 18	eqeltrd	$⊢ φ \to F^{-1} [\emptyset] \in (S ↾_{𝑡} D)$
20	10 19	jca	$⊢ φ \to (\emptyset \in 𝒫 ℝ \land F^{-1} [\emptyset] \in (S ↾_{𝑡} D))$
21		imaeq2	$⊢ e = \emptyset \to F^{-1} [e] = F^{-1} [\emptyset]$
22	21	eleq1d	$⊢ e = \emptyset \to (F^{-1} [e] \in (S ↾_{𝑡} D) \leftrightarrow F^{-1} [\emptyset] \in (S ↾_{𝑡} D))$
23	22 4	elrab2	$⊢ \emptyset \in T \leftrightarrow (\emptyset \in 𝒫 ℝ \land F^{-1} [\emptyset] \in (S ↾_{𝑡} D))$
24	20 23	sylibr	$⊢ φ \to \emptyset \in T$
25		eqid	$⊢ ⋃ T = ⋃ T$
26		nfv	$⊢ Ⅎ y φ$
27		nfcv	$⊢ \underline{Ⅎ} e y$
28		nfrab1	$⊢ \underline{Ⅎ} e \{e \in 𝒫 ℝ \| F^{-1} [e] \in (S ↾_{𝑡} D)\}$
29	4 28	nfcxfr	$⊢ \underline{Ⅎ} e T$
30	27 29	eluni2f	$⊢ y \in ⋃ T \leftrightarrow \exists e \in T y \in e$
31	30	biimpi	$⊢ y \in ⋃ T \to \exists e \in T y \in e$
32	31	adantl	$⊢ (φ \land y \in ⋃ T) \to \exists e \in T y \in e$
33		nfv	$⊢ Ⅎ e φ$
34	29	nfuni	$⊢ \underline{Ⅎ} e ⋃ T$
35	27 34	nfel	$⊢ Ⅎ e y \in ⋃ T$
36	33 35	nfan	$⊢ Ⅎ e (φ \land y \in ⋃ T)$
37	27	nfel1	$⊢ Ⅎ e y \in ℝ$
38	4	eleq2i	$⊢ e \in T \leftrightarrow e \in \{e \in 𝒫 ℝ \| F^{-1} [e] \in (S ↾_{𝑡} D)\}$
39	38	biimpi	$⊢ e \in T \to e \in \{e \in 𝒫 ℝ \| F^{-1} [e] \in (S ↾_{𝑡} D)\}$
40		rabidim1	$⊢ e \in \{e \in 𝒫 ℝ \| F^{-1} [e] \in (S ↾_{𝑡} D)\} \to e \in 𝒫 ℝ$
41	39 40	syl	$⊢ e \in T \to e \in 𝒫 ℝ$
42		elpwi	$⊢ e \in 𝒫 ℝ \to e \subseteq ℝ$
43	41 42	syl	$⊢ e \in T \to e \subseteq ℝ$
44	43	adantr	$⊢ (e \in T \land y \in e) \to e \subseteq ℝ$
45		simpr	$⊢ (e \in T \land y \in e) \to y \in e$
46	44 45	sseldd	$⊢ (e \in T \land y \in e) \to y \in ℝ$
47	46	ex	$⊢ e \in T \to (y \in e \to y \in ℝ)$
48	47	a1i	$⊢ (φ \land y \in ⋃ T) \to (e \in T \to (y \in e \to y \in ℝ))$
49	36 37 48	rexlimd	$⊢ (φ \land y \in ⋃ T) \to (\exists e \in T y \in e \to y \in ℝ)$
50	32 49	mpd	$⊢ (φ \land y \in ⋃ T) \to y \in ℝ$
51	50	ex	$⊢ φ \to (y \in ⋃ T \to y \in ℝ)$
52		ovexd	$⊢ φ \to (y - 1, y + 1) \in V$
53		ioossre	$⊢ (y - 1, y + 1) \subseteq ℝ$
54	53	a1i	$⊢ φ \to (y - 1, y + 1) \subseteq ℝ$
55	52 54	elpwd	$⊢ φ \to (y - 1, y + 1) \in 𝒫 ℝ$
56	55	adantr	$⊢ (φ \land y \in ℝ) \to (y - 1, y + 1) \in 𝒫 ℝ$
57	1 2 3	smff	$⊢ φ \to F : D ⟶ ℝ$
58	57	ffnd	$⊢ φ \to F Fn D$
59		fncnvima2	$⊢ F Fn D \to F^{-1} [(y - 1, y + 1)] = \{x \in D \| F (x) \in (y - 1, y + 1)\}$
60	58 59	syl	$⊢ φ \to F^{-1} [(y - 1, y + 1)] = \{x \in D \| F (x) \in (y - 1, y + 1)\}$
61	60	adantr	$⊢ (φ \land y \in ℝ) \to F^{-1} [(y - 1, y + 1)] = \{x \in D \| F (x) \in (y - 1, y + 1)\}$
62		nfv	$⊢ Ⅎ x (φ \land y \in ℝ)$
63	1	adantr	$⊢ (φ \land y \in ℝ) \to S \in SAlg$
64	15	adantr	$⊢ (φ \land y \in ℝ) \to D \in V$
65	57	adantr	$⊢ (φ \land x \in D) \to F : D ⟶ ℝ$
66		simpr	$⊢ (φ \land x \in D) \to x \in D$
67	65 66	ffvelcdmd	$⊢ (φ \land x \in D) \to F (x) \in ℝ$
68	67	adantlr	$⊢ ((φ \land y \in ℝ) \land x \in D) \to F (x) \in ℝ$
69	57	feqmptd	$⊢ φ \to F = (x \in D ⟼ F (x))$
70	69	eqcomd	$⊢ φ \to (x \in D ⟼ F (x)) = F$
71	70 2	eqeltrd	$⊢ φ \to (x \in D ⟼ F (x)) \in SMblFn (S)$
72	71	adantr	$⊢ (φ \land y \in ℝ) \to (x \in D ⟼ F (x)) \in SMblFn (S)$
73		peano2rem	$⊢ y \in ℝ \to y - 1 \in ℝ$
74	73	rexrd	$⊢ y \in ℝ \to y - 1 \in ℝ^{*}$
75	74	adantl	$⊢ (φ \land y \in ℝ) \to y - 1 \in ℝ^{*}$
76		peano2re	$⊢ y \in ℝ \to y + 1 \in ℝ$
77	76	rexrd	$⊢ y \in ℝ \to y + 1 \in ℝ^{*}$
78	77	adantl	$⊢ (φ \land y \in ℝ) \to y + 1 \in ℝ^{*}$
79	62 63 64 68 72 75 78	smfpimioompt	$⊢ (φ \land y \in ℝ) \to \{x \in D \| F (x) \in (y - 1, y + 1)\} \in (S ↾_{𝑡} D)$
80	61 79	eqeltrd	$⊢ (φ \land y \in ℝ) \to F^{-1} [(y - 1, y + 1)] \in (S ↾_{𝑡} D)$
81	56 80	jca	$⊢ (φ \land y \in ℝ) \to ((y - 1, y + 1) \in 𝒫 ℝ \land F^{-1} [(y - 1, y + 1)] \in (S ↾_{𝑡} D))$
82		imaeq2	$⊢ e = (y - 1, y + 1) \to F^{-1} [e] = F^{-1} [(y - 1, y + 1)]$
83	82	eleq1d	$⊢ e = (y - 1, y + 1) \to (F^{-1} [e] \in (S ↾_{𝑡} D) \leftrightarrow F^{-1} [(y - 1, y + 1)] \in (S ↾_{𝑡} D))$
84	83 4	elrab2	$⊢ (y - 1, y + 1) \in T \leftrightarrow ((y - 1, y + 1) \in 𝒫 ℝ \land F^{-1} [(y - 1, y + 1)] \in (S ↾_{𝑡} D))$
85	81 84	sylibr	$⊢ (φ \land y \in ℝ) \to (y - 1, y + 1) \in T$
86		id	$⊢ y \in ℝ \to y \in ℝ$
87		ltm1	$⊢ y \in ℝ \to y - 1 < y$
88		ltp1	$⊢ y \in ℝ \to y < y + 1$
89	74 77 86 87 88	eliood	$⊢ y \in ℝ \to y \in (y - 1, y + 1)$
90	89	adantl	$⊢ (φ \land y \in ℝ) \to y \in (y - 1, y + 1)$
91		nfv	$⊢ Ⅎ e y \in (y - 1, y + 1)$
92		nfcv	$⊢ \underline{Ⅎ} e (y - 1, y + 1)$
93		eleq2	$⊢ e = (y - 1, y + 1) \to (y \in e \leftrightarrow y \in (y - 1, y + 1))$
94	91 92 29 93	rspcef	$⊢ ((y - 1, y + 1) \in T \land y \in (y - 1, y + 1)) \to \exists e \in T y \in e$
95	85 90 94	syl2anc	$⊢ (φ \land y \in ℝ) \to \exists e \in T y \in e$
96	95 30	sylibr	$⊢ (φ \land y \in ℝ) \to y \in ⋃ T$
97	96	ex	$⊢ φ \to (y \in ℝ \to y \in ⋃ T)$
98	51 97	impbid	$⊢ φ \to (y \in ⋃ T \leftrightarrow y \in ℝ)$
99	26 98	alrimi	$⊢ φ \to \forall y (y \in ⋃ T \leftrightarrow y \in ℝ)$
100		dfcleq	$⊢ ⋃ T = ℝ \leftrightarrow \forall y (y \in ⋃ T \leftrightarrow y \in ℝ)$
101	99 100	sylibr	$⊢ φ \to ⋃ T = ℝ$
102	101	difeq1d	$⊢ φ \to ⋃ T ∖ x = ℝ ∖ x$
103	102	adantr	$⊢ (φ \land x \in T) \to ⋃ T ∖ x = ℝ ∖ x$
104		difss	$⊢ ℝ ∖ x \subseteq ℝ$
105	5 104	ssexi	$⊢ ℝ ∖ x \in V$
106		elpwg	$⊢ ℝ ∖ x \in V \to (ℝ ∖ x \in 𝒫 ℝ \leftrightarrow ℝ ∖ x \subseteq ℝ)$
107	105 106	ax-mp	$⊢ ℝ ∖ x \in 𝒫 ℝ \leftrightarrow ℝ ∖ x \subseteq ℝ$
108	104 107	mpbir	$⊢ ℝ ∖ x \in 𝒫 ℝ$
109	108	a1i	$⊢ (φ \land x \in T) \to ℝ ∖ x \in 𝒫 ℝ$
110	57	ffund	$⊢ φ \to Fun F$
111		difpreima	$⊢ Fun F \to F^{-1} [ℝ ∖ x] = F^{-1} [ℝ] ∖ F^{-1} [x]$
112	110 111	syl	$⊢ φ \to F^{-1} [ℝ ∖ x] = F^{-1} [ℝ] ∖ F^{-1} [x]$
113		fimacnv	$⊢ F : D ⟶ ℝ \to F^{-1} [ℝ] = D$
114	57 113	syl	$⊢ φ \to F^{-1} [ℝ] = D$
115	1 14	restuni4	$⊢ φ \to ⋃ (S ↾_{𝑡} D) = D$
116	114 115	eqtr4d	$⊢ φ \to F^{-1} [ℝ] = ⋃ (S ↾_{𝑡} D)$
117	116	difeq1d	$⊢ φ \to F^{-1} [ℝ] ∖ F^{-1} [x] = ⋃ (S ↾_{𝑡} D) ∖ F^{-1} [x]$
118	112 117	eqtrd	$⊢ φ \to F^{-1} [ℝ ∖ x] = ⋃ (S ↾_{𝑡} D) ∖ F^{-1} [x]$
119	118	adantr	$⊢ (φ \land x \in T) \to F^{-1} [ℝ ∖ x] = ⋃ (S ↾_{𝑡} D) ∖ F^{-1} [x]$
120	17	adantr	$⊢ (φ \land x \in T) \to S ↾_{𝑡} D \in SAlg$
121		imaeq2	$⊢ e = x \to F^{-1} [e] = F^{-1} [x]$
122	121	eleq1d	$⊢ e = x \to (F^{-1} [e] \in (S ↾_{𝑡} D) \leftrightarrow F^{-1} [x] \in (S ↾_{𝑡} D))$
123	122 4	elrab2	$⊢ x \in T \leftrightarrow (x \in 𝒫 ℝ \land F^{-1} [x] \in (S ↾_{𝑡} D))$
124	123	biimpi	$⊢ x \in T \to (x \in 𝒫 ℝ \land F^{-1} [x] \in (S ↾_{𝑡} D))$
125	124	simprd	$⊢ x \in T \to F^{-1} [x] \in (S ↾_{𝑡} D)$
126	125	adantl	$⊢ (φ \land x \in T) \to F^{-1} [x] \in (S ↾_{𝑡} D)$
127	120 126	saldifcld	$⊢ (φ \land x \in T) \to ⋃ (S ↾_{𝑡} D) ∖ F^{-1} [x] \in (S ↾_{𝑡} D)$
128	119 127	eqeltrd	$⊢ (φ \land x \in T) \to F^{-1} [ℝ ∖ x] \in (S ↾_{𝑡} D)$
129	109 128	jca	$⊢ (φ \land x \in T) \to (ℝ ∖ x \in 𝒫 ℝ \land F^{-1} [ℝ ∖ x] \in (S ↾_{𝑡} D))$
130		imaeq2	$⊢ e = ℝ ∖ x \to F^{-1} [e] = F^{-1} [ℝ ∖ x]$
131	130	eleq1d	$⊢ e = ℝ ∖ x \to (F^{-1} [e] \in (S ↾_{𝑡} D) \leftrightarrow F^{-1} [ℝ ∖ x] \in (S ↾_{𝑡} D))$
132	131 4	elrab2	$⊢ ℝ ∖ x \in T \leftrightarrow (ℝ ∖ x \in 𝒫 ℝ \land F^{-1} [ℝ ∖ x] \in (S ↾_{𝑡} D))$
133	129 132	sylibr	$⊢ (φ \land x \in T) \to ℝ ∖ x \in T$
134	103 133	eqeltrd	$⊢ (φ \land x \in T) \to ⋃ T ∖ x \in T$
135		nnex	$⊢ ℕ \in V$
136		fvex	$⊢ g (n) \in V$
137	135 136	iunex	$⊢ ⋃_{n \in ℕ} g (n) \in V$
138	137	a1i	$⊢ g : ℕ ⟶ T \to ⋃_{n \in ℕ} g (n) \in V$
139		ffvelcdm	$⊢ (g : ℕ ⟶ T \land n \in ℕ) \to g (n) \in T$
140	4	eleq2i	$⊢ g (n) \in T \leftrightarrow g (n) \in \{e \in 𝒫 ℝ \| F^{-1} [e] \in (S ↾_{𝑡} D)\}$
141	140	biimpi	$⊢ g (n) \in T \to g (n) \in \{e \in 𝒫 ℝ \| F^{-1} [e] \in (S ↾_{𝑡} D)\}$
142		elrabi	$⊢ g (n) \in \{e \in 𝒫 ℝ \| F^{-1} [e] \in (S ↾_{𝑡} D)\} \to g (n) \in 𝒫 ℝ$
143		elpwi	$⊢ g (n) \in 𝒫 ℝ \to g (n) \subseteq ℝ$
144	139 141 142 143	4syl	$⊢ (g : ℕ ⟶ T \land n \in ℕ) \to g (n) \subseteq ℝ$
145	144	iunssd	$⊢ g : ℕ ⟶ T \to ⋃_{n \in ℕ} g (n) \subseteq ℝ$
146	138 145	elpwd	$⊢ g : ℕ ⟶ T \to ⋃_{n \in ℕ} g (n) \in 𝒫 ℝ$
147	146	adantl	$⊢ (φ \land g : ℕ ⟶ T) \to ⋃_{n \in ℕ} g (n) \in 𝒫 ℝ$
148		imaiun	$⊢ F^{-1} [⋃_{n \in ℕ} g (n)] = ⋃_{n \in ℕ} F^{-1} [g (n)]$
149	148	a1i	$⊢ (φ \land g : ℕ ⟶ T) \to F^{-1} [⋃_{n \in ℕ} g (n)] = ⋃_{n \in ℕ} F^{-1} [g (n)]$
150	17	adantr	$⊢ (φ \land g : ℕ ⟶ T) \to S ↾_{𝑡} D \in SAlg$
151		nnct	$⊢ ℕ ≼ ω$
152	151	a1i	$⊢ (φ \land g : ℕ ⟶ T) \to ℕ ≼ ω$
153		imaeq2	$⊢ e = g (n) \to F^{-1} [e] = F^{-1} [g (n)]$
154	153	eleq1d	$⊢ e = g (n) \to (F^{-1} [e] \in (S ↾_{𝑡} D) \leftrightarrow F^{-1} [g (n)] \in (S ↾_{𝑡} D))$
155	154 4	elrab2	$⊢ g (n) \in T \leftrightarrow (g (n) \in 𝒫 ℝ \land F^{-1} [g (n)] \in (S ↾_{𝑡} D))$
156	155	biimpi	$⊢ g (n) \in T \to (g (n) \in 𝒫 ℝ \land F^{-1} [g (n)] \in (S ↾_{𝑡} D))$
157	156	simprd	$⊢ g (n) \in T \to F^{-1} [g (n)] \in (S ↾_{𝑡} D)$
158	139 157	syl	$⊢ (g : ℕ ⟶ T \land n \in ℕ) \to F^{-1} [g (n)] \in (S ↾_{𝑡} D)$
159	158	adantll	$⊢ ((φ \land g : ℕ ⟶ T) \land n \in ℕ) \to F^{-1} [g (n)] \in (S ↾_{𝑡} D)$
160	150 152 159	saliuncl	$⊢ (φ \land g : ℕ ⟶ T) \to ⋃_{n \in ℕ} F^{-1} [g (n)] \in (S ↾_{𝑡} D)$
161	149 160	eqeltrd	$⊢ (φ \land g : ℕ ⟶ T) \to F^{-1} [⋃_{n \in ℕ} g (n)] \in (S ↾_{𝑡} D)$
162	147 161	jca	$⊢ (φ \land g : ℕ ⟶ T) \to (⋃_{n \in ℕ} g (n) \in 𝒫 ℝ \land F^{-1} [⋃_{n \in ℕ} g (n)] \in (S ↾_{𝑡} D))$
163		imaeq2	$⊢ e = ⋃_{n \in ℕ} g (n) \to F^{-1} [e] = F^{-1} [⋃_{n \in ℕ} g (n)]$
164	163	eleq1d	$⊢ e = ⋃_{n \in ℕ} g (n) \to (F^{-1} [e] \in (S ↾_{𝑡} D) \leftrightarrow F^{-1} [⋃_{n \in ℕ} g (n)] \in (S ↾_{𝑡} D))$
165	164 4	elrab2	$⊢ ⋃_{n \in ℕ} g (n) \in T \leftrightarrow (⋃_{n \in ℕ} g (n) \in 𝒫 ℝ \land F^{-1} [⋃_{n \in ℕ} g (n)] \in (S ↾_{𝑡} D))$
166	162 165	sylibr	$⊢ (φ \land g : ℕ ⟶ T) \to ⋃_{n \in ℕ} g (n) \in T$
167	8 24 25 134 166	issalnnd	$⊢ φ \to T \in SAlg$

Metamath Proof Explorer

Theorem smfresal

Proof