Step | Hyp | Ref
| Expression |
1 | | dff12 6614 |
. 2
⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑧∃*𝑥 𝑥𝐹𝑧)) |
2 | | ffn 6545 |
. . . 4
⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴) |
3 | | vex 3412 |
. . . . . . . . . . . . . . 15
⊢ 𝑥 ∈ V |
4 | | vex 3412 |
. . . . . . . . . . . . . . 15
⊢ 𝑧 ∈ V |
5 | 3, 4 | breldm 5777 |
. . . . . . . . . . . . . 14
⊢ (𝑥𝐹𝑧 → 𝑥 ∈ dom 𝐹) |
6 | | fndm 6481 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴) |
7 | 6 | eleq2d 2823 |
. . . . . . . . . . . . . 14
⊢ (𝐹 Fn 𝐴 → (𝑥 ∈ dom 𝐹 ↔ 𝑥 ∈ 𝐴)) |
8 | 5, 7 | syl5ib 247 |
. . . . . . . . . . . . 13
⊢ (𝐹 Fn 𝐴 → (𝑥𝐹𝑧 → 𝑥 ∈ 𝐴)) |
9 | | vex 3412 |
. . . . . . . . . . . . . . 15
⊢ 𝑦 ∈ V |
10 | 9, 4 | breldm 5777 |
. . . . . . . . . . . . . 14
⊢ (𝑦𝐹𝑧 → 𝑦 ∈ dom 𝐹) |
11 | 6 | eleq2d 2823 |
. . . . . . . . . . . . . 14
⊢ (𝐹 Fn 𝐴 → (𝑦 ∈ dom 𝐹 ↔ 𝑦 ∈ 𝐴)) |
12 | 10, 11 | syl5ib 247 |
. . . . . . . . . . . . 13
⊢ (𝐹 Fn 𝐴 → (𝑦𝐹𝑧 → 𝑦 ∈ 𝐴)) |
13 | 8, 12 | anim12d 612 |
. . . . . . . . . . . 12
⊢ (𝐹 Fn 𝐴 → ((𝑥𝐹𝑧 ∧ 𝑦𝐹𝑧) → (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴))) |
14 | 13 | pm4.71rd 566 |
. . . . . . . . . . 11
⊢ (𝐹 Fn 𝐴 → ((𝑥𝐹𝑧 ∧ 𝑦𝐹𝑧) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (𝑥𝐹𝑧 ∧ 𝑦𝐹𝑧)))) |
15 | | eqcom 2744 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = (𝐹‘𝑥) ↔ (𝐹‘𝑥) = 𝑧) |
16 | | fnbrfvb 6765 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → ((𝐹‘𝑥) = 𝑧 ↔ 𝑥𝐹𝑧)) |
17 | 15, 16 | syl5bb 286 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑧 = (𝐹‘𝑥) ↔ 𝑥𝐹𝑧)) |
18 | | eqcom 2744 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = (𝐹‘𝑦) ↔ (𝐹‘𝑦) = 𝑧) |
19 | | fnbrfvb 6765 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹 Fn 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝐹‘𝑦) = 𝑧 ↔ 𝑦𝐹𝑧)) |
20 | 18, 19 | syl5bb 286 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 Fn 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑧 = (𝐹‘𝑦) ↔ 𝑦𝐹𝑧)) |
21 | 17, 20 | bi2anan9 639 |
. . . . . . . . . . . . 13
⊢ (((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝐹 Fn 𝐴 ∧ 𝑦 ∈ 𝐴)) → ((𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦)) ↔ (𝑥𝐹𝑧 ∧ 𝑦𝐹𝑧))) |
22 | 21 | anandis 678 |
. . . . . . . . . . . 12
⊢ ((𝐹 Fn 𝐴 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → ((𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦)) ↔ (𝑥𝐹𝑧 ∧ 𝑦𝐹𝑧))) |
23 | 22 | pm5.32da 582 |
. . . . . . . . . . 11
⊢ (𝐹 Fn 𝐴 → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦))) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (𝑥𝐹𝑧 ∧ 𝑦𝐹𝑧)))) |
24 | 14, 23 | bitr4d 285 |
. . . . . . . . . 10
⊢ (𝐹 Fn 𝐴 → ((𝑥𝐹𝑧 ∧ 𝑦𝐹𝑧) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦))))) |
25 | 24 | imbi1d 345 |
. . . . . . . . 9
⊢ (𝐹 Fn 𝐴 → (((𝑥𝐹𝑧 ∧ 𝑦𝐹𝑧) → 𝑥 = 𝑦) ↔ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦))) → 𝑥 = 𝑦))) |
26 | | impexp 454 |
. . . . . . . . 9
⊢ ((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦))) → 𝑥 = 𝑦) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦)) → 𝑥 = 𝑦))) |
27 | 25, 26 | bitrdi 290 |
. . . . . . . 8
⊢ (𝐹 Fn 𝐴 → (((𝑥𝐹𝑧 ∧ 𝑦𝐹𝑧) → 𝑥 = 𝑦) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦)) → 𝑥 = 𝑦)))) |
28 | 27 | albidv 1928 |
. . . . . . 7
⊢ (𝐹 Fn 𝐴 → (∀𝑧((𝑥𝐹𝑧 ∧ 𝑦𝐹𝑧) → 𝑥 = 𝑦) ↔ ∀𝑧((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦)) → 𝑥 = 𝑦)))) |
29 | | 19.21v 1947 |
. . . . . . . 8
⊢
(∀𝑧((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦)) → 𝑥 = 𝑦)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ∀𝑧((𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦)) → 𝑥 = 𝑦))) |
30 | | 19.23v 1950 |
. . . . . . . . . 10
⊢
(∀𝑧((𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦)) → 𝑥 = 𝑦) ↔ (∃𝑧(𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦)) → 𝑥 = 𝑦)) |
31 | | fvex 6730 |
. . . . . . . . . . . 12
⊢ (𝐹‘𝑥) ∈ V |
32 | 31 | eqvinc 3556 |
. . . . . . . . . . 11
⊢ ((𝐹‘𝑥) = (𝐹‘𝑦) ↔ ∃𝑧(𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦))) |
33 | 32 | imbi1i 353 |
. . . . . . . . . 10
⊢ (((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦) ↔ (∃𝑧(𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦)) → 𝑥 = 𝑦)) |
34 | 30, 33 | bitr4i 281 |
. . . . . . . . 9
⊢
(∀𝑧((𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦)) → 𝑥 = 𝑦) ↔ ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)) |
35 | 34 | imbi2i 339 |
. . . . . . . 8
⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ∀𝑧((𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦)) → 𝑥 = 𝑦)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))) |
36 | 29, 35 | bitri 278 |
. . . . . . 7
⊢
(∀𝑧((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦)) → 𝑥 = 𝑦)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))) |
37 | 28, 36 | bitrdi 290 |
. . . . . 6
⊢ (𝐹 Fn 𝐴 → (∀𝑧((𝑥𝐹𝑧 ∧ 𝑦𝐹𝑧) → 𝑥 = 𝑦) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)))) |
38 | 37 | 2albidv 1931 |
. . . . 5
⊢ (𝐹 Fn 𝐴 → (∀𝑥∀𝑦∀𝑧((𝑥𝐹𝑧 ∧ 𝑦𝐹𝑧) → 𝑥 = 𝑦) ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)))) |
39 | | breq1 5056 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝑥𝐹𝑧 ↔ 𝑦𝐹𝑧)) |
40 | 39 | mo4 2565 |
. . . . . . 7
⊢
(∃*𝑥 𝑥𝐹𝑧 ↔ ∀𝑥∀𝑦((𝑥𝐹𝑧 ∧ 𝑦𝐹𝑧) → 𝑥 = 𝑦)) |
41 | 40 | albii 1827 |
. . . . . 6
⊢
(∀𝑧∃*𝑥 𝑥𝐹𝑧 ↔ ∀𝑧∀𝑥∀𝑦((𝑥𝐹𝑧 ∧ 𝑦𝐹𝑧) → 𝑥 = 𝑦)) |
42 | | alrot3 2161 |
. . . . . 6
⊢
(∀𝑧∀𝑥∀𝑦((𝑥𝐹𝑧 ∧ 𝑦𝐹𝑧) → 𝑥 = 𝑦) ↔ ∀𝑥∀𝑦∀𝑧((𝑥𝐹𝑧 ∧ 𝑦𝐹𝑧) → 𝑥 = 𝑦)) |
43 | 41, 42 | bitri 278 |
. . . . 5
⊢
(∀𝑧∃*𝑥 𝑥𝐹𝑧 ↔ ∀𝑥∀𝑦∀𝑧((𝑥𝐹𝑧 ∧ 𝑦𝐹𝑧) → 𝑥 = 𝑦)) |
44 | | r2al 3122 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦) ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))) |
45 | 38, 43, 44 | 3bitr4g 317 |
. . . 4
⊢ (𝐹 Fn 𝐴 → (∀𝑧∃*𝑥 𝑥𝐹𝑧 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))) |
46 | 2, 45 | syl 17 |
. . 3
⊢ (𝐹:𝐴⟶𝐵 → (∀𝑧∃*𝑥 𝑥𝐹𝑧 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))) |
47 | 46 | pm5.32i 578 |
. 2
⊢ ((𝐹:𝐴⟶𝐵 ∧ ∀𝑧∃*𝑥 𝑥𝐹𝑧) ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))) |
48 | 1, 47 | bitri 278 |
1
⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))) |