| Step | Hyp | Ref
| Expression |
| 1 | | fssxp 6763 |
. . 3
⊢ (𝐹:𝐴⟶𝐵 → 𝐹 ⊆ (𝐴 × 𝐵)) |
| 2 | | ffun 6739 |
. . . . . . . 8
⊢ (𝐹:𝐴⟶𝐵 → Fun 𝐹) |
| 3 | | fdm 6745 |
. . . . . . . . . 10
⊢ (𝐹:𝐴⟶𝐵 → dom 𝐹 = 𝐴) |
| 4 | 3 | eleq2d 2827 |
. . . . . . . . 9
⊢ (𝐹:𝐴⟶𝐵 → (𝑥 ∈ dom 𝐹 ↔ 𝑥 ∈ 𝐴)) |
| 5 | 4 | biimpar 477 |
. . . . . . . 8
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ dom 𝐹) |
| 6 | | funfvop 7070 |
. . . . . . . 8
⊢ ((Fun
𝐹 ∧ 𝑥 ∈ dom 𝐹) → 〈𝑥, (𝐹‘𝑥)〉 ∈ 𝐹) |
| 7 | 2, 5, 6 | syl2an2r 685 |
. . . . . . 7
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → 〈𝑥, (𝐹‘𝑥)〉 ∈ 𝐹) |
| 8 | | df-br 5144 |
. . . . . . 7
⊢ (𝑥𝐹(𝐹‘𝑥) ↔ 〈𝑥, (𝐹‘𝑥)〉 ∈ 𝐹) |
| 9 | 7, 8 | sylibr 234 |
. . . . . 6
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → 𝑥𝐹(𝐹‘𝑥)) |
| 10 | | fvex 6919 |
. . . . . . 7
⊢ (𝐹‘𝑥) ∈ V |
| 11 | | breq2 5147 |
. . . . . . 7
⊢ (𝑦 = (𝐹‘𝑥) → (𝑥𝐹𝑦 ↔ 𝑥𝐹(𝐹‘𝑥))) |
| 12 | 10, 11 | spcev 3606 |
. . . . . 6
⊢ (𝑥𝐹(𝐹‘𝑥) → ∃𝑦 𝑥𝐹𝑦) |
| 13 | 9, 12 | syl 17 |
. . . . 5
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → ∃𝑦 𝑥𝐹𝑦) |
| 14 | | funmo 6581 |
. . . . . . 7
⊢ (Fun
𝐹 → ∃*𝑦 𝑥𝐹𝑦) |
| 15 | 2, 14 | syl 17 |
. . . . . 6
⊢ (𝐹:𝐴⟶𝐵 → ∃*𝑦 𝑥𝐹𝑦) |
| 16 | 15 | adantr 480 |
. . . . 5
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → ∃*𝑦 𝑥𝐹𝑦) |
| 17 | | df-eu 2569 |
. . . . 5
⊢
(∃!𝑦 𝑥𝐹𝑦 ↔ (∃𝑦 𝑥𝐹𝑦 ∧ ∃*𝑦 𝑥𝐹𝑦)) |
| 18 | 13, 16, 17 | sylanbrc 583 |
. . . 4
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → ∃!𝑦 𝑥𝐹𝑦) |
| 19 | 18 | ralrimiva 3146 |
. . 3
⊢ (𝐹:𝐴⟶𝐵 → ∀𝑥 ∈ 𝐴 ∃!𝑦 𝑥𝐹𝑦) |
| 20 | 1, 19 | jca 511 |
. 2
⊢ (𝐹:𝐴⟶𝐵 → (𝐹 ⊆ (𝐴 × 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∃!𝑦 𝑥𝐹𝑦)) |
| 21 | | xpss 5701 |
. . . . . . . 8
⊢ (𝐴 × 𝐵) ⊆ (V × V) |
| 22 | | sstr 3992 |
. . . . . . . 8
⊢ ((𝐹 ⊆ (𝐴 × 𝐵) ∧ (𝐴 × 𝐵) ⊆ (V × V)) → 𝐹 ⊆ (V ×
V)) |
| 23 | 21, 22 | mpan2 691 |
. . . . . . 7
⊢ (𝐹 ⊆ (𝐴 × 𝐵) → 𝐹 ⊆ (V × V)) |
| 24 | | df-rel 5692 |
. . . . . . 7
⊢ (Rel
𝐹 ↔ 𝐹 ⊆ (V × V)) |
| 25 | 23, 24 | sylibr 234 |
. . . . . 6
⊢ (𝐹 ⊆ (𝐴 × 𝐵) → Rel 𝐹) |
| 26 | 25 | adantr 480 |
. . . . 5
⊢ ((𝐹 ⊆ (𝐴 × 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∃!𝑦 𝑥𝐹𝑦) → Rel 𝐹) |
| 27 | | df-ral 3062 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝐴 ∃!𝑦 𝑥𝐹𝑦 ↔ ∀𝑥(𝑥 ∈ 𝐴 → ∃!𝑦 𝑥𝐹𝑦)) |
| 28 | | eumo 2578 |
. . . . . . . . . . . 12
⊢
(∃!𝑦 𝑥𝐹𝑦 → ∃*𝑦 𝑥𝐹𝑦) |
| 29 | 28 | imim2i 16 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝐴 → ∃!𝑦 𝑥𝐹𝑦) → (𝑥 ∈ 𝐴 → ∃*𝑦 𝑥𝐹𝑦)) |
| 30 | 29 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝐹 ⊆ (𝐴 × 𝐵) ∧ (𝑥 ∈ 𝐴 → ∃!𝑦 𝑥𝐹𝑦)) → (𝑥 ∈ 𝐴 → ∃*𝑦 𝑥𝐹𝑦)) |
| 31 | | df-br 5144 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥𝐹𝑦 ↔ 〈𝑥, 𝑦〉 ∈ 𝐹) |
| 32 | | ssel 3977 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹 ⊆ (𝐴 × 𝐵) → (〈𝑥, 𝑦〉 ∈ 𝐹 → 〈𝑥, 𝑦〉 ∈ (𝐴 × 𝐵))) |
| 33 | 31, 32 | biimtrid 242 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 ⊆ (𝐴 × 𝐵) → (𝑥𝐹𝑦 → 〈𝑥, 𝑦〉 ∈ (𝐴 × 𝐵))) |
| 34 | | opelxp1 5727 |
. . . . . . . . . . . . . . 15
⊢
(〈𝑥, 𝑦〉 ∈ (𝐴 × 𝐵) → 𝑥 ∈ 𝐴) |
| 35 | 33, 34 | syl6 35 |
. . . . . . . . . . . . . 14
⊢ (𝐹 ⊆ (𝐴 × 𝐵) → (𝑥𝐹𝑦 → 𝑥 ∈ 𝐴)) |
| 36 | 35 | exlimdv 1933 |
. . . . . . . . . . . . 13
⊢ (𝐹 ⊆ (𝐴 × 𝐵) → (∃𝑦 𝑥𝐹𝑦 → 𝑥 ∈ 𝐴)) |
| 37 | 36 | con3d 152 |
. . . . . . . . . . . 12
⊢ (𝐹 ⊆ (𝐴 × 𝐵) → (¬ 𝑥 ∈ 𝐴 → ¬ ∃𝑦 𝑥𝐹𝑦)) |
| 38 | | nexmo 2541 |
. . . . . . . . . . . 12
⊢ (¬
∃𝑦 𝑥𝐹𝑦 → ∃*𝑦 𝑥𝐹𝑦) |
| 39 | 37, 38 | syl6 35 |
. . . . . . . . . . 11
⊢ (𝐹 ⊆ (𝐴 × 𝐵) → (¬ 𝑥 ∈ 𝐴 → ∃*𝑦 𝑥𝐹𝑦)) |
| 40 | 39 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝐹 ⊆ (𝐴 × 𝐵) ∧ (𝑥 ∈ 𝐴 → ∃!𝑦 𝑥𝐹𝑦)) → (¬ 𝑥 ∈ 𝐴 → ∃*𝑦 𝑥𝐹𝑦)) |
| 41 | 30, 40 | pm2.61d 179 |
. . . . . . . . 9
⊢ ((𝐹 ⊆ (𝐴 × 𝐵) ∧ (𝑥 ∈ 𝐴 → ∃!𝑦 𝑥𝐹𝑦)) → ∃*𝑦 𝑥𝐹𝑦) |
| 42 | 41 | ex 412 |
. . . . . . . 8
⊢ (𝐹 ⊆ (𝐴 × 𝐵) → ((𝑥 ∈ 𝐴 → ∃!𝑦 𝑥𝐹𝑦) → ∃*𝑦 𝑥𝐹𝑦)) |
| 43 | 42 | alimdv 1916 |
. . . . . . 7
⊢ (𝐹 ⊆ (𝐴 × 𝐵) → (∀𝑥(𝑥 ∈ 𝐴 → ∃!𝑦 𝑥𝐹𝑦) → ∀𝑥∃*𝑦 𝑥𝐹𝑦)) |
| 44 | 27, 43 | biimtrid 242 |
. . . . . 6
⊢ (𝐹 ⊆ (𝐴 × 𝐵) → (∀𝑥 ∈ 𝐴 ∃!𝑦 𝑥𝐹𝑦 → ∀𝑥∃*𝑦 𝑥𝐹𝑦)) |
| 45 | 44 | imp 406 |
. . . . 5
⊢ ((𝐹 ⊆ (𝐴 × 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∃!𝑦 𝑥𝐹𝑦) → ∀𝑥∃*𝑦 𝑥𝐹𝑦) |
| 46 | | dffun6 6574 |
. . . . 5
⊢ (Fun
𝐹 ↔ (Rel 𝐹 ∧ ∀𝑥∃*𝑦 𝑥𝐹𝑦)) |
| 47 | 26, 45, 46 | sylanbrc 583 |
. . . 4
⊢ ((𝐹 ⊆ (𝐴 × 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∃!𝑦 𝑥𝐹𝑦) → Fun 𝐹) |
| 48 | | dmss 5913 |
. . . . . . 7
⊢ (𝐹 ⊆ (𝐴 × 𝐵) → dom 𝐹 ⊆ dom (𝐴 × 𝐵)) |
| 49 | | dmxpss 6191 |
. . . . . . 7
⊢ dom
(𝐴 × 𝐵) ⊆ 𝐴 |
| 50 | 48, 49 | sstrdi 3996 |
. . . . . 6
⊢ (𝐹 ⊆ (𝐴 × 𝐵) → dom 𝐹 ⊆ 𝐴) |
| 51 | | breq1 5146 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑧 → (𝑥𝐹𝑦 ↔ 𝑧𝐹𝑦)) |
| 52 | 51 | eubidv 2586 |
. . . . . . . . 9
⊢ (𝑥 = 𝑧 → (∃!𝑦 𝑥𝐹𝑦 ↔ ∃!𝑦 𝑧𝐹𝑦)) |
| 53 | 52 | rspccv 3619 |
. . . . . . . 8
⊢
(∀𝑥 ∈
𝐴 ∃!𝑦 𝑥𝐹𝑦 → (𝑧 ∈ 𝐴 → ∃!𝑦 𝑧𝐹𝑦)) |
| 54 | | euex 2577 |
. . . . . . . . 9
⊢
(∃!𝑦 𝑧𝐹𝑦 → ∃𝑦 𝑧𝐹𝑦) |
| 55 | | vex 3484 |
. . . . . . . . . 10
⊢ 𝑧 ∈ V |
| 56 | 55 | eldm 5911 |
. . . . . . . . 9
⊢ (𝑧 ∈ dom 𝐹 ↔ ∃𝑦 𝑧𝐹𝑦) |
| 57 | 54, 56 | sylibr 234 |
. . . . . . . 8
⊢
(∃!𝑦 𝑧𝐹𝑦 → 𝑧 ∈ dom 𝐹) |
| 58 | 53, 57 | syl6 35 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝐴 ∃!𝑦 𝑥𝐹𝑦 → (𝑧 ∈ 𝐴 → 𝑧 ∈ dom 𝐹)) |
| 59 | 58 | ssrdv 3989 |
. . . . . 6
⊢
(∀𝑥 ∈
𝐴 ∃!𝑦 𝑥𝐹𝑦 → 𝐴 ⊆ dom 𝐹) |
| 60 | 50, 59 | anim12i 613 |
. . . . 5
⊢ ((𝐹 ⊆ (𝐴 × 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∃!𝑦 𝑥𝐹𝑦) → (dom 𝐹 ⊆ 𝐴 ∧ 𝐴 ⊆ dom 𝐹)) |
| 61 | | eqss 3999 |
. . . . 5
⊢ (dom
𝐹 = 𝐴 ↔ (dom 𝐹 ⊆ 𝐴 ∧ 𝐴 ⊆ dom 𝐹)) |
| 62 | 60, 61 | sylibr 234 |
. . . 4
⊢ ((𝐹 ⊆ (𝐴 × 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∃!𝑦 𝑥𝐹𝑦) → dom 𝐹 = 𝐴) |
| 63 | | df-fn 6564 |
. . . 4
⊢ (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴)) |
| 64 | 47, 62, 63 | sylanbrc 583 |
. . 3
⊢ ((𝐹 ⊆ (𝐴 × 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∃!𝑦 𝑥𝐹𝑦) → 𝐹 Fn 𝐴) |
| 65 | | rnss 5950 |
. . . . 5
⊢ (𝐹 ⊆ (𝐴 × 𝐵) → ran 𝐹 ⊆ ran (𝐴 × 𝐵)) |
| 66 | | rnxpss 6192 |
. . . . 5
⊢ ran
(𝐴 × 𝐵) ⊆ 𝐵 |
| 67 | 65, 66 | sstrdi 3996 |
. . . 4
⊢ (𝐹 ⊆ (𝐴 × 𝐵) → ran 𝐹 ⊆ 𝐵) |
| 68 | 67 | adantr 480 |
. . 3
⊢ ((𝐹 ⊆ (𝐴 × 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∃!𝑦 𝑥𝐹𝑦) → ran 𝐹 ⊆ 𝐵) |
| 69 | | df-f 6565 |
. . 3
⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵)) |
| 70 | 64, 68, 69 | sylanbrc 583 |
. 2
⊢ ((𝐹 ⊆ (𝐴 × 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∃!𝑦 𝑥𝐹𝑦) → 𝐹:𝐴⟶𝐵) |
| 71 | 20, 70 | impbii 209 |
1
⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 ⊆ (𝐴 × 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∃!𝑦 𝑥𝐹𝑦)) |