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