smflimlem3

Description: The limit of sigma-measurable functions is sigma-measurable. Proposition 121F (a) of Fremlin1 p. 38 . (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	smflimlem3.z	$⊢ Z = ℤ_{\geq M}$
	smflimlem3.s	$⊢ φ \to S \in SAlg$
	smflimlem3.m	$⊢ (φ \land m \in Z) \to F (m) \in SMblFn (S)$
	smflimlem3.d	$⊢ D = \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| (m \in Z ⟼ F (m) (x)) \in dom ⇝\}$
	smflimlem3.a	$⊢ φ \to A \in ℝ$
	smflimlem3.p	$⊢ P = (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)\})$
	smflimlem3.h	$⊢ H = (m \in Z, k \in ℕ ⟼ C (m P k))$
	smflimlem3.i	$⊢ I = ⋂_{k \in ℕ} ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} (m H k)$
	smflimlem3.c	$⊢ (φ \land y \in ran P) \to C (y) \in y$
	smflimlem3.x	$⊢ φ \to X \in (D \cap I)$
	smflimlem3.k	$⊢ φ \to K \in ℕ$
	smflimlem3.y	$⊢ φ \to Y \in ℝ^{+}$
	smflimlem3.l	$⊢ φ \to \frac{1}{K} < Y$
Assertion	smflimlem3	$⊢ φ \to \exists m \in Z \forall i \in ℤ_{\geq m} (X \in dom F (i) \land F (i) (X) < A + Y)$

Proof

