Metamath Proof Explorer

Theorem sticksstones2

Description: The range function on strictly monotone functions with finite domain and codomain is an injective mapping onto K -elemental sets. (Contributed by metakunt, 27-Sep-2024)

Ref Expression
Hypotheses sticksstones2.1 ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
sticksstones2.2 ⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
sticksstones2.3 ⊢ 𝐵 = { 𝑎 ∈ 𝒫 ( 1 ... 𝑁 ) ∣ ( ♯ ‘ 𝑎 ) = 𝐾 }
sticksstones2.4 ⊢ 𝐴 = { 𝑓 ∣ ( 𝑓 : ( 1 ... 𝐾 ) ⟶ ( 1 ... 𝑁 ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ) ) }
sticksstones2.5 ⊢ 𝐹 = ( 𝑧 ∈ 𝐴 ↦ ran 𝑧 )
Assertion sticksstones2 ( 𝜑 → 𝐹 : 𝐴 –1-1→ 𝐵 )

Proof

Step Hyp Ref Expression
1 sticksstones2.1 ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
2 sticksstones2.2 ⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
3 sticksstones2.3 ⊢ 𝐵 = { 𝑎 ∈ 𝒫 ( 1 ... 𝑁 ) ∣ ( ♯ ‘ 𝑎 ) = 𝐾 }
4 sticksstones2.4 ⊢ 𝐴 = { 𝑓 ∣ ( 𝑓 : ( 1 ... 𝐾 ) ⟶ ( 1 ... 𝑁 ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ) ) }
5 sticksstones2.5 ⊢ 𝐹 = ( 𝑧 ∈ 𝐴 ↦ ran 𝑧 )
6 fveqeq2 ⊢ ( 𝑎 = ran 𝑧 → ( ( ♯ ‘ 𝑎 ) = 𝐾 ↔ ( ♯ ‘ ran 𝑧 ) = 𝐾 ) )
7 fzfid ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ( 1 ... 𝑁 ) ∈ Fin )
8 eleq1w ⊢ ( 𝑓 = 𝑧 → ( 𝑓 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴 ) )
9 feq1 ⊢ ( 𝑓 = 𝑧 → ( 𝑓 : ( 1 ... 𝐾 ) ⟶ ( 1 ... 𝑁 ) ↔ 𝑧 : ( 1 ... 𝐾 ) ⟶ ( 1 ... 𝑁 ) ) )
10 fveq1 ⊢ ( 𝑓 = 𝑧 → ( 𝑓 ‘ 𝑥 ) = ( 𝑧 ‘ 𝑥 ) )
11 fveq1 ⊢ ( 𝑓 = 𝑧 → ( 𝑓 ‘ 𝑦 ) = ( 𝑧 ‘ 𝑦 ) )
12 10 11 breq12d ⊢ ( 𝑓 = 𝑧 → ( ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ↔ ( 𝑧 ‘ 𝑥 ) < ( 𝑧 ‘ 𝑦 ) ) )
13 12 imbi2d ⊢ ( 𝑓 = 𝑧 → ( ( 𝑥 < 𝑦 → ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ) ↔ ( 𝑥 < 𝑦 → ( 𝑧 ‘ 𝑥 ) < ( 𝑧 ‘ 𝑦 ) ) ) )
14 13 ralbidv ⊢ ( 𝑓 = 𝑧 → ( ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ) ↔ ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑧 ‘ 𝑥 ) < ( 𝑧 ‘ 𝑦 ) ) ) )
15 14 ralbidv ⊢ ( 𝑓 = 𝑧 → ( ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ) ↔ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑧 ‘ 𝑥 ) < ( 𝑧 ‘ 𝑦 ) ) ) )
16 9 15 anbi12d ⊢ ( 𝑓 = 𝑧 → ( ( 𝑓 : ( 1 ... 𝐾 ) ⟶ ( 1 ... 𝑁 ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ) ) ↔ ( 𝑧 : ( 1 ... 𝐾 ) ⟶ ( 1 ... 𝑁 ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑧 ‘ 𝑥 ) < ( 𝑧 ‘ 𝑦 ) ) ) ) )
17 8 16 bibi12d ⊢ ( 𝑓 = 𝑧 → ( ( 𝑓 ∈ 𝐴 ↔ ( 𝑓 : ( 1 ... 𝐾 ) ⟶ ( 1 ... 𝑁 ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ) ) ) ↔ ( 𝑧 ∈ 𝐴 ↔ ( 𝑧 : ( 1 ... 𝐾 ) ⟶ ( 1 ... 𝑁 ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑧 ‘ 𝑥 ) < ( 𝑧 ‘ 𝑦 ) ) ) ) ) )
18 eqabb ⊢ ( 𝐴 = { 𝑓 ∣ ( 𝑓 : ( 1 ... 𝐾 ) ⟶ ( 1 ... 𝑁 ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ) ) } ↔ ∀ 𝑓 ( 𝑓 ∈ 𝐴 ↔ ( 𝑓 : ( 1 ... 𝐾 ) ⟶ ( 1 ... 𝑁 ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ) ) ) )
19 4 18 mpbi ⊢ ∀ 𝑓 ( 𝑓 ∈ 𝐴 ↔ ( 𝑓 : ( 1 ... 𝐾 ) ⟶ ( 1 ... 𝑁 ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ) ) )
20 19 spi ⊢ ( 𝑓 ∈ 𝐴 ↔ ( 𝑓 : ( 1 ... 𝐾 ) ⟶ ( 1 ... 𝑁 ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ) ) )
21 17 20 chvarvv ⊢ ( 𝑧 ∈ 𝐴 ↔ ( 𝑧 : ( 1 ... 𝐾 ) ⟶ ( 1 ... 𝑁 ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑧 ‘ 𝑥 ) < ( 𝑧 ‘ 𝑦 ) ) ) )
22 21 biimpi ⊢ ( 𝑧 ∈ 𝐴 → ( 𝑧 : ( 1 ... 𝐾 ) ⟶ ( 1 ... 𝑁 ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑧 ‘ 𝑥 ) < ( 𝑧 ‘ 𝑦 ) ) ) )
23 22 adantl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ( 𝑧 : ( 1 ... 𝐾 ) ⟶ ( 1 ... 𝑁 ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑧 ‘ 𝑥 ) < ( 𝑧 ‘ 𝑦 ) ) ) )
24 23 simpld ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → 𝑧 : ( 1 ... 𝐾 ) ⟶ ( 1 ... 𝑁 ) )
25 24 frnd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ran 𝑧 ⊆ ( 1 ... 𝑁 ) )
26 7 25 sselpwd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ran 𝑧 ∈ 𝒫 ( 1 ... 𝑁 ) )
27 24 ffnd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → 𝑧 Fn ( 1 ... 𝐾 ) )
28 hashfn ⊢ ( 𝑧 Fn ( 1 ... 𝐾 ) → ( ♯ ‘ 𝑧 ) = ( ♯ ‘ ( 1 ... 𝐾 ) ) )
29 27 28 syl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ( ♯ ‘ 𝑧 ) = ( ♯ ‘ ( 1 ... 𝐾 ) ) )
30 2 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → 𝐾 ∈ ℕ0 )
31 hashfz1 ⊢ ( 𝐾 ∈ ℕ0 → ( ♯ ‘ ( 1 ... 𝐾 ) ) = 𝐾 )
32 30 31 syl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ( ♯ ‘ ( 1 ... 𝐾 ) ) = 𝐾 )
33 29 32 eqtrd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ( ♯ ‘ 𝑧 ) = 𝐾 )
34 33 eqcomd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → 𝐾 = ( ♯ ‘ 𝑧 ) )
35 fzfid ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ( 1 ... 𝐾 ) ∈ Fin )
36 elfznn ⊢ ( 𝑎 ∈ ( 1 ... 𝐾 ) → 𝑎 ∈ ℕ )
37 36 3ad2ant3 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ ( 1 ... 𝐾 ) ) → 𝑎 ∈ ℕ )
38 37 nnred ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ ( 1 ... 𝐾 ) ) → 𝑎 ∈ ℝ )
39 38 adantr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑏 ∈ ( 1 ... 𝐾 ) ) → 𝑎 ∈ ℝ )
40 elfznn ⊢ ( 𝑏 ∈ ( 1 ... 𝐾 ) → 𝑏 ∈ ℕ )
41 40 nnred ⊢ ( 𝑏 ∈ ( 1 ... 𝐾 ) → 𝑏 ∈ ℝ )
42 41 adantl ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑏 ∈ ( 1 ... 𝐾 ) ) → 𝑏 ∈ ℝ )
43 lttri2 ⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) → ( 𝑎 ≠ 𝑏 ↔ ( 𝑎 < 𝑏 ∨ 𝑏 < 𝑎 ) ) )
44 39 42 43 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑏 ∈ ( 1 ... 𝐾 ) ) → ( 𝑎 ≠ 𝑏 ↔ ( 𝑎 < 𝑏 ∨ 𝑏 < 𝑎 ) ) )
45 24 3adant3 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ ( 1 ... 𝐾 ) ) → 𝑧 : ( 1 ... 𝐾 ) ⟶ ( 1 ... 𝑁 ) )
46 simp3 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ ( 1 ... 𝐾 ) ) → 𝑎 ∈ ( 1 ... 𝐾 ) )
47 45 46 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ ( 1 ... 𝐾 ) ) → ( 𝑧 ‘ 𝑎 ) ∈ ( 1 ... 𝑁 ) )
48 47 adantr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑏 ∈ ( 1 ... 𝐾 ) ) → ( 𝑧 ‘ 𝑎 ) ∈ ( 1 ... 𝑁 ) )
49 48 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑏 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑎 < 𝑏 ) → ( 𝑧 ‘ 𝑎 ) ∈ ( 1 ... 𝑁 ) )
50 elfznn ⊢ ( ( 𝑧 ‘ 𝑎 ) ∈ ( 1 ... 𝑁 ) → ( 𝑧 ‘ 𝑎 ) ∈ ℕ )
51 49 50 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑏 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑎 < 𝑏 ) → ( 𝑧 ‘ 𝑎 ) ∈ ℕ )
52 51 nnred ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑏 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑎 < 𝑏 ) → ( 𝑧 ‘ 𝑎 ) ∈ ℝ )
53 23 simprd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑧 ‘ 𝑥 ) < ( 𝑧 ‘ 𝑦 ) ) )
54 53 3adant3 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ ( 1 ... 𝐾 ) ) → ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑧 ‘ 𝑥 ) < ( 𝑧 ‘ 𝑦 ) ) )
55 54 adantr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑏 ∈ ( 1 ... 𝐾 ) ) → ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑧 ‘ 𝑥 ) < ( 𝑧 ‘ 𝑦 ) ) )
56 46 adantr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑏 ∈ ( 1 ... 𝐾 ) ) → 𝑎 ∈ ( 1 ... 𝐾 ) )
57 simpr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑏 ∈ ( 1 ... 𝐾 ) ) → 𝑏 ∈ ( 1 ... 𝐾 ) )
58 breq1 ⊢ ( 𝑥 = 𝑎 → ( 𝑥 < 𝑦 ↔ 𝑎 < 𝑦 ) )
59 fveq2 ⊢ ( 𝑥 = 𝑎 → ( 𝑧 ‘ 𝑥 ) = ( 𝑧 ‘ 𝑎 ) )
60 59 breq1d ⊢ ( 𝑥 = 𝑎 → ( ( 𝑧 ‘ 𝑥 ) < ( 𝑧 ‘ 𝑦 ) ↔ ( 𝑧 ‘ 𝑎 ) < ( 𝑧 ‘ 𝑦 ) ) )
61 58 60 imbi12d ⊢ ( 𝑥 = 𝑎 → ( ( 𝑥 < 𝑦 → ( 𝑧 ‘ 𝑥 ) < ( 𝑧 ‘ 𝑦 ) ) ↔ ( 𝑎 < 𝑦 → ( 𝑧 ‘ 𝑎 ) < ( 𝑧 ‘ 𝑦 ) ) ) )
62 breq2 ⊢ ( 𝑦 = 𝑏 → ( 𝑎 < 𝑦 ↔ 𝑎 < 𝑏 ) )
63 fveq2 ⊢ ( 𝑦 = 𝑏 → ( 𝑧 ‘ 𝑦 ) = ( 𝑧 ‘ 𝑏 ) )
64 63 breq2d ⊢ ( 𝑦 = 𝑏 → ( ( 𝑧 ‘ 𝑎 ) < ( 𝑧 ‘ 𝑦 ) ↔ ( 𝑧 ‘ 𝑎 ) < ( 𝑧 ‘ 𝑏 ) ) )
65 62 64 imbi12d ⊢ ( 𝑦 = 𝑏 → ( ( 𝑎 < 𝑦 → ( 𝑧 ‘ 𝑎 ) < ( 𝑧 ‘ 𝑦 ) ) ↔ ( 𝑎 < 𝑏 → ( 𝑧 ‘ 𝑎 ) < ( 𝑧 ‘ 𝑏 ) ) ) )
66 61 65 rspc2v ⊢ ( ( 𝑎 ∈ ( 1 ... 𝐾 ) ∧ 𝑏 ∈ ( 1 ... 𝐾 ) ) → ( ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑧 ‘ 𝑥 ) < ( 𝑧 ‘ 𝑦 ) ) → ( 𝑎 < 𝑏 → ( 𝑧 ‘ 𝑎 ) < ( 𝑧 ‘ 𝑏 ) ) ) )
67 56 57 66 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑏 ∈ ( 1 ... 𝐾 ) ) → ( ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑧 ‘ 𝑥 ) < ( 𝑧 ‘ 𝑦 ) ) → ( 𝑎 < 𝑏 → ( 𝑧 ‘ 𝑎 ) < ( 𝑧 ‘ 𝑏 ) ) ) )
68 55 67 mpd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑏 ∈ ( 1 ... 𝐾 ) ) → ( 𝑎 < 𝑏 → ( 𝑧 ‘ 𝑎 ) < ( 𝑧 ‘ 𝑏 ) ) )
69 68 imp ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑏 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑎 < 𝑏 ) → ( 𝑧 ‘ 𝑎 ) < ( 𝑧 ‘ 𝑏 ) )
70 52 69 ltned ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑏 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑎 < 𝑏 ) → ( 𝑧 ‘ 𝑎 ) ≠ ( 𝑧 ‘ 𝑏 ) )
71 45 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑏 ∈ ( 1 ... 𝐾 ) ) → ( 𝑧 ‘ 𝑏 ) ∈ ( 1 ... 𝑁 ) )
72 elfznn ⊢ ( ( 𝑧 ‘ 𝑏 ) ∈ ( 1 ... 𝑁 ) → ( 𝑧 ‘ 𝑏 ) ∈ ℕ )
73 71 72 syl ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑏 ∈ ( 1 ... 𝐾 ) ) → ( 𝑧 ‘ 𝑏 ) ∈ ℕ )
74 73 nnred ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑏 ∈ ( 1 ... 𝐾 ) ) → ( 𝑧 ‘ 𝑏 ) ∈ ℝ )
75 74 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑏 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑏 < 𝑎 ) → ( 𝑧 ‘ 𝑏 ) ∈ ℝ )
76 breq1 ⊢ ( 𝑥 = 𝑏 → ( 𝑥 < 𝑦 ↔ 𝑏 < 𝑦 ) )
77 fveq2 ⊢ ( 𝑥 = 𝑏 → ( 𝑧 ‘ 𝑥 ) = ( 𝑧 ‘ 𝑏 ) )
78 77 breq1d ⊢ ( 𝑥 = 𝑏 → ( ( 𝑧 ‘ 𝑥 ) < ( 𝑧 ‘ 𝑦 ) ↔ ( 𝑧 ‘ 𝑏 ) < ( 𝑧 ‘ 𝑦 ) ) )
79 76 78 imbi12d ⊢ ( 𝑥 = 𝑏 → ( ( 𝑥 < 𝑦 → ( 𝑧 ‘ 𝑥 ) < ( 𝑧 ‘ 𝑦 ) ) ↔ ( 𝑏 < 𝑦 → ( 𝑧 ‘ 𝑏 ) < ( 𝑧 ‘ 𝑦 ) ) ) )
80 breq2 ⊢ ( 𝑦 = 𝑎 → ( 𝑏 < 𝑦 ↔ 𝑏 < 𝑎 ) )
81 fveq2 ⊢ ( 𝑦 = 𝑎 → ( 𝑧 ‘ 𝑦 ) = ( 𝑧 ‘ 𝑎 ) )
82 81 breq2d ⊢ ( 𝑦 = 𝑎 → ( ( 𝑧 ‘ 𝑏 ) < ( 𝑧 ‘ 𝑦 ) ↔ ( 𝑧 ‘ 𝑏 ) < ( 𝑧 ‘ 𝑎 ) ) )
83 80 82 imbi12d ⊢ ( 𝑦 = 𝑎 → ( ( 𝑏 < 𝑦 → ( 𝑧 ‘ 𝑏 ) < ( 𝑧 ‘ 𝑦 ) ) ↔ ( 𝑏 < 𝑎 → ( 𝑧 ‘ 𝑏 ) < ( 𝑧 ‘ 𝑎 ) ) ) )
84 79 83 rspc2v ⊢ ( ( 𝑏 ∈ ( 1 ... 𝐾 ) ∧ 𝑎 ∈ ( 1 ... 𝐾 ) ) → ( ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑧 ‘ 𝑥 ) < ( 𝑧 ‘ 𝑦 ) ) → ( 𝑏 < 𝑎 → ( 𝑧 ‘ 𝑏 ) < ( 𝑧 ‘ 𝑎 ) ) ) )
85 57 56 84 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑏 ∈ ( 1 ... 𝐾 ) ) → ( ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑧 ‘ 𝑥 ) < ( 𝑧 ‘ 𝑦 ) ) → ( 𝑏 < 𝑎 → ( 𝑧 ‘ 𝑏 ) < ( 𝑧 ‘ 𝑎 ) ) ) )
86 55 85 mpd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑏 ∈ ( 1 ... 𝐾 ) ) → ( 𝑏 < 𝑎 → ( 𝑧 ‘ 𝑏 ) < ( 𝑧 ‘ 𝑎 ) ) )
87 86 imp ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑏 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑏 < 𝑎 ) → ( 𝑧 ‘ 𝑏 ) < ( 𝑧 ‘ 𝑎 ) )
88 75 87 ltned ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑏 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑏 < 𝑎 ) → ( 𝑧 ‘ 𝑏 ) ≠ ( 𝑧 ‘ 𝑎 ) )
89 88 necomd ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑏 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑏 < 𝑎 ) → ( 𝑧 ‘ 𝑎 ) ≠ ( 𝑧 ‘ 𝑏 ) )
90 70 89 jaodan ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑏 ∈ ( 1 ... 𝐾 ) ) ∧ ( 𝑎 < 𝑏 ∨ 𝑏 < 𝑎 ) ) → ( 𝑧 ‘ 𝑎 ) ≠ ( 𝑧 ‘ 𝑏 ) )
91 90 ex ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑏 ∈ ( 1 ... 𝐾 ) ) → ( ( 𝑎 < 𝑏 ∨ 𝑏 < 𝑎 ) → ( 𝑧 ‘ 𝑎 ) ≠ ( 𝑧 ‘ 𝑏 ) ) )
92 44 91 sylbid ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑏 ∈ ( 1 ... 𝐾 ) ) → ( 𝑎 ≠ 𝑏 → ( 𝑧 ‘ 𝑎 ) ≠ ( 𝑧 ‘ 𝑏 ) ) )
93 92 necon4d ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑏 ∈ ( 1 ... 𝐾 ) ) → ( ( 𝑧 ‘ 𝑎 ) = ( 𝑧 ‘ 𝑏 ) → 𝑎 = 𝑏 ) )
94 93 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ∧ 𝑎 ∈ ( 1 ... 𝐾 ) ) → ∀ 𝑏 ∈ ( 1 ... 𝐾 ) ( ( 𝑧 ‘ 𝑎 ) = ( 𝑧 ‘ 𝑏 ) → 𝑎 = 𝑏 ) )
95 94 3expa ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑎 ∈ ( 1 ... 𝐾 ) ) → ∀ 𝑏 ∈ ( 1 ... 𝐾 ) ( ( 𝑧 ‘ 𝑎 ) = ( 𝑧 ‘ 𝑏 ) → 𝑎 = 𝑏 ) )
96 95 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ∀ 𝑎 ∈ ( 1 ... 𝐾 ) ∀ 𝑏 ∈ ( 1 ... 𝐾 ) ( ( 𝑧 ‘ 𝑎 ) = ( 𝑧 ‘ 𝑏 ) → 𝑎 = 𝑏 ) )
97 24 96 jca ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ( 𝑧 : ( 1 ... 𝐾 ) ⟶ ( 1 ... 𝑁 ) ∧ ∀ 𝑎 ∈ ( 1 ... 𝐾 ) ∀ 𝑏 ∈ ( 1 ... 𝐾 ) ( ( 𝑧 ‘ 𝑎 ) = ( 𝑧 ‘ 𝑏 ) → 𝑎 = 𝑏 ) ) )
98 dff13 ⊢ ( 𝑧 : ( 1 ... 𝐾 ) –1-1→ ( 1 ... 𝑁 ) ↔ ( 𝑧 : ( 1 ... 𝐾 ) ⟶ ( 1 ... 𝑁 ) ∧ ∀ 𝑎 ∈ ( 1 ... 𝐾 ) ∀ 𝑏 ∈ ( 1 ... 𝐾 ) ( ( 𝑧 ‘ 𝑎 ) = ( 𝑧 ‘ 𝑏 ) → 𝑎 = 𝑏 ) ) )
99 97 98 sylibr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → 𝑧 : ( 1 ... 𝐾 ) –1-1→ ( 1 ... 𝑁 ) )
100 hashf1rn ⊢ ( ( ( 1 ... 𝐾 ) ∈ Fin ∧ 𝑧 : ( 1 ... 𝐾 ) –1-1→ ( 1 ... 𝑁 ) ) → ( ♯ ‘ 𝑧 ) = ( ♯ ‘ ran 𝑧 ) )
101 35 99 100 syl2anc ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ( ♯ ‘ 𝑧 ) = ( ♯ ‘ ran 𝑧 ) )
102 34 101 eqtrd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → 𝐾 = ( ♯ ‘ ran 𝑧 ) )
103 102 eqcomd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ( ♯ ‘ ran 𝑧 ) = 𝐾 )
104 6 26 103 elrabd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ran 𝑧 ∈ { 𝑎 ∈ 𝒫 ( 1 ... 𝑁 ) ∣ ( ♯ ‘ 𝑎 ) = 𝐾 } )
105 3 eleq2i ⊢ ( ran 𝑧 ∈ 𝐵 ↔ ran 𝑧 ∈ { 𝑎 ∈ 𝒫 ( 1 ... 𝑁 ) ∣ ( ♯ ‘ 𝑎 ) = 𝐾 } )
106 105 a1i ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ( ran 𝑧 ∈ 𝐵 ↔ ran 𝑧 ∈ { 𝑎 ∈ 𝒫 ( 1 ... 𝑁 ) ∣ ( ♯ ‘ 𝑎 ) = 𝐾 } ) )
107 104 106 mpbird ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ran 𝑧 ∈ 𝐵 )
108 107 5 fmptd ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
109 1 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐴 ) → 𝑁 ∈ ℕ0 )
110 109 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑖 ≠ 𝑗 ) → 𝑁 ∈ ℕ0 )
111 2 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐴 ) → 𝐾 ∈ ℕ0 )
112 111 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑖 ≠ 𝑗 ) → 𝐾 ∈ ℕ0 )
113 simpl2 ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑖 ≠ 𝑗 ) → 𝑖 ∈ 𝐴 )
114 simpl3 ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑖 ≠ 𝑗 ) → 𝑗 ∈ 𝐴 )
115 simpr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑖 ≠ 𝑗 ) → 𝑖 ≠ 𝑗 )
116 fveq2 ⊢ ( 𝑟 = 𝑠 → ( 𝑖 ‘ 𝑟 ) = ( 𝑖 ‘ 𝑠 ) )
117 fveq2 ⊢ ( 𝑟 = 𝑠 → ( 𝑗 ‘ 𝑟 ) = ( 𝑗 ‘ 𝑠 ) )
118 116 117 neeq12d ⊢ ( 𝑟 = 𝑠 → ( ( 𝑖 ‘ 𝑟 ) ≠ ( 𝑗 ‘ 𝑟 ) ↔ ( 𝑖 ‘ 𝑠 ) ≠ ( 𝑗 ‘ 𝑠 ) ) )
119 118 cbvrabv ⊢ { 𝑟 ∈ ( 1 ... 𝐾 ) ∣ ( 𝑖 ‘ 𝑟 ) ≠ ( 𝑗 ‘ 𝑟 ) } = { 𝑠 ∈ ( 1 ... 𝐾 ) ∣ ( 𝑖 ‘ 𝑠 ) ≠ ( 𝑗 ‘ 𝑠 ) }
120 119 infeq1i ⊢ inf ( { 𝑟 ∈ ( 1 ... 𝐾 ) ∣ ( 𝑖 ‘ 𝑟 ) ≠ ( 𝑗 ‘ 𝑟 ) } , ℝ , < ) = inf ( { 𝑠 ∈ ( 1 ... 𝐾 ) ∣ ( 𝑖 ‘ 𝑠 ) ≠ ( 𝑗 ‘ 𝑠 ) } , ℝ , < )
121 110 112 4 113 114 115 120 sticksstones1 ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑖 ≠ 𝑗 ) → ran 𝑖 ≠ ran 𝑗 )
122 5 a1i ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑖 ≠ 𝑗 ) → 𝐹 = ( 𝑧 ∈ 𝐴 ↦ ran 𝑧 ) )
123 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑖 ≠ 𝑗 ) ∧ 𝑧 = 𝑖 ) → 𝑧 = 𝑖 )
124 123 rneqd ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑖 ≠ 𝑗 ) ∧ 𝑧 = 𝑖 ) → ran 𝑧 = ran 𝑖 )
125 fzfid ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑖 ≠ 𝑗 ) → ( 1 ... 𝑁 ) ∈ Fin )
126 eleq1w ⊢ ( 𝑓 = 𝑖 → ( 𝑓 ∈ 𝐴 ↔ 𝑖 ∈ 𝐴 ) )
127 feq1 ⊢ ( 𝑓 = 𝑖 → ( 𝑓 : ( 1 ... 𝐾 ) ⟶ ( 1 ... 𝑁 ) ↔ 𝑖 : ( 1 ... 𝐾 ) ⟶ ( 1 ... 𝑁 ) ) )
128 fveq1 ⊢ ( 𝑓 = 𝑖 → ( 𝑓 ‘ 𝑥 ) = ( 𝑖 ‘ 𝑥 ) )
129 fveq1 ⊢ ( 𝑓 = 𝑖 → ( 𝑓 ‘ 𝑦 ) = ( 𝑖 ‘ 𝑦 ) )
130 128 129 breq12d ⊢ ( 𝑓 = 𝑖 → ( ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ↔ ( 𝑖 ‘ 𝑥 ) < ( 𝑖 ‘ 𝑦 ) ) )
131 130 imbi2d ⊢ ( 𝑓 = 𝑖 → ( ( 𝑥 < 𝑦 → ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ) ↔ ( 𝑥 < 𝑦 → ( 𝑖 ‘ 𝑥 ) < ( 𝑖 ‘ 𝑦 ) ) ) )
132 131 2ralbidv ⊢ ( 𝑓 = 𝑖 → ( ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ) ↔ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑖 ‘ 𝑥 ) < ( 𝑖 ‘ 𝑦 ) ) ) )
133 127 132 anbi12d ⊢ ( 𝑓 = 𝑖 → ( ( 𝑓 : ( 1 ... 𝐾 ) ⟶ ( 1 ... 𝑁 ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ) ) ↔ ( 𝑖 : ( 1 ... 𝐾 ) ⟶ ( 1 ... 𝑁 ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑖 ‘ 𝑥 ) < ( 𝑖 ‘ 𝑦 ) ) ) ) )
134 126 133 bibi12d ⊢ ( 𝑓 = 𝑖 → ( ( 𝑓 ∈ 𝐴 ↔ ( 𝑓 : ( 1 ... 𝐾 ) ⟶ ( 1 ... 𝑁 ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ) ) ) ↔ ( 𝑖 ∈ 𝐴 ↔ ( 𝑖 : ( 1 ... 𝐾 ) ⟶ ( 1 ... 𝑁 ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑖 ‘ 𝑥 ) < ( 𝑖 ‘ 𝑦 ) ) ) ) ) )
135 134 20 chvarvv ⊢ ( 𝑖 ∈ 𝐴 ↔ ( 𝑖 : ( 1 ... 𝐾 ) ⟶ ( 1 ... 𝑁 ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑖 ‘ 𝑥 ) < ( 𝑖 ‘ 𝑦 ) ) ) )
136 135 biimpi ⊢ ( 𝑖 ∈ 𝐴 → ( 𝑖 : ( 1 ... 𝐾 ) ⟶ ( 1 ... 𝑁 ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑖 ‘ 𝑥 ) < ( 𝑖 ‘ 𝑦 ) ) ) )
137 136 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) → ( 𝑖 : ( 1 ... 𝐾 ) ⟶ ( 1 ... 𝑁 ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑖 ‘ 𝑥 ) < ( 𝑖 ‘ 𝑦 ) ) ) )
138 137 simpld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) → 𝑖 : ( 1 ... 𝐾 ) ⟶ ( 1 ... 𝑁 ) )
139 138 3adant3 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐴 ) → 𝑖 : ( 1 ... 𝐾 ) ⟶ ( 1 ... 𝑁 ) )
140 139 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑖 ≠ 𝑗 ) → 𝑖 : ( 1 ... 𝐾 ) ⟶ ( 1 ... 𝑁 ) )
141 140 frnd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑖 ≠ 𝑗 ) → ran 𝑖 ⊆ ( 1 ... 𝑁 ) )
142 125 141 sselpwd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑖 ≠ 𝑗 ) → ran 𝑖 ∈ 𝒫 ( 1 ... 𝑁 ) )
143 122 124 113 142 fvmptd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑖 ≠ 𝑗 ) → ( 𝐹 ‘ 𝑖 ) = ran 𝑖 )
144 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑖 ≠ 𝑗 ) ∧ 𝑧 = 𝑗 ) → 𝑧 = 𝑗 )
145 144 rneqd ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑖 ≠ 𝑗 ) ∧ 𝑧 = 𝑗 ) → ran 𝑧 = ran 𝑗 )
146 fzfid ⊢ ( 𝜑 → ( 1 ... 𝑁 ) ∈ Fin )
147 146 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐴 ) → ( 1 ... 𝑁 ) ∈ Fin )
148 eleq1w ⊢ ( 𝑓 = 𝑗 → ( 𝑓 ∈ 𝐴 ↔ 𝑗 ∈ 𝐴 ) )
149 feq1 ⊢ ( 𝑓 = 𝑗 → ( 𝑓 : ( 1 ... 𝐾 ) ⟶ ( 1 ... 𝑁 ) ↔ 𝑗 : ( 1 ... 𝐾 ) ⟶ ( 1 ... 𝑁 ) ) )
150 fveq1 ⊢ ( 𝑓 = 𝑗 → ( 𝑓 ‘ 𝑥 ) = ( 𝑗 ‘ 𝑥 ) )
151 fveq1 ⊢ ( 𝑓 = 𝑗 → ( 𝑓 ‘ 𝑦 ) = ( 𝑗 ‘ 𝑦 ) )
152 150 151 breq12d ⊢ ( 𝑓 = 𝑗 → ( ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ↔ ( 𝑗 ‘ 𝑥 ) < ( 𝑗 ‘ 𝑦 ) ) )
153 152 imbi2d ⊢ ( 𝑓 = 𝑗 → ( ( 𝑥 < 𝑦 → ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ) ↔ ( 𝑥 < 𝑦 → ( 𝑗 ‘ 𝑥 ) < ( 𝑗 ‘ 𝑦 ) ) ) )
154 153 2ralbidv ⊢ ( 𝑓 = 𝑗 → ( ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ) ↔ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑗 ‘ 𝑥 ) < ( 𝑗 ‘ 𝑦 ) ) ) )
155 149 154 anbi12d ⊢ ( 𝑓 = 𝑗 → ( ( 𝑓 : ( 1 ... 𝐾 ) ⟶ ( 1 ... 𝑁 ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ) ) ↔ ( 𝑗 : ( 1 ... 𝐾 ) ⟶ ( 1 ... 𝑁 ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑗 ‘ 𝑥 ) < ( 𝑗 ‘ 𝑦 ) ) ) ) )
156 148 155 bibi12d ⊢ ( 𝑓 = 𝑗 → ( ( 𝑓 ∈ 𝐴 ↔ ( 𝑓 : ( 1 ... 𝐾 ) ⟶ ( 1 ... 𝑁 ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ) ) ) ↔ ( 𝑗 ∈ 𝐴 ↔ ( 𝑗 : ( 1 ... 𝐾 ) ⟶ ( 1 ... 𝑁 ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑗 ‘ 𝑥 ) < ( 𝑗 ‘ 𝑦 ) ) ) ) ) )
157 156 20 chvarvv ⊢ ( 𝑗 ∈ 𝐴 ↔ ( 𝑗 : ( 1 ... 𝐾 ) ⟶ ( 1 ... 𝑁 ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑗 ‘ 𝑥 ) < ( 𝑗 ‘ 𝑦 ) ) ) )
158 157 biimpi ⊢ ( 𝑗 ∈ 𝐴 → ( 𝑗 : ( 1 ... 𝐾 ) ⟶ ( 1 ... 𝑁 ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑗 ‘ 𝑥 ) < ( 𝑗 ‘ 𝑦 ) ) ) )
159 158 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ( 𝑗 : ( 1 ... 𝐾 ) ⟶ ( 1 ... 𝑁 ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑗 ‘ 𝑥 ) < ( 𝑗 ‘ 𝑦 ) ) ) )
160 159 simpld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 𝑗 : ( 1 ... 𝐾 ) ⟶ ( 1 ... 𝑁 ) )
161 160 3adant2 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐴 ) → 𝑗 : ( 1 ... 𝐾 ) ⟶ ( 1 ... 𝑁 ) )
162 161 frnd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐴 ) → ran 𝑗 ⊆ ( 1 ... 𝑁 ) )
163 147 162 sselpwd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐴 ) → ran 𝑗 ∈ 𝒫 ( 1 ... 𝑁 ) )
164 163 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑖 ≠ 𝑗 ) → ran 𝑗 ∈ 𝒫 ( 1 ... 𝑁 ) )
165 122 145 114 164 fvmptd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑖 ≠ 𝑗 ) → ( 𝐹 ‘ 𝑗 ) = ran 𝑗 )
166 121 143 165 3netr4d ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑖 ≠ 𝑗 ) → ( 𝐹 ‘ 𝑖 ) ≠ ( 𝐹 ‘ 𝑗 ) )
167 166 ex ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐴 ) → ( 𝑖 ≠ 𝑗 → ( 𝐹 ‘ 𝑖 ) ≠ ( 𝐹 ‘ 𝑗 ) ) )
168 167 necon4d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑖 ) = ( 𝐹 ‘ 𝑗 ) → 𝑖 = 𝑗 ) )
169 168 3expa ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) ∧ 𝑗 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑖 ) = ( 𝐹 ‘ 𝑗 ) → 𝑖 = 𝑗 ) )
170 169 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) → ∀ 𝑗 ∈ 𝐴 ( ( 𝐹 ‘ 𝑖 ) = ( 𝐹 ‘ 𝑗 ) → 𝑖 = 𝑗 ) )
171 170 ralrimiva ⊢ ( 𝜑 → ∀ 𝑖 ∈ 𝐴 ∀ 𝑗 ∈ 𝐴 ( ( 𝐹 ‘ 𝑖 ) = ( 𝐹 ‘ 𝑗 ) → 𝑖 = 𝑗 ) )
172 108 171 jca ⊢ ( 𝜑 → ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑖 ∈ 𝐴 ∀ 𝑗 ∈ 𝐴 ( ( 𝐹 ‘ 𝑖 ) = ( 𝐹 ‘ 𝑗 ) → 𝑖 = 𝑗 ) ) )
173 dff13 ⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑖 ∈ 𝐴 ∀ 𝑗 ∈ 𝐴 ( ( 𝐹 ‘ 𝑖 ) = ( 𝐹 ‘ 𝑗 ) → 𝑖 = 𝑗 ) ) )
174 172 173 sylibr ⊢ ( 𝜑 → 𝐹 : 𝐴 –1-1→ 𝐵 )