mbfinf

Description: The infimum of a sequence of measurable, real-valued functions is measurable. (Contributed by Mario Carneiro, 7-Sep-2014) (Revised by AV, 13-Sep-2020)

	Ref	Expression
Hypotheses	mbfinf.1	$⊢ Z = ℤ_{\geq M}$
	mbfinf.2	$⊢ G = (x \in A ⟼ sup (ran (n \in Z ⟼ B) ℝ <))$
	mbfinf.3	$⊢ φ \to M \in ℤ$
	mbfinf.4	$⊢ (φ \land n \in Z) \to (x \in A ⟼ B) \in MblFn$
	mbfinf.5	$⊢ (φ \land (n \in Z \land x \in A)) \to B \in ℝ$
	mbfinf.6	$⊢ (φ \land x \in A) \to \exists y \in ℝ \forall n \in Z y \leq B$
Assertion	mbfinf	$⊢ φ \to G \in MblFn$

Proof

Step	Hyp	Ref	Expression
1		mbfinf.1	$⊢ Z = ℤ_{\geq M}$
2		mbfinf.2	$⊢ G = (x \in A ⟼ sup (ran (n \in Z ⟼ B) ℝ <))$
3		mbfinf.3	$⊢ φ \to M \in ℤ$
4		mbfinf.4	$⊢ (φ \land n \in Z) \to (x \in A ⟼ B) \in MblFn$
5		mbfinf.5	$⊢ (φ \land (n \in Z \land x \in A)) \to B \in ℝ$
6		mbfinf.6	$⊢ (φ \land x \in A) \to \exists y \in ℝ \forall n \in Z y \leq B$
7	5	anass1rs	$⊢ ((φ \land x \in A) \land n \in Z) \to B \in ℝ$
8	7	fmpttd	$⊢ (φ \land x \in A) \to (n \in Z ⟼ B) : Z ⟶ ℝ$
9	8	frnd	$⊢ (φ \land x \in A) \to ran (n \in Z ⟼ B) \subseteq ℝ$
10		uzid	$⊢ M \in ℤ \to M \in ℤ_{\geq M}$
11	3 10	syl	$⊢ φ \to M \in ℤ_{\geq M}$
12	11 1	eleqtrrdi	$⊢ φ \to M \in Z$
13	12	adantr	$⊢ (φ \land x \in A) \to M \in Z$
14		eqid	$⊢ (n \in Z ⟼ B) = (n \in Z ⟼ B)$
15	14 7	dmmptd	$⊢ (φ \land x \in A) \to dom (n \in Z ⟼ B) = Z$
16	13 15	eleqtrrd	$⊢ (φ \land x \in A) \to M \in dom (n \in Z ⟼ B)$
17	16	ne0d	$⊢ (φ \land x \in A) \to dom (n \in Z ⟼ B) \neq \emptyset$
18		dm0rn0	$⊢ dom (n \in Z ⟼ B) = \emptyset \leftrightarrow ran (n \in Z ⟼ B) = \emptyset$
19	18	necon3bii	$⊢ dom (n \in Z ⟼ B) \neq \emptyset \leftrightarrow ran (n \in Z ⟼ B) \neq \emptyset$
20	17 19	sylib	$⊢ (φ \land x \in A) \to ran (n \in Z ⟼ B) \neq \emptyset$
21	8	ffnd	$⊢ (φ \land x \in A) \to (n \in Z ⟼ B) Fn Z$
22		breq2	$⊢ z = (n \in Z ⟼ B) (m) \to (y \leq z \leftrightarrow y \leq (n \in Z ⟼ B) (m))$
23	22	ralrn	$⊢ (n \in Z ⟼ B) Fn Z \to (\forall z \in ran (n \in Z ⟼ B) y \leq z \leftrightarrow \forall m \in Z y \leq (n \in Z ⟼ B) (m))$
24	21 23	syl	$⊢ (φ \land x \in A) \to (\forall z \in ran (n \in Z ⟼ B) y \leq z \leftrightarrow \forall m \in Z y \leq (n \in Z ⟼ B) (m))$
25		nfcv	$⊢ \underline{Ⅎ} n y$
26		nfcv	$⊢ \underline{Ⅎ} n \leq$
27		nffvmpt1	$⊢ \underline{Ⅎ} n (n \in Z ⟼ B) (m)$
28	25 26 27	nfbr	$⊢ Ⅎ n y \leq (n \in Z ⟼ B) (m)$
29		nfv	$⊢ Ⅎ m y \leq (n \in Z ⟼ B) (n)$
30		fveq2	$⊢ m = n \to (n \in Z ⟼ B) (m) = (n \in Z ⟼ B) (n)$
31	30	breq2d	$⊢ m = n \to (y \leq (n \in Z ⟼ B) (m) \leftrightarrow y \leq (n \in Z ⟼ B) (n))$
32	28 29 31	cbvralw	$⊢ \forall m \in Z y \leq (n \in Z ⟼ B) (m) \leftrightarrow \forall n \in Z y \leq (n \in Z ⟼ B) (n)$
33		simpr	$⊢ ((φ \land x \in A) \land n \in Z) \to n \in Z$
34	14	fvmpt2	$⊢ (n \in Z \land B \in ℝ) \to (n \in Z ⟼ B) (n) = B$
35	33 7 34	syl2anc	$⊢ ((φ \land x \in A) \land n \in Z) \to (n \in Z ⟼ B) (n) = B$
36	35	breq2d	$⊢ ((φ \land x \in A) \land n \in Z) \to (y \leq (n \in Z ⟼ B) (n) \leftrightarrow y \leq B)$
37	36	ralbidva	$⊢ (φ \land x \in A) \to (\forall n \in Z y \leq (n \in Z ⟼ B) (n) \leftrightarrow \forall n \in Z y \leq B)$
38	32 37	syl5bb	$⊢ (φ \land x \in A) \to (\forall m \in Z y \leq (n \in Z ⟼ B) (m) \leftrightarrow \forall n \in Z y \leq B)$
39	24 38	bitrd	$⊢ (φ \land x \in A) \to (\forall z \in ran (n \in Z ⟼ B) y \leq z \leftrightarrow \forall n \in Z y \leq B)$
40	39	rexbidv	$⊢ (φ \land x \in A) \to (\exists y \in ℝ \forall z \in ran (n \in Z ⟼ B) y \leq z \leftrightarrow \exists y \in ℝ \forall n \in Z y \leq B)$
41	6 40	mpbird	$⊢ (φ \land x \in A) \to \exists y \in ℝ \forall z \in ran (n \in Z ⟼ B) y \leq z$
42		infrenegsup	$⊢ (ran (n \in Z ⟼ B) \subseteq ℝ \land ran (n \in Z ⟼ B) \neq \emptyset \land \exists y \in ℝ \forall z \in ran (n \in Z ⟼ B) y \leq z) \to sup (ran (n \in Z ⟼ B) ℝ <) = - sup (\{r \in ℝ \| - r \in ran (n \in Z ⟼ B)\} ℝ <)$
43	9 20 41 42	syl3anc	$⊢ (φ \land x \in A) \to sup (ran (n \in Z ⟼ B) ℝ <) = - sup (\{r \in ℝ \| - r \in ran (n \in Z ⟼ B)\} ℝ <)$
44		rabid	$⊢ r \in \{r \in ℝ \| - r \in ran (n \in Z ⟼ B)\} \leftrightarrow (r \in ℝ \land - r \in ran (n \in Z ⟼ B))$
45	7	recnd	$⊢ ((φ \land x \in A) \land n \in Z) \to B \in ℂ$
46	45	adantlr	$⊢ (((φ \land x \in A) \land r \in ℝ) \land n \in Z) \to B \in ℂ$
47		simplr	$⊢ (((φ \land x \in A) \land r \in ℝ) \land n \in Z) \to r \in ℝ$
48	47	recnd	$⊢ (((φ \land x \in A) \land r \in ℝ) \land n \in Z) \to r \in ℂ$
49		negcon2	$⊢ (B \in ℂ \land r \in ℂ) \to (B = - r \leftrightarrow r = - B)$
50	46 48 49	syl2anc	$⊢ (((φ \land x \in A) \land r \in ℝ) \land n \in Z) \to (B = - r \leftrightarrow r = - B)$
51		eqcom	$⊢ r = - B \leftrightarrow - B = r$
52	50 51	bitrdi	$⊢ (((φ \land x \in A) \land r \in ℝ) \land n \in Z) \to (B = - r \leftrightarrow - B = r)$
53	35	adantlr	$⊢ (((φ \land x \in A) \land r \in ℝ) \land n \in Z) \to (n \in Z ⟼ B) (n) = B$
54	53	eqeq1d	$⊢ (((φ \land x \in A) \land r \in ℝ) \land n \in Z) \to ((n \in Z ⟼ B) (n) = - r \leftrightarrow B = - r)$
55		negex	$⊢ - B \in V$
56		eqid	$⊢ (n \in Z ⟼ - B) = (n \in Z ⟼ - B)$
57	56	fvmpt2	$⊢ (n \in Z \land - B \in V) \to (n \in Z ⟼ - B) (n) = - B$
58	55 57	mpan2	$⊢ n \in Z \to (n \in Z ⟼ - B) (n) = - B$
59	58	adantl	$⊢ (((φ \land x \in A) \land r \in ℝ) \land n \in Z) \to (n \in Z ⟼ - B) (n) = - B$
60	59	eqeq1d	$⊢ (((φ \land x \in A) \land r \in ℝ) \land n \in Z) \to ((n \in Z ⟼ - B) (n) = r \leftrightarrow - B = r)$
61	52 54 60	3bitr4d	$⊢ (((φ \land x \in A) \land r \in ℝ) \land n \in Z) \to ((n \in Z ⟼ B) (n) = - r \leftrightarrow (n \in Z ⟼ - B) (n) = r)$
62	61	ralrimiva	$⊢ ((φ \land x \in A) \land r \in ℝ) \to \forall n \in Z ((n \in Z ⟼ B) (n) = - r \leftrightarrow (n \in Z ⟼ - B) (n) = r)$
63	27	nfeq1	$⊢ Ⅎ n (n \in Z ⟼ B) (m) = - r$
64		nffvmpt1	$⊢ \underline{Ⅎ} n (n \in Z ⟼ - B) (m)$
65	64	nfeq1	$⊢ Ⅎ n (n \in Z ⟼ - B) (m) = r$
66	63 65	nfbi	$⊢ Ⅎ n ((n \in Z ⟼ B) (m) = - r \leftrightarrow (n \in Z ⟼ - B) (m) = r)$
67		nfv	$⊢ Ⅎ m ((n \in Z ⟼ B) (n) = - r \leftrightarrow (n \in Z ⟼ - B) (n) = r)$
68		fveqeq2	$⊢ m = n \to ((n \in Z ⟼ B) (m) = - r \leftrightarrow (n \in Z ⟼ B) (n) = - r)$
69		fveqeq2	$⊢ m = n \to ((n \in Z ⟼ - B) (m) = r \leftrightarrow (n \in Z ⟼ - B) (n) = r)$
70	68 69	bibi12d	$⊢ m = n \to (((n \in Z ⟼ B) (m) = - r \leftrightarrow (n \in Z ⟼ - B) (m) = r) \leftrightarrow ((n \in Z ⟼ B) (n) = - r \leftrightarrow (n \in Z ⟼ - B) (n) = r))$
71	66 67 70	cbvralw	$⊢ \forall m \in Z ((n \in Z ⟼ B) (m) = - r \leftrightarrow (n \in Z ⟼ - B) (m) = r) \leftrightarrow \forall n \in Z ((n \in Z ⟼ B) (n) = - r \leftrightarrow (n \in Z ⟼ - B) (n) = r)$
72	62 71	sylibr	$⊢ ((φ \land x \in A) \land r \in ℝ) \to \forall m \in Z ((n \in Z ⟼ B) (m) = - r \leftrightarrow (n \in Z ⟼ - B) (m) = r)$
73	72	r19.21bi	$⊢ (((φ \land x \in A) \land r \in ℝ) \land m \in Z) \to ((n \in Z ⟼ B) (m) = - r \leftrightarrow (n \in Z ⟼ - B) (m) = r)$
74	73	rexbidva	$⊢ ((φ \land x \in A) \land r \in ℝ) \to (\exists m \in Z (n \in Z ⟼ B) (m) = - r \leftrightarrow \exists m \in Z (n \in Z ⟼ - B) (m) = r)$
75	21	adantr	$⊢ ((φ \land x \in A) \land r \in ℝ) \to (n \in Z ⟼ B) Fn Z$
76		fvelrnb	$⊢ (n \in Z ⟼ B) Fn Z \to (- r \in ran (n \in Z ⟼ B) \leftrightarrow \exists m \in Z (n \in Z ⟼ B) (m) = - r)$
77	75 76	syl	$⊢ ((φ \land x \in A) \land r \in ℝ) \to (- r \in ran (n \in Z ⟼ B) \leftrightarrow \exists m \in Z (n \in Z ⟼ B) (m) = - r)$
78	7	renegcld	$⊢ ((φ \land x \in A) \land n \in Z) \to - B \in ℝ$
79	78	fmpttd	$⊢ (φ \land x \in A) \to (n \in Z ⟼ - B) : Z ⟶ ℝ$
80	79	adantr	$⊢ ((φ \land x \in A) \land r \in ℝ) \to (n \in Z ⟼ - B) : Z ⟶ ℝ$
81	80	ffnd	$⊢ ((φ \land x \in A) \land r \in ℝ) \to (n \in Z ⟼ - B) Fn Z$
82		fvelrnb	$⊢ (n \in Z ⟼ - B) Fn Z \to (r \in ran (n \in Z ⟼ - B) \leftrightarrow \exists m \in Z (n \in Z ⟼ - B) (m) = r)$
83	81 82	syl	$⊢ ((φ \land x \in A) \land r \in ℝ) \to (r \in ran (n \in Z ⟼ - B) \leftrightarrow \exists m \in Z (n \in Z ⟼ - B) (m) = r)$
84	74 77 83	3bitr4d	$⊢ ((φ \land x \in A) \land r \in ℝ) \to (- r \in ran (n \in Z ⟼ B) \leftrightarrow r \in ran (n \in Z ⟼ - B))$
85	84	pm5.32da	$⊢ (φ \land x \in A) \to ((r \in ℝ \land - r \in ran (n \in Z ⟼ B)) \leftrightarrow (r \in ℝ \land r \in ran (n \in Z ⟼ - B)))$
86	79	frnd	$⊢ (φ \land x \in A) \to ran (n \in Z ⟼ - B) \subseteq ℝ$
87	86	sseld	$⊢ (φ \land x \in A) \to (r \in ran (n \in Z ⟼ - B) \to r \in ℝ)$
88	87	pm4.71rd	$⊢ (φ \land x \in A) \to (r \in ran (n \in Z ⟼ - B) \leftrightarrow (r \in ℝ \land r \in ran (n \in Z ⟼ - B)))$
89	85 88	bitr4d	$⊢ (φ \land x \in A) \to ((r \in ℝ \land - r \in ran (n \in Z ⟼ B)) \leftrightarrow r \in ran (n \in Z ⟼ - B))$
90	44 89	syl5bb	$⊢ (φ \land x \in A) \to (r \in \{r \in ℝ \| - r \in ran (n \in Z ⟼ B)\} \leftrightarrow r \in ran (n \in Z ⟼ - B))$
91	90	alrimiv	$⊢ (φ \land x \in A) \to \forall r (r \in \{r \in ℝ \| - r \in ran (n \in Z ⟼ B)\} \leftrightarrow r \in ran (n \in Z ⟼ - B))$
92		nfrab1	$⊢ \underline{Ⅎ} r \{r \in ℝ \| - r \in ran (n \in Z ⟼ B)\}$
93		nfcv	$⊢ \underline{Ⅎ} r ran (n \in Z ⟼ - B)$
94	92 93	cleqf	$⊢ \{r \in ℝ \| - r \in ran (n \in Z ⟼ B)\} = ran (n \in Z ⟼ - B) \leftrightarrow \forall r (r \in \{r \in ℝ \| - r \in ran (n \in Z ⟼ B)\} \leftrightarrow r \in ran (n \in Z ⟼ - B))$
95	91 94	sylibr	$⊢ (φ \land x \in A) \to \{r \in ℝ \| - r \in ran (n \in Z ⟼ B)\} = ran (n \in Z ⟼ - B)$
96	95	supeq1d	$⊢ (φ \land x \in A) \to sup (\{r \in ℝ \| - r \in ran (n \in Z ⟼ B)\} ℝ <) = sup (ran (n \in Z ⟼ - B) ℝ <)$
97	96	negeqd	$⊢ (φ \land x \in A) \to - sup (\{r \in ℝ \| - r \in ran (n \in Z ⟼ B)\} ℝ <) = - sup (ran (n \in Z ⟼ - B) ℝ <)$
98	43 97	eqtrd	$⊢ (φ \land x \in A) \to sup (ran (n \in Z ⟼ B) ℝ <) = - sup (ran (n \in Z ⟼ - B) ℝ <)$
99	98	mpteq2dva	$⊢ φ \to (x \in A ⟼ sup (ran (n \in Z ⟼ B) ℝ <)) = (x \in A ⟼ - sup (ran (n \in Z ⟼ - B) ℝ <))$
100	2 99	syl5eq	$⊢ φ \to G = (x \in A ⟼ - sup (ran (n \in Z ⟼ - B) ℝ <))$
101		ltso	$⊢ < Or ℝ$
102	101	supex	$⊢ sup (ran (n \in Z ⟼ - B) ℝ <) \in V$
103	102	a1i	$⊢ (φ \land x \in A) \to sup (ran (n \in Z ⟼ - B) ℝ <) \in V$
104		eqid	$⊢ (x \in A ⟼ sup (ran (n \in Z ⟼ - B) ℝ <)) = (x \in A ⟼ sup (ran (n \in Z ⟼ - B) ℝ <))$
105	5	anassrs	$⊢ ((φ \land n \in Z) \land x \in A) \to B \in ℝ$
106	105 4	mbfneg	$⊢ (φ \land n \in Z) \to (x \in A ⟼ - B) \in MblFn$
107	5	renegcld	$⊢ (φ \land (n \in Z \land x \in A)) \to - B \in ℝ$
108		renegcl	$⊢ y \in ℝ \to - y \in ℝ$
109	108	ad2antrl	$⊢ ((φ \land x \in A) \land (y \in ℝ \land \forall n \in Z y \leq B)) \to - y \in ℝ$
110		simplr	$⊢ (((φ \land x \in A) \land y \in ℝ) \land n \in Z) \to y \in ℝ$
111	7	adantlr	$⊢ (((φ \land x \in A) \land y \in ℝ) \land n \in Z) \to B \in ℝ$
112	110 111	lenegd	$⊢ (((φ \land x \in A) \land y \in ℝ) \land n \in Z) \to (y \leq B \leftrightarrow - B \leq - y)$
113	112	ralbidva	$⊢ ((φ \land x \in A) \land y \in ℝ) \to (\forall n \in Z y \leq B \leftrightarrow \forall n \in Z - B \leq - y)$
114	113	biimpd	$⊢ ((φ \land x \in A) \land y \in ℝ) \to (\forall n \in Z y \leq B \to \forall n \in Z - B \leq - y)$
115	114	impr	$⊢ ((φ \land x \in A) \land (y \in ℝ \land \forall n \in Z y \leq B)) \to \forall n \in Z - B \leq - y$
116		brralrspcev	$⊢ (- y \in ℝ \land \forall n \in Z - B \leq - y) \to \exists z \in ℝ \forall n \in Z - B \leq z$
117	109 115 116	syl2anc	$⊢ ((φ \land x \in A) \land (y \in ℝ \land \forall n \in Z y \leq B)) \to \exists z \in ℝ \forall n \in Z - B \leq z$
118	6 117	rexlimddv	$⊢ (φ \land x \in A) \to \exists z \in ℝ \forall n \in Z - B \leq z$
119	1 104 3 106 107 118	mbfsup	$⊢ φ \to (x \in A ⟼ sup (ran (n \in Z ⟼ - B) ℝ <)) \in MblFn$
120	103 119	mbfneg	$⊢ φ \to (x \in A ⟼ - sup (ran (n \in Z ⟼ - B) ℝ <)) \in MblFn$
121	100 120	eqeltrd	$⊢ φ \to G \in MblFn$

Metamath Proof Explorer

Theorem mbfinf

Proof