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 eldifbd ⊢ φ ∧ x ∈ dom ⁡ W ∘ I ∖ 0 → ¬ x ∈ 0
25 velsn ⊢ x ∈ 0 ↔ x = 0
26 24 25 sylnib ⊢ φ ∧ x ∈ dom ⁡ W ∘ I ∖ 0 → ¬ x = 0
27 26 neqned ⊢ φ ∧ x ∈ dom ⁡ W ∘ I ∖ 0 → x ≠ 0
28 elnnne0 ⊢ x ∈ ℕ ↔ x ∈ ℕ 0 ∧ x ≠ 0
29 22 27 28 sylanbrc ⊢ φ ∧ x ∈ dom ⁡ W ∘ I ∖ 0 → x ∈ ℕ
30 nnm1ge0 ⊢ x ∈ ℕ → 0 ≤ x − 1
31 29 30 syl ⊢ φ ∧ x ∈ dom ⁡ W ∘ I ∖ 0 → 0 ≤ x − 1
32 22 nn0red ⊢ φ ∧ x ∈ dom ⁡ W ∘ I ∖ 0 → x ∈ ℝ
33 peano2rem ⊢ x ∈ ℝ → x − 1 ∈ ℝ
34 32 33 syl ⊢ φ ∧ x ∈ dom ⁡ W ∘ I ∖ 0 → x − 1 ∈ ℝ
35 lencl ⊢ I ∈ Word 0 ..^ W → I ∈ ℕ 0
36 7 35 syl ⊢ φ → I ∈ ℕ 0
37 36 adantr ⊢ φ ∧ x ∈ dom ⁡ W ∘ I ∖ 0 → I ∈ ℕ 0
38 37 nn0red ⊢ φ ∧ x ∈ dom ⁡ W ∘ I ∖ 0 → I ∈ ℝ
39 32 ltm1d ⊢ φ ∧ x ∈ dom ⁡ W ∘ I ∖ 0 → x − 1 < x
40 11 adantl ⊢ φ ∧ x ∈ dom ⁡ W ∘ I ∖ 0 → x ∈ dom ⁡ W ∘ I
41 13 adantr ⊢ φ ∧ x ∈ dom ⁡ W ∘ I ∖ 0 → dom ⁡ W ∘ I = 0 ..^ W ∘ I
42 40 41 eleqtrd ⊢ φ ∧ x ∈ dom ⁡ W ∘ I ∖ 0 → x ∈ 0 ..^ W ∘ I
43 elfzolt2 ⊢ x ∈ 0 ..^ W ∘ I → x < W ∘ I
44 42 43 syl ⊢ φ ∧ x ∈ dom ⁡ W ∘ I ∖ 0 → x < W ∘ I
45 14 adantr ⊢ φ ∧ x ∈ dom ⁡ W ∘ I ∖ 0 → W ∘ I = I
46 44 45 breqtrd ⊢ φ ∧ x ∈ dom ⁡ W ∘ I ∖ 0 → x < I
47 34 32 38 39 46 lttrd ⊢ φ ∧ x ∈ dom ⁡ W ∘ I ∖ 0 → x − 1 < I
48 elfzoelz ⊢ x ∈ 0 ..^ I → x ∈ ℤ
49 19 48 syl ⊢ φ ∧ x ∈ dom ⁡ W ∘ I ∖ 0 → x ∈ ℤ
50 peano2zm ⊢ x ∈ ℤ → x − 1 ∈ ℤ
51 49 50 syl ⊢ φ ∧ x ∈ dom ⁡ W ∘ I ∖ 0 → x − 1 ∈ ℤ
52 0zd ⊢ φ ∧ x ∈ dom ⁡ W ∘ I ∖ 0 → 0 ∈ ℤ
53 36 nn0zd ⊢ φ → I ∈ ℤ
54 53 adantr ⊢ φ ∧ x ∈ dom ⁡ W ∘ I ∖ 0 → I ∈ ℤ
55 elfzo ⊢ x − 1 ∈ ℤ ∧ 0 ∈ ℤ ∧ I ∈ ℤ → x − 1 ∈ 0 ..^ I ↔ 0 ≤ x − 1 ∧ x − 1 < I
56 51 52 54 55 syl3anc ⊢ φ ∧ x ∈ dom ⁡ W ∘ I ∖ 0 → x − 1 ∈ 0 ..^ I ↔ 0 ≤ x − 1 ∧ x − 1 < I
57 31 47 56 mpbir2and ⊢ φ ∧ x ∈ dom ⁡ W ∘ I ∖ 0 → x − 1 ∈ 0 ..^ I
58 10 57 ffvelcdmd ⊢ φ ∧ x ∈ dom ⁡ W ∘ I ∖ 0 → I ⁡ x − 1 ∈ 0 ..^ W
59 elfzonn0 ⊢ I ⁡ x − 1 ∈ 0 ..^ W → I ⁡ x − 1 ∈ ℕ 0
60 58 59 syl ⊢ φ ∧ x ∈ dom ⁡ W ∘ I ∖ 0 → I ⁡ x − 1 ∈ ℕ 0
61 elfzoelz ⊢ I ⁡ x ∈ 0 ..^ W → I ⁡ x ∈ ℤ
62 20 61 syl ⊢ φ ∧ x ∈ dom ⁡ W ∘ I ∖ 0 → I ⁡ x ∈ ℤ
63 2 adantr ⊢ φ ∧ x ∈ dom ⁡ W ∘ I ∖ 0 → I ∈ Chain 0 ..^ W <
64 wrddm ⊢ I ∈ Word 0 ..^ W → dom ⁡ I = 0 ..^ I
65 7 64 syl ⊢ φ → dom ⁡ I = 0 ..^ I
66 15 13 65 3eqtr4d ⊢ φ → dom ⁡ W ∘ I = dom ⁡ I
67 66 difeq1d ⊢ φ → dom ⁡ W ∘ I ∖ 0 = dom ⁡ I ∖ 0
68 67 eleq2d ⊢ φ → x ∈ dom ⁡ W ∘ I ∖ 0 ↔ x ∈ dom ⁡ I ∖ 0
69 68 biimpa ⊢ φ ∧ x ∈ dom ⁡ W ∘ I ∖ 0 → x ∈ dom ⁡ I ∖ 0
70 63 69 chnltm1 ⊢ φ ∧ x ∈ dom ⁡ W ∘ I ∖ 0 → I ⁡ x − 1 < I ⁡ x
71 elfzo0z ⊢ I ⁡ x − 1 ∈ 0 ..^ I ⁡ x ↔ I ⁡ x − 1 ∈ ℕ 0 ∧ I ⁡ x ∈ ℤ ∧ I ⁡ x − 1 < I ⁡ x
72 60 62 70 71 syl3anbrc ⊢ φ ∧ x ∈ dom ⁡ W ∘ I ∖ 0 → I ⁡ x − 1 ∈ 0 ..^ I ⁡ x
73 5 6 20 72 chnlt ⊢ φ ∧ x ∈ dom ⁡ W ∘ I ∖ 0 → W ⁡ I ⁡ x − 1 < ˙ W ⁡ I ⁡ x
74 10 57 fvco3d ⊢ φ ∧ x ∈ dom ⁡ W ∘ I ∖ 0 → W ∘ I ⁡ x − 1 = W ⁡ I ⁡ x − 1
75 10 19 fvco3d ⊢ φ ∧ x ∈ dom ⁡ W ∘ I ∖ 0 → W ∘ I ⁡ x = W ⁡ I ⁡ x
76 73 74 75 3brtr4d ⊢ φ ∧ x ∈ dom ⁡ W ∘ I ∖ 0 → W ∘ I ⁡ x − 1 < ˙ W ∘ I ⁡ x
77 76 ralrimiva ⊢ φ → ∀ x ∈ dom ⁡ W ∘ I ∖ 0 W ∘ I ⁡ x − 1 < ˙ W ∘ I ⁡ x
78 ischn ⊢ W ∘ I ∈ Chain A < ˙ ↔ W ∘ I ∈ Word A ∧ ∀ x ∈ dom ⁡ W ∘ I ∖ 0 W ∘ I ⁡ x − 1 < ˙ W ∘ I ⁡ x
79 4 77 78 sylanbrc ⊢ φ → W ∘ I ∈ Chain A < ˙