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 40103 |
. . . 4
⊢ (𝜑 → 𝐹:𝐴–1-1→𝐵) |
7 | | df-f1 6438 |
. . . . . 6
⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹)) |
8 | 7 | biimpi 215 |
. . . . 5
⊢ (𝐹:𝐴–1-1→𝐵 → (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹)) |
9 | 8 | simpld 495 |
. . . 4
⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴⟶𝐵) |
10 | 6, 9 | syl 17 |
. . 3
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) |
11 | 3 | eleq2i 2830 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑤 ∈ 𝐵 ↔ 𝑤 ∈ {𝑎 ∈ 𝒫 (1...𝑁) ∣ (♯‘𝑎) = 𝐾}) |
12 | 11 | biimpi 215 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤 ∈ 𝐵 → 𝑤 ∈ {𝑎 ∈ 𝒫 (1...𝑁) ∣ (♯‘𝑎) = 𝐾}) |
13 | 12 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵) → 𝑤 ∈ {𝑎 ∈ 𝒫 (1...𝑁) ∣ (♯‘𝑎) = 𝐾}) |
14 | | fveqeq2 6783 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑎 = 𝑤 → ((♯‘𝑎) = 𝐾 ↔ (♯‘𝑤) = 𝐾)) |
15 | 14 | elrab 3624 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 ∈ {𝑎 ∈ 𝒫 (1...𝑁) ∣ (♯‘𝑎) = 𝐾} ↔ (𝑤 ∈ 𝒫 (1...𝑁) ∧ (♯‘𝑤) = 𝐾)) |
16 | 13, 15 | sylib 217 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵) → (𝑤 ∈ 𝒫 (1...𝑁) ∧ (♯‘𝑤) = 𝐾)) |
17 | 16 | simpld 495 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵) → 𝑤 ∈ 𝒫 (1...𝑁)) |
18 | 17 | elpwid 4544 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵) → 𝑤 ⊆ (1...𝑁)) |
19 | 18 | sseld 3920 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵) → (𝑐 ∈ 𝑤 → 𝑐 ∈ (1...𝑁))) |
20 | 19 | imp 407 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐵) ∧ 𝑐 ∈ 𝑤) → 𝑐 ∈ (1...𝑁)) |
21 | 20 | 3impa 1109 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑐 ∈ 𝑤) → 𝑐 ∈ (1...𝑁)) |
22 | | elfznn 13285 |
. . . . . . . . . . . . 13
⊢ (𝑐 ∈ (1...𝑁) → 𝑐 ∈ ℕ) |
23 | 21, 22 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑐 ∈ 𝑤) → 𝑐 ∈ ℕ) |
24 | 23 | nnred 11988 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑐 ∈ 𝑤) → 𝑐 ∈ ℝ) |
25 | 24 | 3expa 1117 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐵) ∧ 𝑐 ∈ 𝑤) → 𝑐 ∈ ℝ) |
26 | 25 | ex 413 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵) → (𝑐 ∈ 𝑤 → 𝑐 ∈ ℝ)) |
27 | 26 | ssrdv 3927 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵) → 𝑤 ⊆ ℝ) |
28 | | ltso 11055 |
. . . . . . . . 9
⊢ < Or
ℝ |
29 | | soss 5523 |
. . . . . . . . 9
⊢ (𝑤 ⊆ ℝ → ( <
Or ℝ → < Or 𝑤)) |
30 | 28, 29 | mpi 20 |
. . . . . . . 8
⊢ (𝑤 ⊆ ℝ → < Or
𝑤) |
31 | 27, 30 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵) → < Or 𝑤) |
32 | | fzfid 13693 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵) → (1...𝑁) ∈ Fin) |
33 | 32, 18 | ssfid 9042 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵) → 𝑤 ∈ Fin) |
34 | | fz1iso 14176 |
. . . . . . 7
⊢ (( <
Or 𝑤 ∧ 𝑤 ∈ Fin) → ∃𝑣 𝑣 Isom < , < ((1...(♯‘𝑤)), 𝑤)) |
35 | 31, 33, 34 | syl2anc 584 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵) → ∃𝑣 𝑣 Isom < , < ((1...(♯‘𝑤)), 𝑤)) |
36 | | df-isom 6442 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑣 Isom < , <
((1...(♯‘𝑤)),
𝑤) ↔ (𝑣:(1...(♯‘𝑤))–1-1-onto→𝑤 ∧ ∀𝑥 ∈
(1...(♯‘𝑤))∀𝑦 ∈ (1...(♯‘𝑤))(𝑥 < 𝑦 ↔ (𝑣‘𝑥) < (𝑣‘𝑦)))) |
37 | 36 | biimpi 215 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑣 Isom < , <
((1...(♯‘𝑤)),
𝑤) → (𝑣:(1...(♯‘𝑤))–1-1-onto→𝑤 ∧ ∀𝑥 ∈
(1...(♯‘𝑤))∀𝑦 ∈ (1...(♯‘𝑤))(𝑥 < 𝑦 ↔ (𝑣‘𝑥) < (𝑣‘𝑦)))) |
38 | 37 | 3ad2ant3 1134 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑣 Isom < , < ((1...(♯‘𝑤)), 𝑤)) → (𝑣:(1...(♯‘𝑤))–1-1-onto→𝑤 ∧ ∀𝑥 ∈
(1...(♯‘𝑤))∀𝑦 ∈ (1...(♯‘𝑤))(𝑥 < 𝑦 ↔ (𝑣‘𝑥) < (𝑣‘𝑦)))) |
39 | 38 | simpld 495 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑣 Isom < , < ((1...(♯‘𝑤)), 𝑤)) → 𝑣:(1...(♯‘𝑤))–1-1-onto→𝑤) |
40 | 16 | simprd 496 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵) → (♯‘𝑤) = 𝐾) |
41 | | oveq2 7283 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((♯‘𝑤) =
𝐾 →
(1...(♯‘𝑤)) =
(1...𝐾)) |
42 | 41 | f1oeq2d 6712 |
. . . . . . . . . . . . . . . . . . 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 228 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵) → (𝑣:(1...(♯‘𝑤))–1-1-onto→𝑤 → 𝑣:(1...𝐾)–1-1-onto→𝑤)) |
45 | 44 | 3adant3 1131 |
. . . . . . . . . . . . . . . 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 6716 |
. . . . . . . . . . . . . . 15
⊢ (𝑣:(1...𝐾)–1-1-onto→𝑤 → 𝑣:(1...𝐾)⟶𝑤) |
48 | 46, 47 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑣 Isom < , < ((1...(♯‘𝑤)), 𝑤)) → 𝑣:(1...𝐾)⟶𝑤) |
49 | 48 | ffnd 6601 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑣 Isom < , < ((1...(♯‘𝑤)), 𝑤)) → 𝑣 Fn (1...𝐾)) |
50 | | ovexd 7310 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑣 Isom < , < ((1...(♯‘𝑤)), 𝑤)) → (1...𝐾) ∈ V) |
51 | 49, 50 | fnexd 7094 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑣 Isom < , < ((1...(♯‘𝑤)), 𝑤)) → 𝑣 ∈ V) |
52 | 18 | 3adant3 1131 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑣 Isom < , < ((1...(♯‘𝑤)), 𝑤)) → 𝑤 ⊆ (1...𝑁)) |
53 | | fss 6617 |
. . . . . . . . . . . . . 14
⊢ ((𝑣:(1...𝐾)⟶𝑤 ∧ 𝑤 ⊆ (1...𝑁)) → 𝑣:(1...𝐾)⟶(1...𝑁)) |
54 | 48, 52, 53 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑣 Isom < , < ((1...(♯‘𝑤)), 𝑤)) → 𝑣:(1...𝐾)⟶(1...𝑁)) |
55 | 38 | simprd 496 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑣 Isom < , < ((1...(♯‘𝑤)), 𝑤)) → ∀𝑥 ∈ (1...(♯‘𝑤))∀𝑦 ∈ (1...(♯‘𝑤))(𝑥 < 𝑦 ↔ (𝑣‘𝑥) < (𝑣‘𝑦))) |
56 | | biimp 214 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 < 𝑦 ↔ (𝑣‘𝑥) < (𝑣‘𝑦)) → (𝑥 < 𝑦 → (𝑣‘𝑥) < (𝑣‘𝑦))) |
57 | 56 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑣 Isom < , < ((1...(♯‘𝑤)), 𝑤)) ∧ 𝑥 ∈ (1...(♯‘𝑤))) ∧ 𝑦 ∈ (1...(♯‘𝑤))) → ((𝑥 < 𝑦 ↔ (𝑣‘𝑥) < (𝑣‘𝑦)) → (𝑥 < 𝑦 → (𝑣‘𝑥) < (𝑣‘𝑦)))) |
58 | 57 | ralimdva 3108 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑣 Isom < , < ((1...(♯‘𝑤)), 𝑤)) ∧ 𝑥 ∈ (1...(♯‘𝑤))) → (∀𝑦 ∈
(1...(♯‘𝑤))(𝑥 < 𝑦 ↔ (𝑣‘𝑥) < (𝑣‘𝑦)) → ∀𝑦 ∈ (1...(♯‘𝑤))(𝑥 < 𝑦 → (𝑣‘𝑥) < (𝑣‘𝑦)))) |
59 | 58 | ralimdva 3108 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑣 Isom < , < ((1...(♯‘𝑤)), 𝑤)) → (∀𝑥 ∈ (1...(♯‘𝑤))∀𝑦 ∈ (1...(♯‘𝑤))(𝑥 < 𝑦 ↔ (𝑣‘𝑥) < (𝑣‘𝑦)) → ∀𝑥 ∈ (1...(♯‘𝑤))∀𝑦 ∈ (1...(♯‘𝑤))(𝑥 < 𝑦 → (𝑣‘𝑥) < (𝑣‘𝑦)))) |
60 | 55, 59 | mpd 15 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑣 Isom < , < ((1...(♯‘𝑤)), 𝑤)) → ∀𝑥 ∈ (1...(♯‘𝑤))∀𝑦 ∈ (1...(♯‘𝑤))(𝑥 < 𝑦 → (𝑣‘𝑥) < (𝑣‘𝑦))) |
61 | 40 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐵) ∧ 𝑣 Isom < , < ((1...(♯‘𝑤)), 𝑤)) → (♯‘𝑤) = 𝐾) |
62 | 61 | 3impa 1109 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑣 Isom < , < ((1...(♯‘𝑤)), 𝑤)) → (♯‘𝑤) = 𝐾) |
63 | 62 | oveq2d 7291 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑣 Isom < , < ((1...(♯‘𝑤)), 𝑤)) → (1...(♯‘𝑤)) = (1...𝐾)) |
64 | 63 | raleqdv 3348 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑣 Isom < , < ((1...(♯‘𝑤)), 𝑤)) → (∀𝑦 ∈ (1...(♯‘𝑤))(𝑥 < 𝑦 → (𝑣‘𝑥) < (𝑣‘𝑦)) ↔ ∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑣‘𝑥) < (𝑣‘𝑦)))) |
65 | 64 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑣 Isom < , < ((1...(♯‘𝑤)), 𝑤)) ∧ 𝑥 ∈ (1...(♯‘𝑤))) → (∀𝑦 ∈
(1...(♯‘𝑤))(𝑥 < 𝑦 → (𝑣‘𝑥) < (𝑣‘𝑦)) ↔ ∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑣‘𝑥) < (𝑣‘𝑦)))) |
66 | 63, 65 | raleqbidva 3354 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑣 Isom < , < ((1...(♯‘𝑤)), 𝑤)) → (∀𝑥 ∈ (1...(♯‘𝑤))∀𝑦 ∈ (1...(♯‘𝑤))(𝑥 < 𝑦 → (𝑣‘𝑥) < (𝑣‘𝑦)) ↔ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑣‘𝑥) < (𝑣‘𝑦)))) |
67 | 60, 66 | mpbid 231 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑣 Isom < , < ((1...(♯‘𝑤)), 𝑤)) → ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑣‘𝑥) < (𝑣‘𝑦))) |
68 | 54, 67 | jca 512 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑣 Isom < , < ((1...(♯‘𝑤)), 𝑤)) → (𝑣:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑣‘𝑥) < (𝑣‘𝑦)))) |
69 | | feq1 6581 |
. . . . . . . . . . . . 13
⊢ (𝑓 = 𝑣 → (𝑓:(1...𝐾)⟶(1...𝑁) ↔ 𝑣:(1...𝐾)⟶(1...𝑁))) |
70 | | fveq1 6773 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 = 𝑣 → (𝑓‘𝑥) = (𝑣‘𝑥)) |
71 | | fveq1 6773 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 = 𝑣 → (𝑓‘𝑦) = (𝑣‘𝑦)) |
72 | 70, 71 | breq12d 5087 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 = 𝑣 → ((𝑓‘𝑥) < (𝑓‘𝑦) ↔ (𝑣‘𝑥) < (𝑣‘𝑦))) |
73 | 72 | imbi2d 341 |
. . . . . . . . . . . . . 14
⊢ (𝑓 = 𝑣 → ((𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)) ↔ (𝑥 < 𝑦 → (𝑣‘𝑥) < (𝑣‘𝑦)))) |
74 | 73 | 2ralbidv 3129 |
. . . . . . . . . . . . 13
⊢ (𝑓 = 𝑣 → (∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)) ↔ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑣‘𝑥) < (𝑣‘𝑦)))) |
75 | 69, 74 | anbi12d 631 |
. . . . . . . . . . . 12
⊢ (𝑓 = 𝑣 → ((𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦))) ↔ (𝑣:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑣‘𝑥) < (𝑣‘𝑦))))) |
76 | 51, 68, 75 | elabd 3612 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑣 Isom < , < ((1...(♯‘𝑤)), 𝑤)) → 𝑣 ∈ {𝑓 ∣ (𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))}) |
77 | 4 | eleq2i 2830 |
. . . . . . . . . . 11
⊢ (𝑣 ∈ 𝐴 ↔ 𝑣 ∈ {𝑓 ∣ (𝑓:(1...𝐾)⟶(1...𝑁) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))}) |
78 | 76, 77 | sylibr 233 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑣 Isom < , < ((1...(♯‘𝑤)), 𝑤)) → 𝑣 ∈ 𝐴) |
79 | 5 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → 𝐹 = (𝑧 ∈ 𝐴 ↦ ran 𝑧)) |
80 | | simpr 485 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑣 ∈ 𝐴) ∧ 𝑧 = 𝑣) → 𝑧 = 𝑣) |
81 | 80 | rneqd 5847 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑣 ∈ 𝐴) ∧ 𝑧 = 𝑣) → ran 𝑧 = ran 𝑣) |
82 | | simpr 485 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → 𝑣 ∈ 𝐴) |
83 | | rnexg 7751 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑣 ∈ 𝐴 → ran 𝑣 ∈ V) |
84 | 82, 83 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → ran 𝑣 ∈ V) |
85 | 79, 81, 82, 84 | fvmptd 6882 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (𝐹‘𝑣) = ran 𝑣) |
86 | 85 | ex 413 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑣 ∈ 𝐴 → (𝐹‘𝑣) = ran 𝑣)) |
87 | 86 | 3ad2ant1 1132 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑣 Isom < , < ((1...(♯‘𝑤)), 𝑤)) → (𝑣 ∈ 𝐴 → (𝐹‘𝑣) = ran 𝑣)) |
88 | 78, 87 | mpd 15 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑣 Isom < , < ((1...(♯‘𝑤)), 𝑤)) → (𝐹‘𝑣) = ran 𝑣) |
89 | | dff1o2 6721 |
. . . . . . . . . . . . . . 15
⊢ (𝑣:(1...𝐾)–1-1-onto→𝑤 ↔ (𝑣 Fn (1...𝐾) ∧ Fun ◡𝑣 ∧ ran 𝑣 = 𝑤)) |
90 | 89 | biimpi 215 |
. . . . . . . . . . . . . 14
⊢ (𝑣:(1...𝐾)–1-1-onto→𝑤 → (𝑣 Fn (1...𝐾) ∧ Fun ◡𝑣 ∧ ran 𝑣 = 𝑤)) |
91 | 90 | simp3d 1143 |
. . . . . . . . . . . . 13
⊢ (𝑣:(1...𝐾)–1-1-onto→𝑤 → ran 𝑣 = 𝑤) |
92 | 46, 91 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑣 Isom < , < ((1...(♯‘𝑤)), 𝑤)) → ran 𝑣 = 𝑤) |
93 | 88, 92 | eqtrd 2778 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑣 Isom < , < ((1...(♯‘𝑤)), 𝑤)) → (𝐹‘𝑣) = 𝑤) |
94 | 93 | eqcomd 2744 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑣 Isom < , < ((1...(♯‘𝑤)), 𝑤)) → 𝑤 = (𝐹‘𝑣)) |
95 | 78, 94 | jca 512 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵 ∧ 𝑣 Isom < , < ((1...(♯‘𝑤)), 𝑤)) → (𝑣 ∈ 𝐴 ∧ 𝑤 = (𝐹‘𝑣))) |
96 | 95 | 3expa 1117 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑤 ∈ 𝐵) ∧ 𝑣 Isom < , < ((1...(♯‘𝑤)), 𝑤)) → (𝑣 ∈ 𝐴 ∧ 𝑤 = (𝐹‘𝑣))) |
97 | 96 | ex 413 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵) → (𝑣 Isom < , < ((1...(♯‘𝑤)), 𝑤) → (𝑣 ∈ 𝐴 ∧ 𝑤 = (𝐹‘𝑣)))) |
98 | 97 | eximdv 1920 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵) → (∃𝑣 𝑣 Isom < , < ((1...(♯‘𝑤)), 𝑤) → ∃𝑣(𝑣 ∈ 𝐴 ∧ 𝑤 = (𝐹‘𝑣)))) |
99 | 35, 98 | mpd 15 |
. . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵) → ∃𝑣(𝑣 ∈ 𝐴 ∧ 𝑤 = (𝐹‘𝑣))) |
100 | | df-rex 3070 |
. . . . 5
⊢
(∃𝑣 ∈
𝐴 𝑤 = (𝐹‘𝑣) ↔ ∃𝑣(𝑣 ∈ 𝐴 ∧ 𝑤 = (𝐹‘𝑣))) |
101 | 99, 100 | sylibr 233 |
. . . 4
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐵) → ∃𝑣 ∈ 𝐴 𝑤 = (𝐹‘𝑣)) |
102 | 101 | ralrimiva 3103 |
. . 3
⊢ (𝜑 → ∀𝑤 ∈ 𝐵 ∃𝑣 ∈ 𝐴 𝑤 = (𝐹‘𝑣)) |
103 | 10, 102 | jca 512 |
. 2
⊢ (𝜑 → (𝐹:𝐴⟶𝐵 ∧ ∀𝑤 ∈ 𝐵 ∃𝑣 ∈ 𝐴 𝑤 = (𝐹‘𝑣))) |
104 | | dffo3 6978 |
. . 3
⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑤 ∈ 𝐵 ∃𝑣 ∈ 𝐴 𝑤 = (𝐹‘𝑣))) |
105 | 104 | a1i 11 |
. 2
⊢ (𝜑 → (𝐹:𝐴–onto→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑤 ∈ 𝐵 ∃𝑣 ∈ 𝐴 𝑤 = (𝐹‘𝑣)))) |
106 | 103, 105 | mpbird 256 |
1
⊢ (𝜑 → 𝐹:𝐴–onto→𝐵) |