smflimsupmpt

Description: The superior limit of a sequence of sigma-measurable functions is sigma-measurable. Proposition 121F (d) 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, 23-Oct-2021)

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

Proof

Step	Hyp	Ref	Expression
1		smflimsupmpt.p	$⊢ Ⅎ m φ$
2		smflimsupmpt.x	$⊢ Ⅎ x φ$
3		smflimsupmpt.n	$⊢ Ⅎ n φ$
4		smflimsupmpt.m	$⊢ φ \to M \in ℤ$
5		smflimsupmpt.z	$⊢ Z = ℤ_{\geq M}$
6		smflimsupmpt.s	$⊢ φ \to S \in SAlg$
7		smflimsupmpt.b	$⊢ (φ \land m \in Z \land x \in A) \to B \in W$
8		smflimsupmpt.f	$⊢ (φ \land m \in Z) \to (x \in A ⟼ B) \in SMblFn (S)$
9		smflimsupmpt.d	$⊢ D = \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} A \| lim sup ((m \in Z ⟼ B)) \in ℝ\}$
10		smflimsupmpt.g	$⊢ G = (x \in D ⟼ lim sup ((m \in Z ⟼ B)))$
11	10	a1i	$⊢ φ \to G = (x \in D ⟼ lim sup ((m \in Z ⟼ B)))$
12	9	a1i	$⊢ φ \to D = \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} A \| lim sup ((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 W$
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 sup ((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 sup ((m \in Z ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x))) = lim sup ((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	18	3adantl3	$⊢ ((φ \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} A) \land m \in ℤ_{\geq n}) \to m \in Z$
51	49 50 48 7	syl3anc	$⊢ ((φ \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} A) \land m \in ℤ_{\geq n}) \to B \in W$
52	27	fvmpt2	$⊢ (x \in A \land B \in W) \to (x \in A ⟼ B) (x) = B$
53	48 51 52	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$
54	46 53	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$
55	43 54	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)$
56	55	fveq2d	$⊢ (φ \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} A) \to lim sup ((m \in ℤ_{\geq n} ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x))) = lim sup ((m \in ℤ_{\geq n} ⟼ B))$
57	4	3ad2ant1	$⊢ (φ \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} A) \to M \in ℤ$
58	5	eluzelz2	$⊢ n \in Z \to n \in ℤ$
59	58	3ad2ant2	$⊢ (φ \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} A) \to n \in ℤ$
60		eqid	$⊢ ℤ_{\geq n} = ℤ_{\geq n}$
61		fvexd	$⊢ ((φ \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} A) \land m \in Z) \to (m \in Z ⟼ (x \in A ⟼ B)) (m) (x) \in V$
62	50 61	syldan	$⊢ ((φ \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$
63	43 57 59 5 60 61 62	limsupequzmpt	$⊢ (φ \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} A) \to lim sup ((m \in Z ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x))) = lim sup ((m \in ℤ_{\geq n} ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x)))$
64	14	nfci	$⊢ \underline{Ⅎ} m Z$
65		nfcv	$⊢ \underline{Ⅎ} m ℤ_{\geq n}$
66		simp2	$⊢ (φ \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} A) \to n \in Z$
67	59	uzidd	$⊢ (φ \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} A) \to n \in ℤ_{\geq n}$
68	43 64 65 5 60 66 67 51	limsupequzmpt2	$⊢ (φ \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} A) \to lim sup ((m \in Z ⟼ B)) = lim sup ((m \in ℤ_{\geq n} ⟼ B))$
69	56 63 68	3eqtr4d	$⊢ (φ \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} A) \to lim sup ((m \in Z ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x))) = lim sup ((m \in Z ⟼ B))$
70	69	3exp	$⊢ φ \to (n \in Z \to (x \in ⋂_{m \in ℤ_{\geq n}} A \to lim sup ((m \in Z ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x))) = lim sup ((m \in Z ⟼ B))))$
71	3 39 70	rexlimd	$⊢ φ \to (\exists n \in Z x \in ⋂_{m \in ℤ_{\geq n}} A \to lim sup ((m \in Z ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x))) = lim sup ((m \in Z ⟼ B)))$
72	71	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 sup ((m \in Z ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x))) = lim sup ((m \in Z ⟼ B)))$
73	38 72	mpd	$⊢ (φ \land x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} A) \to lim sup ((m \in Z ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x))) = lim sup ((m \in Z ⟼ B))$
74	73	adantrr	$⊢ (φ \land (x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} A \land lim sup ((m \in Z ⟼ B)) \in ℝ)) \to lim sup ((m \in Z ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x))) = lim sup ((m \in Z ⟼ B))$
75		simprr	$⊢ (φ \land (x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} A \land lim sup ((m \in Z ⟼ B)) \in ℝ)) \to lim sup ((m \in Z ⟼ B)) \in ℝ$
76	74 75	eqeltrd	$⊢ (φ \land (x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} A \land lim sup ((m \in Z ⟼ B)) \in ℝ)) \to lim sup ((m \in Z ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x))) \in ℝ$
77	36 76	jca	$⊢ (φ \land (x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} A \land lim sup ((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 sup ((m \in Z ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x))) \in ℝ)$
78	77	ex	$⊢ φ \to ((x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} A \land lim sup ((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 sup ((m \in Z ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x))) \in ℝ))$
79		simpl	$⊢ (φ \land (x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom (m \in Z ⟼ (x \in A ⟼ B)) (m) \land lim sup ((m \in Z ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x))) \in ℝ)) \to φ$
80		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)$
81	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$
82	81	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$
83	80 82	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$
84	83	adantrr	$⊢ (φ \land (x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom (m \in Z ⟼ (x \in A ⟼ B)) (m) \land lim sup ((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		simprr	$⊢ (φ \land (x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom (m \in Z ⟼ (x \in A ⟼ B)) (m) \land lim sup ((m \in Z ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x))) \in ℝ)) \to lim sup ((m \in Z ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x))) \in ℝ$
86		simp2	$⊢ (φ \land x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} A \land lim sup ((m \in Z ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x))) \in ℝ) \to x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} A$
87	73	eqcomd	$⊢ (φ \land x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} A) \to lim sup ((m \in Z ⟼ B)) = lim sup ((m \in Z ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x)))$
88	87	3adant3	$⊢ (φ \land x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} A \land lim sup ((m \in Z ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x))) \in ℝ) \to lim sup ((m \in Z ⟼ B)) = lim sup ((m \in Z ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x)))$
89		simp3	$⊢ (φ \land x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} A \land lim sup ((m \in Z ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x))) \in ℝ) \to lim sup ((m \in Z ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x))) \in ℝ$
90	88 89	eqeltrd	$⊢ (φ \land x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} A \land lim sup ((m \in Z ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x))) \in ℝ) \to lim sup ((m \in Z ⟼ B)) \in ℝ$
91	86 90	jca	$⊢ (φ \land x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} A \land lim sup ((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 sup ((m \in Z ⟼ B)) \in ℝ)$
92	79 84 85 91	syl3anc	$⊢ (φ \land (x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom (m \in Z ⟼ (x \in A ⟼ B)) (m) \land lim sup ((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 sup ((m \in Z ⟼ B)) \in ℝ)$
93	92	ex	$⊢ φ \to ((x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom (m \in Z ⟼ (x \in A ⟼ B)) (m) \land lim sup ((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 sup ((m \in Z ⟼ B)) \in ℝ))$
94	78 93	impbid	$⊢ φ \to ((x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} A \land lim sup ((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 sup ((m \in Z ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x))) \in ℝ))$
95	2 94	rabbida3	$⊢ φ \to \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} A \| lim sup ((m \in Z ⟼ B)) \in ℝ\} = \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom (m \in Z ⟼ (x \in A ⟼ B)) (m) \| lim sup ((m \in Z ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x))) \in ℝ\}$
96	12 95	eqtrd	$⊢ φ \to D = \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom (m \in Z ⟼ (x \in A ⟼ B)) (m) \| lim sup ((m \in Z ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x))) \in ℝ\}$
97	9	eleq2i	$⊢ x \in D \leftrightarrow x \in \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} A \| lim sup ((m \in Z ⟼ B)) \in ℝ\}$
98	97	biimpi	$⊢ x \in D \to x \in \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} A \| lim sup ((m \in Z ⟼ B)) \in ℝ\}$
99		rabidim1	$⊢ x \in \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} A \| lim sup ((m \in Z ⟼ B)) \in ℝ\} \to x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} A$
100	98 99	syl	$⊢ x \in D \to x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} A$
101	100 87	sylan2	$⊢ (φ \land x \in D) \to lim sup ((m \in Z ⟼ B)) = lim sup ((m \in Z ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x)))$
102	2 96 101	mpteq12da	$⊢ φ \to (x \in D ⟼ lim sup ((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 sup ((m \in Z ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x))) \in ℝ\} ⟼ lim sup ((m \in Z ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x))))$
103	11 102	eqtrd	$⊢ φ \to G = (x \in \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom (m \in Z ⟼ (x \in A ⟼ B)) (m) \| lim sup ((m \in Z ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x))) \in ℝ\} ⟼ lim sup ((m \in Z ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x))))$
104		nfmpt1	$⊢ \underline{Ⅎ} m (m \in Z ⟼ (x \in A ⟼ B))$
105		nfcv	$⊢ \underline{Ⅎ} x Z$
106		nfmpt1	$⊢ \underline{Ⅎ} x (x \in A ⟼ B)$
107	105 106	nfmpt	$⊢ \underline{Ⅎ} x (m \in Z ⟼ (x \in A ⟼ B))$
108	1 8	fmptd2f	$⊢ φ \to (m \in Z ⟼ (x \in A ⟼ B)) : Z ⟶ SMblFn (S)$
109		eqid	$⊢ \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom (m \in Z ⟼ (x \in A ⟼ B)) (m) \| lim sup ((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 sup ((m \in Z ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x))) \in ℝ\}$
110		eqid	$⊢ (x \in \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom (m \in Z ⟼ (x \in A ⟼ B)) (m) \| lim sup ((m \in Z ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x))) \in ℝ\} ⟼ lim sup ((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 sup ((m \in Z ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x))) \in ℝ\} ⟼ lim sup ((m \in Z ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x))))$
111	104 107 4 5 6 108 109 110	smflimsup	$⊢ φ \to (x \in \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom (m \in Z ⟼ (x \in A ⟼ B)) (m) \| lim sup ((m \in Z ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x))) \in ℝ\} ⟼ lim sup ((m \in Z ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x)))) \in SMblFn (S)$
112	103 111	eqeltrd	$⊢ φ \to G \in SMblFn (S)$

Metamath Proof Explorer

Theorem smflimsupmpt

Proof