| Step | Hyp | Ref
| Expression |
| 1 | | dff12 6803 |
. 2
⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑧∃*𝑥 𝑥𝐹𝑧)) |
| 2 | | ffn 6736 |
. . . 4
⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴) |
| 3 | | vex 3484 |
. . . . . . . . . . . . . . 15
⊢ 𝑥 ∈ V |
| 4 | | vex 3484 |
. . . . . . . . . . . . . . 15
⊢ 𝑧 ∈ V |
| 5 | 3, 4 | breldm 5919 |
. . . . . . . . . . . . . 14
⊢ (𝑥𝐹𝑧 → 𝑥 ∈ dom 𝐹) |
| 6 | | fndm 6671 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴) |
| 7 | 6 | eleq2d 2827 |
. . . . . . . . . . . . . 14
⊢ (𝐹 Fn 𝐴 → (𝑥 ∈ dom 𝐹 ↔ 𝑥 ∈ 𝐴)) |
| 8 | 5, 7 | imbitrid 244 |
. . . . . . . . . . . . 13
⊢ (𝐹 Fn 𝐴 → (𝑥𝐹𝑧 → 𝑥 ∈ 𝐴)) |
| 9 | | vex 3484 |
. . . . . . . . . . . . . . 15
⊢ 𝑦 ∈ V |
| 10 | 9, 4 | breldm 5919 |
. . . . . . . . . . . . . 14
⊢ (𝑦𝐹𝑧 → 𝑦 ∈ dom 𝐹) |
| 11 | 6 | eleq2d 2827 |
. . . . . . . . . . . . . 14
⊢ (𝐹 Fn 𝐴 → (𝑦 ∈ dom 𝐹 ↔ 𝑦 ∈ 𝐴)) |
| 12 | 10, 11 | imbitrid 244 |
. . . . . . . . . . . . 13
⊢ (𝐹 Fn 𝐴 → (𝑦𝐹𝑧 → 𝑦 ∈ 𝐴)) |
| 13 | 8, 12 | anim12d 609 |
. . . . . . . . . . . 12
⊢ (𝐹 Fn 𝐴 → ((𝑥𝐹𝑧 ∧ 𝑦𝐹𝑧) → (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴))) |
| 14 | 13 | pm4.71rd 562 |
. . . . . . . . . . 11
⊢ (𝐹 Fn 𝐴 → ((𝑥𝐹𝑧 ∧ 𝑦𝐹𝑧) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (𝑥𝐹𝑧 ∧ 𝑦𝐹𝑧)))) |
| 15 | | eqcom 2744 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = (𝐹‘𝑥) ↔ (𝐹‘𝑥) = 𝑧) |
| 16 | | fnbrfvb 6959 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → ((𝐹‘𝑥) = 𝑧 ↔ 𝑥𝐹𝑧)) |
| 17 | 15, 16 | bitrid 283 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑧 = (𝐹‘𝑥) ↔ 𝑥𝐹𝑧)) |
| 18 | | eqcom 2744 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = (𝐹‘𝑦) ↔ (𝐹‘𝑦) = 𝑧) |
| 19 | | fnbrfvb 6959 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹 Fn 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝐹‘𝑦) = 𝑧 ↔ 𝑦𝐹𝑧)) |
| 20 | 18, 19 | bitrid 283 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 Fn 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑧 = (𝐹‘𝑦) ↔ 𝑦𝐹𝑧)) |
| 21 | 17, 20 | bi2anan9 638 |
. . . . . . . . . . . . 13
⊢ (((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝐹 Fn 𝐴 ∧ 𝑦 ∈ 𝐴)) → ((𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦)) ↔ (𝑥𝐹𝑧 ∧ 𝑦𝐹𝑧))) |
| 22 | 21 | anandis 678 |
. . . . . . . . . . . 12
⊢ ((𝐹 Fn 𝐴 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → ((𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦)) ↔ (𝑥𝐹𝑧 ∧ 𝑦𝐹𝑧))) |
| 23 | 22 | pm5.32da 579 |
. . . . . . . . . . 11
⊢ (𝐹 Fn 𝐴 → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦))) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (𝑥𝐹𝑧 ∧ 𝑦𝐹𝑧)))) |
| 24 | 14, 23 | bitr4d 282 |
. . . . . . . . . 10
⊢ (𝐹 Fn 𝐴 → ((𝑥𝐹𝑧 ∧ 𝑦𝐹𝑧) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦))))) |
| 25 | 24 | imbi1d 341 |
. . . . . . . . 9
⊢ (𝐹 Fn 𝐴 → (((𝑥𝐹𝑧 ∧ 𝑦𝐹𝑧) → 𝑥 = 𝑦) ↔ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦))) → 𝑥 = 𝑦))) |
| 26 | | impexp 450 |
. . . . . . . . 9
⊢ ((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦))) → 𝑥 = 𝑦) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦)) → 𝑥 = 𝑦))) |
| 27 | 25, 26 | bitrdi 287 |
. . . . . . . 8
⊢ (𝐹 Fn 𝐴 → (((𝑥𝐹𝑧 ∧ 𝑦𝐹𝑧) → 𝑥 = 𝑦) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦)) → 𝑥 = 𝑦)))) |
| 28 | 27 | albidv 1920 |
. . . . . . 7
⊢ (𝐹 Fn 𝐴 → (∀𝑧((𝑥𝐹𝑧 ∧ 𝑦𝐹𝑧) → 𝑥 = 𝑦) ↔ ∀𝑧((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦)) → 𝑥 = 𝑦)))) |
| 29 | | 19.21v 1939 |
. . . . . . . 8
⊢
(∀𝑧((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦)) → 𝑥 = 𝑦)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ∀𝑧((𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦)) → 𝑥 = 𝑦))) |
| 30 | | 19.23v 1942 |
. . . . . . . . . 10
⊢
(∀𝑧((𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦)) → 𝑥 = 𝑦) ↔ (∃𝑧(𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦)) → 𝑥 = 𝑦)) |
| 31 | | fvex 6919 |
. . . . . . . . . . . 12
⊢ (𝐹‘𝑥) ∈ V |
| 32 | 31 | eqvinc 3649 |
. . . . . . . . . . 11
⊢ ((𝐹‘𝑥) = (𝐹‘𝑦) ↔ ∃𝑧(𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦))) |
| 33 | 32 | imbi1i 349 |
. . . . . . . . . 10
⊢ (((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦) ↔ (∃𝑧(𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦)) → 𝑥 = 𝑦)) |
| 34 | 30, 33 | bitr4i 278 |
. . . . . . . . 9
⊢
(∀𝑧((𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦)) → 𝑥 = 𝑦) ↔ ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)) |
| 35 | 34 | imbi2i 336 |
. . . . . . . 8
⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ∀𝑧((𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦)) → 𝑥 = 𝑦)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))) |
| 36 | 29, 35 | bitri 275 |
. . . . . . 7
⊢
(∀𝑧((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝑧 = (𝐹‘𝑥) ∧ 𝑧 = (𝐹‘𝑦)) → 𝑥 = 𝑦)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))) |
| 37 | 28, 36 | bitrdi 287 |
. . . . . 6
⊢ (𝐹 Fn 𝐴 → (∀𝑧((𝑥𝐹𝑧 ∧ 𝑦𝐹𝑧) → 𝑥 = 𝑦) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)))) |
| 38 | 37 | 2albidv 1923 |
. . . . 5
⊢ (𝐹 Fn 𝐴 → (∀𝑥∀𝑦∀𝑧((𝑥𝐹𝑧 ∧ 𝑦𝐹𝑧) → 𝑥 = 𝑦) ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)))) |
| 39 | | breq1 5146 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝑥𝐹𝑧 ↔ 𝑦𝐹𝑧)) |
| 40 | 39 | mo4 2566 |
. . . . . . 7
⊢
(∃*𝑥 𝑥𝐹𝑧 ↔ ∀𝑥∀𝑦((𝑥𝐹𝑧 ∧ 𝑦𝐹𝑧) → 𝑥 = 𝑦)) |
| 41 | 40 | albii 1819 |
. . . . . 6
⊢
(∀𝑧∃*𝑥 𝑥𝐹𝑧 ↔ ∀𝑧∀𝑥∀𝑦((𝑥𝐹𝑧 ∧ 𝑦𝐹𝑧) → 𝑥 = 𝑦)) |
| 42 | | alrot3 2160 |
. . . . . 6
⊢
(∀𝑧∀𝑥∀𝑦((𝑥𝐹𝑧 ∧ 𝑦𝐹𝑧) → 𝑥 = 𝑦) ↔ ∀𝑥∀𝑦∀𝑧((𝑥𝐹𝑧 ∧ 𝑦𝐹𝑧) → 𝑥 = 𝑦)) |
| 43 | 41, 42 | bitri 275 |
. . . . 5
⊢
(∀𝑧∃*𝑥 𝑥𝐹𝑧 ↔ ∀𝑥∀𝑦∀𝑧((𝑥𝐹𝑧 ∧ 𝑦𝐹𝑧) → 𝑥 = 𝑦)) |
| 44 | | r2al 3195 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦) ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))) |
| 45 | 38, 43, 44 | 3bitr4g 314 |
. . . 4
⊢ (𝐹 Fn 𝐴 → (∀𝑧∃*𝑥 𝑥𝐹𝑧 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))) |
| 46 | 2, 45 | syl 17 |
. . 3
⊢ (𝐹:𝐴⟶𝐵 → (∀𝑧∃*𝑥 𝑥𝐹𝑧 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))) |
| 47 | 46 | pm5.32i 574 |
. 2
⊢ ((𝐹:𝐴⟶𝐵 ∧ ∀𝑧∃*𝑥 𝑥𝐹𝑧) ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))) |
| 48 | 1, 47 | bitri 275 |
1
⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))) |