Theorem ex-ovoliunnfl

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

	Ref	Expression
Assertion	ex-ovoliunnfl	⊢ ( ( 𝐴 ≼ ℕ ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≼ ℕ ) → ∪ 𝐴 ≠ ℝ )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ seq 1 ( + , ( 𝑚 ∈ ℕ ↦ ( vol* ‘ ( 𝑓 ‘ 𝑚 ) ) ) ) = seq 1 ( + , ( 𝑚 ∈ ℕ ↦ ( vol* ‘ ( 𝑓 ‘ 𝑚 ) ) ) )
2		eqid	⊢ ( 𝑚 ∈ ℕ ↦ ( vol* ‘ ( 𝑓 ‘ 𝑚 ) ) ) = ( 𝑚 ∈ ℕ ↦ ( vol* ‘ ( 𝑓 ‘ 𝑚 ) ) )
3		fveq2	⊢ ( 𝑛 = 𝑚 → ( 𝑓 ‘ 𝑛 ) = ( 𝑓 ‘ 𝑚 ) )
4	3	sseq1d	⊢ ( 𝑛 = 𝑚 → ( ( 𝑓 ‘ 𝑛 ) ⊆ ℝ ↔ ( 𝑓 ‘ 𝑚 ) ⊆ ℝ ) )
5		2fveq3	⊢ ( 𝑛 = 𝑚 → ( vol* ‘ ( 𝑓 ‘ 𝑛 ) ) = ( vol* ‘ ( 𝑓 ‘ 𝑚 ) ) )
6	5	eleq1d	⊢ ( 𝑛 = 𝑚 → ( ( vol* ‘ ( 𝑓 ‘ 𝑛 ) ) ∈ ℝ ↔ ( vol* ‘ ( 𝑓 ‘ 𝑚 ) ) ∈ ℝ ) )
7	4 6	anbi12d	⊢ ( 𝑛 = 𝑚 → ( ( ( 𝑓 ‘ 𝑛 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑓 ‘ 𝑛 ) ) ∈ ℝ ) ↔ ( ( 𝑓 ‘ 𝑚 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑓 ‘ 𝑚 ) ) ∈ ℝ ) ) )
8	7	rspccva	⊢ ( ( ∀ 𝑛 ∈ ℕ ( ( 𝑓 ‘ 𝑛 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑓 ‘ 𝑛 ) ) ∈ ℝ ) ∧ 𝑚 ∈ ℕ ) → ( ( 𝑓 ‘ 𝑚 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑓 ‘ 𝑚 ) ) ∈ ℝ ) )
9	8	simpld	⊢ ( ( ∀ 𝑛 ∈ ℕ ( ( 𝑓 ‘ 𝑛 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑓 ‘ 𝑛 ) ) ∈ ℝ ) ∧ 𝑚 ∈ ℕ ) → ( 𝑓 ‘ 𝑚 ) ⊆ ℝ )
10	9	adantll	⊢ ( ( ( 𝑓 Fn ℕ ∧ ∀ 𝑛 ∈ ℕ ( ( 𝑓 ‘ 𝑛 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑓 ‘ 𝑛 ) ) ∈ ℝ ) ) ∧ 𝑚 ∈ ℕ ) → ( 𝑓 ‘ 𝑚 ) ⊆ ℝ )
11	8	simprd	⊢ ( ( ∀ 𝑛 ∈ ℕ ( ( 𝑓 ‘ 𝑛 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑓 ‘ 𝑛 ) ) ∈ ℝ ) ∧ 𝑚 ∈ ℕ ) → ( vol* ‘ ( 𝑓 ‘ 𝑚 ) ) ∈ ℝ )
12	11	adantll	⊢ ( ( ( 𝑓 Fn ℕ ∧ ∀ 𝑛 ∈ ℕ ( ( 𝑓 ‘ 𝑛 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑓 ‘ 𝑛 ) ) ∈ ℝ ) ) ∧ 𝑚 ∈ ℕ ) → ( vol* ‘ ( 𝑓 ‘ 𝑚 ) ) ∈ ℝ )
13	1 2 10 12	ovoliun	⊢ ( ( 𝑓 Fn ℕ ∧ ∀ 𝑛 ∈ ℕ ( ( 𝑓 ‘ 𝑛 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑓 ‘ 𝑛 ) ) ∈ ℝ ) ) → ( vol* ‘ ∪ 𝑚 ∈ ℕ ( 𝑓 ‘ 𝑚 ) ) ≤ sup ( ran seq 1 ( + , ( 𝑚 ∈ ℕ ↦ ( vol* ‘ ( 𝑓 ‘ 𝑚 ) ) ) ) , ℝ* , < ) )
14	13	ovoliunnfl	⊢ ( ( 𝐴 ≼ ℕ ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≼ ℕ ) → ∪ 𝐴 ≠ ℝ )