Metamath Proof Explorer

Theorem volsuplem

Description: Lemma for volsup . (Contributed by Mario Carneiro, 4-Jul-2014)

Ref Expression
Assertion volsuplem ( ( ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∧ ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ) ) → ( 𝐹 ‘ 𝐴 ) ⊆ ( 𝐹 ‘ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 fveq2 ⊢ ( 𝑥 = 𝐴 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝐴 ) )
2 1 sseq2d ⊢ ( 𝑥 = 𝐴 → ( ( 𝐹 ‘ 𝐴 ) ⊆ ( 𝐹 ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝐴 ) ⊆ ( 𝐹 ‘ 𝐴 ) ) )
3 2 imbi2d ⊢ ( 𝑥 = 𝐴 → ( ( ( ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∧ 𝐴 ∈ ℕ ) → ( 𝐹 ‘ 𝐴 ) ⊆ ( 𝐹 ‘ 𝑥 ) ) ↔ ( ( ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∧ 𝐴 ∈ ℕ ) → ( 𝐹 ‘ 𝐴 ) ⊆ ( 𝐹 ‘ 𝐴 ) ) ) )
4 fveq2 ⊢ ( 𝑥 = 𝑘 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑘 ) )
5 4 sseq2d ⊢ ( 𝑥 = 𝑘 → ( ( 𝐹 ‘ 𝐴 ) ⊆ ( 𝐹 ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝐴 ) ⊆ ( 𝐹 ‘ 𝑘 ) ) )
6 5 imbi2d ⊢ ( 𝑥 = 𝑘 → ( ( ( ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∧ 𝐴 ∈ ℕ ) → ( 𝐹 ‘ 𝐴 ) ⊆ ( 𝐹 ‘ 𝑥 ) ) ↔ ( ( ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∧ 𝐴 ∈ ℕ ) → ( 𝐹 ‘ 𝐴 ) ⊆ ( 𝐹 ‘ 𝑘 ) ) ) )
7 fveq2 ⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ ( 𝑘 + 1 ) ) )
8 7 sseq2d ⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( ( 𝐹 ‘ 𝐴 ) ⊆ ( 𝐹 ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝐴 ) ⊆ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) )
9 8 imbi2d ⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( ( ( ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∧ 𝐴 ∈ ℕ ) → ( 𝐹 ‘ 𝐴 ) ⊆ ( 𝐹 ‘ 𝑥 ) ) ↔ ( ( ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∧ 𝐴 ∈ ℕ ) → ( 𝐹 ‘ 𝐴 ) ⊆ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) )
10 fveq2 ⊢ ( 𝑥 = 𝐵 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝐵 ) )
11 10 sseq2d ⊢ ( 𝑥 = 𝐵 → ( ( 𝐹 ‘ 𝐴 ) ⊆ ( 𝐹 ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝐴 ) ⊆ ( 𝐹 ‘ 𝐵 ) ) )
12 11 imbi2d ⊢ ( 𝑥 = 𝐵 → ( ( ( ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∧ 𝐴 ∈ ℕ ) → ( 𝐹 ‘ 𝐴 ) ⊆ ( 𝐹 ‘ 𝑥 ) ) ↔ ( ( ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∧ 𝐴 ∈ ℕ ) → ( 𝐹 ‘ 𝐴 ) ⊆ ( 𝐹 ‘ 𝐵 ) ) ) )
13 ssid ⊢ ( 𝐹 ‘ 𝐴 ) ⊆ ( 𝐹 ‘ 𝐴 )
14 13 2a1i ⊢ ( 𝐴 ∈ ℤ → ( ( ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∧ 𝐴 ∈ ℕ ) → ( 𝐹 ‘ 𝐴 ) ⊆ ( 𝐹 ‘ 𝐴 ) ) )
15 eluznn ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝐴 ) ) → 𝑘 ∈ ℕ )
16 fveq2 ⊢ ( 𝑛 = 𝑘 → ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑘 ) )
17 fvoveq1 ⊢ ( 𝑛 = 𝑘 → ( 𝐹 ‘ ( 𝑛 + 1 ) ) = ( 𝐹 ‘ ( 𝑘 + 1 ) ) )
18 16 17 sseq12d ⊢ ( 𝑛 = 𝑘 → ( ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ↔ ( 𝐹 ‘ 𝑘 ) ⊆ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) )
19 18 rspccva ⊢ ( ( ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ 𝑘 ) ⊆ ( 𝐹 ‘ ( 𝑘 + 1 ) ) )
20 15 19 sylan2 ⊢ ( ( ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∧ ( 𝐴 ∈ ℕ ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝐴 ) ) ) → ( 𝐹 ‘ 𝑘 ) ⊆ ( 𝐹 ‘ ( 𝑘 + 1 ) ) )
21 20 anassrs ⊢ ( ( ( ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∧ 𝐴 ∈ ℕ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( 𝐹 ‘ 𝑘 ) ⊆ ( 𝐹 ‘ ( 𝑘 + 1 ) ) )
22 sstr2 ⊢ ( ( 𝐹 ‘ 𝐴 ) ⊆ ( 𝐹 ‘ 𝑘 ) → ( ( 𝐹 ‘ 𝑘 ) ⊆ ( 𝐹 ‘ ( 𝑘 + 1 ) ) → ( 𝐹 ‘ 𝐴 ) ⊆ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) )
23 21 22 syl5com ⊢ ( ( ( ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∧ 𝐴 ∈ ℕ ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( ( 𝐹 ‘ 𝐴 ) ⊆ ( 𝐹 ‘ 𝑘 ) → ( 𝐹 ‘ 𝐴 ) ⊆ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) )
24 23 expcom ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝐴 ) → ( ( ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∧ 𝐴 ∈ ℕ ) → ( ( 𝐹 ‘ 𝐴 ) ⊆ ( 𝐹 ‘ 𝑘 ) → ( 𝐹 ‘ 𝐴 ) ⊆ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) )
25 24 a2d ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝐴 ) → ( ( ( ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∧ 𝐴 ∈ ℕ ) → ( 𝐹 ‘ 𝐴 ) ⊆ ( 𝐹 ‘ 𝑘 ) ) → ( ( ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∧ 𝐴 ∈ ℕ ) → ( 𝐹 ‘ 𝐴 ) ⊆ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ) )
26 3 6 9 12 14 25 uzind4 ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → ( ( ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∧ 𝐴 ∈ ℕ ) → ( 𝐹 ‘ 𝐴 ) ⊆ ( 𝐹 ‘ 𝐵 ) ) )
27 26 com12 ⊢ ( ( ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∧ 𝐴 ∈ ℕ ) → ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → ( 𝐹 ‘ 𝐴 ) ⊆ ( 𝐹 ‘ 𝐵 ) ) )
28 27 impr ⊢ ( ( ∀ 𝑛 ∈ ℕ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑛 + 1 ) ) ∧ ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ) ) → ( 𝐹 ‘ 𝐴 ) ⊆ ( 𝐹 ‘ 𝐵 ) )