smfsupmpt

Description: The supremum of a countable set of sigma-measurable functions is sigma-measurable. Proposition 121F (b) of Fremlin1 p. 38 . (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	smfsupmpt.n	$⊢ Ⅎ n φ$
	smfsupmpt.x	$⊢ Ⅎ x φ$
	smfsupmpt.y	$⊢ Ⅎ y φ$
	smfsupmpt.m	$⊢ φ \to M \in ℤ$
	smfsupmpt.z	$⊢ Z = ℤ_{\geq M}$
	smfsupmpt.s	$⊢ φ \to S \in SAlg$
	smfsupmpt.b	$⊢ (φ \land n \in Z \land x \in A) \to B \in V$
	smfsupmpt.f	$⊢ (φ \land n \in Z) \to (x \in A ⟼ B) \in SMblFn (S)$
	smfsupmpt.d	$⊢ D = \{x \in ⋂_{n \in Z} A \| \exists y \in ℝ \forall n \in Z B \leq y\}$
	smfsupmpt.g	$⊢ G = (x \in D ⟼ sup (ran (n \in Z ⟼ B) ℝ <))$
Assertion	smfsupmpt	$⊢ φ \to G \in SMblFn (S)$

Proof

Step	Hyp	Ref	Expression
1		smfsupmpt.n	$⊢ Ⅎ n φ$
2		smfsupmpt.x	$⊢ Ⅎ x φ$
3		smfsupmpt.y	$⊢ Ⅎ y φ$
4		smfsupmpt.m	$⊢ φ \to M \in ℤ$
5		smfsupmpt.z	$⊢ Z = ℤ_{\geq M}$
6		smfsupmpt.s	$⊢ φ \to S \in SAlg$
7		smfsupmpt.b	$⊢ (φ \land n \in Z \land x \in A) \to B \in V$
8		smfsupmpt.f	$⊢ (φ \land n \in Z) \to (x \in A ⟼ B) \in SMblFn (S)$
9		smfsupmpt.d	$⊢ D = \{x \in ⋂_{n \in Z} A \| \exists y \in ℝ \forall n \in Z B \leq y\}$
10		smfsupmpt.g	$⊢ G = (x \in D ⟼ sup (ran (n \in Z ⟼ B) ℝ <))$
11		eqidd	$⊢ φ \to (n \in Z ⟼ (x \in A ⟼ B)) = (n \in Z ⟼ (x \in A ⟼ B))$
12	11 8	fvmpt2d	$⊢ (φ \land n \in Z) \to (n \in Z ⟼ (x \in A ⟼ B)) (n) = (x \in A ⟼ B)$
13	12	dmeqd	$⊢ (φ \land n \in Z) \to dom (n \in Z ⟼ (x \in A ⟼ B)) (n) = dom (x \in A ⟼ B)$
14		nfcv	$⊢ \underline{Ⅎ} x Z$
15	14	nfcri	$⊢ Ⅎ x n \in Z$
16	2 15	nfan	$⊢ Ⅎ x (φ \land n \in Z)$
17		eqid	$⊢ (x \in A ⟼ B) = (x \in A ⟼ B)$
18	7	3expa	$⊢ ((φ \land n \in Z) \land x \in A) \to B \in V$
19	16 17 18	dmmptdf	$⊢ (φ \land n \in Z) \to dom (x \in A ⟼ B) = A$
20	13 19	eqtr2d	$⊢ (φ \land n \in Z) \to A = dom (n \in Z ⟼ (x \in A ⟼ B)) (n)$
21	1 20	iineq2d	$⊢ φ \to ⋂_{n \in Z} A = ⋂_{n \in Z} dom (n \in Z ⟼ (x \in A ⟼ B)) (n)$
22		nfcv	$⊢ \underline{Ⅎ} x ⋂_{n \in Z} A$
23		nfmpt1	$⊢ \underline{Ⅎ} x (x \in A ⟼ B)$
24	14 23	nfmpt	$⊢ \underline{Ⅎ} x (n \in Z ⟼ (x \in A ⟼ B))$
25		nfcv	$⊢ \underline{Ⅎ} x n$
26	24 25	nffv	$⊢ \underline{Ⅎ} x (n \in Z ⟼ (x \in A ⟼ B)) (n)$
27	26	nfdm	$⊢ \underline{Ⅎ} x dom (n \in Z ⟼ (x \in A ⟼ B)) (n)$
28	14 27	nfiin	$⊢ \underline{Ⅎ} x ⋂_{n \in Z} dom (n \in Z ⟼ (x \in A ⟼ B)) (n)$
29	22 28	rabeqf	$⊢ ⋂_{n \in Z} A = ⋂_{n \in Z} dom (n \in Z ⟼ (x \in A ⟼ B)) (n) \to \{x \in ⋂_{n \in Z} A \| \exists y \in ℝ \forall n \in Z B \leq y\} = \{x \in ⋂_{n \in Z} dom (n \in Z ⟼ (x \in A ⟼ B)) (n) \| \exists y \in ℝ \forall n \in Z B \leq y\}$
30	21 29	syl	$⊢ φ \to \{x \in ⋂_{n \in Z} A \| \exists y \in ℝ \forall n \in Z B \leq y\} = \{x \in ⋂_{n \in Z} dom (n \in Z ⟼ (x \in A ⟼ B)) (n) \| \exists y \in ℝ \forall n \in Z B \leq y\}$
31		nfv	$⊢ Ⅎ y x \in ⋂_{n \in Z} dom (n \in Z ⟼ (x \in A ⟼ B)) (n)$
32	3 31	nfan	$⊢ Ⅎ y (φ \land x \in ⋂_{n \in Z} dom (n \in Z ⟼ (x \in A ⟼ B)) (n))$
33		nfii1	$⊢ \underline{Ⅎ} n ⋂_{n \in Z} dom (n \in Z ⟼ (x \in A ⟼ B)) (n)$
34	33	nfcri	$⊢ Ⅎ n x \in ⋂_{n \in Z} dom (n \in Z ⟼ (x \in A ⟼ B)) (n)$
35	1 34	nfan	$⊢ Ⅎ n (φ \land x \in ⋂_{n \in Z} dom (n \in Z ⟼ (x \in A ⟼ B)) (n))$
36		simpll	$⊢ ((φ \land x \in ⋂_{n \in Z} dom (n \in Z ⟼ (x \in A ⟼ B)) (n)) \land n \in Z) \to φ$
37		simpr	$⊢ ((φ \land x \in ⋂_{n \in Z} dom (n \in Z ⟼ (x \in A ⟼ B)) (n)) \land n \in Z) \to n \in Z$
38		eliinid	$⊢ (x \in ⋂_{n \in Z} dom (n \in Z ⟼ (x \in A ⟼ B)) (n) \land n \in Z) \to x \in dom (n \in Z ⟼ (x \in A ⟼ B)) (n)$
39	38	adantll	$⊢ ((φ \land x \in ⋂_{n \in Z} dom (n \in Z ⟼ (x \in A ⟼ B)) (n)) \land n \in Z) \to x \in dom (n \in Z ⟼ (x \in A ⟼ B)) (n)$
40	13 19	eqtrd	$⊢ (φ \land n \in Z) \to dom (n \in Z ⟼ (x \in A ⟼ B)) (n) = A$
41	40	adantlr	$⊢ ((φ \land x \in ⋂_{n \in Z} dom (n \in Z ⟼ (x \in A ⟼ B)) (n)) \land n \in Z) \to dom (n \in Z ⟼ (x \in A ⟼ B)) (n) = A$
42	39 41	eleqtrd	$⊢ ((φ \land x \in ⋂_{n \in Z} dom (n \in Z ⟼ (x \in A ⟼ B)) (n)) \land n \in Z) \to x \in A$
43	12	fveq1d	$⊢ (φ \land n \in Z) \to (n \in Z ⟼ (x \in A ⟼ B)) (n) (x) = (x \in A ⟼ B) (x)$
44	43	3adant3	$⊢ (φ \land n \in Z \land x \in A) \to (n \in Z ⟼ (x \in A ⟼ B)) (n) (x) = (x \in A ⟼ B) (x)$
45		simp3	$⊢ (φ \land n \in Z \land x \in A) \to x \in A$
46		fvmpt4	$⊢ (x \in A \land B \in V) \to (x \in A ⟼ B) (x) = B$
47	45 7 46	syl2anc	$⊢ (φ \land n \in Z \land x \in A) \to (x \in A ⟼ B) (x) = B$
48	44 47	eqtr2d	$⊢ (φ \land n \in Z \land x \in A) \to B = (n \in Z ⟼ (x \in A ⟼ B)) (n) (x)$
49	48	breq1d	$⊢ (φ \land n \in Z \land x \in A) \to (B \leq y \leftrightarrow (n \in Z ⟼ (x \in A ⟼ B)) (n) (x) \leq y)$
50	36 37 42 49	syl3anc	$⊢ ((φ \land x \in ⋂_{n \in Z} dom (n \in Z ⟼ (x \in A ⟼ B)) (n)) \land n \in Z) \to (B \leq y \leftrightarrow (n \in Z ⟼ (x \in A ⟼ B)) (n) (x) \leq y)$
51	35 50	ralbida	$⊢ (φ \land x \in ⋂_{n \in Z} dom (n \in Z ⟼ (x \in A ⟼ B)) (n)) \to (\forall n \in Z B \leq y \leftrightarrow \forall n \in Z (n \in Z ⟼ (x \in A ⟼ B)) (n) (x) \leq y)$
52	32 51	rexbid	$⊢ (φ \land x \in ⋂_{n \in Z} dom (n \in Z ⟼ (x \in A ⟼ B)) (n)) \to (\exists y \in ℝ \forall n \in Z B \leq y \leftrightarrow \exists y \in ℝ \forall n \in Z (n \in Z ⟼ (x \in A ⟼ B)) (n) (x) \leq y)$
53	2 52	rabbida	$⊢ φ \to \{x \in ⋂_{n \in Z} dom (n \in Z ⟼ (x \in A ⟼ B)) (n) \| \exists y \in ℝ \forall n \in Z B \leq y\} = \{x \in ⋂_{n \in Z} dom (n \in Z ⟼ (x \in A ⟼ B)) (n) \| \exists y \in ℝ \forall n \in Z (n \in Z ⟼ (x \in A ⟼ B)) (n) (x) \leq y\}$
54	30 53	eqtrd	$⊢ φ \to \{x \in ⋂_{n \in Z} A \| \exists y \in ℝ \forall n \in Z B \leq y\} = \{x \in ⋂_{n \in Z} dom (n \in Z ⟼ (x \in A ⟼ B)) (n) \| \exists y \in ℝ \forall n \in Z (n \in Z ⟼ (x \in A ⟼ B)) (n) (x) \leq y\}$
55	9 54	eqtrid	$⊢ φ \to D = \{x \in ⋂_{n \in Z} dom (n \in Z ⟼ (x \in A ⟼ B)) (n) \| \exists y \in ℝ \forall n \in Z (n \in Z ⟼ (x \in A ⟼ B)) (n) (x) \leq y\}$
56		nfcv	$⊢ \underline{Ⅎ} n ℝ$
57		nfra1	$⊢ Ⅎ n \forall n \in Z B \leq y$
58	56 57	nfrexw	$⊢ Ⅎ n \exists y \in ℝ \forall n \in Z B \leq y$
59		nfii1	$⊢ \underline{Ⅎ} n ⋂_{n \in Z} A$
60	58 59	nfrabw	$⊢ \underline{Ⅎ} n \{x \in ⋂_{n \in Z} A \| \exists y \in ℝ \forall n \in Z B \leq y\}$
61	9 60	nfcxfr	$⊢ \underline{Ⅎ} n D$
62	61	nfcri	$⊢ Ⅎ n x \in D$
63	1 62	nfan	$⊢ Ⅎ n (φ \land x \in D)$
64		simpll	$⊢ ((φ \land x \in D) \land n \in Z) \to φ$
65		simpr	$⊢ ((φ \land x \in D) \land n \in Z) \to n \in Z$
66		rabidim1	$⊢ x \in \{x \in ⋂_{n \in Z} A \| \exists y \in ℝ \forall n \in Z B \leq y\} \to x \in ⋂_{n \in Z} A$
67	66 9	eleq2s	$⊢ x \in D \to x \in ⋂_{n \in Z} A$
68		eliinid	$⊢ (x \in ⋂_{n \in Z} A \land n \in Z) \to x \in A$
69	67 68	sylan	$⊢ (x \in D \land n \in Z) \to x \in A$
70	69	adantll	$⊢ ((φ \land x \in D) \land n \in Z) \to x \in A$
71	64 65 70 48	syl3anc	$⊢ ((φ \land x \in D) \land n \in Z) \to B = (n \in Z ⟼ (x \in A ⟼ B)) (n) (x)$
72	63 71	mpteq2da	$⊢ (φ \land x \in D) \to (n \in Z ⟼ B) = (n \in Z ⟼ (n \in Z ⟼ (x \in A ⟼ B)) (n) (x))$
73	72	rneqd	$⊢ (φ \land x \in D) \to ran (n \in Z ⟼ B) = ran (n \in Z ⟼ (n \in Z ⟼ (x \in A ⟼ B)) (n) (x))$
74	73	supeq1d	$⊢ (φ \land x \in D) \to sup (ran (n \in Z ⟼ B) ℝ <) = sup (ran (n \in Z ⟼ (n \in Z ⟼ (x \in A ⟼ B)) (n) (x)) ℝ <)$
75	2 55 74	mpteq12da	$⊢ φ \to (x \in D ⟼ sup (ran (n \in Z ⟼ B) ℝ <)) = (x \in \{x \in ⋂_{n \in Z} dom (n \in Z ⟼ (x \in A ⟼ B)) (n) \| \exists y \in ℝ \forall n \in Z (n \in Z ⟼ (x \in A ⟼ B)) (n) (x) \leq y\} ⟼ sup (ran (n \in Z ⟼ (n \in Z ⟼ (x \in A ⟼ B)) (n) (x)) ℝ <))$
76	10 75	eqtrid	$⊢ φ \to G = (x \in \{x \in ⋂_{n \in Z} dom (n \in Z ⟼ (x \in A ⟼ B)) (n) \| \exists y \in ℝ \forall n \in Z (n \in Z ⟼ (x \in A ⟼ B)) (n) (x) \leq y\} ⟼ sup (ran (n \in Z ⟼ (n \in Z ⟼ (x \in A ⟼ B)) (n) (x)) ℝ <))$
77		nfmpt1	$⊢ \underline{Ⅎ} n (n \in Z ⟼ (x \in A ⟼ B))$
78	1 8	fmptd2f	$⊢ φ \to (n \in Z ⟼ (x \in A ⟼ B)) : Z ⟶ SMblFn (S)$
79		eqid	$⊢ \{x \in ⋂_{n \in Z} dom (n \in Z ⟼ (x \in A ⟼ B)) (n) \| \exists y \in ℝ \forall n \in Z (n \in Z ⟼ (x \in A ⟼ B)) (n) (x) \leq y\} = \{x \in ⋂_{n \in Z} dom (n \in Z ⟼ (x \in A ⟼ B)) (n) \| \exists y \in ℝ \forall n \in Z (n \in Z ⟼ (x \in A ⟼ B)) (n) (x) \leq y\}$
80		eqid	$⊢ (x \in \{x \in ⋂_{n \in Z} dom (n \in Z ⟼ (x \in A ⟼ B)) (n) \| \exists y \in ℝ \forall n \in Z (n \in Z ⟼ (x \in A ⟼ B)) (n) (x) \leq y\} ⟼ sup (ran (n \in Z ⟼ (n \in Z ⟼ (x \in A ⟼ B)) (n) (x)) ℝ <)) = (x \in \{x \in ⋂_{n \in Z} dom (n \in Z ⟼ (x \in A ⟼ B)) (n) \| \exists y \in ℝ \forall n \in Z (n \in Z ⟼ (x \in A ⟼ B)) (n) (x) \leq y\} ⟼ sup (ran (n \in Z ⟼ (n \in Z ⟼ (x \in A ⟼ B)) (n) (x)) ℝ <))$
81	77 24 4 5 6 78 79 80	smfsup	$⊢ φ \to (x \in \{x \in ⋂_{n \in Z} dom (n \in Z ⟼ (x \in A ⟼ B)) (n) \| \exists y \in ℝ \forall n \in Z (n \in Z ⟼ (x \in A ⟼ B)) (n) (x) \leq y\} ⟼ sup (ran (n \in Z ⟼ (n \in Z ⟼ (x \in A ⟼ B)) (n) (x)) ℝ <)) \in SMblFn (S)$
82	76 81	eqeltrd	$⊢ φ \to G \in SMblFn (S)$

Metamath Proof Explorer

Theorem smfsupmpt

Proof