ormkglobd

Description: If all adjacent elements of a certain sequence are ordered according to a relation which is a total order on S, then any element is so related to anything to right of it (so-called "global monotonicity"). Deduction form. (Contributed by Ender Ting, 30-Apr-2025)

	Ref	Expression
Hypotheses	ormkglobd.1	$⊢ φ \to R Or S$
	ormkglobd.2	$⊢ φ \to \forall k \in (0 ..^T + 1) B (k) \in S$
	ormkglobd.3	$⊢ φ \to \forall k \in (0 ..^T) B (k) R B (k + 1)$
Assertion	ormkglobd	$⊢ φ \to \forall k \in (0 ..^T) \forall t \in (1 ..^T + 1) (k < t \to B (k) R B (t))$

Proof

Step	Hyp	Ref	Expression
1		ormkglobd.1	$⊢ φ \to R Or S$
2		ormkglobd.2	$⊢ φ \to \forall k \in (0 ..^T + 1) B (k) \in S$
3		ormkglobd.3	$⊢ φ \to \forall k \in (0 ..^T) B (k) R B (k + 1)$
4		2a1	$⊢ φ \to ((k \in (0 ..^T) \land t \in (1 ..^T + 1)) \to (k < t \to φ))$
5	4	imp	$⊢ (φ \land (k \in (0 ..^T) \land t \in (1 ..^T + 1))) \to (k < t \to φ)$
6		2a1	$⊢ k \in (0 ..^T) \to (t \in (1 ..^T + 1) \to (k < t \to k \in (0 ..^T)))$
7	6	imp	$⊢ (k \in (0 ..^T) \land t \in (1 ..^T + 1)) \to (k < t \to k \in (0 ..^T))$
8	7	adantl	$⊢ (φ \land (k \in (0 ..^T) \land t \in (1 ..^T + 1))) \to (k < t \to k \in (0 ..^T))$
9	5 8	jcad	$⊢ (φ \land (k \in (0 ..^T) \land t \in (1 ..^T + 1))) \to (k < t \to (φ \land k \in (0 ..^T)))$
10		elfzoelz	$⊢ t \in (1 ..^T + 1) \to t \in ℤ$
11	10	adantl	$⊢ (k \in (0 ..^T) \land t \in (1 ..^T + 1)) \to t \in ℤ$
12	11	a1d	$⊢ (k \in (0 ..^T) \land t \in (1 ..^T + 1)) \to (k < t \to t \in ℤ)$
13		elfzoelz	$⊢ k \in (0 ..^T) \to k \in ℤ$
14	13	adantr	$⊢ (k \in (0 ..^T) \land t \in (1 ..^T + 1)) \to k \in ℤ$
15		zltp1le	$⊢ (k \in ℤ \land t \in ℤ) \to (k < t \leftrightarrow k + 1 \leq t)$
16	14 11 15	syl2anc	$⊢ (k \in (0 ..^T) \land t \in (1 ..^T + 1)) \to (k < t \leftrightarrow k + 1 \leq t)$
17	16	biimpd	$⊢ (k \in (0 ..^T) \land t \in (1 ..^T + 1)) \to (k < t \to k + 1 \leq t)$
18	11	zred	$⊢ (k \in (0 ..^T) \land t \in (1 ..^T + 1)) \to t \in ℝ$
19		elfzoel2	$⊢ k \in (0 ..^T) \to T \in ℤ$
20	19	adantr	$⊢ (k \in (0 ..^T) \land t \in (1 ..^T + 1)) \to T \in ℤ$
21	20	zred	$⊢ (k \in (0 ..^T) \land t \in (1 ..^T + 1)) \to T \in ℝ$
22		1red	$⊢ (k \in (0 ..^T) \land t \in (1 ..^T + 1)) \to 1 \in ℝ$
23	18 21 22	3jca	$⊢ (k \in (0 ..^T) \land t \in (1 ..^T + 1)) \to (t \in ℝ \land T \in ℝ \land 1 \in ℝ)$
24		elfzop1le2	$⊢ t \in (1 ..^T + 1) \to t + 1 \leq T + 1$
25	24	adantl	$⊢ (k \in (0 ..^T) \land t \in (1 ..^T + 1)) \to t + 1 \leq T + 1$
26		leadd1	$⊢ (t \in ℝ \land T \in ℝ \land 1 \in ℝ) \to (t \leq T \leftrightarrow t + 1 \leq T + 1)$
27	26	biimprd	$⊢ (t \in ℝ \land T \in ℝ \land 1 \in ℝ) \to (t + 1 \leq T + 1 \to t \leq T)$
28	23 25 27	sylc	$⊢ (k \in (0 ..^T) \land t \in (1 ..^T + 1)) \to t \leq T$
29	28	a1d	$⊢ (k \in (0 ..^T) \land t \in (1 ..^T + 1)) \to (k < t \to t \leq T)$
30	12 17 29	3jcad	$⊢ (k \in (0 ..^T) \land t \in (1 ..^T + 1)) \to (k < t \to (t \in ℤ \land k + 1 \leq t \land t \leq T))$
31	30	adantl	$⊢ (φ \land (k \in (0 ..^T) \land t \in (1 ..^T + 1))) \to (k < t \to (t \in ℤ \land k + 1 \leq t \land t \leq T))$
32	9 31	jcad	$⊢ (φ \land (k \in (0 ..^T) \land t \in (1 ..^T + 1))) \to (k < t \to ((φ \land k \in (0 ..^T)) \land (t \in ℤ \land k + 1 \leq t \land t \leq T)))$
33	32	ex	$⊢ φ \to ((k \in (0 ..^T) \land t \in (1 ..^T + 1)) \to (k < t \to ((φ \land k \in (0 ..^T)) \land (t \in ℤ \land k + 1 \leq t \land t \leq T))))$
34		fveq2	$⊢ a = k + 1 \to B (a) = B (k + 1)$
35	34	breq2d	$⊢ a = k + 1 \to (B (k) R B (a) \leftrightarrow B (k) R B (k + 1))$
36		fveq2	$⊢ a = b \to B (a) = B (b)$
37	36	breq2d	$⊢ a = b \to (B (k) R B (a) \leftrightarrow B (k) R B (b))$
38		fveq2	$⊢ a = b + 1 \to B (a) = B (b + 1)$
39	38	breq2d	$⊢ a = b + 1 \to (B (k) R B (a) \leftrightarrow B (k) R B (b + 1))$
40		fveq2	$⊢ a = t \to B (a) = B (t)$
41	40	breq2d	$⊢ a = t \to (B (k) R B (a) \leftrightarrow B (k) R B (t))$
42	3	r19.21bi	$⊢ (φ \land k \in (0 ..^T)) \to B (k) R B (k + 1)$
43		simp1l	$⊢ ((φ \land k \in (0 ..^T)) \land (b \in ℤ \land k + 1 \leq b \land b < T) \land B (k) R B (b)) \to φ$
44	43 1	syl	$⊢ ((φ \land k \in (0 ..^T)) \land (b \in ℤ \land k + 1 \leq b \land b < T) \land B (k) R B (b)) \to R Or S$
45		elfzofz	$⊢ k \in (0 ..^T) \to k \in (0 \dots T)$
46		fzval3	$⊢ T \in ℤ \to (0 \dots T) = (0 ..^T + 1)$
47	19 46	syl	$⊢ k \in (0 ..^T) \to (0 \dots T) = (0 ..^T + 1)$
48	45 47	eleqtrd	$⊢ k \in (0 ..^T) \to k \in (0 ..^T + 1)$
49	2	r19.21bi	$⊢ (φ \land k \in (0 ..^T + 1)) \to B (k) \in S$
50	48 49	sylan2	$⊢ (φ \land k \in (0 ..^T)) \to B (k) \in S$
51	50	3ad2ant1	$⊢ ((φ \land k \in (0 ..^T)) \land (b \in ℤ \land k + 1 \leq b \land b < T) \land B (k) R B (b)) \to B (k) \in S$
52		simp21	$⊢ ((φ \land k \in (0 ..^T)) \land (b \in ℤ \land k + 1 \leq b \land b < T) \land B (k) R B (b)) \to b \in ℤ$
53		0red	$⊢ ((φ \land k \in (0 ..^T)) \land (b \in ℤ \land k + 1 \leq b \land b < T) \land B (k) R B (b)) \to 0 \in ℝ$
54		simp1r	$⊢ ((φ \land k \in (0 ..^T)) \land (b \in ℤ \land k + 1 \leq b \land b < T) \land B (k) R B (b)) \to k \in (0 ..^T)$
55	54 13	syl	$⊢ ((φ \land k \in (0 ..^T)) \land (b \in ℤ \land k + 1 \leq b \land b < T) \land B (k) R B (b)) \to k \in ℤ$
56	55	zred	$⊢ ((φ \land k \in (0 ..^T)) \land (b \in ℤ \land k + 1 \leq b \land b < T) \land B (k) R B (b)) \to k \in ℝ$
57		1red	$⊢ ((φ \land k \in (0 ..^T)) \land (b \in ℤ \land k + 1 \leq b \land b < T) \land B (k) R B (b)) \to 1 \in ℝ$
58	56 57	readdcld	$⊢ ((φ \land k \in (0 ..^T)) \land (b \in ℤ \land k + 1 \leq b \land b < T) \land B (k) R B (b)) \to k + 1 \in ℝ$
59	52	zred	$⊢ ((φ \land k \in (0 ..^T)) \land (b \in ℤ \land k + 1 \leq b \land b < T) \land B (k) R B (b)) \to b \in ℝ$
60		elfzole1	$⊢ k \in (0 ..^T) \to 0 \leq k$
61	54 60	syl	$⊢ ((φ \land k \in (0 ..^T)) \land (b \in ℤ \land k + 1 \leq b \land b < T) \land B (k) R B (b)) \to 0 \leq k$
62		0le1	$⊢ 0 \leq 1$
63	62	a1i	$⊢ ((φ \land k \in (0 ..^T)) \land (b \in ℤ \land k + 1 \leq b \land b < T) \land B (k) R B (b)) \to 0 \leq 1$
64	56 57 61 63	addge0d	$⊢ ((φ \land k \in (0 ..^T)) \land (b \in ℤ \land k + 1 \leq b \land b < T) \land B (k) R B (b)) \to 0 \leq k + 1$
65		simp22	$⊢ ((φ \land k \in (0 ..^T)) \land (b \in ℤ \land k + 1 \leq b \land b < T) \land B (k) R B (b)) \to k + 1 \leq b$
66	53 58 59 64 65	letrd	$⊢ ((φ \land k \in (0 ..^T)) \land (b \in ℤ \land k + 1 \leq b \land b < T) \land B (k) R B (b)) \to 0 \leq b$
67		elnn0z	$⊢ b \in ℕ_{0} \leftrightarrow (b \in ℤ \land 0 \leq b)$
68	52 66 67	sylanbrc	$⊢ ((φ \land k \in (0 ..^T)) \land (b \in ℤ \land k + 1 \leq b \land b < T) \land B (k) R B (b)) \to b \in ℕ_{0}$
69	54 19	syl	$⊢ ((φ \land k \in (0 ..^T)) \land (b \in ℤ \land k + 1 \leq b \land b < T) \land B (k) R B (b)) \to T \in ℤ$
70	69	peano2zd	$⊢ ((φ \land k \in (0 ..^T)) \land (b \in ℤ \land k + 1 \leq b \land b < T) \land B (k) R B (b)) \to T + 1 \in ℤ$
71	69	zred	$⊢ ((φ \land k \in (0 ..^T)) \land (b \in ℤ \land k + 1 \leq b \land b < T) \land B (k) R B (b)) \to T \in ℝ$
72	71 57	readdcld	$⊢ ((φ \land k \in (0 ..^T)) \land (b \in ℤ \land k + 1 \leq b \land b < T) \land B (k) R B (b)) \to T + 1 \in ℝ$
73		simp23	$⊢ ((φ \land k \in (0 ..^T)) \land (b \in ℤ \land k + 1 \leq b \land b < T) \land B (k) R B (b)) \to b < T$
74	71	ltp1d	$⊢ ((φ \land k \in (0 ..^T)) \land (b \in ℤ \land k + 1 \leq b \land b < T) \land B (k) R B (b)) \to T < T + 1$
75	59 71 72 73 74	lttrd	$⊢ ((φ \land k \in (0 ..^T)) \land (b \in ℤ \land k + 1 \leq b \land b < T) \land B (k) R B (b)) \to b < T + 1$
76		elfzo0z	$⊢ b \in (0 ..^T + 1) \leftrightarrow (b \in ℕ_{0} \land T + 1 \in ℤ \land b < T + 1)$
77	68 70 75 76	syl3anbrc	$⊢ ((φ \land k \in (0 ..^T)) \land (b \in ℤ \land k + 1 \leq b \land b < T) \land B (k) R B (b)) \to b \in (0 ..^T + 1)$
78		eleq1w	$⊢ k = b \to (k \in (0 ..^T + 1) \leftrightarrow b \in (0 ..^T + 1))$
79	78	anbi2d	$⊢ k = b \to ((φ \land k \in (0 ..^T + 1)) \leftrightarrow (φ \land b \in (0 ..^T + 1)))$
80		fveq2	$⊢ k = b \to B (k) = B (b)$
81	80	eleq1d	$⊢ k = b \to (B (k) \in S \leftrightarrow B (b) \in S)$
82	49 81	imbitrid	$⊢ k = b \to ((φ \land k \in (0 ..^T + 1)) \to B (b) \in S)$
83	79 82	sylbird	$⊢ k = b \to ((φ \land b \in (0 ..^T + 1)) \to B (b) \in S)$
84		ax6ev	$⊢ \exists k k = b$
85	83 84	exlimiiv	$⊢ (φ \land b \in (0 ..^T + 1)) \to B (b) \in S$
86	43 77 85	syl2anc	$⊢ ((φ \land k \in (0 ..^T)) \land (b \in ℤ \land k + 1 \leq b \land b < T) \land B (k) R B (b)) \to B (b) \in S$
87		1nn0	$⊢ 1 \in ℕ_{0}$
88	87	a1i	$⊢ ((φ \land k \in (0 ..^T)) \land (b \in ℤ \land k + 1 \leq b \land b < T) \land B (k) R B (b)) \to 1 \in ℕ_{0}$
89	68 88	nn0addcld	$⊢ ((φ \land k \in (0 ..^T)) \land (b \in ℤ \land k + 1 \leq b \land b < T) \land B (k) R B (b)) \to b + 1 \in ℕ_{0}$
90	59 71 57 73	ltadd1dd	$⊢ ((φ \land k \in (0 ..^T)) \land (b \in ℤ \land k + 1 \leq b \land b < T) \land B (k) R B (b)) \to b + 1 < T + 1$
91		elfzo0z	$⊢ b + 1 \in (0 ..^T + 1) \leftrightarrow (b + 1 \in ℕ_{0} \land T + 1 \in ℤ \land b + 1 < T + 1)$
92	89 70 90 91	syl3anbrc	$⊢ ((φ \land k \in (0 ..^T)) \land (b \in ℤ \land k + 1 \leq b \land b < T) \land B (k) R B (b)) \to b + 1 \in (0 ..^T + 1)$
93		ovex	$⊢ b + 1 \in V$
94		eleq1	$⊢ k = b + 1 \to (k \in (0 ..^T + 1) \leftrightarrow b + 1 \in (0 ..^T + 1))$
95	94	anbi2d	$⊢ k = b + 1 \to ((φ \land k \in (0 ..^T + 1)) \leftrightarrow (φ \land b + 1 \in (0 ..^T + 1)))$
96		fveq2	$⊢ k = b + 1 \to B (k) = B (b + 1)$
97	96	eleq1d	$⊢ k = b + 1 \to (B (k) \in S \leftrightarrow B (b + 1) \in S)$
98	49 97	imbitrid	$⊢ k = b + 1 \to ((φ \land k \in (0 ..^T + 1)) \to B (b + 1) \in S)$
99	95 98	sylbird	$⊢ k = b + 1 \to ((φ \land b + 1 \in (0 ..^T + 1)) \to B (b + 1) \in S)$
100	93 99	vtocle	$⊢ (φ \land b + 1 \in (0 ..^T + 1)) \to B (b + 1) \in S$
101	43 92 100	syl2anc	$⊢ ((φ \land k \in (0 ..^T)) \land (b \in ℤ \land k + 1 \leq b \land b < T) \land B (k) R B (b)) \to B (b + 1) \in S$
102		simp3	$⊢ ((φ \land k \in (0 ..^T)) \land (b \in ℤ \land k + 1 \leq b \land b < T) \land B (k) R B (b)) \to B (k) R B (b)$
103		elfzo0z	$⊢ b \in (0 ..^T) \leftrightarrow (b \in ℕ_{0} \land T \in ℤ \land b < T)$
104	68 69 73 103	syl3anbrc	$⊢ ((φ \land k \in (0 ..^T)) \land (b \in ℤ \land k + 1 \leq b \land b < T) \land B (k) R B (b)) \to b \in (0 ..^T)$
105		eleq1w	$⊢ b = k \to (b \in (0 ..^T) \leftrightarrow k \in (0 ..^T))$
106	105	anbi2d	$⊢ b = k \to ((φ \land b \in (0 ..^T)) \leftrightarrow (φ \land k \in (0 ..^T)))$
107		fveq2	$⊢ b = k \to B (b) = B (k)$
108		fvoveq1	$⊢ b = k \to B (b + 1) = B (k + 1)$
109	107 108	breq12d	$⊢ b = k \to (B (b) R B (b + 1) \leftrightarrow B (k) R B (k + 1))$
110	42 109	imbitrrid	$⊢ b = k \to ((φ \land k \in (0 ..^T)) \to B (b) R B (b + 1))$
111	106 110	sylbid	$⊢ b = k \to ((φ \land b \in (0 ..^T)) \to B (b) R B (b + 1))$
112		ax6evr	$⊢ \exists k b = k$
113	111 112	exlimiiv	$⊢ (φ \land b \in (0 ..^T)) \to B (b) R B (b + 1)$
114	43 104 113	syl2anc	$⊢ ((φ \land k \in (0 ..^T)) \land (b \in ℤ \land k + 1 \leq b \land b < T) \land B (k) R B (b)) \to B (b) R B (b + 1)$
115	44 51 86 101 102 114	sotrd	$⊢ ((φ \land k \in (0 ..^T)) \land (b \in ℤ \land k + 1 \leq b \land b < T) \land B (k) R B (b)) \to B (k) R B (b + 1)$
116	13	adantl	$⊢ (φ \land k \in (0 ..^T)) \to k \in ℤ$
117	116	peano2zd	$⊢ (φ \land k \in (0 ..^T)) \to k + 1 \in ℤ$
118	19	adantl	$⊢ (φ \land k \in (0 ..^T)) \to T \in ℤ$
119		elfzop1le2	$⊢ k \in (0 ..^T) \to k + 1 \leq T$
120	119	adantl	$⊢ (φ \land k \in (0 ..^T)) \to k + 1 \leq T$
121	35 37 39 41 42 115 117 118 120	fzindd	$⊢ ((φ \land k \in (0 ..^T)) \land (t \in ℤ \land k + 1 \leq t \land t \leq T)) \to B (k) R B (t)$
122	33 121	syl8	$⊢ φ \to ((k \in (0 ..^T) \land t \in (1 ..^T + 1)) \to (k < t \to B (k) R B (t)))$
123	122	ralrimivv	$⊢ φ \to \forall k \in (0 ..^T) \forall t \in (1 ..^T + 1) (k < t \to B (k) R B (t))$

Metamath Proof Explorer

Theorem ormkglobd

Proof