smfsuplem1

Description: The supremum of a countable set of sigma-measurable functions is sigma-measurable. Proposition 121F (b) of Fremlin1 p. 38 . (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	smfsuplem1.m	$⊢ φ \to M \in ℤ$
	smfsuplem1.z	$⊢ Z = ℤ_{\geq M}$
	smfsuplem1.s	$⊢ φ \to S \in SAlg$
	smfsuplem1.f	$⊢ φ \to F : Z ⟶ SMblFn (S)$
	smfsuplem1.d	$⊢ D = \{x \in ⋂_{n \in Z} dom F (n) \| \exists y \in ℝ \forall n \in Z F (n) (x) \leq y\}$
	smfsuplem1.g	$⊢ G = (x \in D ⟼ sup (ran (n \in Z ⟼ F (n) (x)) ℝ <))$
	smfsuplem1.a	$⊢ φ \to A \in ℝ$
	smfsuplem1.h	$⊢ φ \to H : Z ⟶ S$
	smfsuplem1.i	$⊢ (φ \land n \in Z) \to {F (n)}^{-1} [(−∞, A]] = H (n) \cap dom F (n)$
Assertion	smfsuplem1	$⊢ φ \to G^{-1} [(−∞, A]] \in (S ↾_{𝑡} D)$

Proof

Step	Hyp	Ref	Expression
1		smfsuplem1.m	$⊢ φ \to M \in ℤ$
2		smfsuplem1.z	$⊢ Z = ℤ_{\geq M}$
3		smfsuplem1.s	$⊢ φ \to S \in SAlg$
4		smfsuplem1.f	$⊢ φ \to F : Z ⟶ SMblFn (S)$
5		smfsuplem1.d	$⊢ D = \{x \in ⋂_{n \in Z} dom F (n) \| \exists y \in ℝ \forall n \in Z F (n) (x) \leq y\}$
6		smfsuplem1.g	$⊢ G = (x \in D ⟼ sup (ran (n \in Z ⟼ F (n) (x)) ℝ <))$
7		smfsuplem1.a	$⊢ φ \to A \in ℝ$
8		smfsuplem1.h	$⊢ φ \to H : Z ⟶ S$
9		smfsuplem1.i	$⊢ (φ \land n \in Z) \to {F (n)}^{-1} [(−∞, A]] = H (n) \cap dom F (n)$
10	3	adantr	$⊢ (φ \land n \in Z) \to S \in SAlg$
11	4	ffvelcdmda	$⊢ (φ \land n \in Z) \to F (n) \in SMblFn (S)$
12		eqid	$⊢ dom F (n) = dom F (n)$
13	10 11 12	smff	$⊢ (φ \land n \in Z) \to F (n) : dom F (n) ⟶ ℝ$
14	13	ffnd	$⊢ (φ \land n \in Z) \to F (n) Fn dom F (n)$
15	14	adantr	$⊢ ((φ \land n \in Z) \land x \in G^{-1} [(−∞, A]]) \to F (n) Fn dom F (n)$
16		ssrab2	$⊢ \{x \in ⋂_{n \in Z} dom F (n) \| \exists y \in ℝ \forall n \in Z F (n) (x) \leq y\} \subseteq ⋂_{n \in Z} dom F (n)$
17	5 16	eqsstri	$⊢ D \subseteq ⋂_{n \in Z} dom F (n)$
18		iinss2	$⊢ n \in Z \to ⋂_{n \in Z} dom F (n) \subseteq dom F (n)$
19	17 18	sstrid	$⊢ n \in Z \to D \subseteq dom F (n)$
20	19	ad2antlr	$⊢ ((φ \land n \in Z) \land x \in G^{-1} [(−∞, A]]) \to D \subseteq dom F (n)$
21		cnvimass	$⊢ G^{-1} [(−∞, A]] \subseteq dom G$
22	21	sseli	$⊢ x \in G^{-1} [(−∞, A]] \to x \in dom G$
23	22	adantl	$⊢ ((φ \land n \in Z) \land x \in G^{-1} [(−∞, A]]) \to x \in dom G$
24		nfv	$⊢ Ⅎ n (φ \land x \in D)$
25		uzid	$⊢ M \in ℤ \to M \in ℤ_{\geq M}$
26	1 25	syl	$⊢ φ \to M \in ℤ_{\geq M}$
27	26 2	eleqtrrdi	$⊢ φ \to M \in Z$
28	27	ne0d	$⊢ φ \to Z \neq \emptyset$
29	28	adantr	$⊢ (φ \land x \in D) \to Z \neq \emptyset$
30	13	adantlr	$⊢ ((φ \land x \in D) \land n \in Z) \to F (n) : dom F (n) ⟶ ℝ$
31	18	adantl	$⊢ (x \in D \land n \in Z) \to ⋂_{n \in Z} dom F (n) \subseteq dom F (n)$
32	17	sseli	$⊢ x \in D \to x \in ⋂_{n \in Z} dom F (n)$
33	32	adantr	$⊢ (x \in D \land n \in Z) \to x \in ⋂_{n \in Z} dom F (n)$
34	31 33	sseldd	$⊢ (x \in D \land n \in Z) \to x \in dom F (n)$
35	34	adantll	$⊢ ((φ \land x \in D) \land n \in Z) \to x \in dom F (n)$
36	30 35	ffvelcdmd	$⊢ ((φ \land x \in D) \land n \in Z) \to F (n) (x) \in ℝ$
37	5	reqabi	$⊢ x \in D \leftrightarrow (x \in ⋂_{n \in Z} dom F (n) \land \exists y \in ℝ \forall n \in Z F (n) (x) \leq y)$
38	37	simprbi	$⊢ x \in D \to \exists y \in ℝ \forall n \in Z F (n) (x) \leq y$
39	38	adantl	$⊢ (φ \land x \in D) \to \exists y \in ℝ \forall n \in Z F (n) (x) \leq y$
40	24 29 36 39	suprclrnmpt	$⊢ (φ \land x \in D) \to sup (ran (n \in Z ⟼ F (n) (x)) ℝ <) \in ℝ$
41	40 6	fmptd	$⊢ φ \to G : D ⟶ ℝ$
42	41	fdmd	$⊢ φ \to dom G = D$
43	42	ad2antrr	$⊢ ((φ \land n \in Z) \land x \in G^{-1} [(−∞, A]]) \to dom G = D$
44	23 43	eleqtrd	$⊢ ((φ \land n \in Z) \land x \in G^{-1} [(−∞, A]]) \to x \in D$
45	20 44	sseldd	$⊢ ((φ \land n \in Z) \land x \in G^{-1} [(−∞, A]]) \to x \in dom F (n)$
46		mnfxr	$⊢ −∞ \in ℝ^{*}$
47	46	a1i	$⊢ ((φ \land n \in Z) \land x \in G^{-1} [(−∞, A]]) \to −∞ \in ℝ^{*}$
48	7	rexrd	$⊢ φ \to A \in ℝ^{*}$
49	48	ad2antrr	$⊢ ((φ \land n \in Z) \land x \in G^{-1} [(−∞, A]]) \to A \in ℝ^{*}$
50	36	an32s	$⊢ ((φ \land n \in Z) \land x \in D) \to F (n) (x) \in ℝ$
51	44 50	syldan	$⊢ ((φ \land n \in Z) \land x \in G^{-1} [(−∞, A]]) \to F (n) (x) \in ℝ$
52	51	rexrd	$⊢ ((φ \land n \in Z) \land x \in G^{-1} [(−∞, A]]) \to F (n) (x) \in ℝ^{*}$
53	51	mnfltd	$⊢ ((φ \land n \in Z) \land x \in G^{-1} [(−∞, A]]) \to −∞ < F (n) (x)$
54	22	adantl	$⊢ (φ \land x \in G^{-1} [(−∞, A]]) \to x \in dom G$
55	41	ffdmd	$⊢ φ \to G : dom G ⟶ ℝ$
56	55	ffvelcdmda	$⊢ (φ \land x \in dom G) \to G (x) \in ℝ$
57	54 56	syldan	$⊢ (φ \land x \in G^{-1} [(−∞, A]]) \to G (x) \in ℝ$
58	57	adantlr	$⊢ ((φ \land n \in Z) \land x \in G^{-1} [(−∞, A]]) \to G (x) \in ℝ$
59	7	ad2antrr	$⊢ ((φ \land n \in Z) \land x \in G^{-1} [(−∞, A]]) \to A \in ℝ$
60		an32	$⊢ ((φ \land n \in Z) \land x \in D) \leftrightarrow ((φ \land x \in D) \land n \in Z)$
61	60	biimpi	$⊢ ((φ \land n \in Z) \land x \in D) \to ((φ \land x \in D) \land n \in Z)$
62	24 36 39	suprubrnmpt	$⊢ ((φ \land x \in D) \land n \in Z) \to F (n) (x) \leq sup (ran (n \in Z ⟼ F (n) (x)) ℝ <)$
63	61 62	syl	$⊢ ((φ \land n \in Z) \land x \in D) \to F (n) (x) \leq sup (ran (n \in Z ⟼ F (n) (x)) ℝ <)$
64	6	a1i	$⊢ φ \to G = (x \in D ⟼ sup (ran (n \in Z ⟼ F (n) (x)) ℝ <))$
65	64 40	fvmpt2d	$⊢ (φ \land x \in D) \to G (x) = sup (ran (n \in Z ⟼ F (n) (x)) ℝ <)$
66	65	adantlr	$⊢ ((φ \land n \in Z) \land x \in D) \to G (x) = sup (ran (n \in Z ⟼ F (n) (x)) ℝ <)$
67	63 66	breqtrrd	$⊢ ((φ \land n \in Z) \land x \in D) \to F (n) (x) \leq G (x)$
68	44 67	syldan	$⊢ ((φ \land n \in Z) \land x \in G^{-1} [(−∞, A]]) \to F (n) (x) \leq G (x)$
69	46	a1i	$⊢ (φ \land x \in G^{-1} [(−∞, A]]) \to −∞ \in ℝ^{*}$
70	48	adantr	$⊢ (φ \land x \in G^{-1} [(−∞, A]]) \to A \in ℝ^{*}$
71		simpr	$⊢ (φ \land x \in G^{-1} [(−∞, A]]) \to x \in G^{-1} [(−∞, A]]$
72	41	ffnd	$⊢ φ \to G Fn D$
73		elpreima	$⊢ G Fn D \to (x \in G^{-1} [(−∞, A]] \leftrightarrow (x \in D \land G (x) \in (−∞, A]))$
74	72 73	syl	$⊢ φ \to (x \in G^{-1} [(−∞, A]] \leftrightarrow (x \in D \land G (x) \in (−∞, A]))$
75	74	adantr	$⊢ (φ \land x \in G^{-1} [(−∞, A]]) \to (x \in G^{-1} [(−∞, A]] \leftrightarrow (x \in D \land G (x) \in (−∞, A]))$
76	71 75	mpbid	$⊢ (φ \land x \in G^{-1} [(−∞, A]]) \to (x \in D \land G (x) \in (−∞, A])$
77	76	simprd	$⊢ (φ \land x \in G^{-1} [(−∞, A]]) \to G (x) \in (−∞, A]$
78	69 70 77	iocleubd	$⊢ (φ \land x \in G^{-1} [(−∞, A]]) \to G (x) \leq A$
79	78	adantlr	$⊢ ((φ \land n \in Z) \land x \in G^{-1} [(−∞, A]]) \to G (x) \leq A$
80	51 58 59 68 79	letrd	$⊢ ((φ \land n \in Z) \land x \in G^{-1} [(−∞, A]]) \to F (n) (x) \leq A$
81	47 49 52 53 80	eliocd	$⊢ ((φ \land n \in Z) \land x \in G^{-1} [(−∞, A]]) \to F (n) (x) \in (−∞, A]$
82	15 45 81	elpreimad	$⊢ ((φ \land n \in Z) \land x \in G^{-1} [(−∞, A]]) \to x \in {F (n)}^{-1} [(−∞, A]]$
83	82	ssd	$⊢ (φ \land n \in Z) \to G^{-1} [(−∞, A]] \subseteq {F (n)}^{-1} [(−∞, A]]$
84		inss1	$⊢ H (n) \cap dom F (n) \subseteq H (n)$
85	9 84	eqsstrdi	$⊢ (φ \land n \in Z) \to {F (n)}^{-1} [(−∞, A]] \subseteq H (n)$
86	83 85	sstrd	$⊢ (φ \land n \in Z) \to G^{-1} [(−∞, A]] \subseteq H (n)$
87	86	ralrimiva	$⊢ φ \to \forall n \in Z G^{-1} [(−∞, A]] \subseteq H (n)$
88		ssiin	$⊢ G^{-1} [(−∞, A]] \subseteq ⋂_{n \in Z} H (n) \leftrightarrow \forall n \in Z G^{-1} [(−∞, A]] \subseteq H (n)$
89	87 88	sylibr	$⊢ φ \to G^{-1} [(−∞, A]] \subseteq ⋂_{n \in Z} H (n)$
90	21 41	fssdm	$⊢ φ \to G^{-1} [(−∞, A]] \subseteq D$
91	89 90	ssind	$⊢ φ \to G^{-1} [(−∞, A]] \subseteq ⋂_{n \in Z} H (n) \cap D$
92		iniin1	$⊢ Z \neq \emptyset \to ⋂_{n \in Z} H (n) \cap D = ⋂_{n \in Z} (H (n) \cap D)$
93	28 92	syl	$⊢ φ \to ⋂_{n \in Z} H (n) \cap D = ⋂_{n \in Z} (H (n) \cap D)$
94	72	adantr	$⊢ (φ \land x \in ⋂_{n \in Z} (H (n) \cap D)) \to G Fn D$
95		simpr	$⊢ (φ \land x \in ⋂_{n \in Z} (H (n) \cap D)) \to x \in ⋂_{n \in Z} (H (n) \cap D)$
96	27	adantr	$⊢ (φ \land x \in ⋂_{n \in Z} (H (n) \cap D)) \to M \in Z$
97		fveq2	$⊢ n = M \to H (n) = H (M)$
98	97	ineq1d	$⊢ n = M \to H (n) \cap D = H (M) \cap D$
99	98	eleq2d	$⊢ n = M \to (x \in (H (n) \cap D) \leftrightarrow x \in (H (M) \cap D))$
100	95 96 99	eliind	$⊢ (φ \land x \in ⋂_{n \in Z} (H (n) \cap D)) \to x \in (H (M) \cap D)$
101		elinel2	$⊢ x \in (H (M) \cap D) \to x \in D$
102	100 101	syl	$⊢ (φ \land x \in ⋂_{n \in Z} (H (n) \cap D)) \to x \in D$
103	46	a1i	$⊢ (φ \land x \in ⋂_{n \in Z} (H (n) \cap D)) \to −∞ \in ℝ^{*}$
104	48	adantr	$⊢ (φ \land x \in ⋂_{n \in Z} (H (n) \cap D)) \to A \in ℝ^{*}$
105	65 40	eqeltrd	$⊢ (φ \land x \in D) \to G (x) \in ℝ$
106	105	rexrd	$⊢ (φ \land x \in D) \to G (x) \in ℝ^{*}$
107	102 106	syldan	$⊢ (φ \land x \in ⋂_{n \in Z} (H (n) \cap D)) \to G (x) \in ℝ^{*}$
108	101	adantl	$⊢ (φ \land x \in (H (M) \cap D)) \to x \in D$
109	108 105	syldan	$⊢ (φ \land x \in (H (M) \cap D)) \to G (x) \in ℝ$
110	109	mnfltd	$⊢ (φ \land x \in (H (M) \cap D)) \to −∞ < G (x)$
111	100 110	syldan	$⊢ (φ \land x \in ⋂_{n \in Z} (H (n) \cap D)) \to −∞ < G (x)$
112	102 65	syldan	$⊢ (φ \land x \in ⋂_{n \in Z} (H (n) \cap D)) \to G (x) = sup (ran (n \in Z ⟼ F (n) (x)) ℝ <)$
113		nfv	$⊢ Ⅎ n φ$
114		nfcv	$⊢ \underline{Ⅎ} n x$
115		nfii1	$⊢ \underline{Ⅎ} n ⋂_{n \in Z} (H (n) \cap D)$
116	114 115	nfel	$⊢ Ⅎ n x \in ⋂_{n \in Z} (H (n) \cap D)$
117	113 116	nfan	$⊢ Ⅎ n (φ \land x \in ⋂_{n \in Z} (H (n) \cap D))$
118		simpll	$⊢ ((φ \land x \in ⋂_{n \in Z} (H (n) \cap D)) \land n \in Z) \to φ$
119		simpr	$⊢ ((φ \land x \in ⋂_{n \in Z} (H (n) \cap D)) \land n \in Z) \to n \in Z$
120		eliinid	$⊢ (x \in ⋂_{n \in Z} (H (n) \cap D) \land n \in Z) \to x \in (H (n) \cap D)$
121	120	adantll	$⊢ ((φ \land x \in ⋂_{n \in Z} (H (n) \cap D)) \land n \in Z) \to x \in (H (n) \cap D)$
122		elinel1	$⊢ x \in (H (n) \cap D) \to x \in H (n)$
123	122	3ad2ant3	$⊢ (φ \land n \in Z \land x \in (H (n) \cap D)) \to x \in H (n)$
124		elinel2	$⊢ x \in (H (n) \cap D) \to x \in D$
125	124	adantl	$⊢ (n \in Z \land x \in (H (n) \cap D)) \to x \in D$
126	34	ancoms	$⊢ (n \in Z \land x \in D) \to x \in dom F (n)$
127	125 126	syldan	$⊢ (n \in Z \land x \in (H (n) \cap D)) \to x \in dom F (n)$
128	127	3adant1	$⊢ (φ \land n \in Z \land x \in (H (n) \cap D)) \to x \in dom F (n)$
129	123 128	elind	$⊢ (φ \land n \in Z \land x \in (H (n) \cap D)) \to x \in (H (n) \cap dom F (n))$
130	9	3adant3	$⊢ (φ \land n \in Z \land x \in (H (n) \cap D)) \to {F (n)}^{-1} [(−∞, A]] = H (n) \cap dom F (n)$
131	129 130	eleqtrrd	$⊢ (φ \land n \in Z \land x \in (H (n) \cap D)) \to x \in {F (n)}^{-1} [(−∞, A]]$
132	46	a1i	$⊢ (φ \land n \in Z \land x \in {F (n)}^{-1} [(−∞, A]]) \to −∞ \in ℝ^{*}$
133	48	3ad2ant1	$⊢ (φ \land n \in Z \land x \in {F (n)}^{-1} [(−∞, A]]) \to A \in ℝ^{*}$
134		simp3	$⊢ (φ \land n \in Z \land x \in {F (n)}^{-1} [(−∞, A]]) \to x \in {F (n)}^{-1} [(−∞, A]]$
135		elpreima	$⊢ F (n) Fn dom F (n) \to (x \in {F (n)}^{-1} [(−∞, A]] \leftrightarrow (x \in dom F (n) \land F (n) (x) \in (−∞, A]))$
136	14 135	syl	$⊢ (φ \land n \in Z) \to (x \in {F (n)}^{-1} [(−∞, A]] \leftrightarrow (x \in dom F (n) \land F (n) (x) \in (−∞, A]))$
137	136	3adant3	$⊢ (φ \land n \in Z \land x \in {F (n)}^{-1} [(−∞, A]]) \to (x \in {F (n)}^{-1} [(−∞, A]] \leftrightarrow (x \in dom F (n) \land F (n) (x) \in (−∞, A]))$
138	134 137	mpbid	$⊢ (φ \land n \in Z \land x \in {F (n)}^{-1} [(−∞, A]]) \to (x \in dom F (n) \land F (n) (x) \in (−∞, A])$
139	138	simprd	$⊢ (φ \land n \in Z \land x \in {F (n)}^{-1} [(−∞, A]]) \to F (n) (x) \in (−∞, A]$
140	132 133 139	iocleubd	$⊢ (φ \land n \in Z \land x \in {F (n)}^{-1} [(−∞, A]]) \to F (n) (x) \leq A$
141	131 140	syld3an3	$⊢ (φ \land n \in Z \land x \in (H (n) \cap D)) \to F (n) (x) \leq A$
142	118 119 121 141	syl3anc	$⊢ ((φ \land x \in ⋂_{n \in Z} (H (n) \cap D)) \land n \in Z) \to F (n) (x) \leq A$
143	142	ex	$⊢ (φ \land x \in ⋂_{n \in Z} (H (n) \cap D)) \to (n \in Z \to F (n) (x) \leq A)$
144	117 143	ralrimi	$⊢ (φ \land x \in ⋂_{n \in Z} (H (n) \cap D)) \to \forall n \in Z F (n) (x) \leq A$
145	28	adantr	$⊢ (φ \land x \in ⋂_{n \in Z} (H (n) \cap D)) \to Z \neq \emptyset$
146	102 36	syldanl	$⊢ ((φ \land x \in ⋂_{n \in Z} (H (n) \cap D)) \land n \in Z) \to F (n) (x) \in ℝ$
147	102 38	syl	$⊢ (φ \land x \in ⋂_{n \in Z} (H (n) \cap D)) \to \exists y \in ℝ \forall n \in Z F (n) (x) \leq y$
148	7	adantr	$⊢ (φ \land x \in ⋂_{n \in Z} (H (n) \cap D)) \to A \in ℝ$
149	117 145 146 147 148	suprleubrnmpt	$⊢ (φ \land x \in ⋂_{n \in Z} (H (n) \cap D)) \to (sup (ran (n \in Z ⟼ F (n) (x)) ℝ <) \leq A \leftrightarrow \forall n \in Z F (n) (x) \leq A)$
150	144 149	mpbird	$⊢ (φ \land x \in ⋂_{n \in Z} (H (n) \cap D)) \to sup (ran (n \in Z ⟼ F (n) (x)) ℝ <) \leq A$
151	112 150	eqbrtrd	$⊢ (φ \land x \in ⋂_{n \in Z} (H (n) \cap D)) \to G (x) \leq A$
152	103 104 107 111 151	eliocd	$⊢ (φ \land x \in ⋂_{n \in Z} (H (n) \cap D)) \to G (x) \in (−∞, A]$
153	94 102 152	elpreimad	$⊢ (φ \land x \in ⋂_{n \in Z} (H (n) \cap D)) \to x \in G^{-1} [(−∞, A]]$
154	153	ssd	$⊢ φ \to ⋂_{n \in Z} (H (n) \cap D) \subseteq G^{-1} [(−∞, A]]$
155	93 154	eqsstrd	$⊢ φ \to ⋂_{n \in Z} H (n) \cap D \subseteq G^{-1} [(−∞, A]]$
156	91 155	eqssd	$⊢ φ \to G^{-1} [(−∞, A]] = ⋂_{n \in Z} H (n) \cap D$
157		eqid	$⊢ \{x \in ⋂_{n \in Z} dom F (n) \| \exists y \in ℝ \forall n \in Z F (n) (x) \leq y\} = \{x \in ⋂_{n \in Z} dom F (n) \| \exists y \in ℝ \forall n \in Z F (n) (x) \leq y\}$
158		fvex	$⊢ F (n) \in V$
159	158	dmex	$⊢ dom F (n) \in V$
160	159	rgenw	$⊢ \forall n \in Z dom F (n) \in V$
161	160	a1i	$⊢ φ \to \forall n \in Z dom F (n) \in V$
162	28 161	iinexd	$⊢ φ \to ⋂_{n \in Z} dom F (n) \in V$
163	157 162	rabexd	$⊢ φ \to \{x \in ⋂_{n \in Z} dom F (n) \| \exists y \in ℝ \forall n \in Z F (n) (x) \leq y\} \in V$
164	5 163	eqeltrid	$⊢ φ \to D \in V$
165	2	uzct	$⊢ Z ≼ ω$
166	165	a1i	$⊢ φ \to Z ≼ ω$
167	8	ffvelcdmda	$⊢ (φ \land n \in Z) \to H (n) \in S$
168	3 166 28 167	saliincl	$⊢ φ \to ⋂_{n \in Z} H (n) \in S$
169		eqid	$⊢ ⋂_{n \in Z} H (n) \cap D = ⋂_{n \in Z} H (n) \cap D$
170	3 164 168 169	elrestd	$⊢ φ \to ⋂_{n \in Z} H (n) \cap D \in (S ↾_{𝑡} D)$
171	156 170	eqeltrd	$⊢ φ \to G^{-1} [(−∞, A]] \in (S ↾_{𝑡} D)$

Metamath Proof Explorer

Theorem smfsuplem1

Proof