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 𝐴 )
chnpof1.2 ⊢ ( 𝜑 → 𝐵 ∈ ( < Chain 𝐴 ) )
Assertion chnpof1 ( 𝜑 → 𝐵 : ( 0 ..^ ( ♯ ‘ 𝐵 ) ) –1-1→ 𝐴 )

Proof

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