Step | Hyp | Ref
| Expression |
1 | | fssxp 6060 |
. . 3
⊢ (𝐹:𝐴⟶𝐵 → 𝐹 ⊆ (𝐴 × 𝐵)) |
2 | | ffun 6048 |
. . . . . . . 8
⊢ (𝐹:𝐴⟶𝐵 → Fun 𝐹) |
3 | | fdm 6051 |
. . . . . . . . . 10
⊢ (𝐹:𝐴⟶𝐵 → dom 𝐹 = 𝐴) |
4 | 3 | eleq2d 2687 |
. . . . . . . . 9
⊢ (𝐹:𝐴⟶𝐵 → (𝑥 ∈ dom 𝐹 ↔ 𝑥 ∈ 𝐴)) |
5 | 4 | biimpar 502 |
. . . . . . . 8
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ dom 𝐹) |
6 | | funfvop 6329 |
. . . . . . . 8
⊢ ((Fun
𝐹 ∧ 𝑥 ∈ dom 𝐹) → 〈𝑥, (𝐹‘𝑥)〉 ∈ 𝐹) |
7 | 2, 5, 6 | syl2an2r 876 |
. . . . . . 7
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → 〈𝑥, (𝐹‘𝑥)〉 ∈ 𝐹) |
8 | | df-br 4654 |
. . . . . . 7
⊢ (𝑥𝐹(𝐹‘𝑥) ↔ 〈𝑥, (𝐹‘𝑥)〉 ∈ 𝐹) |
9 | 7, 8 | sylibr 224 |
. . . . . 6
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → 𝑥𝐹(𝐹‘𝑥)) |
10 | | fvex 6201 |
. . . . . . 7
⊢ (𝐹‘𝑥) ∈ V |
11 | | breq2 4657 |
. . . . . . 7
⊢ (𝑦 = (𝐹‘𝑥) → (𝑥𝐹𝑦 ↔ 𝑥𝐹(𝐹‘𝑥))) |
12 | 10, 11 | spcev 3300 |
. . . . . 6
⊢ (𝑥𝐹(𝐹‘𝑥) → ∃𝑦 𝑥𝐹𝑦) |
13 | 9, 12 | syl 17 |
. . . . 5
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → ∃𝑦 𝑥𝐹𝑦) |
14 | | funmo 5904 |
. . . . . . 7
⊢ (Fun
𝐹 → ∃*𝑦 𝑥𝐹𝑦) |
15 | 2, 14 | syl 17 |
. . . . . 6
⊢ (𝐹:𝐴⟶𝐵 → ∃*𝑦 𝑥𝐹𝑦) |
16 | 15 | adantr 481 |
. . . . 5
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → ∃*𝑦 𝑥𝐹𝑦) |
17 | | eu5 2496 |
. . . . 5
⊢
(∃!𝑦 𝑥𝐹𝑦 ↔ (∃𝑦 𝑥𝐹𝑦 ∧ ∃*𝑦 𝑥𝐹𝑦)) |
18 | 13, 16, 17 | sylanbrc 698 |
. . . 4
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → ∃!𝑦 𝑥𝐹𝑦) |
19 | 18 | ralrimiva 2966 |
. . 3
⊢ (𝐹:𝐴⟶𝐵 → ∀𝑥 ∈ 𝐴 ∃!𝑦 𝑥𝐹𝑦) |
20 | 1, 19 | jca 554 |
. 2
⊢ (𝐹:𝐴⟶𝐵 → (𝐹 ⊆ (𝐴 × 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∃!𝑦 𝑥𝐹𝑦)) |
21 | | xpss 5226 |
. . . . . . . 8
⊢ (𝐴 × 𝐵) ⊆ (V × V) |
22 | | sstr 3611 |
. . . . . . . 8
⊢ ((𝐹 ⊆ (𝐴 × 𝐵) ∧ (𝐴 × 𝐵) ⊆ (V × V)) → 𝐹 ⊆ (V ×
V)) |
23 | 21, 22 | mpan2 707 |
. . . . . . 7
⊢ (𝐹 ⊆ (𝐴 × 𝐵) → 𝐹 ⊆ (V × V)) |
24 | | df-rel 5121 |
. . . . . . 7
⊢ (Rel
𝐹 ↔ 𝐹 ⊆ (V × V)) |
25 | 23, 24 | sylibr 224 |
. . . . . 6
⊢ (𝐹 ⊆ (𝐴 × 𝐵) → Rel 𝐹) |
26 | 25 | adantr 481 |
. . . . 5
⊢ ((𝐹 ⊆ (𝐴 × 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∃!𝑦 𝑥𝐹𝑦) → Rel 𝐹) |
27 | | df-ral 2917 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝐴 ∃!𝑦 𝑥𝐹𝑦 ↔ ∀𝑥(𝑥 ∈ 𝐴 → ∃!𝑦 𝑥𝐹𝑦)) |
28 | | eumo 2499 |
. . . . . . . . . . . 12
⊢
(∃!𝑦 𝑥𝐹𝑦 → ∃*𝑦 𝑥𝐹𝑦) |
29 | 28 | imim2i 16 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝐴 → ∃!𝑦 𝑥𝐹𝑦) → (𝑥 ∈ 𝐴 → ∃*𝑦 𝑥𝐹𝑦)) |
30 | 29 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝐹 ⊆ (𝐴 × 𝐵) ∧ (𝑥 ∈ 𝐴 → ∃!𝑦 𝑥𝐹𝑦)) → (𝑥 ∈ 𝐴 → ∃*𝑦 𝑥𝐹𝑦)) |
31 | | df-br 4654 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥𝐹𝑦 ↔ 〈𝑥, 𝑦〉 ∈ 𝐹) |
32 | | ssel 3597 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹 ⊆ (𝐴 × 𝐵) → (〈𝑥, 𝑦〉 ∈ 𝐹 → 〈𝑥, 𝑦〉 ∈ (𝐴 × 𝐵))) |
33 | 31, 32 | syl5bi 232 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 ⊆ (𝐴 × 𝐵) → (𝑥𝐹𝑦 → 〈𝑥, 𝑦〉 ∈ (𝐴 × 𝐵))) |
34 | | opelxp1 5150 |
. . . . . . . . . . . . . . 15
⊢
(〈𝑥, 𝑦〉 ∈ (𝐴 × 𝐵) → 𝑥 ∈ 𝐴) |
35 | 33, 34 | syl6 35 |
. . . . . . . . . . . . . 14
⊢ (𝐹 ⊆ (𝐴 × 𝐵) → (𝑥𝐹𝑦 → 𝑥 ∈ 𝐴)) |
36 | 35 | exlimdv 1861 |
. . . . . . . . . . . . 13
⊢ (𝐹 ⊆ (𝐴 × 𝐵) → (∃𝑦 𝑥𝐹𝑦 → 𝑥 ∈ 𝐴)) |
37 | 36 | con3d 148 |
. . . . . . . . . . . 12
⊢ (𝐹 ⊆ (𝐴 × 𝐵) → (¬ 𝑥 ∈ 𝐴 → ¬ ∃𝑦 𝑥𝐹𝑦)) |
38 | | exmo 2495 |
. . . . . . . . . . . . 13
⊢
(∃𝑦 𝑥𝐹𝑦 ∨ ∃*𝑦 𝑥𝐹𝑦) |
39 | 38 | ori 390 |
. . . . . . . . . . . 12
⊢ (¬
∃𝑦 𝑥𝐹𝑦 → ∃*𝑦 𝑥𝐹𝑦) |
40 | 37, 39 | syl6 35 |
. . . . . . . . . . 11
⊢ (𝐹 ⊆ (𝐴 × 𝐵) → (¬ 𝑥 ∈ 𝐴 → ∃*𝑦 𝑥𝐹𝑦)) |
41 | 40 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝐹 ⊆ (𝐴 × 𝐵) ∧ (𝑥 ∈ 𝐴 → ∃!𝑦 𝑥𝐹𝑦)) → (¬ 𝑥 ∈ 𝐴 → ∃*𝑦 𝑥𝐹𝑦)) |
42 | 30, 41 | pm2.61d 170 |
. . . . . . . . 9
⊢ ((𝐹 ⊆ (𝐴 × 𝐵) ∧ (𝑥 ∈ 𝐴 → ∃!𝑦 𝑥𝐹𝑦)) → ∃*𝑦 𝑥𝐹𝑦) |
43 | 42 | ex 450 |
. . . . . . . 8
⊢ (𝐹 ⊆ (𝐴 × 𝐵) → ((𝑥 ∈ 𝐴 → ∃!𝑦 𝑥𝐹𝑦) → ∃*𝑦 𝑥𝐹𝑦)) |
44 | 43 | alimdv 1845 |
. . . . . . 7
⊢ (𝐹 ⊆ (𝐴 × 𝐵) → (∀𝑥(𝑥 ∈ 𝐴 → ∃!𝑦 𝑥𝐹𝑦) → ∀𝑥∃*𝑦 𝑥𝐹𝑦)) |
45 | 27, 44 | syl5bi 232 |
. . . . . 6
⊢ (𝐹 ⊆ (𝐴 × 𝐵) → (∀𝑥 ∈ 𝐴 ∃!𝑦 𝑥𝐹𝑦 → ∀𝑥∃*𝑦 𝑥𝐹𝑦)) |
46 | 45 | imp 445 |
. . . . 5
⊢ ((𝐹 ⊆ (𝐴 × 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∃!𝑦 𝑥𝐹𝑦) → ∀𝑥∃*𝑦 𝑥𝐹𝑦) |
47 | | dffun6 5903 |
. . . . 5
⊢ (Fun
𝐹 ↔ (Rel 𝐹 ∧ ∀𝑥∃*𝑦 𝑥𝐹𝑦)) |
48 | 26, 46, 47 | sylanbrc 698 |
. . . 4
⊢ ((𝐹 ⊆ (𝐴 × 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∃!𝑦 𝑥𝐹𝑦) → Fun 𝐹) |
49 | | dmss 5323 |
. . . . . . 7
⊢ (𝐹 ⊆ (𝐴 × 𝐵) → dom 𝐹 ⊆ dom (𝐴 × 𝐵)) |
50 | | dmxpss 5565 |
. . . . . . 7
⊢ dom
(𝐴 × 𝐵) ⊆ 𝐴 |
51 | 49, 50 | syl6ss 3615 |
. . . . . 6
⊢ (𝐹 ⊆ (𝐴 × 𝐵) → dom 𝐹 ⊆ 𝐴) |
52 | | breq1 4656 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑧 → (𝑥𝐹𝑦 ↔ 𝑧𝐹𝑦)) |
53 | 52 | eubidv 2490 |
. . . . . . . . 9
⊢ (𝑥 = 𝑧 → (∃!𝑦 𝑥𝐹𝑦 ↔ ∃!𝑦 𝑧𝐹𝑦)) |
54 | 53 | rspccv 3306 |
. . . . . . . 8
⊢
(∀𝑥 ∈
𝐴 ∃!𝑦 𝑥𝐹𝑦 → (𝑧 ∈ 𝐴 → ∃!𝑦 𝑧𝐹𝑦)) |
55 | | euex 2494 |
. . . . . . . . 9
⊢
(∃!𝑦 𝑧𝐹𝑦 → ∃𝑦 𝑧𝐹𝑦) |
56 | | vex 3203 |
. . . . . . . . . 10
⊢ 𝑧 ∈ V |
57 | 56 | eldm 5321 |
. . . . . . . . 9
⊢ (𝑧 ∈ dom 𝐹 ↔ ∃𝑦 𝑧𝐹𝑦) |
58 | 55, 57 | sylibr 224 |
. . . . . . . 8
⊢
(∃!𝑦 𝑧𝐹𝑦 → 𝑧 ∈ dom 𝐹) |
59 | 54, 58 | syl6 35 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝐴 ∃!𝑦 𝑥𝐹𝑦 → (𝑧 ∈ 𝐴 → 𝑧 ∈ dom 𝐹)) |
60 | 59 | ssrdv 3609 |
. . . . . 6
⊢
(∀𝑥 ∈
𝐴 ∃!𝑦 𝑥𝐹𝑦 → 𝐴 ⊆ dom 𝐹) |
61 | 51, 60 | anim12i 590 |
. . . . 5
⊢ ((𝐹 ⊆ (𝐴 × 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∃!𝑦 𝑥𝐹𝑦) → (dom 𝐹 ⊆ 𝐴 ∧ 𝐴 ⊆ dom 𝐹)) |
62 | | eqss 3618 |
. . . . 5
⊢ (dom
𝐹 = 𝐴 ↔ (dom 𝐹 ⊆ 𝐴 ∧ 𝐴 ⊆ dom 𝐹)) |
63 | 61, 62 | sylibr 224 |
. . . 4
⊢ ((𝐹 ⊆ (𝐴 × 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∃!𝑦 𝑥𝐹𝑦) → dom 𝐹 = 𝐴) |
64 | | df-fn 5891 |
. . . 4
⊢ (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴)) |
65 | 48, 63, 64 | sylanbrc 698 |
. . 3
⊢ ((𝐹 ⊆ (𝐴 × 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∃!𝑦 𝑥𝐹𝑦) → 𝐹 Fn 𝐴) |
66 | | rnss 5354 |
. . . . 5
⊢ (𝐹 ⊆ (𝐴 × 𝐵) → ran 𝐹 ⊆ ran (𝐴 × 𝐵)) |
67 | | rnxpss 5566 |
. . . . 5
⊢ ran
(𝐴 × 𝐵) ⊆ 𝐵 |
68 | 66, 67 | syl6ss 3615 |
. . . 4
⊢ (𝐹 ⊆ (𝐴 × 𝐵) → ran 𝐹 ⊆ 𝐵) |
69 | 68 | adantr 481 |
. . 3
⊢ ((𝐹 ⊆ (𝐴 × 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∃!𝑦 𝑥𝐹𝑦) → ran 𝐹 ⊆ 𝐵) |
70 | | df-f 5892 |
. . 3
⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵)) |
71 | 65, 69, 70 | sylanbrc 698 |
. 2
⊢ ((𝐹 ⊆ (𝐴 × 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∃!𝑦 𝑥𝐹𝑦) → 𝐹:𝐴⟶𝐵) |
72 | 20, 71 | impbii 199 |
1
⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 ⊆ (𝐴 × 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∃!𝑦 𝑥𝐹𝑦)) |