smflimsuplem7

Description: The superior limit of a sequence of sigma-measurable functions is sigma-measurable. Proposition 121F (d) of Fremlin1 p. 39 . (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	smflimsuplem7.m	$⊢ φ \to M \in ℤ$
	smflimsuplem7.z	$⊢ Z = ℤ_{\geq M}$
	smflimsuplem7.s	$⊢ φ \to S \in SAlg$
	smflimsuplem7.f	$⊢ φ \to F : Z ⟶ SMblFn (S)$
	smflimsuplem7.d	$⊢ D = \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| lim sup ((m \in Z ⟼ F (m) (x))) \in ℝ\}$
	smflimsuplem7.e	$⊢ E = (k \in Z ⟼ \{x \in ⋂_{m \in ℤ_{\geq k}} dom F (m) \| sup (ran (m \in ℤ_{\geq k} ⟼ F (m) (x)) ℝ^{*} <) \in ℝ\})$
	smflimsuplem7.h	$⊢ H = (k \in Z ⟼ (x \in E (k) ⟼ sup (ran (m \in ℤ_{\geq k} ⟼ F (m) (x)) ℝ^{*} <)))$
Assertion	smflimsuplem7	$⊢ φ \to D = \{x \in ⋃_{n \in Z} ⋂_{k \in ℤ_{\geq n}} dom H (k) \| (k \in Z ⟼ H (k) (x)) \in dom ⇝\}$

Proof

