smflimlem2

Description: Lemma for the proof that the limit of sigma-measurable functions is sigma-measurable, Proposition 121F (a) of Fremlin1 p. 38 . This lemma proves one-side of the double inclusion for the proof that the preimages of right-closed, unbounded-below intervals are in the subspace sigma-algebra induced by D . (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	smflimlem2.1	$⊢ Z = ℤ_{\geq M}$
	smflimlem2.2	$⊢ φ \to S \in SAlg$
	smflimlem2.3	$⊢ φ \to F : Z ⟶ SMblFn (S)$
	smflimlem2.4	$⊢ D = \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| (m \in Z ⟼ F (m) (x)) \in dom ⇝\}$
	smflimlem2.5	$⊢ G = (x \in D ⟼ ⇝ ((m \in Z ⟼ F (m) (x))))$
	smflimlem2.6	$⊢ φ \to A \in ℝ$
	smflimlem2.7	$⊢ 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)\})$
	smflimlem2.8	$⊢ H = (m \in Z, k \in ℕ ⟼ C (m P k))$
	smflimlem2.9	$⊢ I = ⋂_{k \in ℕ} ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} (m H k)$
	smflimlem2.10	$⊢ (φ \land r \in ran P) \to C (r) \in r$
Assertion	smflimlem2	$⊢ φ \to \{x \in D \| G (x) \leq A\} \subseteq D \cap I$

Proof

