mbfsup

Description: The supremum of a sequence of measurable, real-valued functions is measurable. Note that in this and related theorems, B ( n , x ) is a function of both n and x , since it is an n -indexed sequence of functions on x . (Contributed by Mario Carneiro, 14-Aug-2014) (Revised by Mario Carneiro, 7-Sep-2014)

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

Proof

Step	Hyp	Ref	Expression
1		mbfsup.1	$⊢ Z = ℤ_{\geq M}$
2		mbfsup.2	$⊢ G = (x \in A ⟼ sup (ran (n \in Z ⟼ B) ℝ <))$
3		mbfsup.3	$⊢ φ \to M \in ℤ$
4		mbfsup.4	$⊢ (φ \land n \in Z) \to (x \in A ⟼ B) \in MblFn$
5		mbfsup.5	$⊢ (φ \land (n \in Z \land x \in A)) \to B \in ℝ$
6		mbfsup.6	$⊢ (φ \land x \in A) \to \exists y \in ℝ \forall n \in Z B \leq y$
7	5	anassrs	$⊢ ((φ \land n \in Z) \land x \in A) \to B \in ℝ$
8	7	an32s	$⊢ ((φ \land x \in A) \land n \in Z) \to B \in ℝ$
9	8	fmpttd	$⊢ (φ \land x \in A) \to (n \in Z ⟼ B) : Z ⟶ ℝ$
10	9	frnd	$⊢ (φ \land x \in A) \to ran (n \in Z ⟼ B) \subseteq ℝ$
11		uzid	$⊢ M \in ℤ \to M \in ℤ_{\geq M}$
12	3 11	syl	$⊢ φ \to M \in ℤ_{\geq M}$
13	12 1	eleqtrrdi	$⊢ φ \to M \in Z$
14	13	adantr	$⊢ (φ \land x \in A) \to M \in Z$
15		eqid	$⊢ (n \in Z ⟼ B) = (n \in Z ⟼ B)$
16	15 8	dmmptd	$⊢ (φ \land x \in A) \to dom (n \in Z ⟼ B) = Z$
17	14 16	eleqtrrd	$⊢ (φ \land x \in A) \to M \in dom (n \in Z ⟼ B)$
18	17	ne0d	$⊢ (φ \land x \in A) \to dom (n \in Z ⟼ B) \neq \emptyset$
19		dm0rn0	$⊢ dom (n \in Z ⟼ B) = \emptyset \leftrightarrow ran (n \in Z ⟼ B) = \emptyset$
20	19	necon3bii	$⊢ dom (n \in Z ⟼ B) \neq \emptyset \leftrightarrow ran (n \in Z ⟼ B) \neq \emptyset$
21	18 20	sylib	$⊢ (φ \land x \in A) \to ran (n \in Z ⟼ B) \neq \emptyset$
22	9	ffnd	$⊢ (φ \land x \in A) \to (n \in Z ⟼ B) Fn Z$
23		breq1	$⊢ z = (n \in Z ⟼ B) (m) \to (z \leq y \leftrightarrow (n \in Z ⟼ B) (m) \leq y)$
24	23	ralrn	$⊢ (n \in Z ⟼ B) Fn Z \to (\forall z \in ran (n \in Z ⟼ B) z \leq y \leftrightarrow \forall m \in Z (n \in Z ⟼ B) (m) \leq y)$
25	22 24	syl	$⊢ (φ \land x \in A) \to (\forall z \in ran (n \in Z ⟼ B) z \leq y \leftrightarrow \forall m \in Z (n \in Z ⟼ B) (m) \leq y)$
26		nffvmpt1	$⊢ \underline{Ⅎ} n (n \in Z ⟼ B) (m)$
27		nfcv	$⊢ \underline{Ⅎ} n \leq$
28		nfcv	$⊢ \underline{Ⅎ} n y$
29	26 27 28	nfbr	$⊢ Ⅎ n (n \in Z ⟼ B) (m) \leq y$
30		nfv	$⊢ Ⅎ m (n \in Z ⟼ B) (n) \leq y$
31		fveq2	$⊢ m = n \to (n \in Z ⟼ B) (m) = (n \in Z ⟼ B) (n)$
32	31	breq1d	$⊢ m = n \to ((n \in Z ⟼ B) (m) \leq y \leftrightarrow (n \in Z ⟼ B) (n) \leq y)$
33	29 30 32	cbvralw	$⊢ \forall m \in Z (n \in Z ⟼ B) (m) \leq y \leftrightarrow \forall n \in Z (n \in Z ⟼ B) (n) \leq y$
34		simpr	$⊢ ((φ \land x \in A) \land n \in Z) \to n \in Z$
35	15	fvmpt2	$⊢ (n \in Z \land B \in ℝ) \to (n \in Z ⟼ B) (n) = B$
36	34 8 35	syl2anc	$⊢ ((φ \land x \in A) \land n \in Z) \to (n \in Z ⟼ B) (n) = B$
37	36	breq1d	$⊢ ((φ \land x \in A) \land n \in Z) \to ((n \in Z ⟼ B) (n) \leq y \leftrightarrow B \leq y)$
38	37	ralbidva	$⊢ (φ \land x \in A) \to (\forall n \in Z (n \in Z ⟼ B) (n) \leq y \leftrightarrow \forall n \in Z B \leq y)$
39	33 38	syl5bb	$⊢ (φ \land x \in A) \to (\forall m \in Z (n \in Z ⟼ B) (m) \leq y \leftrightarrow \forall n \in Z B \leq y)$
40	25 39	bitrd	$⊢ (φ \land x \in A) \to (\forall z \in ran (n \in Z ⟼ B) z \leq y \leftrightarrow \forall n \in Z B \leq y)$
41	40	rexbidv	$⊢ (φ \land x \in A) \to (\exists y \in ℝ \forall z \in ran (n \in Z ⟼ B) z \leq y \leftrightarrow \exists y \in ℝ \forall n \in Z B \leq y)$
42	6 41	mpbird	$⊢ (φ \land x \in A) \to \exists y \in ℝ \forall z \in ran (n \in Z ⟼ B) z \leq y$
43	10 21 42	suprcld	$⊢ (φ \land x \in A) \to sup (ran (n \in Z ⟼ B) ℝ <) \in ℝ$
44	43 2	fmptd	$⊢ φ \to G : A ⟶ ℝ$
45		simpr	$⊢ ((φ \land t \in ℝ) \land x \in A) \to x \in A$
46		ltso	$⊢ < Or ℝ$
47	46	supex	$⊢ sup (ran (n \in Z ⟼ B) ℝ <) \in V$
48	2	fvmpt2	$⊢ (x \in A \land sup (ran (n \in Z ⟼ B) ℝ <) \in V) \to G (x) = sup (ran (n \in Z ⟼ B) ℝ <)$
49	45 47 48	sylancl	$⊢ ((φ \land t \in ℝ) \land x \in A) \to G (x) = sup (ran (n \in Z ⟼ B) ℝ <)$
50	49	breq2d	$⊢ ((φ \land t \in ℝ) \land x \in A) \to (t < G (x) \leftrightarrow t < sup (ran (n \in Z ⟼ B) ℝ <))$
51	10 21 42	3jca	$⊢ (φ \land x \in A) \to (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) z \leq y)$
52	51	adantlr	$⊢ ((φ \land t \in ℝ) \land x \in A) \to (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) z \leq y)$
53		simplr	$⊢ ((φ \land t \in ℝ) \land x \in A) \to t \in ℝ$
54		suprlub	$⊢ ((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) z \leq y) \land t \in ℝ) \to (t < sup (ran (n \in Z ⟼ B) ℝ <) \leftrightarrow \exists z \in ran (n \in Z ⟼ B) t < z)$
55	52 53 54	syl2anc	$⊢ ((φ \land t \in ℝ) \land x \in A) \to (t < sup (ran (n \in Z ⟼ B) ℝ <) \leftrightarrow \exists z \in ran (n \in Z ⟼ B) t < z)$
56	22	adantlr	$⊢ ((φ \land t \in ℝ) \land x \in A) \to (n \in Z ⟼ B) Fn Z$
57		breq2	$⊢ z = (n \in Z ⟼ B) (m) \to (t < z \leftrightarrow t < (n \in Z ⟼ B) (m))$
58	57	rexrn	$⊢ (n \in Z ⟼ B) Fn Z \to (\exists z \in ran (n \in Z ⟼ B) t < z \leftrightarrow \exists m \in Z t < (n \in Z ⟼ B) (m))$
59	56 58	syl	$⊢ ((φ \land t \in ℝ) \land x \in A) \to (\exists z \in ran (n \in Z ⟼ B) t < z \leftrightarrow \exists m \in Z t < (n \in Z ⟼ B) (m))$
60		nfcv	$⊢ \underline{Ⅎ} n t$
61		nfcv	$⊢ \underline{Ⅎ} n <$
62	60 61 26	nfbr	$⊢ Ⅎ n t < (n \in Z ⟼ B) (m)$
63		nfv	$⊢ Ⅎ m t < (n \in Z ⟼ B) (n)$
64	31	breq2d	$⊢ m = n \to (t < (n \in Z ⟼ B) (m) \leftrightarrow t < (n \in Z ⟼ B) (n))$
65	62 63 64	cbvrexw	$⊢ \exists m \in Z t < (n \in Z ⟼ B) (m) \leftrightarrow \exists n \in Z t < (n \in Z ⟼ B) (n)$
66	15	fvmpt2i	$⊢ n \in Z \to (n \in Z ⟼ B) (n) = I (B)$
67		eqid	$⊢ (x \in A ⟼ B) = (x \in A ⟼ B)$
68	67	fvmpt2i	$⊢ x \in A \to (x \in A ⟼ B) (x) = I (B)$
69	68	adantl	$⊢ (φ \land x \in A) \to (x \in A ⟼ B) (x) = I (B)$
70	69	eqcomd	$⊢ (φ \land x \in A) \to I (B) = (x \in A ⟼ B) (x)$
71	66 70	sylan9eqr	$⊢ ((φ \land x \in A) \land n \in Z) \to (n \in Z ⟼ B) (n) = (x \in A ⟼ B) (x)$
72	71	breq2d	$⊢ ((φ \land x \in A) \land n \in Z) \to (t < (n \in Z ⟼ B) (n) \leftrightarrow t < (x \in A ⟼ B) (x))$
73	72	rexbidva	$⊢ (φ \land x \in A) \to (\exists n \in Z t < (n \in Z ⟼ B) (n) \leftrightarrow \exists n \in Z t < (x \in A ⟼ B) (x))$
74	73	adantlr	$⊢ ((φ \land t \in ℝ) \land x \in A) \to (\exists n \in Z t < (n \in Z ⟼ B) (n) \leftrightarrow \exists n \in Z t < (x \in A ⟼ B) (x))$
75	65 74	syl5bb	$⊢ ((φ \land t \in ℝ) \land x \in A) \to (\exists m \in Z t < (n \in Z ⟼ B) (m) \leftrightarrow \exists n \in Z t < (x \in A ⟼ B) (x))$
76	59 75	bitrd	$⊢ ((φ \land t \in ℝ) \land x \in A) \to (\exists z \in ran (n \in Z ⟼ B) t < z \leftrightarrow \exists n \in Z t < (x \in A ⟼ B) (x))$
77	50 55 76	3bitrd	$⊢ ((φ \land t \in ℝ) \land x \in A) \to (t < G (x) \leftrightarrow \exists n \in Z t < (x \in A ⟼ B) (x))$
78	77	ralrimiva	$⊢ (φ \land t \in ℝ) \to \forall x \in A (t < G (x) \leftrightarrow \exists n \in Z t < (x \in A ⟼ B) (x))$
79		nfv	$⊢ Ⅎ z (t < G (x) \leftrightarrow \exists n \in Z t < (x \in A ⟼ B) (x))$
80		nfcv	$⊢ \underline{Ⅎ} x t$
81		nfcv	$⊢ \underline{Ⅎ} x <$
82		nfmpt1	$⊢ \underline{Ⅎ} x (x \in A ⟼ sup (ran (n \in Z ⟼ B) ℝ <))$
83	2 82	nfcxfr	$⊢ \underline{Ⅎ} x G$
84		nfcv	$⊢ \underline{Ⅎ} x z$
85	83 84	nffv	$⊢ \underline{Ⅎ} x G (z)$
86	80 81 85	nfbr	$⊢ Ⅎ x t < G (z)$
87		nfcv	$⊢ \underline{Ⅎ} x Z$
88		nffvmpt1	$⊢ \underline{Ⅎ} x (x \in A ⟼ B) (z)$
89	80 81 88	nfbr	$⊢ Ⅎ x t < (x \in A ⟼ B) (z)$
90	87 89	nfrex	$⊢ Ⅎ x \exists n \in Z t < (x \in A ⟼ B) (z)$
91	86 90	nfbi	$⊢ Ⅎ x (t < G (z) \leftrightarrow \exists n \in Z t < (x \in A ⟼ B) (z))$
92		fveq2	$⊢ x = z \to G (x) = G (z)$
93	92	breq2d	$⊢ x = z \to (t < G (x) \leftrightarrow t < G (z))$
94		fveq2	$⊢ x = z \to (x \in A ⟼ B) (x) = (x \in A ⟼ B) (z)$
95	94	breq2d	$⊢ x = z \to (t < (x \in A ⟼ B) (x) \leftrightarrow t < (x \in A ⟼ B) (z))$
96	95	rexbidv	$⊢ x = z \to (\exists n \in Z t < (x \in A ⟼ B) (x) \leftrightarrow \exists n \in Z t < (x \in A ⟼ B) (z))$
97	93 96	bibi12d	$⊢ x = z \to ((t < G (x) \leftrightarrow \exists n \in Z t < (x \in A ⟼ B) (x)) \leftrightarrow (t < G (z) \leftrightarrow \exists n \in Z t < (x \in A ⟼ B) (z)))$
98	79 91 97	cbvralw	$⊢ \forall x \in A (t < G (x) \leftrightarrow \exists n \in Z t < (x \in A ⟼ B) (x)) \leftrightarrow \forall z \in A (t < G (z) \leftrightarrow \exists n \in Z t < (x \in A ⟼ B) (z))$
99	78 98	sylib	$⊢ (φ \land t \in ℝ) \to \forall z \in A (t < G (z) \leftrightarrow \exists n \in Z t < (x \in A ⟼ B) (z))$
100	99	r19.21bi	$⊢ ((φ \land t \in ℝ) \land z \in A) \to (t < G (z) \leftrightarrow \exists n \in Z t < (x \in A ⟼ B) (z))$
101	44	adantr	$⊢ (φ \land t \in ℝ) \to G : A ⟶ ℝ$
102	101	ffvelrnda	$⊢ ((φ \land t \in ℝ) \land z \in A) \to G (z) \in ℝ$
103		rexr	$⊢ t \in ℝ \to t \in ℝ^{*}$
104	103	ad2antlr	$⊢ ((φ \land t \in ℝ) \land z \in A) \to t \in ℝ^{*}$
105		elioopnf	$⊢ t \in ℝ^{*} \to (G (z) \in (t, +∞) \leftrightarrow (G (z) \in ℝ \land t < G (z)))$
106	104 105	syl	$⊢ ((φ \land t \in ℝ) \land z \in A) \to (G (z) \in (t, +∞) \leftrightarrow (G (z) \in ℝ \land t < G (z)))$
107	102 106	mpbirand	$⊢ ((φ \land t \in ℝ) \land z \in A) \to (G (z) \in (t, +∞) \leftrightarrow t < G (z))$
108	104	adantr	$⊢ (((φ \land t \in ℝ) \land z \in A) \land n \in Z) \to t \in ℝ^{*}$
109		elioopnf	$⊢ t \in ℝ^{*} \to ((x \in A ⟼ B) (z) \in (t, +∞) \leftrightarrow ((x \in A ⟼ B) (z) \in ℝ \land t < (x \in A ⟼ B) (z)))$
110	108 109	syl	$⊢ (((φ \land t \in ℝ) \land z \in A) \land n \in Z) \to ((x \in A ⟼ B) (z) \in (t, +∞) \leftrightarrow ((x \in A ⟼ B) (z) \in ℝ \land t < (x \in A ⟼ B) (z)))$
111	7	fmpttd	$⊢ (φ \land n \in Z) \to (x \in A ⟼ B) : A ⟶ ℝ$
112	111	ffvelrnda	$⊢ ((φ \land n \in Z) \land z \in A) \to (x \in A ⟼ B) (z) \in ℝ$
113	112	biantrurd	$⊢ ((φ \land n \in Z) \land z \in A) \to (t < (x \in A ⟼ B) (z) \leftrightarrow ((x \in A ⟼ B) (z) \in ℝ \land t < (x \in A ⟼ B) (z)))$
114	113	an32s	$⊢ ((φ \land z \in A) \land n \in Z) \to (t < (x \in A ⟼ B) (z) \leftrightarrow ((x \in A ⟼ B) (z) \in ℝ \land t < (x \in A ⟼ B) (z)))$
115	114	adantllr	$⊢ (((φ \land t \in ℝ) \land z \in A) \land n \in Z) \to (t < (x \in A ⟼ B) (z) \leftrightarrow ((x \in A ⟼ B) (z) \in ℝ \land t < (x \in A ⟼ B) (z)))$
116	110 115	bitr4d	$⊢ (((φ \land t \in ℝ) \land z \in A) \land n \in Z) \to ((x \in A ⟼ B) (z) \in (t, +∞) \leftrightarrow t < (x \in A ⟼ B) (z))$
117	116	rexbidva	$⊢ ((φ \land t \in ℝ) \land z \in A) \to (\exists n \in Z (x \in A ⟼ B) (z) \in (t, +∞) \leftrightarrow \exists n \in Z t < (x \in A ⟼ B) (z))$
118	100 107 117	3bitr4d	$⊢ ((φ \land t \in ℝ) \land z \in A) \to (G (z) \in (t, +∞) \leftrightarrow \exists n \in Z (x \in A ⟼ B) (z) \in (t, +∞))$
119	118	pm5.32da	$⊢ (φ \land t \in ℝ) \to ((z \in A \land G (z) \in (t, +∞)) \leftrightarrow (z \in A \land \exists n \in Z (x \in A ⟼ B) (z) \in (t, +∞)))$
120	44	ffnd	$⊢ φ \to G Fn A$
121	120	adantr	$⊢ (φ \land t \in ℝ) \to G Fn A$
122		elpreima	$⊢ G Fn A \to (z \in G^{-1} [(t, +∞)] \leftrightarrow (z \in A \land G (z) \in (t, +∞)))$
123	121 122	syl	$⊢ (φ \land t \in ℝ) \to (z \in G^{-1} [(t, +∞)] \leftrightarrow (z \in A \land G (z) \in (t, +∞)))$
124		eliun	$⊢ z \in ⋃_{n \in Z} {(x \in A ⟼ B)}^{-1} [(t, +∞)] \leftrightarrow \exists n \in Z z \in {(x \in A ⟼ B)}^{-1} [(t, +∞)]$
125	111	ffnd	$⊢ (φ \land n \in Z) \to (x \in A ⟼ B) Fn A$
126		elpreima	$⊢ (x \in A ⟼ B) Fn A \to (z \in {(x \in A ⟼ B)}^{-1} [(t, +∞)] \leftrightarrow (z \in A \land (x \in A ⟼ B) (z) \in (t, +∞)))$
127	125 126	syl	$⊢ (φ \land n \in Z) \to (z \in {(x \in A ⟼ B)}^{-1} [(t, +∞)] \leftrightarrow (z \in A \land (x \in A ⟼ B) (z) \in (t, +∞)))$
128	127	rexbidva	$⊢ φ \to (\exists n \in Z z \in {(x \in A ⟼ B)}^{-1} [(t, +∞)] \leftrightarrow \exists n \in Z (z \in A \land (x \in A ⟼ B) (z) \in (t, +∞)))$
129	128	adantr	$⊢ (φ \land t \in ℝ) \to (\exists n \in Z z \in {(x \in A ⟼ B)}^{-1} [(t, +∞)] \leftrightarrow \exists n \in Z (z \in A \land (x \in A ⟼ B) (z) \in (t, +∞)))$
130		r19.42v	$⊢ \exists n \in Z (z \in A \land (x \in A ⟼ B) (z) \in (t, +∞)) \leftrightarrow (z \in A \land \exists n \in Z (x \in A ⟼ B) (z) \in (t, +∞))$
131	129 130	bitrdi	$⊢ (φ \land t \in ℝ) \to (\exists n \in Z z \in {(x \in A ⟼ B)}^{-1} [(t, +∞)] \leftrightarrow (z \in A \land \exists n \in Z (x \in A ⟼ B) (z) \in (t, +∞)))$
132	124 131	syl5bb	$⊢ (φ \land t \in ℝ) \to (z \in ⋃_{n \in Z} {(x \in A ⟼ B)}^{-1} [(t, +∞)] \leftrightarrow (z \in A \land \exists n \in Z (x \in A ⟼ B) (z) \in (t, +∞)))$
133	119 123 132	3bitr4d	$⊢ (φ \land t \in ℝ) \to (z \in G^{-1} [(t, +∞)] \leftrightarrow z \in ⋃_{n \in Z} {(x \in A ⟼ B)}^{-1} [(t, +∞)])$
134	133	eqrdv	$⊢ (φ \land t \in ℝ) \to G^{-1} [(t, +∞)] = ⋃_{n \in Z} {(x \in A ⟼ B)}^{-1} [(t, +∞)]$
135		zex	$⊢ ℤ \in V$
136		uzssz	$⊢ ℤ_{\geq M} \subseteq ℤ$
137		ssdomg	$⊢ ℤ \in V \to (ℤ_{\geq M} \subseteq ℤ \to ℤ_{\geq M} ≼ ℤ)$
138	135 136 137	mp2	$⊢ ℤ_{\geq M} ≼ ℤ$
139	1 138	eqbrtri	$⊢ Z ≼ ℤ$
140		znnen	$⊢ ℤ \approx ℕ$
141		domentr	$⊢ (Z ≼ ℤ \land ℤ \approx ℕ) \to Z ≼ ℕ$
142	139 140 141	mp2an	$⊢ Z ≼ ℕ$
143		mbfima	$⊢ ((x \in A ⟼ B) \in MblFn \land (x \in A ⟼ B) : A ⟶ ℝ) \to {(x \in A ⟼ B)}^{-1} [(t, +∞)] \in dom vol$
144	4 111 143	syl2anc	$⊢ (φ \land n \in Z) \to {(x \in A ⟼ B)}^{-1} [(t, +∞)] \in dom vol$
145	144	ralrimiva	$⊢ φ \to \forall n \in Z {(x \in A ⟼ B)}^{-1} [(t, +∞)] \in dom vol$
146	145	adantr	$⊢ (φ \land t \in ℝ) \to \forall n \in Z {(x \in A ⟼ B)}^{-1} [(t, +∞)] \in dom vol$
147		iunmbl2	$⊢ (Z ≼ ℕ \land \forall n \in Z {(x \in A ⟼ B)}^{-1} [(t, +∞)] \in dom vol) \to ⋃_{n \in Z} {(x \in A ⟼ B)}^{-1} [(t, +∞)] \in dom vol$
148	142 146 147	sylancr	$⊢ (φ \land t \in ℝ) \to ⋃_{n \in Z} {(x \in A ⟼ B)}^{-1} [(t, +∞)] \in dom vol$
149	134 148	eqeltrd	$⊢ (φ \land t \in ℝ) \to G^{-1} [(t, +∞)] \in dom vol$
150	44 149	ismbf3d	$⊢ φ \to G \in MblFn$

Metamath Proof Explorer

Theorem mbfsup

Proof