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	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 sup ((m \in Z ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x))) = lim sup ((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	18	3adantl3	$⊢ ((φ \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} A) \land m \in ℤ_{\geq n}) \to m \in Z$
52	50 51 49 7	syl3anc	$⊢ ((φ \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} A) \land m \in ℤ_{\geq n}) \to B \in W$
53	27	fvmpt2	$⊢ (x \in A \land B \in W) \to (x \in A ⟼ B) (x) = B$
54	49 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	47 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	44 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 sup ((m \in ℤ_{\geq n} ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x))) = lim sup ((m \in ℤ_{\geq n} ⟼ B))$
58	4	3ad2ant1	$⊢ (φ \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} A) \to M \in ℤ$
59	5	eluzelz2	$⊢ n \in Z \to n \in ℤ$
60	59	3ad2ant2	$⊢ (φ \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} A) \to n \in ℤ$
61		eqid	$⊢ ℤ_{\geq n} = ℤ_{\geq n}$
62		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$
63	51 62	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$
64	44 58 60 5 61 62 63	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)))$
65	14	nfci	$⊢ \underline{Ⅎ} m Z$
66		nfcv	$⊢ \underline{Ⅎ} m ℤ_{\geq n}$
67		simp2	$⊢ (φ \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} A) \to n \in Z$
68	60	uzidd	$⊢ (φ \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} A) \to n \in ℤ_{\geq n}$
69	44 65 66 5 61 67 68 52	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))$
70	57 64 69	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))$
71	70	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))))$
72	3 40 71	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)))$
73	72	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)))$
74	39 73	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))$
75	74	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))$
76		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 ℝ$
77	75 76	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 ℝ$
78	36 77	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 ℝ)$
79	78	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 ℝ))$
80		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 φ$
81		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)$
82	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$
83	82	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$
84	81 83	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$
85	84	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$
86		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 ℝ$
87		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$
88	74	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)))$
89	88	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)))$
90		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 ℝ$
91	89 90	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 ℝ$
92	87 91	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 ℝ)$
93	80 85 86 92	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 ℝ)$
94	93	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 ℝ))$
95	79 94	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 ℝ))$
96	2 95	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 ℝ\}$
97	12 96	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 ℝ\}$
98	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 ℝ\}$
99	98	biimpi	$⊢ x \in D \to x \in \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} A \| lim sup ((m \in Z ⟼ B)) \in ℝ\}$
100		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$
101	99 100	syl	$⊢ x \in D \to x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} A$
102	101 88	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)))$
103	2 97 102	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))))$
104	11 103	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))))$
105		nfmpt1	$⊢ \underline{Ⅎ} m (m \in Z ⟼ (x \in A ⟼ B))$
106		nfcv	$⊢ \underline{Ⅎ} x Z$
107		nfmpt1	$⊢ \underline{Ⅎ} x (x \in A ⟼ B)$
108	106 107	nfmpt	$⊢ \underline{Ⅎ} x (m \in Z ⟼ (x \in A ⟼ B))$
109	1 8	fmptd2f	$⊢ φ \to (m \in Z ⟼ (x \in A ⟼ B)) : Z ⟶ SMblFn (S)$
110		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 ℝ\}$
111		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))))$
112	105 108 4 5 6 109 110 111	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)$
113	104 112	eqeltrd	$⊢ φ \to G \in SMblFn (S)$

Metamath Proof Explorer

Theorem smflimsupmpt

Proof