Metamath Proof Explorer

Theorem chnpof1

Description: A chain under relation which orders the alphabet is a one-to-one function from its domain to alphabet. (Contributed by Ender Ting, 20-Jan-2026)

Ref Expression
Hypotheses chnpof1.1 
|- ( ph -> .< Po A )
chnpof1.2 
|- ( ph -> B e. ( .< Chain A ) )
Assertion chnpof1 
|- ( ph -> B : ( 0 ..^ ( # ` B ) ) -1-1-> A )

Proof

Step Hyp Ref Expression
1 chnpof1.1 
 |-  ( ph -> .< Po A )
2 chnpof1.2 
 |-  ( ph -> B e. ( .< Chain A ) )
3 chnf 
 |-  ( B e. ( .< Chain A ) -> B : ( 0 ..^ ( # ` B ) ) --> A )
4 2 3 syl 
 |-  ( ph -> B : ( 0 ..^ ( # ` B ) ) --> A )
5 1 adantr 
 |-  ( ( ph /\ ( i e. ( 0 ..^ ( # ` B ) ) /\ j e. ( 0 ..^ ( # ` B ) ) ) ) -> .< Po A )
6 5 adantr 
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ ( # ` B ) ) /\ j e. ( 0 ..^ ( # ` B ) ) ) ) /\ i < j ) -> .< Po A )
7 2 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ ( # ` B ) ) ) -> B e. ( .< Chain A ) )
8 7 3 syl 
 |-  ( ( ph /\ i e. ( 0 ..^ ( # ` B ) ) ) -> B : ( 0 ..^ ( # ` B ) ) --> A )
9 simpr 
 |-  ( ( ph /\ i e. ( 0 ..^ ( # ` B ) ) ) -> i e. ( 0 ..^ ( # ` B ) ) )
10 ffvelcdm 
 |-  ( ( B : ( 0 ..^ ( # ` B ) ) --> A /\ i e. ( 0 ..^ ( # ` B ) ) ) -> ( B ` i ) e. A )
11 8 9 10 syl2anc 
 |-  ( ( ph /\ i e. ( 0 ..^ ( # ` B ) ) ) -> ( B ` i ) e. A )
12 11 adantrr 
 |-  ( ( ph /\ ( i e. ( 0 ..^ ( # ` B ) ) /\ j e. ( 0 ..^ ( # ` B ) ) ) ) -> ( B ` i ) e. A )
13 4 adantr 
 |-  ( ( ph /\ ( i e. ( 0 ..^ ( # ` B ) ) /\ j e. ( 0 ..^ ( # ` B ) ) ) ) -> B : ( 0 ..^ ( # ` B ) ) --> A )
14 simpr 
 |-  ( ( i e. ( 0 ..^ ( # ` B ) ) /\ j e. ( 0 ..^ ( # ` B ) ) ) -> j e. ( 0 ..^ ( # ` B ) ) )
15 14 adantl 
 |-  ( ( ph /\ ( i e. ( 0 ..^ ( # ` B ) ) /\ j e. ( 0 ..^ ( # ` B ) ) ) ) -> j e. ( 0 ..^ ( # ` B ) ) )
16 ffvelcdm 
 |-  ( ( B : ( 0 ..^ ( # ` B ) ) --> A /\ j e. ( 0 ..^ ( # ` B ) ) ) -> ( B ` j ) e. A )
17 13 15 16 syl2anc 
 |-  ( ( ph /\ ( i e. ( 0 ..^ ( # ` B ) ) /\ j e. ( 0 ..^ ( # ` B ) ) ) ) -> ( B ` j ) e. A )
18 12 17 jca 
 |-  ( ( ph /\ ( i e. ( 0 ..^ ( # ` B ) ) /\ j e. ( 0 ..^ ( # ` B ) ) ) ) -> ( ( B ` i ) e. A /\ ( B ` j ) e. A ) )
19 18 adantr 
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ ( # ` B ) ) /\ j e. ( 0 ..^ ( # ` B ) ) ) ) /\ i < j ) -> ( ( B ` i ) e. A /\ ( B ` j ) e. A ) )
20 2 adantr 
 |-  ( ( ph /\ ( i e. ( 0 ..^ ( # ` B ) ) /\ j e. ( 0 ..^ ( # ` B ) ) ) ) -> B e. ( .< Chain A ) )
21 20 adantr 
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ ( # ` B ) ) /\ j e. ( 0 ..^ ( # ` B ) ) ) ) /\ i < j ) -> B e. ( .< Chain A ) )
22 15 adantr 
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ ( # ` B ) ) /\ j e. ( 0 ..^ ( # ` B ) ) ) ) /\ i < j ) -> j e. ( 0 ..^ ( # ` B ) ) )
23 simplrl 
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ ( # ` B ) ) /\ j e. ( 0 ..^ ( # ` B ) ) ) ) /\ i < j ) -> i e. ( 0 ..^ ( # ` B ) ) )
24 elfzonn0 
 |-  ( i e. ( 0 ..^ ( # ` B ) ) -> i e. NN0 )
25 23 24 syl 
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ ( # ` B ) ) /\ j e. ( 0 ..^ ( # ` B ) ) ) ) /\ i < j ) -> i e. NN0 )
26 elfzoelz 
 |-  ( j e. ( 0 ..^ ( # ` B ) ) -> j e. ZZ )
27 22 26 syl 
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ ( # ` B ) ) /\ j e. ( 0 ..^ ( # ` B ) ) ) ) /\ i < j ) -> j e. ZZ )
28 simpr 
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ ( # ` B ) ) /\ j e. ( 0 ..^ ( # ` B ) ) ) ) /\ i < j ) -> i < j )
29 25 27 28 3jca 
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ ( # ` B ) ) /\ j e. ( 0 ..^ ( # ` B ) ) ) ) /\ i < j ) -> ( i e. NN0 /\ j e. ZZ /\ i < j ) )
30 elfzo0z 
 |-  ( i e. ( 0 ..^ j ) <-> ( i e. NN0 /\ j e. ZZ /\ i < j ) )
31 29 30 sylibr 
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ ( # ` B ) ) /\ j e. ( 0 ..^ ( # ` B ) ) ) ) /\ i < j ) -> i e. ( 0 ..^ j ) )
32 6 21 22 31 chnlt 
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ ( # ` B ) ) /\ j e. ( 0 ..^ ( # ` B ) ) ) ) /\ i < j ) -> ( B ` i ) .< ( B ` j ) )
33 po2ne 
 |-  ( ( .< Po A /\ ( ( B ` i ) e. A /\ ( B ` j ) e. A ) /\ ( B ` i ) .< ( B ` j ) ) -> ( B ` i ) =/= ( B ` j ) )
34 6 19 32 33 syl3anc 
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ ( # ` B ) ) /\ j e. ( 0 ..^ ( # ` B ) ) ) ) /\ i < j ) -> ( B ` i ) =/= ( B ` j ) )
35 34 neneqd 
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ ( # ` B ) ) /\ j e. ( 0 ..^ ( # ` B ) ) ) ) /\ i < j ) -> -. ( B ` i ) = ( B ` j ) )
36 35 ex 
 |-  ( ( ph /\ ( i e. ( 0 ..^ ( # ` B ) ) /\ j e. ( 0 ..^ ( # ` B ) ) ) ) -> ( i < j -> -. ( B ` i ) = ( B ` j ) ) )
37 36 con2d 
 |-  ( ( ph /\ ( i e. ( 0 ..^ ( # ` B ) ) /\ j e. ( 0 ..^ ( # ` B ) ) ) ) -> ( ( B ` i ) = ( B ` j ) -> -. i < j ) )
38 37 imp 
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ ( # ` B ) ) /\ j e. ( 0 ..^ ( # ` B ) ) ) ) /\ ( B ` i ) = ( B ` j ) ) -> -. i < j )
39 5 adantr 
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ ( # ` B ) ) /\ j e. ( 0 ..^ ( # ` B ) ) ) ) /\ j < i ) -> .< Po A )
40 17 12 jca 
 |-  ( ( ph /\ ( i e. ( 0 ..^ ( # ` B ) ) /\ j e. ( 0 ..^ ( # ` B ) ) ) ) -> ( ( B ` j ) e. A /\ ( B ` i ) e. A ) )
41 40 adantr 
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ ( # ` B ) ) /\ j e. ( 0 ..^ ( # ` B ) ) ) ) /\ j < i ) -> ( ( B ` j ) e. A /\ ( B ` i ) e. A ) )
42 20 adantr 
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ ( # ` B ) ) /\ j e. ( 0 ..^ ( # ` B ) ) ) ) /\ j < i ) -> B e. ( .< Chain A ) )
43 simplrl 
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ ( # ` B ) ) /\ j e. ( 0 ..^ ( # ` B ) ) ) ) /\ j < i ) -> i e. ( 0 ..^ ( # ` B ) ) )
44 simplrr 
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ ( # ` B ) ) /\ j e. ( 0 ..^ ( # ` B ) ) ) ) /\ j < i ) -> j e. ( 0 ..^ ( # ` B ) ) )
45 elfzonn0 
 |-  ( j e. ( 0 ..^ ( # ` B ) ) -> j e. NN0 )
46 44 45 syl 
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ ( # ` B ) ) /\ j e. ( 0 ..^ ( # ` B ) ) ) ) /\ j < i ) -> j e. NN0 )
47 elfzoelz 
 |-  ( i e. ( 0 ..^ ( # ` B ) ) -> i e. ZZ )
48 43 47 syl 
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ ( # ` B ) ) /\ j e. ( 0 ..^ ( # ` B ) ) ) ) /\ j < i ) -> i e. ZZ )
49 simpr 
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ ( # ` B ) ) /\ j e. ( 0 ..^ ( # ` B ) ) ) ) /\ j < i ) -> j < i )
50 46 48 49 3jca 
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ ( # ` B ) ) /\ j e. ( 0 ..^ ( # ` B ) ) ) ) /\ j < i ) -> ( j e. NN0 /\ i e. ZZ /\ j < i ) )
51 elfzo0z 
 |-  ( j e. ( 0 ..^ i ) <-> ( j e. NN0 /\ i e. ZZ /\ j < i ) )
52 50 51 sylibr 
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ ( # ` B ) ) /\ j e. ( 0 ..^ ( # ` B ) ) ) ) /\ j < i ) -> j e. ( 0 ..^ i ) )
53 39 42 43 52 chnlt 
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ ( # ` B ) ) /\ j e. ( 0 ..^ ( # ` B ) ) ) ) /\ j < i ) -> ( B ` j ) .< ( B ` i ) )
54 po2ne 
 |-  ( ( .< Po A /\ ( ( B ` j ) e. A /\ ( B ` i ) e. A ) /\ ( B ` j ) .< ( B ` i ) ) -> ( B ` j ) =/= ( B ` i ) )
55 54 necomd 
 |-  ( ( .< Po A /\ ( ( B ` j ) e. A /\ ( B ` i ) e. A ) /\ ( B ` j ) .< ( B ` i ) ) -> ( B ` i ) =/= ( B ` j ) )
56 39 41 53 55 syl3anc 
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ ( # ` B ) ) /\ j e. ( 0 ..^ ( # ` B ) ) ) ) /\ j < i ) -> ( B ` i ) =/= ( B ` j ) )
57 56 neneqd 
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ ( # ` B ) ) /\ j e. ( 0 ..^ ( # ` B ) ) ) ) /\ j < i ) -> -. ( B ` i ) = ( B ` j ) )
58 57 ex 
 |-  ( ( ph /\ ( i e. ( 0 ..^ ( # ` B ) ) /\ j e. ( 0 ..^ ( # ` B ) ) ) ) -> ( j < i -> -. ( B ` i ) = ( B ` j ) ) )
59 58 con2d 
 |-  ( ( ph /\ ( i e. ( 0 ..^ ( # ` B ) ) /\ j e. ( 0 ..^ ( # ` B ) ) ) ) -> ( ( B ` i ) = ( B ` j ) -> -. j < i ) )
60 59 imp 
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ ( # ` B ) ) /\ j e. ( 0 ..^ ( # ` B ) ) ) ) /\ ( B ` i ) = ( B ` j ) ) -> -. j < i )
61 47 zred 
 |-  ( i e. ( 0 ..^ ( # ` B ) ) -> i e. RR )
62 26 zred 
 |-  ( j e. ( 0 ..^ ( # ` B ) ) -> j e. RR )
63 61 62 anim12i 
 |-  ( ( i e. ( 0 ..^ ( # ` B ) ) /\ j e. ( 0 ..^ ( # ` B ) ) ) -> ( i e. RR /\ j e. RR ) )
64 63 adantl 
 |-  ( ( ph /\ ( i e. ( 0 ..^ ( # ` B ) ) /\ j e. ( 0 ..^ ( # ` B ) ) ) ) -> ( i e. RR /\ j e. RR ) )
65 64 adantr 
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ ( # ` B ) ) /\ j e. ( 0 ..^ ( # ` B ) ) ) ) /\ ( B ` i ) = ( B ` j ) ) -> ( i e. RR /\ j e. RR ) )
66 lttri4 
 |-  ( ( i e. RR /\ j e. RR ) -> ( i < j \/ i = j \/ j < i ) )
67 65 66 syl 
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ ( # ` B ) ) /\ j e. ( 0 ..^ ( # ` B ) ) ) ) /\ ( B ` i ) = ( B ` j ) ) -> ( i < j \/ i = j \/ j < i ) )
68 3orcoma 
 |-  ( ( i < j \/ i = j \/ j < i ) <-> ( i = j \/ i < j \/ j < i ) )
69 67 68 sylib 
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ ( # ` B ) ) /\ j e. ( 0 ..^ ( # ` B ) ) ) ) /\ ( B ` i ) = ( B ` j ) ) -> ( i = j \/ i < j \/ j < i ) )
70 38 60 69 ecase23d 
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ ( # ` B ) ) /\ j e. ( 0 ..^ ( # ` B ) ) ) ) /\ ( B ` i ) = ( B ` j ) ) -> i = j )
71 70 ex 
 |-  ( ( ph /\ ( i e. ( 0 ..^ ( # ` B ) ) /\ j e. ( 0 ..^ ( # ` B ) ) ) ) -> ( ( B ` i ) = ( B ` j ) -> i = j ) )
72 71 ralrimivva 
 |-  ( ph -> A. i e. ( 0 ..^ ( # ` B ) ) A. j e. ( 0 ..^ ( # ` B ) ) ( ( B ` i ) = ( B ` j ) -> i = j ) )
73 4 72 jca 
 |-  ( ph -> ( B : ( 0 ..^ ( # ` B ) ) --> A /\ A. i e. ( 0 ..^ ( # ` B ) ) A. j e. ( 0 ..^ ( # ` B ) ) ( ( B ` i ) = ( B ` j ) -> i = j ) ) )
74 dff13 
 |-  ( B : ( 0 ..^ ( # ` B ) ) -1-1-> A <-> ( B : ( 0 ..^ ( # ` B ) ) --> A /\ A. i e. ( 0 ..^ ( # ` B ) ) A. j e. ( 0 ..^ ( # ` B ) ) ( ( B ` i ) = ( B ` j ) -> i = j ) ) )
75 73 74 sylibr 
 |-  ( ph -> B : ( 0 ..^ ( # ` B ) ) -1-1-> A )