ormklocald

Description: If elements of a certain sequence are ordered with respect to a certain relation, then its consecutive elements satisfy that relation (so-called "local monotonicity"). (Contributed by Ender Ting, 30-Apr-2025)

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

Proof

Step	Hyp	Ref	Expression
1		ormklocald.1	$⊢ φ \to R Or S$
2		ormklocald.2	$⊢ φ \to \forall k \in (0 ..^T + 1) B (k) \in S$
3		ormklocald.3	$⊢ φ \to \forall k \in (0 ..^T) \forall t \in (1 ..^T + 1) (k < t \to B (k) R B (t))$
4		ovex	$⊢ k + 1 \in V$
5	4	isseti	$⊢ \exists t t = k + 1$
6		elfzoelz	$⊢ k \in (0 ..^T) \to k \in ℤ$
7	6	zred	$⊢ k \in (0 ..^T) \to k \in ℝ$
8	7	ltp1d	$⊢ k \in (0 ..^T) \to k < k + 1$
9		breq2	$⊢ t = k + 1 \to (k < t \leftrightarrow k < k + 1)$
10	8 9	syl5ibrcom	$⊢ k \in (0 ..^T) \to (t = k + 1 \to k < t)$
11	10	adantl	$⊢ (φ \land k \in (0 ..^T)) \to (t = k + 1 \to k < t)$
12		1z	$⊢ 1 \in ℤ$
13		fzoaddel	$⊢ (k \in (0 ..^T) \land 1 \in ℤ) \to k + 1 \in (0 + 1 ..^T + 1)$
14	12 13	mpan2	$⊢ k \in (0 ..^T) \to k + 1 \in (0 + 1 ..^T + 1)$
15		0p1e1	$⊢ 0 + 1 = 1$
16	15	oveq1i	$⊢ (0 + 1 ..^T + 1) = (1 ..^T + 1)$
17	14 16	eleqtrdi	$⊢ k \in (0 ..^T) \to k + 1 \in (1 ..^T + 1)$
18		eleq1	$⊢ t = k + 1 \to (t \in (1 ..^T + 1) \leftrightarrow k + 1 \in (1 ..^T + 1))$
19	17 18	syl5ibrcom	$⊢ k \in (0 ..^T) \to (t = k + 1 \to t \in (1 ..^T + 1))$
20	19	adantl	$⊢ (φ \land k \in (0 ..^T)) \to (t = k + 1 \to t \in (1 ..^T + 1))$
21	3	r19.21bi	$⊢ (φ \land k \in (0 ..^T)) \to \forall t \in (1 ..^T + 1) (k < t \to B (k) R B (t))$
22	21	r19.21bi	$⊢ ((φ \land k \in (0 ..^T)) \land t \in (1 ..^T + 1)) \to (k < t \to B (k) R B (t))$
23	22	ex	$⊢ (φ \land k \in (0 ..^T)) \to (t \in (1 ..^T + 1) \to (k < t \to B (k) R B (t)))$
24	20 23	syld	$⊢ (φ \land k \in (0 ..^T)) \to (t = k + 1 \to (k < t \to B (k) R B (t)))$
25	11 24	mpdd	$⊢ (φ \land k \in (0 ..^T)) \to (t = k + 1 \to B (k) R B (t))$
26		fveq2	$⊢ t = k + 1 \to B (t) = B (k + 1)$
27	26	breq2d	$⊢ t = k + 1 \to (B (k) R B (t) \leftrightarrow B (k) R B (k + 1))$
28	25 27	mpbidi	$⊢ (φ \land k \in (0 ..^T)) \to (t = k + 1 \to B (k) R B (k + 1))$
29	28	eximdv	$⊢ (φ \land k \in (0 ..^T)) \to (\exists t t = k + 1 \to \exists t B (k) R B (k + 1))$
30	5 29	mpi	$⊢ (φ \land k \in (0 ..^T)) \to \exists t B (k) R B (k + 1)$
31		ax5e	$⊢ \exists t B (k) R B (k + 1) \to B (k) R B (k + 1)$
32	30 31	syl	$⊢ (φ \land k \in (0 ..^T)) \to B (k) R B (k + 1)$
33	32	ralrimiva	$⊢ φ \to \forall k \in (0 ..^T) B (k) R B (k + 1)$

Metamath Proof Explorer

Theorem ormklocald

Proof