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 ) ) ∧ ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ( ℤ𝐴 ) ) ) → ( 𝐹𝐴 ) ⊆ ( 𝐹𝐵 ) )