Metamath Proof Explorer

Theorem chnsubseq

Description: An order-preserving subsequence of an ordered chain is itself a chain. (Contributed by Ender Ting, 22-Jan-2026)

Ref Expression
Hypotheses chnsubseq.1 ⊢ φ → W ∈ Chain A < ˙
chnsubseq.2 ⊢ φ → I ∈ Chain 0 ..^ W <
chnsubseq.3 ⊢ φ → < ˙ Po A
Assertion chnsubseq ⊢ φ → W ∘ I ∈ Chain A < ˙

Proof

Step Hyp Ref Expression
1 chnsubseq.1 ⊢ φ → W ∈ Chain A < ˙
2 chnsubseq.2 ⊢ φ → I ∈ Chain 0 ..^ W <
3 chnsubseq.3 ⊢ φ → < ˙ Po A
4 1 2 chnsubseqword ⊢ φ → W ∘ I ∈ Word A
5 3 adantr ⊢ φ ∧ x ∈ dom ⁡ W ∘ I ∖ 0 → < ˙ Po A
6 1 adantr ⊢ φ ∧ x ∈ dom ⁡ W ∘ I ∖ 0 → W ∈ Chain A < ˙
7 2 chnwrd ⊢ φ → I ∈ Word 0 ..^ W
8 7 adantr ⊢ φ ∧ x ∈ dom ⁡ W ∘ I ∖ 0 → I ∈ Word 0 ..^ W
9 wrdf ⊢ I ∈ Word 0 ..^ W → I : 0 ..^ I ⟶ 0 ..^ W
10 8 9 syl ⊢ φ ∧ x ∈ dom ⁡ W ∘ I ∖ 0 → I : 0 ..^ I ⟶ 0 ..^ W
11 eldifi ⊢ x ∈ dom ⁡ W ∘ I ∖ 0 → x ∈ dom ⁡ W ∘ I
12 wrddm ⊢ W ∘ I ∈ Word A → dom ⁡ W ∘ I = 0 ..^ W ∘ I
13 4 12 syl ⊢ φ → dom ⁡ W ∘ I = 0 ..^ W ∘ I
14 1 2 chnsubseqwl ⊢ φ → W ∘ I = I
15 14 oveq2d ⊢ φ → 0 ..^ W ∘ I = 0 ..^ I
16 13 15 eqtrd ⊢ φ → dom ⁡ W ∘ I = 0 ..^ I
17 16 eleq2d ⊢ φ → x ∈ dom ⁡ W ∘ I ↔ x ∈ 0 ..^ I
18 17 biimpa ⊢ φ ∧ x ∈ dom ⁡ W ∘ I → x ∈ 0 ..^ I
19 11 18 sylan2 ⊢ φ ∧ x ∈ dom ⁡ W ∘ I ∖ 0 → x ∈ 0 ..^ I
20 10 19 ffvelcdmd ⊢ φ ∧ x ∈ dom ⁡ W ∘ I ∖ 0 → I ⁡ x ∈ 0 ..^ W
21 elfzonn0 ⊢ x ∈ 0 ..^ I → x ∈ ℕ 0
22 19 21 syl ⊢ φ ∧ x ∈ dom ⁡ W ∘ I ∖ 0 → x ∈ ℕ 0
23 simpr ⊢ φ ∧ x ∈ dom ⁡ W ∘ I ∖ 0 → x ∈ dom ⁡ W ∘ I ∖ 0
24 23 eldifsnbd ⊢ φ ∧ x ∈ dom ⁡ W ∘ I ∖ 0 → x ≠ 0
25 elnnne0 ⊢ x ∈ ℕ ↔ x ∈ ℕ 0 ∧ x ≠ 0
26 22 24 25 sylanbrc ⊢ φ ∧ x ∈ dom ⁡ W ∘ I ∖ 0 → x ∈ ℕ
27 nnm1ge0 ⊢ x ∈ ℕ → 0 ≤ x − 1
28 26 27 syl ⊢ φ ∧ x ∈ dom ⁡ W ∘ I ∖ 0 → 0 ≤ x − 1
29 22 nn0red ⊢ φ ∧ x ∈ dom ⁡ W ∘ I ∖ 0 → x ∈ ℝ
30 peano2rem ⊢ x ∈ ℝ → x − 1 ∈ ℝ
31 29 30 syl ⊢ φ ∧ x ∈ dom ⁡ W ∘ I ∖ 0 → x − 1 ∈ ℝ
32 lencl ⊢ I ∈ Word 0 ..^ W → I ∈ ℕ 0
33 7 32 syl ⊢ φ → I ∈ ℕ 0
34 33 adantr ⊢ φ ∧ x ∈ dom ⁡ W ∘ I ∖ 0 → I ∈ ℕ 0
35 34 nn0red ⊢ φ ∧ x ∈ dom ⁡ W ∘ I ∖ 0 → I ∈ ℝ
36 29 ltm1d ⊢ φ ∧ x ∈ dom ⁡ W ∘ I ∖ 0 → x − 1 < x
37 11 adantl ⊢ φ ∧ x ∈ dom ⁡ W ∘ I ∖ 0 → x ∈ dom ⁡ W ∘ I
38 13 adantr ⊢ φ ∧ x ∈ dom ⁡ W ∘ I ∖ 0 → dom ⁡ W ∘ I = 0 ..^ W ∘ I
39 37 38 eleqtrd ⊢ φ ∧ x ∈ dom ⁡ W ∘ I ∖ 0 → x ∈ 0 ..^ W ∘ I
40 elfzolt2 ⊢ x ∈ 0 ..^ W ∘ I → x < W ∘ I
41 39 40 syl ⊢ φ ∧ x ∈ dom ⁡ W ∘ I ∖ 0 → x < W ∘ I
42 14 adantr ⊢ φ ∧ x ∈ dom ⁡ W ∘ I ∖ 0 → W ∘ I = I
43 41 42 breqtrd ⊢ φ ∧ x ∈ dom ⁡ W ∘ I ∖ 0 → x < I
44 31 29 35 36 43 lttrd ⊢ φ ∧ x ∈ dom ⁡ W ∘ I ∖ 0 → x − 1 < I
45 elfzoelz ⊢ x ∈ 0 ..^ I → x ∈ ℤ
46 peano2zm ⊢ x ∈ ℤ → x − 1 ∈ ℤ
47 19 45 46 3syl ⊢ φ ∧ x ∈ dom ⁡ W ∘ I ∖ 0 → x − 1 ∈ ℤ
48 0zd ⊢ φ ∧ x ∈ dom ⁡ W ∘ I ∖ 0 → 0 ∈ ℤ
49 33 nn0zd ⊢ φ → I ∈ ℤ
50 49 adantr ⊢ φ ∧ x ∈ dom ⁡ W ∘ I ∖ 0 → I ∈ ℤ
51 elfzo ⊢ x − 1 ∈ ℤ ∧ 0 ∈ ℤ ∧ I ∈ ℤ → x − 1 ∈ 0 ..^ I ↔ 0 ≤ x − 1 ∧ x − 1 < I
52 47 48 50 51 syl3anc ⊢ φ ∧ x ∈ dom ⁡ W ∘ I ∖ 0 → x − 1 ∈ 0 ..^ I ↔ 0 ≤ x − 1 ∧ x − 1 < I
53 28 44 52 mpbir2and ⊢ φ ∧ x ∈ dom ⁡ W ∘ I ∖ 0 → x − 1 ∈ 0 ..^ I
54 10 53 ffvelcdmd ⊢ φ ∧ x ∈ dom ⁡ W ∘ I ∖ 0 → I ⁡ x − 1 ∈ 0 ..^ W
55 elfzonn0 ⊢ I ⁡ x − 1 ∈ 0 ..^ W → I ⁡ x − 1 ∈ ℕ 0
56 54 55 syl ⊢ φ ∧ x ∈ dom ⁡ W ∘ I ∖ 0 → I ⁡ x − 1 ∈ ℕ 0
57 elfzoelz ⊢ I ⁡ x ∈ 0 ..^ W → I ⁡ x ∈ ℤ
58 20 57 syl ⊢ φ ∧ x ∈ dom ⁡ W ∘ I ∖ 0 → I ⁡ x ∈ ℤ
59 2 adantr ⊢ φ ∧ x ∈ dom ⁡ W ∘ I ∖ 0 → I ∈ Chain 0 ..^ W <
60 wrddm ⊢ I ∈ Word 0 ..^ W → dom ⁡ I = 0 ..^ I
61 7 60 syl ⊢ φ → dom ⁡ I = 0 ..^ I
62 15 13 61 3eqtr4d ⊢ φ → dom ⁡ W ∘ I = dom ⁡ I
63 62 difeq1d ⊢ φ → dom ⁡ W ∘ I ∖ 0 = dom ⁡ I ∖ 0
64 63 eleq2d ⊢ φ → x ∈ dom ⁡ W ∘ I ∖ 0 ↔ x ∈ dom ⁡ I ∖ 0
65 64 biimpa ⊢ φ ∧ x ∈ dom ⁡ W ∘ I ∖ 0 → x ∈ dom ⁡ I ∖ 0
66 59 65 chnltm1 ⊢ φ ∧ x ∈ dom ⁡ W ∘ I ∖ 0 → I ⁡ x − 1 < I ⁡ x
67 elfzo0z ⊢ I ⁡ x − 1 ∈ 0 ..^ I ⁡ x ↔ I ⁡ x − 1 ∈ ℕ 0 ∧ I ⁡ x ∈ ℤ ∧ I ⁡ x − 1 < I ⁡ x
68 56 58 66 67 syl3anbrc ⊢ φ ∧ x ∈ dom ⁡ W ∘ I ∖ 0 → I ⁡ x − 1 ∈ 0 ..^ I ⁡ x
69 5 6 20 68 chnlt ⊢ φ ∧ x ∈ dom ⁡ W ∘ I ∖ 0 → W ⁡ I ⁡ x − 1 < ˙ W ⁡ I ⁡ x
70 10 53 fvco3d ⊢ φ ∧ x ∈ dom ⁡ W ∘ I ∖ 0 → W ∘ I ⁡ x − 1 = W ⁡ I ⁡ x − 1
71 10 19 fvco3d ⊢ φ ∧ x ∈ dom ⁡ W ∘ I ∖ 0 → W ∘ I ⁡ x = W ⁡ I ⁡ x
72 69 70 71 3brtr4d ⊢ φ ∧ x ∈ dom ⁡ W ∘ I ∖ 0 → W ∘ I ⁡ x − 1 < ˙ W ∘ I ⁡ x
73 72 ralrimiva ⊢ φ → ∀ x ∈ dom ⁡ W ∘ I ∖ 0 W ∘ I ⁡ x − 1 < ˙ W ∘ I ⁡ x
74 ischn ⊢ W ∘ I ∈ Chain A < ˙ ↔ W ∘ I ∈ Word A ∧ ∀ x ∈ dom ⁡ W ∘ I ∖ 0 W ∘ I ⁡ x − 1 < ˙ W ∘ I ⁡ x
75 4 73 74 sylanbrc ⊢ φ → W ∘ I ∈ Chain A < ˙