Metamath Proof Explorer

Theorem chnerlem3

Description: Lemma for chner - trichotomy of integers within the word's domain. (Contributed by Ender Ting, 29-Jan-2026)

Ref Expression
Hypotheses chner.1 ⊢ ( 𝜑 → ∼ Er 𝐴 )
chner.2 ⊢ ( 𝜑 → 𝐶 ∈ ( ∼ Chain 𝐴 ) )
chner.3 ⊢ ( 𝜑 → 𝐽 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) )
chner.4 ⊢ ( 𝜑 → 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) )
Assertion chnerlem3 ( 𝜑 → ( 𝐼 ∈ ( 0 ..^ 𝐽 ) ∨ 𝐽 ∈ ( 0 ..^ 𝐼 ) ∨ 𝐼 = 𝐽 ) )

Proof

Step Hyp Ref Expression
1 chner.1 ⊢ ( 𝜑 → ∼ Er 𝐴 )
2 chner.2 ⊢ ( 𝜑 → 𝐶 ∈ ( ∼ Chain 𝐴 ) )
3 chner.3 ⊢ ( 𝜑 → 𝐽 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) )
4 chner.4 ⊢ ( 𝜑 → 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) )
5 elfzoelz ⊢ ( 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) → 𝐼 ∈ ℤ )
6 4 5 syl ⊢ ( 𝜑 → 𝐼 ∈ ℤ )
7 6 zred ⊢ ( 𝜑 → 𝐼 ∈ ℝ )
8 elfzoelz ⊢ ( 𝐽 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) → 𝐽 ∈ ℤ )
9 3 8 syl ⊢ ( 𝜑 → 𝐽 ∈ ℤ )
10 9 zred ⊢ ( 𝜑 → 𝐽 ∈ ℝ )
11 lttri4 ⊢ ( ( 𝐼 ∈ ℝ ∧ 𝐽 ∈ ℝ ) → ( 𝐼 < 𝐽 ∨ 𝐼 = 𝐽 ∨ 𝐽 < 𝐼 ) )
12 7 10 11 syl2anc ⊢ ( 𝜑 → ( 𝐼 < 𝐽 ∨ 𝐼 = 𝐽 ∨ 𝐽 < 𝐼 ) )
13 3orcomb ⊢ ( ( 𝐼 < 𝐽 ∨ 𝐼 = 𝐽 ∨ 𝐽 < 𝐼 ) ↔ ( 𝐼 < 𝐽 ∨ 𝐽 < 𝐼 ∨ 𝐼 = 𝐽 ) )
14 12 13 sylib ⊢ ( 𝜑 → ( 𝐼 < 𝐽 ∨ 𝐽 < 𝐼 ∨ 𝐼 = 𝐽 ) )
15 elfzonn0 ⊢ ( 𝐼 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) → 𝐼 ∈ ℕ0 )
16 4 15 syl ⊢ ( 𝜑 → 𝐼 ∈ ℕ0 )
17 16 adantr ⊢ ( ( 𝜑 ∧ 𝐼 < 𝐽 ) → 𝐼 ∈ ℕ0 )
18 9 adantr ⊢ ( ( 𝜑 ∧ 𝐼 < 𝐽 ) → 𝐽 ∈ ℤ )
19 simpr ⊢ ( ( 𝜑 ∧ 𝐼 < 𝐽 ) → 𝐼 < 𝐽 )
20 17 18 19 3jca ⊢ ( ( 𝜑 ∧ 𝐼 < 𝐽 ) → ( 𝐼 ∈ ℕ0 ∧ 𝐽 ∈ ℤ ∧ 𝐼 < 𝐽 ) )
21 elfzo0z ⊢ ( 𝐼 ∈ ( 0 ..^ 𝐽 ) ↔ ( 𝐼 ∈ ℕ0 ∧ 𝐽 ∈ ℤ ∧ 𝐼 < 𝐽 ) )
22 20 21 sylibr ⊢ ( ( 𝜑 ∧ 𝐼 < 𝐽 ) → 𝐼 ∈ ( 0 ..^ 𝐽 ) )
23 22 ex ⊢ ( 𝜑 → ( 𝐼 < 𝐽 → 𝐼 ∈ ( 0 ..^ 𝐽 ) ) )
24 elfzonn0 ⊢ ( 𝐽 ∈ ( 0 ..^ ( ♯ ‘ 𝐶 ) ) → 𝐽 ∈ ℕ0 )
25 3 24 syl ⊢ ( 𝜑 → 𝐽 ∈ ℕ0 )
26 25 adantr ⊢ ( ( 𝜑 ∧ 𝐽 < 𝐼 ) → 𝐽 ∈ ℕ0 )
27 6 adantr ⊢ ( ( 𝜑 ∧ 𝐽 < 𝐼 ) → 𝐼 ∈ ℤ )
28 simpr ⊢ ( ( 𝜑 ∧ 𝐽 < 𝐼 ) → 𝐽 < 𝐼 )
29 26 27 28 3jca ⊢ ( ( 𝜑 ∧ 𝐽 < 𝐼 ) → ( 𝐽 ∈ ℕ0 ∧ 𝐼 ∈ ℤ ∧ 𝐽 < 𝐼 ) )
30 elfzo0z ⊢ ( 𝐽 ∈ ( 0 ..^ 𝐼 ) ↔ ( 𝐽 ∈ ℕ0 ∧ 𝐼 ∈ ℤ ∧ 𝐽 < 𝐼 ) )
31 29 30 sylibr ⊢ ( ( 𝜑 ∧ 𝐽 < 𝐼 ) → 𝐽 ∈ ( 0 ..^ 𝐼 ) )
32 31 ex ⊢ ( 𝜑 → ( 𝐽 < 𝐼 → 𝐽 ∈ ( 0 ..^ 𝐼 ) ) )
33 idd ⊢ ( 𝜑 → ( 𝐼 = 𝐽 → 𝐼 = 𝐽 ) )
34 23 32 33 3orim123d ⊢ ( 𝜑 → ( ( 𝐼 < 𝐽 ∨ 𝐽 < 𝐼 ∨ 𝐼 = 𝐽 ) → ( 𝐼 ∈ ( 0 ..^ 𝐽 ) ∨ 𝐽 ∈ ( 0 ..^ 𝐼 ) ∨ 𝐼 = 𝐽 ) ) )
35 14 34 mpd ⊢ ( 𝜑 → ( 𝐼 ∈ ( 0 ..^ 𝐽 ) ∨ 𝐽 ∈ ( 0 ..^ 𝐼 ) ∨ 𝐼 = 𝐽 ) )