Step	Hyp	Ref	Expression
1		smflimsuplem7.m	$⊢ φ \to M \in ℤ$
2		smflimsuplem7.z	$⊢ Z = ℤ_{\geq M}$
3		smflimsuplem7.s	$⊢ φ \to S \in SAlg$
4		smflimsuplem7.f	$⊢ φ \to F : Z ⟶ SMblFn (S)$
5		smflimsuplem7.d	$⊢ D = \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| lim sup ((m \in Z ⟼ F (m) (x))) \in ℝ\}$
6		smflimsuplem7.e	$⊢ E = (k \in Z ⟼ \{x \in ⋂_{m \in ℤ_{\geq k}} dom F (m) \| sup (ran (m \in ℤ_{\geq k} ⟼ F (m) (x)) ℝ^{*} <) \in ℝ\})$
7		smflimsuplem7.h	$⊢ H = (k \in Z ⟼ (x \in E (k) ⟼ sup (ran (m \in ℤ_{\geq k} ⟼ F (m) (x)) ℝ^{*} <)))$
8	5	a1i	$⊢ φ \to D = \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| lim sup ((m \in Z ⟼ F (m) (x))) \in ℝ\}$
9		simpl	$⊢ (φ \land x \in \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| lim sup ((m \in Z ⟼ F (m) (x))) \in ℝ\}) \to φ$
10		rabidim2	$⊢ x \in \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| lim sup ((m \in Z ⟼ F (m) (x))) \in ℝ\} \to lim sup ((m \in Z ⟼ F (m) (x))) \in ℝ$
11	10	adantl	$⊢ (φ \land x \in \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| lim sup ((m \in Z ⟼ F (m) (x))) \in ℝ\}) \to lim sup ((m \in Z ⟼ F (m) (x))) \in ℝ$
12		rabidim1	$⊢ x \in \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| lim sup ((m \in Z ⟼ F (m) (x))) \in ℝ\} \to x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m)$
13		eliun	$⊢ x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \leftrightarrow \exists n \in Z x \in ⋂_{m \in ℤ_{\geq n}} dom F (m)$
14	12 13	sylib	$⊢ x \in \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| lim sup ((m \in Z ⟼ F (m) (x))) \in ℝ\} \to \exists n \in Z x \in ⋂_{m \in ℤ_{\geq n}} dom F (m)$
15	14	adantl	$⊢ (φ \land x \in \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| lim sup ((m \in Z ⟼ F (m) (x))) \in ℝ\}) \to \exists n \in Z x \in ⋂_{m \in ℤ_{\geq n}} dom F (m)$
16		nfv	$⊢ Ⅎ n (φ \land lim sup ((m \in Z ⟼ F (m) (x))) \in ℝ)$
17		nfv	$⊢ Ⅎ m φ$
18		nfcv	$⊢ \underline{Ⅎ} m lim sup$
19		nfmpt1	$⊢ \underline{Ⅎ} m (m \in Z ⟼ F (m) (x))$
20	18 19	nffv	$⊢ \underline{Ⅎ} m lim sup ((m \in Z ⟼ F (m) (x)))$
21		nfcv	$⊢ \underline{Ⅎ} m ℝ$
22	20 21	nfel	$⊢ Ⅎ m lim sup ((m \in Z ⟼ F (m) (x))) \in ℝ$
23	17 22	nfan	$⊢ Ⅎ m (φ \land lim sup ((m \in Z ⟼ F (m) (x))) \in ℝ)$
24		nfv	$⊢ Ⅎ m n \in Z$
25		nfcv	$⊢ \underline{Ⅎ} m x$
26		nfii1	$⊢ \underline{Ⅎ} m ⋂_{m \in ℤ_{\geq n}} dom F (m)$
27	25 26	nfel	$⊢ Ⅎ m x \in ⋂_{m \in ℤ_{\geq n}} dom F (m)$
28	23 24 27	nf3an	$⊢ Ⅎ m ((φ \land lim sup ((m \in Z ⟼ F (m) (x))) \in ℝ) \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} dom F (m))$
29		nfv	$⊢ Ⅎ m k \in ℤ_{\geq n}$
30	28 29	nfan	$⊢ Ⅎ m (((φ \land lim sup ((m \in Z ⟼ F (m) (x))) \in ℝ) \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} dom F (m)) \land k \in ℤ_{\geq n})$
31		simpl1l	$⊢ (((φ \land lim sup ((m \in Z ⟼ F (m) (x))) \in ℝ) \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} dom F (m)) \land k \in ℤ_{\geq n}) \to φ$
32	31 1	syl	$⊢ (((φ \land lim sup ((m \in Z ⟼ F (m) (x))) \in ℝ) \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} dom F (m)) \land k \in ℤ_{\geq n}) \to M \in ℤ$
33	31 3	syl	$⊢ (((φ \land lim sup ((m \in Z ⟼ F (m) (x))) \in ℝ) \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} dom F (m)) \land k \in ℤ_{\geq n}) \to S \in SAlg$
34	31 4	syl	$⊢ (((φ \land lim sup ((m \in Z ⟼ F (m) (x))) \in ℝ) \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} dom F (m)) \land k \in ℤ_{\geq n}) \to F : Z ⟶ SMblFn (S)$
35	2	uztrn2	$⊢ (n \in Z \land k \in ℤ_{\geq n}) \to k \in Z$
36	35	3ad2antl2	$⊢ (((φ \land lim sup ((m \in Z ⟼ F (m) (x))) \in ℝ) \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} dom F (m)) \land k \in ℤ_{\geq n}) \to k \in Z$
37		simpl1r	$⊢ (((φ \land lim sup ((m \in Z ⟼ F (m) (x))) \in ℝ) \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} dom F (m)) \land k \in ℤ_{\geq n}) \to lim sup ((m \in Z ⟼ F (m) (x))) \in ℝ$
38		uzss	$⊢ k \in ℤ_{\geq n} \to ℤ_{\geq k} \subseteq ℤ_{\geq n}$
39		iinss1	$⊢ ℤ_{\geq k} \subseteq ℤ_{\geq n} \to ⋂_{m \in ℤ_{\geq n}} dom F (m) \subseteq ⋂_{m \in ℤ_{\geq k}} dom F (m)$
40	38 39	syl	$⊢ k \in ℤ_{\geq n} \to ⋂_{m \in ℤ_{\geq n}} dom F (m) \subseteq ⋂_{m \in ℤ_{\geq k}} dom F (m)$
41	40	adantl	$⊢ (x \in ⋂_{m \in ℤ_{\geq n}} dom F (m) \land k \in ℤ_{\geq n}) \to ⋂_{m \in ℤ_{\geq n}} dom F (m) \subseteq ⋂_{m \in ℤ_{\geq k}} dom F (m)$
42		simpl	$⊢ (x \in ⋂_{m \in ℤ_{\geq n}} dom F (m) \land k \in ℤ_{\geq n}) \to x \in ⋂_{m \in ℤ_{\geq n}} dom F (m)$
43	41 42	sseldd	$⊢ (x \in ⋂_{m \in ℤ_{\geq n}} dom F (m) \land k \in ℤ_{\geq n}) \to x \in ⋂_{m \in ℤ_{\geq k}} dom F (m)$
44	43	3ad2antl3	$⊢ (((φ \land lim sup ((m \in Z ⟼ F (m) (x))) \in ℝ) \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} dom F (m)) \land k \in ℤ_{\geq n}) \to x \in ⋂_{m \in ℤ_{\geq k}} dom F (m)$
45	30 32 2 33 34 6 7 36 37 44	smflimsuplem2	$⊢ (((φ \land lim sup ((m \in Z ⟼ F (m) (x))) \in ℝ) \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} dom F (m)) \land k \in ℤ_{\geq n}) \to x \in dom H (k)$
46	45	ralrimiva	$⊢ ((φ \land lim sup ((m \in Z ⟼ F (m) (x))) \in ℝ) \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} dom F (m)) \to \forall k \in ℤ_{\geq n} x \in dom H (k)$
47		vex	$⊢ x \in V$
48		eliin	$⊢ x \in V \to (x \in ⋂_{k \in ℤ_{\geq n}} dom H (k) \leftrightarrow \forall k \in ℤ_{\geq n} x \in dom H (k))$
49	47 48	ax-mp	$⊢ x \in ⋂_{k \in ℤ_{\geq n}} dom H (k) \leftrightarrow \forall k \in ℤ_{\geq n} x \in dom H (k)$
50	46 49	sylibr	$⊢ ((φ \land lim sup ((m \in Z ⟼ F (m) (x))) \in ℝ) \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} dom F (m)) \to x \in ⋂_{k \in ℤ_{\geq n}} dom H (k)$
51	50	3exp	$⊢ (φ \land lim sup ((m \in Z ⟼ F (m) (x))) \in ℝ) \to (n \in Z \to (x \in ⋂_{m \in ℤ_{\geq n}} dom F (m) \to x \in ⋂_{k \in ℤ_{\geq n}} dom H (k)))$
52	16 51	reximdai	$⊢ (φ \land lim sup ((m \in Z ⟼ F (m) (x))) \in ℝ) \to (\exists n \in Z x \in ⋂_{m \in ℤ_{\geq n}} dom F (m) \to \exists n \in Z x \in ⋂_{k \in ℤ_{\geq n}} dom H (k))$
53	52	imp	$⊢ ((φ \land lim sup ((m \in Z ⟼ F (m) (x))) \in ℝ) \land \exists n \in Z x \in ⋂_{m \in ℤ_{\geq n}} dom F (m)) \to \exists n \in Z x \in ⋂_{k \in ℤ_{\geq n}} dom H (k)$
54		eliun	$⊢ x \in ⋃_{n \in Z} ⋂_{k \in ℤ_{\geq n}} dom H (k) \leftrightarrow \exists n \in Z x \in ⋂_{k \in ℤ_{\geq n}} dom H (k)$
55	53 54	sylibr	$⊢ ((φ \land lim sup ((m \in Z ⟼ F (m) (x))) \in ℝ) \land \exists n \in Z x \in ⋂_{m \in ℤ_{\geq n}} dom F (m)) \to x \in ⋃_{n \in Z} ⋂_{k \in ℤ_{\geq n}} dom H (k)$
56	9 11 15 55	syl21anc	$⊢ (φ \land x \in \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| lim sup ((m \in Z ⟼ F (m) (x))) \in ℝ\}) \to x \in ⋃_{n \in Z} ⋂_{k \in ℤ_{\geq n}} dom H (k)$
57	13	biimpi	$⊢ x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \to \exists n \in Z x \in ⋂_{m \in ℤ_{\geq n}} dom F (m)$
58	12 57	syl	$⊢ x \in \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| lim sup ((m \in Z ⟼ F (m) (x))) \in ℝ\} \to \exists n \in Z x \in ⋂_{m \in ℤ_{\geq n}} dom F (m)$
59	58	adantl	$⊢ (φ \land x \in \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| lim sup ((m \in Z ⟼ F (m) (x))) \in ℝ\}) \to \exists n \in Z x \in ⋂_{m \in ℤ_{\geq n}} dom F (m)$
60		nfv	$⊢ Ⅎ n φ$
61		nfcv	$⊢ \underline{Ⅎ} n x$
62		nfv	$⊢ Ⅎ n lim sup ((m \in Z ⟼ F (m) (x))) \in ℝ$
63		nfiu1	$⊢ \underline{Ⅎ} n ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m)$
64	62 63	nfrabw	$⊢ \underline{Ⅎ} n \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| lim sup ((m \in Z ⟼ F (m) (x))) \in ℝ\}$
65	61 64	nfel	$⊢ Ⅎ n x \in \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| lim sup ((m \in Z ⟼ F (m) (x))) \in ℝ\}$
66	60 65	nfan	$⊢ Ⅎ n (φ \land x \in \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| lim sup ((m \in Z ⟼ F (m) (x))) \in ℝ\})$
67		nfv	$⊢ Ⅎ n (k \in Z ⟼ H (k) (x)) \in dom ⇝$
68		nfv	$⊢ Ⅎ k ((φ \land lim sup ((m \in Z ⟼ F (m) (x))) \in ℝ) \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} dom F (m))$
69		simp1l	$⊢ ((φ \land lim sup ((m \in Z ⟼ F (m) (x))) \in ℝ) \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} dom F (m)) \to φ$
70	69 1	syl	$⊢ ((φ \land lim sup ((m \in Z ⟼ F (m) (x))) \in ℝ) \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} dom F (m)) \to M \in ℤ$
71	69 3	syl	$⊢ ((φ \land lim sup ((m \in Z ⟼ F (m) (x))) \in ℝ) \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} dom F (m)) \to S \in SAlg$
72	69 4	syl	$⊢ ((φ \land lim sup ((m \in Z ⟼ F (m) (x))) \in ℝ) \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} dom F (m)) \to F : Z ⟶ SMblFn (S)$
73		simp1r	$⊢ ((φ \land lim sup ((m \in Z ⟼ F (m) (x))) \in ℝ) \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} dom F (m)) \to lim sup ((m \in Z ⟼ F (m) (x))) \in ℝ$
74		simp2	$⊢ ((φ \land lim sup ((m \in Z ⟼ F (m) (x))) \in ℝ) \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} dom F (m)) \to n \in Z$
75		simp3	$⊢ ((φ \land lim sup ((m \in Z ⟼ F (m) (x))) \in ℝ) \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} dom F (m)) \to x \in ⋂_{m \in ℤ_{\geq n}} dom F (m)$
76	68 28 70 2 71 72 6 7 73 74 75	smflimsuplem6	$⊢ ((φ \land lim sup ((m \in Z ⟼ F (m) (x))) \in ℝ) \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} dom F (m)) \to (k \in Z ⟼ H (k) (x)) \in dom ⇝$
77	76	3exp	$⊢ (φ \land lim sup ((m \in Z ⟼ F (m) (x))) \in ℝ) \to (n \in Z \to (x \in ⋂_{m \in ℤ_{\geq n}} dom F (m) \to (k \in Z ⟼ H (k) (x)) \in dom ⇝))$
78	11 77	syldan	$⊢ (φ \land x \in \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| lim sup ((m \in Z ⟼ F (m) (x))) \in ℝ\}) \to (n \in Z \to (x \in ⋂_{m \in ℤ_{\geq n}} dom F (m) \to (k \in Z ⟼ H (k) (x)) \in dom ⇝))$
79	66 67 78	rexlimd	$⊢ (φ \land x \in \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| lim sup ((m \in Z ⟼ F (m) (x))) \in ℝ\}) \to (\exists n \in Z x \in ⋂_{m \in ℤ_{\geq n}} dom F (m) \to (k \in Z ⟼ H (k) (x)) \in dom ⇝)$
80	59 79	mpd	$⊢ (φ \land x \in \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| lim sup ((m \in Z ⟼ F (m) (x))) \in ℝ\}) \to (k \in Z ⟼ H (k) (x)) \in dom ⇝$
81	56 80	jca	$⊢ (φ \land x \in \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| lim sup ((m \in Z ⟼ F (m) (x))) \in ℝ\}) \to (x \in ⋃_{n \in Z} ⋂_{k \in ℤ_{\geq n}} dom H (k) \land (k \in Z ⟼ H (k) (x)) \in dom ⇝)$
82		rabid	$⊢ x \in \{x \in ⋃_{n \in Z} ⋂_{k \in ℤ_{\geq n}} dom H (k) \| (k \in Z ⟼ H (k) (x)) \in dom ⇝\} \leftrightarrow (x \in ⋃_{n \in Z} ⋂_{k \in ℤ_{\geq n}} dom H (k) \land (k \in Z ⟼ H (k) (x)) \in dom ⇝)$
83	81 82	sylibr	$⊢ (φ \land x \in \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| lim sup ((m \in Z ⟼ F (m) (x))) \in ℝ\}) \to x \in \{x \in ⋃_{n \in Z} ⋂_{k \in ℤ_{\geq n}} dom H (k) \| (k \in Z ⟼ H (k) (x)) \in dom ⇝\}$
84	83	ex	$⊢ φ \to (x \in \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| lim sup ((m \in Z ⟼ F (m) (x))) \in ℝ\} \to x \in \{x \in ⋃_{n \in Z} ⋂_{k \in ℤ_{\geq n}} dom H (k) \| (k \in Z ⟼ H (k) (x)) \in dom ⇝\})$
85		ssrab2	$⊢ \{x \in ⋃_{n \in Z} ⋂_{k \in ℤ_{\geq n}} dom H (k) \| (k \in Z ⟼ H (k) (x)) \in dom ⇝\} \subseteq ⋃_{n \in Z} ⋂_{k \in ℤ_{\geq n}} dom H (k)$
86	85	a1i	$⊢ φ \to \{x \in ⋃_{n \in Z} ⋂_{k \in ℤ_{\geq n}} dom H (k) \| (k \in Z ⟼ H (k) (x)) \in dom ⇝\} \subseteq ⋃_{n \in Z} ⋂_{k \in ℤ_{\geq n}} dom H (k)$
87	2	eluzelz2	$⊢ n \in Z \to n \in ℤ$
88	87	uzidd	$⊢ n \in Z \to n \in ℤ_{\geq n}$
89	88	adantl	$⊢ (φ \land n \in Z) \to n \in ℤ_{\geq n}$
90		nfv	$⊢ Ⅎ x (φ \land n \in Z)$
91		xrltso	$⊢ < Or ℝ^{*}$
92	91	a1i	$⊢ ((φ \land n \in Z) \land x \in E (n)) \to < Or ℝ^{*}$
93	92	supexd	$⊢ ((φ \land n \in Z) \land x \in E (n)) \to sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{*} <) \in V$
94		eqid	$⊢ (x \in E (n) ⟼ sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{} <)) = (x \in E (n) ⟼ sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{} <))$
95	90 93 94	fnmptd	$⊢ (φ \land n \in Z) \to (x \in E (n) ⟼ sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{*} <)) Fn E (n)$
96		fveq2	$⊢ k = n \to E (k) = E (n)$
97		fveq2	$⊢ k = n \to ℤ_{\geq k} = ℤ_{\geq n}$
98	97	mpteq1d	$⊢ k = n \to (m \in ℤ_{\geq k} ⟼ F (m) (x)) = (m \in ℤ_{\geq n} ⟼ F (m) (x))$
99	98	rneqd	$⊢ k = n \to ran (m \in ℤ_{\geq k} ⟼ F (m) (x)) = ran (m \in ℤ_{\geq n} ⟼ F (m) (x))$
100	99	supeq1d	$⊢ k = n \to sup (ran (m \in ℤ_{\geq k} ⟼ F (m) (x)) ℝ^{} <) = sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{} <)$
101	96 100	mpteq12dv	$⊢ k = n \to (x \in E (k) ⟼ sup (ran (m \in ℤ_{\geq k} ⟼ F (m) (x)) ℝ^{} <)) = (x \in E (n) ⟼ sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{} <))$
102		fvex	$⊢ E (n) \in V$
103	102	mptex	$⊢ (x \in E (n) ⟼ sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{*} <)) \in V$
104	101 7 103	fvmpt	$⊢ n \in Z \to H (n) = (x \in E (n) ⟼ sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{*} <))$
105	104	adantl	$⊢ (φ \land n \in Z) \to H (n) = (x \in E (n) ⟼ sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{*} <))$
106	105	fneq1d	$⊢ (φ \land n \in Z) \to (H (n) Fn E (n) \leftrightarrow (x \in E (n) ⟼ sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{*} <)) Fn E (n))$
107	95 106	mpbird	$⊢ (φ \land n \in Z) \to H (n) Fn E (n)$
108	107	fndmd	$⊢ (φ \land n \in Z) \to dom H (n) = E (n)$
109	97	iineq1d	$⊢ k = n \to ⋂_{m \in ℤ_{\geq k}} dom F (m) = ⋂_{m \in ℤ_{\geq n}} dom F (m)$
110	109	eleq2d	$⊢ k = n \to (x \in ⋂_{m \in ℤ_{\geq k}} dom F (m) \leftrightarrow x \in ⋂_{m \in ℤ_{\geq n}} dom F (m))$
111	100	eleq1d	$⊢ k = n \to (sup (ran (m \in ℤ_{\geq k} ⟼ F (m) (x)) ℝ^{} <) \in ℝ \leftrightarrow sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{} <) \in ℝ)$
112	110 111	anbi12d	$⊢ k = n \to ((x \in ⋂_{m \in ℤ_{\geq k}} dom F (m) \land sup (ran (m \in ℤ_{\geq k} ⟼ F (m) (x)) ℝ^{} <) \in ℝ) \leftrightarrow (x \in ⋂_{m \in ℤ_{\geq n}} dom F (m) \land sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{} <) \in ℝ))$
113	112	rabbidva2	$⊢ k = n \to \{x \in ⋂_{m \in ℤ_{\geq k}} dom F (m) \| sup (ran (m \in ℤ_{\geq k} ⟼ F (m) (x)) ℝ^{} <) \in ℝ\} = \{x \in ⋂_{m \in ℤ_{\geq n}} dom F (m) \| sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{} <) \in ℝ\}$
114		id	$⊢ n \in Z \to n \in Z$
115		fveq2	$⊢ x = y \to F (m) (x) = F (m) (y)$
116	115	mpteq2dv	$⊢ x = y \to (m \in ℤ_{\geq n} ⟼ F (m) (x)) = (m \in ℤ_{\geq n} ⟼ F (m) (y))$
117	116	rneqd	$⊢ x = y \to ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) = ran (m \in ℤ_{\geq n} ⟼ F (m) (y))$
118	117	supeq1d	$⊢ x = y \to sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{} <) = sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (y)) ℝ^{} <)$
119	118	eleq1d	$⊢ x = y \to (sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{} <) \in ℝ \leftrightarrow sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (y)) ℝ^{} <) \in ℝ)$
120	119	cbvrabv	$⊢ \{x \in ⋂_{m \in ℤ_{\geq n}} dom F (m) \| sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{} <) \in ℝ\} = \{y \in ⋂_{m \in ℤ_{\geq n}} dom F (m) \| sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (y)) ℝ^{} <) \in ℝ\}$
121	88	ne0d	$⊢ n \in Z \to ℤ_{\geq n} \neq \emptyset$
122		fvex	$⊢ F (m) \in V$
123	122	dmex	$⊢ dom F (m) \in V$
124	123	rgenw	$⊢ \forall m \in ℤ_{\geq n} dom F (m) \in V$
125	124	a1i	$⊢ n \in Z \to \forall m \in ℤ_{\geq n} dom F (m) \in V$
126	121 125	iinexd	$⊢ n \in Z \to ⋂_{m \in ℤ_{\geq n}} dom F (m) \in V$
127	120 126	rabexd	$⊢ n \in Z \to \{x \in ⋂_{m \in ℤ_{\geq n}} dom F (m) \| sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{*} <) \in ℝ\} \in V$
128	6 113 114 127	fvmptd3	$⊢ n \in Z \to E (n) = \{x \in ⋂_{m \in ℤ_{\geq n}} dom F (m) \| sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{*} <) \in ℝ\}$
129	128	adantl	$⊢ (φ \land n \in Z) \to E (n) = \{x \in ⋂_{m \in ℤ_{\geq n}} dom F (m) \| sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{*} <) \in ℝ\}$
130		ssrab2	$⊢ \{x \in ⋂_{m \in ℤ_{\geq n}} dom F (m) \| sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{*} <) \in ℝ\} \subseteq ⋂_{m \in ℤ_{\geq n}} dom F (m)$
131	130	a1i	$⊢ (φ \land n \in Z) \to \{x \in ⋂_{m \in ℤ_{\geq n}} dom F (m) \| sup (ran (m \in ℤ_{\geq n} ⟼ F (m) (x)) ℝ^{*} <) \in ℝ\} \subseteq ⋂_{m \in ℤ_{\geq n}} dom F (m)$
132	129 131	eqsstrd	$⊢ (φ \land n \in Z) \to E (n) \subseteq ⋂_{m \in ℤ_{\geq n}} dom F (m)$
133	108 132	eqsstrd	$⊢ (φ \land n \in Z) \to dom H (n) \subseteq ⋂_{m \in ℤ_{\geq n}} dom F (m)$
134		fveq2	$⊢ k = n \to H (k) = H (n)$
135	134	dmeqd	$⊢ k = n \to dom H (k) = dom H (n)$
136	135	sseq1d	$⊢ k = n \to (dom H (k) \subseteq ⋂_{m \in ℤ_{\geq n}} dom F (m) \leftrightarrow dom H (n) \subseteq ⋂_{m \in ℤ_{\geq n}} dom F (m))$
137	136	rspcev	$⊢ (n \in ℤ_{\geq n} \land dom H (n) \subseteq ⋂_{m \in ℤ_{\geq n}} dom F (m)) \to \exists k \in ℤ_{\geq n} dom H (k) \subseteq ⋂_{m \in ℤ_{\geq n}} dom F (m)$
138	89 133 137	syl2anc	$⊢ (φ \land n \in Z) \to \exists k \in ℤ_{\geq n} dom H (k) \subseteq ⋂_{m \in ℤ_{\geq n}} dom F (m)$
139		iinss	$⊢ \exists k \in ℤ_{\geq n} dom H (k) \subseteq ⋂_{m \in ℤ_{\geq n}} dom F (m) \to ⋂_{k \in ℤ_{\geq n}} dom H (k) \subseteq ⋂_{m \in ℤ_{\geq n}} dom F (m)$
140	138 139	syl	$⊢ (φ \land n \in Z) \to ⋂_{k \in ℤ_{\geq n}} dom H (k) \subseteq ⋂_{m \in ℤ_{\geq n}} dom F (m)$
141	140	ralrimiva	$⊢ φ \to \forall n \in Z ⋂_{k \in ℤ_{\geq n}} dom H (k) \subseteq ⋂_{m \in ℤ_{\geq n}} dom F (m)$
142		ss2iun	$⊢ \forall n \in Z ⋂_{k \in ℤ_{\geq n}} dom H (k) \subseteq ⋂_{m \in ℤ_{\geq n}} dom F (m) \to ⋃_{n \in Z} ⋂_{k \in ℤ_{\geq n}} dom H (k) \subseteq ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m)$
143	141 142	syl	$⊢ φ \to ⋃_{n \in Z} ⋂_{k \in ℤ_{\geq n}} dom H (k) \subseteq ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m)$
144	86 143	sstrd	$⊢ φ \to \{x \in ⋃_{n \in Z} ⋂_{k \in ℤ_{\geq n}} dom H (k) \| (k \in Z ⟼ H (k) (x)) \in dom ⇝\} \subseteq ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m)$
145	82	simplbi	$⊢ x \in \{x \in ⋃_{n \in Z} ⋂_{k \in ℤ_{\geq n}} dom H (k) \| (k \in Z ⟼ H (k) (x)) \in dom ⇝\} \to x \in ⋃_{n \in Z} ⋂_{k \in ℤ_{\geq n}} dom H (k)$
146	54	biimpi	$⊢ x \in ⋃_{n \in Z} ⋂_{k \in ℤ_{\geq n}} dom H (k) \to \exists n \in Z x \in ⋂_{k \in ℤ_{\geq n}} dom H (k)$
147	145 146	syl	$⊢ x \in \{x \in ⋃_{n \in Z} ⋂_{k \in ℤ_{\geq n}} dom H (k) \| (k \in Z ⟼ H (k) (x)) \in dom ⇝\} \to \exists n \in Z x \in ⋂_{k \in ℤ_{\geq n}} dom H (k)$
148	147	adantl	$⊢ (φ \land x \in \{x \in ⋃_{n \in Z} ⋂_{k \in ℤ_{\geq n}} dom H (k) \| (k \in Z ⟼ H (k) (x)) \in dom ⇝\}) \to \exists n \in Z x \in ⋂_{k \in ℤ_{\geq n}} dom H (k)$
149		nfiu1	$⊢ \underline{Ⅎ} n ⋃_{n \in Z} ⋂_{k \in ℤ_{\geq n}} dom H (k)$
150	67 149	nfrabw	$⊢ \underline{Ⅎ} n \{x \in ⋃_{n \in Z} ⋂_{k \in ℤ_{\geq n}} dom H (k) \| (k \in Z ⟼ H (k) (x)) \in dom ⇝\}$
151	61 150	nfel	$⊢ Ⅎ n x \in \{x \in ⋃_{n \in Z} ⋂_{k \in ℤ_{\geq n}} dom H (k) \| (k \in Z ⟼ H (k) (x)) \in dom ⇝\}$
152	60 151	nfan	$⊢ Ⅎ n (φ \land x \in \{x \in ⋃_{n \in Z} ⋂_{k \in ℤ_{\geq n}} dom H (k) \| (k \in Z ⟼ H (k) (x)) \in dom ⇝\})$
153	82	simprbi	$⊢ x \in \{x \in ⋃_{n \in Z} ⋂_{k \in ℤ_{\geq n}} dom H (k) \| (k \in Z ⟼ H (k) (x)) \in dom ⇝\} \to (k \in Z ⟼ H (k) (x)) \in dom ⇝$
154		nfv	$⊢ Ⅎ k φ$
155		nfmpt1	$⊢ \underline{Ⅎ} k (k \in Z ⟼ H (k) (x))$
156		nfcv	$⊢ \underline{Ⅎ} k dom ⇝$
157	155 156	nfel	$⊢ Ⅎ k (k \in Z ⟼ H (k) (x)) \in dom ⇝$
158	154 157	nfan	$⊢ Ⅎ k (φ \land (k \in Z ⟼ H (k) (x)) \in dom ⇝)$
159		nfv	$⊢ Ⅎ k n \in Z$
160		nfcv	$⊢ \underline{Ⅎ} k x$
161		nfii1	$⊢ \underline{Ⅎ} k ⋂_{k \in ℤ_{\geq n}} dom H (k)$
162	160 161	nfel	$⊢ Ⅎ k x \in ⋂_{k \in ℤ_{\geq n}} dom H (k)$
163	158 159 162	nf3an	$⊢ Ⅎ k ((φ \land (k \in Z ⟼ H (k) (x)) \in dom ⇝) \land n \in Z \land x \in ⋂_{k \in ℤ_{\geq n}} dom H (k))$
164	1	adantr	$⊢ (φ \land n \in Z) \to M \in ℤ$
165	164	3adant3	$⊢ (φ \land n \in Z \land x \in ⋂_{k \in ℤ_{\geq n}} dom H (k)) \to M \in ℤ$
166	165	3adant1r	$⊢ ((φ \land (k \in Z ⟼ H (k) (x)) \in dom ⇝) \land n \in Z \land x \in ⋂_{k \in ℤ_{\geq n}} dom H (k)) \to M \in ℤ$
167	3	adantr	$⊢ (φ \land n \in Z) \to S \in SAlg$
168	167	3adant3	$⊢ (φ \land n \in Z \land x \in ⋂_{k \in ℤ_{\geq n}} dom H (k)) \to S \in SAlg$
169	168	3adant1r	$⊢ ((φ \land (k \in Z ⟼ H (k) (x)) \in dom ⇝) \land n \in Z \land x \in ⋂_{k \in ℤ_{\geq n}} dom H (k)) \to S \in SAlg$
170	4	adantr	$⊢ (φ \land n \in Z) \to F : Z ⟶ SMblFn (S)$
171	170	3adant3	$⊢ (φ \land n \in Z \land x \in ⋂_{k \in ℤ_{\geq n}} dom H (k)) \to F : Z ⟶ SMblFn (S)$
172	171	3adant1r	$⊢ ((φ \land (k \in Z ⟼ H (k) (x)) \in dom ⇝) \land n \in Z \land x \in ⋂_{k \in ℤ_{\geq n}} dom H (k)) \to F : Z ⟶ SMblFn (S)$
173		simp2	$⊢ ((φ \land (k \in Z ⟼ H (k) (x)) \in dom ⇝) \land n \in Z \land x \in ⋂_{k \in ℤ_{\geq n}} dom H (k)) \to n \in Z$
174		simp3	$⊢ ((φ \land (k \in Z ⟼ H (k) (x)) \in dom ⇝) \land n \in Z \land x \in ⋂_{k \in ℤ_{\geq n}} dom H (k)) \to x \in ⋂_{k \in ℤ_{\geq n}} dom H (k)$
175		simp1r	$⊢ ((φ \land (k \in Z ⟼ H (k) (x)) \in dom ⇝) \land n \in Z \land x \in ⋂_{k \in ℤ_{\geq n}} dom H (k)) \to (k \in Z ⟼ H (k) (x)) \in dom ⇝$
176	163 166 2 169 172 6 7 173 174 175	smflimsuplem4	$⊢ ((φ \land (k \in Z ⟼ H (k) (x)) \in dom ⇝) \land n \in Z \land x \in ⋂_{k \in ℤ_{\geq n}} dom H (k)) \to lim sup ((m \in Z ⟼ F (m) (x))) \in ℝ$
177	176	3exp	$⊢ (φ \land (k \in Z ⟼ H (k) (x)) \in dom ⇝) \to (n \in Z \to (x \in ⋂_{k \in ℤ_{\geq n}} dom H (k) \to lim sup ((m \in Z ⟼ F (m) (x))) \in ℝ))$
178	153 177	sylan2	$⊢ (φ \land x \in \{x \in ⋃_{n \in Z} ⋂_{k \in ℤ_{\geq n}} dom H (k) \| (k \in Z ⟼ H (k) (x)) \in dom ⇝\}) \to (n \in Z \to (x \in ⋂_{k \in ℤ_{\geq n}} dom H (k) \to lim sup ((m \in Z ⟼ F (m) (x))) \in ℝ))$
179	152 62 178	rexlimd	$⊢ (φ \land x \in \{x \in ⋃_{n \in Z} ⋂_{k \in ℤ_{\geq n}} dom H (k) \| (k \in Z ⟼ H (k) (x)) \in dom ⇝\}) \to (\exists n \in Z x \in ⋂_{k \in ℤ_{\geq n}} dom H (k) \to lim sup ((m \in Z ⟼ F (m) (x))) \in ℝ)$
180	148 179	mpd	$⊢ (φ \land x \in \{x \in ⋃_{n \in Z} ⋂_{k \in ℤ_{\geq n}} dom H (k) \| (k \in Z ⟼ H (k) (x)) \in dom ⇝\}) \to lim sup ((m \in Z ⟼ F (m) (x))) \in ℝ$
181	180	ralrimiva	$⊢ φ \to \forall x \in \{x \in ⋃_{n \in Z} ⋂_{k \in ℤ_{\geq n}} dom H (k) \| (k \in Z ⟼ H (k) (x)) \in dom ⇝\} lim sup ((m \in Z ⟼ F (m) (x))) \in ℝ$
182	144 181	jca	$⊢ φ \to (\{x \in ⋃_{n \in Z} ⋂_{k \in ℤ_{\geq n}} dom H (k) \| (k \in Z ⟼ H (k) (x)) \in dom ⇝\} \subseteq ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \land \forall x \in \{x \in ⋃_{n \in Z} ⋂_{k \in ℤ_{\geq n}} dom H (k) \| (k \in Z ⟼ H (k) (x)) \in dom ⇝\} lim sup ((m \in Z ⟼ F (m) (x))) \in ℝ)$
183		nfrab1	$⊢ \underline{Ⅎ} x \{x \in ⋃_{n \in Z} ⋂_{k \in ℤ_{\geq n}} dom H (k) \| (k \in Z ⟼ H (k) (x)) \in dom ⇝\}$
184		nfcv	$⊢ \underline{Ⅎ} x ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m)$
185	183 184	ssrabf	$⊢ \{x \in ⋃_{n \in Z} ⋂_{k \in ℤ_{\geq n}} dom H (k) \| (k \in Z ⟼ H (k) (x)) \in dom ⇝\} \subseteq \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| lim sup ((m \in Z ⟼ F (m) (x))) \in ℝ\} \leftrightarrow (\{x \in ⋃_{n \in Z} ⋂_{k \in ℤ_{\geq n}} dom H (k) \| (k \in Z ⟼ H (k) (x)) \in dom ⇝\} \subseteq ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \land \forall x \in \{x \in ⋃_{n \in Z} ⋂_{k \in ℤ_{\geq n}} dom H (k) \| (k \in Z ⟼ H (k) (x)) \in dom ⇝\} lim sup ((m \in Z ⟼ F (m) (x))) \in ℝ)$
186	182 185	sylibr	$⊢ φ \to \{x \in ⋃_{n \in Z} ⋂_{k \in ℤ_{\geq n}} dom H (k) \| (k \in Z ⟼ H (k) (x)) \in dom ⇝\} \subseteq \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| lim sup ((m \in Z ⟼ F (m) (x))) \in ℝ\}$
187	186	sseld	$⊢ φ \to (x \in \{x \in ⋃_{n \in Z} ⋂_{k \in ℤ_{\geq n}} dom H (k) \| (k \in Z ⟼ H (k) (x)) \in dom ⇝\} \to x \in \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| lim sup ((m \in Z ⟼ F (m) (x))) \in ℝ\})$
188	84 187	impbid	$⊢ φ \to (x \in \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| lim sup ((m \in Z ⟼ F (m) (x))) \in ℝ\} \leftrightarrow x \in \{x \in ⋃_{n \in Z} ⋂_{k \in ℤ_{\geq n}} dom H (k) \| (k \in Z ⟼ H (k) (x)) \in dom ⇝\})$
189	188	alrimiv	$⊢ φ \to \forall x (x \in \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| lim sup ((m \in Z ⟼ F (m) (x))) \in ℝ\} \leftrightarrow x \in \{x \in ⋃_{n \in Z} ⋂_{k \in ℤ_{\geq n}} dom H (k) \| (k \in Z ⟼ H (k) (x)) \in dom ⇝\})$
190		nfrab1	$⊢ \underline{Ⅎ} x \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| lim sup ((m \in Z ⟼ F (m) (x))) \in ℝ\}$
191	190 183	cleqf	$⊢ \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| lim sup ((m \in Z ⟼ F (m) (x))) \in ℝ\} = \{x \in ⋃_{n \in Z} ⋂_{k \in ℤ_{\geq n}} dom H (k) \| (k \in Z ⟼ H (k) (x)) \in dom ⇝\} \leftrightarrow \forall x (x \in \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| lim sup ((m \in Z ⟼ F (m) (x))) \in ℝ\} \leftrightarrow x \in \{x \in ⋃_{n \in Z} ⋂_{k \in ℤ_{\geq n}} dom H (k) \| (k \in Z ⟼ H (k) (x)) \in dom ⇝\})$
192	189 191	sylibr	$⊢ φ \to \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom F (m) \| lim sup ((m \in Z ⟼ F (m) (x))) \in ℝ\} = \{x \in ⋃_{n \in Z} ⋂_{k \in ℤ_{\geq n}} dom H (k) \| (k \in Z ⟼ H (k) (x)) \in dom ⇝\}$
193	8 192	eqtrd	$⊢ φ \to D = \{x \in ⋃_{n \in Z} ⋂_{k \in ℤ_{\geq n}} dom H (k) \| (k \in Z ⟼ H (k) (x)) \in dom ⇝\}$

Metamath Proof Explorer

Theorem smflimsuplem7

Proof