Step	Hyp	Ref	Expression
1		smflimlem2.1	$⊢ Z = ℤ_{\geq M}$
2		smflimlem2.2	$⊢ φ \to S \in SAlg$
3		smflimlem2.3	$⊢ φ \to F : Z ⟶ SMblFn (S)$
4		smflimlem2.4	$⊢ D = \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| (m \in Z ⟼ F (m) (x)) \in dom ⇝\}$
5		smflimlem2.5	$⊢ G = (x \in D ⟼ ⇝ ((m \in Z ⟼ F (m) (x))))$
6		smflimlem2.6	$⊢ φ \to A \in ℝ$
7		smflimlem2.7	$⊢ 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)\})$
8		smflimlem2.8	$⊢ H = (m \in Z, k \in ℕ ⟼ C (m P k))$
9		smflimlem2.9	$⊢ I = ⋂_{k \in ℕ} ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} (m H k)$
10		smflimlem2.10	$⊢ (φ \land r \in ran P) \to C (r) \in r$
11		nfrab1	$⊢ \underline{Ⅎ} x \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| (m \in Z ⟼ F (m) (x)) \in dom ⇝\}$
12	4 11	nfcxfr	$⊢ \underline{Ⅎ} x D$
13	12	ssrab2f	$⊢ \{x \in D \| G (x) \leq A\} \subseteq D$
14	13	a1i	$⊢ φ \to \{x \in D \| G (x) \leq A\} \subseteq D$
15		simpllr	$⊢ (((φ \land x \in D) \land G (x) \leq A) \land k \in ℕ) \to x \in D$
16		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)$
17	4 16	eqsstri	$⊢ D \subseteq ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m)$
18	17	sseli	$⊢ x \in D \to x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m)$
19		fveq2	$⊢ n = i \to ℤ_{\geq n} = ℤ_{\geq i}$
20	19	iineq1d	$⊢ n = i \to ⋂_{m \in ℤ_{\geq n}} dom F (m) = ⋂_{m \in ℤ_{\geq i}} dom F (m)$
21	20	cbviunv	$⊢ ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) = ⋃_{i \in Z} ⋂_{m \in ℤ_{\geq i}} dom F (m)$
22	21	eleq2i	$⊢ x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \leftrightarrow x \in ⋃_{i \in Z} ⋂_{m \in ℤ_{\geq i}} dom F (m)$
23		eliun	$⊢ x \in ⋃_{i \in Z} ⋂_{m \in ℤ_{\geq i}} dom F (m) \leftrightarrow \exists i \in Z x \in ⋂_{m \in ℤ_{\geq i}} dom F (m)$
24	22 23	bitri	$⊢ x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \leftrightarrow \exists i \in Z x \in ⋂_{m \in ℤ_{\geq i}} dom F (m)$
25	18 24	sylib	$⊢ x \in D \to \exists i \in Z x \in ⋂_{m \in ℤ_{\geq i}} dom F (m)$
26	15 25	syl	$⊢ (((φ \land x \in D) \land G (x) \leq A) \land k \in ℕ) \to \exists i \in Z x \in ⋂_{m \in ℤ_{\geq i}} dom F (m)$
27		nfv	$⊢ Ⅎ m ((φ \land x \in D) \land G (x) \leq A)$
28		nfv	$⊢ Ⅎ m k \in ℕ$
29	27 28	nfan	$⊢ Ⅎ m (((φ \land x \in D) \land G (x) \leq A) \land k \in ℕ)$
30		nfv	$⊢ Ⅎ m i \in Z$
31	29 30	nfan	$⊢ Ⅎ m ((((φ \land x \in D) \land G (x) \leq A) \land k \in ℕ) \land i \in Z)$
32		nfcv	$⊢ \underline{Ⅎ} m x$
33		nfii1	$⊢ \underline{Ⅎ} m ⋂_{m \in ℤ_{\geq i}} dom F (m)$
34	32 33	nfel	$⊢ Ⅎ m x \in ⋂_{m \in ℤ_{\geq i}} dom F (m)$
35	31 34	nfan	$⊢ Ⅎ m (((((φ \land x \in D) \land G (x) \leq A) \land k \in ℕ) \land i \in Z) \land x \in ⋂_{m \in ℤ_{\geq i}} dom F (m))$
36		nfmpt1	$⊢ \underline{Ⅎ} m (m \in Z ⟼ F (m) (x))$
37		eqid	$⊢ ℤ_{\geq i} = ℤ_{\geq i}$
38		uzssz	$⊢ ℤ_{\geq M} \subseteq ℤ$
39	1	eleq2i	$⊢ i \in Z \leftrightarrow i \in ℤ_{\geq M}$
40	39	biimpi	$⊢ i \in Z \to i \in ℤ_{\geq M}$
41	38 40	sseldi	$⊢ i \in Z \to i \in ℤ$
42		uzid	$⊢ i \in ℤ \to i \in ℤ_{\geq i}$
43	41 42	syl	$⊢ i \in Z \to i \in ℤ_{\geq i}$
44	43	ad2antlr	$⊢ (((((φ \land x \in D) \land G (x) \leq A) \land k \in ℕ) \land i \in Z) \land x \in ⋂_{m \in ℤ_{\geq i}} dom F (m)) \to i \in ℤ_{\geq i}$
45		simplll	$⊢ ((((φ \land x \in D) \land i \in Z) \land x \in ⋂_{m \in ℤ_{\geq i}} dom F (m)) \land m \in ℤ_{\geq i}) \to (φ \land x \in D)$
46	45	simpld	$⊢ ((((φ \land x \in D) \land i \in Z) \land x \in ⋂_{m \in ℤ_{\geq i}} dom F (m)) \land m \in ℤ_{\geq i}) \to φ$
47		uzss	$⊢ i \in ℤ_{\geq M} \to ℤ_{\geq i} \subseteq ℤ_{\geq M}$
48	40 47	syl	$⊢ i \in Z \to ℤ_{\geq i} \subseteq ℤ_{\geq M}$
49	48 1	sseqtrrdi	$⊢ i \in Z \to ℤ_{\geq i} \subseteq Z$
50	49	sselda	$⊢ (i \in Z \land m \in ℤ_{\geq i}) \to m \in Z$
51	50	ad4ant24	$⊢ ((((φ \land x \in D) \land i \in Z) \land x \in ⋂_{m \in ℤ_{\geq i}} dom F (m)) \land m \in ℤ_{\geq i}) \to m \in Z$
52		eliinid	$⊢ (x \in ⋂_{m \in ℤ_{\geq i}} dom F (m) \land m \in ℤ_{\geq i}) \to x \in dom F (m)$
53	52	adantll	$⊢ ((((φ \land x \in D) \land i \in Z) \land x \in ⋂_{m \in ℤ_{\geq i}} dom F (m)) \land m \in ℤ_{\geq i}) \to x \in dom F (m)$
54		eqidd	$⊢ φ \to (m \in Z ⟼ F (m) (x)) = (m \in Z ⟼ F (m) (x))$
55		fvexd	$⊢ (φ \land m \in Z) \to F (m) (x) \in V$
56	54 55	fvmpt2d	$⊢ (φ \land m \in Z) \to (m \in Z ⟼ F (m) (x)) (m) = F (m) (x)$
57	56	3adant3	$⊢ (φ \land m \in Z \land x \in dom F (m)) \to (m \in Z ⟼ F (m) (x)) (m) = F (m) (x)$
58	2	adantr	$⊢ (φ \land m \in Z) \to S \in SAlg$
59	3	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	3adant3	$⊢ (φ \land m \in Z \land x \in dom F (m)) \to F (m) : dom F (m) ⟶ ℝ$
63		simp3	$⊢ (φ \land m \in Z \land x \in dom F (m)) \to x \in dom F (m)$
64	62 63	ffvelrnd	$⊢ (φ \land m \in Z \land x \in dom F (m)) \to F (m) (x) \in ℝ$
65	57 64	eqeltrd	$⊢ (φ \land m \in Z \land x \in dom F (m)) \to (m \in Z ⟼ F (m) (x)) (m) \in ℝ$
66	46 51 53 65	syl3anc	$⊢ ((((φ \land x \in D) \land i \in Z) \land x \in ⋂_{m \in ℤ_{\geq i}} dom F (m)) \land m \in ℤ_{\geq i}) \to (m \in Z ⟼ F (m) (x)) (m) \in ℝ$
67	66	adantl3r	$⊢ (((((φ \land x \in D) \land G (x) \leq A) \land i \in Z) \land x \in ⋂_{m \in ℤ_{\geq i}} dom F (m)) \land m \in ℤ_{\geq i}) \to (m \in Z ⟼ F (m) (x)) (m) \in ℝ$
68	67	adantl3r	$⊢ ((((((φ \land x \in D) \land G (x) \leq A) \land k \in ℕ) \land i \in Z) \land x \in ⋂_{m \in ℤ_{\geq i}} dom F (m)) \land m \in ℤ_{\geq i}) \to (m \in Z ⟼ F (m) (x)) (m) \in ℝ$
69	4	eleq2i	$⊢ x \in D \leftrightarrow x \in \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| (m \in Z ⟼ F (m) (x)) \in dom ⇝\}$
70	69	biimpi	$⊢ x \in D \to x \in \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| (m \in Z ⟼ F (m) (x)) \in dom ⇝\}$
71		rabidim2	$⊢ x \in \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| (m \in Z ⟼ F (m) (x)) \in dom ⇝\} \to (m \in Z ⟼ F (m) (x)) \in dom ⇝$
72	70 71	syl	$⊢ x \in D \to (m \in Z ⟼ F (m) (x)) \in dom ⇝$
73		climdm	$⊢ (m \in Z ⟼ F (m) (x)) \in dom ⇝ \leftrightarrow (m \in Z ⟼ F (m) (x)) ⇝ ⇝ ((m \in Z ⟼ F (m) (x)))$
74	72 73	sylib	$⊢ x \in D \to (m \in Z ⟼ F (m) (x)) ⇝ ⇝ ((m \in Z ⟼ F (m) (x)))$
75	74	adantl	$⊢ (φ \land x \in D) \to (m \in Z ⟼ F (m) (x)) ⇝ ⇝ ((m \in Z ⟼ F (m) (x)))$
76	75 73	sylibr	$⊢ (φ \land x \in D) \to (m \in Z ⟼ F (m) (x)) \in dom ⇝$
77	76 73	sylib	$⊢ (φ \land x \in D) \to (m \in Z ⟼ F (m) (x)) ⇝ ⇝ ((m \in Z ⟼ F (m) (x)))$
78		nfcv	$⊢ \underline{Ⅎ} x F$
79		simpr	$⊢ (φ \land x \in D) \to x \in D$
80	12 78 5 79	fnlimfv	$⊢ (φ \land x \in D) \to G (x) = ⇝ ((m \in Z ⟼ F (m) (x)))$
81	80	eqcomd	$⊢ (φ \land x \in D) \to ⇝ ((m \in Z ⟼ F (m) (x))) = G (x)$
82	77 81	breqtrd	$⊢ (φ \land x \in D) \to (m \in Z ⟼ F (m) (x)) ⇝ G (x)$
83	82	ad4antr	$⊢ (((((φ \land x \in D) \land G (x) \leq A) \land k \in ℕ) \land i \in Z) \land x \in ⋂_{m \in ℤ_{\geq i}} dom F (m)) \to (m \in Z ⟼ F (m) (x)) ⇝ G (x)$
84	6	ad5antr	$⊢ (((((φ \land x \in D) \land G (x) \leq A) \land k \in ℕ) \land i \in Z) \land x \in ⋂_{m \in ℤ_{\geq i}} dom F (m)) \to A \in ℝ$
85		simp-4r	$⊢ (((((φ \land x \in D) \land G (x) \leq A) \land k \in ℕ) \land i \in Z) \land x \in ⋂_{m \in ℤ_{\geq i}} dom F (m)) \to G (x) \leq A$
86		simpllr	$⊢ (((((φ \land x \in D) \land G (x) \leq A) \land k \in ℕ) \land i \in Z) \land x \in ⋂_{m \in ℤ_{\geq i}} dom F (m)) \to k \in ℕ$
87		nnrecrp	$⊢ k \in ℕ \to \frac{1}{k} \in ℝ^{+}$
88	86 87	syl	$⊢ (((((φ \land x \in D) \land G (x) \leq A) \land k \in ℕ) \land i \in Z) \land x \in ⋂_{m \in ℤ_{\geq i}} dom F (m)) \to \frac{1}{k} \in ℝ^{+}$
89	35 36 37 44 68 83 84 85 88	climleltrp	$⊢ (((((φ \land x \in D) \land G (x) \leq A) \land k \in ℕ) \land i \in Z) \land x \in ⋂_{m \in ℤ_{\geq i}} dom F (m)) \to \exists n \in ℤ_{\geq i} \forall m \in ℤ_{\geq n} ((m \in Z ⟼ F (m) (x)) (m) \in ℝ \land (m \in Z ⟼ F (m) (x)) (m) < A + (\frac{1}{k}))$
90		simp-6l	$⊢ ((((((φ \land x \in D) \land G (x) \leq A) \land k \in ℕ) \land i \in Z) \land x \in ⋂_{m \in ℤ_{\geq i}} dom F (m)) \land n \in ℤ_{\geq i}) \to φ$
91		simplr	$⊢ (((((φ \land x \in D) \land G (x) \leq A) \land k \in ℕ) \land i \in Z) \land x \in ⋂_{m \in ℤ_{\geq i}} dom F (m)) \to i \in Z$
92	91	adantr	$⊢ ((((((φ \land x \in D) \land G (x) \leq A) \land k \in ℕ) \land i \in Z) \land x \in ⋂_{m \in ℤ_{\geq i}} dom F (m)) \land n \in ℤ_{\geq i}) \to i \in Z$
93		simplr	$⊢ ((((((φ \land x \in D) \land G (x) \leq A) \land k \in ℕ) \land i \in Z) \land x \in ⋂_{m \in ℤ_{\geq i}} dom F (m)) \land n \in ℤ_{\geq i}) \to x \in ⋂_{m \in ℤ_{\geq i}} dom F (m)$
94		simpr	$⊢ ((((((φ \land x \in D) \land G (x) \leq A) \land k \in ℕ) \land i \in Z) \land x \in ⋂_{m \in ℤ_{\geq i}} dom F (m)) \land n \in ℤ_{\geq i}) \to n \in ℤ_{\geq i}$
95		nfv	$⊢ Ⅎ m φ$
96	95 30 34	nf3an	$⊢ Ⅎ m (φ \land i \in Z \land x \in ⋂_{m \in ℤ_{\geq i}} dom F (m))$
97		nfv	$⊢ Ⅎ m n \in ℤ_{\geq i}$
98	96 97	nfan	$⊢ Ⅎ m ((φ \land i \in Z \land x \in ⋂_{m \in ℤ_{\geq i}} dom F (m)) \land n \in ℤ_{\geq i})$
99		simpll	$⊢ (((φ \land i \in Z \land x \in ⋂_{m \in ℤ_{\geq i}} dom F (m)) \land n \in ℤ_{\geq i}) \land m \in ℤ_{\geq n}) \to (φ \land i \in Z \land x \in ⋂_{m \in ℤ_{\geq i}} dom F (m))$
100	37	uztrn2	$⊢ (n \in ℤ_{\geq i} \land m \in ℤ_{\geq n}) \to m \in ℤ_{\geq i}$
101	100	adantll	$⊢ (((φ \land i \in Z \land x \in ⋂_{m \in ℤ_{\geq i}} dom F (m)) \land n \in ℤ_{\geq i}) \land m \in ℤ_{\geq n}) \to m \in ℤ_{\geq i}$
102		simpll2	$⊢ (((φ \land i \in Z \land x \in ⋂_{m \in ℤ_{\geq i}} dom F (m)) \land m \in ℤ_{\geq i}) \land (m \in Z ⟼ F (m) (x)) (m) < A + (\frac{1}{k})) \to i \in Z$
103		simplr	$⊢ (((φ \land i \in Z \land x \in ⋂_{m \in ℤ_{\geq i}} dom F (m)) \land m \in ℤ_{\geq i}) \land (m \in Z ⟼ F (m) (x)) (m) < A + (\frac{1}{k})) \to m \in ℤ_{\geq i}$
104	102 103 50	syl2anc	$⊢ (((φ \land i \in Z \land x \in ⋂_{m \in ℤ_{\geq i}} dom F (m)) \land m \in ℤ_{\geq i}) \land (m \in Z ⟼ F (m) (x)) (m) < A + (\frac{1}{k})) \to m \in Z$
105		simpr	$⊢ (((φ \land i \in Z \land x \in ⋂_{m \in ℤ_{\geq i}} dom F (m)) \land m \in ℤ_{\geq i}) \land (m \in Z ⟼ F (m) (x)) (m) < A + (\frac{1}{k})) \to (m \in Z ⟼ F (m) (x)) (m) < A + (\frac{1}{k})$
106		id	$⊢ m \in Z \to m \in Z$
107		fvexd	$⊢ m \in Z \to F (m) (x) \in V$
108		eqid	$⊢ (m \in Z ⟼ F (m) (x)) = (m \in Z ⟼ F (m) (x))$
109	108	fvmpt2	$⊢ (m \in Z \land F (m) (x) \in V) \to (m \in Z ⟼ F (m) (x)) (m) = F (m) (x)$
110	106 107 109	syl2anc	$⊢ m \in Z \to (m \in Z ⟼ F (m) (x)) (m) = F (m) (x)$
111	110	eqcomd	$⊢ m \in Z \to F (m) (x) = (m \in Z ⟼ F (m) (x)) (m)$
112	111	adantr	$⊢ (m \in Z \land (m \in Z ⟼ F (m) (x)) (m) < A + (\frac{1}{k})) \to F (m) (x) = (m \in Z ⟼ F (m) (x)) (m)$
113		simpr	$⊢ (m \in Z \land (m \in Z ⟼ F (m) (x)) (m) < A + (\frac{1}{k})) \to (m \in Z ⟼ F (m) (x)) (m) < A + (\frac{1}{k})$
114	112 113	eqbrtrd	$⊢ (m \in Z \land (m \in Z ⟼ F (m) (x)) (m) < A + (\frac{1}{k})) \to F (m) (x) < A + (\frac{1}{k})$
115	104 105 114	syl2anc	$⊢ (((φ \land i \in Z \land x \in ⋂_{m \in ℤ_{\geq i}} dom F (m)) \land m \in ℤ_{\geq i}) \land (m \in Z ⟼ F (m) (x)) (m) < A + (\frac{1}{k})) \to F (m) (x) < A + (\frac{1}{k})$
116	52	3ad2antl3	$⊢ ((φ \land i \in Z \land x \in ⋂_{m \in ℤ_{\geq i}} dom F (m)) \land m \in ℤ_{\geq i}) \to x \in dom F (m)$
117	116	adantr	$⊢ (((φ \land i \in Z \land x \in ⋂_{m \in ℤ_{\geq i}} dom F (m)) \land m \in ℤ_{\geq i}) \land F (m) (x) < A + (\frac{1}{k})) \to x \in dom F (m)$
118		simpr	$⊢ (((φ \land i \in Z \land x \in ⋂_{m \in ℤ_{\geq i}} dom F (m)) \land m \in ℤ_{\geq i}) \land F (m) (x) < A + (\frac{1}{k})) \to F (m) (x) < A + (\frac{1}{k})$
119	117 118	jca	$⊢ (((φ \land i \in Z \land x \in ⋂_{m \in ℤ_{\geq i}} dom F (m)) \land m \in ℤ_{\geq i}) \land F (m) (x) < A + (\frac{1}{k})) \to (x \in dom F (m) \land F (m) (x) < A + (\frac{1}{k}))$
120		rabid	$⊢ x \in \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\} \leftrightarrow (x \in dom F (m) \land F (m) (x) < A + (\frac{1}{k}))$
121	119 120	sylibr	$⊢ (((φ \land i \in Z \land x \in ⋂_{m \in ℤ_{\geq i}} dom F (m)) \land m \in ℤ_{\geq i}) \land F (m) (x) < A + (\frac{1}{k})) \to x \in \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\}$
122	115 121	syldan	$⊢ (((φ \land i \in Z \land x \in ⋂_{m \in ℤ_{\geq i}} dom F (m)) \land m \in ℤ_{\geq i}) \land (m \in Z ⟼ F (m) (x)) (m) < A + (\frac{1}{k})) \to x \in \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\}$
123	122	adantrl	$⊢ (((φ \land i \in Z \land x \in ⋂_{m \in ℤ_{\geq i}} dom F (m)) \land m \in ℤ_{\geq i}) \land ((m \in Z ⟼ F (m) (x)) (m) \in ℝ \land (m \in Z ⟼ F (m) (x)) (m) < A + (\frac{1}{k}))) \to x \in \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\}$
124	123	ex	$⊢ ((φ \land i \in Z \land x \in ⋂_{m \in ℤ_{\geq i}} dom F (m)) \land m \in ℤ_{\geq i}) \to (((m \in Z ⟼ F (m) (x)) (m) \in ℝ \land (m \in Z ⟼ F (m) (x)) (m) < A + (\frac{1}{k})) \to x \in \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\})$
125	99 101 124	syl2anc	$⊢ (((φ \land i \in Z \land x \in ⋂_{m \in ℤ_{\geq i}} dom F (m)) \land n \in ℤ_{\geq i}) \land m \in ℤ_{\geq n}) \to (((m \in Z ⟼ F (m) (x)) (m) \in ℝ \land (m \in Z ⟼ F (m) (x)) (m) < A + (\frac{1}{k})) \to x \in \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\})$
126	98 125	ralimdaa	$⊢ ((φ \land i \in Z \land x \in ⋂_{m \in ℤ_{\geq i}} dom F (m)) \land n \in ℤ_{\geq i}) \to (\forall m \in ℤ_{\geq n} ((m \in Z ⟼ F (m) (x)) (m) \in ℝ \land (m \in Z ⟼ F (m) (x)) (m) < A + (\frac{1}{k})) \to \forall m \in ℤ_{\geq n} x \in \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\})$
127	90 92 93 94 126	syl31anc	$⊢ ((((((φ \land x \in D) \land G (x) \leq A) \land k \in ℕ) \land i \in Z) \land x \in ⋂_{m \in ℤ_{\geq i}} dom F (m)) \land n \in ℤ_{\geq i}) \to (\forall m \in ℤ_{\geq n} ((m \in Z ⟼ F (m) (x)) (m) \in ℝ \land (m \in Z ⟼ F (m) (x)) (m) < A + (\frac{1}{k})) \to \forall m \in ℤ_{\geq n} x \in \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\})$
128	127	reximdva	$⊢ (((((φ \land x \in D) \land G (x) \leq A) \land k \in ℕ) \land i \in Z) \land x \in ⋂_{m \in ℤ_{\geq i}} dom F (m)) \to (\exists n \in ℤ_{\geq i} \forall m \in ℤ_{\geq n} ((m \in Z ⟼ F (m) (x)) (m) \in ℝ \land (m \in Z ⟼ F (m) (x)) (m) < A + (\frac{1}{k})) \to \exists n \in ℤ_{\geq i} \forall m \in ℤ_{\geq n} x \in \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\})$
129	89 128	mpd	$⊢ (((((φ \land x \in D) \land G (x) \leq A) \land k \in ℕ) \land i \in Z) \land x \in ⋂_{m \in ℤ_{\geq i}} dom F (m)) \to \exists n \in ℤ_{\geq i} \forall m \in ℤ_{\geq n} x \in \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\}$
130		ssrexv	$⊢ ℤ_{\geq i} \subseteq Z \to (\exists n \in ℤ_{\geq i} \forall m \in ℤ_{\geq n} x \in \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\} \to \exists n \in Z \forall m \in ℤ_{\geq n} x \in \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\})$
131	49 130	syl	$⊢ i \in Z \to (\exists n \in ℤ_{\geq i} \forall m \in ℤ_{\geq n} x \in \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\} \to \exists n \in Z \forall m \in ℤ_{\geq n} x \in \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\})$
132	131	ad2antlr	$⊢ (((((φ \land x \in D) \land G (x) \leq A) \land k \in ℕ) \land i \in Z) \land x \in ⋂_{m \in ℤ_{\geq i}} dom F (m)) \to (\exists n \in ℤ_{\geq i} \forall m \in ℤ_{\geq n} x \in \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\} \to \exists n \in Z \forall m \in ℤ_{\geq n} x \in \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\})$
133	129 132	mpd	$⊢ (((((φ \land x \in D) \land G (x) \leq A) \land k \in ℕ) \land i \in Z) \land x \in ⋂_{m \in ℤ_{\geq i}} dom F (m)) \to \exists n \in Z \forall m \in ℤ_{\geq n} x \in \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\}$
134	133	rexlimdva2	$⊢ (((φ \land x \in D) \land G (x) \leq A) \land k \in ℕ) \to (\exists i \in Z x \in ⋂_{m \in ℤ_{\geq i}} dom F (m) \to \exists n \in Z \forall m \in ℤ_{\geq n} x \in \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\})$
135	26 134	mpd	$⊢ (((φ \land x \in D) \land G (x) \leq A) \land k \in ℕ) \to \exists n \in Z \forall m \in ℤ_{\geq n} x \in \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\}$
136		nfv	$⊢ Ⅎ m (φ \land k \in ℕ \land n \in Z)$
137		nfra1	$⊢ Ⅎ m \forall m \in ℤ_{\geq n} x \in \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\}$
138	136 137	nfan	$⊢ Ⅎ m ((φ \land k \in ℕ \land n \in Z) \land \forall m \in ℤ_{\geq n} x \in \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\})$
139		simpll1	$⊢ (((φ \land k \in ℕ \land n \in Z) \land \forall m \in ℤ_{\geq n} x \in \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\}) \land m \in ℤ_{\geq n}) \to φ$
140		simpll2	$⊢ (((φ \land k \in ℕ \land n \in Z) \land \forall m \in ℤ_{\geq n} x \in \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\}) \land m \in ℤ_{\geq n}) \to k \in ℕ$
141	1	uztrn2	$⊢ (n \in Z \land j \in ℤ_{\geq n}) \to j \in Z$
142	141	ssd	$⊢ n \in Z \to ℤ_{\geq n} \subseteq Z$
143	142	sselda	$⊢ (n \in Z \land m \in ℤ_{\geq n}) \to m \in Z$
144	143	adantll	$⊢ ((k \in ℕ \land n \in Z) \land m \in ℤ_{\geq n}) \to m \in Z$
145	144	3adantl1	$⊢ ((φ \land k \in ℕ \land n \in Z) \land m \in ℤ_{\geq n}) \to m \in Z$
146	145	adantlr	$⊢ (((φ \land k \in ℕ \land n \in Z) \land \forall m \in ℤ_{\geq n} x \in \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\}) \land m \in ℤ_{\geq n}) \to m \in Z$
147		rspa	$⊢ (\forall m \in ℤ_{\geq n} x \in \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\} \land m \in ℤ_{\geq n}) \to x \in \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\}$
148	147	adantll	$⊢ (((φ \land k \in ℕ \land n \in Z) \land \forall m \in ℤ_{\geq n} x \in \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\}) \land m \in ℤ_{\geq n}) \to x \in \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\}$
149		simp1	$⊢ (φ \land k \in ℕ \land m \in Z) \to φ$
150		simp3	$⊢ (φ \land k \in ℕ \land m \in Z) \to m \in Z$
151		simp2	$⊢ (φ \land k \in ℕ \land m \in Z) \to k \in ℕ$
152		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)\}$
153	152 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$
154	153	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$
155	154	ralrimivw	$⊢ φ \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$
156	155	3ad2ant1	$⊢ (φ \land k \in ℕ \land m \in Z) \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$
157	7	elrnmpoid	$⊢ (m \in Z \land k \in ℕ \land \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 m P k \in ran P$
158	150 151 156 157	syl3anc	$⊢ (φ \land k \in ℕ \land m \in Z) \to m P k \in ran P$
159		ovex	$⊢ m P k \in V$
160		eleq1	$⊢ r = m P k \to (r \in ran P \leftrightarrow m P k \in ran P)$
161	160	anbi2d	$⊢ r = m P k \to ((φ \land r \in ran P) \leftrightarrow (φ \land m P k \in ran P))$
162		fveq2	$⊢ r = m P k \to C (r) = C (m P k)$
163		id	$⊢ r = m P k \to r = m P k$
164	162 163	eleq12d	$⊢ r = m P k \to (C (r) \in r \leftrightarrow C (m P k) \in (m P k))$
165	161 164	imbi12d	$⊢ r = m P k \to (((φ \land r \in ran P) \to C (r) \in r) \leftrightarrow ((φ \land m P k \in ran P) \to C (m P k) \in (m P k)))$
166	159 165 10	vtocl	$⊢ (φ \land m P k \in ran P) \to C (m P k) \in (m P k)$
167	149 158 166	syl2anc	$⊢ (φ \land k \in ℕ \land m \in Z) \to C (m P k) \in (m P k)$
168		fvexd	$⊢ (φ \land k \in ℕ \land m \in Z) \to C (m P k) \in V$
169	8	ovmpt4g	$⊢ (m \in Z \land k \in ℕ \land C (m P k) \in V) \to m H k = C (m P k)$
170	150 151 168 169	syl3anc	$⊢ (φ \land k \in ℕ \land m \in Z) \to m H k = C (m P k)$
171	170	eqcomd	$⊢ (φ \land k \in ℕ \land m \in Z) \to C (m P k) = m H k$
172	149 153	syl	$⊢ (φ \land k \in ℕ \land m \in Z) \to \{s \in S \| \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\} = s \cap dom F (m)\} \in V$
173	7	ovmpt4g	$⊢ (m \in Z \land k \in ℕ \land \{s \in S \| \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\} = s \cap dom F (m)\} \in V) \to m P k = \{s \in S \| \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\} = s \cap dom F (m)\}$
174	150 151 172 173	syl3anc	$⊢ (φ \land k \in ℕ \land m \in Z) \to m P k = \{s \in S \| \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\} = s \cap dom F (m)\}$
175	171 174	eleq12d	$⊢ (φ \land k \in ℕ \land m \in Z) \to (C (m P k) \in (m P k) \leftrightarrow m H k \in \{s \in S \| \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\} = s \cap dom F (m)\})$
176	167 175	mpbid	$⊢ (φ \land k \in ℕ \land m \in Z) \to m H k \in \{s \in S \| \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\} = s \cap dom F (m)\}$
177		ineq1	$⊢ s = m H k \to s \cap dom F (m) = (m H k) \cap dom F (m)$
178	177	eqeq2d	$⊢ s = m H k \to (\{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\} = s \cap dom F (m) \leftrightarrow \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\} = (m H k) \cap dom F (m))$
179	178	elrab	$⊢ m H k \in \{s \in S \| \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\} = s \cap dom F (m)\} \leftrightarrow (m H k \in S \land \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\} = (m H k) \cap dom F (m))$
180	176 179	sylib	$⊢ (φ \land k \in ℕ \land m \in Z) \to (m H k \in S \land \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\} = (m H k) \cap dom F (m))$
181	180	simprd	$⊢ (φ \land k \in ℕ \land m \in Z) \to \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\} = (m H k) \cap dom F (m)$
182		inss1	$⊢ (m H k) \cap dom F (m) \subseteq m H k$
183	181 182	eqsstrdi	$⊢ (φ \land k \in ℕ \land m \in Z) \to \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\} \subseteq m H k$
184	183	adantr	$⊢ ((φ \land k \in ℕ \land m \in Z) \land x \in \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\}) \to \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\} \subseteq m H k$
185		simpr	$⊢ ((φ \land k \in ℕ \land m \in Z) \land x \in \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\}) \to x \in \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\}$
186	184 185	sseldd	$⊢ ((φ \land k \in ℕ \land m \in Z) \land x \in \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\}) \to x \in (m H k)$
187	139 140 146 148 186	syl31anc	$⊢ (((φ \land k \in ℕ \land n \in Z) \land \forall m \in ℤ_{\geq n} x \in \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\}) \land m \in ℤ_{\geq n}) \to x \in (m H k)$
188	187	ex	$⊢ ((φ \land k \in ℕ \land n \in Z) \land \forall m \in ℤ_{\geq n} x \in \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\}) \to (m \in ℤ_{\geq n} \to x \in (m H k))$
189	138 188	ralrimi	$⊢ ((φ \land k \in ℕ \land n \in Z) \land \forall m \in ℤ_{\geq n} x \in \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\}) \to \forall m \in ℤ_{\geq n} x \in (m H k)$
190		vex	$⊢ x \in V$
191		eliin	$⊢ x \in V \to (x \in ⋂_{m \in ℤ_{\geq n}} (m H k) \leftrightarrow \forall m \in ℤ_{\geq n} x \in (m H k))$
192	190 191	ax-mp	$⊢ x \in ⋂_{m \in ℤ_{\geq n}} (m H k) \leftrightarrow \forall m \in ℤ_{\geq n} x \in (m H k)$
193	189 192	sylibr	$⊢ ((φ \land k \in ℕ \land n \in Z) \land \forall m \in ℤ_{\geq n} x \in \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\}) \to x \in ⋂_{m \in ℤ_{\geq n}} (m H k)$
194	193	ex	$⊢ (φ \land k \in ℕ \land n \in Z) \to (\forall m \in ℤ_{\geq n} x \in \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\} \to x \in ⋂_{m \in ℤ_{\geq n}} (m H k))$
195	194	ad5ant145	$⊢ ((((φ \land x \in D) \land G (x) \leq A) \land k \in ℕ) \land n \in Z) \to (\forall m \in ℤ_{\geq n} x \in \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\} \to x \in ⋂_{m \in ℤ_{\geq n}} (m H k))$
196	195	reximdva	$⊢ (((φ \land x \in D) \land G (x) \leq A) \land k \in ℕ) \to (\exists n \in Z \forall m \in ℤ_{\geq n} x \in \{x \in dom F (m) \| F (m) (x) < A + (\frac{1}{k})\} \to \exists n \in Z x \in ⋂_{m \in ℤ_{\geq n}} (m H k))$
197	135 196	mpd	$⊢ (((φ \land x \in D) \land G (x) \leq A) \land k \in ℕ) \to \exists n \in Z x \in ⋂_{m \in ℤ_{\geq n}} (m H k)$
198		eliun	$⊢ x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} (m H k) \leftrightarrow \exists n \in Z x \in ⋂_{m \in ℤ_{\geq n}} (m H k)$
199	197 198	sylibr	$⊢ (((φ \land x \in D) \land G (x) \leq A) \land k \in ℕ) \to x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} (m H k)$
200	199	ralrimiva	$⊢ ((φ \land x \in D) \land G (x) \leq A) \to \forall k \in ℕ x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} (m H k)$
201		eliin	$⊢ x \in V \to (x \in ⋂_{k \in ℕ} ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} (m H k) \leftrightarrow \forall k \in ℕ x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} (m H k))$
202	190 201	ax-mp	$⊢ x \in ⋂_{k \in ℕ} ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} (m H k) \leftrightarrow \forall k \in ℕ x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} (m H k)$
203	200 202	sylibr	$⊢ ((φ \land x \in D) \land G (x) \leq A) \to x \in ⋂_{k \in ℕ} ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} (m H k)$
204	203 9	eleqtrrdi	$⊢ ((φ \land x \in D) \land G (x) \leq A) \to x \in I$
205	204	ex	$⊢ (φ \land x \in D) \to (G (x) \leq A \to x \in I)$
206	205	ralrimiva	$⊢ φ \to \forall x \in D (G (x) \leq A \to x \in I)$
207		rabss	$⊢ \{x \in D \| G (x) \leq A\} \subseteq I \leftrightarrow \forall x \in D (G (x) \leq A \to x \in I)$
208	206 207	sylibr	$⊢ φ \to \{x \in D \| G (x) \leq A\} \subseteq I$
209	14 208	ssind	$⊢ φ \to \{x \in D \| G (x) \leq A\} \subseteq D \cap I$

Metamath Proof Explorer

Theorem smflimlem2

Proof