Metamath Proof Explorer

Theorem chnso

Description: A chain induces a total order. (Contributed by Thierry Arnoux, 19-Jun-2025)

Ref Expression
Assertion chnso 
|- ( ( .< Po A /\ C e. ( .< Chain A ) ) -> .< Or ran C )

Proof

Step Hyp Ref Expression
1 eqidd 
 |-  ( ( .< Po A /\ C e. ( .< Chain A ) ) -> ( # ` C ) = ( # ` C ) )
2 ischn 
 |-  ( C e. ( .< Chain A ) <-> ( C e. Word A /\ A. n e. ( dom C \ { 0 } ) ( C ` ( n - 1 ) ) .< ( C ` n ) ) )
3 2 biimpi 
 |-  ( C e. ( .< Chain A ) -> ( C e. Word A /\ A. n e. ( dom C \ { 0 } ) ( C ` ( n - 1 ) ) .< ( C ` n ) ) )
4 3 adantl 
 |-  ( ( .< Po A /\ C e. ( .< Chain A ) ) -> ( C e. Word A /\ A. n e. ( dom C \ { 0 } ) ( C ` ( n - 1 ) ) .< ( C ` n ) ) )
5 4 simpld 
 |-  ( ( .< Po A /\ C e. ( .< Chain A ) ) -> C e. Word A )
6 1 5 wrdfd 
 |-  ( ( .< Po A /\ C e. ( .< Chain A ) ) -> C : ( 0 ..^ ( # ` C ) ) --> A )
7 6 frnd 
 |-  ( ( .< Po A /\ C e. ( .< Chain A ) ) -> ran C C_ A )
8 simpl 
 |-  ( ( .< Po A /\ C e. ( .< Chain A ) ) -> .< Po A )
9 poss 
 |-  ( ran C C_ A -> ( .< Po A -> .< Po ran C ) )
10 7 8 9 sylc 
 |-  ( ( .< Po A /\ C e. ( .< Chain A ) ) -> .< Po ran C )
11 fzossz 
 |-  ( 0 ..^ ( # ` C ) ) C_ ZZ
12 simp-4r 
 |-  ( ( ( ( ( ( ( ( .< Po A /\ C e. ( .< Chain A ) ) /\ x e. ran C ) /\ y e. ran C ) /\ i e. ( 0 ..^ ( # ` C ) ) ) /\ ( C ` i ) = x ) /\ j e. ( 0 ..^ ( # ` C ) ) ) /\ ( C ` j ) = y ) -> i e. ( 0 ..^ ( # ` C ) ) )
13 11 12 sselid 
 |-  ( ( ( ( ( ( ( ( .< Po A /\ C e. ( .< Chain A ) ) /\ x e. ran C ) /\ y e. ran C ) /\ i e. ( 0 ..^ ( # ` C ) ) ) /\ ( C ` i ) = x ) /\ j e. ( 0 ..^ ( # ` C ) ) ) /\ ( C ` j ) = y ) -> i e. ZZ )
14 13 zred 
 |-  ( ( ( ( ( ( ( ( .< Po A /\ C e. ( .< Chain A ) ) /\ x e. ran C ) /\ y e. ran C ) /\ i e. ( 0 ..^ ( # ` C ) ) ) /\ ( C ` i ) = x ) /\ j e. ( 0 ..^ ( # ` C ) ) ) /\ ( C ` j ) = y ) -> i e. RR )
15 simplr 
 |-  ( ( ( ( ( ( ( ( .< Po A /\ C e. ( .< Chain A ) ) /\ x e. ran C ) /\ y e. ran C ) /\ i e. ( 0 ..^ ( # ` C ) ) ) /\ ( C ` i ) = x ) /\ j e. ( 0 ..^ ( # ` C ) ) ) /\ ( C ` j ) = y ) -> j e. ( 0 ..^ ( # ` C ) ) )
16 11 15 sselid 
 |-  ( ( ( ( ( ( ( ( .< Po A /\ C e. ( .< Chain A ) ) /\ x e. ran C ) /\ y e. ran C ) /\ i e. ( 0 ..^ ( # ` C ) ) ) /\ ( C ` i ) = x ) /\ j e. ( 0 ..^ ( # ` C ) ) ) /\ ( C ` j ) = y ) -> j e. ZZ )
17 16 zred 
 |-  ( ( ( ( ( ( ( ( .< Po A /\ C e. ( .< Chain A ) ) /\ x e. ran C ) /\ y e. ran C ) /\ i e. ( 0 ..^ ( # ` C ) ) ) /\ ( C ` i ) = x ) /\ j e. ( 0 ..^ ( # ` C ) ) ) /\ ( C ` j ) = y ) -> j e. RR )
18 14 17 lttri4d 
 |-  ( ( ( ( ( ( ( ( .< Po A /\ C e. ( .< Chain A ) ) /\ x e. ran C ) /\ y e. ran C ) /\ i e. ( 0 ..^ ( # ` C ) ) ) /\ ( C ` i ) = x ) /\ j e. ( 0 ..^ ( # ` C ) ) ) /\ ( C ` j ) = y ) -> ( i < j \/ i = j \/ j < i ) )
19 simp-8l 
 |-  ( ( ( ( ( ( ( ( ( .< Po A /\ C e. ( .< Chain A ) ) /\ x e. ran C ) /\ y e. ran C ) /\ i e. ( 0 ..^ ( # ` C ) ) ) /\ ( C ` i ) = x ) /\ j e. ( 0 ..^ ( # ` C ) ) ) /\ ( C ` j ) = y ) /\ i < j ) -> .< Po A )
20 simp-8r 
 |-  ( ( ( ( ( ( ( ( ( .< Po A /\ C e. ( .< Chain A ) ) /\ x e. ran C ) /\ y e. ran C ) /\ i e. ( 0 ..^ ( # ` C ) ) ) /\ ( C ` i ) = x ) /\ j e. ( 0 ..^ ( # ` C ) ) ) /\ ( C ` j ) = y ) /\ i < j ) -> C e. ( .< Chain A ) )
21 simpllr 
 |-  ( ( ( ( ( ( ( ( ( .< Po A /\ C e. ( .< Chain A ) ) /\ x e. ran C ) /\ y e. ran C ) /\ i e. ( 0 ..^ ( # ` C ) ) ) /\ ( C ` i ) = x ) /\ j e. ( 0 ..^ ( # ` C ) ) ) /\ ( C ` j ) = y ) /\ i < j ) -> j e. ( 0 ..^ ( # ` C ) ) )
22 elfzouz 
 |-  ( i e. ( 0 ..^ ( # ` C ) ) -> i e. ( ZZ>= ` 0 ) )
23 22 ad5antlr 
 |-  ( ( ( ( ( ( ( ( ( .< Po A /\ C e. ( .< Chain A ) ) /\ x e. ran C ) /\ y e. ran C ) /\ i e. ( 0 ..^ ( # ` C ) ) ) /\ ( C ` i ) = x ) /\ j e. ( 0 ..^ ( # ` C ) ) ) /\ ( C ` j ) = y ) /\ i < j ) -> i e. ( ZZ>= ` 0 ) )
24 16 adantr 
 |-  ( ( ( ( ( ( ( ( ( .< Po A /\ C e. ( .< Chain A ) ) /\ x e. ran C ) /\ y e. ran C ) /\ i e. ( 0 ..^ ( # ` C ) ) ) /\ ( C ` i ) = x ) /\ j e. ( 0 ..^ ( # ` C ) ) ) /\ ( C ` j ) = y ) /\ i < j ) -> j e. ZZ )
25 simpr 
 |-  ( ( ( ( ( ( ( ( ( .< Po A /\ C e. ( .< Chain A ) ) /\ x e. ran C ) /\ y e. ran C ) /\ i e. ( 0 ..^ ( # ` C ) ) ) /\ ( C ` i ) = x ) /\ j e. ( 0 ..^ ( # ` C ) ) ) /\ ( C ` j ) = y ) /\ i < j ) -> i < j )
26 elfzo2 
 |-  ( i e. ( 0 ..^ j ) <-> ( i e. ( ZZ>= ` 0 ) /\ j e. ZZ /\ i < j ) )
27 23 24 25 26 syl3anbrc 
 |-  ( ( ( ( ( ( ( ( ( .< Po A /\ C e. ( .< Chain A ) ) /\ x e. ran C ) /\ y e. ran C ) /\ i e. ( 0 ..^ ( # ` C ) ) ) /\ ( C ` i ) = x ) /\ j e. ( 0 ..^ ( # ` C ) ) ) /\ ( C ` j ) = y ) /\ i < j ) -> i e. ( 0 ..^ j ) )
28 19 20 21 27 chnlt 
 |-  ( ( ( ( ( ( ( ( ( .< Po A /\ C e. ( .< Chain A ) ) /\ x e. ran C ) /\ y e. ran C ) /\ i e. ( 0 ..^ ( # ` C ) ) ) /\ ( C ` i ) = x ) /\ j e. ( 0 ..^ ( # ` C ) ) ) /\ ( C ` j ) = y ) /\ i < j ) -> ( C ` i ) .< ( C ` j ) )
29 simp-4r 
 |-  ( ( ( ( ( ( ( ( ( .< Po A /\ C e. ( .< Chain A ) ) /\ x e. ran C ) /\ y e. ran C ) /\ i e. ( 0 ..^ ( # ` C ) ) ) /\ ( C ` i ) = x ) /\ j e. ( 0 ..^ ( # ` C ) ) ) /\ ( C ` j ) = y ) /\ i < j ) -> ( C ` i ) = x )
30 simplr 
 |-  ( ( ( ( ( ( ( ( ( .< Po A /\ C e. ( .< Chain A ) ) /\ x e. ran C ) /\ y e. ran C ) /\ i e. ( 0 ..^ ( # ` C ) ) ) /\ ( C ` i ) = x ) /\ j e. ( 0 ..^ ( # ` C ) ) ) /\ ( C ` j ) = y ) /\ i < j ) -> ( C ` j ) = y )
31 28 29 30 3brtr3d 
 |-  ( ( ( ( ( ( ( ( ( .< Po A /\ C e. ( .< Chain A ) ) /\ x e. ran C ) /\ y e. ran C ) /\ i e. ( 0 ..^ ( # ` C ) ) ) /\ ( C ` i ) = x ) /\ j e. ( 0 ..^ ( # ` C ) ) ) /\ ( C ` j ) = y ) /\ i < j ) -> x .< y )
32 31 ex 
 |-  ( ( ( ( ( ( ( ( .< Po A /\ C e. ( .< Chain A ) ) /\ x e. ran C ) /\ y e. ran C ) /\ i e. ( 0 ..^ ( # ` C ) ) ) /\ ( C ` i ) = x ) /\ j e. ( 0 ..^ ( # ` C ) ) ) /\ ( C ` j ) = y ) -> ( i < j -> x .< y ) )
33 simpr 
 |-  ( ( ( ( ( ( ( ( ( .< Po A /\ C e. ( .< Chain A ) ) /\ x e. ran C ) /\ y e. ran C ) /\ i e. ( 0 ..^ ( # ` C ) ) ) /\ ( C ` i ) = x ) /\ j e. ( 0 ..^ ( # ` C ) ) ) /\ ( C ` j ) = y ) /\ i = j ) -> i = j )
34 33 fveq2d 
 |-  ( ( ( ( ( ( ( ( ( .< Po A /\ C e. ( .< Chain A ) ) /\ x e. ran C ) /\ y e. ran C ) /\ i e. ( 0 ..^ ( # ` C ) ) ) /\ ( C ` i ) = x ) /\ j e. ( 0 ..^ ( # ` C ) ) ) /\ ( C ` j ) = y ) /\ i = j ) -> ( C ` i ) = ( C ` j ) )
35 simp-4r 
 |-  ( ( ( ( ( ( ( ( ( .< Po A /\ C e. ( .< Chain A ) ) /\ x e. ran C ) /\ y e. ran C ) /\ i e. ( 0 ..^ ( # ` C ) ) ) /\ ( C ` i ) = x ) /\ j e. ( 0 ..^ ( # ` C ) ) ) /\ ( C ` j ) = y ) /\ i = j ) -> ( C ` i ) = x )
36 simplr 
 |-  ( ( ( ( ( ( ( ( ( .< Po A /\ C e. ( .< Chain A ) ) /\ x e. ran C ) /\ y e. ran C ) /\ i e. ( 0 ..^ ( # ` C ) ) ) /\ ( C ` i ) = x ) /\ j e. ( 0 ..^ ( # ` C ) ) ) /\ ( C ` j ) = y ) /\ i = j ) -> ( C ` j ) = y )
37 34 35 36 3eqtr3d 
 |-  ( ( ( ( ( ( ( ( ( .< Po A /\ C e. ( .< Chain A ) ) /\ x e. ran C ) /\ y e. ran C ) /\ i e. ( 0 ..^ ( # ` C ) ) ) /\ ( C ` i ) = x ) /\ j e. ( 0 ..^ ( # ` C ) ) ) /\ ( C ` j ) = y ) /\ i = j ) -> x = y )
38 37 ex 
 |-  ( ( ( ( ( ( ( ( .< Po A /\ C e. ( .< Chain A ) ) /\ x e. ran C ) /\ y e. ran C ) /\ i e. ( 0 ..^ ( # ` C ) ) ) /\ ( C ` i ) = x ) /\ j e. ( 0 ..^ ( # ` C ) ) ) /\ ( C ` j ) = y ) -> ( i = j -> x = y ) )
39 simp-8l 
 |-  ( ( ( ( ( ( ( ( ( .< Po A /\ C e. ( .< Chain A ) ) /\ x e. ran C ) /\ y e. ran C ) /\ i e. ( 0 ..^ ( # ` C ) ) ) /\ ( C ` i ) = x ) /\ j e. ( 0 ..^ ( # ` C ) ) ) /\ ( C ` j ) = y ) /\ j < i ) -> .< Po A )
40 simp-8r 
 |-  ( ( ( ( ( ( ( ( ( .< Po A /\ C e. ( .< Chain A ) ) /\ x e. ran C ) /\ y e. ran C ) /\ i e. ( 0 ..^ ( # ` C ) ) ) /\ ( C ` i ) = x ) /\ j e. ( 0 ..^ ( # ` C ) ) ) /\ ( C ` j ) = y ) /\ j < i ) -> C e. ( .< Chain A ) )
41 12 adantr 
 |-  ( ( ( ( ( ( ( ( ( .< Po A /\ C e. ( .< Chain A ) ) /\ x e. ran C ) /\ y e. ran C ) /\ i e. ( 0 ..^ ( # ` C ) ) ) /\ ( C ` i ) = x ) /\ j e. ( 0 ..^ ( # ` C ) ) ) /\ ( C ` j ) = y ) /\ j < i ) -> i e. ( 0 ..^ ( # ` C ) ) )
42 elfzouz 
 |-  ( j e. ( 0 ..^ ( # ` C ) ) -> j e. ( ZZ>= ` 0 ) )
43 42 ad3antlr 
 |-  ( ( ( ( ( ( ( ( ( .< Po A /\ C e. ( .< Chain A ) ) /\ x e. ran C ) /\ y e. ran C ) /\ i e. ( 0 ..^ ( # ` C ) ) ) /\ ( C ` i ) = x ) /\ j e. ( 0 ..^ ( # ` C ) ) ) /\ ( C ` j ) = y ) /\ j < i ) -> j e. ( ZZ>= ` 0 ) )
44 13 adantr 
 |-  ( ( ( ( ( ( ( ( ( .< Po A /\ C e. ( .< Chain A ) ) /\ x e. ran C ) /\ y e. ran C ) /\ i e. ( 0 ..^ ( # ` C ) ) ) /\ ( C ` i ) = x ) /\ j e. ( 0 ..^ ( # ` C ) ) ) /\ ( C ` j ) = y ) /\ j < i ) -> i e. ZZ )
45 simpr 
 |-  ( ( ( ( ( ( ( ( ( .< Po A /\ C e. ( .< Chain A ) ) /\ x e. ran C ) /\ y e. ran C ) /\ i e. ( 0 ..^ ( # ` C ) ) ) /\ ( C ` i ) = x ) /\ j e. ( 0 ..^ ( # ` C ) ) ) /\ ( C ` j ) = y ) /\ j < i ) -> j < i )
46 elfzo2 
 |-  ( j e. ( 0 ..^ i ) <-> ( j e. ( ZZ>= ` 0 ) /\ i e. ZZ /\ j < i ) )
47 43 44 45 46 syl3anbrc 
 |-  ( ( ( ( ( ( ( ( ( .< Po A /\ C e. ( .< Chain A ) ) /\ x e. ran C ) /\ y e. ran C ) /\ i e. ( 0 ..^ ( # ` C ) ) ) /\ ( C ` i ) = x ) /\ j e. ( 0 ..^ ( # ` C ) ) ) /\ ( C ` j ) = y ) /\ j < i ) -> j e. ( 0 ..^ i ) )
48 39 40 41 47 chnlt 
 |-  ( ( ( ( ( ( ( ( ( .< Po A /\ C e. ( .< Chain A ) ) /\ x e. ran C ) /\ y e. ran C ) /\ i e. ( 0 ..^ ( # ` C ) ) ) /\ ( C ` i ) = x ) /\ j e. ( 0 ..^ ( # ` C ) ) ) /\ ( C ` j ) = y ) /\ j < i ) -> ( C ` j ) .< ( C ` i ) )
49 simplr 
 |-  ( ( ( ( ( ( ( ( ( .< Po A /\ C e. ( .< Chain A ) ) /\ x e. ran C ) /\ y e. ran C ) /\ i e. ( 0 ..^ ( # ` C ) ) ) /\ ( C ` i ) = x ) /\ j e. ( 0 ..^ ( # ` C ) ) ) /\ ( C ` j ) = y ) /\ j < i ) -> ( C ` j ) = y )
50 simp-4r 
 |-  ( ( ( ( ( ( ( ( ( .< Po A /\ C e. ( .< Chain A ) ) /\ x e. ran C ) /\ y e. ran C ) /\ i e. ( 0 ..^ ( # ` C ) ) ) /\ ( C ` i ) = x ) /\ j e. ( 0 ..^ ( # ` C ) ) ) /\ ( C ` j ) = y ) /\ j < i ) -> ( C ` i ) = x )
51 48 49 50 3brtr3d 
 |-  ( ( ( ( ( ( ( ( ( .< Po A /\ C e. ( .< Chain A ) ) /\ x e. ran C ) /\ y e. ran C ) /\ i e. ( 0 ..^ ( # ` C ) ) ) /\ ( C ` i ) = x ) /\ j e. ( 0 ..^ ( # ` C ) ) ) /\ ( C ` j ) = y ) /\ j < i ) -> y .< x )
52 51 ex 
 |-  ( ( ( ( ( ( ( ( .< Po A /\ C e. ( .< Chain A ) ) /\ x e. ran C ) /\ y e. ran C ) /\ i e. ( 0 ..^ ( # ` C ) ) ) /\ ( C ` i ) = x ) /\ j e. ( 0 ..^ ( # ` C ) ) ) /\ ( C ` j ) = y ) -> ( j < i -> y .< x ) )
53 32 38 52 3orim123d 
 |-  ( ( ( ( ( ( ( ( .< Po A /\ C e. ( .< Chain A ) ) /\ x e. ran C ) /\ y e. ran C ) /\ i e. ( 0 ..^ ( # ` C ) ) ) /\ ( C ` i ) = x ) /\ j e. ( 0 ..^ ( # ` C ) ) ) /\ ( C ` j ) = y ) -> ( ( i < j \/ i = j \/ j < i ) -> ( x .< y \/ x = y \/ y .< x ) ) )
54 18 53 mpd 
 |-  ( ( ( ( ( ( ( ( .< Po A /\ C e. ( .< Chain A ) ) /\ x e. ran C ) /\ y e. ran C ) /\ i e. ( 0 ..^ ( # ` C ) ) ) /\ ( C ` i ) = x ) /\ j e. ( 0 ..^ ( # ` C ) ) ) /\ ( C ` j ) = y ) -> ( x .< y \/ x = y \/ y .< x ) )
55 6 ffnd 
 |-  ( ( .< Po A /\ C e. ( .< Chain A ) ) -> C Fn ( 0 ..^ ( # ` C ) ) )
56 55 ad4antr 
 |-  ( ( ( ( ( ( .< Po A /\ C e. ( .< Chain A ) ) /\ x e. ran C ) /\ y e. ran C ) /\ i e. ( 0 ..^ ( # ` C ) ) ) /\ ( C ` i ) = x ) -> C Fn ( 0 ..^ ( # ` C ) ) )
57 simpllr 
 |-  ( ( ( ( ( ( .< Po A /\ C e. ( .< Chain A ) ) /\ x e. ran C ) /\ y e. ran C ) /\ i e. ( 0 ..^ ( # ` C ) ) ) /\ ( C ` i ) = x ) -> y e. ran C )
58 fvelrnb 
 |-  ( C Fn ( 0 ..^ ( # ` C ) ) -> ( y e. ran C <-> E. j e. ( 0 ..^ ( # ` C ) ) ( C ` j ) = y ) )
59 58 biimpa 
 |-  ( ( C Fn ( 0 ..^ ( # ` C ) ) /\ y e. ran C ) -> E. j e. ( 0 ..^ ( # ` C ) ) ( C ` j ) = y )
60 56 57 59 syl2anc 
 |-  ( ( ( ( ( ( .< Po A /\ C e. ( .< Chain A ) ) /\ x e. ran C ) /\ y e. ran C ) /\ i e. ( 0 ..^ ( # ` C ) ) ) /\ ( C ` i ) = x ) -> E. j e. ( 0 ..^ ( # ` C ) ) ( C ` j ) = y )
61 54 60 r19.29a 
 |-  ( ( ( ( ( ( .< Po A /\ C e. ( .< Chain A ) ) /\ x e. ran C ) /\ y e. ran C ) /\ i e. ( 0 ..^ ( # ` C ) ) ) /\ ( C ` i ) = x ) -> ( x .< y \/ x = y \/ y .< x ) )
62 55 ad2antrr 
 |-  ( ( ( ( .< Po A /\ C e. ( .< Chain A ) ) /\ x e. ran C ) /\ y e. ran C ) -> C Fn ( 0 ..^ ( # ` C ) ) )
63 simplr 
 |-  ( ( ( ( .< Po A /\ C e. ( .< Chain A ) ) /\ x e. ran C ) /\ y e. ran C ) -> x e. ran C )
64 fvelrnb 
 |-  ( C Fn ( 0 ..^ ( # ` C ) ) -> ( x e. ran C <-> E. i e. ( 0 ..^ ( # ` C ) ) ( C ` i ) = x ) )
65 64 biimpa 
 |-  ( ( C Fn ( 0 ..^ ( # ` C ) ) /\ x e. ran C ) -> E. i e. ( 0 ..^ ( # ` C ) ) ( C ` i ) = x )
66 62 63 65 syl2anc 
 |-  ( ( ( ( .< Po A /\ C e. ( .< Chain A ) ) /\ x e. ran C ) /\ y e. ran C ) -> E. i e. ( 0 ..^ ( # ` C ) ) ( C ` i ) = x )
67 61 66 r19.29a 
 |-  ( ( ( ( .< Po A /\ C e. ( .< Chain A ) ) /\ x e. ran C ) /\ y e. ran C ) -> ( x .< y \/ x = y \/ y .< x ) )
68 67 anasss 
 |-  ( ( ( .< Po A /\ C e. ( .< Chain A ) ) /\ ( x e. ran C /\ y e. ran C ) ) -> ( x .< y \/ x = y \/ y .< x ) )
69 10 68 issod 
 |-  ( ( .< Po A /\ C e. ( .< Chain A ) ) -> .< Or ran C )