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	|- ( ( R Po A /\ F : NN --> A ) -> ( A. s e. NN ( F ` s ) R ( F ` ( s + 1 ) ) <-> A. m e. NN A. n e. ( ZZ>= ` ( m + 1 ) ) ( F ` m ) R ( F ` n ) ) )

Proof

Step	Hyp	Ref	Expression
1		fveq2	|- ( p = ( m + 1 ) -> ( F ` p ) = ( F ` ( m + 1 ) ) )
2	1	breq2d	|- ( p = ( m + 1 ) -> ( ( F ` m ) R ( F ` p ) <-> ( F ` m ) R ( F ` ( m + 1 ) ) ) )
3	2	imbi2d	|- ( p = ( m + 1 ) -> ( ( ( ( R Po A /\ F : NN --> A ) /\ ( A. s e. NN ( F ` s ) R ( F ` ( s + 1 ) ) /\ m e. NN ) ) -> ( F ` m ) R ( F ` p ) ) <-> ( ( ( R Po A /\ F : NN --> A ) /\ ( A. s e. NN ( F ` s ) R ( F ` ( s + 1 ) ) /\ m e. NN ) ) -> ( F ` m ) R ( F ` ( m + 1 ) ) ) ) )
4		fveq2	|- ( p = q -> ( F ` p ) = ( F ` q ) )
5	4	breq2d	|- ( p = q -> ( ( F ` m ) R ( F ` p ) <-> ( F ` m ) R ( F ` q ) ) )
6	5	imbi2d	|- ( p = q -> ( ( ( ( R Po A /\ F : NN --> A ) /\ ( A. s e. NN ( F ` s ) R ( F ` ( s + 1 ) ) /\ m e. NN ) ) -> ( F ` m ) R ( F ` p ) ) <-> ( ( ( R Po A /\ F : NN --> A ) /\ ( A. s e. NN ( F ` s ) R ( F ` ( s + 1 ) ) /\ m e. NN ) ) -> ( F ` m ) R ( F ` q ) ) ) )
7		fveq2	|- ( p = ( q + 1 ) -> ( F ` p ) = ( F ` ( q + 1 ) ) )
8	7	breq2d	|- ( p = ( q + 1 ) -> ( ( F ` m ) R ( F ` p ) <-> ( F ` m ) R ( F ` ( q + 1 ) ) ) )
9	8	imbi2d	|- ( p = ( q + 1 ) -> ( ( ( ( R Po A /\ F : NN --> A ) /\ ( A. s e. NN ( F ` s ) R ( F ` ( s + 1 ) ) /\ m e. NN ) ) -> ( F ` m ) R ( F ` p ) ) <-> ( ( ( R Po A /\ F : NN --> A ) /\ ( A. s e. NN ( F ` s ) R ( F ` ( s + 1 ) ) /\ m e. NN ) ) -> ( F ` m ) R ( F ` ( q + 1 ) ) ) ) )
10		fveq2	|- ( p = n -> ( F ` p ) = ( F ` n ) )
11	10	breq2d	|- ( p = n -> ( ( F ` m ) R ( F ` p ) <-> ( F ` m ) R ( F ` n ) ) )
12	11	imbi2d	|- ( p = n -> ( ( ( ( R Po A /\ F : NN --> A ) /\ ( A. s e. NN ( F ` s ) R ( F ` ( s + 1 ) ) /\ m e. NN ) ) -> ( F ` m ) R ( F ` p ) ) <-> ( ( ( R Po A /\ F : NN --> A ) /\ ( A. s e. NN ( F ` s ) R ( F ` ( s + 1 ) ) /\ m e. NN ) ) -> ( F ` m ) R ( F ` n ) ) ) )
13		fveq2	|- ( s = m -> ( F ` s ) = ( F ` m ) )
14		fvoveq1	|- ( s = m -> ( F ` ( s + 1 ) ) = ( F ` ( m + 1 ) ) )
15	13 14	breq12d	|- ( s = m -> ( ( F ` s ) R ( F ` ( s + 1 ) ) <-> ( F ` m ) R ( F ` ( m + 1 ) ) ) )
16	15	rspccva	|- ( ( A. s e. NN ( F ` s ) R ( F ` ( s + 1 ) ) /\ m e. NN ) -> ( F ` m ) R ( F ` ( m + 1 ) ) )
17	16	adantl	|- ( ( ( R Po A /\ F : NN --> A ) /\ ( A. s e. NN ( F ` s ) R ( F ` ( s + 1 ) ) /\ m e. NN ) ) -> ( F ` m ) R ( F ` ( m + 1 ) ) )
18	17	a1i	|- ( ( m + 1 ) e. ZZ -> ( ( ( R Po A /\ F : NN --> A ) /\ ( A. s e. NN ( F ` s ) R ( F ` ( s + 1 ) ) /\ m e. NN ) ) -> ( F ` m ) R ( F ` ( m + 1 ) ) ) )
19		peano2nn	|- ( m e. NN -> ( m + 1 ) e. NN )
20		elnnuz	|- ( ( m + 1 ) e. NN <-> ( m + 1 ) e. ( ZZ>= ` 1 ) )
21	19 20	sylib	|- ( m e. NN -> ( m + 1 ) e. ( ZZ>= ` 1 ) )
22		uztrn	|- ( ( q e. ( ZZ>= ` ( m + 1 ) ) /\ ( m + 1 ) e. ( ZZ>= ` 1 ) ) -> q e. ( ZZ>= ` 1 ) )
23		elnnuz	|- ( q e. NN <-> q e. ( ZZ>= ` 1 ) )
24	22 23	sylibr	|- ( ( q e. ( ZZ>= ` ( m + 1 ) ) /\ ( m + 1 ) e. ( ZZ>= ` 1 ) ) -> q e. NN )
25	24	expcom	|- ( ( m + 1 ) e. ( ZZ>= ` 1 ) -> ( q e. ( ZZ>= ` ( m + 1 ) ) -> q e. NN ) )
26	21 25	syl	|- ( m e. NN -> ( q e. ( ZZ>= ` ( m + 1 ) ) -> q e. NN ) )
27	26	imdistani	|- ( ( m e. NN /\ q e. ( ZZ>= ` ( m + 1 ) ) ) -> ( m e. NN /\ q e. NN ) )
28		fveq2	|- ( s = q -> ( F ` s ) = ( F ` q ) )
29		fvoveq1	|- ( s = q -> ( F ` ( s + 1 ) ) = ( F ` ( q + 1 ) ) )
30	28 29	breq12d	|- ( s = q -> ( ( F ` s ) R ( F ` ( s + 1 ) ) <-> ( F ` q ) R ( F ` ( q + 1 ) ) ) )
31	30	rspccva	|- ( ( A. s e. NN ( F ` s ) R ( F ` ( s + 1 ) ) /\ q e. NN ) -> ( F ` q ) R ( F ` ( q + 1 ) ) )
32	31	ad2ant2l	|- ( ( ( ( R Po A /\ F : NN --> A ) /\ A. s e. NN ( F ` s ) R ( F ` ( s + 1 ) ) ) /\ ( m e. NN /\ q e. NN ) ) -> ( F ` q ) R ( F ` ( q + 1 ) ) )
33	32	ex	|- ( ( ( R Po A /\ F : NN --> A ) /\ A. s e. NN ( F ` s ) R ( F ` ( s + 1 ) ) ) -> ( ( m e. NN /\ q e. NN ) -> ( F ` q ) R ( F ` ( q + 1 ) ) ) )
34		ffvelcdm	|- ( ( F : NN --> A /\ m e. NN ) -> ( F ` m ) e. A )
35	34	adantrr	|- ( ( F : NN --> A /\ ( m e. NN /\ q e. NN ) ) -> ( F ` m ) e. A )
36		ffvelcdm	|- ( ( F : NN --> A /\ q e. NN ) -> ( F ` q ) e. A )
37	36	adantrl	|- ( ( F : NN --> A /\ ( m e. NN /\ q e. NN ) ) -> ( F ` q ) e. A )
38		peano2nn	|- ( q e. NN -> ( q + 1 ) e. NN )
39		ffvelcdm	|- ( ( F : NN --> A /\ ( q + 1 ) e. NN ) -> ( F ` ( q + 1 ) ) e. A )
40	38 39	sylan2	|- ( ( F : NN --> A /\ q e. NN ) -> ( F ` ( q + 1 ) ) e. A )
41	40	adantrl	|- ( ( F : NN --> A /\ ( m e. NN /\ q e. NN ) ) -> ( F ` ( q + 1 ) ) e. A )
42	35 37 41	3jca	|- ( ( F : NN --> A /\ ( m e. NN /\ q e. NN ) ) -> ( ( F ` m ) e. A /\ ( F ` q ) e. A /\ ( F ` ( q + 1 ) ) e. A ) )
43		potr	|- ( ( R Po A /\ ( ( F ` m ) e. A /\ ( F ` q ) e. A /\ ( F ` ( q + 1 ) ) e. A ) ) -> ( ( ( F ` m ) R ( F ` q ) /\ ( F ` q ) R ( F ` ( q + 1 ) ) ) -> ( F ` m ) R ( F ` ( q + 1 ) ) ) )
44	43	expcomd	|- ( ( R Po A /\ ( ( F ` m ) e. A /\ ( F ` q ) e. A /\ ( F ` ( q + 1 ) ) e. A ) ) -> ( ( F ` q ) R ( F ` ( q + 1 ) ) -> ( ( F ` m ) R ( F ` q ) -> ( F ` m ) R ( F ` ( q + 1 ) ) ) ) )
45	44	ex	|- ( R Po A -> ( ( ( F ` m ) e. A /\ ( F ` q ) e. A /\ ( F ` ( q + 1 ) ) e. A ) -> ( ( F ` q ) R ( F ` ( q + 1 ) ) -> ( ( F ` m ) R ( F ` q ) -> ( F ` m ) R ( F ` ( q + 1 ) ) ) ) ) )
46	42 45	syl5	|- ( R Po A -> ( ( F : NN --> A /\ ( m e. NN /\ q e. NN ) ) -> ( ( F ` q ) R ( F ` ( q + 1 ) ) -> ( ( F ` m ) R ( F ` q ) -> ( F ` m ) R ( F ` ( q + 1 ) ) ) ) ) )
47	46	expdimp	|- ( ( R Po A /\ F : NN --> A ) -> ( ( m e. NN /\ q e. NN ) -> ( ( F ` q ) R ( F ` ( q + 1 ) ) -> ( ( F ` m ) R ( F ` q ) -> ( F ` m ) R ( F ` ( q + 1 ) ) ) ) ) )
48	47	adantr	|- ( ( ( R Po A /\ F : NN --> A ) /\ A. s e. NN ( F ` s ) R ( F ` ( s + 1 ) ) ) -> ( ( m e. NN /\ q e. NN ) -> ( ( F ` q ) R ( F ` ( q + 1 ) ) -> ( ( F ` m ) R ( F ` q ) -> ( F ` m ) R ( F ` ( q + 1 ) ) ) ) ) )
49	33 48	mpdd	|- ( ( ( R Po A /\ F : NN --> A ) /\ A. s e. NN ( F ` s ) R ( F ` ( s + 1 ) ) ) -> ( ( m e. NN /\ q e. NN ) -> ( ( F ` m ) R ( F ` q ) -> ( F ` m ) R ( F ` ( q + 1 ) ) ) ) )
50	27 49	syl5	|- ( ( ( R Po A /\ F : NN --> A ) /\ A. s e. NN ( F ` s ) R ( F ` ( s + 1 ) ) ) -> ( ( m e. NN /\ q e. ( ZZ>= ` ( m + 1 ) ) ) -> ( ( F ` m ) R ( F ` q ) -> ( F ` m ) R ( F ` ( q + 1 ) ) ) ) )
51	50	expdimp	|- ( ( ( ( R Po A /\ F : NN --> A ) /\ A. s e. NN ( F ` s ) R ( F ` ( s + 1 ) ) ) /\ m e. NN ) -> ( q e. ( ZZ>= ` ( m + 1 ) ) -> ( ( F ` m ) R ( F ` q ) -> ( F ` m ) R ( F ` ( q + 1 ) ) ) ) )
52	51	anasss	|- ( ( ( R Po A /\ F : NN --> A ) /\ ( A. s e. NN ( F ` s ) R ( F ` ( s + 1 ) ) /\ m e. NN ) ) -> ( q e. ( ZZ>= ` ( m + 1 ) ) -> ( ( F ` m ) R ( F ` q ) -> ( F ` m ) R ( F ` ( q + 1 ) ) ) ) )
53	52	com12	|- ( q e. ( ZZ>= ` ( m + 1 ) ) -> ( ( ( R Po A /\ F : NN --> A ) /\ ( A. s e. NN ( F ` s ) R ( F ` ( s + 1 ) ) /\ m e. NN ) ) -> ( ( F ` m ) R ( F ` q ) -> ( F ` m ) R ( F ` ( q + 1 ) ) ) ) )
54	53	a2d	|- ( q e. ( ZZ>= ` ( m + 1 ) ) -> ( ( ( ( R Po A /\ F : NN --> A ) /\ ( A. s e. NN ( F ` s ) R ( F ` ( s + 1 ) ) /\ m e. NN ) ) -> ( F ` m ) R ( F ` q ) ) -> ( ( ( R Po A /\ F : NN --> A ) /\ ( A. s e. NN ( F ` s ) R ( F ` ( s + 1 ) ) /\ m e. NN ) ) -> ( F ` m ) R ( F ` ( q + 1 ) ) ) ) )
55	3 6 9 12 18 54	uzind4	|- ( n e. ( ZZ>= ` ( m + 1 ) ) -> ( ( ( R Po A /\ F : NN --> A ) /\ ( A. s e. NN ( F ` s ) R ( F ` ( s + 1 ) ) /\ m e. NN ) ) -> ( F ` m ) R ( F ` n ) ) )
56	55	com12	|- ( ( ( R Po A /\ F : NN --> A ) /\ ( A. s e. NN ( F ` s ) R ( F ` ( s + 1 ) ) /\ m e. NN ) ) -> ( n e. ( ZZ>= ` ( m + 1 ) ) -> ( F ` m ) R ( F ` n ) ) )
57	56	ralrimiv	|- ( ( ( R Po A /\ F : NN --> A ) /\ ( A. s e. NN ( F ` s ) R ( F ` ( s + 1 ) ) /\ m e. NN ) ) -> A. n e. ( ZZ>= ` ( m + 1 ) ) ( F ` m ) R ( F ` n ) )
58	57	anassrs	|- ( ( ( ( R Po A /\ F : NN --> A ) /\ A. s e. NN ( F ` s ) R ( F ` ( s + 1 ) ) ) /\ m e. NN ) -> A. n e. ( ZZ>= ` ( m + 1 ) ) ( F ` m ) R ( F ` n ) )
59	58	ralrimiva	|- ( ( ( R Po A /\ F : NN --> A ) /\ A. s e. NN ( F ` s ) R ( F ` ( s + 1 ) ) ) -> A. m e. NN A. n e. ( ZZ>= ` ( m + 1 ) ) ( F ` m ) R ( F ` n ) )
60	59	ex	|- ( ( R Po A /\ F : NN --> A ) -> ( A. s e. NN ( F ` s ) R ( F ` ( s + 1 ) ) -> A. m e. NN A. n e. ( ZZ>= ` ( m + 1 ) ) ( F ` m ) R ( F ` n ) ) )
61		fvoveq1	|- ( m = s -> ( ZZ>= ` ( m + 1 ) ) = ( ZZ>= ` ( s + 1 ) ) )
62		fveq2	|- ( m = s -> ( F ` m ) = ( F ` s ) )
63	62	breq1d	|- ( m = s -> ( ( F ` m ) R ( F ` n ) <-> ( F ` s ) R ( F ` n ) ) )
64	61 63	raleqbidv	|- ( m = s -> ( A. n e. ( ZZ>= ` ( m + 1 ) ) ( F ` m ) R ( F ` n ) <-> A. n e. ( ZZ>= ` ( s + 1 ) ) ( F ` s ) R ( F ` n ) ) )
65	64	rspcv	|- ( s e. NN -> ( A. m e. NN A. n e. ( ZZ>= ` ( m + 1 ) ) ( F ` m ) R ( F ` n ) -> A. n e. ( ZZ>= ` ( s + 1 ) ) ( F ` s ) R ( F ` n ) ) )
66	65	imdistanri	|- ( ( A. m e. NN A. n e. ( ZZ>= ` ( m + 1 ) ) ( F ` m ) R ( F ` n ) /\ s e. NN ) -> ( A. n e. ( ZZ>= ` ( s + 1 ) ) ( F ` s ) R ( F ` n ) /\ s e. NN ) )
67		peano2nn	|- ( s e. NN -> ( s + 1 ) e. NN )
68	67	nnzd	|- ( s e. NN -> ( s + 1 ) e. ZZ )
69		uzid	|- ( ( s + 1 ) e. ZZ -> ( s + 1 ) e. ( ZZ>= ` ( s + 1 ) ) )
70	68 69	syl	|- ( s e. NN -> ( s + 1 ) e. ( ZZ>= ` ( s + 1 ) ) )
71		fveq2	|- ( n = ( s + 1 ) -> ( F ` n ) = ( F ` ( s + 1 ) ) )
72	71	breq2d	|- ( n = ( s + 1 ) -> ( ( F ` s ) R ( F ` n ) <-> ( F ` s ) R ( F ` ( s + 1 ) ) ) )
73	72	rspccva	|- ( ( A. n e. ( ZZ>= ` ( s + 1 ) ) ( F ` s ) R ( F ` n ) /\ ( s + 1 ) e. ( ZZ>= ` ( s + 1 ) ) ) -> ( F ` s ) R ( F ` ( s + 1 ) ) )
74	70 73	sylan2	|- ( ( A. n e. ( ZZ>= ` ( s + 1 ) ) ( F ` s ) R ( F ` n ) /\ s e. NN ) -> ( F ` s ) R ( F ` ( s + 1 ) ) )
75	66 74	syl	|- ( ( A. m e. NN A. n e. ( ZZ>= ` ( m + 1 ) ) ( F ` m ) R ( F ` n ) /\ s e. NN ) -> ( F ` s ) R ( F ` ( s + 1 ) ) )
76	75	ralrimiva	|- ( A. m e. NN A. n e. ( ZZ>= ` ( m + 1 ) ) ( F ` m ) R ( F ` n ) -> A. s e. NN ( F ` s ) R ( F ` ( s + 1 ) ) )
77	60 76	impbid1	|- ( ( R Po A /\ F : NN --> A ) -> ( A. s e. NN ( F ` s ) R ( F ` ( s + 1 ) ) <-> A. m e. NN A. n e. ( ZZ>= ` ( m + 1 ) ) ( F ` m ) R ( F ` n ) ) )