smfinfmpt

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

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

Proof

Step	Hyp	Ref	Expression
1		smfinfmpt.n	$⊢ Ⅎ n φ$
2		smfinfmpt.x	$⊢ Ⅎ x φ$
3		smfinfmpt.y	$⊢ Ⅎ y φ$
4		smfinfmpt.m	$⊢ φ \to M \in ℤ$
5		smfinfmpt.z	$⊢ Z = ℤ_{\geq M}$
6		smfinfmpt.s	$⊢ φ \to S \in SAlg$
7		smfinfmpt.b	$⊢ (φ \land n \in Z \land x \in A) \to B \in V$
8		smfinfmpt.f	$⊢ (φ \land n \in Z) \to (x \in A ⟼ B) \in SMblFn (S)$
9		smfinfmpt.d	$⊢ D = \{x \in ⋂_{n \in Z} A \| \exists y \in ℝ \forall n \in Z y \leq B\}$
10		smfinfmpt.g	$⊢ G = (x \in D ⟼ sup (ran (n \in Z ⟼ B) ℝ <))$
11	10	a1i	$⊢ φ \to G = (x \in D ⟼ sup (ran (n \in Z ⟼ B) ℝ <))$
12	9	a1i	$⊢ φ \to D = \{x \in ⋂_{n \in Z} A \| \exists y \in ℝ \forall n \in Z y \leq B\}$
13		eqidd	$⊢ φ \to (n \in Z ⟼ (x \in A ⟼ B)) = (n \in Z ⟼ (x \in A ⟼ B))$
14	13 8	fvmpt2d	$⊢ (φ \land n \in Z) \to (n \in Z ⟼ (x \in A ⟼ B)) (n) = (x \in A ⟼ B)$
15	14	dmeqd	$⊢ (φ \land n \in Z) \to dom (n \in Z ⟼ (x \in A ⟼ B)) (n) = dom (x \in A ⟼ B)$
16		nfcv	$⊢ \underline{Ⅎ} x n$
17		nfcv	$⊢ \underline{Ⅎ} x Z$
18	16 17	nfel	$⊢ Ⅎ x n \in Z$
19	2 18	nfan	$⊢ Ⅎ x (φ \land n \in Z)$
20		eqid	$⊢ (x \in A ⟼ B) = (x \in A ⟼ B)$
21	6	adantr	$⊢ (φ \land n \in Z) \to S \in SAlg$
22	7	3expa	$⊢ ((φ \land n \in Z) \land x \in A) \to B \in V$
23	19 21 22 8	smffmpt	$⊢ (φ \land n \in Z) \to (x \in A ⟼ B) : A ⟶ ℝ$
24	23	fvmptelrn	$⊢ ((φ \land n \in Z) \land x \in A) \to B \in ℝ$
25	19 20 24	dmmptdf	$⊢ (φ \land n \in Z) \to dom (x \in A ⟼ B) = A$
26		eqidd	$⊢ (φ \land n \in Z) \to A = A$
27	15 25 26	3eqtrrd	$⊢ (φ \land n \in Z) \to A = dom (n \in Z ⟼ (x \in A ⟼ B)) (n)$
28	1 27	iineq2d	$⊢ φ \to ⋂_{n \in Z} A = ⋂_{n \in Z} dom (n \in Z ⟼ (x \in A ⟼ B)) (n)$
29		nfcv	$⊢ \underline{Ⅎ} x ⋂_{n \in Z} A$
30		nfmpt1	$⊢ \underline{Ⅎ} x (x \in A ⟼ B)$
31	17 30	nfmpt	$⊢ \underline{Ⅎ} x (n \in Z ⟼ (x \in A ⟼ B))$
32	31 16	nffv	$⊢ \underline{Ⅎ} x (n \in Z ⟼ (x \in A ⟼ B)) (n)$
33	32	nfdm	$⊢ \underline{Ⅎ} x dom (n \in Z ⟼ (x \in A ⟼ B)) (n)$
34	17 33	nfiin	$⊢ \underline{Ⅎ} x ⋂_{n \in Z} dom (n \in Z ⟼ (x \in A ⟼ B)) (n)$
35	29 34	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 y \leq B\} = \{x \in ⋂_{n \in Z} dom (n \in Z ⟼ (x \in A ⟼ B)) (n) \| \exists y \in ℝ \forall n \in Z y \leq B\}$
36	28 35	syl	$⊢ φ \to \{x \in ⋂_{n \in Z} A \| \exists y \in ℝ \forall n \in Z y \leq B\} = \{x \in ⋂_{n \in Z} dom (n \in Z ⟼ (x \in A ⟼ B)) (n) \| \exists y \in ℝ \forall n \in Z y \leq B\}$
37		nfv	$⊢ Ⅎ y x \in ⋂_{n \in Z} dom (n \in Z ⟼ (x \in A ⟼ B)) (n)$
38	3 37	nfan	$⊢ Ⅎ y (φ \land x \in ⋂_{n \in Z} dom (n \in Z ⟼ (x \in A ⟼ B)) (n))$
39		nfcv	$⊢ \underline{Ⅎ} n x$
40		nfii1	$⊢ \underline{Ⅎ} n ⋂_{n \in Z} dom (n \in Z ⟼ (x \in A ⟼ B)) (n)$
41	39 40	nfel	$⊢ Ⅎ n x \in ⋂_{n \in Z} dom (n \in Z ⟼ (x \in A ⟼ B)) (n)$
42	1 41	nfan	$⊢ Ⅎ n (φ \land x \in ⋂_{n \in Z} dom (n \in Z ⟼ (x \in A ⟼ B)) (n))$
43		simpll	$⊢ ((φ \land x \in ⋂_{n \in Z} dom (n \in Z ⟼ (x \in A ⟼ B)) (n)) \land n \in Z) \to φ$
44		simpr	$⊢ ((φ \land x \in ⋂_{n \in Z} dom (n \in Z ⟼ (x \in A ⟼ B)) (n)) \land n \in Z) \to n \in Z$
45		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)$
46	45	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)$
47	27	eqcomd	$⊢ (φ \land n \in Z) \to dom (n \in Z ⟼ (x \in A ⟼ B)) (n) = A$
48	47	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$
49	46 48	eleqtrd	$⊢ ((φ \land x \in ⋂_{n \in Z} dom (n \in Z ⟼ (x \in A ⟼ B)) (n)) \land n \in Z) \to x \in A$
50	14	fveq1d	$⊢ (φ \land n \in Z) \to (n \in Z ⟼ (x \in A ⟼ B)) (n) (x) = (x \in A ⟼ B) (x)$
51	50	3adant3	$⊢ (φ \land n \in Z \land x \in A) \to (n \in Z ⟼ (x \in A ⟼ B)) (n) (x) = (x \in A ⟼ B) (x)$
52		simp3	$⊢ (φ \land n \in Z \land x \in A) \to x \in A$
53	20	fvmpt2	$⊢ (x \in A \land B \in V) \to (x \in A ⟼ B) (x) = B$
54	52 7 53	syl2anc	$⊢ (φ \land n \in Z \land x \in A) \to (x \in A ⟼ B) (x) = B$
55	51 54	eqtr2d	$⊢ (φ \land n \in Z \land x \in A) \to B = (n \in Z ⟼ (x \in A ⟼ B)) (n) (x)$
56	55	breq2d	$⊢ (φ \land n \in Z \land x \in A) \to (y \leq B \leftrightarrow y \leq (n \in Z ⟼ (x \in A ⟼ B)) (n) (x))$
57	43 44 49 56	syl3anc	$⊢ ((φ \land x \in ⋂_{n \in Z} dom (n \in Z ⟼ (x \in A ⟼ B)) (n)) \land n \in Z) \to (y \leq B \leftrightarrow y \leq (n \in Z ⟼ (x \in A ⟼ B)) (n) (x))$
58	42 57	ralbida	$⊢ (φ \land x \in ⋂_{n \in Z} dom (n \in Z ⟼ (x \in A ⟼ B)) (n)) \to (\forall n \in Z y \leq B \leftrightarrow \forall n \in Z y \leq (n \in Z ⟼ (x \in A ⟼ B)) (n) (x))$
59	38 58	rexbid	$⊢ (φ \land x \in ⋂_{n \in Z} dom (n \in Z ⟼ (x \in A ⟼ B)) (n)) \to (\exists y \in ℝ \forall n \in Z y \leq B \leftrightarrow \exists y \in ℝ \forall n \in Z y \leq (n \in Z ⟼ (x \in A ⟼ B)) (n) (x))$
60	2 59	rabbida	$⊢ φ \to \{x \in ⋂_{n \in Z} dom (n \in Z ⟼ (x \in A ⟼ B)) (n) \| \exists y \in ℝ \forall n \in Z y \leq B\} = \{x \in ⋂_{n \in Z} dom (n \in Z ⟼ (x \in A ⟼ B)) (n) \| \exists y \in ℝ \forall n \in Z y \leq (n \in Z ⟼ (x \in A ⟼ B)) (n) (x)\}$
61	36 60	eqtrd	$⊢ φ \to \{x \in ⋂_{n \in Z} A \| \exists y \in ℝ \forall n \in Z y \leq B\} = \{x \in ⋂_{n \in Z} dom (n \in Z ⟼ (x \in A ⟼ B)) (n) \| \exists y \in ℝ \forall n \in Z y \leq (n \in Z ⟼ (x \in A ⟼ B)) (n) (x)\}$
62	12 61	eqtrd	$⊢ φ \to D = \{x \in ⋂_{n \in Z} dom (n \in Z ⟼ (x \in A ⟼ B)) (n) \| \exists y \in ℝ \forall n \in Z y \leq (n \in Z ⟼ (x \in A ⟼ B)) (n) (x)\}$
63	2 62	alrimi	$⊢ φ \to \forall x D = \{x \in ⋂_{n \in Z} dom (n \in Z ⟼ (x \in A ⟼ B)) (n) \| \exists y \in ℝ \forall n \in Z y \leq (n \in Z ⟼ (x \in A ⟼ B)) (n) (x)\}$
64		nfcv	$⊢ \underline{Ⅎ} n ℝ$
65		nfra1	$⊢ Ⅎ n \forall n \in Z y \leq B$
66	64 65	nfrex	$⊢ Ⅎ n \exists y \in ℝ \forall n \in Z y \leq B$
67		nfii1	$⊢ \underline{Ⅎ} n ⋂_{n \in Z} A$
68	66 67	nfrabw	$⊢ \underline{Ⅎ} n \{x \in ⋂_{n \in Z} A \| \exists y \in ℝ \forall n \in Z y \leq B\}$
69	9 68	nfcxfr	$⊢ \underline{Ⅎ} n D$
70	39 69	nfel	$⊢ Ⅎ n x \in D$
71	1 70	nfan	$⊢ Ⅎ n (φ \land x \in D)$
72		simpll	$⊢ ((φ \land x \in D) \land n \in Z) \to φ$
73		simpr	$⊢ ((φ \land x \in D) \land n \in Z) \to n \in Z$
74	9	eleq2i	$⊢ x \in D \leftrightarrow x \in \{x \in ⋂_{n \in Z} A \| \exists y \in ℝ \forall n \in Z y \leq B\}$
75	74	biimpi	$⊢ x \in D \to x \in \{x \in ⋂_{n \in Z} A \| \exists y \in ℝ \forall n \in Z y \leq B\}$
76		rabidim1	$⊢ x \in \{x \in ⋂_{n \in Z} A \| \exists y \in ℝ \forall n \in Z y \leq B\} \to x \in ⋂_{n \in Z} A$
77	75 76	syl	$⊢ x \in D \to x \in ⋂_{n \in Z} A$
78	77	adantr	$⊢ (x \in D \land n \in Z) \to x \in ⋂_{n \in Z} A$
79		simpr	$⊢ (x \in D \land n \in Z) \to n \in Z$
80		eliinid	$⊢ (x \in ⋂_{n \in Z} A \land n \in Z) \to x \in A$
81	78 79 80	syl2anc	$⊢ (x \in D \land n \in Z) \to x \in A$
82	81	adantll	$⊢ ((φ \land x \in D) \land n \in Z) \to x \in A$
83	55	idi	$⊢ (φ \land n \in Z \land x \in A) \to B = (n \in Z ⟼ (x \in A ⟼ B)) (n) (x)$
84	72 73 82 83	syl3anc	$⊢ ((φ \land x \in D) \land n \in Z) \to B = (n \in Z ⟼ (x \in A ⟼ B)) (n) (x)$
85	71 84	mpteq2da	$⊢ (φ \land x \in D) \to (n \in Z ⟼ B) = (n \in Z ⟼ (n \in Z ⟼ (x \in A ⟼ B)) (n) (x))$
86	85	rneqd	$⊢ (φ \land x \in D) \to ran (n \in Z ⟼ B) = ran (n \in Z ⟼ (n \in Z ⟼ (x \in A ⟼ B)) (n) (x))$
87	86	infeq1d	$⊢ (φ \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)) ℝ <)$
88	87	ex	$⊢ φ \to (x \in D \to sup (ran (n \in Z ⟼ B) ℝ <) = sup (ran (n \in Z ⟼ (n \in Z ⟼ (x \in A ⟼ B)) (n) (x)) ℝ <))$
89	2 88	ralrimi	$⊢ φ \to \forall x \in D sup (ran (n \in Z ⟼ B) ℝ <) = sup (ran (n \in Z ⟼ (n \in Z ⟼ (x \in A ⟼ B)) (n) (x)) ℝ <)$
90		mpteq12f	$⊢ (\forall x D = \{x \in ⋂_{n \in Z} dom (n \in Z ⟼ (x \in A ⟼ B)) (n) \| \exists y \in ℝ \forall n \in Z y \leq (n \in Z ⟼ (x \in A ⟼ B)) (n) (x)\} \land \forall x \in D sup (ran (n \in Z ⟼ B) ℝ <) = sup (ran (n \in Z ⟼ (n \in Z ⟼ (x \in A ⟼ B)) (n) (x)) ℝ <)) \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 y \leq (n \in Z ⟼ (x \in A ⟼ B)) (n) (x)\} ⟼ sup (ran (n \in Z ⟼ (n \in Z ⟼ (x \in A ⟼ B)) (n) (x)) ℝ <))$
91	63 89 90	syl2anc	$⊢ φ \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 y \leq (n \in Z ⟼ (x \in A ⟼ B)) (n) (x)\} ⟼ sup (ran (n \in Z ⟼ (n \in Z ⟼ (x \in A ⟼ B)) (n) (x)) ℝ <))$
92	11 91	eqtrd	$⊢ φ \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 y \leq (n \in Z ⟼ (x \in A ⟼ B)) (n) (x)\} ⟼ sup (ran (n \in Z ⟼ (n \in Z ⟼ (x \in A ⟼ B)) (n) (x)) ℝ <))$
93		nfmpt1	$⊢ \underline{Ⅎ} n (n \in Z ⟼ (x \in A ⟼ B))$
94		eqid	$⊢ (n \in Z ⟼ (x \in A ⟼ B)) = (n \in Z ⟼ (x \in A ⟼ B))$
95	1 8 94	fmptdf	$⊢ φ \to (n \in Z ⟼ (x \in A ⟼ B)) : Z ⟶ SMblFn (S)$
96		eqid	$⊢ \{x \in ⋂_{n \in Z} dom (n \in Z ⟼ (x \in A ⟼ B)) (n) \| \exists y \in ℝ \forall n \in Z y \leq (n \in Z ⟼ (x \in A ⟼ B)) (n) (x)\} = \{x \in ⋂_{n \in Z} dom (n \in Z ⟼ (x \in A ⟼ B)) (n) \| \exists y \in ℝ \forall n \in Z y \leq (n \in Z ⟼ (x \in A ⟼ B)) (n) (x)\}$
97		eqid	$⊢ (x \in \{x \in ⋂_{n \in Z} dom (n \in Z ⟼ (x \in A ⟼ B)) (n) \| \exists y \in ℝ \forall n \in Z y \leq (n \in Z ⟼ (x \in A ⟼ B)) (n) (x)\} ⟼ 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 y \leq (n \in Z ⟼ (x \in A ⟼ B)) (n) (x)\} ⟼ sup (ran (n \in Z ⟼ (n \in Z ⟼ (x \in A ⟼ B)) (n) (x)) ℝ <))$
98	93 31 4 5 6 95 96 97	smfinf	$⊢ φ \to (x \in \{x \in ⋂_{n \in Z} dom (n \in Z ⟼ (x \in A ⟼ B)) (n) \| \exists y \in ℝ \forall n \in Z y \leq (n \in Z ⟼ (x \in A ⟼ B)) (n) (x)\} ⟼ sup (ran (n \in Z ⟼ (n \in Z ⟼ (x \in A ⟼ B)) (n) (x)) ℝ <)) \in SMblFn (S)$
99	92 98	eqeltrd	$⊢ φ \to G \in SMblFn (S)$

Metamath Proof Explorer

Theorem smfinfmpt

Proof