| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | sticksstones3.1 | . . . . 5
⊢ (𝜑 → 𝑁 ∈
ℕ0) | 
| 2 |  | sticksstones3.2 | . . . . 5
⊢ (𝜑 → 𝐾 ∈
ℕ0) | 
| 3 |  | sticksstones3.3 | . . . . 5
⊢ 𝐵 = {𝑎 ∈ 𝒫 (1...𝑁) ∣ (♯‘𝑎) = 𝐾} | 
| 4 |  | sticksstones3.4 | . . . . 5
⊢ 𝐴 = {𝑓 ∣ (𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))} | 
| 5 |  | sticksstones3.5 | . . . . 5
⊢ 𝐹 = (𝑧 ∈ 𝐴 ↦ ran 𝑧) | 
| 6 | 1, 2, 3, 4, 5 | sticksstones2 42149 | . . . 4
⊢ (𝜑 → 𝐹:𝐴–1-1→𝐵) | 
| 7 |  | df-f1 6565 | . . . . . 6
⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹)) | 
| 8 | 7 | biimpi 216 | . . . . 5
⊢ (𝐹:𝐴–1-1→𝐵 → (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹)) | 
| 9 | 8 | simpld 494 | . . . 4
⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴⟶𝐵) | 
| 10 | 6, 9 | syl 17 | . . 3
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) | 
| 11 | 3 | eleq2i 2832 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑤 ∈ 𝐵 ↔ 𝑤 ∈ {𝑎 ∈ 𝒫 (1...𝑁) ∣ (♯‘𝑎) = 𝐾}) | 
| 12 | 11 | biimpi 216 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤 ∈ 𝐵 → 𝑤 ∈ {𝑎 ∈ 𝒫 (1...𝑁) ∣ (♯‘𝑎) = 𝐾}) | 
| 13 | 12 | adantl 481 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵) → 𝑤 ∈ {𝑎 ∈ 𝒫 (1...𝑁) ∣ (♯‘𝑎) = 𝐾}) | 
| 14 |  | fveqeq2 6914 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑎 = 𝑤 → ((♯‘𝑎) = 𝐾 ↔ (♯‘𝑤) = 𝐾)) | 
| 15 | 14 | elrab 3691 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 ∈ {𝑎 ∈ 𝒫 (1...𝑁) ∣ (♯‘𝑎) = 𝐾} ↔ (𝑤 ∈ 𝒫 (1...𝑁) ∧ (♯‘𝑤) = 𝐾)) | 
| 16 | 13, 15 | sylib 218 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵) → (𝑤 ∈ 𝒫 (1...𝑁) ∧ (♯‘𝑤) = 𝐾)) | 
| 17 | 16 | simpld 494 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵) → 𝑤 ∈ 𝒫 (1...𝑁)) | 
| 18 | 17 | elpwid 4608 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵) → 𝑤 ⊆ (1...𝑁)) | 
| 19 | 18 | sseld 3981 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵) → (𝑐 ∈ 𝑤 → 𝑐 ∈ (1...𝑁))) | 
| 20 | 19 | imp 406 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐵) ∧ 𝑐 ∈ 𝑤) → 𝑐 ∈ (1...𝑁)) | 
| 21 | 20 | 3impa 1109 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑐 ∈ 𝑤) → 𝑐 ∈ (1...𝑁)) | 
| 22 |  | elfznn 13594 | . . . . . . . . . . . . 13
⊢ (𝑐 ∈ (1...𝑁) → 𝑐 ∈ ℕ) | 
| 23 | 21, 22 | syl 17 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑐 ∈ 𝑤) → 𝑐 ∈ ℕ) | 
| 24 | 23 | nnred 12282 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑐 ∈ 𝑤) → 𝑐 ∈ ℝ) | 
| 25 | 24 | 3expa 1118 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐵) ∧ 𝑐 ∈ 𝑤) → 𝑐 ∈ ℝ) | 
| 26 | 25 | ex 412 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵) → (𝑐 ∈ 𝑤 → 𝑐 ∈ ℝ)) | 
| 27 | 26 | ssrdv 3988 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵) → 𝑤 ⊆ ℝ) | 
| 28 |  | ltso 11342 | . . . . . . . . 9
⊢  < Or
ℝ | 
| 29 |  | soss 5611 | . . . . . . . . 9
⊢ (𝑤 ⊆ ℝ → ( <
Or ℝ → < Or 𝑤)) | 
| 30 | 28, 29 | mpi 20 | . . . . . . . 8
⊢ (𝑤 ⊆ ℝ → < Or
𝑤) | 
| 31 | 27, 30 | syl 17 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵) → < Or 𝑤) | 
| 32 |  | fzfid 14015 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵) → (1...𝑁) ∈ Fin) | 
| 33 | 32, 18 | ssfid 9302 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵) → 𝑤 ∈ Fin) | 
| 34 |  | fz1iso 14502 | . . . . . . 7
⊢ (( <
Or 𝑤 ∧ 𝑤 ∈ Fin) → ∃𝑣 𝑣 Isom < , < ((1...(♯‘𝑤)), 𝑤)) | 
| 35 | 31, 33, 34 | syl2anc 584 | . . . . . 6
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵) → ∃𝑣 𝑣 Isom < , < ((1...(♯‘𝑤)), 𝑤)) | 
| 36 |  | df-isom 6569 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑣 Isom < , <
((1...(♯‘𝑤)),
𝑤) ↔ (𝑣:(1...(♯‘𝑤))–1-1-onto→𝑤 ∧ ∀𝑥 ∈
(1...(♯‘𝑤))∀𝑦 ∈ (1...(♯‘𝑤))(𝑥 < 𝑦 ↔ (𝑣‘𝑥) < (𝑣‘𝑦)))) | 
| 37 | 36 | biimpi 216 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑣 Isom < , <
((1...(♯‘𝑤)),
𝑤) → (𝑣:(1...(♯‘𝑤))–1-1-onto→𝑤 ∧ ∀𝑥 ∈
(1...(♯‘𝑤))∀𝑦 ∈ (1...(♯‘𝑤))(𝑥 < 𝑦 ↔ (𝑣‘𝑥) < (𝑣‘𝑦)))) | 
| 38 | 37 | 3ad2ant3 1135 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑣 Isom < , < ((1...(♯‘𝑤)), 𝑤)) → (𝑣:(1...(♯‘𝑤))–1-1-onto→𝑤 ∧ ∀𝑥 ∈
(1...(♯‘𝑤))∀𝑦 ∈ (1...(♯‘𝑤))(𝑥 < 𝑦 ↔ (𝑣‘𝑥) < (𝑣‘𝑦)))) | 
| 39 | 38 | simpld 494 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑣 Isom < , < ((1...(♯‘𝑤)), 𝑤)) → 𝑣:(1...(♯‘𝑤))–1-1-onto→𝑤) | 
| 40 | 16 | simprd 495 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵) → (♯‘𝑤) = 𝐾) | 
| 41 |  | oveq2 7440 | . . . . . . . . . . . . . . . . . . . 20
⊢
((♯‘𝑤) =
𝐾 →
(1...(♯‘𝑤)) =
(1...𝐾)) | 
| 42 | 41 | f1oeq2d 6843 | . . . . . . . . . . . . . . . . . . 19
⊢
((♯‘𝑤) =
𝐾 → (𝑣:(1...(♯‘𝑤))–1-1-onto→𝑤 ↔ 𝑣:(1...𝐾)–1-1-onto→𝑤)) | 
| 43 | 40, 42 | syl 17 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵) → (𝑣:(1...(♯‘𝑤))–1-1-onto→𝑤 ↔ 𝑣:(1...𝐾)–1-1-onto→𝑤)) | 
| 44 | 43 | biimpd 229 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵) → (𝑣:(1...(♯‘𝑤))–1-1-onto→𝑤 → 𝑣:(1...𝐾)–1-1-onto→𝑤)) | 
| 45 | 44 | 3adant3 1132 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑣 Isom < , < ((1...(♯‘𝑤)), 𝑤)) → (𝑣:(1...(♯‘𝑤))–1-1-onto→𝑤 → 𝑣:(1...𝐾)–1-1-onto→𝑤)) | 
| 46 | 39, 45 | mpd 15 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑣 Isom < , < ((1...(♯‘𝑤)), 𝑤)) → 𝑣:(1...𝐾)–1-1-onto→𝑤) | 
| 47 |  | f1of 6847 | . . . . . . . . . . . . . . 15
⊢ (𝑣:(1...𝐾)–1-1-onto→𝑤 → 𝑣:(1...𝐾)⟶𝑤) | 
| 48 | 46, 47 | syl 17 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑣 Isom < , < ((1...(♯‘𝑤)), 𝑤)) → 𝑣:(1...𝐾)⟶𝑤) | 
| 49 | 48 | ffnd 6736 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑣 Isom < , < ((1...(♯‘𝑤)), 𝑤)) → 𝑣 Fn (1...𝐾)) | 
| 50 |  | ovexd 7467 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑣 Isom < , < ((1...(♯‘𝑤)), 𝑤)) → (1...𝐾) ∈ V) | 
| 51 | 49, 50 | fnexd 7239 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑣 Isom < , < ((1...(♯‘𝑤)), 𝑤)) → 𝑣 ∈ V) | 
| 52 | 18 | 3adant3 1132 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑣 Isom < , < ((1...(♯‘𝑤)), 𝑤)) → 𝑤 ⊆ (1...𝑁)) | 
| 53 |  | fss 6751 | . . . . . . . . . . . . . 14
⊢ ((𝑣:(1...𝐾)⟶𝑤 ∧ 𝑤 ⊆ (1...𝑁)) → 𝑣:(1...𝐾)⟶(1...𝑁)) | 
| 54 | 48, 52, 53 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑣 Isom < , < ((1...(♯‘𝑤)), 𝑤)) → 𝑣:(1...𝐾)⟶(1...𝑁)) | 
| 55 | 38 | simprd 495 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑣 Isom < , < ((1...(♯‘𝑤)), 𝑤)) → ∀𝑥 ∈ (1...(♯‘𝑤))∀𝑦 ∈ (1...(♯‘𝑤))(𝑥 < 𝑦 ↔ (𝑣‘𝑥) < (𝑣‘𝑦))) | 
| 56 |  | biimp 215 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 < 𝑦 ↔ (𝑣‘𝑥) < (𝑣‘𝑦)) → (𝑥 < 𝑦 → (𝑣‘𝑥) < (𝑣‘𝑦))) | 
| 57 | 56 | a1i 11 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑣 Isom < , < ((1...(♯‘𝑤)), 𝑤)) ∧ 𝑥 ∈ (1...(♯‘𝑤))) ∧ 𝑦 ∈ (1...(♯‘𝑤))) → ((𝑥 < 𝑦 ↔ (𝑣‘𝑥) < (𝑣‘𝑦)) → (𝑥 < 𝑦 → (𝑣‘𝑥) < (𝑣‘𝑦)))) | 
| 58 | 57 | ralimdva 3166 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑣 Isom < , < ((1...(♯‘𝑤)), 𝑤)) ∧ 𝑥 ∈ (1...(♯‘𝑤))) → (∀𝑦 ∈
(1...(♯‘𝑤))(𝑥 < 𝑦 ↔ (𝑣‘𝑥) < (𝑣‘𝑦)) → ∀𝑦 ∈ (1...(♯‘𝑤))(𝑥 < 𝑦 → (𝑣‘𝑥) < (𝑣‘𝑦)))) | 
| 59 | 58 | ralimdva 3166 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑣 Isom < , < ((1...(♯‘𝑤)), 𝑤)) → (∀𝑥 ∈ (1...(♯‘𝑤))∀𝑦 ∈ (1...(♯‘𝑤))(𝑥 < 𝑦 ↔ (𝑣‘𝑥) < (𝑣‘𝑦)) → ∀𝑥 ∈ (1...(♯‘𝑤))∀𝑦 ∈ (1...(♯‘𝑤))(𝑥 < 𝑦 → (𝑣‘𝑥) < (𝑣‘𝑦)))) | 
| 60 | 55, 59 | mpd 15 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑣 Isom < , < ((1...(♯‘𝑤)), 𝑤)) → ∀𝑥 ∈ (1...(♯‘𝑤))∀𝑦 ∈ (1...(♯‘𝑤))(𝑥 < 𝑦 → (𝑣‘𝑥) < (𝑣‘𝑦))) | 
| 61 | 40 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐵) ∧ 𝑣 Isom < , < ((1...(♯‘𝑤)), 𝑤)) → (♯‘𝑤) = 𝐾) | 
| 62 | 61 | 3impa 1109 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑣 Isom < , < ((1...(♯‘𝑤)), 𝑤)) → (♯‘𝑤) = 𝐾) | 
| 63 | 62 | oveq2d 7448 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑣 Isom < , < ((1...(♯‘𝑤)), 𝑤)) → (1...(♯‘𝑤)) = (1...𝐾)) | 
| 64 | 63 | raleqdv 3325 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑣 Isom < , < ((1...(♯‘𝑤)), 𝑤)) → (∀𝑦 ∈ (1...(♯‘𝑤))(𝑥 < 𝑦 → (𝑣‘𝑥) < (𝑣‘𝑦)) ↔ ∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑣‘𝑥) < (𝑣‘𝑦)))) | 
| 65 | 64 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑣 Isom < , < ((1...(♯‘𝑤)), 𝑤)) ∧ 𝑥 ∈ (1...(♯‘𝑤))) → (∀𝑦 ∈
(1...(♯‘𝑤))(𝑥 < 𝑦 → (𝑣‘𝑥) < (𝑣‘𝑦)) ↔ ∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑣‘𝑥) < (𝑣‘𝑦)))) | 
| 66 | 63, 65 | raleqbidva 3331 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑣 Isom < , < ((1...(♯‘𝑤)), 𝑤)) → (∀𝑥 ∈ (1...(♯‘𝑤))∀𝑦 ∈ (1...(♯‘𝑤))(𝑥 < 𝑦 → (𝑣‘𝑥) < (𝑣‘𝑦)) ↔ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑣‘𝑥) < (𝑣‘𝑦)))) | 
| 67 | 60, 66 | mpbid 232 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑣 Isom < , < ((1...(♯‘𝑤)), 𝑤)) → ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑣‘𝑥) < (𝑣‘𝑦))) | 
| 68 | 54, 67 | jca 511 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑣 Isom < , < ((1...(♯‘𝑤)), 𝑤)) → (𝑣:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑣‘𝑥) < (𝑣‘𝑦)))) | 
| 69 |  | feq1 6715 | . . . . . . . . . . . . 13
⊢ (𝑓 = 𝑣 → (𝑓:(1...𝐾)⟶(1...𝑁) ↔ 𝑣:(1...𝐾)⟶(1...𝑁))) | 
| 70 |  | fveq1 6904 | . . . . . . . . . . . . . . . 16
⊢ (𝑓 = 𝑣 → (𝑓‘𝑥) = (𝑣‘𝑥)) | 
| 71 |  | fveq1 6904 | . . . . . . . . . . . . . . . 16
⊢ (𝑓 = 𝑣 → (𝑓‘𝑦) = (𝑣‘𝑦)) | 
| 72 | 70, 71 | breq12d 5155 | . . . . . . . . . . . . . . 15
⊢ (𝑓 = 𝑣 → ((𝑓‘𝑥) < (𝑓‘𝑦) ↔ (𝑣‘𝑥) < (𝑣‘𝑦))) | 
| 73 | 72 | imbi2d 340 | . . . . . . . . . . . . . 14
⊢ (𝑓 = 𝑣 → ((𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)) ↔ (𝑥 < 𝑦 → (𝑣‘𝑥) < (𝑣‘𝑦)))) | 
| 74 | 73 | 2ralbidv 3220 | . . . . . . . . . . . . 13
⊢ (𝑓 = 𝑣 → (∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)) ↔ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑣‘𝑥) < (𝑣‘𝑦)))) | 
| 75 | 69, 74 | anbi12d 632 | . . . . . . . . . . . 12
⊢ (𝑓 = 𝑣 → ((𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦))) ↔ (𝑣:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑣‘𝑥) < (𝑣‘𝑦))))) | 
| 76 | 51, 68, 75 | elabd 3680 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑣 Isom < , < ((1...(♯‘𝑤)), 𝑤)) → 𝑣 ∈ {𝑓 ∣ (𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))}) | 
| 77 | 4 | eleq2i 2832 | . . . . . . . . . . 11
⊢ (𝑣 ∈ 𝐴 ↔ 𝑣 ∈ {𝑓 ∣ (𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))}) | 
| 78 | 76, 77 | sylibr 234 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑣 Isom < , < ((1...(♯‘𝑤)), 𝑤)) → 𝑣 ∈ 𝐴) | 
| 79 | 5 | a1i 11 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → 𝐹 = (𝑧 ∈ 𝐴 ↦ ran 𝑧)) | 
| 80 |  | simpr 484 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑣 ∈ 𝐴) ∧ 𝑧 = 𝑣) → 𝑧 = 𝑣) | 
| 81 | 80 | rneqd 5948 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑣 ∈ 𝐴) ∧ 𝑧 = 𝑣) → ran 𝑧 = ran 𝑣) | 
| 82 |  | simpr 484 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → 𝑣 ∈ 𝐴) | 
| 83 |  | rnexg 7925 | . . . . . . . . . . . . . . . . 17
⊢ (𝑣 ∈ 𝐴 → ran 𝑣 ∈ V) | 
| 84 | 82, 83 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → ran 𝑣 ∈ V) | 
| 85 | 79, 81, 82, 84 | fvmptd 7022 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (𝐹‘𝑣) = ran 𝑣) | 
| 86 | 85 | ex 412 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑣 ∈ 𝐴 → (𝐹‘𝑣) = ran 𝑣)) | 
| 87 | 86 | 3ad2ant1 1133 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑣 Isom < , < ((1...(♯‘𝑤)), 𝑤)) → (𝑣 ∈ 𝐴 → (𝐹‘𝑣) = ran 𝑣)) | 
| 88 | 78, 87 | mpd 15 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑣 Isom < , < ((1...(♯‘𝑤)), 𝑤)) → (𝐹‘𝑣) = ran 𝑣) | 
| 89 |  | dff1o2 6852 | . . . . . . . . . . . . . . 15
⊢ (𝑣:(1...𝐾)–1-1-onto→𝑤 ↔ (𝑣 Fn (1...𝐾) ∧ Fun ◡𝑣 ∧ ran 𝑣 = 𝑤)) | 
| 90 | 89 | biimpi 216 | . . . . . . . . . . . . . 14
⊢ (𝑣:(1...𝐾)–1-1-onto→𝑤 → (𝑣 Fn (1...𝐾) ∧ Fun ◡𝑣 ∧ ran 𝑣 = 𝑤)) | 
| 91 | 90 | simp3d 1144 | . . . . . . . . . . . . 13
⊢ (𝑣:(1...𝐾)–1-1-onto→𝑤 → ran 𝑣 = 𝑤) | 
| 92 | 46, 91 | syl 17 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑣 Isom < , < ((1...(♯‘𝑤)), 𝑤)) → ran 𝑣 = 𝑤) | 
| 93 | 88, 92 | eqtrd 2776 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑣 Isom < , < ((1...(♯‘𝑤)), 𝑤)) → (𝐹‘𝑣) = 𝑤) | 
| 94 | 93 | eqcomd 2742 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑣 Isom < , < ((1...(♯‘𝑤)), 𝑤)) → 𝑤 = (𝐹‘𝑣)) | 
| 95 | 78, 94 | jca 511 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑣 Isom < , < ((1...(♯‘𝑤)), 𝑤)) → (𝑣 ∈ 𝐴 ∧ 𝑤 = (𝐹‘𝑣))) | 
| 96 | 95 | 3expa 1118 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐵) ∧ 𝑣 Isom < , < ((1...(♯‘𝑤)), 𝑤)) → (𝑣 ∈ 𝐴 ∧ 𝑤 = (𝐹‘𝑣))) | 
| 97 | 96 | ex 412 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵) → (𝑣 Isom < , < ((1...(♯‘𝑤)), 𝑤) → (𝑣 ∈ 𝐴 ∧ 𝑤 = (𝐹‘𝑣)))) | 
| 98 | 97 | eximdv 1916 | . . . . . 6
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵) → (∃𝑣 𝑣 Isom < , < ((1...(♯‘𝑤)), 𝑤) → ∃𝑣(𝑣 ∈ 𝐴 ∧ 𝑤 = (𝐹‘𝑣)))) | 
| 99 | 35, 98 | mpd 15 | . . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵) → ∃𝑣(𝑣 ∈ 𝐴 ∧ 𝑤 = (𝐹‘𝑣))) | 
| 100 |  | df-rex 3070 | . . . . 5
⊢
(∃𝑣 ∈
𝐴 𝑤 = (𝐹‘𝑣) ↔ ∃𝑣(𝑣 ∈ 𝐴 ∧ 𝑤 = (𝐹‘𝑣))) | 
| 101 | 99, 100 | sylibr 234 | . . . 4
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵) → ∃𝑣 ∈ 𝐴 𝑤 = (𝐹‘𝑣)) | 
| 102 | 101 | ralrimiva 3145 | . . 3
⊢ (𝜑 → ∀𝑤 ∈ 𝐵 ∃𝑣 ∈ 𝐴 𝑤 = (𝐹‘𝑣)) | 
| 103 | 10, 102 | jca 511 | . 2
⊢ (𝜑 → (𝐹:𝐴⟶𝐵 ∧ ∀𝑤 ∈ 𝐵 ∃𝑣 ∈ 𝐴 𝑤 = (𝐹‘𝑣))) | 
| 104 |  | dffo3 7121 | . . 3
⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑤 ∈ 𝐵 ∃𝑣 ∈ 𝐴 𝑤 = (𝐹‘𝑣))) | 
| 105 | 104 | a1i 11 | . 2
⊢ (𝜑 → (𝐹:𝐴–onto→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑤 ∈ 𝐵 ∃𝑣 ∈ 𝐴 𝑤 = (𝐹‘𝑣)))) | 
| 106 | 103, 105 | mpbird 257 | 1
⊢ (𝜑 → 𝐹:𝐴–onto→𝐵) |