smfliminfmpt

Description: The inferior limit of a countable set of sigma-measurable functions is sigma-measurable. Proposition 121F (e) of Fremlin1 p. 39 . A can contain m as a free variable, in other words it can be thought of as an indexed collection A ( m ) . B can be thought of as a collection with two indices B ( m , x ) . (Contributed by Glauco Siliprandi, 2-Jan-2022)

	Ref	Expression
Hypotheses	smfliminfmpt.p	$⊢ Ⅎ m φ$
	smfliminfmpt.x	$⊢ Ⅎ x φ$
	smfliminfmpt.n	$⊢ Ⅎ n φ$
	smfliminfmpt.m	$⊢ φ \to M \in ℤ$
	smfliminfmpt.z	$⊢ Z = ℤ_{\geq M}$
	smfliminfmpt.s	$⊢ φ \to S \in SAlg$
	smfliminfmpt.b	$⊢ (φ \land m \in Z \land x \in A) \to B \in V$
	smfliminfmpt.f	$⊢ (φ \land m \in Z) \to (x \in A ⟼ B) \in SMblFn (S)$
	smfliminfmpt.d	$⊢ D = \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} A \| lim inf ((m \in Z ⟼ B)) \in ℝ\}$
	smfliminfmpt.g	$⊢ G = (x \in D ⟼ lim inf ((m \in Z ⟼ B)))$
Assertion	smfliminfmpt	$⊢ φ \to G \in SMblFn (S)$

Proof

