Metamath Proof Explorer

Theorem seqpo

Description: Two ways to say that a sequence respects a partial order. (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Assertion seqpo ( ( 𝑅 Po 𝐴 ∧ 𝐹 : ℕ ⟶ 𝐴 ) → ( ∀ 𝑠 ∈ ℕ ( 𝐹 ‘ 𝑠 ) 𝑅 ( 𝐹 ‘ ( 𝑠 + 1 ) ) ↔ ∀ 𝑚 ∈ ℕ ∀ 𝑛 ∈ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ( 𝐹 ‘ 𝑚 ) 𝑅 ( 𝐹 ‘ 𝑛 ) ) )

Proof

Step Hyp Ref Expression
1 fveq2 ⊢ ( 𝑝 = ( 𝑚 + 1 ) → ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ ( 𝑚 + 1 ) ) )
2 1 breq2d ⊢ ( 𝑝 = ( 𝑚 + 1 ) → ( ( 𝐹 ‘ 𝑚 ) 𝑅 ( 𝐹 ‘ 𝑝 ) ↔ ( 𝐹 ‘ 𝑚 ) 𝑅 ( 𝐹 ‘ ( 𝑚 + 1 ) ) ) )
3 2 imbi2d ⊢ ( 𝑝 = ( 𝑚 + 1 ) → ( ( ( ( 𝑅 Po 𝐴 ∧ 𝐹 : ℕ ⟶ 𝐴 ) ∧ ( ∀ 𝑠 ∈ ℕ ( 𝐹 ‘ 𝑠 ) 𝑅 ( 𝐹 ‘ ( 𝑠 + 1 ) ) ∧ 𝑚 ∈ ℕ ) ) → ( 𝐹 ‘ 𝑚 ) 𝑅 ( 𝐹 ‘ 𝑝 ) ) ↔ ( ( ( 𝑅 Po 𝐴 ∧ 𝐹 : ℕ ⟶ 𝐴 ) ∧ ( ∀ 𝑠 ∈ ℕ ( 𝐹 ‘ 𝑠 ) 𝑅 ( 𝐹 ‘ ( 𝑠 + 1 ) ) ∧ 𝑚 ∈ ℕ ) ) → ( 𝐹 ‘ 𝑚 ) 𝑅 ( 𝐹 ‘ ( 𝑚 + 1 ) ) ) ) )
4 fveq2 ⊢ ( 𝑝 = 𝑞 → ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑞 ) )
5 4 breq2d ⊢ ( 𝑝 = 𝑞 → ( ( 𝐹 ‘ 𝑚 ) 𝑅 ( 𝐹 ‘ 𝑝 ) ↔ ( 𝐹 ‘ 𝑚 ) 𝑅 ( 𝐹 ‘ 𝑞 ) ) )
6 5 imbi2d ⊢ ( 𝑝 = 𝑞 → ( ( ( ( 𝑅 Po 𝐴 ∧ 𝐹 : ℕ ⟶ 𝐴 ) ∧ ( ∀ 𝑠 ∈ ℕ ( 𝐹 ‘ 𝑠 ) 𝑅 ( 𝐹 ‘ ( 𝑠 + 1 ) ) ∧ 𝑚 ∈ ℕ ) ) → ( 𝐹 ‘ 𝑚 ) 𝑅 ( 𝐹 ‘ 𝑝 ) ) ↔ ( ( ( 𝑅 Po 𝐴 ∧ 𝐹 : ℕ ⟶ 𝐴 ) ∧ ( ∀ 𝑠 ∈ ℕ ( 𝐹 ‘ 𝑠 ) 𝑅 ( 𝐹 ‘ ( 𝑠 + 1 ) ) ∧ 𝑚 ∈ ℕ ) ) → ( 𝐹 ‘ 𝑚 ) 𝑅 ( 𝐹 ‘ 𝑞 ) ) ) )
7 fveq2 ⊢ ( 𝑝 = ( 𝑞 + 1 ) → ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ ( 𝑞 + 1 ) ) )
8 7 breq2d ⊢ ( 𝑝 = ( 𝑞 + 1 ) → ( ( 𝐹 ‘ 𝑚 ) 𝑅 ( 𝐹 ‘ 𝑝 ) ↔ ( 𝐹 ‘ 𝑚 ) 𝑅 ( 𝐹 ‘ ( 𝑞 + 1 ) ) ) )
9 8 imbi2d ⊢ ( 𝑝 = ( 𝑞 + 1 ) → ( ( ( ( 𝑅 Po 𝐴 ∧ 𝐹 : ℕ ⟶ 𝐴 ) ∧ ( ∀ 𝑠 ∈ ℕ ( 𝐹 ‘ 𝑠 ) 𝑅 ( 𝐹 ‘ ( 𝑠 + 1 ) ) ∧ 𝑚 ∈ ℕ ) ) → ( 𝐹 ‘ 𝑚 ) 𝑅 ( 𝐹 ‘ 𝑝 ) ) ↔ ( ( ( 𝑅 Po 𝐴 ∧ 𝐹 : ℕ ⟶ 𝐴 ) ∧ ( ∀ 𝑠 ∈ ℕ ( 𝐹 ‘ 𝑠 ) 𝑅 ( 𝐹 ‘ ( 𝑠 + 1 ) ) ∧ 𝑚 ∈ ℕ ) ) → ( 𝐹 ‘ 𝑚 ) 𝑅 ( 𝐹 ‘ ( 𝑞 + 1 ) ) ) ) )
10 fveq2 ⊢ ( 𝑝 = 𝑛 → ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑛 ) )
11 10 breq2d ⊢ ( 𝑝 = 𝑛 → ( ( 𝐹 ‘ 𝑚 ) 𝑅 ( 𝐹 ‘ 𝑝 ) ↔ ( 𝐹 ‘ 𝑚 ) 𝑅 ( 𝐹 ‘ 𝑛 ) ) )
12 11 imbi2d ⊢ ( 𝑝 = 𝑛 → ( ( ( ( 𝑅 Po 𝐴 ∧ 𝐹 : ℕ ⟶ 𝐴 ) ∧ ( ∀ 𝑠 ∈ ℕ ( 𝐹 ‘ 𝑠 ) 𝑅 ( 𝐹 ‘ ( 𝑠 + 1 ) ) ∧ 𝑚 ∈ ℕ ) ) → ( 𝐹 ‘ 𝑚 ) 𝑅 ( 𝐹 ‘ 𝑝 ) ) ↔ ( ( ( 𝑅 Po 𝐴 ∧ 𝐹 : ℕ ⟶ 𝐴 ) ∧ ( ∀ 𝑠 ∈ ℕ ( 𝐹 ‘ 𝑠 ) 𝑅 ( 𝐹 ‘ ( 𝑠 + 1 ) ) ∧ 𝑚 ∈ ℕ ) ) → ( 𝐹 ‘ 𝑚 ) 𝑅 ( 𝐹 ‘ 𝑛 ) ) ) )
13 fveq2 ⊢ ( 𝑠 = 𝑚 → ( 𝐹 ‘ 𝑠 ) = ( 𝐹 ‘ 𝑚 ) )
14 fvoveq1 ⊢ ( 𝑠 = 𝑚 → ( 𝐹 ‘ ( 𝑠 + 1 ) ) = ( 𝐹 ‘ ( 𝑚 + 1 ) ) )
15 13 14 breq12d ⊢ ( 𝑠 = 𝑚 → ( ( 𝐹 ‘ 𝑠 ) 𝑅 ( 𝐹 ‘ ( 𝑠 + 1 ) ) ↔ ( 𝐹 ‘ 𝑚 ) 𝑅 ( 𝐹 ‘ ( 𝑚 + 1 ) ) ) )
16 15 rspccva ⊢ ( ( ∀ 𝑠 ∈ ℕ ( 𝐹 ‘ 𝑠 ) 𝑅 ( 𝐹 ‘ ( 𝑠 + 1 ) ) ∧ 𝑚 ∈ ℕ ) → ( 𝐹 ‘ 𝑚 ) 𝑅 ( 𝐹 ‘ ( 𝑚 + 1 ) ) )
17 16 adantl ⊢ ( ( ( 𝑅 Po 𝐴 ∧ 𝐹 : ℕ ⟶ 𝐴 ) ∧ ( ∀ 𝑠 ∈ ℕ ( 𝐹 ‘ 𝑠 ) 𝑅 ( 𝐹 ‘ ( 𝑠 + 1 ) ) ∧ 𝑚 ∈ ℕ ) ) → ( 𝐹 ‘ 𝑚 ) 𝑅 ( 𝐹 ‘ ( 𝑚 + 1 ) ) )
18 17 a1i ⊢ ( ( 𝑚 + 1 ) ∈ ℤ → ( ( ( 𝑅 Po 𝐴 ∧ 𝐹 : ℕ ⟶ 𝐴 ) ∧ ( ∀ 𝑠 ∈ ℕ ( 𝐹 ‘ 𝑠 ) 𝑅 ( 𝐹 ‘ ( 𝑠 + 1 ) ) ∧ 𝑚 ∈ ℕ ) ) → ( 𝐹 ‘ 𝑚 ) 𝑅 ( 𝐹 ‘ ( 𝑚 + 1 ) ) ) )
19 peano2nn ⊢ ( 𝑚 ∈ ℕ → ( 𝑚 + 1 ) ∈ ℕ )
20 elnnuz ⊢ ( ( 𝑚 + 1 ) ∈ ℕ ↔ ( 𝑚 + 1 ) ∈ ( ℤ≥ ‘ 1 ) )
21 19 20 sylib ⊢ ( 𝑚 ∈ ℕ → ( 𝑚 + 1 ) ∈ ( ℤ≥ ‘ 1 ) )
22 uztrn ⊢ ( ( 𝑞 ∈ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ∧ ( 𝑚 + 1 ) ∈ ( ℤ≥ ‘ 1 ) ) → 𝑞 ∈ ( ℤ≥ ‘ 1 ) )
23 elnnuz ⊢ ( 𝑞 ∈ ℕ ↔ 𝑞 ∈ ( ℤ≥ ‘ 1 ) )
24 22 23 sylibr ⊢ ( ( 𝑞 ∈ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ∧ ( 𝑚 + 1 ) ∈ ( ℤ≥ ‘ 1 ) ) → 𝑞 ∈ ℕ )
25 24 expcom ⊢ ( ( 𝑚 + 1 ) ∈ ( ℤ≥ ‘ 1 ) → ( 𝑞 ∈ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) → 𝑞 ∈ ℕ ) )
26 21 25 syl ⊢ ( 𝑚 ∈ ℕ → ( 𝑞 ∈ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) → 𝑞 ∈ ℕ ) )
27 26 imdistani ⊢ ( ( 𝑚 ∈ ℕ ∧ 𝑞 ∈ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ) → ( 𝑚 ∈ ℕ ∧ 𝑞 ∈ ℕ ) )
28 fveq2 ⊢ ( 𝑠 = 𝑞 → ( 𝐹 ‘ 𝑠 ) = ( 𝐹 ‘ 𝑞 ) )
29 fvoveq1 ⊢ ( 𝑠 = 𝑞 → ( 𝐹 ‘ ( 𝑠 + 1 ) ) = ( 𝐹 ‘ ( 𝑞 + 1 ) ) )
30 28 29 breq12d ⊢ ( 𝑠 = 𝑞 → ( ( 𝐹 ‘ 𝑠 ) 𝑅 ( 𝐹 ‘ ( 𝑠 + 1 ) ) ↔ ( 𝐹 ‘ 𝑞 ) 𝑅 ( 𝐹 ‘ ( 𝑞 + 1 ) ) ) )
31 30 rspccva ⊢ ( ( ∀ 𝑠 ∈ ℕ ( 𝐹 ‘ 𝑠 ) 𝑅 ( 𝐹 ‘ ( 𝑠 + 1 ) ) ∧ 𝑞 ∈ ℕ ) → ( 𝐹 ‘ 𝑞 ) 𝑅 ( 𝐹 ‘ ( 𝑞 + 1 ) ) )
32 31 ad2ant2l ⊢ ( ( ( ( 𝑅 Po 𝐴 ∧ 𝐹 : ℕ ⟶ 𝐴 ) ∧ ∀ 𝑠 ∈ ℕ ( 𝐹 ‘ 𝑠 ) 𝑅 ( 𝐹 ‘ ( 𝑠 + 1 ) ) ) ∧ ( 𝑚 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → ( 𝐹 ‘ 𝑞 ) 𝑅 ( 𝐹 ‘ ( 𝑞 + 1 ) ) )
33 32 ex ⊢ ( ( ( 𝑅 Po 𝐴 ∧ 𝐹 : ℕ ⟶ 𝐴 ) ∧ ∀ 𝑠 ∈ ℕ ( 𝐹 ‘ 𝑠 ) 𝑅 ( 𝐹 ‘ ( 𝑠 + 1 ) ) ) → ( ( 𝑚 ∈ ℕ ∧ 𝑞 ∈ ℕ ) → ( 𝐹 ‘ 𝑞 ) 𝑅 ( 𝐹 ‘ ( 𝑞 + 1 ) ) ) )
34 ffvelcdm ⊢ ( ( 𝐹 : ℕ ⟶ 𝐴 ∧ 𝑚 ∈ ℕ ) → ( 𝐹 ‘ 𝑚 ) ∈ 𝐴 )
35 34 adantrr ⊢ ( ( 𝐹 : ℕ ⟶ 𝐴 ∧ ( 𝑚 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → ( 𝐹 ‘ 𝑚 ) ∈ 𝐴 )
36 ffvelcdm ⊢ ( ( 𝐹 : ℕ ⟶ 𝐴 ∧ 𝑞 ∈ ℕ ) → ( 𝐹 ‘ 𝑞 ) ∈ 𝐴 )
37 36 adantrl ⊢ ( ( 𝐹 : ℕ ⟶ 𝐴 ∧ ( 𝑚 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → ( 𝐹 ‘ 𝑞 ) ∈ 𝐴 )
38 peano2nn ⊢ ( 𝑞 ∈ ℕ → ( 𝑞 + 1 ) ∈ ℕ )
39 ffvelcdm ⊢ ( ( 𝐹 : ℕ ⟶ 𝐴 ∧ ( 𝑞 + 1 ) ∈ ℕ ) → ( 𝐹 ‘ ( 𝑞 + 1 ) ) ∈ 𝐴 )
40 38 39 sylan2 ⊢ ( ( 𝐹 : ℕ ⟶ 𝐴 ∧ 𝑞 ∈ ℕ ) → ( 𝐹 ‘ ( 𝑞 + 1 ) ) ∈ 𝐴 )
41 40 adantrl ⊢ ( ( 𝐹 : ℕ ⟶ 𝐴 ∧ ( 𝑚 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → ( 𝐹 ‘ ( 𝑞 + 1 ) ) ∈ 𝐴 )
42 35 37 41 3jca ⊢ ( ( 𝐹 : ℕ ⟶ 𝐴 ∧ ( 𝑚 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → ( ( 𝐹 ‘ 𝑚 ) ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑞 ) ∈ 𝐴 ∧ ( 𝐹 ‘ ( 𝑞 + 1 ) ) ∈ 𝐴 ) )
43 potr ⊢ ( ( 𝑅 Po 𝐴 ∧ ( ( 𝐹 ‘ 𝑚 ) ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑞 ) ∈ 𝐴 ∧ ( 𝐹 ‘ ( 𝑞 + 1 ) ) ∈ 𝐴 ) ) → ( ( ( 𝐹 ‘ 𝑚 ) 𝑅 ( 𝐹 ‘ 𝑞 ) ∧ ( 𝐹 ‘ 𝑞 ) 𝑅 ( 𝐹 ‘ ( 𝑞 + 1 ) ) ) → ( 𝐹 ‘ 𝑚 ) 𝑅 ( 𝐹 ‘ ( 𝑞 + 1 ) ) ) )
44 43 expcomd ⊢ ( ( 𝑅 Po 𝐴 ∧ ( ( 𝐹 ‘ 𝑚 ) ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑞 ) ∈ 𝐴 ∧ ( 𝐹 ‘ ( 𝑞 + 1 ) ) ∈ 𝐴 ) ) → ( ( 𝐹 ‘ 𝑞 ) 𝑅 ( 𝐹 ‘ ( 𝑞 + 1 ) ) → ( ( 𝐹 ‘ 𝑚 ) 𝑅 ( 𝐹 ‘ 𝑞 ) → ( 𝐹 ‘ 𝑚 ) 𝑅 ( 𝐹 ‘ ( 𝑞 + 1 ) ) ) ) )
45 44 ex ⊢ ( 𝑅 Po 𝐴 → ( ( ( 𝐹 ‘ 𝑚 ) ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑞 ) ∈ 𝐴 ∧ ( 𝐹 ‘ ( 𝑞 + 1 ) ) ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑞 ) 𝑅 ( 𝐹 ‘ ( 𝑞 + 1 ) ) → ( ( 𝐹 ‘ 𝑚 ) 𝑅 ( 𝐹 ‘ 𝑞 ) → ( 𝐹 ‘ 𝑚 ) 𝑅 ( 𝐹 ‘ ( 𝑞 + 1 ) ) ) ) ) )
46 42 45 syl5 ⊢ ( 𝑅 Po 𝐴 → ( ( 𝐹 : ℕ ⟶ 𝐴 ∧ ( 𝑚 ∈ ℕ ∧ 𝑞 ∈ ℕ ) ) → ( ( 𝐹 ‘ 𝑞 ) 𝑅 ( 𝐹 ‘ ( 𝑞 + 1 ) ) → ( ( 𝐹 ‘ 𝑚 ) 𝑅 ( 𝐹 ‘ 𝑞 ) → ( 𝐹 ‘ 𝑚 ) 𝑅 ( 𝐹 ‘ ( 𝑞 + 1 ) ) ) ) ) )
47 46 expdimp ⊢ ( ( 𝑅 Po 𝐴 ∧ 𝐹 : ℕ ⟶ 𝐴 ) → ( ( 𝑚 ∈ ℕ ∧ 𝑞 ∈ ℕ ) → ( ( 𝐹 ‘ 𝑞 ) 𝑅 ( 𝐹 ‘ ( 𝑞 + 1 ) ) → ( ( 𝐹 ‘ 𝑚 ) 𝑅 ( 𝐹 ‘ 𝑞 ) → ( 𝐹 ‘ 𝑚 ) 𝑅 ( 𝐹 ‘ ( 𝑞 + 1 ) ) ) ) ) )
48 47 adantr ⊢ ( ( ( 𝑅 Po 𝐴 ∧ 𝐹 : ℕ ⟶ 𝐴 ) ∧ ∀ 𝑠 ∈ ℕ ( 𝐹 ‘ 𝑠 ) 𝑅 ( 𝐹 ‘ ( 𝑠 + 1 ) ) ) → ( ( 𝑚 ∈ ℕ ∧ 𝑞 ∈ ℕ ) → ( ( 𝐹 ‘ 𝑞 ) 𝑅 ( 𝐹 ‘ ( 𝑞 + 1 ) ) → ( ( 𝐹 ‘ 𝑚 ) 𝑅 ( 𝐹 ‘ 𝑞 ) → ( 𝐹 ‘ 𝑚 ) 𝑅 ( 𝐹 ‘ ( 𝑞 + 1 ) ) ) ) ) )
49 33 48 mpdd ⊢ ( ( ( 𝑅 Po 𝐴 ∧ 𝐹 : ℕ ⟶ 𝐴 ) ∧ ∀ 𝑠 ∈ ℕ ( 𝐹 ‘ 𝑠 ) 𝑅 ( 𝐹 ‘ ( 𝑠 + 1 ) ) ) → ( ( 𝑚 ∈ ℕ ∧ 𝑞 ∈ ℕ ) → ( ( 𝐹 ‘ 𝑚 ) 𝑅 ( 𝐹 ‘ 𝑞 ) → ( 𝐹 ‘ 𝑚 ) 𝑅 ( 𝐹 ‘ ( 𝑞 + 1 ) ) ) ) )
50 27 49 syl5 ⊢ ( ( ( 𝑅 Po 𝐴 ∧ 𝐹 : ℕ ⟶ 𝐴 ) ∧ ∀ 𝑠 ∈ ℕ ( 𝐹 ‘ 𝑠 ) 𝑅 ( 𝐹 ‘ ( 𝑠 + 1 ) ) ) → ( ( 𝑚 ∈ ℕ ∧ 𝑞 ∈ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ) → ( ( 𝐹 ‘ 𝑚 ) 𝑅 ( 𝐹 ‘ 𝑞 ) → ( 𝐹 ‘ 𝑚 ) 𝑅 ( 𝐹 ‘ ( 𝑞 + 1 ) ) ) ) )
51 50 expdimp ⊢ ( ( ( ( 𝑅 Po 𝐴 ∧ 𝐹 : ℕ ⟶ 𝐴 ) ∧ ∀ 𝑠 ∈ ℕ ( 𝐹 ‘ 𝑠 ) 𝑅 ( 𝐹 ‘ ( 𝑠 + 1 ) ) ) ∧ 𝑚 ∈ ℕ ) → ( 𝑞 ∈ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) → ( ( 𝐹 ‘ 𝑚 ) 𝑅 ( 𝐹 ‘ 𝑞 ) → ( 𝐹 ‘ 𝑚 ) 𝑅 ( 𝐹 ‘ ( 𝑞 + 1 ) ) ) ) )
52 51 anasss ⊢ ( ( ( 𝑅 Po 𝐴 ∧ 𝐹 : ℕ ⟶ 𝐴 ) ∧ ( ∀ 𝑠 ∈ ℕ ( 𝐹 ‘ 𝑠 ) 𝑅 ( 𝐹 ‘ ( 𝑠 + 1 ) ) ∧ 𝑚 ∈ ℕ ) ) → ( 𝑞 ∈ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) → ( ( 𝐹 ‘ 𝑚 ) 𝑅 ( 𝐹 ‘ 𝑞 ) → ( 𝐹 ‘ 𝑚 ) 𝑅 ( 𝐹 ‘ ( 𝑞 + 1 ) ) ) ) )
53 52 com12 ⊢ ( 𝑞 ∈ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) → ( ( ( 𝑅 Po 𝐴 ∧ 𝐹 : ℕ ⟶ 𝐴 ) ∧ ( ∀ 𝑠 ∈ ℕ ( 𝐹 ‘ 𝑠 ) 𝑅 ( 𝐹 ‘ ( 𝑠 + 1 ) ) ∧ 𝑚 ∈ ℕ ) ) → ( ( 𝐹 ‘ 𝑚 ) 𝑅 ( 𝐹 ‘ 𝑞 ) → ( 𝐹 ‘ 𝑚 ) 𝑅 ( 𝐹 ‘ ( 𝑞 + 1 ) ) ) ) )
54 53 a2d ⊢ ( 𝑞 ∈ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) → ( ( ( ( 𝑅 Po 𝐴 ∧ 𝐹 : ℕ ⟶ 𝐴 ) ∧ ( ∀ 𝑠 ∈ ℕ ( 𝐹 ‘ 𝑠 ) 𝑅 ( 𝐹 ‘ ( 𝑠 + 1 ) ) ∧ 𝑚 ∈ ℕ ) ) → ( 𝐹 ‘ 𝑚 ) 𝑅 ( 𝐹 ‘ 𝑞 ) ) → ( ( ( 𝑅 Po 𝐴 ∧ 𝐹 : ℕ ⟶ 𝐴 ) ∧ ( ∀ 𝑠 ∈ ℕ ( 𝐹 ‘ 𝑠 ) 𝑅 ( 𝐹 ‘ ( 𝑠 + 1 ) ) ∧ 𝑚 ∈ ℕ ) ) → ( 𝐹 ‘ 𝑚 ) 𝑅 ( 𝐹 ‘ ( 𝑞 + 1 ) ) ) ) )
55 3 6 9 12 18 54 uzind4 ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) → ( ( ( 𝑅 Po 𝐴 ∧ 𝐹 : ℕ ⟶ 𝐴 ) ∧ ( ∀ 𝑠 ∈ ℕ ( 𝐹 ‘ 𝑠 ) 𝑅 ( 𝐹 ‘ ( 𝑠 + 1 ) ) ∧ 𝑚 ∈ ℕ ) ) → ( 𝐹 ‘ 𝑚 ) 𝑅 ( 𝐹 ‘ 𝑛 ) ) )
56 55 com12 ⊢ ( ( ( 𝑅 Po 𝐴 ∧ 𝐹 : ℕ ⟶ 𝐴 ) ∧ ( ∀ 𝑠 ∈ ℕ ( 𝐹 ‘ 𝑠 ) 𝑅 ( 𝐹 ‘ ( 𝑠 + 1 ) ) ∧ 𝑚 ∈ ℕ ) ) → ( 𝑛 ∈ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) → ( 𝐹 ‘ 𝑚 ) 𝑅 ( 𝐹 ‘ 𝑛 ) ) )
57 56 ralrimiv ⊢ ( ( ( 𝑅 Po 𝐴 ∧ 𝐹 : ℕ ⟶ 𝐴 ) ∧ ( ∀ 𝑠 ∈ ℕ ( 𝐹 ‘ 𝑠 ) 𝑅 ( 𝐹 ‘ ( 𝑠 + 1 ) ) ∧ 𝑚 ∈ ℕ ) ) → ∀ 𝑛 ∈ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ( 𝐹 ‘ 𝑚 ) 𝑅 ( 𝐹 ‘ 𝑛 ) )
58 57 anassrs ⊢ ( ( ( ( 𝑅 Po 𝐴 ∧ 𝐹 : ℕ ⟶ 𝐴 ) ∧ ∀ 𝑠 ∈ ℕ ( 𝐹 ‘ 𝑠 ) 𝑅 ( 𝐹 ‘ ( 𝑠 + 1 ) ) ) ∧ 𝑚 ∈ ℕ ) → ∀ 𝑛 ∈ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ( 𝐹 ‘ 𝑚 ) 𝑅 ( 𝐹 ‘ 𝑛 ) )
59 58 ralrimiva ⊢ ( ( ( 𝑅 Po 𝐴 ∧ 𝐹 : ℕ ⟶ 𝐴 ) ∧ ∀ 𝑠 ∈ ℕ ( 𝐹 ‘ 𝑠 ) 𝑅 ( 𝐹 ‘ ( 𝑠 + 1 ) ) ) → ∀ 𝑚 ∈ ℕ ∀ 𝑛 ∈ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ( 𝐹 ‘ 𝑚 ) 𝑅 ( 𝐹 ‘ 𝑛 ) )
60 59 ex ⊢ ( ( 𝑅 Po 𝐴 ∧ 𝐹 : ℕ ⟶ 𝐴 ) → ( ∀ 𝑠 ∈ ℕ ( 𝐹 ‘ 𝑠 ) 𝑅 ( 𝐹 ‘ ( 𝑠 + 1 ) ) → ∀ 𝑚 ∈ ℕ ∀ 𝑛 ∈ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ( 𝐹 ‘ 𝑚 ) 𝑅 ( 𝐹 ‘ 𝑛 ) ) )
61 fvoveq1 ⊢ ( 𝑚 = 𝑠 → ( ℤ≥ ‘ ( 𝑚 + 1 ) ) = ( ℤ≥ ‘ ( 𝑠 + 1 ) ) )
62 fveq2 ⊢ ( 𝑚 = 𝑠 → ( 𝐹 ‘ 𝑚 ) = ( 𝐹 ‘ 𝑠 ) )
63 62 breq1d ⊢ ( 𝑚 = 𝑠 → ( ( 𝐹 ‘ 𝑚 ) 𝑅 ( 𝐹 ‘ 𝑛 ) ↔ ( 𝐹 ‘ 𝑠 ) 𝑅 ( 𝐹 ‘ 𝑛 ) ) )
64 61 63 raleqbidv ⊢ ( 𝑚 = 𝑠 → ( ∀ 𝑛 ∈ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ( 𝐹 ‘ 𝑚 ) 𝑅 ( 𝐹 ‘ 𝑛 ) ↔ ∀ 𝑛 ∈ ( ℤ≥ ‘ ( 𝑠 + 1 ) ) ( 𝐹 ‘ 𝑠 ) 𝑅 ( 𝐹 ‘ 𝑛 ) ) )
65 64 rspcv ⊢ ( 𝑠 ∈ ℕ → ( ∀ 𝑚 ∈ ℕ ∀ 𝑛 ∈ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ( 𝐹 ‘ 𝑚 ) 𝑅 ( 𝐹 ‘ 𝑛 ) → ∀ 𝑛 ∈ ( ℤ≥ ‘ ( 𝑠 + 1 ) ) ( 𝐹 ‘ 𝑠 ) 𝑅 ( 𝐹 ‘ 𝑛 ) ) )
66 65 imdistanri ⊢ ( ( ∀ 𝑚 ∈ ℕ ∀ 𝑛 ∈ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ( 𝐹 ‘ 𝑚 ) 𝑅 ( 𝐹 ‘ 𝑛 ) ∧ 𝑠 ∈ ℕ ) → ( ∀ 𝑛 ∈ ( ℤ≥ ‘ ( 𝑠 + 1 ) ) ( 𝐹 ‘ 𝑠 ) 𝑅 ( 𝐹 ‘ 𝑛 ) ∧ 𝑠 ∈ ℕ ) )
67 peano2nn ⊢ ( 𝑠 ∈ ℕ → ( 𝑠 + 1 ) ∈ ℕ )
68 67 nnzd ⊢ ( 𝑠 ∈ ℕ → ( 𝑠 + 1 ) ∈ ℤ )
69 uzid ⊢ ( ( 𝑠 + 1 ) ∈ ℤ → ( 𝑠 + 1 ) ∈ ( ℤ≥ ‘ ( 𝑠 + 1 ) ) )
70 68 69 syl ⊢ ( 𝑠 ∈ ℕ → ( 𝑠 + 1 ) ∈ ( ℤ≥ ‘ ( 𝑠 + 1 ) ) )
71 fveq2 ⊢ ( 𝑛 = ( 𝑠 + 1 ) → ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ ( 𝑠 + 1 ) ) )
72 71 breq2d ⊢ ( 𝑛 = ( 𝑠 + 1 ) → ( ( 𝐹 ‘ 𝑠 ) 𝑅 ( 𝐹 ‘ 𝑛 ) ↔ ( 𝐹 ‘ 𝑠 ) 𝑅 ( 𝐹 ‘ ( 𝑠 + 1 ) ) ) )
73 72 rspccva ⊢ ( ( ∀ 𝑛 ∈ ( ℤ≥ ‘ ( 𝑠 + 1 ) ) ( 𝐹 ‘ 𝑠 ) 𝑅 ( 𝐹 ‘ 𝑛 ) ∧ ( 𝑠 + 1 ) ∈ ( ℤ≥ ‘ ( 𝑠 + 1 ) ) ) → ( 𝐹 ‘ 𝑠 ) 𝑅 ( 𝐹 ‘ ( 𝑠 + 1 ) ) )
74 70 73 sylan2 ⊢ ( ( ∀ 𝑛 ∈ ( ℤ≥ ‘ ( 𝑠 + 1 ) ) ( 𝐹 ‘ 𝑠 ) 𝑅 ( 𝐹 ‘ 𝑛 ) ∧ 𝑠 ∈ ℕ ) → ( 𝐹 ‘ 𝑠 ) 𝑅 ( 𝐹 ‘ ( 𝑠 + 1 ) ) )
75 66 74 syl ⊢ ( ( ∀ 𝑚 ∈ ℕ ∀ 𝑛 ∈ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ( 𝐹 ‘ 𝑚 ) 𝑅 ( 𝐹 ‘ 𝑛 ) ∧ 𝑠 ∈ ℕ ) → ( 𝐹 ‘ 𝑠 ) 𝑅 ( 𝐹 ‘ ( 𝑠 + 1 ) ) )
76 75 ralrimiva ⊢ ( ∀ 𝑚 ∈ ℕ ∀ 𝑛 ∈ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ( 𝐹 ‘ 𝑚 ) 𝑅 ( 𝐹 ‘ 𝑛 ) → ∀ 𝑠 ∈ ℕ ( 𝐹 ‘ 𝑠 ) 𝑅 ( 𝐹 ‘ ( 𝑠 + 1 ) ) )
77 60 76 impbid1 ⊢ ( ( 𝑅 Po 𝐴 ∧ 𝐹 : ℕ ⟶ 𝐴 ) → ( ∀ 𝑠 ∈ ℕ ( 𝐹 ‘ 𝑠 ) 𝑅 ( 𝐹 ‘ ( 𝑠 + 1 ) ) ↔ ∀ 𝑚 ∈ ℕ ∀ 𝑛 ∈ ( ℤ≥ ‘ ( 𝑚 + 1 ) ) ( 𝐹 ‘ 𝑚 ) 𝑅 ( 𝐹 ‘ 𝑛 ) ) )