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 ⊢ φ → < ˙ Po A
chnpof1.2 ⊢ φ → B ∈ Chain A < ˙
Assertion chnpof1 ⊢ φ → B : 0 ..^ B ⟶ 1-1 A

Proof

Step Hyp Ref Expression
1 chnpof1.1 ⊢ φ → < ˙ Po A
2 chnpof1.2 ⊢ φ → B ∈ Chain A < ˙
3 chnf ⊢ B ∈ Chain A < ˙ → B : 0 ..^ B ⟶ A
4 2 3 syl ⊢ φ → B : 0 ..^ B ⟶ A
5 1 adantr ⊢ φ ∧ i ∈ 0 ..^ B ∧ j ∈ 0 ..^ B → < ˙ Po A
6 5 adantr ⊢ φ ∧ i ∈ 0 ..^ B ∧ j ∈ 0 ..^ B ∧ i < j → < ˙ Po A
7 2 adantr ⊢ φ ∧ i ∈ 0 ..^ B → B ∈ Chain A < ˙
8 7 3 syl ⊢ φ ∧ i ∈ 0 ..^ B → B : 0 ..^ B ⟶ A
9 simpr ⊢ φ ∧ i ∈ 0 ..^ B → i ∈ 0 ..^ B
10 ffvelcdm ⊢ B : 0 ..^ B ⟶ A ∧ i ∈ 0 ..^ B → B ⁡ i ∈ A
11 8 9 10 syl2anc ⊢ φ ∧ i ∈ 0 ..^ B → B ⁡ i ∈ A
12 11 adantrr ⊢ φ ∧ i ∈ 0 ..^ B ∧ j ∈ 0 ..^ B → B ⁡ i ∈ A
13 4 adantr ⊢ φ ∧ i ∈ 0 ..^ B ∧ j ∈ 0 ..^ B → B : 0 ..^ B ⟶ A
14 simpr ⊢ i ∈ 0 ..^ B ∧ j ∈ 0 ..^ B → j ∈ 0 ..^ B
15 14 adantl ⊢ φ ∧ i ∈ 0 ..^ B ∧ j ∈ 0 ..^ B → j ∈ 0 ..^ B
16 ffvelcdm ⊢ B : 0 ..^ B ⟶ A ∧ j ∈ 0 ..^ B → B ⁡ j ∈ A
17 13 15 16 syl2anc ⊢ φ ∧ i ∈ 0 ..^ B ∧ j ∈ 0 ..^ B → B ⁡ j ∈ A
18 12 17 jca ⊢ φ ∧ i ∈ 0 ..^ B ∧ j ∈ 0 ..^ B → B ⁡ i ∈ A ∧ B ⁡ j ∈ A
19 18 adantr ⊢ φ ∧ i ∈ 0 ..^ B ∧ j ∈ 0 ..^ B ∧ i < j → B ⁡ i ∈ A ∧ B ⁡ j ∈ A
20 2 adantr ⊢ φ ∧ i ∈ 0 ..^ B ∧ j ∈ 0 ..^ B → B ∈ Chain A < ˙
21 20 adantr ⊢ φ ∧ i ∈ 0 ..^ B ∧ j ∈ 0 ..^ B ∧ i < j → B ∈ Chain A < ˙
22 15 adantr ⊢ φ ∧ i ∈ 0 ..^ B ∧ j ∈ 0 ..^ B ∧ i < j → j ∈ 0 ..^ B
23 simplrl ⊢ φ ∧ i ∈ 0 ..^ B ∧ j ∈ 0 ..^ B ∧ i < j → i ∈ 0 ..^ B
24 elfzonn0 ⊢ i ∈ 0 ..^ B → i ∈ ℕ 0
25 23 24 syl ⊢ φ ∧ i ∈ 0 ..^ B ∧ j ∈ 0 ..^ B ∧ i < j → i ∈ ℕ 0
26 elfzoelz ⊢ j ∈ 0 ..^ B → j ∈ ℤ
27 22 26 syl ⊢ φ ∧ i ∈ 0 ..^ B ∧ j ∈ 0 ..^ B ∧ i < j → j ∈ ℤ
28 simpr ⊢ φ ∧ i ∈ 0 ..^ B ∧ j ∈ 0 ..^ B ∧ i < j → i < j
29 25 27 28 3jca ⊢ φ ∧ i ∈ 0 ..^ B ∧ j ∈ 0 ..^ B ∧ i < j → i ∈ ℕ 0 ∧ j ∈ ℤ ∧ i < j
30 elfzo0z ⊢ i ∈ 0 ..^ j ↔ i ∈ ℕ 0 ∧ j ∈ ℤ ∧ i < j
31 29 30 sylibr ⊢ φ ∧ i ∈ 0 ..^ B ∧ j ∈ 0 ..^ B ∧ i < j → i ∈ 0 ..^ j
32 6 21 22 31 chnlt ⊢ φ ∧ i ∈ 0 ..^ B ∧ j ∈ 0 ..^ B ∧ i < j → B ⁡ i < ˙ B ⁡ j
33 po2ne ⊢ < ˙ Po A ∧ B ⁡ i ∈ A ∧ B ⁡ j ∈ A ∧ B ⁡ i < ˙ B ⁡ j → B ⁡ i ≠ B ⁡ j
34 6 19 32 33 syl3anc ⊢ φ ∧ i ∈ 0 ..^ B ∧ j ∈ 0 ..^ B ∧ i < j → B ⁡ i ≠ B ⁡ j
35 34 neneqd ⊢ φ ∧ i ∈ 0 ..^ B ∧ j ∈ 0 ..^ B ∧ i < j → ¬ B ⁡ i = B ⁡ j
36 35 ex ⊢ φ ∧ i ∈ 0 ..^ B ∧ j ∈ 0 ..^ B → i < j → ¬ B ⁡ i = B ⁡ j
37 36 con2d ⊢ φ ∧ i ∈ 0 ..^ B ∧ j ∈ 0 ..^ B → B ⁡ i = B ⁡ j → ¬ i < j
38 37 imp ⊢ φ ∧ i ∈ 0 ..^ B ∧ j ∈ 0 ..^ B ∧ B ⁡ i = B ⁡ j → ¬ i < j
39 5 adantr ⊢ φ ∧ i ∈ 0 ..^ B ∧ j ∈ 0 ..^ B ∧ j < i → < ˙ Po A
40 17 12 jca ⊢ φ ∧ i ∈ 0 ..^ B ∧ j ∈ 0 ..^ B → B ⁡ j ∈ A ∧ B ⁡ i ∈ A
41 40 adantr ⊢ φ ∧ i ∈ 0 ..^ B ∧ j ∈ 0 ..^ B ∧ j < i → B ⁡ j ∈ A ∧ B ⁡ i ∈ A
42 20 adantr ⊢ φ ∧ i ∈ 0 ..^ B ∧ j ∈ 0 ..^ B ∧ j < i → B ∈ Chain A < ˙
43 simplrl ⊢ φ ∧ i ∈ 0 ..^ B ∧ j ∈ 0 ..^ B ∧ j < i → i ∈ 0 ..^ B
44 simplrr ⊢ φ ∧ i ∈ 0 ..^ B ∧ j ∈ 0 ..^ B ∧ j < i → j ∈ 0 ..^ B
45 elfzonn0 ⊢ j ∈ 0 ..^ B → j ∈ ℕ 0
46 44 45 syl ⊢ φ ∧ i ∈ 0 ..^ B ∧ j ∈ 0 ..^ B ∧ j < i → j ∈ ℕ 0
47 elfzoelz ⊢ i ∈ 0 ..^ B → i ∈ ℤ
48 43 47 syl ⊢ φ ∧ i ∈ 0 ..^ B ∧ j ∈ 0 ..^ B ∧ j < i → i ∈ ℤ
49 simpr ⊢ φ ∧ i ∈ 0 ..^ B ∧ j ∈ 0 ..^ B ∧ j < i → j < i
50 46 48 49 3jca ⊢ φ ∧ i ∈ 0 ..^ B ∧ j ∈ 0 ..^ B ∧ j < i → j ∈ ℕ 0 ∧ i ∈ ℤ ∧ j < i
51 elfzo0z ⊢ j ∈ 0 ..^ i ↔ j ∈ ℕ 0 ∧ i ∈ ℤ ∧ j < i
52 50 51 sylibr ⊢ φ ∧ i ∈ 0 ..^ B ∧ j ∈ 0 ..^ B ∧ j < i → j ∈ 0 ..^ i
53 39 42 43 52 chnlt ⊢ φ ∧ i ∈ 0 ..^ B ∧ j ∈ 0 ..^ B ∧ j < i → B ⁡ j < ˙ B ⁡ i
54 po2ne ⊢ < ˙ Po A ∧ B ⁡ j ∈ A ∧ B ⁡ i ∈ A ∧ B ⁡ j < ˙ B ⁡ i → B ⁡ j ≠ B ⁡ i
55 54 necomd ⊢ < ˙ Po A ∧ B ⁡ j ∈ A ∧ B ⁡ i ∈ A ∧ B ⁡ j < ˙ B ⁡ i → B ⁡ i ≠ B ⁡ j
56 39 41 53 55 syl3anc ⊢ φ ∧ i ∈ 0 ..^ B ∧ j ∈ 0 ..^ B ∧ j < i → B ⁡ i ≠ B ⁡ j
57 56 neneqd ⊢ φ ∧ i ∈ 0 ..^ B ∧ j ∈ 0 ..^ B ∧ j < i → ¬ B ⁡ i = B ⁡ j
58 57 ex ⊢ φ ∧ i ∈ 0 ..^ B ∧ j ∈ 0 ..^ B → j < i → ¬ B ⁡ i = B ⁡ j
59 58 con2d ⊢ φ ∧ i ∈ 0 ..^ B ∧ j ∈ 0 ..^ B → B ⁡ i = B ⁡ j → ¬ j < i
60 59 imp ⊢ φ ∧ i ∈ 0 ..^ B ∧ j ∈ 0 ..^ B ∧ B ⁡ i = B ⁡ j → ¬ j < i
61 47 zred ⊢ i ∈ 0 ..^ B → i ∈ ℝ
62 26 zred ⊢ j ∈ 0 ..^ B → j ∈ ℝ
63 61 62 anim12i ⊢ i ∈ 0 ..^ B ∧ j ∈ 0 ..^ B → i ∈ ℝ ∧ j ∈ ℝ
64 63 adantl ⊢ φ ∧ i ∈ 0 ..^ B ∧ j ∈ 0 ..^ B → i ∈ ℝ ∧ j ∈ ℝ
65 64 adantr ⊢ φ ∧ i ∈ 0 ..^ B ∧ j ∈ 0 ..^ B ∧ B ⁡ i = B ⁡ j → i ∈ ℝ ∧ j ∈ ℝ
66 lttri4 ⊢ i ∈ ℝ ∧ j ∈ ℝ → i < j ∨ i = j ∨ j < i
67 65 66 syl ⊢ φ ∧ i ∈ 0 ..^ B ∧ j ∈ 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 ⊢ φ ∧ i ∈ 0 ..^ B ∧ j ∈ 0 ..^ B ∧ B ⁡ i = B ⁡ j → i = j ∨ i < j ∨ j < i
70 38 60 69 ecase23d ⊢ φ ∧ i ∈ 0 ..^ B ∧ j ∈ 0 ..^ B ∧ B ⁡ i = B ⁡ j → i = j
71 70 ex ⊢ φ ∧ i ∈ 0 ..^ B ∧ j ∈ 0 ..^ B → B ⁡ i = B ⁡ j → i = j
72 71 ralrimivva ⊢ φ → ∀ i ∈ 0 ..^ B ∀ j ∈ 0 ..^ B B ⁡ i = B ⁡ j → i = j
73 4 72 jca ⊢ φ → B : 0 ..^ B ⟶ A ∧ ∀ i ∈ 0 ..^ B ∀ j ∈ 0 ..^ B B ⁡ i = B ⁡ j → i = j
74 dff13 ⊢ B : 0 ..^ B ⟶ 1-1 A ↔ B : 0 ..^ B ⟶ A ∧ ∀ i ∈ 0 ..^ B ∀ j ∈ 0 ..^ B B ⁡ i = B ⁡ j → i = j
75 73 74 sylibr ⊢ φ → B : 0 ..^ B ⟶ 1-1 A