| Step | Hyp | Ref
| Expression |
| 1 | | hashnexinj.4 |
. . 3
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) |
| 2 | | hashnexinj.3 |
. . . . . . . . 9
⊢ (𝜑 → (♯‘𝐵) < (♯‘𝐴)) |
| 3 | | hashnexinj.2 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐵 ∈ Fin) |
| 4 | | hashcl 14395 |
. . . . . . . . . . . 12
⊢ (𝐵 ∈ Fin →
(♯‘𝐵) ∈
ℕ0) |
| 5 | 3, 4 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (♯‘𝐵) ∈
ℕ0) |
| 6 | 5 | nn0red 12588 |
. . . . . . . . . 10
⊢ (𝜑 → (♯‘𝐵) ∈
ℝ) |
| 7 | | hashnexinj.1 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ∈ Fin) |
| 8 | | hashcl 14395 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ Fin →
(♯‘𝐴) ∈
ℕ0) |
| 9 | 7, 8 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (♯‘𝐴) ∈
ℕ0) |
| 10 | 9 | nn0red 12588 |
. . . . . . . . . 10
⊢ (𝜑 → (♯‘𝐴) ∈
ℝ) |
| 11 | 6, 10 | ltnled 11408 |
. . . . . . . . 9
⊢ (𝜑 → ((♯‘𝐵) < (♯‘𝐴) ↔ ¬
(♯‘𝐴) ≤
(♯‘𝐵))) |
| 12 | 2, 11 | mpbid 232 |
. . . . . . . 8
⊢ (𝜑 → ¬ (♯‘𝐴) ≤ (♯‘𝐵)) |
| 13 | | hashdom 14418 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) →
((♯‘𝐴) ≤
(♯‘𝐵) ↔
𝐴 ≼ 𝐵)) |
| 14 | 7, 3, 13 | syl2anc 584 |
. . . . . . . . . 10
⊢ (𝜑 → ((♯‘𝐴) ≤ (♯‘𝐵) ↔ 𝐴 ≼ 𝐵)) |
| 15 | 14 | notbid 318 |
. . . . . . . . 9
⊢ (𝜑 → (¬
(♯‘𝐴) ≤
(♯‘𝐵) ↔
¬ 𝐴 ≼ 𝐵)) |
| 16 | 15 | biimpd 229 |
. . . . . . . 8
⊢ (𝜑 → (¬
(♯‘𝐴) ≤
(♯‘𝐵) →
¬ 𝐴 ≼ 𝐵)) |
| 17 | 12, 16 | mpd 15 |
. . . . . . 7
⊢ (𝜑 → ¬ 𝐴 ≼ 𝐵) |
| 18 | | brdomg 8997 |
. . . . . . . . . 10
⊢ (𝐵 ∈ Fin → (𝐴 ≼ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1→𝐵)) |
| 19 | 18 | notbid 318 |
. . . . . . . . 9
⊢ (𝐵 ∈ Fin → (¬ 𝐴 ≼ 𝐵 ↔ ¬ ∃𝑓 𝑓:𝐴–1-1→𝐵)) |
| 20 | 19 | biimpd 229 |
. . . . . . . 8
⊢ (𝐵 ∈ Fin → (¬ 𝐴 ≼ 𝐵 → ¬ ∃𝑓 𝑓:𝐴–1-1→𝐵)) |
| 21 | 3, 20 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (¬ 𝐴 ≼ 𝐵 → ¬ ∃𝑓 𝑓:𝐴–1-1→𝐵)) |
| 22 | 17, 21 | mpd 15 |
. . . . . 6
⊢ (𝜑 → ¬ ∃𝑓 𝑓:𝐴–1-1→𝐵) |
| 23 | | alnex 1781 |
. . . . . 6
⊢
(∀𝑓 ¬
𝑓:𝐴–1-1→𝐵 ↔ ¬ ∃𝑓 𝑓:𝐴–1-1→𝐵) |
| 24 | 22, 23 | sylibr 234 |
. . . . 5
⊢ (𝜑 → ∀𝑓 ¬ 𝑓:𝐴–1-1→𝐵) |
| 25 | 3, 7, 1 | elmapdd 8881 |
. . . . . 6
⊢ (𝜑 → 𝐹 ∈ (𝐵 ↑m 𝐴)) |
| 26 | | f1eq1 6799 |
. . . . . . . 8
⊢ (𝑓 = 𝐹 → (𝑓:𝐴–1-1→𝐵 ↔ 𝐹:𝐴–1-1→𝐵)) |
| 27 | 26 | notbid 318 |
. . . . . . 7
⊢ (𝑓 = 𝐹 → (¬ 𝑓:𝐴–1-1→𝐵 ↔ ¬ 𝐹:𝐴–1-1→𝐵)) |
| 28 | 27 | spcgv 3596 |
. . . . . 6
⊢ (𝐹 ∈ (𝐵 ↑m 𝐴) → (∀𝑓 ¬ 𝑓:𝐴–1-1→𝐵 → ¬ 𝐹:𝐴–1-1→𝐵)) |
| 29 | 25, 28 | syl 17 |
. . . . 5
⊢ (𝜑 → (∀𝑓 ¬ 𝑓:𝐴–1-1→𝐵 → ¬ 𝐹:𝐴–1-1→𝐵)) |
| 30 | 24, 29 | mpd 15 |
. . . 4
⊢ (𝜑 → ¬ 𝐹:𝐴–1-1→𝐵) |
| 31 | | dff13 7275 |
. . . . . . . 8
⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))) |
| 32 | | iman 401 |
. . . . . . . . . . . 12
⊢ (((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦) ↔ ¬ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ ¬ 𝑥 = 𝑦)) |
| 33 | | df-ne 2941 |
. . . . . . . . . . . . 13
⊢ (𝑥 ≠ 𝑦 ↔ ¬ 𝑥 = 𝑦) |
| 34 | 33 | anbi2i 623 |
. . . . . . . . . . . 12
⊢ (((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥 ≠ 𝑦) ↔ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ ¬ 𝑥 = 𝑦)) |
| 35 | 32, 34 | xchbinxr 335 |
. . . . . . . . . . 11
⊢ (((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦) ↔ ¬ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥 ≠ 𝑦)) |
| 36 | 35 | 2ralbii 3128 |
. . . . . . . . . 10
⊢
(∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥 ≠ 𝑦)) |
| 37 | | ralnex2 3133 |
. . . . . . . . . 10
⊢
(∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 ¬ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥 ≠ 𝑦) ↔ ¬ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥 ≠ 𝑦)) |
| 38 | 36, 37 | bitri 275 |
. . . . . . . . 9
⊢
(∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦) ↔ ¬ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥 ≠ 𝑦)) |
| 39 | 38 | anbi2i 623 |
. . . . . . . 8
⊢ ((𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)) ↔ (𝐹:𝐴⟶𝐵 ∧ ¬ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥 ≠ 𝑦))) |
| 40 | 31, 39 | bitri 275 |
. . . . . . 7
⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ¬ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥 ≠ 𝑦))) |
| 41 | 40 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ¬ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥 ≠ 𝑦)))) |
| 42 | 41 | notbid 318 |
. . . . 5
⊢ (𝜑 → (¬ 𝐹:𝐴–1-1→𝐵 ↔ ¬ (𝐹:𝐴⟶𝐵 ∧ ¬ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥 ≠ 𝑦)))) |
| 43 | 42 | biimpd 229 |
. . . 4
⊢ (𝜑 → (¬ 𝐹:𝐴–1-1→𝐵 → ¬ (𝐹:𝐴⟶𝐵 ∧ ¬ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥 ≠ 𝑦)))) |
| 44 | 30, 43 | mpd 15 |
. . 3
⊢ (𝜑 → ¬ (𝐹:𝐴⟶𝐵 ∧ ¬ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥 ≠ 𝑦))) |
| 45 | 1, 44 | mpnanrd 409 |
. 2
⊢ (𝜑 → ¬ ¬ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥 ≠ 𝑦)) |
| 46 | 45 | notnotrd 133 |
1
⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥 ≠ 𝑦)) |