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 \land F : ℕ ⟶ A) \to (\forall s \in ℕ F (s) R F (s + 1) \leftrightarrow \forall m \in ℕ \forall n \in ℤ_{\geq (m + 1)} F (m) R F (n))$

Proof

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

Metamath Proof Explorer

Theorem seqpo

Proof