Metamath Proof Explorer

Theorem incssnn0

Description: Transitivity induction of subsets, lemma for nacsfix . (Contributed by Stefan O'Rear, 4-Apr-2015)

Ref Expression
Assertion incssnn0 ( ( ∀ 𝑥 ∈ ℕ0 ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ ( 𝑥 + 1 ) ) ∧ 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( 𝐹 ‘ 𝐴 ) ⊆ ( 𝐹 ‘ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 fveq2 ⊢ ( 𝑎 = 𝐴 → ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝐴 ) )
2 1 sseq2d ⊢ ( 𝑎 = 𝐴 → ( ( 𝐹 ‘ 𝐴 ) ⊆ ( 𝐹 ‘ 𝑎 ) ↔ ( 𝐹 ‘ 𝐴 ) ⊆ ( 𝐹 ‘ 𝐴 ) ) )
3 2 imbi2d ⊢ ( 𝑎 = 𝐴 → ( ( ( ∀ 𝑥 ∈ ℕ0 ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ ( 𝑥 + 1 ) ) ∧ 𝐴 ∈ ℕ0 ) → ( 𝐹 ‘ 𝐴 ) ⊆ ( 𝐹 ‘ 𝑎 ) ) ↔ ( ( ∀ 𝑥 ∈ ℕ0 ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ ( 𝑥 + 1 ) ) ∧ 𝐴 ∈ ℕ0 ) → ( 𝐹 ‘ 𝐴 ) ⊆ ( 𝐹 ‘ 𝐴 ) ) ) )
4 fveq2 ⊢ ( 𝑎 = 𝑏 → ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) )
5 4 sseq2d ⊢ ( 𝑎 = 𝑏 → ( ( 𝐹 ‘ 𝐴 ) ⊆ ( 𝐹 ‘ 𝑎 ) ↔ ( 𝐹 ‘ 𝐴 ) ⊆ ( 𝐹 ‘ 𝑏 ) ) )
6 5 imbi2d ⊢ ( 𝑎 = 𝑏 → ( ( ( ∀ 𝑥 ∈ ℕ0 ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ ( 𝑥 + 1 ) ) ∧ 𝐴 ∈ ℕ0 ) → ( 𝐹 ‘ 𝐴 ) ⊆ ( 𝐹 ‘ 𝑎 ) ) ↔ ( ( ∀ 𝑥 ∈ ℕ0 ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ ( 𝑥 + 1 ) ) ∧ 𝐴 ∈ ℕ0 ) → ( 𝐹 ‘ 𝐴 ) ⊆ ( 𝐹 ‘ 𝑏 ) ) ) )
7 fveq2 ⊢ ( 𝑎 = ( 𝑏 + 1 ) → ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑏 + 1 ) ) )
8 7 sseq2d ⊢ ( 𝑎 = ( 𝑏 + 1 ) → ( ( 𝐹 ‘ 𝐴 ) ⊆ ( 𝐹 ‘ 𝑎 ) ↔ ( 𝐹 ‘ 𝐴 ) ⊆ ( 𝐹 ‘ ( 𝑏 + 1 ) ) ) )
9 8 imbi2d ⊢ ( 𝑎 = ( 𝑏 + 1 ) → ( ( ( ∀ 𝑥 ∈ ℕ0 ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ ( 𝑥 + 1 ) ) ∧ 𝐴 ∈ ℕ0 ) → ( 𝐹 ‘ 𝐴 ) ⊆ ( 𝐹 ‘ 𝑎 ) ) ↔ ( ( ∀ 𝑥 ∈ ℕ0 ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ ( 𝑥 + 1 ) ) ∧ 𝐴 ∈ ℕ0 ) → ( 𝐹 ‘ 𝐴 ) ⊆ ( 𝐹 ‘ ( 𝑏 + 1 ) ) ) ) )
10 fveq2 ⊢ ( 𝑎 = 𝐵 → ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝐵 ) )
11 10 sseq2d ⊢ ( 𝑎 = 𝐵 → ( ( 𝐹 ‘ 𝐴 ) ⊆ ( 𝐹 ‘ 𝑎 ) ↔ ( 𝐹 ‘ 𝐴 ) ⊆ ( 𝐹 ‘ 𝐵 ) ) )
12 11 imbi2d ⊢ ( 𝑎 = 𝐵 → ( ( ( ∀ 𝑥 ∈ ℕ0 ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ ( 𝑥 + 1 ) ) ∧ 𝐴 ∈ ℕ0 ) → ( 𝐹 ‘ 𝐴 ) ⊆ ( 𝐹 ‘ 𝑎 ) ) ↔ ( ( ∀ 𝑥 ∈ ℕ0 ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ ( 𝑥 + 1 ) ) ∧ 𝐴 ∈ ℕ0 ) → ( 𝐹 ‘ 𝐴 ) ⊆ ( 𝐹 ‘ 𝐵 ) ) ) )
13 ssid ⊢ ( 𝐹 ‘ 𝐴 ) ⊆ ( 𝐹 ‘ 𝐴 )
14 13 2a1i ⊢ ( 𝐴 ∈ ℤ → ( ( ∀ 𝑥 ∈ ℕ0 ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ ( 𝑥 + 1 ) ) ∧ 𝐴 ∈ ℕ0 ) → ( 𝐹 ‘ 𝐴 ) ⊆ ( 𝐹 ‘ 𝐴 ) ) )
15 eluznn0 ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝑏 ∈ ( ℤ≥ ‘ 𝐴 ) ) → 𝑏 ∈ ℕ0 )
16 15 ancoms ⊢ ( ( 𝑏 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐴 ∈ ℕ0 ) → 𝑏 ∈ ℕ0 )
17 fveq2 ⊢ ( 𝑥 = 𝑏 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑏 ) )
18 fvoveq1 ⊢ ( 𝑥 = 𝑏 → ( 𝐹 ‘ ( 𝑥 + 1 ) ) = ( 𝐹 ‘ ( 𝑏 + 1 ) ) )
19 17 18 sseq12d ⊢ ( 𝑥 = 𝑏 → ( ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ ( 𝑥 + 1 ) ) ↔ ( 𝐹 ‘ 𝑏 ) ⊆ ( 𝐹 ‘ ( 𝑏 + 1 ) ) ) )
20 19 rspcv ⊢ ( 𝑏 ∈ ℕ0 → ( ∀ 𝑥 ∈ ℕ0 ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ ( 𝑥 + 1 ) ) → ( 𝐹 ‘ 𝑏 ) ⊆ ( 𝐹 ‘ ( 𝑏 + 1 ) ) ) )
21 16 20 syl ⊢ ( ( 𝑏 ∈ ( ℤ≥ ‘ 𝐴 ) ∧ 𝐴 ∈ ℕ0 ) → ( ∀ 𝑥 ∈ ℕ0 ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ ( 𝑥 + 1 ) ) → ( 𝐹 ‘ 𝑏 ) ⊆ ( 𝐹 ‘ ( 𝑏 + 1 ) ) ) )
22 21 expimpd ⊢ ( 𝑏 ∈ ( ℤ≥ ‘ 𝐴 ) → ( ( 𝐴 ∈ ℕ0 ∧ ∀ 𝑥 ∈ ℕ0 ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ ( 𝑥 + 1 ) ) ) → ( 𝐹 ‘ 𝑏 ) ⊆ ( 𝐹 ‘ ( 𝑏 + 1 ) ) ) )
23 22 ancomsd ⊢ ( 𝑏 ∈ ( ℤ≥ ‘ 𝐴 ) → ( ( ∀ 𝑥 ∈ ℕ0 ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ ( 𝑥 + 1 ) ) ∧ 𝐴 ∈ ℕ0 ) → ( 𝐹 ‘ 𝑏 ) ⊆ ( 𝐹 ‘ ( 𝑏 + 1 ) ) ) )
24 sstr2 ⊢ ( ( 𝐹 ‘ 𝐴 ) ⊆ ( 𝐹 ‘ 𝑏 ) → ( ( 𝐹 ‘ 𝑏 ) ⊆ ( 𝐹 ‘ ( 𝑏 + 1 ) ) → ( 𝐹 ‘ 𝐴 ) ⊆ ( 𝐹 ‘ ( 𝑏 + 1 ) ) ) )
25 24 com12 ⊢ ( ( 𝐹 ‘ 𝑏 ) ⊆ ( 𝐹 ‘ ( 𝑏 + 1 ) ) → ( ( 𝐹 ‘ 𝐴 ) ⊆ ( 𝐹 ‘ 𝑏 ) → ( 𝐹 ‘ 𝐴 ) ⊆ ( 𝐹 ‘ ( 𝑏 + 1 ) ) ) )
26 23 25 syl6 ⊢ ( 𝑏 ∈ ( ℤ≥ ‘ 𝐴 ) → ( ( ∀ 𝑥 ∈ ℕ0 ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ ( 𝑥 + 1 ) ) ∧ 𝐴 ∈ ℕ0 ) → ( ( 𝐹 ‘ 𝐴 ) ⊆ ( 𝐹 ‘ 𝑏 ) → ( 𝐹 ‘ 𝐴 ) ⊆ ( 𝐹 ‘ ( 𝑏 + 1 ) ) ) ) )
27 26 a2d ⊢ ( 𝑏 ∈ ( ℤ≥ ‘ 𝐴 ) → ( ( ( ∀ 𝑥 ∈ ℕ0 ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ ( 𝑥 + 1 ) ) ∧ 𝐴 ∈ ℕ0 ) → ( 𝐹 ‘ 𝐴 ) ⊆ ( 𝐹 ‘ 𝑏 ) ) → ( ( ∀ 𝑥 ∈ ℕ0 ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ ( 𝑥 + 1 ) ) ∧ 𝐴 ∈ ℕ0 ) → ( 𝐹 ‘ 𝐴 ) ⊆ ( 𝐹 ‘ ( 𝑏 + 1 ) ) ) ) )
28 3 6 9 12 14 27 uzind4 ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → ( ( ∀ 𝑥 ∈ ℕ0 ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ ( 𝑥 + 1 ) ) ∧ 𝐴 ∈ ℕ0 ) → ( 𝐹 ‘ 𝐴 ) ⊆ ( 𝐹 ‘ 𝐵 ) ) )
29 28 com12 ⊢ ( ( ∀ 𝑥 ∈ ℕ0 ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ ( 𝑥 + 1 ) ) ∧ 𝐴 ∈ ℕ0 ) → ( 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) → ( 𝐹 ‘ 𝐴 ) ⊆ ( 𝐹 ‘ 𝐵 ) ) )
30 29 3impia ⊢ ( ( ∀ 𝑥 ∈ ℕ0 ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ ( 𝑥 + 1 ) ) ∧ 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ( ℤ≥ ‘ 𝐴 ) ) → ( 𝐹 ‘ 𝐴 ) ⊆ ( 𝐹 ‘ 𝐵 ) )