Metamath Proof Explorer

Theorem ovnpnfelsup

Description: +oo is an element of the set used in the definition of the Lebesgue outer measure. (Contributed by Glauco Siliprandi, 11-Oct-2020)

		Ref	Expression
	Hypotheses	ovnpnfelsup.1	$⊢ φ \to X \in Fin$
		ovnpnfelsup.2	$⊢ φ \to A \subseteq ℝ^{X}$
		ovnpnfelsup.3	$⊢ M = \{z \in ℝ^{*} \| \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k) \land z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k)))))\}$
	Assertion	ovnpnfelsup	$⊢ φ \to +∞ \in M$

Proof

Step	Hyp	Ref	Expression
1		ovnpnfelsup.1	$⊢ φ \to X \in Fin$
2		ovnpnfelsup.2	$⊢ φ \to A \subseteq ℝ^{X}$
3		ovnpnfelsup.3	$⊢ M = \{z \in ℝ^{*} \| \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k) \land z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k)))))\}$
4		pnfxr	$⊢ +∞ \in ℝ^{*}$
5	4	a1i	$⊢ φ \to +∞ \in ℝ^{*}$
6	1 2	hoicvrrex	$⊢ φ \to \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k) \land +∞ = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k)))))$
7	5 6	jca	$⊢ φ \to (+∞ \in ℝ^{*} \land \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k) \land +∞ = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k))))))$
8		eqeq1	$⊢ z = +∞ \to (z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k)))) \leftrightarrow +∞ = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k)))))$
9	8	anbi2d	$⊢ z = +∞ \to ((A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k) \land z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k))))) \leftrightarrow (A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k) \land +∞ = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k))))))$
10	9	rexbidv	$⊢ z = +∞ \to (\exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k) \land z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k))))) \leftrightarrow \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k) \land +∞ = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k))))))$
11	10	elrab	$⊢ +∞ \in \{z \in ℝ^{} \| \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k) \land z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k)))))\} \leftrightarrow (+∞ \in ℝ^{} \land \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k) \land +∞ = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k))))))$
12	7 11	sylibr	$⊢ φ \to +∞ \in \{z \in ℝ^{*} \| \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k) \land z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k)))))\}$
13	3	eqcomi	$⊢ \{z \in ℝ^{*} \| \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k) \land z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k)))))\} = M$
14	13	a1i	$⊢ φ \to \{z \in ℝ^{*} \| \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k) \land z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k)))))\} = M$
15	12 14	eleqtrd	$⊢ φ \to +∞ \in M$