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