Step | Hyp | Ref
| Expression |
1 | | simp1 1134 |
. . . . 5
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑋 ≠ 𝑌) → 𝑋 ∈ 𝐴) |
2 | | simp2 1135 |
. . . . 5
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑋 ≠ 𝑌) → 𝑌 ∈ 𝐴) |
3 | | fvconst 7023 |
. . . . . . . 8
⊢ ((𝐹:𝐴⟶{𝐵} ∧ 𝑋 ∈ 𝐴) → (𝐹‘𝑋) = 𝐵) |
4 | 1, 3 | sylan2 592 |
. . . . . . 7
⊢ ((𝐹:𝐴⟶{𝐵} ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑋 ≠ 𝑌)) → (𝐹‘𝑋) = 𝐵) |
5 | | fvconst 7023 |
. . . . . . . 8
⊢ ((𝐹:𝐴⟶{𝐵} ∧ 𝑌 ∈ 𝐴) → (𝐹‘𝑌) = 𝐵) |
6 | 2, 5 | sylan2 592 |
. . . . . . 7
⊢ ((𝐹:𝐴⟶{𝐵} ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑋 ≠ 𝑌)) → (𝐹‘𝑌) = 𝐵) |
7 | 4, 6 | eqtr4d 2780 |
. . . . . 6
⊢ ((𝐹:𝐴⟶{𝐵} ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑋 ≠ 𝑌)) → (𝐹‘𝑋) = (𝐹‘𝑌)) |
8 | | neneq 2947 |
. . . . . . . 8
⊢ (𝑋 ≠ 𝑌 → ¬ 𝑋 = 𝑌) |
9 | 8 | 3ad2ant3 1133 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑋 ≠ 𝑌) → ¬ 𝑋 = 𝑌) |
10 | 9 | adantl 481 |
. . . . . 6
⊢ ((𝐹:𝐴⟶{𝐵} ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑋 ≠ 𝑌)) → ¬ 𝑋 = 𝑌) |
11 | 7, 10 | jcnd 163 |
. . . . 5
⊢ ((𝐹:𝐴⟶{𝐵} ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑋 ≠ 𝑌)) → ¬ ((𝐹‘𝑋) = (𝐹‘𝑌) → 𝑋 = 𝑌)) |
12 | | fveqeq2 6770 |
. . . . . . . 8
⊢ (𝑥 = 𝑋 → ((𝐹‘𝑥) = (𝐹‘𝑦) ↔ (𝐹‘𝑋) = (𝐹‘𝑦))) |
13 | | eqeq1 2741 |
. . . . . . . 8
⊢ (𝑥 = 𝑋 → (𝑥 = 𝑦 ↔ 𝑋 = 𝑦)) |
14 | 12, 13 | imbi12d 344 |
. . . . . . 7
⊢ (𝑥 = 𝑋 → (((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦) ↔ ((𝐹‘𝑋) = (𝐹‘𝑦) → 𝑋 = 𝑦))) |
15 | 14 | notbid 317 |
. . . . . 6
⊢ (𝑥 = 𝑋 → (¬ ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦) ↔ ¬ ((𝐹‘𝑋) = (𝐹‘𝑦) → 𝑋 = 𝑦))) |
16 | | fveq2 6761 |
. . . . . . . . 9
⊢ (𝑦 = 𝑌 → (𝐹‘𝑦) = (𝐹‘𝑌)) |
17 | 16 | eqeq2d 2748 |
. . . . . . . 8
⊢ (𝑦 = 𝑌 → ((𝐹‘𝑋) = (𝐹‘𝑦) ↔ (𝐹‘𝑋) = (𝐹‘𝑌))) |
18 | | eqeq2 2749 |
. . . . . . . 8
⊢ (𝑦 = 𝑌 → (𝑋 = 𝑦 ↔ 𝑋 = 𝑌)) |
19 | 17, 18 | imbi12d 344 |
. . . . . . 7
⊢ (𝑦 = 𝑌 → (((𝐹‘𝑋) = (𝐹‘𝑦) → 𝑋 = 𝑦) ↔ ((𝐹‘𝑋) = (𝐹‘𝑌) → 𝑋 = 𝑌))) |
20 | 19 | notbid 317 |
. . . . . 6
⊢ (𝑦 = 𝑌 → (¬ ((𝐹‘𝑋) = (𝐹‘𝑦) → 𝑋 = 𝑦) ↔ ¬ ((𝐹‘𝑋) = (𝐹‘𝑌) → 𝑋 = 𝑌))) |
21 | 15, 20 | rspc2ev 3569 |
. . . . 5
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ ¬ ((𝐹‘𝑋) = (𝐹‘𝑌) → 𝑋 = 𝑌)) → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ¬ ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)) |
22 | 1, 2, 11, 21 | syl2an23an 1421 |
. . . 4
⊢ ((𝐹:𝐴⟶{𝐵} ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑋 ≠ 𝑌)) → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ¬ ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)) |
23 | | rexnal2 3185 |
. . . 4
⊢
(∃𝑥 ∈
𝐴 ∃𝑦 ∈ 𝐴 ¬ ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦) ↔ ¬ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)) |
24 | 22, 23 | sylib 217 |
. . 3
⊢ ((𝐹:𝐴⟶{𝐵} ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑋 ≠ 𝑌)) → ¬ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)) |
25 | 24 | olcd 870 |
. 2
⊢ ((𝐹:𝐴⟶{𝐵} ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑋 ≠ 𝑌)) → (¬ 𝐹:𝐴⟶𝐶 ∨ ¬ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))) |
26 | | ianor 978 |
. . 3
⊢ (¬
(𝐹:𝐴⟶𝐶 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)) ↔ (¬ 𝐹:𝐴⟶𝐶 ∨ ¬ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))) |
27 | | dff13 7114 |
. . 3
⊢ (𝐹:𝐴–1-1→𝐶 ↔ (𝐹:𝐴⟶𝐶 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))) |
28 | 26, 27 | xchnxbir 332 |
. 2
⊢ (¬
𝐹:𝐴–1-1→𝐶 ↔ (¬ 𝐹:𝐴⟶𝐶 ∨ ¬ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))) |
29 | 25, 28 | sylibr 233 |
1
⊢ ((𝐹:𝐴⟶{𝐵} ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑋 ≠ 𝑌)) → ¬ 𝐹:𝐴–1-1→𝐶) |