Step | Hyp | Ref
| Expression |
1 | | dff12 5416 |
. 2
⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑧∃*𝑥 𝑥𝐹𝑧)) |
2 | | ffn 5361 |
. . . 4
⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴) |
3 | | vex 2740 |
. . . . . . . . . . . . . . 15
⊢ 𝑥 ∈ V |
4 | | vex 2740 |
. . . . . . . . . . . . . . 15
⊢ 𝑧 ∈ V |
5 | 3, 4 | breldm 4827 |
. . . . . . . . . . . . . 14
⊢ (𝑥𝐹𝑧 → 𝑥 ∈ dom 𝐹) |
6 | | fndm 5311 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴) |
7 | 6 | eleq2d 2247 |
. . . . . . . . . . . . . 14
⊢ (𝐹 Fn 𝐴 → (𝑥 ∈ dom 𝐹 ↔ 𝑥 ∈ 𝐴)) |
8 | 5, 7 | imbitrid 154 |
. . . . . . . . . . . . 13
⊢ (𝐹 Fn 𝐴 → (𝑥𝐹𝑧 → 𝑥 ∈ 𝐴)) |
9 | | vex 2740 |
. . . . . . . . . . . . . . 15
⊢ 𝑦 ∈ V |
10 | 9, 4 | breldm 4827 |
. . . . . . . . . . . . . 14
⊢ (𝑦𝐹𝑧 → 𝑦 ∈ dom 𝐹) |
11 | 6 | eleq2d 2247 |
. . . . . . . . . . . . . 14
⊢ (𝐹 Fn 𝐴 → (𝑦 ∈ dom 𝐹 ↔ 𝑦 ∈ 𝐴)) |
12 | 10, 11 | imbitrid 154 |
. . . . . . . . . . . . 13
⊢ (𝐹 Fn 𝐴 → (𝑦𝐹𝑧 → 𝑦 ∈ 𝐴)) |
13 | 8, 12 | anim12d 335 |
. . . . . . . . . . . 12
⊢ (𝐹 Fn 𝐴 → ((𝑥𝐹𝑧 ∧ 𝑦𝐹𝑧) → (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴))) |
14 | 13 | pm4.71rd 394 |
. . . . . . . . . . 11
⊢ (𝐹 Fn 𝐴 → ((𝑥𝐹𝑧 ∧ 𝑦𝐹𝑧) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (𝑥𝐹𝑧 ∧ 𝑦𝐹𝑧)))) |
15 | | eqcom 2179 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = (𝐹‘𝑥) ↔ (𝐹‘𝑥) = 𝑧) |
16 | | fnbrfvb 5552 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → ((𝐹‘𝑥) = 𝑧 ↔ 𝑥𝐹𝑧)) |
17 | 15, 16 | bitrid 192 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑧 = (𝐹‘𝑥) ↔ 𝑥𝐹𝑧)) |
18 | | eqcom 2179 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = (𝐹‘𝑦) ↔ (𝐹‘𝑦) = 𝑧) |
19 | | fnbrfvb 5552 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹 Fn 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝐹‘𝑦) = 𝑧 ↔ 𝑦𝐹𝑧)) |
20 | 18, 19 | bitrid 192 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 Fn 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑧 = (𝐹‘𝑦) ↔ 𝑦𝐹𝑧)) |
21 | 17, 20 | bi2anan9 606 |
. . . . . . . . . . . . 13
⊢ (((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝐹 Fn 𝐴 ∧ 𝑦 ∈ 𝐴)) → ((𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦)) ↔ (𝑥𝐹𝑧 ∧ 𝑦𝐹𝑧))) |
22 | 21 | anandis 592 |
. . . . . . . . . . . 12
⊢ ((𝐹 Fn 𝐴 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → ((𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦)) ↔ (𝑥𝐹𝑧 ∧ 𝑦𝐹𝑧))) |
23 | 22 | pm5.32da 452 |
. . . . . . . . . . 11
⊢ (𝐹 Fn 𝐴 → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦))) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (𝑥𝐹𝑧 ∧ 𝑦𝐹𝑧)))) |
24 | 14, 23 | bitr4d 191 |
. . . . . . . . . 10
⊢ (𝐹 Fn 𝐴 → ((𝑥𝐹𝑧 ∧ 𝑦𝐹𝑧) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦))))) |
25 | 24 | imbi1d 231 |
. . . . . . . . 9
⊢ (𝐹 Fn 𝐴 → (((𝑥𝐹𝑧 ∧ 𝑦𝐹𝑧) → 𝑥 = 𝑦) ↔ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦))) → 𝑥 = 𝑦))) |
26 | | impexp 263 |
. . . . . . . . 9
⊢ ((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦))) → 𝑥 = 𝑦) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦)) → 𝑥 = 𝑦))) |
27 | 25, 26 | bitrdi 196 |
. . . . . . . 8
⊢ (𝐹 Fn 𝐴 → (((𝑥𝐹𝑧 ∧ 𝑦𝐹𝑧) → 𝑥 = 𝑦) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦)) → 𝑥 = 𝑦)))) |
28 | 27 | albidv 1824 |
. . . . . . 7
⊢ (𝐹 Fn 𝐴 → (∀𝑧((𝑥𝐹𝑧 ∧ 𝑦𝐹𝑧) → 𝑥 = 𝑦) ↔ ∀𝑧((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦)) → 𝑥 = 𝑦)))) |
29 | | 19.21v 1873 |
. . . . . . . 8
⊢
(∀𝑧((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦)) → 𝑥 = 𝑦)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ∀𝑧((𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦)) → 𝑥 = 𝑦))) |
30 | | 19.23v 1883 |
. . . . . . . . . . 11
⊢
(∀𝑧((𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦)) → 𝑥 = 𝑦) ↔ (∃𝑧(𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦)) → 𝑥 = 𝑦)) |
31 | | funfvex 5528 |
. . . . . . . . . . . . . 14
⊢ ((Fun
𝐹 ∧ 𝑥 ∈ dom 𝐹) → (𝐹‘𝑥) ∈ V) |
32 | 31 | funfni 5312 |
. . . . . . . . . . . . 13
⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ V) |
33 | | eqvincg 2861 |
. . . . . . . . . . . . 13
⊢ ((𝐹‘𝑥) ∈ V → ((𝐹‘𝑥) = (𝐹‘𝑦) ↔ ∃𝑧(𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦)))) |
34 | 32, 33 | syl 14 |
. . . . . . . . . . . 12
⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → ((𝐹‘𝑥) = (𝐹‘𝑦) ↔ ∃𝑧(𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦)))) |
35 | 34 | imbi1d 231 |
. . . . . . . . . . 11
⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → (((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦) ↔ (∃𝑧(𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦)) → 𝑥 = 𝑦))) |
36 | 30, 35 | bitr4id 199 |
. . . . . . . . . 10
⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → (∀𝑧((𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦)) → 𝑥 = 𝑦) ↔ ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))) |
37 | 36 | adantrr 479 |
. . . . . . . . 9
⊢ ((𝐹 Fn 𝐴 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (∀𝑧((𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦)) → 𝑥 = 𝑦) ↔ ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))) |
38 | 37 | pm5.74da 443 |
. . . . . . . 8
⊢ (𝐹 Fn 𝐴 → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ∀𝑧((𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦)) → 𝑥 = 𝑦)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)))) |
39 | 29, 38 | bitrid 192 |
. . . . . . 7
⊢ (𝐹 Fn 𝐴 → (∀𝑧((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦)) → 𝑥 = 𝑦)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)))) |
40 | 28, 39 | bitrd 188 |
. . . . . 6
⊢ (𝐹 Fn 𝐴 → (∀𝑧((𝑥𝐹𝑧 ∧ 𝑦𝐹𝑧) → 𝑥 = 𝑦) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)))) |
41 | 40 | 2albidv 1867 |
. . . . 5
⊢ (𝐹 Fn 𝐴 → (∀𝑥∀𝑦∀𝑧((𝑥𝐹𝑧 ∧ 𝑦𝐹𝑧) → 𝑥 = 𝑦) ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)))) |
42 | | breq1 4003 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝑥𝐹𝑧 ↔ 𝑦𝐹𝑧)) |
43 | 42 | mo4 2087 |
. . . . . . 7
⊢
(∃*𝑥 𝑥𝐹𝑧 ↔ ∀𝑥∀𝑦((𝑥𝐹𝑧 ∧ 𝑦𝐹𝑧) → 𝑥 = 𝑦)) |
44 | 43 | albii 1470 |
. . . . . 6
⊢
(∀𝑧∃*𝑥 𝑥𝐹𝑧 ↔ ∀𝑧∀𝑥∀𝑦((𝑥𝐹𝑧 ∧ 𝑦𝐹𝑧) → 𝑥 = 𝑦)) |
45 | | alrot3 1485 |
. . . . . 6
⊢
(∀𝑧∀𝑥∀𝑦((𝑥𝐹𝑧 ∧ 𝑦𝐹𝑧) → 𝑥 = 𝑦) ↔ ∀𝑥∀𝑦∀𝑧((𝑥𝐹𝑧 ∧ 𝑦𝐹𝑧) → 𝑥 = 𝑦)) |
46 | 44, 45 | bitri 184 |
. . . . 5
⊢
(∀𝑧∃*𝑥 𝑥𝐹𝑧 ↔ ∀𝑥∀𝑦∀𝑧((𝑥𝐹𝑧 ∧ 𝑦𝐹𝑧) → 𝑥 = 𝑦)) |
47 | | r2al 2496 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦) ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))) |
48 | 41, 46, 47 | 3bitr4g 223 |
. . . 4
⊢ (𝐹 Fn 𝐴 → (∀𝑧∃*𝑥 𝑥𝐹𝑧 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))) |
49 | 2, 48 | syl 14 |
. . 3
⊢ (𝐹:𝐴⟶𝐵 → (∀𝑧∃*𝑥 𝑥𝐹𝑧 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))) |
50 | 49 | pm5.32i 454 |
. 2
⊢ ((𝐹:𝐴⟶𝐵 ∧ ∀𝑧∃*𝑥 𝑥𝐹𝑧) ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))) |
51 | 1, 50 | bitri 184 |
1
⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))) |