Proof of Theorem 2f1fvneq
Step | Hyp | Ref
| Expression |
1 | | f1veqaeq 6418 |
. . . . 5
⊢ ((𝐹:𝐶–1-1→𝐷 ∧ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶)) → ((𝐹‘𝐴) = (𝐹‘𝐵) → 𝐴 = 𝐵)) |
2 | 1 | adantll 746 |
. . . 4
⊢ (((𝐸:𝐷–1-1→𝑅 ∧ 𝐹:𝐶–1-1→𝐷) ∧ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶)) → ((𝐹‘𝐴) = (𝐹‘𝐵) → 𝐴 = 𝐵)) |
3 | 2 | necon3ad 2795 |
. . 3
⊢ (((𝐸:𝐷–1-1→𝑅 ∧ 𝐹:𝐶–1-1→𝐷) ∧ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶)) → (𝐴 ≠ 𝐵 → ¬ (𝐹‘𝐴) = (𝐹‘𝐵))) |
4 | 3 | 3impia 1253 |
. 2
⊢ (((𝐸:𝐷–1-1→𝑅 ∧ 𝐹:𝐶–1-1→𝐷) ∧ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) ∧ 𝐴 ≠ 𝐵) → ¬ (𝐹‘𝐴) = (𝐹‘𝐵)) |
5 | | simpll 786 |
. . . . . . 7
⊢ (((𝐸:𝐷–1-1→𝑅 ∧ 𝐹:𝐶–1-1→𝐷) ∧ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶)) → 𝐸:𝐷–1-1→𝑅) |
6 | | f1f 6014 |
. . . . . . . . . 10
⊢ (𝐹:𝐶–1-1→𝐷 → 𝐹:𝐶⟶𝐷) |
7 | | ffvelrn 6265 |
. . . . . . . . . . . 12
⊢ ((𝐹:𝐶⟶𝐷 ∧ 𝐴 ∈ 𝐶) → (𝐹‘𝐴) ∈ 𝐷) |
8 | | ffvelrn 6265 |
. . . . . . . . . . . 12
⊢ ((𝐹:𝐶⟶𝐷 ∧ 𝐵 ∈ 𝐶) → (𝐹‘𝐵) ∈ 𝐷) |
9 | 7, 8 | anim12dan 878 |
. . . . . . . . . . 11
⊢ ((𝐹:𝐶⟶𝐷 ∧ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶)) → ((𝐹‘𝐴) ∈ 𝐷 ∧ (𝐹‘𝐵) ∈ 𝐷)) |
10 | 9 | ex 449 |
. . . . . . . . . 10
⊢ (𝐹:𝐶⟶𝐷 → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → ((𝐹‘𝐴) ∈ 𝐷 ∧ (𝐹‘𝐵) ∈ 𝐷))) |
11 | 6, 10 | syl 17 |
. . . . . . . . 9
⊢ (𝐹:𝐶–1-1→𝐷 → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → ((𝐹‘𝐴) ∈ 𝐷 ∧ (𝐹‘𝐵) ∈ 𝐷))) |
12 | 11 | adantl 481 |
. . . . . . . 8
⊢ ((𝐸:𝐷–1-1→𝑅 ∧ 𝐹:𝐶–1-1→𝐷) → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → ((𝐹‘𝐴) ∈ 𝐷 ∧ (𝐹‘𝐵) ∈ 𝐷))) |
13 | 12 | imp 444 |
. . . . . . 7
⊢ (((𝐸:𝐷–1-1→𝑅 ∧ 𝐹:𝐶–1-1→𝐷) ∧ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶)) → ((𝐹‘𝐴) ∈ 𝐷 ∧ (𝐹‘𝐵) ∈ 𝐷)) |
14 | | f1veqaeq 6418 |
. . . . . . 7
⊢ ((𝐸:𝐷–1-1→𝑅 ∧ ((𝐹‘𝐴) ∈ 𝐷 ∧ (𝐹‘𝐵) ∈ 𝐷)) → ((𝐸‘(𝐹‘𝐴)) = (𝐸‘(𝐹‘𝐵)) → (𝐹‘𝐴) = (𝐹‘𝐵))) |
15 | 5, 13, 14 | syl2anc 691 |
. . . . . 6
⊢ (((𝐸:𝐷–1-1→𝑅 ∧ 𝐹:𝐶–1-1→𝐷) ∧ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶)) → ((𝐸‘(𝐹‘𝐴)) = (𝐸‘(𝐹‘𝐵)) → (𝐹‘𝐴) = (𝐹‘𝐵))) |
16 | 15 | con3dimp 456 |
. . . . 5
⊢ ((((𝐸:𝐷–1-1→𝑅 ∧ 𝐹:𝐶–1-1→𝐷) ∧ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶)) ∧ ¬ (𝐹‘𝐴) = (𝐹‘𝐵)) → ¬ (𝐸‘(𝐹‘𝐴)) = (𝐸‘(𝐹‘𝐵))) |
17 | | eqeq12 2623 |
. . . . . . 7
⊢ (((𝐸‘(𝐹‘𝐴)) = 𝑋 ∧ (𝐸‘(𝐹‘𝐵)) = 𝑌) → ((𝐸‘(𝐹‘𝐴)) = (𝐸‘(𝐹‘𝐵)) ↔ 𝑋 = 𝑌)) |
18 | 17 | notbid 307 |
. . . . . 6
⊢ (((𝐸‘(𝐹‘𝐴)) = 𝑋 ∧ (𝐸‘(𝐹‘𝐵)) = 𝑌) → (¬ (𝐸‘(𝐹‘𝐴)) = (𝐸‘(𝐹‘𝐵)) ↔ ¬ 𝑋 = 𝑌)) |
19 | | df-ne 2782 |
. . . . . . 7
⊢ (𝑋 ≠ 𝑌 ↔ ¬ 𝑋 = 𝑌) |
20 | 19 | biimpri 217 |
. . . . . 6
⊢ (¬
𝑋 = 𝑌 → 𝑋 ≠ 𝑌) |
21 | 18, 20 | syl6bi 242 |
. . . . 5
⊢ (((𝐸‘(𝐹‘𝐴)) = 𝑋 ∧ (𝐸‘(𝐹‘𝐵)) = 𝑌) → (¬ (𝐸‘(𝐹‘𝐴)) = (𝐸‘(𝐹‘𝐵)) → 𝑋 ≠ 𝑌)) |
22 | 16, 21 | syl5com 31 |
. . . 4
⊢ ((((𝐸:𝐷–1-1→𝑅 ∧ 𝐹:𝐶–1-1→𝐷) ∧ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶)) ∧ ¬ (𝐹‘𝐴) = (𝐹‘𝐵)) → (((𝐸‘(𝐹‘𝐴)) = 𝑋 ∧ (𝐸‘(𝐹‘𝐵)) = 𝑌) → 𝑋 ≠ 𝑌)) |
23 | 22 | ex 449 |
. . 3
⊢ (((𝐸:𝐷–1-1→𝑅 ∧ 𝐹:𝐶–1-1→𝐷) ∧ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶)) → (¬ (𝐹‘𝐴) = (𝐹‘𝐵) → (((𝐸‘(𝐹‘𝐴)) = 𝑋 ∧ (𝐸‘(𝐹‘𝐵)) = 𝑌) → 𝑋 ≠ 𝑌))) |
24 | 23 | 3adant3 1074 |
. 2
⊢ (((𝐸:𝐷–1-1→𝑅 ∧ 𝐹:𝐶–1-1→𝐷) ∧ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) ∧ 𝐴 ≠ 𝐵) → (¬ (𝐹‘𝐴) = (𝐹‘𝐵) → (((𝐸‘(𝐹‘𝐴)) = 𝑋 ∧ (𝐸‘(𝐹‘𝐵)) = 𝑌) → 𝑋 ≠ 𝑌))) |
25 | 4, 24 | mpd 15 |
1
⊢ (((𝐸:𝐷–1-1→𝑅 ∧ 𝐹:𝐶–1-1→𝐷) ∧ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) ∧ 𝐴 ≠ 𝐵) → (((𝐸‘(𝐹‘𝐴)) = 𝑋 ∧ (𝐸‘(𝐹‘𝐵)) = 𝑌) → 𝑋 ≠ 𝑌)) |