smflim

Description: The limit of sigma-measurable functions is sigma-measurable. Proposition 121F (a) of Fremlin1 p. 38 . Notice that every function in the sequence can have a different (partial) domain, and the domain of convergence can be decidedly irregular (Remark 121G of Fremlin1 p. 39 ). (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	smflim.n	$⊢ \underline{Ⅎ} m F$
	smflim.x	$⊢ \underline{Ⅎ} x F$
	smflim.m	$⊢ φ \to M \in ℤ$
	smflim.z	$⊢ Z = ℤ_{\geq M}$
	smflim.s	$⊢ φ \to S \in SAlg$
	smflim.f	$⊢ φ \to F : Z ⟶ SMblFn (S)$
	smflim.d	$⊢ D = \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| (m \in Z ⟼ F (m) (x)) \in dom ⇝\}$
	smflim.g	$⊢ G = (x \in D ⟼ ⇝ ((m \in Z ⟼ F (m) (x))))$
Assertion	smflim	$⊢ φ \to G \in SMblFn (S)$

Proof

Step	Hyp	Ref	Expression
1		smflim.n	$⊢ \underline{Ⅎ} m F$
2		smflim.x	$⊢ \underline{Ⅎ} x F$
3		smflim.m	$⊢ φ \to M \in ℤ$
4		smflim.z	$⊢ Z = ℤ_{\geq M}$
5		smflim.s	$⊢ φ \to S \in SAlg$
6		smflim.f	$⊢ φ \to F : Z ⟶ SMblFn (S)$
7		smflim.d	$⊢ D = \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| (m \in Z ⟼ F (m) (x)) \in dom ⇝\}$
8		smflim.g	$⊢ G = (x \in D ⟼ ⇝ ((m \in Z ⟼ F (m) (x))))$
9		nfv	$⊢ Ⅎ a φ$
10		nfcv	$⊢ \underline{Ⅎ} x Z$
11		nfcv	$⊢ \underline{Ⅎ} x ℤ_{\geq n}$
12		nfcv	$⊢ \underline{Ⅎ} x m$
13	2 12	nffv	$⊢ \underline{Ⅎ} x F (m)$
14	13	nfdm	$⊢ \underline{Ⅎ} x dom F (m)$
15	11 14	nfiin	$⊢ \underline{Ⅎ} x ⋂_{m \in ℤ_{\geq n}} dom F (m)$
16	10 15	nfiun	$⊢ \underline{Ⅎ} x ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m)$
17	16	ssrab2f	$⊢ \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| (m \in Z ⟼ F (m) (x)) \in dom ⇝\} \subseteq ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m)$
18	7 17	eqsstri	$⊢ D \subseteq ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m)$
19	18	a1i	$⊢ φ \to D \subseteq ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m)$
20		uzssz	$⊢ ℤ_{\geq M} \subseteq ℤ$
21	4	eleq2i	$⊢ n \in Z \leftrightarrow n \in ℤ_{\geq M}$
22	21	biimpi	$⊢ n \in Z \to n \in ℤ_{\geq M}$
23	20 22	sseldi	$⊢ n \in Z \to n \in ℤ$
24		uzid	$⊢ n \in ℤ \to n \in ℤ_{\geq n}$
25	23 24	syl	$⊢ n \in Z \to n \in ℤ_{\geq n}$
26	25	adantl	$⊢ (φ \land n \in Z) \to n \in ℤ_{\geq n}$
27	5	adantr	$⊢ (φ \land n \in Z) \to S \in SAlg$
28	6	ffvelrnda	$⊢ (φ \land n \in Z) \to F (n) \in SMblFn (S)$
29		eqid	$⊢ dom F (n) = dom F (n)$
30	27 28 29	smfdmss	$⊢ (φ \land n \in Z) \to dom F (n) \subseteq ⋃ S$
31		nfcv	$⊢ \underline{Ⅎ} m n$
32	1 31	nffv	$⊢ \underline{Ⅎ} m F (n)$
33	32	nfdm	$⊢ \underline{Ⅎ} m dom F (n)$
34		nfcv	$⊢ \underline{Ⅎ} m ⋃ S$
35	33 34	nfss	$⊢ Ⅎ m dom F (n) \subseteq ⋃ S$
36		fveq2	$⊢ m = n \to F (m) = F (n)$
37	36	dmeqd	$⊢ m = n \to dom F (m) = dom F (n)$
38	37	sseq1d	$⊢ m = n \to (dom F (m) \subseteq ⋃ S \leftrightarrow dom F (n) \subseteq ⋃ S)$
39	35 38	rspce	$⊢ (n \in ℤ_{\geq n} \land dom F (n) \subseteq ⋃ S) \to \exists m \in ℤ_{\geq n} dom F (m) \subseteq ⋃ S$
40	26 30 39	syl2anc	$⊢ (φ \land n \in Z) \to \exists m \in ℤ_{\geq n} dom F (m) \subseteq ⋃ S$
41		iinss	$⊢ \exists m \in ℤ_{\geq n} dom F (m) \subseteq ⋃ S \to ⋂_{m \in ℤ_{\geq n}} dom F (m) \subseteq ⋃ S$
42	40 41	syl	$⊢ (φ \land n \in Z) \to ⋂_{m \in ℤ_{\geq n}} dom F (m) \subseteq ⋃ S$
43	42	iunssd	$⊢ φ \to ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \subseteq ⋃ S$
44	19 43	sstrd	$⊢ φ \to D \subseteq ⋃ S$
45		nfv	$⊢ Ⅎ m φ$
46		nfcv	$⊢ \underline{Ⅎ} m y$
47		nfmpt1	$⊢ \underline{Ⅎ} m (m \in Z ⟼ F (m) (x))$
48		nfcv	$⊢ \underline{Ⅎ} m dom ⇝$
49	47 48	nfel	$⊢ Ⅎ m (m \in Z ⟼ F (m) (x)) \in dom ⇝$
50		nfcv	$⊢ \underline{Ⅎ} m Z$
51		nfii1	$⊢ \underline{Ⅎ} m ⋂_{m \in ℤ_{\geq n}} dom F (m)$
52	50 51	nfiun	$⊢ \underline{Ⅎ} m ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m)$
53	49 52	nfrabw	$⊢ \underline{Ⅎ} m \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| (m \in Z ⟼ F (m) (x)) \in dom ⇝\}$
54	7 53	nfcxfr	$⊢ \underline{Ⅎ} m D$
55	46 54	nfel	$⊢ Ⅎ m y \in D$
56	45 55	nfan	$⊢ Ⅎ m (φ \land y \in D)$
57		nfcv	$⊢ \underline{Ⅎ} w F$
58	5	adantr	$⊢ (φ \land m \in Z) \to S \in SAlg$
59	6	ffvelrnda	$⊢ (φ \land m \in Z) \to F (m) \in SMblFn (S)$
60		eqid	$⊢ dom F (m) = dom F (m)$
61	58 59 60	smff	$⊢ (φ \land m \in Z) \to F (m) : dom F (m) ⟶ ℝ$
62	61	adantlr	$⊢ ((φ \land y \in D) \land m \in Z) \to F (m) : dom F (m) ⟶ ℝ$
63		nfcv	$⊢ \underline{Ⅎ} y ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m)$
64		nfv	$⊢ Ⅎ y (m \in Z ⟼ F (m) (x)) \in dom ⇝$
65		nfcv	$⊢ \underline{Ⅎ} x y$
66	13 65	nffv	$⊢ \underline{Ⅎ} x F (m) (y)$
67	10 66	nfmpt	$⊢ \underline{Ⅎ} x (m \in Z ⟼ F (m) (y))$
68	67	nfel1	$⊢ Ⅎ x (m \in Z ⟼ F (m) (y)) \in dom ⇝$
69		fveq2	$⊢ x = y \to F (m) (x) = F (m) (y)$
70	69	mpteq2dv	$⊢ x = y \to (m \in Z ⟼ F (m) (x)) = (m \in Z ⟼ F (m) (y))$
71	70	eleq1d	$⊢ x = y \to ((m \in Z ⟼ F (m) (x)) \in dom ⇝ \leftrightarrow (m \in Z ⟼ F (m) (y)) \in dom ⇝)$
72	16 63 64 68 71	cbvrabw	$⊢ \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| (m \in Z ⟼ F (m) (x)) \in dom ⇝\} = \{y \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| (m \in Z ⟼ F (m) (y)) \in dom ⇝\}$
73		nfcv	$⊢ \underline{Ⅎ} l dom F (m)$
74		nfcv	$⊢ \underline{Ⅎ} m l$
75	1 74	nffv	$⊢ \underline{Ⅎ} m F (l)$
76	75	nfdm	$⊢ \underline{Ⅎ} m dom F (l)$
77		fveq2	$⊢ m = l \to F (m) = F (l)$
78	77	dmeqd	$⊢ m = l \to dom F (m) = dom F (l)$
79	73 76 78	cbviin	$⊢ ⋂_{m \in ℤ_{\geq n}} dom F (m) = ⋂_{l \in ℤ_{\geq n}} dom F (l)$
80	79	a1i	$⊢ n = i \to ⋂_{m \in ℤ_{\geq n}} dom F (m) = ⋂_{l \in ℤ_{\geq n}} dom F (l)$
81		fveq2	$⊢ n = i \to ℤ_{\geq n} = ℤ_{\geq i}$
82		eqidd	$⊢ (n = i \land l \in ℤ_{\geq i}) \to dom F (l) = dom F (l)$
83	81 82	iineq12dv	$⊢ n = i \to ⋂_{l \in ℤ_{\geq n}} dom F (l) = ⋂_{l \in ℤ_{\geq i}} dom F (l)$
84	80 83	eqtrd	$⊢ n = i \to ⋂_{m \in ℤ_{\geq n}} dom F (m) = ⋂_{l \in ℤ_{\geq i}} dom F (l)$
85	84	cbviunv	$⊢ ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) = ⋃_{i \in Z} ⋂_{l \in ℤ_{\geq i}} dom F (l)$
86	85	eleq2i	$⊢ y \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \leftrightarrow y \in ⋃_{i \in Z} ⋂_{l \in ℤ_{\geq i}} dom F (l)$
87		nfcv	$⊢ \underline{Ⅎ} l Z$
88		nfcv	$⊢ \underline{Ⅎ} l F (m) (y)$
89	75 46	nffv	$⊢ \underline{Ⅎ} m F (l) (y)$
90	77	fveq1d	$⊢ m = l \to F (m) (y) = F (l) (y)$
91	50 87 88 89 90	cbvmptf	$⊢ (m \in Z ⟼ F (m) (y)) = (l \in Z ⟼ F (l) (y))$
92	91	eleq1i	$⊢ (m \in Z ⟼ F (m) (y)) \in dom ⇝ \leftrightarrow (l \in Z ⟼ F (l) (y)) \in dom ⇝$
93	86 92	anbi12i	$⊢ (y \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \land (m \in Z ⟼ F (m) (y)) \in dom ⇝) \leftrightarrow (y \in ⋃_{i \in Z} ⋂_{l \in ℤ_{\geq i}} dom F (l) \land (l \in Z ⟼ F (l) (y)) \in dom ⇝)$
94	93	rabbia2	$⊢ \{y \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| (m \in Z ⟼ F (m) (y)) \in dom ⇝\} = \{y \in ⋃_{i \in Z} ⋂_{l \in ℤ_{\geq i}} dom F (l) \| (l \in Z ⟼ F (l) (y)) \in dom ⇝\}$
95	7 72 94	3eqtri	$⊢ D = \{y \in ⋃_{i \in Z} ⋂_{l \in ℤ_{\geq i}} dom F (l) \| (l \in Z ⟼ F (l) (y)) \in dom ⇝\}$
96		fveq2	$⊢ y = w \to F (l) (y) = F (l) (w)$
97	96	mpteq2dv	$⊢ y = w \to (l \in Z ⟼ F (l) (y)) = (l \in Z ⟼ F (l) (w))$
98	97	eleq1d	$⊢ y = w \to ((l \in Z ⟼ F (l) (y)) \in dom ⇝ \leftrightarrow (l \in Z ⟼ F (l) (w)) \in dom ⇝)$
99	98	cbvrabv	$⊢ \{y \in ⋃_{i \in Z} ⋂_{l \in ℤ_{\geq i}} dom F (l) \| (l \in Z ⟼ F (l) (y)) \in dom ⇝\} = \{w \in ⋃_{i \in Z} ⋂_{l \in ℤ_{\geq i}} dom F (l) \| (l \in Z ⟼ F (l) (w)) \in dom ⇝\}$
100		fveq2	$⊢ l = m \to F (l) = F (m)$
101	100	dmeqd	$⊢ l = m \to dom F (l) = dom F (m)$
102	76 73 101	cbviin	$⊢ ⋂_{l \in ℤ_{\geq i}} dom F (l) = ⋂_{m \in ℤ_{\geq i}} dom F (m)$
103	102	a1i	$⊢ i \in Z \to ⋂_{l \in ℤ_{\geq i}} dom F (l) = ⋂_{m \in ℤ_{\geq i}} dom F (m)$
104	103	iuneq2i	$⊢ ⋃_{i \in Z} ⋂_{l \in ℤ_{\geq i}} dom F (l) = ⋃_{i \in Z} ⋂_{m \in ℤ_{\geq i}} dom F (m)$
105	104	eleq2i	$⊢ w \in ⋃_{i \in Z} ⋂_{l \in ℤ_{\geq i}} dom F (l) \leftrightarrow w \in ⋃_{i \in Z} ⋂_{m \in ℤ_{\geq i}} dom F (m)$
106		nfcv	$⊢ \underline{Ⅎ} m w$
107	75 106	nffv	$⊢ \underline{Ⅎ} m F (l) (w)$
108		nfcv	$⊢ \underline{Ⅎ} l F (m) (w)$
109	100	fveq1d	$⊢ l = m \to F (l) (w) = F (m) (w)$
110	87 50 107 108 109	cbvmptf	$⊢ (l \in Z ⟼ F (l) (w)) = (m \in Z ⟼ F (m) (w))$
111	110	eleq1i	$⊢ (l \in Z ⟼ F (l) (w)) \in dom ⇝ \leftrightarrow (m \in Z ⟼ F (m) (w)) \in dom ⇝$
112	105 111	anbi12i	$⊢ (w \in ⋃_{i \in Z} ⋂_{l \in ℤ_{\geq i}} dom F (l) \land (l \in Z ⟼ F (l) (w)) \in dom ⇝) \leftrightarrow (w \in ⋃_{i \in Z} ⋂_{m \in ℤ_{\geq i}} dom F (m) \land (m \in Z ⟼ F (m) (w)) \in dom ⇝)$
113	112	rabbia2	$⊢ \{w \in ⋃_{i \in Z} ⋂_{l \in ℤ_{\geq i}} dom F (l) \| (l \in Z ⟼ F (l) (w)) \in dom ⇝\} = \{w \in ⋃_{i \in Z} ⋂_{m \in ℤ_{\geq i}} dom F (m) \| (m \in Z ⟼ F (m) (w)) \in dom ⇝\}$
114	99 113	eqtri	$⊢ \{y \in ⋃_{i \in Z} ⋂_{l \in ℤ_{\geq i}} dom F (l) \| (l \in Z ⟼ F (l) (y)) \in dom ⇝\} = \{w \in ⋃_{i \in Z} ⋂_{m \in ℤ_{\geq i}} dom F (m) \| (m \in Z ⟼ F (m) (w)) \in dom ⇝\}$
115	95 114	eqtri	$⊢ D = \{w \in ⋃_{i \in Z} ⋂_{m \in ℤ_{\geq i}} dom F (m) \| (m \in Z ⟼ F (m) (w)) \in dom ⇝\}$
116		simpr	$⊢ (φ \land y \in D) \to y \in D$
117	56 1 57 4 62 115 116	fnlimfvre	$⊢ (φ \land y \in D) \to ⇝ ((m \in Z ⟼ F (m) (y))) \in ℝ$
118		nfrab1	$⊢ \underline{Ⅎ} x \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| (m \in Z ⟼ F (m) (x)) \in dom ⇝\}$
119	7 118	nfcxfr	$⊢ \underline{Ⅎ} x D$
120		nfcv	$⊢ \underline{Ⅎ} y D$
121		nfcv	$⊢ \underline{Ⅎ} y ⇝ ((m \in Z ⟼ F (m) (x)))$
122		nfcv	$⊢ \underline{Ⅎ} x ⇝$
123	122 67	nffv	$⊢ \underline{Ⅎ} x ⇝ ((m \in Z ⟼ F (m) (y)))$
124	70	fveq2d	$⊢ x = y \to ⇝ ((m \in Z ⟼ F (m) (x))) = ⇝ ((m \in Z ⟼ F (m) (y)))$
125	119 120 121 123 124	cbvmptf	$⊢ (x \in D ⟼ ⇝ ((m \in Z ⟼ F (m) (x)))) = (y \in D ⟼ ⇝ ((m \in Z ⟼ F (m) (y))))$
126	8 125	eqtri	$⊢ G = (y \in D ⟼ ⇝ ((m \in Z ⟼ F (m) (y))))$
127	117 126	fmptd	$⊢ φ \to G : D ⟶ ℝ$
128	3	adantr	$⊢ (φ \land a \in ℝ) \to M \in ℤ$
129	5	adantr	$⊢ (φ \land a \in ℝ) \to S \in SAlg$
130	6	adantr	$⊢ (φ \land a \in ℝ) \to F : Z ⟶ SMblFn (S)$
131		nfcv	$⊢ \underline{Ⅎ} x l$
132	2 131	nffv	$⊢ \underline{Ⅎ} x F (l)$
133	132 65	nffv	$⊢ \underline{Ⅎ} x F (l) (y)$
134	10 133	nfmpt	$⊢ \underline{Ⅎ} x (l \in Z ⟼ F (l) (y))$
135	122 134	nffv	$⊢ \underline{Ⅎ} x ⇝ ((l \in Z ⟼ F (l) (y)))$
136		nfcv	$⊢ \underline{Ⅎ} l F (m) (x)$
137		nfcv	$⊢ \underline{Ⅎ} m x$
138	75 137	nffv	$⊢ \underline{Ⅎ} m F (l) (x)$
139	77	fveq1d	$⊢ m = l \to F (m) (x) = F (l) (x)$
140	50 87 136 138 139	cbvmptf	$⊢ (m \in Z ⟼ F (m) (x)) = (l \in Z ⟼ F (l) (x))$
141	140	a1i	$⊢ x = y \to (m \in Z ⟼ F (m) (x)) = (l \in Z ⟼ F (l) (x))$
142		simpl	$⊢ (x = y \land l \in Z) \to x = y$
143	142	fveq2d	$⊢ (x = y \land l \in Z) \to F (l) (x) = F (l) (y)$
144	143	mpteq2dva	$⊢ x = y \to (l \in Z ⟼ F (l) (x)) = (l \in Z ⟼ F (l) (y))$
145	141 144	eqtrd	$⊢ x = y \to (m \in Z ⟼ F (m) (x)) = (l \in Z ⟼ F (l) (y))$
146	145	fveq2d	$⊢ x = y \to ⇝ ((m \in Z ⟼ F (m) (x))) = ⇝ ((l \in Z ⟼ F (l) (y)))$
147	119 120 121 135 146	cbvmptf	$⊢ (x \in D ⟼ ⇝ ((m \in Z ⟼ F (m) (x)))) = (y \in D ⟼ ⇝ ((l \in Z ⟼ F (l) (y))))$
148	8 147	eqtri	$⊢ G = (y \in D ⟼ ⇝ ((l \in Z ⟼ F (l) (y))))$
149		simpr	$⊢ (φ \land a \in ℝ) \to a \in ℝ$
150		nfcv	$⊢ \underline{Ⅎ} m <$
151		nfcv	$⊢ \underline{Ⅎ} m (a + (\frac{1}{j}))$
152	89 150 151	nfbr	$⊢ Ⅎ m F (l) (y) < a + (\frac{1}{j})$
153	152 76	nfrabw	$⊢ \underline{Ⅎ} m \{y \in dom F (l) \| F (l) (y) < a + (\frac{1}{j})\}$
154		nfcv	$⊢ \underline{Ⅎ} m t$
155	154 76	nfin	$⊢ \underline{Ⅎ} m (t \cap dom F (l))$
156	153 155	nfeq	$⊢ Ⅎ m \{y \in dom F (l) \| F (l) (y) < a + (\frac{1}{j})\} = t \cap dom F (l)$
157		nfcv	$⊢ \underline{Ⅎ} m S$
158	156 157	nfrabw	$⊢ \underline{Ⅎ} m \{t \in S \| \{y \in dom F (l) \| F (l) (y) < a + (\frac{1}{j})\} = t \cap dom F (l)\}$
159		nfcv	$⊢ \underline{Ⅎ} k \{t \in S \| \{y \in dom F (l) \| F (l) (y) < a + (\frac{1}{j})\} = t \cap dom F (l)\}$
160		nfcv	$⊢ \underline{Ⅎ} l \{s \in S \| \{x \in dom F (m) \| F (m) (x) < a + (\frac{1}{k})\} = s \cap dom F (m)\}$
161		nfcv	$⊢ \underline{Ⅎ} j \{s \in S \| \{x \in dom F (m) \| F (m) (x) < a + (\frac{1}{k})\} = s \cap dom F (m)\}$
162		nfcv	$⊢ \underline{Ⅎ} y dom F (l)$
163	132	nfdm	$⊢ \underline{Ⅎ} x dom F (l)$
164		nfcv	$⊢ \underline{Ⅎ} x <$
165		nfcv	$⊢ \underline{Ⅎ} x (a + (\frac{1}{j}))$
166	133 164 165	nfbr	$⊢ Ⅎ x F (l) (y) < a + (\frac{1}{j})$
167		nfv	$⊢ Ⅎ y F (l) (x) < a + (\frac{1}{j})$
168		fveq2	$⊢ y = x \to F (l) (y) = F (l) (x)$
169	168	breq1d	$⊢ y = x \to (F (l) (y) < a + (\frac{1}{j}) \leftrightarrow F (l) (x) < a + (\frac{1}{j}))$
170	162 163 166 167 169	cbvrabw	$⊢ \{y \in dom F (l) \| F (l) (y) < a + (\frac{1}{j})\} = \{x \in dom F (l) \| F (l) (x) < a + (\frac{1}{j})\}$
171	170	a1i	$⊢ t = s \to \{y \in dom F (l) \| F (l) (y) < a + (\frac{1}{j})\} = \{x \in dom F (l) \| F (l) (x) < a + (\frac{1}{j})\}$
172		ineq1	$⊢ t = s \to t \cap dom F (l) = s \cap dom F (l)$
173	171 172	eqeq12d	$⊢ t = s \to (\{y \in dom F (l) \| F (l) (y) < a + (\frac{1}{j})\} = t \cap dom F (l) \leftrightarrow \{x \in dom F (l) \| F (l) (x) < a + (\frac{1}{j})\} = s \cap dom F (l))$
174	173	cbvrabv	$⊢ \{t \in S \| \{y \in dom F (l) \| F (l) (y) < a + (\frac{1}{j})\} = t \cap dom F (l)\} = \{s \in S \| \{x \in dom F (l) \| F (l) (x) < a + (\frac{1}{j})\} = s \cap dom F (l)\}$
175	174	a1i	$⊢ l = m \to \{t \in S \| \{y \in dom F (l) \| F (l) (y) < a + (\frac{1}{j})\} = t \cap dom F (l)\} = \{s \in S \| \{x \in dom F (l) \| F (l) (x) < a + (\frac{1}{j})\} = s \cap dom F (l)\}$
176	101	eleq2d	$⊢ l = m \to (x \in dom F (l) \leftrightarrow x \in dom F (m))$
177	100	fveq1d	$⊢ l = m \to F (l) (x) = F (m) (x)$
178	177	breq1d	$⊢ l = m \to (F (l) (x) < a + (\frac{1}{j}) \leftrightarrow F (m) (x) < a + (\frac{1}{j}))$
179	176 178	anbi12d	$⊢ l = m \to ((x \in dom F (l) \land F (l) (x) < a + (\frac{1}{j})) \leftrightarrow (x \in dom F (m) \land F (m) (x) < a + (\frac{1}{j})))$
180	179	rabbidva2	$⊢ l = m \to \{x \in dom F (l) \| F (l) (x) < a + (\frac{1}{j})\} = \{x \in dom F (m) \| F (m) (x) < a + (\frac{1}{j})\}$
181	101	ineq2d	$⊢ l = m \to s \cap dom F (l) = s \cap dom F (m)$
182	180 181	eqeq12d	$⊢ l = m \to (\{x \in dom F (l) \| F (l) (x) < a + (\frac{1}{j})\} = s \cap dom F (l) \leftrightarrow \{x \in dom F (m) \| F (m) (x) < a + (\frac{1}{j})\} = s \cap dom F (m))$
183	182	rabbidv	$⊢ l = m \to \{s \in S \| \{x \in dom F (l) \| F (l) (x) < a + (\frac{1}{j})\} = s \cap dom F (l)\} = \{s \in S \| \{x \in dom F (m) \| F (m) (x) < a + (\frac{1}{j})\} = s \cap dom F (m)\}$
184	175 183	eqtrd	$⊢ l = m \to \{t \in S \| \{y \in dom F (l) \| F (l) (y) < a + (\frac{1}{j})\} = t \cap dom F (l)\} = \{s \in S \| \{x \in dom F (m) \| F (m) (x) < a + (\frac{1}{j})\} = s \cap dom F (m)\}$
185		oveq2	$⊢ j = k \to \frac{1}{j} = \frac{1}{k}$
186	185	oveq2d	$⊢ j = k \to a + (\frac{1}{j}) = a + (\frac{1}{k})$
187	186	breq2d	$⊢ j = k \to (F (m) (x) < a + (\frac{1}{j}) \leftrightarrow F (m) (x) < a + (\frac{1}{k}))$
188	187	rabbidv	$⊢ j = k \to \{x \in dom F (m) \| F (m) (x) < a + (\frac{1}{j})\} = \{x \in dom F (m) \| F (m) (x) < a + (\frac{1}{k})\}$
189	188	eqeq1d	$⊢ j = k \to (\{x \in dom F (m) \| F (m) (x) < a + (\frac{1}{j})\} = s \cap dom F (m) \leftrightarrow \{x \in dom F (m) \| F (m) (x) < a + (\frac{1}{k})\} = s \cap dom F (m))$
190	189	rabbidv	$⊢ j = k \to \{s \in S \| \{x \in dom F (m) \| F (m) (x) < a + (\frac{1}{j})\} = s \cap dom F (m)\} = \{s \in S \| \{x \in dom F (m) \| F (m) (x) < a + (\frac{1}{k})\} = s \cap dom F (m)\}$
191	184 190	sylan9eq	$⊢ (l = m \land j = k) \to \{t \in S \| \{y \in dom F (l) \| F (l) (y) < a + (\frac{1}{j})\} = t \cap dom F (l)\} = \{s \in S \| \{x \in dom F (m) \| F (m) (x) < a + (\frac{1}{k})\} = s \cap dom F (m)\}$
192	158 159 160 161 191	cbvmpo	$⊢ (l \in Z, j \in ℕ ⟼ \{t \in S \| \{y \in dom F (l) \| F (l) (y) < a + (\frac{1}{j})\} = t \cap dom F (l)\}) = (m \in Z, k \in ℕ ⟼ \{s \in S \| \{x \in dom F (m) \| F (m) (x) < a + (\frac{1}{k})\} = s \cap dom F (m)\})$
193	192	eqcomi	$⊢ (m \in Z, k \in ℕ ⟼ \{s \in S \| \{x \in dom F (m) \| F (m) (x) < a + (\frac{1}{k})\} = s \cap dom F (m)\}) = (l \in Z, j \in ℕ ⟼ \{t \in S \| \{y \in dom F (l) \| F (l) (y) < a + (\frac{1}{j})\} = t \cap dom F (l)\})$
194	128 4 129 130 95 148 149 193	smflimlem6	$⊢ (φ \land a \in ℝ) \to \{y \in D \| G (y) \leq a\} \in (S ↾_{𝑡} D)$
195	9 5 44 127 194	issmfled	$⊢ φ \to G \in SMblFn (S)$

Metamath Proof Explorer

Theorem smflim

Proof