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	bilani	$⊢ (φ \land x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} A) \to \exists n \in Z x \in ⋂_{m \in ℤ_{\geq n}} A$
39		nfv	$⊢ Ⅎ n lim inf ((m \in Z ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x))) = lim inf ((m \in Z ⟼ B))$
40		nfcv	$⊢ \underline{Ⅎ} m x$
41		nfii1	$⊢ \underline{Ⅎ} m ⋂_{m \in ℤ_{\geq n}} A$
42	40 41	nfel	$⊢ Ⅎ m x \in ⋂_{m \in ℤ_{\geq n}} A$
43	1 14 42	nf3an	$⊢ Ⅎ m (φ \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} A)$
44	23	fveq1d	$⊢ (φ \land m \in Z) \to (m \in Z ⟼ (x \in A ⟼ B)) (m) (x) = (x \in A ⟼ B) (x)$
45	16 18 44	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)$
46	45	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)$
47		eliinid	$⊢ (x \in ⋂_{m \in ℤ_{\geq n}} A \land m \in ℤ_{\geq n}) \to x \in A$
48	47	3ad2antl3	$⊢ ((φ \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} A) \land m \in ℤ_{\geq n}) \to x \in A$
49		simpl1	$⊢ ((φ \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} A) \land m \in ℤ_{\geq n}) \to φ$
50		simp2	$⊢ (φ \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} A) \to n \in Z$
51	50 17	sylan	$⊢ ((φ \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} A) \land m \in ℤ_{\geq n}) \to m \in Z$
52	49 51 48 7	syl3anc	$⊢ ((φ \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} A) \land m \in ℤ_{\geq n}) \to B \in V$
53	27	fvmpt2	$⊢ (x \in A \land B \in V) \to (x \in A ⟼ B) (x) = B$
54	48 52 53	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$
55	46 54	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$
56	43 55	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)$
57	56	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))$
58		nfcv	$⊢ \underline{Ⅎ} m Z$
59		nfcv	$⊢ \underline{Ⅎ} m ℤ_{\geq n}$
60		eqid	$⊢ ℤ_{\geq n} = ℤ_{\geq n}$
61	5	eluzelz2	$⊢ n \in Z \to n \in ℤ$
62	61	uzidd	$⊢ n \in Z \to n \in ℤ_{\geq n}$
63	62	3ad2ant2	$⊢ (φ \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} A) \to n \in ℤ_{\geq n}$
64		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$
65	43 58 59 5 60 50 63 64	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)))$
66	43 58 59 5 60 50 63 52	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))$
67	57 65 66	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))$
68	67	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))))$
69	3 39 68	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)))$
70	69	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)))$
71	38 70	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))$
72	71	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))$
73		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 ℝ$
74	72 73	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 ℝ$
75	36 74	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 ℝ)$
76		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 φ$
77		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)$
78	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$
79	78	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$
80	77 79	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$
81	80	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$
82		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 ℝ$
83		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$
84	71	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)))$
85	84	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)))$
86		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 ℝ$
87	85 86	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 ℝ$
88	83 87	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 ℝ)$
89	76 81 82 88	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 ℝ)$
90	75 89	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 ℝ))$
91	2 90	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 ℝ\}$
92	12 91	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 ℝ\}$
93	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 ℝ\}$
94	93	biimpi	$⊢ x \in D \to x \in \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} A \| lim inf ((m \in Z ⟼ B)) \in ℝ\}$
95		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$
96	94 95	syl	$⊢ x \in D \to x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} A$
97	96 84	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)))$
98	2 92 97	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))))$
99	11 98	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))))$
100		nfmpt1	$⊢ \underline{Ⅎ} m (m \in Z ⟼ (x \in A ⟼ B))$
101		nfcv	$⊢ \underline{Ⅎ} x Z$
102		nfmpt1	$⊢ \underline{Ⅎ} x (x \in A ⟼ B)$
103	101 102	nfmpt	$⊢ \underline{Ⅎ} x (m \in Z ⟼ (x \in A ⟼ B))$
104	1 8	fmptd2f	$⊢ φ \to (m \in Z ⟼ (x \in A ⟼ B)) : Z ⟶ SMblFn (S)$
105		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 ℝ\}$
106		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))))$
107	100 103 4 5 6 104 105 106	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)$
108	99 107	eqeltrd	$⊢ φ \to G \in SMblFn (S)$

Metamath Proof Explorer

Theorem smfliminfmpt

Proof