ovolval5lem3

Description: The value of the Lebesgue outer measure for subsets of the reals, using covers of left-closed right-open intervals are used, instead of open intervals. (Contributed by Glauco Siliprandi, 3-Mar-2021)

	Ref	Expression
Hypotheses	ovolval5lem3.m	$⊢ M = \{y \in ℝ^{*} \| \exists f \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ([.) \circ f) \land y = sum^((vol \circ [.)) \circ f))\}$
	ovolval5lem3.q	$⊢ Q = \{z \in ℝ^{*} \| \exists f \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land z = sum^((vol \circ (.)) \circ f))\}$
Assertion	ovolval5lem3	$⊢ sup (Q ℝ^{} <) = sup (M ℝ^{} <)$

Proof

Step	Hyp	Ref	Expression
1		ovolval5lem3.m	$⊢ M = \{y \in ℝ^{*} \| \exists f \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ([.) \circ f) \land y = sum^((vol \circ [.)) \circ f))\}$
2		ovolval5lem3.q	$⊢ Q = \{z \in ℝ^{*} \| \exists f \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land z = sum^((vol \circ (.)) \circ f))\}$
3		ssrab2	$⊢ \{z \in ℝ^{} \| \exists f \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land z = sum^((vol \circ (.)) \circ f))\} \subseteq ℝ^{}$
4	2 3	eqsstri	$⊢ Q \subseteq ℝ^{*}$
5		infxrcl	$⊢ Q \subseteq ℝ^{} \to sup (Q ℝ^{} <) \in ℝ^{*}$
6	4 5	mp1i	$⊢ ⊤ \to sup (Q ℝ^{} <) \in ℝ^{}$
7		ssrab2	$⊢ \{y \in ℝ^{} \| \exists f \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ([.) \circ f) \land y = sum^((vol \circ [.)) \circ f))\} \subseteq ℝ^{}$
8	1 7	eqsstri	$⊢ M \subseteq ℝ^{*}$
9		infxrcl	$⊢ M \subseteq ℝ^{} \to sup (M ℝ^{} <) \in ℝ^{*}$
10	8 9	mp1i	$⊢ ⊤ \to sup (M ℝ^{} <) \in ℝ^{}$
11	4	a1i	$⊢ ⊤ \to Q \subseteq ℝ^{*}$
12	8	a1i	$⊢ ⊤ \to M \subseteq ℝ^{*}$
13		simpr	$⊢ (y \in M \land w \in ℝ^{+}) \to w \in ℝ^{+}$
14	1	rabeq2i	$⊢ y \in M \leftrightarrow (y \in ℝ^{*} \land \exists f \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ([.) \circ f) \land y = sum^((vol \circ [.)) \circ f)))$
15	14	biimpi	$⊢ y \in M \to (y \in ℝ^{*} \land \exists f \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ([.) \circ f) \land y = sum^((vol \circ [.)) \circ f)))$
16	15	simprd	$⊢ y \in M \to \exists f \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ([.) \circ f) \land y = sum^((vol \circ [.)) \circ f))$
17	16	adantr	$⊢ (y \in M \land w \in ℝ^{+}) \to \exists f \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ([.) \circ f) \land y = sum^((vol \circ [.)) \circ f))$
18		coeq2	$⊢ g = f \to (.) \circ g = (.) \circ f$
19	18	rneqd	$⊢ g = f \to ran ((.) \circ g) = ran ((.) \circ f)$
20	19	unieqd	$⊢ g = f \to ⋃ ran ((.) \circ g) = ⋃ ran ((.) \circ f)$
21	20	sseq2d	$⊢ g = f \to (A \subseteq ⋃ ran ((.) \circ g) \leftrightarrow A \subseteq ⋃ ran ((.) \circ f))$
22		coeq2	$⊢ g = f \to (vol \circ (.)) \circ g = (vol \circ (.)) \circ f$
23	22	fveq2d	$⊢ g = f \to sum^((vol \circ (.)) \circ g) = sum^((vol \circ (.)) \circ f)$
24	23	eqeq2d	$⊢ g = f \to (z = sum^((vol \circ (.)) \circ g) \leftrightarrow z = sum^((vol \circ (.)) \circ f))$
25	21 24	anbi12d	$⊢ g = f \to ((A \subseteq ⋃ ran ((.) \circ g) \land z = sum^((vol \circ (.)) \circ g)) \leftrightarrow (A \subseteq ⋃ ran ((.) \circ f) \land z = sum^((vol \circ (.)) \circ f)))$
26	25	cbvrexvw	$⊢ \exists g \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ g) \land z = sum^((vol \circ (.)) \circ g)) \leftrightarrow \exists f \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land z = sum^((vol \circ (.)) \circ f))$
27	26	rabbii	$⊢ \{z \in ℝ^{} \| \exists g \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ g) \land z = sum^((vol \circ (.)) \circ g))\} = \{z \in ℝ^{} \| \exists f \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land z = sum^((vol \circ (.)) \circ f))\}$
28	2 27	eqtr4i	$⊢ Q = \{z \in ℝ^{*} \| \exists g \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ g) \land z = sum^((vol \circ (.)) \circ g))\}$
29		simp3r	$⊢ (w \in ℝ^{+} \land f \in ({ℝ^{2}}^{ℕ}) \land (A \subseteq ⋃ ran ([.) \circ f) \land y = sum^((vol \circ [.)) \circ f))) \to y = sum^((vol \circ [.)) \circ f)$
30		eqid	$⊢ sum^((vol \circ (.)) \circ (m \in ℕ ⟼ ⟨1^{st} (f (m)) - (\frac{w}{2^{m}}), 2^{nd} (f (m))⟩)) = sum^((vol \circ (.)) \circ (m \in ℕ ⟼ ⟨1^{st} (f (m)) - (\frac{w}{2^{m}}), 2^{nd} (f (m))⟩))$
31		elmapi	$⊢ f \in ({ℝ^{2}}^{ℕ}) \to f : ℕ ⟶ ℝ^{2}$
32	31	3ad2ant2	$⊢ (w \in ℝ^{+} \land f \in ({ℝ^{2}}^{ℕ}) \land (A \subseteq ⋃ ran ([.) \circ f) \land y = sum^((vol \circ [.)) \circ f))) \to f : ℕ ⟶ ℝ^{2}$
33		simp3l	$⊢ (w \in ℝ^{+} \land f \in ({ℝ^{2}}^{ℕ}) \land (A \subseteq ⋃ ran ([.) \circ f) \land y = sum^((vol \circ [.)) \circ f))) \to A \subseteq ⋃ ran ([.) \circ f)$
34		simp1	$⊢ (w \in ℝ^{+} \land f \in ({ℝ^{2}}^{ℕ}) \land (A \subseteq ⋃ ran ([.) \circ f) \land y = sum^((vol \circ [.)) \circ f))) \to w \in ℝ^{+}$
35		2fveq3	$⊢ m = n \to 1^{st} (f (m)) = 1^{st} (f (n))$
36		oveq2	$⊢ m = n \to 2^{m} = 2^{n}$
37	36	oveq2d	$⊢ m = n \to \frac{w}{2^{m}} = \frac{w}{2^{n}}$
38	35 37	oveq12d	$⊢ m = n \to 1^{st} (f (m)) - (\frac{w}{2^{m}}) = 1^{st} (f (n)) - (\frac{w}{2^{n}})$
39		2fveq3	$⊢ m = n \to 2^{nd} (f (m)) = 2^{nd} (f (n))$
40	38 39	opeq12d	$⊢ m = n \to ⟨1^{st} (f (m)) - (\frac{w}{2^{m}}), 2^{nd} (f (m))⟩ = ⟨1^{st} (f (n)) - (\frac{w}{2^{n}}), 2^{nd} (f (n))⟩$
41	40	cbvmptv	$⊢ (m \in ℕ ⟼ ⟨1^{st} (f (m)) - (\frac{w}{2^{m}}), 2^{nd} (f (m))⟩) = (n \in ℕ ⟼ ⟨1^{st} (f (n)) - (\frac{w}{2^{n}}), 2^{nd} (f (n))⟩)$
42	28 29 30 32 33 34 41	ovolval5lem2	$⊢ (w \in ℝ^{+} \land f \in ({ℝ^{2}}^{ℕ}) \land (A \subseteq ⋃ ran ([.) \circ f) \land y = sum^((vol \circ [.)) \circ f))) \to \exists z \in Q z \leq y +_{𝑒} w$
43	42	3exp	$⊢ w \in ℝ^{+} \to (f \in ({ℝ^{2}}^{ℕ}) \to ((A \subseteq ⋃ ran ([.) \circ f) \land y = sum^((vol \circ [.)) \circ f)) \to \exists z \in Q z \leq y +_{𝑒} w))$
44	43	rexlimdv	$⊢ w \in ℝ^{+} \to (\exists f \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ([.) \circ f) \land y = sum^((vol \circ [.)) \circ f)) \to \exists z \in Q z \leq y +_{𝑒} w)$
45	44	imp	$⊢ (w \in ℝ^{+} \land \exists f \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ([.) \circ f) \land y = sum^((vol \circ [.)) \circ f))) \to \exists z \in Q z \leq y +_{𝑒} w$
46	13 17 45	syl2anc	$⊢ (y \in M \land w \in ℝ^{+}) \to \exists z \in Q z \leq y +_{𝑒} w$
47	46	3adant1	$⊢ (⊤ \land y \in M \land w \in ℝ^{+}) \to \exists z \in Q z \leq y +_{𝑒} w$
48	11 12 47	infleinf	$⊢ ⊤ \to sup (Q ℝ^{} <) \leq sup (M ℝ^{} <)$
49		eqeq1	$⊢ z = y \to (z = sum^((vol \circ (.)) \circ f) \leftrightarrow y = sum^((vol \circ (.)) \circ f))$
50	49	anbi2d	$⊢ z = y \to ((A \subseteq ⋃ ran ((.) \circ f) \land z = sum^((vol \circ (.)) \circ f)) \leftrightarrow (A \subseteq ⋃ ran ((.) \circ f) \land y = sum^((vol \circ (.)) \circ f)))$
51	50	rexbidv	$⊢ z = y \to (\exists f \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land z = sum^((vol \circ (.)) \circ f)) \leftrightarrow \exists f \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land y = sum^((vol \circ (.)) \circ f)))$
52	51	cbvrabv	$⊢ \{z \in ℝ^{} \| \exists f \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land z = sum^((vol \circ (.)) \circ f))\} = \{y \in ℝ^{} \| \exists f \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land y = sum^((vol \circ (.)) \circ f))\}$
53		simpr	$⊢ (f \in ({ℝ^{2}}^{ℕ}) \land A \subseteq ⋃ ran ((.) \circ f)) \to A \subseteq ⋃ ran ((.) \circ f)$
54		ioossico	$⊢ (1^{st} (f (n)), 2^{nd} (f (n))) \subseteq [1^{st} (f (n)), 2^{nd} (f (n)))$
55	54	a1i	$⊢ (f \in ({ℝ^{2}}^{ℕ}) \land n \in ℕ) \to (1^{st} (f (n)), 2^{nd} (f (n))) \subseteq [1^{st} (f (n)), 2^{nd} (f (n)))$
56	31	adantr	$⊢ (f \in ({ℝ^{2}}^{ℕ}) \land n \in ℕ) \to f : ℕ ⟶ ℝ^{2}$
57		simpr	$⊢ (f \in ({ℝ^{2}}^{ℕ}) \land n \in ℕ) \to n \in ℕ$
58	56 57	fvovco	$⊢ (f \in ({ℝ^{2}}^{ℕ}) \land n \in ℕ) \to ((.) \circ f) (n) = (1^{st} (f (n)), 2^{nd} (f (n)))$
59	56 57	fvovco	$⊢ (f \in ({ℝ^{2}}^{ℕ}) \land n \in ℕ) \to ([.) \circ f) (n) = [1^{st} (f (n)), 2^{nd} (f (n)))$
60	58 59	sseq12d	$⊢ (f \in ({ℝ^{2}}^{ℕ}) \land n \in ℕ) \to (((.) \circ f) (n) \subseteq ([.) \circ f) (n) \leftrightarrow (1^{st} (f (n)), 2^{nd} (f (n))) \subseteq [1^{st} (f (n)), 2^{nd} (f (n))))$
61	55 60	mpbird	$⊢ (f \in ({ℝ^{2}}^{ℕ}) \land n \in ℕ) \to ((.) \circ f) (n) \subseteq ([.) \circ f) (n)$
62	61	ralrimiva	$⊢ f \in ({ℝ^{2}}^{ℕ}) \to \forall n \in ℕ ((.) \circ f) (n) \subseteq ([.) \circ f) (n)$
63		ss2iun	$⊢ \forall n \in ℕ ((.) \circ f) (n) \subseteq ([.) \circ f) (n) \to ⋃_{n \in ℕ} ((.) \circ f) (n) \subseteq ⋃_{n \in ℕ} ([.) \circ f) (n)$
64	62 63	syl	$⊢ f \in ({ℝ^{2}}^{ℕ}) \to ⋃_{n \in ℕ} ((.) \circ f) (n) \subseteq ⋃_{n \in ℕ} ([.) \circ f) (n)$
65		ioof	$⊢ (.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ$
66	65	a1i	$⊢ f \in ({ℝ^{2}}^{ℕ}) \to (.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ$
67		rexpssxrxp	$⊢ ℝ^{2} \subseteq ℝ^{} \times ℝ^{}$
68	67	a1i	$⊢ f \in ({ℝ^{2}}^{ℕ}) \to ℝ^{2} \subseteq ℝ^{} \times ℝ^{}$
69	31 68	fssd	$⊢ f \in ({ℝ^{2}}^{ℕ}) \to f : ℕ ⟶ ℝ^{} \times ℝ^{}$
70		fco	$⊢ ((.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ \land f : ℕ ⟶ ℝ^{} \times ℝ^{}) \to ((.) \circ f) : ℕ ⟶ 𝒫 ℝ$
71	66 69 70	syl2anc	$⊢ f \in ({ℝ^{2}}^{ℕ}) \to ((.) \circ f) : ℕ ⟶ 𝒫 ℝ$
72	71	ffnd	$⊢ f \in ({ℝ^{2}}^{ℕ}) \to ((.) \circ f) Fn ℕ$
73		fniunfv	$⊢ ((.) \circ f) Fn ℕ \to ⋃_{n \in ℕ} ((.) \circ f) (n) = ⋃ ran ((.) \circ f)$
74	72 73	syl	$⊢ f \in ({ℝ^{2}}^{ℕ}) \to ⋃_{n \in ℕ} ((.) \circ f) (n) = ⋃ ran ((.) \circ f)$
75		icof	$⊢ [.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ^{*}$
76	75	a1i	$⊢ f \in ({ℝ^{2}}^{ℕ}) \to [.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ^{*}$
77		fco	$⊢ ([.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ^{} \land f : ℕ ⟶ ℝ^{} \times ℝ^{}) \to ([.) \circ f) : ℕ ⟶ 𝒫 ℝ^{}$
78	76 69 77	syl2anc	$⊢ f \in ({ℝ^{2}}^{ℕ}) \to ([.) \circ f) : ℕ ⟶ 𝒫 ℝ^{*}$
79	78	ffnd	$⊢ f \in ({ℝ^{2}}^{ℕ}) \to ([.) \circ f) Fn ℕ$
80		fniunfv	$⊢ ([.) \circ f) Fn ℕ \to ⋃_{n \in ℕ} ([.) \circ f) (n) = ⋃ ran ([.) \circ f)$
81	79 80	syl	$⊢ f \in ({ℝ^{2}}^{ℕ}) \to ⋃_{n \in ℕ} ([.) \circ f) (n) = ⋃ ran ([.) \circ f)$
82	74 81	sseq12d	$⊢ f \in ({ℝ^{2}}^{ℕ}) \to (⋃_{n \in ℕ} ((.) \circ f) (n) \subseteq ⋃_{n \in ℕ} ([.) \circ f) (n) \leftrightarrow ⋃ ran ((.) \circ f) \subseteq ⋃ ran ([.) \circ f))$
83	64 82	mpbid	$⊢ f \in ({ℝ^{2}}^{ℕ}) \to ⋃ ran ((.) \circ f) \subseteq ⋃ ran ([.) \circ f)$
84	83	adantr	$⊢ (f \in ({ℝ^{2}}^{ℕ}) \land A \subseteq ⋃ ran ((.) \circ f)) \to ⋃ ran ((.) \circ f) \subseteq ⋃ ran ([.) \circ f)$
85	53 84	sstrd	$⊢ (f \in ({ℝ^{2}}^{ℕ}) \land A \subseteq ⋃ ran ((.) \circ f)) \to A \subseteq ⋃ ran ([.) \circ f)$
86	85	adantrr	$⊢ (f \in ({ℝ^{2}}^{ℕ}) \land (A \subseteq ⋃ ran ((.) \circ f) \land y = sum^((vol \circ (.)) \circ f))) \to A \subseteq ⋃ ran ([.) \circ f)$
87		simpr	$⊢ (f \in ({ℝ^{2}}^{ℕ}) \land y = sum^((vol \circ (.)) \circ f)) \to y = sum^((vol \circ (.)) \circ f)$
88	31	voliooicof	$⊢ f \in ({ℝ^{2}}^{ℕ}) \to (vol \circ (.)) \circ f = (vol \circ [.)) \circ f$
89	88	fveq2d	$⊢ f \in ({ℝ^{2}}^{ℕ}) \to sum^((vol \circ (.)) \circ f) = sum^((vol \circ [.)) \circ f)$
90	89	adantr	$⊢ (f \in ({ℝ^{2}}^{ℕ}) \land y = sum^((vol \circ (.)) \circ f)) \to sum^((vol \circ (.)) \circ f) = sum^((vol \circ [.)) \circ f)$
91	87 90	eqtrd	$⊢ (f \in ({ℝ^{2}}^{ℕ}) \land y = sum^((vol \circ (.)) \circ f)) \to y = sum^((vol \circ [.)) \circ f)$
92	91	adantrl	$⊢ (f \in ({ℝ^{2}}^{ℕ}) \land (A \subseteq ⋃ ran ((.) \circ f) \land y = sum^((vol \circ (.)) \circ f))) \to y = sum^((vol \circ [.)) \circ f)$
93	86 92	jca	$⊢ (f \in ({ℝ^{2}}^{ℕ}) \land (A \subseteq ⋃ ran ((.) \circ f) \land y = sum^((vol \circ (.)) \circ f))) \to (A \subseteq ⋃ ran ([.) \circ f) \land y = sum^((vol \circ [.)) \circ f))$
94	93	ex	$⊢ f \in ({ℝ^{2}}^{ℕ}) \to ((A \subseteq ⋃ ran ((.) \circ f) \land y = sum^((vol \circ (.)) \circ f)) \to (A \subseteq ⋃ ran ([.) \circ f) \land y = sum^((vol \circ [.)) \circ f)))$
95	94	reximia	$⊢ \exists f \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land y = sum^((vol \circ (.)) \circ f)) \to \exists f \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ([.) \circ f) \land y = sum^((vol \circ [.)) \circ f))$
96	95	rgenw	$⊢ \forall y \in ℝ^{*} (\exists f \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land y = sum^((vol \circ (.)) \circ f)) \to \exists f \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ([.) \circ f) \land y = sum^((vol \circ [.)) \circ f)))$
97		ss2rab	$⊢ \{y \in ℝ^{} \| \exists f \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land y = sum^((vol \circ (.)) \circ f))\} \subseteq \{y \in ℝ^{} \| \exists f \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ([.) \circ f) \land y = sum^((vol \circ [.)) \circ f))\} \leftrightarrow \forall y \in ℝ^{*} (\exists f \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land y = sum^((vol \circ (.)) \circ f)) \to \exists f \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ([.) \circ f) \land y = sum^((vol \circ [.)) \circ f)))$
98	96 97	mpbir	$⊢ \{y \in ℝ^{} \| \exists f \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land y = sum^((vol \circ (.)) \circ f))\} \subseteq \{y \in ℝ^{} \| \exists f \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ([.) \circ f) \land y = sum^((vol \circ [.)) \circ f))\}$
99	52 98	eqsstri	$⊢ \{z \in ℝ^{} \| \exists f \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land z = sum^((vol \circ (.)) \circ f))\} \subseteq \{y \in ℝ^{} \| \exists f \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ([.) \circ f) \land y = sum^((vol \circ [.)) \circ f))\}$
100	2 1	sseq12i	$⊢ Q \subseteq M \leftrightarrow \{z \in ℝ^{} \| \exists f \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land z = sum^((vol \circ (.)) \circ f))\} \subseteq \{y \in ℝ^{} \| \exists f \in ({ℝ^{2}}^{ℕ}) (A \subseteq ⋃ ran ([.) \circ f) \land y = sum^((vol \circ [.)) \circ f))\}$
101	99 100	mpbir	$⊢ Q \subseteq M$
102		infxrss	$⊢ (Q \subseteq M \land M \subseteq ℝ^{}) \to sup (M ℝ^{} <) \leq sup (Q ℝ^{*} <)$
103	101 8 102	mp2an	$⊢ sup (M ℝ^{} <) \leq sup (Q ℝ^{} <)$
104	103	a1i	$⊢ ⊤ \to sup (M ℝ^{} <) \leq sup (Q ℝ^{} <)$
105	6 10 48 104	xrletrid	$⊢ ⊤ \to sup (Q ℝ^{} <) = sup (M ℝ^{} <)$
106	105	mptru	$⊢ sup (Q ℝ^{} <) = sup (M ℝ^{} <)$

Metamath Proof Explorer

Theorem ovolval5lem3

Proof