Step	Hyp	Ref	Expression
1		smflimlem3.z	$⊢ Z = ℤ_{\geq M}$
2		smflimlem3.s	$⊢ φ \to S \in SAlg$
3		smflimlem3.m	$⊢ (φ \land m \in Z) \to F (m) \in SMblFn (S)$
4		smflimlem3.d	$⊢ D = \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| (m \in Z ⟼ F (m) (x)) \in dom ⇝\}$
5		smflimlem3.a	$⊢ φ \to A \in ℝ$
6		smflimlem3.p	$⊢ P = (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)\})$
7		smflimlem3.h	$⊢ H = (m \in Z, k \in ℕ ⟼ C (m P k))$
8		smflimlem3.i	$⊢ I = ⋂_{k \in ℕ} ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} (m H k)$
9		smflimlem3.c	$⊢ (φ \land y \in ran P) \to C (y) \in y$
10		smflimlem3.x	$⊢ φ \to X \in (D \cap I)$
11		smflimlem3.k	$⊢ φ \to K \in ℕ$
12		smflimlem3.y	$⊢ φ \to Y \in ℝ^{+}$
13		smflimlem3.l	$⊢ φ \to \frac{1}{K} < Y$
14		ssrab2	$⊢ \{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)$
15	4 14	eqsstri	$⊢ D \subseteq ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m)$
16		inss1	$⊢ D \cap I \subseteq D$
17	16 10	sseldi	$⊢ φ \to X \in D$
18	15 17	sseldi	$⊢ φ \to X \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m)$
19		fveq2	$⊢ i = m \to F (i) = F (m)$
20	19	dmeqd	$⊢ i = m \to dom F (i) = dom F (m)$
21		eqcom	$⊢ i = m \leftrightarrow m = i$
22	21	imbi1i	$⊢ (i = m \to dom F (i) = dom F (m)) \leftrightarrow (m = i \to dom F (i) = dom F (m))$
23		eqcom	$⊢ dom F (i) = dom F (m) \leftrightarrow dom F (m) = dom F (i)$
24	23	imbi2i	$⊢ (m = i \to dom F (i) = dom F (m)) \leftrightarrow (m = i \to dom F (m) = dom F (i))$
25	22 24	bitri	$⊢ (i = m \to dom F (i) = dom F (m)) \leftrightarrow (m = i \to dom F (m) = dom F (i))$
26	20 25	mpbi	$⊢ m = i \to dom F (m) = dom F (i)$
27	26	cbviinv	$⊢ ⋂_{m \in ℤ_{\geq n}} dom F (m) = ⋂_{i \in ℤ_{\geq n}} dom F (i)$
28	27	a1i	$⊢ n \in Z \to ⋂_{m \in ℤ_{\geq n}} dom F (m) = ⋂_{i \in ℤ_{\geq n}} dom F (i)$
29	28	iuneq2i	$⊢ ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) = ⋃_{n \in Z} ⋂_{i \in ℤ_{\geq n}} dom F (i)$
30		fveq2	$⊢ n = m \to ℤ_{\geq n} = ℤ_{\geq m}$
31	30	iineq1d	$⊢ n = m \to ⋂_{i \in ℤ_{\geq n}} dom F (i) = ⋂_{i \in ℤ_{\geq m}} dom F (i)$
32	31	cbviunv	$⊢ ⋃_{n \in Z} ⋂_{i \in ℤ_{\geq n}} dom F (i) = ⋃_{m \in Z} ⋂_{i \in ℤ_{\geq m}} dom F (i)$
33	29 32	eqtri	$⊢ ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) = ⋃_{m \in Z} ⋂_{i \in ℤ_{\geq m}} dom F (i)$
34	18 33	eleqtrdi	$⊢ φ \to X \in ⋃_{m \in Z} ⋂_{i \in ℤ_{\geq m}} dom F (i)$
35		eqid	$⊢ ⋃_{m \in Z} ⋂_{i \in ℤ_{\geq m}} dom F (i) = ⋃_{m \in Z} ⋂_{i \in ℤ_{\geq m}} dom F (i)$
36	1 35	allbutfi	$⊢ X \in ⋃_{m \in Z} ⋂_{i \in ℤ_{\geq m}} dom F (i) \leftrightarrow \exists m \in Z \forall i \in ℤ_{\geq m} X \in dom F (i)$
37	36	biimpi	$⊢ X \in ⋃_{m \in Z} ⋂_{i \in ℤ_{\geq m}} dom F (i) \to \exists m \in Z \forall i \in ℤ_{\geq m} X \in dom F (i)$
38	34 37	syl	$⊢ φ \to \exists m \in Z \forall i \in ℤ_{\geq m} X \in dom F (i)$
39	10	elin2d	$⊢ φ \to X \in I$
40		oveq1	$⊢ m = i \to m H k = i H k$
41	40	cbviinv	$⊢ ⋂_{m \in ℤ_{\geq n}} (m H k) = ⋂_{i \in ℤ_{\geq n}} (i H k)$
42	41	a1i	$⊢ n \in Z \to ⋂_{m \in ℤ_{\geq n}} (m H k) = ⋂_{i \in ℤ_{\geq n}} (i H k)$
43	42	iuneq2i	$⊢ ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} (m H k) = ⋃_{n \in Z} ⋂_{i \in ℤ_{\geq n}} (i H k)$
44	30	iineq1d	$⊢ n = m \to ⋂_{i \in ℤ_{\geq n}} (i H k) = ⋂_{i \in ℤ_{\geq m}} (i H k)$
45	44	cbviunv	$⊢ ⋃_{n \in Z} ⋂_{i \in ℤ_{\geq n}} (i H k) = ⋃_{m \in Z} ⋂_{i \in ℤ_{\geq m}} (i H k)$
46	43 45	eqtri	$⊢ ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} (m H k) = ⋃_{m \in Z} ⋂_{i \in ℤ_{\geq m}} (i H k)$
47	46	a1i	$⊢ k \in ℕ \to ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} (m H k) = ⋃_{m \in Z} ⋂_{i \in ℤ_{\geq m}} (i H k)$
48	47	iineq2i	$⊢ ⋂_{k \in ℕ} ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} (m H k) = ⋂_{k \in ℕ} ⋃_{m \in Z} ⋂_{i \in ℤ_{\geq m}} (i H k)$
49	8 48	eqtri	$⊢ I = ⋂_{k \in ℕ} ⋃_{m \in Z} ⋂_{i \in ℤ_{\geq m}} (i H k)$
50	39 49	eleqtrdi	$⊢ φ \to X \in ⋂_{k \in ℕ} ⋃_{m \in Z} ⋂_{i \in ℤ_{\geq m}} (i H k)$
51		oveq2	$⊢ k = K \to i H k = i H K$
52	51	adantr	$⊢ (k = K \land i \in ℤ_{\geq m}) \to i H k = i H K$
53	52	iineq2dv	$⊢ k = K \to ⋂_{i \in ℤ_{\geq m}} (i H k) = ⋂_{i \in ℤ_{\geq m}} (i H K)$
54	53	iuneq2d	$⊢ k = K \to ⋃_{m \in Z} ⋂_{i \in ℤ_{\geq m}} (i H k) = ⋃_{m \in Z} ⋂_{i \in ℤ_{\geq m}} (i H K)$
55	54	eleq2d	$⊢ k = K \to (X \in ⋃_{m \in Z} ⋂_{i \in ℤ_{\geq m}} (i H k) \leftrightarrow X \in ⋃_{m \in Z} ⋂_{i \in ℤ_{\geq m}} (i H K))$
56	50 11 55	eliind	$⊢ φ \to X \in ⋃_{m \in Z} ⋂_{i \in ℤ_{\geq m}} (i H K)$
57		eqid	$⊢ ⋃_{m \in Z} ⋂_{i \in ℤ_{\geq m}} (i H K) = ⋃_{m \in Z} ⋂_{i \in ℤ_{\geq m}} (i H K)$
58	1 57	allbutfi	$⊢ X \in ⋃_{m \in Z} ⋂_{i \in ℤ_{\geq m}} (i H K) \leftrightarrow \exists m \in Z \forall i \in ℤ_{\geq m} X \in (i H K)$
59	56 58	sylib	$⊢ φ \to \exists m \in Z \forall i \in ℤ_{\geq m} X \in (i H K)$
60	38 59	jca	$⊢ φ \to (\exists m \in Z \forall i \in ℤ_{\geq m} X \in dom F (i) \land \exists m \in Z \forall i \in ℤ_{\geq m} X \in (i H K))$
61	1	rexanuz2	$⊢ \exists m \in Z \forall i \in ℤ_{\geq m} (X \in dom F (i) \land X \in (i H K)) \leftrightarrow (\exists m \in Z \forall i \in ℤ_{\geq m} X \in dom F (i) \land \exists m \in Z \forall i \in ℤ_{\geq m} X \in (i H K))$
62	60 61	sylibr	$⊢ φ \to \exists m \in Z \forall i \in ℤ_{\geq m} (X \in dom F (i) \land X \in (i H K))$
63		simpll	$⊢ ((φ \land m \in Z) \land i \in ℤ_{\geq m}) \to φ$
64		simpr	$⊢ (φ \land m \in Z) \to m \in Z$
65	1	uztrn2	$⊢ (m \in Z \land i \in ℤ_{\geq m}) \to i \in Z$
66	64 65	sylan	$⊢ ((φ \land m \in Z) \land i \in ℤ_{\geq m}) \to i \in Z$
67		simprl	$⊢ ((φ \land i \in Z) \land (X \in dom F (i) \land X \in (i H K))) \to X \in dom F (i)$
68		simp3	$⊢ (φ \land i \in Z \land X \in (i H K)) \to X \in (i H K)$
69	7	a1i	$⊢ (φ \land i \in Z) \to H = (m \in Z, k \in ℕ ⟼ C (m P k))$
70		oveq12	$⊢ (m = i \land k = K) \to m P k = i P K$
71	70	fveq2d	$⊢ (m = i \land k = K) \to C (m P k) = C (i P K)$
72	71	adantl	$⊢ ((φ \land i \in Z) \land (m = i \land k = K)) \to C (m P k) = C (i P K)$
73		simpr	$⊢ (φ \land i \in Z) \to i \in Z$
74	11	adantr	$⊢ (φ \land i \in Z) \to K \in ℕ$
75		fvexd	$⊢ (φ \land i \in Z) \to C (i P K) \in V$
76	69 72 73 74 75	ovmpod	$⊢ (φ \land i \in Z) \to i H K = C (i P K)$
77	76	3adant3	$⊢ (φ \land i \in Z \land X \in (i H K)) \to i H K = C (i P K)$
78	68 77	eleqtrd	$⊢ (φ \land i \in Z \land X \in (i H K)) \to X \in C (i P K)$
79	78	3expa	$⊢ ((φ \land i \in Z) \land X \in (i H K)) \to X \in C (i P K)$
80	79	adantrl	$⊢ ((φ \land i \in Z) \land (X \in dom F (i) \land X \in (i H K))) \to X \in C (i P K)$
81	80 67	elind	$⊢ ((φ \land i \in Z) \land (X \in dom F (i) \land X \in (i H K))) \to X \in (C (i P K) \cap dom F (i))$
82		eqid	$⊢ \{s \in S \| \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\} = 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)\}$
83	82 2	rabexd	$⊢ φ \to \{s \in S \| \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\} = s \cap dom F (m)\} \in V$
84	83	ralrimivw	$⊢ φ \to \forall k \in ℕ \{s \in S \| \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\} = s \cap dom F (m)\} \in V$
85	84	a1d	$⊢ φ \to (m \in Z \to \forall k \in ℕ \{s \in S \| \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\} = s \cap dom F (m)\} \in V)$
86	85	imp	$⊢ (φ \land m \in Z) \to \forall k \in ℕ \{s \in S \| \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\} = s \cap dom F (m)\} \in V$
87	86	ralrimiva	$⊢ φ \to \forall m \in Z \forall k \in ℕ \{s \in S \| \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\} = s \cap dom F (m)\} \in V$
88	6	fnmpo	$⊢ \forall m \in Z \forall k \in ℕ \{s \in S \| \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\} = s \cap dom F (m)\} \in V \to P Fn (Z \times ℕ)$
89	87 88	syl	$⊢ φ \to P Fn (Z \times ℕ)$
90	89	adantr	$⊢ (φ \land i \in Z) \to P Fn (Z \times ℕ)$
91		fnovrn	$⊢ (P Fn (Z \times ℕ) \land i \in Z \land K \in ℕ) \to i P K \in ran P$
92	90 73 74 91	syl3anc	$⊢ (φ \land i \in Z) \to i P K \in ran P$
93		ovex	$⊢ i P K \in V$
94		eleq1	$⊢ y = i P K \to (y \in ran P \leftrightarrow i P K \in ran P)$
95	94	anbi2d	$⊢ y = i P K \to ((φ \land y \in ran P) \leftrightarrow (φ \land i P K \in ran P))$
96		fveq2	$⊢ y = i P K \to C (y) = C (i P K)$
97		id	$⊢ y = i P K \to y = i P K$
98	96 97	eleq12d	$⊢ y = i P K \to (C (y) \in y \leftrightarrow C (i P K) \in (i P K))$
99	95 98	imbi12d	$⊢ y = i P K \to (((φ \land y \in ran P) \to C (y) \in y) \leftrightarrow ((φ \land i P K \in ran P) \to C (i P K) \in (i P K)))$
100	93 99 9	vtocl	$⊢ (φ \land i P K \in ran P) \to C (i P K) \in (i P K)$
101	92 100	syldan	$⊢ (φ \land i \in Z) \to C (i P K) \in (i P K)$
102	6	a1i	$⊢ (φ \land i \in Z) \to P = (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)\})$
103	26	adantr	$⊢ (m = i \land k = K) \to dom F (m) = dom F (i)$
104	19	fveq1d	$⊢ i = m \to F (i) (x) = F (m) (x)$
105	21	imbi1i	$⊢ (i = m \to F (i) (x) = F (m) (x)) \leftrightarrow (m = i \to F (i) (x) = F (m) (x))$
106		eqcom	$⊢ F (i) (x) = F (m) (x) \leftrightarrow F (m) (x) = F (i) (x)$
107	106	imbi2i	$⊢ (m = i \to F (i) (x) = F (m) (x)) \leftrightarrow (m = i \to F (m) (x) = F (i) (x))$
108	105 107	bitri	$⊢ (i = m \to F (i) (x) = F (m) (x)) \leftrightarrow (m = i \to F (m) (x) = F (i) (x))$
109	104 108	mpbi	$⊢ m = i \to F (m) (x) = F (i) (x)$
110	109	adantr	$⊢ (m = i \land k = K) \to F (m) (x) = F (i) (x)$
111		oveq2	$⊢ k = K \to \frac{1}{k} = \frac{1}{K}$
112	111	oveq2d	$⊢ k = K \to A + (\frac{1}{k}) = A + (\frac{1}{K})$
113	112	adantl	$⊢ (m = i \land k = K) \to A + (\frac{1}{k}) = A + (\frac{1}{K})$
114	110 113	breq12d	$⊢ (m = i \land k = K) \to (F (m) (x) < A + (\frac{1}{k}) \leftrightarrow F (i) (x) < A + (\frac{1}{K}))$
115	103 114	rabeqbidv	$⊢ (m = i \land k = K) \to \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\} = \{x \in dom F (i) \| F (i) (x) < A + (\frac{1}{K})\}$
116	26	ineq2d	$⊢ m = i \to s \cap dom F (m) = s \cap dom F (i)$
117	116	adantr	$⊢ (m = i \land k = K) \to s \cap dom F (m) = s \cap dom F (i)$
118	115 117	eqeq12d	$⊢ (m = i \land k = K) \to (\{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\} = s \cap dom F (m) \leftrightarrow \{x \in dom F (i) \| F (i) (x) < A + (\frac{1}{K})\} = s \cap dom F (i))$
119	118	rabbidv	$⊢ (m = i \land k = K) \to \{s \in S \| \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\} = s \cap dom F (m)\} = \{s \in S \| \{x \in dom F (i) \| F (i) (x) < A + (\frac{1}{K})\} = s \cap dom F (i)\}$
120	119	adantl	$⊢ ((φ \land i \in Z) \land (m = i \land k = K)) \to \{s \in S \| \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\} = s \cap dom F (m)\} = \{s \in S \| \{x \in dom F (i) \| F (i) (x) < A + (\frac{1}{K})\} = s \cap dom F (i)\}$
121		eqid	$⊢ \{s \in S \| \{x \in dom F (i) \| F (i) (x) < A + (\frac{1}{K})\} = s \cap dom F (i)\} = \{s \in S \| \{x \in dom F (i) \| F (i) (x) < A + (\frac{1}{K})\} = s \cap dom F (i)\}$
122	121 2	rabexd	$⊢ φ \to \{s \in S \| \{x \in dom F (i) \| F (i) (x) < A + (\frac{1}{K})\} = s \cap dom F (i)\} \in V$
123	122	adantr	$⊢ (φ \land i \in Z) \to \{s \in S \| \{x \in dom F (i) \| F (i) (x) < A + (\frac{1}{K})\} = s \cap dom F (i)\} \in V$
124	102 120 73 74 123	ovmpod	$⊢ (φ \land i \in Z) \to i P K = \{s \in S \| \{x \in dom F (i) \| F (i) (x) < A + (\frac{1}{K})\} = s \cap dom F (i)\}$
125	101 124	eleqtrd	$⊢ (φ \land i \in Z) \to C (i P K) \in \{s \in S \| \{x \in dom F (i) \| F (i) (x) < A + (\frac{1}{K})\} = s \cap dom F (i)\}$
126		ineq1	$⊢ s = C (i P K) \to s \cap dom F (i) = C (i P K) \cap dom F (i)$
127	126	eqeq2d	$⊢ s = C (i P K) \to (\{x \in dom F (i) \| F (i) (x) < A + (\frac{1}{K})\} = s \cap dom F (i) \leftrightarrow \{x \in dom F (i) \| F (i) (x) < A + (\frac{1}{K})\} = C (i P K) \cap dom F (i))$
128	127	elrab	$⊢ C (i P K) \in \{s \in S \| \{x \in dom F (i) \| F (i) (x) < A + (\frac{1}{K})\} = s \cap dom F (i)\} \leftrightarrow (C (i P K) \in S \land \{x \in dom F (i) \| F (i) (x) < A + (\frac{1}{K})\} = C (i P K) \cap dom F (i))$
129	125 128	sylib	$⊢ (φ \land i \in Z) \to (C (i P K) \in S \land \{x \in dom F (i) \| F (i) (x) < A + (\frac{1}{K})\} = C (i P K) \cap dom F (i))$
130	129	simprd	$⊢ (φ \land i \in Z) \to \{x \in dom F (i) \| F (i) (x) < A + (\frac{1}{K})\} = C (i P K) \cap dom F (i)$
131	130	eqcomd	$⊢ (φ \land i \in Z) \to C (i P K) \cap dom F (i) = \{x \in dom F (i) \| F (i) (x) < A + (\frac{1}{K})\}$
132	131	adantr	$⊢ ((φ \land i \in Z) \land (X \in dom F (i) \land X \in (i H K))) \to C (i P K) \cap dom F (i) = \{x \in dom F (i) \| F (i) (x) < A + (\frac{1}{K})\}$
133	81 132	eleqtrd	$⊢ ((φ \land i \in Z) \land (X \in dom F (i) \land X \in (i H K))) \to X \in \{x \in dom F (i) \| F (i) (x) < A + (\frac{1}{K})\}$
134		fveq2	$⊢ x = X \to F (i) (x) = F (i) (X)$
135		eqidd	$⊢ x = X \to A + (\frac{1}{K}) = A + (\frac{1}{K})$
136	134 135	breq12d	$⊢ x = X \to (F (i) (x) < A + (\frac{1}{K}) \leftrightarrow F (i) (X) < A + (\frac{1}{K}))$
137	136	elrab	$⊢ X \in \{x \in dom F (i) \| F (i) (x) < A + (\frac{1}{K})\} \leftrightarrow (X \in dom F (i) \land F (i) (X) < A + (\frac{1}{K}))$
138	133 137	sylib	$⊢ ((φ \land i \in Z) \land (X \in dom F (i) \land X \in (i H K))) \to (X \in dom F (i) \land F (i) (X) < A + (\frac{1}{K}))$
139	138	simprd	$⊢ ((φ \land i \in Z) \land (X \in dom F (i) \land X \in (i H K))) \to F (i) (X) < A + (\frac{1}{K})$
140	67 139	jca	$⊢ ((φ \land i \in Z) \land (X \in dom F (i) \land X \in (i H K))) \to (X \in dom F (i) \land F (i) (X) < A + (\frac{1}{K}))$
141	140	ex	$⊢ (φ \land i \in Z) \to ((X \in dom F (i) \land X \in (i H K)) \to (X \in dom F (i) \land F (i) (X) < A + (\frac{1}{K})))$
142	63 66 141	syl2anc	$⊢ ((φ \land m \in Z) \land i \in ℤ_{\geq m}) \to ((X \in dom F (i) \land X \in (i H K)) \to (X \in dom F (i) \land F (i) (X) < A + (\frac{1}{K})))$
143	142	ralimdva	$⊢ (φ \land m \in Z) \to (\forall i \in ℤ_{\geq m} (X \in dom F (i) \land X \in (i H K)) \to \forall i \in ℤ_{\geq m} (X \in dom F (i) \land F (i) (X) < A + (\frac{1}{K})))$
144	143	reximdva	$⊢ φ \to (\exists m \in Z \forall i \in ℤ_{\geq m} (X \in dom F (i) \land X \in (i H K)) \to \exists m \in Z \forall i \in ℤ_{\geq m} (X \in dom F (i) \land F (i) (X) < A + (\frac{1}{K})))$
145	62 144	mpd	$⊢ φ \to \exists m \in Z \forall i \in ℤ_{\geq m} (X \in dom F (i) \land F (i) (X) < A + (\frac{1}{K}))$
146		simprl	$⊢ ((φ \land i \in Z) \land (X \in dom F (i) \land F (i) (X) < A + (\frac{1}{K}))) \to X \in dom F (i)$
147		eleq1	$⊢ m = i \to (m \in Z \leftrightarrow i \in Z)$
148	147	anbi2d	$⊢ m = i \to ((φ \land m \in Z) \leftrightarrow (φ \land i \in Z))$
149		fveq2	$⊢ m = i \to F (m) = F (i)$
150	149 26	feq12d	$⊢ m = i \to (F (m) : dom F (m) ⟶ ℝ \leftrightarrow F (i) : dom F (i) ⟶ ℝ)$
151	148 150	imbi12d	$⊢ m = i \to (((φ \land m \in Z) \to F (m) : dom F (m) ⟶ ℝ) \leftrightarrow ((φ \land i \in Z) \to F (i) : dom F (i) ⟶ ℝ))$
152	2	adantr	$⊢ (φ \land m \in Z) \to S \in SAlg$
153		eqid	$⊢ dom F (m) = dom F (m)$
154	152 3 153	smff	$⊢ (φ \land m \in Z) \to F (m) : dom F (m) ⟶ ℝ$
155	151 154	chvarvv	$⊢ (φ \land i \in Z) \to F (i) : dom F (i) ⟶ ℝ$
156	155	adantr	$⊢ ((φ \land i \in Z) \land X \in dom F (i)) \to F (i) : dom F (i) ⟶ ℝ$
157		simpr	$⊢ ((φ \land i \in Z) \land X \in dom F (i)) \to X \in dom F (i)$
158	156 157	ffvelrnd	$⊢ ((φ \land i \in Z) \land X \in dom F (i)) \to F (i) (X) \in ℝ$
159	158	adantrr	$⊢ ((φ \land i \in Z) \land (X \in dom F (i) \land F (i) (X) < A + (\frac{1}{K}))) \to F (i) (X) \in ℝ$
160	11	nnrecred	$⊢ φ \to \frac{1}{K} \in ℝ$
161	5 160	readdcld	$⊢ φ \to A + (\frac{1}{K}) \in ℝ$
162	161	ad2antrr	$⊢ ((φ \land i \in Z) \land (X \in dom F (i) \land F (i) (X) < A + (\frac{1}{K}))) \to A + (\frac{1}{K}) \in ℝ$
163	12	rpred	$⊢ φ \to Y \in ℝ$
164	5 163	readdcld	$⊢ φ \to A + Y \in ℝ$
165	164	ad2antrr	$⊢ ((φ \land i \in Z) \land (X \in dom F (i) \land F (i) (X) < A + (\frac{1}{K}))) \to A + Y \in ℝ$
166		simprr	$⊢ ((φ \land i \in Z) \land (X \in dom F (i) \land F (i) (X) < A + (\frac{1}{K}))) \to F (i) (X) < A + (\frac{1}{K})$
167	160 163 5 13	ltadd2dd	$⊢ φ \to A + (\frac{1}{K}) < A + Y$
168	167	ad2antrr	$⊢ ((φ \land i \in Z) \land (X \in dom F (i) \land F (i) (X) < A + (\frac{1}{K}))) \to A + (\frac{1}{K}) < A + Y$
169	159 162 165 166 168	lttrd	$⊢ ((φ \land i \in Z) \land (X \in dom F (i) \land F (i) (X) < A + (\frac{1}{K}))) \to F (i) (X) < A + Y$
170	146 169	jca	$⊢ ((φ \land i \in Z) \land (X \in dom F (i) \land F (i) (X) < A + (\frac{1}{K}))) \to (X \in dom F (i) \land F (i) (X) < A + Y)$
171	170	ex	$⊢ (φ \land i \in Z) \to ((X \in dom F (i) \land F (i) (X) < A + (\frac{1}{K})) \to (X \in dom F (i) \land F (i) (X) < A + Y))$
172	63 66 171	syl2anc	$⊢ ((φ \land m \in Z) \land i \in ℤ_{\geq m}) \to ((X \in dom F (i) \land F (i) (X) < A + (\frac{1}{K})) \to (X \in dom F (i) \land F (i) (X) < A + Y))$
173	172	ralimdva	$⊢ (φ \land m \in Z) \to (\forall i \in ℤ_{\geq m} (X \in dom F (i) \land F (i) (X) < A + (\frac{1}{K})) \to \forall i \in ℤ_{\geq m} (X \in dom F (i) \land F (i) (X) < A + Y))$
174	173	reximdva	$⊢ φ \to (\exists m \in Z \forall i \in ℤ_{\geq m} (X \in dom F (i) \land F (i) (X) < A + (\frac{1}{K})) \to \exists m \in Z \forall i \in ℤ_{\geq m} (X \in dom F (i) \land F (i) (X) < A + Y))$
175	145 174	mpd	$⊢ φ \to \exists m \in Z \forall i \in ℤ_{\geq m} (X \in dom F (i) \land F (i) (X) < A + Y)$

Metamath Proof Explorer

Theorem smflimlem3

Proof