Step | Hyp | Ref
| Expression |
1 | | fssxp 6200 |
. . 3
⊢ (𝐹:𝐴⟶𝐵 → 𝐹 ⊆ (𝐴 × 𝐵)) |
2 | | ffun 6188 |
. . . . . . . 8
⊢ (𝐹:𝐴⟶𝐵 → Fun 𝐹) |
3 | | fdm 6191 |
. . . . . . . . . 10
⊢ (𝐹:𝐴⟶𝐵 → dom 𝐹 = 𝐴) |
4 | 3 | eleq2d 2836 |
. . . . . . . . 9
⊢ (𝐹:𝐴⟶𝐵 → (𝑥 ∈ dom 𝐹 ↔ 𝑥 ∈ 𝐴)) |
5 | 4 | biimpar 463 |
. . . . . . . 8
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ dom 𝐹) |
6 | | funfvop 6472 |
. . . . . . . 8
⊢ ((Fun
𝐹 ∧ 𝑥 ∈ dom 𝐹) → 〈𝑥, (𝐹‘𝑥)〉 ∈ 𝐹) |
7 | 2, 5, 6 | syl2an2r 664 |
. . . . . . 7
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → 〈𝑥, (𝐹‘𝑥)〉 ∈ 𝐹) |
8 | | df-br 4787 |
. . . . . . 7
⊢ (𝑥𝐹(𝐹‘𝑥) ↔ 〈𝑥, (𝐹‘𝑥)〉 ∈ 𝐹) |
9 | 7, 8 | sylibr 224 |
. . . . . 6
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → 𝑥𝐹(𝐹‘𝑥)) |
10 | | fvex 6342 |
. . . . . . 7
⊢ (𝐹‘𝑥) ∈ V |
11 | | breq2 4790 |
. . . . . . 7
⊢ (𝑦 = (𝐹‘𝑥) → (𝑥𝐹𝑦 ↔ 𝑥𝐹(𝐹‘𝑥))) |
12 | 10, 11 | spcev 3451 |
. . . . . 6
⊢ (𝑥𝐹(𝐹‘𝑥) → ∃𝑦 𝑥𝐹𝑦) |
13 | 9, 12 | syl 17 |
. . . . 5
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → ∃𝑦 𝑥𝐹𝑦) |
14 | | funmo 6047 |
. . . . . . 7
⊢ (Fun
𝐹 → ∃*𝑦 𝑥𝐹𝑦) |
15 | 2, 14 | syl 17 |
. . . . . 6
⊢ (𝐹:𝐴⟶𝐵 → ∃*𝑦 𝑥𝐹𝑦) |
16 | 15 | adantr 466 |
. . . . 5
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → ∃*𝑦 𝑥𝐹𝑦) |
17 | | eu5 2644 |
. . . . 5
⊢
(∃!𝑦 𝑥𝐹𝑦 ↔ (∃𝑦 𝑥𝐹𝑦 ∧ ∃*𝑦 𝑥𝐹𝑦)) |
18 | 13, 16, 17 | sylanbrc 572 |
. . . 4
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → ∃!𝑦 𝑥𝐹𝑦) |
19 | 18 | ralrimiva 3115 |
. . 3
⊢ (𝐹:𝐴⟶𝐵 → ∀𝑥 ∈ 𝐴 ∃!𝑦 𝑥𝐹𝑦) |
20 | 1, 19 | jca 501 |
. 2
⊢ (𝐹:𝐴⟶𝐵 → (𝐹 ⊆ (𝐴 × 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∃!𝑦 𝑥𝐹𝑦)) |
21 | | xpss 5265 |
. . . . . . . 8
⊢ (𝐴 × 𝐵) ⊆ (V × V) |
22 | | sstr 3760 |
. . . . . . . 8
⊢ ((𝐹 ⊆ (𝐴 × 𝐵) ∧ (𝐴 × 𝐵) ⊆ (V × V)) → 𝐹 ⊆ (V ×
V)) |
23 | 21, 22 | mpan2 671 |
. . . . . . 7
⊢ (𝐹 ⊆ (𝐴 × 𝐵) → 𝐹 ⊆ (V × V)) |
24 | | df-rel 5256 |
. . . . . . 7
⊢ (Rel
𝐹 ↔ 𝐹 ⊆ (V × V)) |
25 | 23, 24 | sylibr 224 |
. . . . . 6
⊢ (𝐹 ⊆ (𝐴 × 𝐵) → Rel 𝐹) |
26 | 25 | adantr 466 |
. . . . 5
⊢ ((𝐹 ⊆ (𝐴 × 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∃!𝑦 𝑥𝐹𝑦) → Rel 𝐹) |
27 | | df-ral 3066 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝐴 ∃!𝑦 𝑥𝐹𝑦 ↔ ∀𝑥(𝑥 ∈ 𝐴 → ∃!𝑦 𝑥𝐹𝑦)) |
28 | | eumo 2647 |
. . . . . . . . . . . 12
⊢
(∃!𝑦 𝑥𝐹𝑦 → ∃*𝑦 𝑥𝐹𝑦) |
29 | 28 | imim2i 16 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝐴 → ∃!𝑦 𝑥𝐹𝑦) → (𝑥 ∈ 𝐴 → ∃*𝑦 𝑥𝐹𝑦)) |
30 | 29 | adantl 467 |
. . . . . . . . . 10
⊢ ((𝐹 ⊆ (𝐴 × 𝐵) ∧ (𝑥 ∈ 𝐴 → ∃!𝑦 𝑥𝐹𝑦)) → (𝑥 ∈ 𝐴 → ∃*𝑦 𝑥𝐹𝑦)) |
31 | | df-br 4787 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥𝐹𝑦 ↔ 〈𝑥, 𝑦〉 ∈ 𝐹) |
32 | | ssel 3746 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹 ⊆ (𝐴 × 𝐵) → (〈𝑥, 𝑦〉 ∈ 𝐹 → 〈𝑥, 𝑦〉 ∈ (𝐴 × 𝐵))) |
33 | 31, 32 | syl5bi 232 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 ⊆ (𝐴 × 𝐵) → (𝑥𝐹𝑦 → 〈𝑥, 𝑦〉 ∈ (𝐴 × 𝐵))) |
34 | | opelxp1 5290 |
. . . . . . . . . . . . . . 15
⊢
(〈𝑥, 𝑦〉 ∈ (𝐴 × 𝐵) → 𝑥 ∈ 𝐴) |
35 | 33, 34 | syl6 35 |
. . . . . . . . . . . . . 14
⊢ (𝐹 ⊆ (𝐴 × 𝐵) → (𝑥𝐹𝑦 → 𝑥 ∈ 𝐴)) |
36 | 35 | exlimdv 2013 |
. . . . . . . . . . . . 13
⊢ (𝐹 ⊆ (𝐴 × 𝐵) → (∃𝑦 𝑥𝐹𝑦 → 𝑥 ∈ 𝐴)) |
37 | 36 | con3d 149 |
. . . . . . . . . . . 12
⊢ (𝐹 ⊆ (𝐴 × 𝐵) → (¬ 𝑥 ∈ 𝐴 → ¬ ∃𝑦 𝑥𝐹𝑦)) |
38 | | exmo 2643 |
. . . . . . . . . . . . 13
⊢
(∃𝑦 𝑥𝐹𝑦 ∨ ∃*𝑦 𝑥𝐹𝑦) |
39 | 38 | ori 850 |
. . . . . . . . . . . 12
⊢ (¬
∃𝑦 𝑥𝐹𝑦 → ∃*𝑦 𝑥𝐹𝑦) |
40 | 37, 39 | syl6 35 |
. . . . . . . . . . 11
⊢ (𝐹 ⊆ (𝐴 × 𝐵) → (¬ 𝑥 ∈ 𝐴 → ∃*𝑦 𝑥𝐹𝑦)) |
41 | 40 | adantr 466 |
. . . . . . . . . 10
⊢ ((𝐹 ⊆ (𝐴 × 𝐵) ∧ (𝑥 ∈ 𝐴 → ∃!𝑦 𝑥𝐹𝑦)) → (¬ 𝑥 ∈ 𝐴 → ∃*𝑦 𝑥𝐹𝑦)) |
42 | 30, 41 | pm2.61d 171 |
. . . . . . . . 9
⊢ ((𝐹 ⊆ (𝐴 × 𝐵) ∧ (𝑥 ∈ 𝐴 → ∃!𝑦 𝑥𝐹𝑦)) → ∃*𝑦 𝑥𝐹𝑦) |
43 | 42 | ex 397 |
. . . . . . . 8
⊢ (𝐹 ⊆ (𝐴 × 𝐵) → ((𝑥 ∈ 𝐴 → ∃!𝑦 𝑥𝐹𝑦) → ∃*𝑦 𝑥𝐹𝑦)) |
44 | 43 | alimdv 1997 |
. . . . . . 7
⊢ (𝐹 ⊆ (𝐴 × 𝐵) → (∀𝑥(𝑥 ∈ 𝐴 → ∃!𝑦 𝑥𝐹𝑦) → ∀𝑥∃*𝑦 𝑥𝐹𝑦)) |
45 | 27, 44 | syl5bi 232 |
. . . . . 6
⊢ (𝐹 ⊆ (𝐴 × 𝐵) → (∀𝑥 ∈ 𝐴 ∃!𝑦 𝑥𝐹𝑦 → ∀𝑥∃*𝑦 𝑥𝐹𝑦)) |
46 | 45 | imp 393 |
. . . . 5
⊢ ((𝐹 ⊆ (𝐴 × 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∃!𝑦 𝑥𝐹𝑦) → ∀𝑥∃*𝑦 𝑥𝐹𝑦) |
47 | | dffun6 6046 |
. . . . 5
⊢ (Fun
𝐹 ↔ (Rel 𝐹 ∧ ∀𝑥∃*𝑦 𝑥𝐹𝑦)) |
48 | 26, 46, 47 | sylanbrc 572 |
. . . 4
⊢ ((𝐹 ⊆ (𝐴 × 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∃!𝑦 𝑥𝐹𝑦) → Fun 𝐹) |
49 | | dmss 5461 |
. . . . . . 7
⊢ (𝐹 ⊆ (𝐴 × 𝐵) → dom 𝐹 ⊆ dom (𝐴 × 𝐵)) |
50 | | dmxpss 5706 |
. . . . . . 7
⊢ dom
(𝐴 × 𝐵) ⊆ 𝐴 |
51 | 49, 50 | syl6ss 3764 |
. . . . . 6
⊢ (𝐹 ⊆ (𝐴 × 𝐵) → dom 𝐹 ⊆ 𝐴) |
52 | | breq1 4789 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑧 → (𝑥𝐹𝑦 ↔ 𝑧𝐹𝑦)) |
53 | 52 | eubidv 2638 |
. . . . . . . . 9
⊢ (𝑥 = 𝑧 → (∃!𝑦 𝑥𝐹𝑦 ↔ ∃!𝑦 𝑧𝐹𝑦)) |
54 | 53 | rspccv 3457 |
. . . . . . . 8
⊢
(∀𝑥 ∈
𝐴 ∃!𝑦 𝑥𝐹𝑦 → (𝑧 ∈ 𝐴 → ∃!𝑦 𝑧𝐹𝑦)) |
55 | | euex 2642 |
. . . . . . . . 9
⊢
(∃!𝑦 𝑧𝐹𝑦 → ∃𝑦 𝑧𝐹𝑦) |
56 | | vex 3354 |
. . . . . . . . . 10
⊢ 𝑧 ∈ V |
57 | 56 | eldm 5459 |
. . . . . . . . 9
⊢ (𝑧 ∈ dom 𝐹 ↔ ∃𝑦 𝑧𝐹𝑦) |
58 | 55, 57 | sylibr 224 |
. . . . . . . 8
⊢
(∃!𝑦 𝑧𝐹𝑦 → 𝑧 ∈ dom 𝐹) |
59 | 54, 58 | syl6 35 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝐴 ∃!𝑦 𝑥𝐹𝑦 → (𝑧 ∈ 𝐴 → 𝑧 ∈ dom 𝐹)) |
60 | 59 | ssrdv 3758 |
. . . . . 6
⊢
(∀𝑥 ∈
𝐴 ∃!𝑦 𝑥𝐹𝑦 → 𝐴 ⊆ dom 𝐹) |
61 | 51, 60 | anim12i 600 |
. . . . 5
⊢ ((𝐹 ⊆ (𝐴 × 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∃!𝑦 𝑥𝐹𝑦) → (dom 𝐹 ⊆ 𝐴 ∧ 𝐴 ⊆ dom 𝐹)) |
62 | | eqss 3767 |
. . . . 5
⊢ (dom
𝐹 = 𝐴 ↔ (dom 𝐹 ⊆ 𝐴 ∧ 𝐴 ⊆ dom 𝐹)) |
63 | 61, 62 | sylibr 224 |
. . . 4
⊢ ((𝐹 ⊆ (𝐴 × 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∃!𝑦 𝑥𝐹𝑦) → dom 𝐹 = 𝐴) |
64 | | df-fn 6034 |
. . . 4
⊢ (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴)) |
65 | 48, 63, 64 | sylanbrc 572 |
. . 3
⊢ ((𝐹 ⊆ (𝐴 × 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∃!𝑦 𝑥𝐹𝑦) → 𝐹 Fn 𝐴) |
66 | | rnss 5492 |
. . . . 5
⊢ (𝐹 ⊆ (𝐴 × 𝐵) → ran 𝐹 ⊆ ran (𝐴 × 𝐵)) |
67 | | rnxpss 5707 |
. . . . 5
⊢ ran
(𝐴 × 𝐵) ⊆ 𝐵 |
68 | 66, 67 | syl6ss 3764 |
. . . 4
⊢ (𝐹 ⊆ (𝐴 × 𝐵) → ran 𝐹 ⊆ 𝐵) |
69 | 68 | adantr 466 |
. . 3
⊢ ((𝐹 ⊆ (𝐴 × 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∃!𝑦 𝑥𝐹𝑦) → ran 𝐹 ⊆ 𝐵) |
70 | | df-f 6035 |
. . 3
⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵)) |
71 | 65, 69, 70 | sylanbrc 572 |
. 2
⊢ ((𝐹 ⊆ (𝐴 × 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∃!𝑦 𝑥𝐹𝑦) → 𝐹:𝐴⟶𝐵) |
72 | 20, 71 | impbii 199 |
1
⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 ⊆ (𝐴 × 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∃!𝑦 𝑥𝐹𝑦)) |