Metamath Proof Explorer

Theorem ex-ovoliunnfl

Description: Demonstration of ovoliunnfl . (Contributed by Brendan Leahy, 21-Nov-2017)

		Ref	Expression
	Assertion	ex-ovoliunnfl	$⊢ (A ≼ ℕ \land \forall x \in A x ≼ ℕ) \to ⋃ A \neq ℝ$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ seq 1 (+ (m \in ℕ ⟼ {vol}^{} (f (m)))) = seq 1 (+ (m \in ℕ ⟼ {vol}^{} (f (m))))$
2		eqid	$⊢ (m \in ℕ ⟼ {vol}^{} (f (m))) = (m \in ℕ ⟼ {vol}^{} (f (m)))$
3		fveq2	$⊢ n = m \to f (n) = f (m)$
4	3	sseq1d	$⊢ n = m \to (f (n) \subseteq ℝ \leftrightarrow f (m) \subseteq ℝ)$
5		2fveq3	$⊢ n = m \to {vol}^{} (f (n)) = {vol}^{} (f (m))$
6	5	eleq1d	$⊢ n = m \to ({vol}^{} (f (n)) \in ℝ \leftrightarrow {vol}^{} (f (m)) \in ℝ)$
7	4 6	anbi12d	$⊢ n = m \to ((f (n) \subseteq ℝ \land {vol}^{} (f (n)) \in ℝ) \leftrightarrow (f (m) \subseteq ℝ \land {vol}^{} (f (m)) \in ℝ))$
8	7	rspccva	$⊢ (\forall n \in ℕ (f (n) \subseteq ℝ \land {vol}^{} (f (n)) \in ℝ) \land m \in ℕ) \to (f (m) \subseteq ℝ \land {vol}^{} (f (m)) \in ℝ)$
9	8	simpld	$⊢ (\forall n \in ℕ (f (n) \subseteq ℝ \land {vol}^{*} (f (n)) \in ℝ) \land m \in ℕ) \to f (m) \subseteq ℝ$
10	9	adantll	$⊢ ((f Fn ℕ \land \forall n \in ℕ (f (n) \subseteq ℝ \land {vol}^{*} (f (n)) \in ℝ)) \land m \in ℕ) \to f (m) \subseteq ℝ$
11	8	simprd	$⊢ (\forall n \in ℕ (f (n) \subseteq ℝ \land {vol}^{} (f (n)) \in ℝ) \land m \in ℕ) \to {vol}^{} (f (m)) \in ℝ$
12	11	adantll	$⊢ ((f Fn ℕ \land \forall n \in ℕ (f (n) \subseteq ℝ \land {vol}^{} (f (n)) \in ℝ)) \land m \in ℕ) \to {vol}^{} (f (m)) \in ℝ$
13	1 2 10 12	ovoliun	$⊢ (f Fn ℕ \land \forall n \in ℕ (f (n) \subseteq ℝ \land {vol}^{} (f (n)) \in ℝ)) \to {vol}^{} (⋃_{m \in ℕ} f (m)) \leq sup (ran seq 1 (+ (m \in ℕ ⟼ {vol}^{} (f (m)))) ℝ^{} <)$
14	13	ovoliunnfl	$⊢ (A ≼ ℕ \land \forall x \in A x ≼ ℕ) \to ⋃ A \neq ℝ$