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 bilani 
 |-  ( ( .< Po A /\ C e. ( .< Chain A ) ) -> ( C e. Word A /\ A. n e. ( dom C \ { 0 } ) ( C ` ( n - 1 ) ) .< ( C ` n ) ) )
4 3 simpld 
 |-  ( ( .< Po A /\ C e. ( .< Chain A ) ) -> C e. Word A )
5 1 4 wrdfd 
 |-  ( ( .< Po A /\ C e. ( .< Chain A ) ) -> C : ( 0 ..^ ( # ` C ) ) --> A )
6 5 frnd 
 |-  ( ( .< Po A /\ C e. ( .< Chain A ) ) -> ran C C_ A )
7 simpl 
 |-  ( ( .< Po A /\ C e. ( .< Chain A ) ) -> .< Po A )
8 poss 
 |-  ( ran C C_ A -> ( .< Po A -> .< Po ran C ) )
9 6 7 8 sylc 
 |-  ( ( .< Po A /\ C e. ( .< Chain A ) ) -> .< Po ran C )
10 fzossz 
 |-  ( 0 ..^ ( # ` C ) ) C_ ZZ
11 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 ) ) )
12 10 11 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 )
13 12 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 )
14 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 ) ) )
15 10 14 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 )
16 15 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 )
17 13 16 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 ) )
18 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 )
19 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 ) )
20 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 ) ) )
21 elfzouz 
 |-  ( i e. ( 0 ..^ ( # ` C ) ) -> i e. ( ZZ>= ` 0 ) )
22 21 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 ) )
23 15 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 )
24 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 )
25 elfzo2 
 |-  ( i e. ( 0 ..^ j ) <-> ( i e. ( ZZ>= ` 0 ) /\ j e. ZZ /\ i < j ) )
26 22 23 24 25 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 ) )
27 18 19 20 26 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 ) )
28 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 )
29 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 )
30 27 28 29 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 )
31 30 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 ) )
32 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 )
33 32 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 ) )
34 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 )
35 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 )
36 33 34 35 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 )
37 36 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 ) )
38 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 )
39 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 ) )
40 11 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 ) ) )
41 elfzouz 
 |-  ( j e. ( 0 ..^ ( # ` C ) ) -> j e. ( ZZ>= ` 0 ) )
42 41 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 ) )
43 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. ZZ )
44 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 )
45 elfzo2 
 |-  ( j e. ( 0 ..^ i ) <-> ( j e. ( ZZ>= ` 0 ) /\ i e. ZZ /\ j < i ) )
46 42 43 44 45 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 ) )
47 38 39 40 46 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 ) )
48 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 )
49 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 )
50 47 48 49 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 )
51 50 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 ) )
52 31 37 51 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 ) ) )
53 17 52 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 ) )
54 5 ffnd 
 |-  ( ( .< Po A /\ C e. ( .< Chain A ) ) -> C Fn ( 0 ..^ ( # ` C ) ) )
55 54 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 ) ) )
56 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 )
57 fvelrnb 
 |-  ( C Fn ( 0 ..^ ( # ` C ) ) -> ( y e. ran C <-> E. j e. ( 0 ..^ ( # ` C ) ) ( C ` j ) = y ) )
58 57 biimpa 
 |-  ( ( C Fn ( 0 ..^ ( # ` C ) ) /\ y e. ran C ) -> E. j e. ( 0 ..^ ( # ` C ) ) ( C ` j ) = y )
59 55 56 58 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 )
60 53 59 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 ) )
61 54 ad2antrr 
 |-  ( ( ( ( .< Po A /\ C e. ( .< Chain A ) ) /\ x e. ran C ) /\ y e. ran C ) -> C Fn ( 0 ..^ ( # ` C ) ) )
62 simplr 
 |-  ( ( ( ( .< Po A /\ C e. ( .< Chain A ) ) /\ x e. ran C ) /\ y e. ran C ) -> x e. ran C )
63 fvelrnb 
 |-  ( C Fn ( 0 ..^ ( # ` C ) ) -> ( x e. ran C <-> E. i e. ( 0 ..^ ( # ` C ) ) ( C ` i ) = x ) )
64 63 biimpa 
 |-  ( ( C Fn ( 0 ..^ ( # ` C ) ) /\ x e. ran C ) -> E. i e. ( 0 ..^ ( # ` C ) ) ( C ` i ) = x )
65 61 62 64 syl2anc 
 |-  ( ( ( ( .< Po A /\ C e. ( .< Chain A ) ) /\ x e. ran C ) /\ y e. ran C ) -> E. i e. ( 0 ..^ ( # ` C ) ) ( C ` i ) = x )
66 60 65 r19.29a 
 |-  ( ( ( ( .< Po A /\ C e. ( .< Chain A ) ) /\ x e. ran C ) /\ y e. ran C ) -> ( x .< y \/ x = y \/ y .< x ) )
67 66 anasss 
 |-  ( ( ( .< Po A /\ C e. ( .< Chain A ) ) /\ ( x e. ran C /\ y e. ran C ) ) -> ( x .< y \/ x = y \/ y .< x ) )
68 9 67 issod 
 |-  ( ( .< Po A /\ C e. ( .< Chain A ) ) -> .< Or ran C )