smflimmpt

Description: The limit of a sequence of sigma-measurable functions is sigma-measurable. Proposition 121F (a) of Fremlin1 p. 38 . Notice that every function in the sequence can have a different (partial) domain, and the domain of convergence can be decidedly irregular (Remark 121G of Fremlin1 p. 39 ). A can contain m as a free variable, in other words it can be thought as an indexed collection A ( m ) . B can be thought as a collection with two indices B ( m , x ) . (Contributed by Glauco Siliprandi, 23-Oct-2021)

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

Proof

Step	Hyp	Ref	Expression
1		smflimmpt.p	$⊢ Ⅎ m φ$
2		smflimmpt.x	$⊢ Ⅎ x φ$
3		smflimmpt.n	$⊢ Ⅎ n φ$
4		smflimmpt.m	$⊢ φ \to M \in ℤ$
5		smflimmpt.z	$⊢ Z = ℤ_{\geq M}$
6		smflimmpt.a	$⊢ (φ \land m \in Z) \to A \in V$
7		smflimmpt.b	$⊢ (φ \land m \in Z \land x \in A) \to B \in W$
8		smflimmpt.s	$⊢ φ \to S \in SAlg$
9		smflimmpt.l	$⊢ (φ \land m \in Z) \to (x \in A ⟼ B) \in SMblFn (S)$
10		smflimmpt.d	$⊢ D = \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} A \| (m \in Z ⟼ B) \in dom ⇝\}$
11		smflimmpt.g	$⊢ G = (x \in D ⟼ ⇝ ((m \in Z ⟼ B)))$
12	11	a1i	$⊢ φ \to G = (x \in D ⟼ ⇝ ((m \in Z ⟼ B)))$
13	10	a1i	$⊢ φ \to D = \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} A \| (m \in Z ⟼ B) \in dom ⇝\}$
14		nfv	$⊢ Ⅎ m n \in Z$
15	1 14	nfan	$⊢ Ⅎ m (φ \land n \in Z)$
16	5	uztrn2	$⊢ (n \in Z \land m \in ℤ_{\geq n}) \to m \in Z$
17	16	adantll	$⊢ ((φ \land n \in Z) \land m \in ℤ_{\geq n}) \to m \in Z$
18		simpll	$⊢ ((φ \land n \in Z) \land m \in ℤ_{\geq n}) \to φ$
19	6	mptexd	$⊢ (φ \land m \in Z) \to (x \in A ⟼ B) \in V$
20	18 17 19	syl2anc	$⊢ ((φ \land n \in Z) \land m \in ℤ_{\geq n}) \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	17 20 22	syl2anc	$⊢ ((φ \land n \in Z) \land m \in ℤ_{\geq n}) \to (m \in Z ⟼ (x \in A ⟼ B)) (m) = (x \in A ⟼ B)$
24	23	dmeqd	$⊢ ((φ \land n \in Z) \land m \in ℤ_{\geq n}) \to dom (m \in Z ⟼ (x \in A ⟼ B)) (m) = dom (x \in A ⟼ B)$
25		nfv	$⊢ Ⅎ x n \in Z$
26	2 25	nfan	$⊢ Ⅎ x (φ \land n \in Z)$
27		nfv	$⊢ Ⅎ x m \in ℤ_{\geq n}$
28	26 27	nfan	$⊢ Ⅎ x ((φ \land n \in Z) \land m \in ℤ_{\geq n})$
29		simplll	$⊢ (((φ \land n \in Z) \land m \in ℤ_{\geq n}) \land x \in A) \to φ$
30	17	adantr	$⊢ (((φ \land n \in Z) \land m \in ℤ_{\geq n}) \land x \in A) \to m \in Z$
31		simpr	$⊢ (((φ \land n \in Z) \land m \in ℤ_{\geq n}) \land x \in A) \to x \in A$
32	29 30 31 7	syl3anc	$⊢ (((φ \land n \in Z) \land m \in ℤ_{\geq n}) \land x \in A) \to B \in W$
33		eqid	$⊢ (x \in A ⟼ B) = (x \in A ⟼ B)$
34	28 32 33	fnmptd	$⊢ ((φ \land n \in Z) \land m \in ℤ_{\geq n}) \to (x \in A ⟼ B) Fn A$
35	34	fndmd	$⊢ ((φ \land n \in Z) \land m \in ℤ_{\geq n}) \to dom (x \in A ⟼ B) = A$
36	24 35	eqtr2d	$⊢ ((φ \land n \in Z) \land m \in ℤ_{\geq n}) \to A = dom (m \in Z ⟼ (x \in A ⟼ B)) (m)$
37	15 36	iineq2d	$⊢ (φ \land n \in Z) \to ⋂_{m \in ℤ_{\geq n}} A = ⋂_{m \in ℤ_{\geq n}} dom (m \in Z ⟼ (x \in A ⟼ B)) (m)$
38	3 37	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)$
39		simpr	$⊢ (φ \land m \in Z) \to m \in Z$
40	39 19 22	syl2anc	$⊢ (φ \land m \in Z) \to (m \in Z ⟼ (x \in A ⟼ B)) (m) = (x \in A ⟼ B)$
41	40	eqcomd	$⊢ (φ \land m \in Z) \to (x \in A ⟼ B) = (m \in Z ⟼ (x \in A ⟼ B)) (m)$
42	41	dmeqd	$⊢ (φ \land m \in Z) \to dom (x \in A ⟼ B) = dom (m \in Z ⟼ (x \in A ⟼ B)) (m)$
43	18 17 42	syl2anc	$⊢ ((φ \land n \in Z) \land m \in ℤ_{\geq n}) \to dom (x \in A ⟼ B) = dom (m \in Z ⟼ (x \in A ⟼ B)) (m)$
44	15 43	iineq2d	$⊢ (φ \land n \in Z) \to ⋂_{m \in ℤ_{\geq n}} dom (x \in A ⟼ B) = ⋂_{m \in ℤ_{\geq n}} dom (m \in Z ⟼ (x \in A ⟼ B)) (m)$
45	3 44	iuneq2df	$⊢ φ \to ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom (x \in A ⟼ B) = ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom (m \in Z ⟼ (x \in A ⟼ B)) (m)$
46	38 45	eqtr4d	$⊢ φ \to ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} A = ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom (x \in A ⟼ B)$
47	46	eleq2d	$⊢ φ \to (x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} A \leftrightarrow x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom (x \in A ⟼ B))$
48	47	biimpa	$⊢ (φ \land x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} A) \to x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom (x \in A ⟼ B)$
49	48	adantrr	$⊢ (φ \land (x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} A \land (m \in Z ⟼ B) \in dom ⇝)) \to x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom (x \in A ⟼ B)$
50		eliun	$⊢ x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} A \leftrightarrow \exists n \in Z x \in ⋂_{m \in ℤ_{\geq n}} A$
51	50	biimpi	$⊢ x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} A \to \exists n \in Z x \in ⋂_{m \in ℤ_{\geq n}} A$
52	51	adantl	$⊢ (φ \land x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} A) \to \exists n \in Z x \in ⋂_{m \in ℤ_{\geq n}} A$
53	52	adantrr	$⊢ (φ \land (x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} A \land (m \in Z ⟼ B) \in dom ⇝)) \to \exists n \in Z x \in ⋂_{m \in ℤ_{\geq n}} A$
54		nfv	$⊢ Ⅎ n (m \in Z ⟼ B) \in dom ⇝$
55	3 54	nfan	$⊢ Ⅎ n (φ \land (m \in Z ⟼ B) \in dom ⇝)$
56		nfv	$⊢ Ⅎ n (m \in Z ⟼ (x \in A ⟼ B) (x)) \in dom ⇝$
57		simpllr	$⊢ (((φ \land (m \in Z ⟼ B) \in dom ⇝) \land n \in Z) \land x \in ⋂_{m \in ℤ_{\geq n}} A) \to (m \in Z ⟼ B) \in dom ⇝$
58		nfcv	$⊢ \underline{Ⅎ} m x$
59		nfii1	$⊢ \underline{Ⅎ} m ⋂_{m \in ℤ_{\geq n}} A$
60	58 59	nfel	$⊢ Ⅎ m x \in ⋂_{m \in ℤ_{\geq n}} A$
61	15 60	nfan	$⊢ Ⅎ m ((φ \land n \in Z) \land x \in ⋂_{m \in ℤ_{\geq n}} A)$
62	5	eluzelz2	$⊢ n \in Z \to n \in ℤ$
63	62	ad2antlr	$⊢ ((φ \land n \in Z) \land x \in ⋂_{m \in ℤ_{\geq n}} A) \to n \in ℤ$
64		eqid	$⊢ ℤ_{\geq n} = ℤ_{\geq n}$
65	5	fvexi	$⊢ Z \in V$
66	65	a1i	$⊢ ((φ \land n \in Z) \land x \in ⋂_{m \in ℤ_{\geq n}} A) \to Z \in V$
67	5	uzssd3	$⊢ n \in Z \to ℤ_{\geq n} \subseteq Z$
68	67	ad2antlr	$⊢ ((φ \land n \in Z) \land x \in ⋂_{m \in ℤ_{\geq n}} A) \to ℤ_{\geq n} \subseteq Z$
69		fvexd	$⊢ (((φ \land n \in Z) \land x \in ⋂_{m \in ℤ_{\geq n}} A) \land m \in ℤ_{\geq n}) \to (x \in A ⟼ B) (x) \in V$
70		eliinid	$⊢ (x \in ⋂_{m \in ℤ_{\geq n}} A \land m \in ℤ_{\geq n}) \to x \in A$
71	70	adantll	$⊢ (((φ \land n \in Z) \land x \in ⋂_{m \in ℤ_{\geq n}} A) \land m \in ℤ_{\geq n}) \to x \in A$
72	18	adantlr	$⊢ (((φ \land n \in Z) \land x \in ⋂_{m \in ℤ_{\geq n}} A) \land m \in ℤ_{\geq n}) \to φ$
73	17	adantlr	$⊢ (((φ \land n \in Z) \land x \in ⋂_{m \in ℤ_{\geq n}} A) \land m \in ℤ_{\geq n}) \to m \in Z$
74	72 73 71 7	syl3anc	$⊢ (((φ \land n \in Z) \land x \in ⋂_{m \in ℤ_{\geq n}} A) \land m \in ℤ_{\geq n}) \to B \in W$
75	33	fvmpt2	$⊢ (x \in A \land B \in W) \to (x \in A ⟼ B) (x) = B$
76	71 74 75	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$
77	61 63 64 66 66 68 68 69 76	climeldmeqmpt3	$⊢ ((φ \land n \in Z) \land x \in ⋂_{m \in ℤ_{\geq n}} A) \to ((m \in Z ⟼ (x \in A ⟼ B) (x)) \in dom ⇝ \leftrightarrow (m \in Z ⟼ B) \in dom ⇝)$
78	77	adantllr	$⊢ (((φ \land (m \in Z ⟼ B) \in dom ⇝) \land n \in Z) \land x \in ⋂_{m \in ℤ_{\geq n}} A) \to ((m \in Z ⟼ (x \in A ⟼ B) (x)) \in dom ⇝ \leftrightarrow (m \in Z ⟼ B) \in dom ⇝)$
79	57 78	mpbird	$⊢ (((φ \land (m \in Z ⟼ B) \in dom ⇝) \land n \in Z) \land x \in ⋂_{m \in ℤ_{\geq n}} A) \to (m \in Z ⟼ (x \in A ⟼ B) (x)) \in dom ⇝$
80	79	exp31	$⊢ (φ \land (m \in Z ⟼ B) \in dom ⇝) \to (n \in Z \to (x \in ⋂_{m \in ℤ_{\geq n}} A \to (m \in Z ⟼ (x \in A ⟼ B) (x)) \in dom ⇝))$
81	55 56 80	rexlimd	$⊢ (φ \land (m \in Z ⟼ B) \in dom ⇝) \to (\exists n \in Z x \in ⋂_{m \in ℤ_{\geq n}} A \to (m \in Z ⟼ (x \in A ⟼ B) (x)) \in dom ⇝)$
82	81	adantrl	$⊢ (φ \land (x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} A \land (m \in Z ⟼ B) \in dom ⇝)) \to (\exists n \in Z x \in ⋂_{m \in ℤ_{\geq n}} A \to (m \in Z ⟼ (x \in A ⟼ B) (x)) \in dom ⇝)$
83	53 82	mpd	$⊢ (φ \land (x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} A \land (m \in Z ⟼ B) \in dom ⇝)) \to (m \in Z ⟼ (x \in A ⟼ B) (x)) \in dom ⇝$
84	49 83	jca	$⊢ (φ \land (x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} A \land (m \in Z ⟼ B) \in dom ⇝)) \to (x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom (x \in A ⟼ B) \land (m \in Z ⟼ (x \in A ⟼ B) (x)) \in dom ⇝)$
85	84	ex	$⊢ φ \to ((x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} A \land (m \in Z ⟼ B) \in dom ⇝) \to (x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom (x \in A ⟼ B) \land (m \in Z ⟼ (x \in A ⟼ B) (x)) \in dom ⇝))$
86	47	biimpar	$⊢ (φ \land x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom (x \in A ⟼ B)) \to x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} A$
87	86	adantrr	$⊢ (φ \land (x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom (x \in A ⟼ B) \land (m \in Z ⟼ (x \in A ⟼ B) (x)) \in dom ⇝)) \to x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} A$
88	87 51	syl	$⊢ (φ \land (x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom (x \in A ⟼ B) \land (m \in Z ⟼ (x \in A ⟼ B) (x)) \in dom ⇝)) \to \exists n \in Z x \in ⋂_{m \in ℤ_{\geq n}} A$
89	3 56	nfan	$⊢ Ⅎ n (φ \land (m \in Z ⟼ (x \in A ⟼ B) (x)) \in dom ⇝)$
90		simpllr	$⊢ (((φ \land (m \in Z ⟼ (x \in A ⟼ B) (x)) \in dom ⇝) \land n \in Z) \land x \in ⋂_{m \in ℤ_{\geq n}} A) \to (m \in Z ⟼ (x \in A ⟼ B) (x)) \in dom ⇝$
91	77	adantllr	$⊢ (((φ \land (m \in Z ⟼ (x \in A ⟼ B) (x)) \in dom ⇝) \land n \in Z) \land x \in ⋂_{m \in ℤ_{\geq n}} A) \to ((m \in Z ⟼ (x \in A ⟼ B) (x)) \in dom ⇝ \leftrightarrow (m \in Z ⟼ B) \in dom ⇝)$
92	90 91	mpbid	$⊢ (((φ \land (m \in Z ⟼ (x \in A ⟼ B) (x)) \in dom ⇝) \land n \in Z) \land x \in ⋂_{m \in ℤ_{\geq n}} A) \to (m \in Z ⟼ B) \in dom ⇝$
93	92	exp31	$⊢ (φ \land (m \in Z ⟼ (x \in A ⟼ B) (x)) \in dom ⇝) \to (n \in Z \to (x \in ⋂_{m \in ℤ_{\geq n}} A \to (m \in Z ⟼ B) \in dom ⇝))$
94	89 54 93	rexlimd	$⊢ (φ \land (m \in Z ⟼ (x \in A ⟼ B) (x)) \in dom ⇝) \to (\exists n \in Z x \in ⋂_{m \in ℤ_{\geq n}} A \to (m \in Z ⟼ B) \in dom ⇝)$
95	94	adantrl	$⊢ (φ \land (x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom (x \in A ⟼ B) \land (m \in Z ⟼ (x \in A ⟼ B) (x)) \in dom ⇝)) \to (\exists n \in Z x \in ⋂_{m \in ℤ_{\geq n}} A \to (m \in Z ⟼ B) \in dom ⇝)$
96	88 95	mpd	$⊢ (φ \land (x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom (x \in A ⟼ B) \land (m \in Z ⟼ (x \in A ⟼ B) (x)) \in dom ⇝)) \to (m \in Z ⟼ B) \in dom ⇝$
97	87 96	jca	$⊢ (φ \land (x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom (x \in A ⟼ B) \land (m \in Z ⟼ (x \in A ⟼ B) (x)) \in dom ⇝)) \to (x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} A \land (m \in Z ⟼ B) \in dom ⇝)$
98	97	ex	$⊢ φ \to ((x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom (x \in A ⟼ B) \land (m \in Z ⟼ (x \in A ⟼ B) (x)) \in dom ⇝) \to (x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} A \land (m \in Z ⟼ B) \in dom ⇝))$
99	85 98	impbid	$⊢ φ \to ((x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} A \land (m \in Z ⟼ B) \in dom ⇝) \leftrightarrow (x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom (x \in A ⟼ B) \land (m \in Z ⟼ (x \in A ⟼ B) (x)) \in dom ⇝))$
100	2 99	rabbida3	$⊢ φ \to \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} A \| (m \in Z ⟼ B) \in dom ⇝\} = \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom (x \in A ⟼ B) \| (m \in Z ⟼ (x \in A ⟼ B) (x)) \in dom ⇝\}$
101	13 100	eqtrd	$⊢ φ \to D = \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom (x \in A ⟼ B) \| (m \in Z ⟼ (x \in A ⟼ B) (x)) \in dom ⇝\}$
102	10	eleq2i	$⊢ x \in D \leftrightarrow x \in \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} A \| (m \in Z ⟼ B) \in dom ⇝\}$
103	102	biimpi	$⊢ x \in D \to x \in \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} A \| (m \in Z ⟼ B) \in dom ⇝\}$
104		rabidim1	$⊢ x \in \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} A \| (m \in Z ⟼ B) \in dom ⇝\} \to x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} A$
105	103 104 51	3syl	$⊢ x \in D \to \exists n \in Z x \in ⋂_{m \in ℤ_{\geq n}} A$
106	105	adantl	$⊢ (φ \land x \in D) \to \exists n \in Z x \in ⋂_{m \in ℤ_{\geq n}} A$
107		nfcv	$⊢ \underline{Ⅎ} n x$
108		nfiu1	$⊢ \underline{Ⅎ} n ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} A$
109	54 108	nfrabw	$⊢ \underline{Ⅎ} n \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} A \| (m \in Z ⟼ B) \in dom ⇝\}$
110	10 109	nfcxfr	$⊢ \underline{Ⅎ} n D$
111	107 110	nfel	$⊢ Ⅎ n x \in D$
112	3 111	nfan	$⊢ Ⅎ n (φ \land x \in D)$
113		nfv	$⊢ Ⅎ n ⇝ ((m \in Z ⟼ (x \in A ⟼ B) (x))) = ⇝ ((m \in Z ⟼ B))$
114	1 14 60	nf3an	$⊢ Ⅎ m (φ \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} A)$
115		simp2	$⊢ (φ \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} A) \to n \in Z$
116	115 62	syl	$⊢ (φ \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} A) \to n \in ℤ$
117	65	a1i	$⊢ (φ \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} A) \to Z \in V$
118	5 115	uzssd2	$⊢ (φ \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} A) \to ℤ_{\geq n} \subseteq Z$
119		fvexd	$⊢ ((φ \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} A) \land m \in ℤ_{\geq n}) \to (x \in A ⟼ B) (x) \in V$
120	70	3ad2antl3	$⊢ ((φ \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} A) \land m \in ℤ_{\geq n}) \to x \in A$
121		simpl1	$⊢ ((φ \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} A) \land m \in ℤ_{\geq n}) \to φ$
122	115 16	sylan	$⊢ ((φ \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} A) \land m \in ℤ_{\geq n}) \to m \in Z$
123	121 122 120 7	syl3anc	$⊢ ((φ \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} A) \land m \in ℤ_{\geq n}) \to B \in W$
124	120 123 75	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$
125	114 116 64 117 117 118 118 119 124	climfveqmpt3	$⊢ (φ \land n \in Z \land x \in ⋂_{m \in ℤ_{\geq n}} A) \to ⇝ ((m \in Z ⟼ (x \in A ⟼ B) (x))) = ⇝ ((m \in Z ⟼ B))$
126	125	3exp	$⊢ φ \to (n \in Z \to (x \in ⋂_{m \in ℤ_{\geq n}} A \to ⇝ ((m \in Z ⟼ (x \in A ⟼ B) (x))) = ⇝ ((m \in Z ⟼ B))))$
127	126	adantr	$⊢ (φ \land x \in D) \to (n \in Z \to (x \in ⋂_{m \in ℤ_{\geq n}} A \to ⇝ ((m \in Z ⟼ (x \in A ⟼ B) (x))) = ⇝ ((m \in Z ⟼ B))))$
128	112 113 127	rexlimd	$⊢ (φ \land x \in D) \to (\exists n \in Z x \in ⋂_{m \in ℤ_{\geq n}} A \to ⇝ ((m \in Z ⟼ (x \in A ⟼ B) (x))) = ⇝ ((m \in Z ⟼ B)))$
129	106 128	mpd	$⊢ (φ \land x \in D) \to ⇝ ((m \in Z ⟼ (x \in A ⟼ B) (x))) = ⇝ ((m \in Z ⟼ B))$
130	129	eqcomd	$⊢ (φ \land x \in D) \to ⇝ ((m \in Z ⟼ B)) = ⇝ ((m \in Z ⟼ (x \in A ⟼ B) (x)))$
131	2 101 130	mpteq12da	$⊢ φ \to (x \in D ⟼ ⇝ ((m \in Z ⟼ B))) = (x \in \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom (x \in A ⟼ B) \| (m \in Z ⟼ (x \in A ⟼ B) (x)) \in dom ⇝\} ⟼ ⇝ ((m \in Z ⟼ (x \in A ⟼ B) (x))))$
132	41	eqcomd	$⊢ (φ \land m \in Z) \to (m \in Z ⟼ (x \in A ⟼ B)) (m) = (x \in A ⟼ B)$
133	132	fveq1d	$⊢ (φ \land m \in Z) \to (m \in Z ⟼ (x \in A ⟼ B)) (m) (x) = (x \in A ⟼ B) (x)$
134	1 133	mpteq2da	$⊢ φ \to (m \in Z ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x)) = (m \in Z ⟼ (x \in A ⟼ B) (x))$
135	134	eqcomd	$⊢ φ \to (m \in Z ⟼ (x \in A ⟼ B) (x)) = (m \in Z ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x))$
136	135	eleq1d	$⊢ φ \to ((m \in Z ⟼ (x \in A ⟼ B) (x)) \in dom ⇝ \leftrightarrow (m \in Z ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x)) \in dom ⇝)$
137	2 45 136	rabbida2	$⊢ φ \to \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom (x \in A ⟼ B) \| (m \in Z ⟼ (x \in A ⟼ B) (x)) \in dom ⇝\} = \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom (m \in Z ⟼ (x \in A ⟼ B)) (m) \| (m \in Z ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x)) \in dom ⇝\}$
138	133	eqcomd	$⊢ (φ \land m \in Z) \to (x \in A ⟼ B) (x) = (m \in Z ⟼ (x \in A ⟼ B)) (m) (x)$
139	1 138	mpteq2da	$⊢ φ \to (m \in Z ⟼ (x \in A ⟼ B) (x)) = (m \in Z ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x))$
140	139	fveq2d	$⊢ φ \to ⇝ ((m \in Z ⟼ (x \in A ⟼ B) (x))) = ⇝ ((m \in Z ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x)))$
141	2 137 140	mpteq12df	$⊢ φ \to (x \in \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom (x \in A ⟼ B) \| (m \in Z ⟼ (x \in A ⟼ B) (x)) \in dom ⇝\} ⟼ ⇝ ((m \in Z ⟼ (x \in A ⟼ B) (x)))) = (x \in \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom (m \in Z ⟼ (x \in A ⟼ B)) (m) \| (m \in Z ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x)) \in dom ⇝\} ⟼ ⇝ ((m \in Z ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x))))$
142	12 131 141	3eqtrd	$⊢ φ \to G = (x \in \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom (m \in Z ⟼ (x \in A ⟼ B)) (m) \| (m \in Z ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x)) \in dom ⇝\} ⟼ ⇝ ((m \in Z ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x))))$
143		nfmpt1	$⊢ \underline{Ⅎ} m (m \in Z ⟼ (x \in A ⟼ B))$
144		nfcv	$⊢ \underline{Ⅎ} x Z$
145		nfmpt1	$⊢ \underline{Ⅎ} x (x \in A ⟼ B)$
146	144 145	nfmpt	$⊢ \underline{Ⅎ} x (m \in Z ⟼ (x \in A ⟼ B))$
147	1 9 21	fmptdf	$⊢ φ \to (m \in Z ⟼ (x \in A ⟼ B)) : Z ⟶ SMblFn (S)$
148		eqid	$⊢ \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom (m \in Z ⟼ (x \in A ⟼ B)) (m) \| (m \in Z ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x)) \in dom ⇝\} = \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom (m \in Z ⟼ (x \in A ⟼ B)) (m) \| (m \in Z ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x)) \in dom ⇝\}$
149		eqid	$⊢ (x \in \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom (m \in Z ⟼ (x \in A ⟼ B)) (m) \| (m \in Z ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x)) \in dom ⇝\} ⟼ ⇝ ((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) \| (m \in Z ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x)) \in dom ⇝\} ⟼ ⇝ ((m \in Z ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x))))$
150	143 146 4 5 8 147 148 149	smflim2	$⊢ φ \to (x \in \{x \in ⋃_{n \in Z} ⋂_{m \in ℤ_{\geq n}} dom (m \in Z ⟼ (x \in A ⟼ B)) (m) \| (m \in Z ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x)) \in dom ⇝\} ⟼ ⇝ ((m \in Z ⟼ (m \in Z ⟼ (x \in A ⟼ B)) (m) (x)))) \in SMblFn (S)$
151	142 150	eqeltrd	$⊢ φ \to G \in SMblFn (S)$

Metamath Proof Explorer

Theorem smflimmpt

Proof