Metamath Proof Explorer

Theorem sticksstones3

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

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

Proof

Step Hyp Ref Expression
1 sticksstones3.1 ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
2 sticksstones3.2 ⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
3 sticksstones3.3 ⊢ 𝐵 = { 𝑎 ∈ 𝒫 ( 1 ... 𝑁 ) ∣ ( ♯ ‘ 𝑎 ) = 𝐾 }
4 sticksstones3.4 ⊢ 𝐴 = { 𝑓 ∣ ( 𝑓 : ( 1 ... 𝐾 ) ⟶ ( 1 ... 𝑁 ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ) ) }
5 sticksstones3.5 ⊢ 𝐹 = ( 𝑧 ∈ 𝐴 ↦ ran 𝑧 )
6 1 2 3 4 5 sticksstones2 ⊢ ( 𝜑 → 𝐹 : 𝐴 –1-1→ 𝐵 )
7 df-f1 ⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ Fun ◡ 𝐹 ) )
8 7 biimpi ⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ Fun ◡ 𝐹 ) )
9 8 simpld ⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → 𝐹 : 𝐴 ⟶ 𝐵 )
10 6 9 syl ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
11 3 eleq2i ⊢ ( 𝑤 ∈ 𝐵 ↔ 𝑤 ∈ { 𝑎 ∈ 𝒫 ( 1 ... 𝑁 ) ∣ ( ♯ ‘ 𝑎 ) = 𝐾 } )
12 11 biimpi ⊢ ( 𝑤 ∈ 𝐵 → 𝑤 ∈ { 𝑎 ∈ 𝒫 ( 1 ... 𝑁 ) ∣ ( ♯ ‘ 𝑎 ) = 𝐾 } )
13 12 adantl ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐵 ) → 𝑤 ∈ { 𝑎 ∈ 𝒫 ( 1 ... 𝑁 ) ∣ ( ♯ ‘ 𝑎 ) = 𝐾 } )
14 fveqeq2 ⊢ ( 𝑎 = 𝑤 → ( ( ♯ ‘ 𝑎 ) = 𝐾 ↔ ( ♯ ‘ 𝑤 ) = 𝐾 ) )
15 14 elrab ⊢ ( 𝑤 ∈ { 𝑎 ∈ 𝒫 ( 1 ... 𝑁 ) ∣ ( ♯ ‘ 𝑎 ) = 𝐾 } ↔ ( 𝑤 ∈ 𝒫 ( 1 ... 𝑁 ) ∧ ( ♯ ‘ 𝑤 ) = 𝐾 ) )
16 13 15 sylib ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐵 ) → ( 𝑤 ∈ 𝒫 ( 1 ... 𝑁 ) ∧ ( ♯ ‘ 𝑤 ) = 𝐾 ) )
17 16 simpld ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐵 ) → 𝑤 ∈ 𝒫 ( 1 ... 𝑁 ) )
18 17 elpwid ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐵 ) → 𝑤 ⊆ ( 1 ... 𝑁 ) )
19 18 sseld ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐵 ) → ( 𝑐 ∈ 𝑤 → 𝑐 ∈ ( 1 ... 𝑁 ) ) )
20 19 imp ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝐵 ) ∧ 𝑐 ∈ 𝑤 ) → 𝑐 ∈ ( 1 ... 𝑁 ) )
21 20 3impa ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑐 ∈ 𝑤 ) → 𝑐 ∈ ( 1 ... 𝑁 ) )
22 elfznn ⊢ ( 𝑐 ∈ ( 1 ... 𝑁 ) → 𝑐 ∈ ℕ )
23 21 22 syl ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑐 ∈ 𝑤 ) → 𝑐 ∈ ℕ )
24 23 nnred ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑐 ∈ 𝑤 ) → 𝑐 ∈ ℝ )
25 24 3expa ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝐵 ) ∧ 𝑐 ∈ 𝑤 ) → 𝑐 ∈ ℝ )
26 25 ex ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐵 ) → ( 𝑐 ∈ 𝑤 → 𝑐 ∈ ℝ ) )
27 26 ssrdv ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐵 ) → 𝑤 ⊆ ℝ )
28 ltso ⊢ < Or ℝ
29 soss ⊢ ( 𝑤 ⊆ ℝ → ( < Or ℝ → < Or 𝑤 ) )
30 28 29 mpi ⊢ ( 𝑤 ⊆ ℝ → < Or 𝑤 )
31 27 30 syl ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐵 ) → < Or 𝑤 )
32 fzfid ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐵 ) → ( 1 ... 𝑁 ) ∈ Fin )
33 32 18 ssfid ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐵 ) → 𝑤 ∈ Fin )
34 fz1iso ⊢ ( ( < Or 𝑤 ∧ 𝑤 ∈ Fin ) → ∃ 𝑣 𝑣 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑤 ) ) , 𝑤 ) )
35 31 33 34 syl2anc ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐵 ) → ∃ 𝑣 𝑣 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑤 ) ) , 𝑤 ) )
36 df-isom ⊢ ( 𝑣 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑤 ) ) , 𝑤 ) ↔ ( 𝑣 : ( 1 ... ( ♯ ‘ 𝑤 ) ) –1-1-onto→ 𝑤 ∧ ∀ 𝑥 ∈ ( 1 ... ( ♯ ‘ 𝑤 ) ) ∀ 𝑦 ∈ ( 1 ... ( ♯ ‘ 𝑤 ) ) ( 𝑥 < 𝑦 ↔ ( 𝑣 ‘ 𝑥 ) < ( 𝑣 ‘ 𝑦 ) ) ) )
37 36 biimpi ⊢ ( 𝑣 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑤 ) ) , 𝑤 ) → ( 𝑣 : ( 1 ... ( ♯ ‘ 𝑤 ) ) –1-1-onto→ 𝑤 ∧ ∀ 𝑥 ∈ ( 1 ... ( ♯ ‘ 𝑤 ) ) ∀ 𝑦 ∈ ( 1 ... ( ♯ ‘ 𝑤 ) ) ( 𝑥 < 𝑦 ↔ ( 𝑣 ‘ 𝑥 ) < ( 𝑣 ‘ 𝑦 ) ) ) )
38 37 3ad2ant3 ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑣 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑤 ) ) , 𝑤 ) ) → ( 𝑣 : ( 1 ... ( ♯ ‘ 𝑤 ) ) –1-1-onto→ 𝑤 ∧ ∀ 𝑥 ∈ ( 1 ... ( ♯ ‘ 𝑤 ) ) ∀ 𝑦 ∈ ( 1 ... ( ♯ ‘ 𝑤 ) ) ( 𝑥 < 𝑦 ↔ ( 𝑣 ‘ 𝑥 ) < ( 𝑣 ‘ 𝑦 ) ) ) )
39 38 simpld ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑣 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑤 ) ) , 𝑤 ) ) → 𝑣 : ( 1 ... ( ♯ ‘ 𝑤 ) ) –1-1-onto→ 𝑤 )
40 16 simprd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐵 ) → ( ♯ ‘ 𝑤 ) = 𝐾 )
41 oveq2 ⊢ ( ( ♯ ‘ 𝑤 ) = 𝐾 → ( 1 ... ( ♯ ‘ 𝑤 ) ) = ( 1 ... 𝐾 ) )
42 41 f1oeq2d ⊢ ( ( ♯ ‘ 𝑤 ) = 𝐾 → ( 𝑣 : ( 1 ... ( ♯ ‘ 𝑤 ) ) –1-1-onto→ 𝑤 ↔ 𝑣 : ( 1 ... 𝐾 ) –1-1-onto→ 𝑤 ) )
43 40 42 syl ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐵 ) → ( 𝑣 : ( 1 ... ( ♯ ‘ 𝑤 ) ) –1-1-onto→ 𝑤 ↔ 𝑣 : ( 1 ... 𝐾 ) –1-1-onto→ 𝑤 ) )
44 43 biimpd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐵 ) → ( 𝑣 : ( 1 ... ( ♯ ‘ 𝑤 ) ) –1-1-onto→ 𝑤 → 𝑣 : ( 1 ... 𝐾 ) –1-1-onto→ 𝑤 ) )
45 44 3adant3 ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑣 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑤 ) ) , 𝑤 ) ) → ( 𝑣 : ( 1 ... ( ♯ ‘ 𝑤 ) ) –1-1-onto→ 𝑤 → 𝑣 : ( 1 ... 𝐾 ) –1-1-onto→ 𝑤 ) )
46 39 45 mpd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑣 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑤 ) ) , 𝑤 ) ) → 𝑣 : ( 1 ... 𝐾 ) –1-1-onto→ 𝑤 )
47 f1of ⊢ ( 𝑣 : ( 1 ... 𝐾 ) –1-1-onto→ 𝑤 → 𝑣 : ( 1 ... 𝐾 ) ⟶ 𝑤 )
48 46 47 syl ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑣 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑤 ) ) , 𝑤 ) ) → 𝑣 : ( 1 ... 𝐾 ) ⟶ 𝑤 )
49 48 ffnd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑣 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑤 ) ) , 𝑤 ) ) → 𝑣 Fn ( 1 ... 𝐾 ) )
50 ovexd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑣 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑤 ) ) , 𝑤 ) ) → ( 1 ... 𝐾 ) ∈ V )
51 49 50 fnexd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑣 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑤 ) ) , 𝑤 ) ) → 𝑣 ∈ V )
52 18 3adant3 ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑣 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑤 ) ) , 𝑤 ) ) → 𝑤 ⊆ ( 1 ... 𝑁 ) )
53 fss ⊢ ( ( 𝑣 : ( 1 ... 𝐾 ) ⟶ 𝑤 ∧ 𝑤 ⊆ ( 1 ... 𝑁 ) ) → 𝑣 : ( 1 ... 𝐾 ) ⟶ ( 1 ... 𝑁 ) )
54 48 52 53 syl2anc ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑣 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑤 ) ) , 𝑤 ) ) → 𝑣 : ( 1 ... 𝐾 ) ⟶ ( 1 ... 𝑁 ) )
55 38 simprd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑣 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑤 ) ) , 𝑤 ) ) → ∀ 𝑥 ∈ ( 1 ... ( ♯ ‘ 𝑤 ) ) ∀ 𝑦 ∈ ( 1 ... ( ♯ ‘ 𝑤 ) ) ( 𝑥 < 𝑦 ↔ ( 𝑣 ‘ 𝑥 ) < ( 𝑣 ‘ 𝑦 ) ) )
56 biimp ⊢ ( ( 𝑥 < 𝑦 ↔ ( 𝑣 ‘ 𝑥 ) < ( 𝑣 ‘ 𝑦 ) ) → ( 𝑥 < 𝑦 → ( 𝑣 ‘ 𝑥 ) < ( 𝑣 ‘ 𝑦 ) ) )
57 56 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑣 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑤 ) ) , 𝑤 ) ) ∧ 𝑥 ∈ ( 1 ... ( ♯ ‘ 𝑤 ) ) ) ∧ 𝑦 ∈ ( 1 ... ( ♯ ‘ 𝑤 ) ) ) → ( ( 𝑥 < 𝑦 ↔ ( 𝑣 ‘ 𝑥 ) < ( 𝑣 ‘ 𝑦 ) ) → ( 𝑥 < 𝑦 → ( 𝑣 ‘ 𝑥 ) < ( 𝑣 ‘ 𝑦 ) ) ) )
58 57 ralimdva ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑣 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑤 ) ) , 𝑤 ) ) ∧ 𝑥 ∈ ( 1 ... ( ♯ ‘ 𝑤 ) ) ) → ( ∀ 𝑦 ∈ ( 1 ... ( ♯ ‘ 𝑤 ) ) ( 𝑥 < 𝑦 ↔ ( 𝑣 ‘ 𝑥 ) < ( 𝑣 ‘ 𝑦 ) ) → ∀ 𝑦 ∈ ( 1 ... ( ♯ ‘ 𝑤 ) ) ( 𝑥 < 𝑦 → ( 𝑣 ‘ 𝑥 ) < ( 𝑣 ‘ 𝑦 ) ) ) )
59 58 ralimdva ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑣 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑤 ) ) , 𝑤 ) ) → ( ∀ 𝑥 ∈ ( 1 ... ( ♯ ‘ 𝑤 ) ) ∀ 𝑦 ∈ ( 1 ... ( ♯ ‘ 𝑤 ) ) ( 𝑥 < 𝑦 ↔ ( 𝑣 ‘ 𝑥 ) < ( 𝑣 ‘ 𝑦 ) ) → ∀ 𝑥 ∈ ( 1 ... ( ♯ ‘ 𝑤 ) ) ∀ 𝑦 ∈ ( 1 ... ( ♯ ‘ 𝑤 ) ) ( 𝑥 < 𝑦 → ( 𝑣 ‘ 𝑥 ) < ( 𝑣 ‘ 𝑦 ) ) ) )
60 55 59 mpd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑣 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑤 ) ) , 𝑤 ) ) → ∀ 𝑥 ∈ ( 1 ... ( ♯ ‘ 𝑤 ) ) ∀ 𝑦 ∈ ( 1 ... ( ♯ ‘ 𝑤 ) ) ( 𝑥 < 𝑦 → ( 𝑣 ‘ 𝑥 ) < ( 𝑣 ‘ 𝑦 ) ) )
61 40 adantr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝐵 ) ∧ 𝑣 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑤 ) ) , 𝑤 ) ) → ( ♯ ‘ 𝑤 ) = 𝐾 )
62 61 3impa ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑣 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑤 ) ) , 𝑤 ) ) → ( ♯ ‘ 𝑤 ) = 𝐾 )
63 62 oveq2d ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑣 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑤 ) ) , 𝑤 ) ) → ( 1 ... ( ♯ ‘ 𝑤 ) ) = ( 1 ... 𝐾 ) )
64 63 raleqdv ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑣 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑤 ) ) , 𝑤 ) ) → ( ∀ 𝑦 ∈ ( 1 ... ( ♯ ‘ 𝑤 ) ) ( 𝑥 < 𝑦 → ( 𝑣 ‘ 𝑥 ) < ( 𝑣 ‘ 𝑦 ) ) ↔ ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑣 ‘ 𝑥 ) < ( 𝑣 ‘ 𝑦 ) ) ) )
65 64 adantr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑣 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑤 ) ) , 𝑤 ) ) ∧ 𝑥 ∈ ( 1 ... ( ♯ ‘ 𝑤 ) ) ) → ( ∀ 𝑦 ∈ ( 1 ... ( ♯ ‘ 𝑤 ) ) ( 𝑥 < 𝑦 → ( 𝑣 ‘ 𝑥 ) < ( 𝑣 ‘ 𝑦 ) ) ↔ ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑣 ‘ 𝑥 ) < ( 𝑣 ‘ 𝑦 ) ) ) )
66 63 65 raleqbidva ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑣 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑤 ) ) , 𝑤 ) ) → ( ∀ 𝑥 ∈ ( 1 ... ( ♯ ‘ 𝑤 ) ) ∀ 𝑦 ∈ ( 1 ... ( ♯ ‘ 𝑤 ) ) ( 𝑥 < 𝑦 → ( 𝑣 ‘ 𝑥 ) < ( 𝑣 ‘ 𝑦 ) ) ↔ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑣 ‘ 𝑥 ) < ( 𝑣 ‘ 𝑦 ) ) ) )
67 60 66 mpbid ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑣 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑤 ) ) , 𝑤 ) ) → ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑣 ‘ 𝑥 ) < ( 𝑣 ‘ 𝑦 ) ) )
68 54 67 jca ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑣 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑤 ) ) , 𝑤 ) ) → ( 𝑣 : ( 1 ... 𝐾 ) ⟶ ( 1 ... 𝑁 ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑣 ‘ 𝑥 ) < ( 𝑣 ‘ 𝑦 ) ) ) )
69 feq1 ⊢ ( 𝑓 = 𝑣 → ( 𝑓 : ( 1 ... 𝐾 ) ⟶ ( 1 ... 𝑁 ) ↔ 𝑣 : ( 1 ... 𝐾 ) ⟶ ( 1 ... 𝑁 ) ) )
70 fveq1 ⊢ ( 𝑓 = 𝑣 → ( 𝑓 ‘ 𝑥 ) = ( 𝑣 ‘ 𝑥 ) )
71 fveq1 ⊢ ( 𝑓 = 𝑣 → ( 𝑓 ‘ 𝑦 ) = ( 𝑣 ‘ 𝑦 ) )
72 70 71 breq12d ⊢ ( 𝑓 = 𝑣 → ( ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ↔ ( 𝑣 ‘ 𝑥 ) < ( 𝑣 ‘ 𝑦 ) ) )
73 72 imbi2d ⊢ ( 𝑓 = 𝑣 → ( ( 𝑥 < 𝑦 → ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ) ↔ ( 𝑥 < 𝑦 → ( 𝑣 ‘ 𝑥 ) < ( 𝑣 ‘ 𝑦 ) ) ) )
74 73 2ralbidv ⊢ ( 𝑓 = 𝑣 → ( ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ) ↔ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑣 ‘ 𝑥 ) < ( 𝑣 ‘ 𝑦 ) ) ) )
75 69 74 anbi12d ⊢ ( 𝑓 = 𝑣 → ( ( 𝑓 : ( 1 ... 𝐾 ) ⟶ ( 1 ... 𝑁 ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ) ) ↔ ( 𝑣 : ( 1 ... 𝐾 ) ⟶ ( 1 ... 𝑁 ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑣 ‘ 𝑥 ) < ( 𝑣 ‘ 𝑦 ) ) ) ) )
76 51 68 75 elabd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑣 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑤 ) ) , 𝑤 ) ) → 𝑣 ∈ { 𝑓 ∣ ( 𝑓 : ( 1 ... 𝐾 ) ⟶ ( 1 ... 𝑁 ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ) ) } )
77 4 eleq2i ⊢ ( 𝑣 ∈ 𝐴 ↔ 𝑣 ∈ { 𝑓 ∣ ( 𝑓 : ( 1 ... 𝐾 ) ⟶ ( 1 ... 𝑁 ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ) ) } )
78 76 77 sylibr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑣 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑤 ) ) , 𝑤 ) ) → 𝑣 ∈ 𝐴 )
79 5 a1i ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) → 𝐹 = ( 𝑧 ∈ 𝐴 ↦ ran 𝑧 ) )
80 simpr ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) ∧ 𝑧 = 𝑣 ) → 𝑧 = 𝑣 )
81 80 rneqd ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) ∧ 𝑧 = 𝑣 ) → ran 𝑧 = ran 𝑣 )
82 simpr ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) → 𝑣 ∈ 𝐴 )
83 rnexg ⊢ ( 𝑣 ∈ 𝐴 → ran 𝑣 ∈ V )
84 82 83 syl ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) → ran 𝑣 ∈ V )
85 79 81 82 84 fvmptd ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑣 ) = ran 𝑣 )
86 85 ex ⊢ ( 𝜑 → ( 𝑣 ∈ 𝐴 → ( 𝐹 ‘ 𝑣 ) = ran 𝑣 ) )
87 86 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑣 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑤 ) ) , 𝑤 ) ) → ( 𝑣 ∈ 𝐴 → ( 𝐹 ‘ 𝑣 ) = ran 𝑣 ) )
88 78 87 mpd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑣 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑤 ) ) , 𝑤 ) ) → ( 𝐹 ‘ 𝑣 ) = ran 𝑣 )
89 dff1o2 ⊢ ( 𝑣 : ( 1 ... 𝐾 ) –1-1-onto→ 𝑤 ↔ ( 𝑣 Fn ( 1 ... 𝐾 ) ∧ Fun ◡ 𝑣 ∧ ran 𝑣 = 𝑤 ) )
90 89 biimpi ⊢ ( 𝑣 : ( 1 ... 𝐾 ) –1-1-onto→ 𝑤 → ( 𝑣 Fn ( 1 ... 𝐾 ) ∧ Fun ◡ 𝑣 ∧ ran 𝑣 = 𝑤 ) )
91 90 simp3d ⊢ ( 𝑣 : ( 1 ... 𝐾 ) –1-1-onto→ 𝑤 → ran 𝑣 = 𝑤 )
92 46 91 syl ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑣 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑤 ) ) , 𝑤 ) ) → ran 𝑣 = 𝑤 )
93 88 92 eqtrd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑣 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑤 ) ) , 𝑤 ) ) → ( 𝐹 ‘ 𝑣 ) = 𝑤 )
94 93 eqcomd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑣 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑤 ) ) , 𝑤 ) ) → 𝑤 = ( 𝐹 ‘ 𝑣 ) )
95 78 94 jca ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑣 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑤 ) ) , 𝑤 ) ) → ( 𝑣 ∈ 𝐴 ∧ 𝑤 = ( 𝐹 ‘ 𝑣 ) ) )
96 95 3expa ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝐵 ) ∧ 𝑣 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑤 ) ) , 𝑤 ) ) → ( 𝑣 ∈ 𝐴 ∧ 𝑤 = ( 𝐹 ‘ 𝑣 ) ) )
97 96 ex ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐵 ) → ( 𝑣 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑤 ) ) , 𝑤 ) → ( 𝑣 ∈ 𝐴 ∧ 𝑤 = ( 𝐹 ‘ 𝑣 ) ) ) )
98 97 eximdv ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐵 ) → ( ∃ 𝑣 𝑣 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑤 ) ) , 𝑤 ) → ∃ 𝑣 ( 𝑣 ∈ 𝐴 ∧ 𝑤 = ( 𝐹 ‘ 𝑣 ) ) ) )
99 35 98 mpd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐵 ) → ∃ 𝑣 ( 𝑣 ∈ 𝐴 ∧ 𝑤 = ( 𝐹 ‘ 𝑣 ) ) )
100 df-rex ⊢ ( ∃ 𝑣 ∈ 𝐴 𝑤 = ( 𝐹 ‘ 𝑣 ) ↔ ∃ 𝑣 ( 𝑣 ∈ 𝐴 ∧ 𝑤 = ( 𝐹 ‘ 𝑣 ) ) )
101 99 100 sylibr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐵 ) → ∃ 𝑣 ∈ 𝐴 𝑤 = ( 𝐹 ‘ 𝑣 ) )
102 101 ralrimiva ⊢ ( 𝜑 → ∀ 𝑤 ∈ 𝐵 ∃ 𝑣 ∈ 𝐴 𝑤 = ( 𝐹 ‘ 𝑣 ) )
103 10 102 jca ⊢ ( 𝜑 → ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑤 ∈ 𝐵 ∃ 𝑣 ∈ 𝐴 𝑤 = ( 𝐹 ‘ 𝑣 ) ) )
104 dffo3 ⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑤 ∈ 𝐵 ∃ 𝑣 ∈ 𝐴 𝑤 = ( 𝐹 ‘ 𝑣 ) ) )
105 104 a1i ⊢ ( 𝜑 → ( 𝐹 : 𝐴 –onto→ 𝐵 ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑤 ∈ 𝐵 ∃ 𝑣 ∈ 𝐴 𝑤 = ( 𝐹 ‘ 𝑣 ) ) ) )
106 103 105 mpbird ⊢ ( 𝜑 → 𝐹 : 𝐴 –onto→ 𝐵 )