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

Metamath Proof Explorer

Theorem smfresal

Proof