Metamath Proof Explorer

Theorem ex-ovoliunnfl

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

Ref Expression
Assertion ex-ovoliunnfl ⊢ A ≼ ℕ ∧ ∀ x ∈ A x ≼ ℕ → ⋃ A ≠ ℝ

Proof

Step Hyp Ref Expression
1 eqid ⊢ seq 1 + m ∈ ℕ ⟼ vol * ⁡ f ⁡ m = seq 1 + m ∈ ℕ ⟼ vol * ⁡ f ⁡ m
2 eqid ⊢ m ∈ ℕ ⟼ vol * ⁡ f ⁡ m = m ∈ ℕ ⟼ vol * ⁡ f ⁡ m
3 fveq2 ⊢ n = m → f ⁡ n = f ⁡ m
4 3 sseq1d ⊢ n = m → f ⁡ n ⊆ ℝ ↔ f ⁡ m ⊆ ℝ
5 2fveq3 ⊢ n = m → vol * ⁡ f ⁡ n = vol * ⁡ f ⁡ m
6 5 eleq1d ⊢ n = m → vol * ⁡ f ⁡ n ∈ ℝ ↔ vol * ⁡ f ⁡ m ∈ ℝ
7 4 6 anbi12d ⊢ n = m → f ⁡ n ⊆ ℝ ∧ vol * ⁡ f ⁡ n ∈ ℝ ↔ f ⁡ m ⊆ ℝ ∧ vol * ⁡ f ⁡ m ∈ ℝ
8 7 rspccva ⊢ ∀ n ∈ ℕ f ⁡ n ⊆ ℝ ∧ vol * ⁡ f ⁡ n ∈ ℝ ∧ m ∈ ℕ → f ⁡ m ⊆ ℝ ∧ vol * ⁡ f ⁡ m ∈ ℝ
9 8 simpld ⊢ ∀ n ∈ ℕ f ⁡ n ⊆ ℝ ∧ vol * ⁡ f ⁡ n ∈ ℝ ∧ m ∈ ℕ → f ⁡ m ⊆ ℝ
10 9 adantll ⊢ f Fn ℕ ∧ ∀ n ∈ ℕ f ⁡ n ⊆ ℝ ∧ vol * ⁡ f ⁡ n ∈ ℝ ∧ m ∈ ℕ → f ⁡ m ⊆ ℝ
11 8 simprd ⊢ ∀ n ∈ ℕ f ⁡ n ⊆ ℝ ∧ vol * ⁡ f ⁡ n ∈ ℝ ∧ m ∈ ℕ → vol * ⁡ f ⁡ m ∈ ℝ
12 11 adantll ⊢ f Fn ℕ ∧ ∀ n ∈ ℕ f ⁡ n ⊆ ℝ ∧ vol * ⁡ f ⁡ n ∈ ℝ ∧ m ∈ ℕ → vol * ⁡ f ⁡ m ∈ ℝ
13 1 2 10 12 ovoliun ⊢ f Fn ℕ ∧ ∀ n ∈ ℕ f ⁡ n ⊆ ℝ ∧ vol * ⁡ f ⁡ n ∈ ℝ → vol * ⁡ ⋃ m ∈ ℕ f ⁡ m ≤ sup ran ⁡ seq 1 + m ∈ ℕ ⟼ vol * ⁡ f ⁡ m ℝ * <
14 13 ovoliunnfl ⊢ A ≼ ℕ ∧ ∀ x ∈ A x ≼ ℕ → ⋃ A ≠ ℝ