Step	Hyp	Ref	Expression
1		smfliminfmpt.p	$⊢ Ⅎ m φ$
2		smfliminfmpt.x	$⊢ Ⅎ x φ$
3		smfliminfmpt.n	$⊢ Ⅎ n φ$
4		smfliminfmpt.m	$⊢ φ \to M \in ℤ$
5		smfliminfmpt.z	$⊢ Z = ℤ_{\geq M}$
6		smfliminfmpt.s	$⊢ φ \to S \in SAlg$
7		smfliminfmpt.b	$⊢ (φ \land m \in Z \land x \in A) \to B \in V$
8		smfliminfmpt.f	$⊢ (φ \land m \in Z) \to (x \in A ⟼ B) \in SMblFn (S)$
9		smfliminfmpt.d	$⊢ D = \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} A \| lim inf ((m \in Z ⟼ B)) \in ℝ\}$
10		smfliminfmpt.g	$⊢ G = (x \in D ⟼ lim inf ((m \in Z ⟼ B)))$
11	10	a1i	$⊢ φ \to G = (x \in D ⟼ lim inf ((m \in Z ⟼ B)))$
12	9	a1i	$⊢ φ \to D = \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} A \| lim inf ((m \in Z ⟼ B)) \in ℝ\}$
13		simpr	$⊢ (φ \land x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} A) \to x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} A$
14		nfv	$⊢ Ⅎ m n \in Z$
15	1 14	nfan	$⊢ Ⅎ m (φ \land n \in Z)$
16		simpll	$⊢ ((φ \land n \in Z) \land m \in ℤ_{\geq n}) \to φ$
17	5	uztrn2	$⊢ (n \in Z \land m \in ℤ_{\geq n}) \to m \in Z$
18	17	adantll	$⊢ ((φ \land n \in Z) \land m \in ℤ_{\geq n}) \to m \in Z$
19		simpr	$⊢ (φ \land m \in Z) \to m \in Z$
20	8	elexd	$⊢ (φ \land m \in Z) \to (x \in A ⟼ B) \in V$
21		eqid	$⊢ (m \in Z ⟼ (x \in A ⟼ B)) = (m \in Z ⟼ (x \in A ⟼ B))$
22	21	fvmpt2	$⊢ (m \in Z \land (x \in A ⟼ B) \in V) \to (m \in Z ⟼ (x \in A ⟼ B)) (m) = (x \in A ⟼ B)$
23	19 20 22	syl2anc	$⊢ (φ \land m \in Z) \to (m \in Z ⟼ (x \in A ⟼ B)) (m) = (x \in A ⟼ B)$
24	23	dmeqd	$⊢ (φ \land m \in Z) \to dom (m \in Z ⟼ (x \in A ⟼ B)) (m) = dom (x \in A ⟼ B)$
25		nfv	$⊢ Ⅎ x m \in Z$
26	2 25	nfan	$⊢ Ⅎ x (φ \land m \in Z)$
27		eqid	$⊢ (x \in A ⟼ B) = (x \in A ⟼ B)$
28	7	3expa	$⊢ ((φ \land m \in Z) \land x \in A) \to B \in V$
29	26 27 28	dmmptdf	$⊢ (φ \land m \in Z) \to dom (x \in A ⟼ B) = A$
30	24 29	eqtr2d	$⊢ (φ \land m \in Z) \to A = dom (m \in Z ⟼ (x \in A ⟼ B)) (m)$
31	16 18 30	syl2anc	$⊢ ((φ \land n \in Z) \land m \in ℤ_{\geq n}) \to A = dom (m \in Z ⟼ (x \in A ⟼ B)) (m)$
32	15 31	iineq2d	$⊢ (φ \land n \in Z) \to ⋂_{m \in ℤ_{\geq n}} A = ⋂_{m \in ℤ_{\geq n}} dom (m \in Z ⟼ (x \in A ⟼ B)) (m)$
33	3 32	iuneq2df	$⊢ φ \to ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} A = ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom (m \in Z ⟼ (x \in A ⟼ B)) (m)$
34	33	adantr	$⊢ (φ \land x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} A) \to ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} A = ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom (m \in Z ⟼ (x \in A ⟼ B)) (m)$
35	13 34	eleqtrd	$⊢ (φ \land x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} A) \to x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom (m \in Z ⟼ (x \in A ⟼ B)) (m)$
36	35	adantrr	$⊢ (φ \land (x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} A \land lim inf ((m \in Z ⟼ B)) \in ℝ)) \to x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom (m \in Z ⟼ (x \in A ⟼ B)) (m)$
37		eliun	$⊢ x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} A \leftrightarrow \exists n \in Z x \in ⋂_{m \in ℤ_{\geq n}} A$
38	37	biimpi	$⊢ x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} A \to \exists n \in Z x \in ⋂_{m \in ℤ_{\geq n}} A$
39	38	adantl	$⊢ (φ \land x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} A) \to \exists n \in Z x \in ⋂_{m \in ℤ_{\geq n}} A$
40		nfv	$⊢ Ⅎ n lim inf ((m \in Z ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x))) = lim inf ((m \in Z ⟼ B))$
41		nfcv	$⊢ \underline{Ⅎ} m x$
42		nfii1	$⊢ \underline{Ⅎ} m ⋂_{m \in ℤ_{\geq n}} A$
43	41 42	nfel	$⊢ Ⅎ m x \in ⋂_{m \in ℤ_{\geq n}} A$
44	1 14 43	nf3an	$⊢ Ⅎ m (φ \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} A)$
45	23	fveq1d	$⊢ (φ \land m \in Z) \to (m \in Z ⟼ (x \in A ⟼ B)) (m) (x) = (x \in A ⟼ B) (x)$
46	16 18 45	syl2anc	$⊢ ((φ \land n \in Z) \land m \in ℤ_{\geq n}) \to (m \in Z ⟼ (x \in A ⟼ B)) (m) (x) = (x \in A ⟼ B) (x)$
47	46	3adantl3	$⊢ ((φ \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} A) \land m \in ℤ_{\geq n}) \to (m \in Z ⟼ (x \in A ⟼ B)) (m) (x) = (x \in A ⟼ B) (x)$
48		eliinid	$⊢ (x \in ⋂_{m \in ℤ_{\geq n}} A \land m \in ℤ_{\geq n}) \to x \in A$
49	48	3ad2antl3	$⊢ ((φ \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} A) \land m \in ℤ_{\geq n}) \to x \in A$
50		simpl1	$⊢ ((φ \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} A) \land m \in ℤ_{\geq n}) \to φ$
51		simp2	$⊢ (φ \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} A) \to n \in Z$
52	51 17	sylan	$⊢ ((φ \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} A) \land m \in ℤ_{\geq n}) \to m \in Z$
53	50 52 49 7	syl3anc	$⊢ ((φ \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} A) \land m \in ℤ_{\geq n}) \to B \in V$
54	27	fvmpt2	$⊢ (x \in A \land B \in V) \to (x \in A ⟼ B) (x) = B$
55	49 53 54	syl2anc	$⊢ ((φ \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} A) \land m \in ℤ_{\geq n}) \to (x \in A ⟼ B) (x) = B$
56	47 55	eqtrd	$⊢ ((φ \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} A) \land m \in ℤ_{\geq n}) \to (m \in Z ⟼ (x \in A ⟼ B)) (m) (x) = B$
57	44 56	mpteq2da	$⊢ (φ \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} A) \to (m \in ℤ_{\geq n} ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x)) = (m \in ℤ_{\geq n} ⟼ B)$
58	57	fveq2d	$⊢ (φ \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} A) \to lim inf ((m \in ℤ_{\geq n} ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x))) = lim inf ((m \in ℤ_{\geq n} ⟼ B))$
59		nfcv	$⊢ \underline{Ⅎ} m Z$
60		nfcv	$⊢ \underline{Ⅎ} m ℤ_{\geq n}$
61		eqid	$⊢ ℤ_{\geq n} = ℤ_{\geq n}$
62	5	eluzelz2	$⊢ n \in Z \to n \in ℤ$
63	62	uzidd	$⊢ n \in Z \to n \in ℤ_{\geq n}$
64	63	3ad2ant2	$⊢ (φ \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} A) \to n \in ℤ_{\geq n}$
65		fvexd	$⊢ ((φ \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} A) \land m \in ℤ_{\geq n}) \to (m \in Z ⟼ (x \in A ⟼ B)) (m) (x) \in V$
66	44 59 60 5 61 51 64 65	liminfequzmpt2	$⊢ (φ \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} A) \to lim inf ((m \in Z ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x))) = lim inf ((m \in ℤ_{\geq n} ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x)))$
67	44 59 60 5 61 51 64 53	liminfequzmpt2	$⊢ (φ \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} A) \to lim inf ((m \in Z ⟼ B)) = lim inf ((m \in ℤ_{\geq n} ⟼ B))$
68	58 66 67	3eqtr4d	$⊢ (φ \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} A) \to lim inf ((m \in Z ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x))) = lim inf ((m \in Z ⟼ B))$
69	68	3exp	$⊢ φ \to (n \in Z \to (x \in ⋂_{m \in ℤ_{\geq n}} A \to lim inf ((m \in Z ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x))) = lim inf ((m \in Z ⟼ B))))$
70	3 40 69	rexlimd	$⊢ φ \to (\exists n \in Z x \in ⋂_{m \in ℤ_{\geq n}} A \to lim inf ((m \in Z ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x))) = lim inf ((m \in Z ⟼ B)))$
71	70	adantr	$⊢ (φ \land x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} A) \to (\exists n \in Z x \in ⋂_{m \in ℤ_{\geq n}} A \to lim inf ((m \in Z ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x))) = lim inf ((m \in Z ⟼ B)))$
72	39 71	mpd	$⊢ (φ \land x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} A) \to lim inf ((m \in Z ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x))) = lim inf ((m \in Z ⟼ B))$
73	72	adantrr	$⊢ (φ \land (x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} A \land lim inf ((m \in Z ⟼ B)) \in ℝ)) \to lim inf ((m \in Z ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x))) = lim inf ((m \in Z ⟼ B))$
74		simprr	$⊢ (φ \land (x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} A \land lim inf ((m \in Z ⟼ B)) \in ℝ)) \to lim inf ((m \in Z ⟼ B)) \in ℝ$
75	73 74	eqeltrd	$⊢ (φ \land (x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} A \land lim inf ((m \in Z ⟼ B)) \in ℝ)) \to lim inf ((m \in Z ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x))) \in ℝ$
76	36 75	jca	$⊢ (φ \land (x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} A \land lim inf ((m \in Z ⟼ B)) \in ℝ)) \to (x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom (m \in Z ⟼ (x \in A ⟼ B)) (m) \land lim inf ((m \in Z ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x))) \in ℝ)$
77		simpl	$⊢ (φ \land (x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom (m \in Z ⟼ (x \in A ⟼ B)) (m) \land lim inf ((m \in Z ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x))) \in ℝ)) \to φ$
78		simpr	$⊢ (φ \land x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom (m \in Z ⟼ (x \in A ⟼ B)) (m)) \to x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom (m \in Z ⟼ (x \in A ⟼ B)) (m)$
79	33	eqcomd	$⊢ φ \to ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom (m \in Z ⟼ (x \in A ⟼ B)) (m) = ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} A$
80	79	adantr	$⊢ (φ \land x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom (m \in Z ⟼ (x \in A ⟼ B)) (m)) \to ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom (m \in Z ⟼ (x \in A ⟼ B)) (m) = ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} A$
81	78 80	eleqtrd	$⊢ (φ \land x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom (m \in Z ⟼ (x \in A ⟼ B)) (m)) \to x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} A$
82	81	adantrr	$⊢ (φ \land (x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom (m \in Z ⟼ (x \in A ⟼ B)) (m) \land lim inf ((m \in Z ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x))) \in ℝ)) \to x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} A$
83		simprr	$⊢ (φ \land (x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom (m \in Z ⟼ (x \in A ⟼ B)) (m) \land lim inf ((m \in Z ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x))) \in ℝ)) \to lim inf ((m \in Z ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x))) \in ℝ$
84		simp2	$⊢ (φ \land x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} A \land lim inf ((m \in Z ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x))) \in ℝ) \to x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} A$
85	72	eqcomd	$⊢ (φ \land x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} A) \to lim inf ((m \in Z ⟼ B)) = lim inf ((m \in Z ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x)))$
86	85	3adant3	$⊢ (φ \land x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} A \land lim inf ((m \in Z ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x))) \in ℝ) \to lim inf ((m \in Z ⟼ B)) = lim inf ((m \in Z ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x)))$
87		simp3	$⊢ (φ \land x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} A \land lim inf ((m \in Z ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x))) \in ℝ) \to lim inf ((m \in Z ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x))) \in ℝ$
88	86 87	eqeltrd	$⊢ (φ \land x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} A \land lim inf ((m \in Z ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x))) \in ℝ) \to lim inf ((m \in Z ⟼ B)) \in ℝ$
89	84 88	jca	$⊢ (φ \land x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} A \land lim inf ((m \in Z ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x))) \in ℝ) \to (x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} A \land lim inf ((m \in Z ⟼ B)) \in ℝ)$
90	77 82 83 89	syl3anc	$⊢ (φ \land (x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom (m \in Z ⟼ (x \in A ⟼ B)) (m) \land lim inf ((m \in Z ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x))) \in ℝ)) \to (x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} A \land lim inf ((m \in Z ⟼ B)) \in ℝ)$
91	76 90	impbida	$⊢ φ \to ((x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} A \land lim inf ((m \in Z ⟼ B)) \in ℝ) \leftrightarrow (x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom (m \in Z ⟼ (x \in A ⟼ B)) (m) \land lim inf ((m \in Z ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x))) \in ℝ))$
92	2 91	rabbida3	$⊢ φ \to \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} A \| lim inf ((m \in Z ⟼ B)) \in ℝ\} = \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom (m \in Z ⟼ (x \in A ⟼ B)) (m) \| lim inf ((m \in Z ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x))) \in ℝ\}$
93	12 92	eqtrd	$⊢ φ \to D = \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom (m \in Z ⟼ (x \in A ⟼ B)) (m) \| lim inf ((m \in Z ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x))) \in ℝ\}$
94	9	eleq2i	$⊢ x \in D \leftrightarrow x \in \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} A \| lim inf ((m \in Z ⟼ B)) \in ℝ\}$
95	94	biimpi	$⊢ x \in D \to x \in \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} A \| lim inf ((m \in Z ⟼ B)) \in ℝ\}$
96		rabidim1	$⊢ x \in \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} A \| lim inf ((m \in Z ⟼ B)) \in ℝ\} \to x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} A$
97	95 96	syl	$⊢ x \in D \to x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} A$
98	97 85	sylan2	$⊢ (φ \land x \in D) \to lim inf ((m \in Z ⟼ B)) = lim inf ((m \in Z ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x)))$
99	2 93 98	mpteq12da	$⊢ φ \to (x \in D ⟼ lim inf ((m \in Z ⟼ B))) = (x \in \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom (m \in Z ⟼ (x \in A ⟼ B)) (m) \| lim inf ((m \in Z ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x))) \in ℝ\} ⟼ lim inf ((m \in Z ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x))))$
100	11 99	eqtrd	$⊢ φ \to G = (x \in \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom (m \in Z ⟼ (x \in A ⟼ B)) (m) \| lim inf ((m \in Z ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x))) \in ℝ\} ⟼ lim inf ((m \in Z ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x))))$
101		nfmpt1	$⊢ \underline{Ⅎ} m (m \in Z ⟼ (x \in A ⟼ B))$
102		nfcv	$⊢ \underline{Ⅎ} x Z$
103		nfmpt1	$⊢ \underline{Ⅎ} x (x \in A ⟼ B)$
104	102 103	nfmpt	$⊢ \underline{Ⅎ} x (m \in Z ⟼ (x \in A ⟼ B))$
105	1 8	fmptd2f	$⊢ φ \to (m \in Z ⟼ (x \in A ⟼ B)) : Z ⟶ SMblFn (S)$
106		eqid	$⊢ \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom (m \in Z ⟼ (x \in A ⟼ B)) (m) \| lim inf ((m \in Z ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x))) \in ℝ\} = \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom (m \in Z ⟼ (x \in A ⟼ B)) (m) \| lim inf ((m \in Z ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x))) \in ℝ\}$
107		eqid	$⊢ (x \in \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom (m \in Z ⟼ (x \in A ⟼ B)) (m) \| lim inf ((m \in Z ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x))) \in ℝ\} ⟼ lim inf ((m \in Z ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x)))) = (x \in \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom (m \in Z ⟼ (x \in A ⟼ B)) (m) \| lim inf ((m \in Z ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x))) \in ℝ\} ⟼ lim inf ((m \in Z ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x))))$
108	101 104 4 5 6 105 106 107	smfliminf	$⊢ φ \to (x \in \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom (m \in Z ⟼ (x \in A ⟼ B)) (m) \| lim inf ((m \in Z ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x))) \in ℝ\} ⟼ lim inf ((m \in Z ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x)))) \in SMblFn (S)$
109	100 108	eqeltrd	$⊢ φ \to G \in SMblFn (S)$

Metamath Proof Explorer

Theorem smfliminfmpt

Proof