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