Step | Hyp | Ref
| Expression |
1 | | fvfundmfvn0 6226 |
. . 3
⊢ ((𝐹‘𝑎) ≠ ∅ → (𝑎 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝑎}))) |
2 | 1 | ralimi 2952 |
. 2
⊢
(∀𝑎 ∈
𝐷 (𝐹‘𝑎) ≠ ∅ → ∀𝑎 ∈ 𝐷 (𝑎 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝑎}))) |
3 | | r19.26 3064 |
. . 3
⊢
(∀𝑎 ∈
𝐷 (𝑎 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝑎})) ↔ (∀𝑎 ∈ 𝐷 𝑎 ∈ dom 𝐹 ∧ ∀𝑎 ∈ 𝐷 Fun (𝐹 ↾ {𝑎}))) |
4 | | eleq1 2689 |
. . . . . 6
⊢ (𝑎 = 𝑝 → (𝑎 ∈ dom 𝐹 ↔ 𝑝 ∈ dom 𝐹)) |
5 | 4 | rspccv 3306 |
. . . . 5
⊢
(∀𝑎 ∈
𝐷 𝑎 ∈ dom 𝐹 → (𝑝 ∈ 𝐷 → 𝑝 ∈ dom 𝐹)) |
6 | 5 | ssrdv 3609 |
. . . 4
⊢
(∀𝑎 ∈
𝐷 𝑎 ∈ dom 𝐹 → 𝐷 ⊆ dom 𝐹) |
7 | | funrel 5905 |
. . . . . . . 8
⊢ (Fun
(𝐹 ↾ {𝑎}) → Rel (𝐹 ↾ {𝑎})) |
8 | 7 | ralimi 2952 |
. . . . . . 7
⊢
(∀𝑎 ∈
𝐷 Fun (𝐹 ↾ {𝑎}) → ∀𝑎 ∈ 𝐷 Rel (𝐹 ↾ {𝑎})) |
9 | | reliun 5239 |
. . . . . . 7
⊢ (Rel
∪ 𝑎 ∈ 𝐷 (𝐹 ↾ {𝑎}) ↔ ∀𝑎 ∈ 𝐷 Rel (𝐹 ↾ {𝑎})) |
10 | 8, 9 | sylibr 224 |
. . . . . 6
⊢
(∀𝑎 ∈
𝐷 Fun (𝐹 ↾ {𝑎}) → Rel ∪ 𝑎 ∈ 𝐷 (𝐹 ↾ {𝑎})) |
11 | | sneq 4187 |
. . . . . . . . . . . . . 14
⊢ (𝑎 = 𝑥 → {𝑎} = {𝑥}) |
12 | 11 | reseq2d 5396 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 𝑥 → (𝐹 ↾ {𝑎}) = (𝐹 ↾ {𝑥})) |
13 | 12 | funeqd 5910 |
. . . . . . . . . . . 12
⊢ (𝑎 = 𝑥 → (Fun (𝐹 ↾ {𝑎}) ↔ Fun (𝐹 ↾ {𝑥}))) |
14 | 13 | rspcva 3307 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝐷 ∧ ∀𝑎 ∈ 𝐷 Fun (𝐹 ↾ {𝑎})) → Fun (𝐹 ↾ {𝑥})) |
15 | | dffun5 5901 |
. . . . . . . . . . . 12
⊢ (Fun
(𝐹 ↾ {𝑥}) ↔ (Rel (𝐹 ↾ {𝑥}) ∧ ∀𝑤∃𝑦∀𝑧(〈𝑤, 𝑧〉 ∈ (𝐹 ↾ {𝑥}) → 𝑧 = 𝑦))) |
16 | | vex 3203 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑥 ∈ V |
17 | 16 | elsnres 5436 |
. . . . . . . . . . . . . . . . . 18
⊢
(〈𝑤, 𝑧〉 ∈ (𝐹 ↾ {𝑥}) ↔ ∃𝑎(〈𝑤, 𝑧〉 = 〈𝑥, 𝑎〉 ∧ 〈𝑥, 𝑎〉 ∈ 𝐹)) |
18 | 17 | imbi1i 339 |
. . . . . . . . . . . . . . . . 17
⊢
((〈𝑤, 𝑧〉 ∈ (𝐹 ↾ {𝑥}) → 𝑧 = 𝑦) ↔ (∃𝑎(〈𝑤, 𝑧〉 = 〈𝑥, 𝑎〉 ∧ 〈𝑥, 𝑎〉 ∈ 𝐹) → 𝑧 = 𝑦)) |
19 | 18 | albii 1747 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑧(〈𝑤, 𝑧〉 ∈ (𝐹 ↾ {𝑥}) → 𝑧 = 𝑦) ↔ ∀𝑧(∃𝑎(〈𝑤, 𝑧〉 = 〈𝑥, 𝑎〉 ∧ 〈𝑥, 𝑎〉 ∈ 𝐹) → 𝑧 = 𝑦)) |
20 | 19 | exbii 1774 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑦∀𝑧(〈𝑤, 𝑧〉 ∈ (𝐹 ↾ {𝑥}) → 𝑧 = 𝑦) ↔ ∃𝑦∀𝑧(∃𝑎(〈𝑤, 𝑧〉 = 〈𝑥, 𝑎〉 ∧ 〈𝑥, 𝑎〉 ∈ 𝐹) → 𝑧 = 𝑦)) |
21 | 20 | albii 1747 |
. . . . . . . . . . . . . 14
⊢
(∀𝑤∃𝑦∀𝑧(〈𝑤, 𝑧〉 ∈ (𝐹 ↾ {𝑥}) → 𝑧 = 𝑦) ↔ ∀𝑤∃𝑦∀𝑧(∃𝑎(〈𝑤, 𝑧〉 = 〈𝑥, 𝑎〉 ∧ 〈𝑥, 𝑎〉 ∈ 𝐹) → 𝑧 = 𝑦)) |
22 | | equcom 1945 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑎 = 𝑧 ↔ 𝑧 = 𝑎) |
23 | | opeq12 4404 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑤 = 𝑥 ∧ 𝑧 = 𝑎) → 〈𝑤, 𝑧〉 = 〈𝑥, 𝑎〉) |
24 | 23 | ex 450 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑤 = 𝑥 → (𝑧 = 𝑎 → 〈𝑤, 𝑧〉 = 〈𝑥, 𝑎〉)) |
25 | 22, 24 | syl5bi 232 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑤 = 𝑥 → (𝑎 = 𝑧 → 〈𝑤, 𝑧〉 = 〈𝑥, 𝑎〉)) |
26 | 25 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑤 = 𝑥 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) → (𝑎 = 𝑧 → 〈𝑤, 𝑧〉 = 〈𝑥, 𝑎〉)) |
27 | 26 | impcom 446 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑎 = 𝑧 ∧ (𝑤 = 𝑥 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹)) → 〈𝑤, 𝑧〉 = 〈𝑥, 𝑎〉) |
28 | | opeq2 4403 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑧 = 𝑎 → 〈𝑥, 𝑧〉 = 〈𝑥, 𝑎〉) |
29 | 28 | equcoms 1947 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑎 = 𝑧 → 〈𝑥, 𝑧〉 = 〈𝑥, 𝑎〉) |
30 | 29 | eleq1d 2686 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑎 = 𝑧 → (〈𝑥, 𝑧〉 ∈ 𝐹 ↔ 〈𝑥, 𝑎〉 ∈ 𝐹)) |
31 | 30 | biimpcd 239 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(〈𝑥, 𝑧〉 ∈ 𝐹 → (𝑎 = 𝑧 → 〈𝑥, 𝑎〉 ∈ 𝐹)) |
32 | 31 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑤 = 𝑥 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) → (𝑎 = 𝑧 → 〈𝑥, 𝑎〉 ∈ 𝐹)) |
33 | 32 | impcom 446 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑎 = 𝑧 ∧ (𝑤 = 𝑥 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹)) → 〈𝑥, 𝑎〉 ∈ 𝐹) |
34 | 27, 33 | jca 554 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑎 = 𝑧 ∧ (𝑤 = 𝑥 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹)) → (〈𝑤, 𝑧〉 = 〈𝑥, 𝑎〉 ∧ 〈𝑥, 𝑎〉 ∈ 𝐹)) |
35 | 34 | ex 450 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑎 = 𝑧 → ((𝑤 = 𝑥 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) → (〈𝑤, 𝑧〉 = 〈𝑥, 𝑎〉 ∧ 〈𝑥, 𝑎〉 ∈ 𝐹))) |
36 | 35 | spimev 2259 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑤 = 𝑥 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) → ∃𝑎(〈𝑤, 𝑧〉 = 〈𝑥, 𝑎〉 ∧ 〈𝑥, 𝑎〉 ∈ 𝐹)) |
37 | 36 | ex 450 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 = 𝑥 → (〈𝑥, 𝑧〉 ∈ 𝐹 → ∃𝑎(〈𝑤, 𝑧〉 = 〈𝑥, 𝑎〉 ∧ 〈𝑥, 𝑎〉 ∈ 𝐹))) |
38 | 37 | imim1d 82 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 = 𝑥 → ((∃𝑎(〈𝑤, 𝑧〉 = 〈𝑥, 𝑎〉 ∧ 〈𝑥, 𝑎〉 ∈ 𝐹) → 𝑧 = 𝑦) → (〈𝑥, 𝑧〉 ∈ 𝐹 → 𝑧 = 𝑦))) |
39 | 38 | alimdv 1845 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 = 𝑥 → (∀𝑧(∃𝑎(〈𝑤, 𝑧〉 = 〈𝑥, 𝑎〉 ∧ 〈𝑥, 𝑎〉 ∈ 𝐹) → 𝑧 = 𝑦) → ∀𝑧(〈𝑥, 𝑧〉 ∈ 𝐹 → 𝑧 = 𝑦))) |
40 | 39 | eximdv 1846 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = 𝑥 → (∃𝑦∀𝑧(∃𝑎(〈𝑤, 𝑧〉 = 〈𝑥, 𝑎〉 ∧ 〈𝑥, 𝑎〉 ∈ 𝐹) → 𝑧 = 𝑦) → ∃𝑦∀𝑧(〈𝑥, 𝑧〉 ∈ 𝐹 → 𝑧 = 𝑦))) |
41 | 40 | spimvw 1927 |
. . . . . . . . . . . . . 14
⊢
(∀𝑤∃𝑦∀𝑧(∃𝑎(〈𝑤, 𝑧〉 = 〈𝑥, 𝑎〉 ∧ 〈𝑥, 𝑎〉 ∈ 𝐹) → 𝑧 = 𝑦) → ∃𝑦∀𝑧(〈𝑥, 𝑧〉 ∈ 𝐹 → 𝑧 = 𝑦)) |
42 | 21, 41 | sylbi 207 |
. . . . . . . . . . . . 13
⊢
(∀𝑤∃𝑦∀𝑧(〈𝑤, 𝑧〉 ∈ (𝐹 ↾ {𝑥}) → 𝑧 = 𝑦) → ∃𝑦∀𝑧(〈𝑥, 𝑧〉 ∈ 𝐹 → 𝑧 = 𝑦)) |
43 | 42 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((Rel
(𝐹 ↾ {𝑥}) ∧ ∀𝑤∃𝑦∀𝑧(〈𝑤, 𝑧〉 ∈ (𝐹 ↾ {𝑥}) → 𝑧 = 𝑦)) → ∃𝑦∀𝑧(〈𝑥, 𝑧〉 ∈ 𝐹 → 𝑧 = 𝑦)) |
44 | 15, 43 | sylbi 207 |
. . . . . . . . . . 11
⊢ (Fun
(𝐹 ↾ {𝑥}) → ∃𝑦∀𝑧(〈𝑥, 𝑧〉 ∈ 𝐹 → 𝑧 = 𝑦)) |
45 | 14, 44 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝐷 ∧ ∀𝑎 ∈ 𝐷 Fun (𝐹 ↾ {𝑎})) → ∃𝑦∀𝑧(〈𝑥, 𝑧〉 ∈ 𝐹 → 𝑧 = 𝑦)) |
46 | 45 | expcom 451 |
. . . . . . . . 9
⊢
(∀𝑎 ∈
𝐷 Fun (𝐹 ↾ {𝑎}) → (𝑥 ∈ 𝐷 → ∃𝑦∀𝑧(〈𝑥, 𝑧〉 ∈ 𝐹 → 𝑧 = 𝑦))) |
47 | | ancomst 468 |
. . . . . . . . . . . . 13
⊢
(((〈𝑥, 𝑧〉 ∈ 𝐹 ∧ 𝑥 ∈ 𝐷) → 𝑧 = 𝑦) ↔ ((𝑥 ∈ 𝐷 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) → 𝑧 = 𝑦)) |
48 | | impexp 462 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ 𝐷 ∧ 〈𝑥, 𝑧〉 ∈ 𝐹) → 𝑧 = 𝑦) ↔ (𝑥 ∈ 𝐷 → (〈𝑥, 𝑧〉 ∈ 𝐹 → 𝑧 = 𝑦))) |
49 | 47, 48 | bitri 264 |
. . . . . . . . . . . 12
⊢
(((〈𝑥, 𝑧〉 ∈ 𝐹 ∧ 𝑥 ∈ 𝐷) → 𝑧 = 𝑦) ↔ (𝑥 ∈ 𝐷 → (〈𝑥, 𝑧〉 ∈ 𝐹 → 𝑧 = 𝑦))) |
50 | 49 | albii 1747 |
. . . . . . . . . . 11
⊢
(∀𝑧((〈𝑥, 𝑧〉 ∈ 𝐹 ∧ 𝑥 ∈ 𝐷) → 𝑧 = 𝑦) ↔ ∀𝑧(𝑥 ∈ 𝐷 → (〈𝑥, 𝑧〉 ∈ 𝐹 → 𝑧 = 𝑦))) |
51 | 50 | exbii 1774 |
. . . . . . . . . 10
⊢
(∃𝑦∀𝑧((〈𝑥, 𝑧〉 ∈ 𝐹 ∧ 𝑥 ∈ 𝐷) → 𝑧 = 𝑦) ↔ ∃𝑦∀𝑧(𝑥 ∈ 𝐷 → (〈𝑥, 𝑧〉 ∈ 𝐹 → 𝑧 = 𝑦))) |
52 | | 19.21v 1868 |
. . . . . . . . . . 11
⊢
(∀𝑧(𝑥 ∈ 𝐷 → (〈𝑥, 𝑧〉 ∈ 𝐹 → 𝑧 = 𝑦)) ↔ (𝑥 ∈ 𝐷 → ∀𝑧(〈𝑥, 𝑧〉 ∈ 𝐹 → 𝑧 = 𝑦))) |
53 | 52 | exbii 1774 |
. . . . . . . . . 10
⊢
(∃𝑦∀𝑧(𝑥 ∈ 𝐷 → (〈𝑥, 𝑧〉 ∈ 𝐹 → 𝑧 = 𝑦)) ↔ ∃𝑦(𝑥 ∈ 𝐷 → ∀𝑧(〈𝑥, 𝑧〉 ∈ 𝐹 → 𝑧 = 𝑦))) |
54 | | 19.37v 1910 |
. . . . . . . . . 10
⊢
(∃𝑦(𝑥 ∈ 𝐷 → ∀𝑧(〈𝑥, 𝑧〉 ∈ 𝐹 → 𝑧 = 𝑦)) ↔ (𝑥 ∈ 𝐷 → ∃𝑦∀𝑧(〈𝑥, 𝑧〉 ∈ 𝐹 → 𝑧 = 𝑦))) |
55 | 51, 53, 54 | 3bitri 286 |
. . . . . . . . 9
⊢
(∃𝑦∀𝑧((〈𝑥, 𝑧〉 ∈ 𝐹 ∧ 𝑥 ∈ 𝐷) → 𝑧 = 𝑦) ↔ (𝑥 ∈ 𝐷 → ∃𝑦∀𝑧(〈𝑥, 𝑧〉 ∈ 𝐹 → 𝑧 = 𝑦))) |
56 | 46, 55 | sylibr 224 |
. . . . . . . 8
⊢
(∀𝑎 ∈
𝐷 Fun (𝐹 ↾ {𝑎}) → ∃𝑦∀𝑧((〈𝑥, 𝑧〉 ∈ 𝐹 ∧ 𝑥 ∈ 𝐷) → 𝑧 = 𝑦)) |
57 | 56 | alrimiv 1855 |
. . . . . . 7
⊢
(∀𝑎 ∈
𝐷 Fun (𝐹 ↾ {𝑎}) → ∀𝑥∃𝑦∀𝑧((〈𝑥, 𝑧〉 ∈ 𝐹 ∧ 𝑥 ∈ 𝐷) → 𝑧 = 𝑦)) |
58 | | resiun2 5418 |
. . . . . . . . . . . . . 14
⊢ (𝐹 ↾ ∪ 𝑎 ∈ 𝐷 {𝑎}) = ∪
𝑎 ∈ 𝐷 (𝐹 ↾ {𝑎}) |
59 | 58 | eqcomi 2631 |
. . . . . . . . . . . . 13
⊢ ∪ 𝑎 ∈ 𝐷 (𝐹 ↾ {𝑎}) = (𝐹 ↾ ∪
𝑎 ∈ 𝐷 {𝑎}) |
60 | 59 | eleq2i 2693 |
. . . . . . . . . . . 12
⊢
(〈𝑥, 𝑧〉 ∈ ∪ 𝑎 ∈ 𝐷 (𝐹 ↾ {𝑎}) ↔ 〈𝑥, 𝑧〉 ∈ (𝐹 ↾ ∪
𝑎 ∈ 𝐷 {𝑎})) |
61 | | iunid 4575 |
. . . . . . . . . . . . . 14
⊢ ∪ 𝑎 ∈ 𝐷 {𝑎} = 𝐷 |
62 | 61 | reseq2i 5393 |
. . . . . . . . . . . . 13
⊢ (𝐹 ↾ ∪ 𝑎 ∈ 𝐷 {𝑎}) = (𝐹 ↾ 𝐷) |
63 | 62 | eleq2i 2693 |
. . . . . . . . . . . 12
⊢
(〈𝑥, 𝑧〉 ∈ (𝐹 ↾ ∪
𝑎 ∈ 𝐷 {𝑎}) ↔ 〈𝑥, 𝑧〉 ∈ (𝐹 ↾ 𝐷)) |
64 | | vex 3203 |
. . . . . . . . . . . . 13
⊢ 𝑧 ∈ V |
65 | 64 | opelres 5401 |
. . . . . . . . . . . 12
⊢
(〈𝑥, 𝑧〉 ∈ (𝐹 ↾ 𝐷) ↔ (〈𝑥, 𝑧〉 ∈ 𝐹 ∧ 𝑥 ∈ 𝐷)) |
66 | 60, 63, 65 | 3bitri 286 |
. . . . . . . . . . 11
⊢
(〈𝑥, 𝑧〉 ∈ ∪ 𝑎 ∈ 𝐷 (𝐹 ↾ {𝑎}) ↔ (〈𝑥, 𝑧〉 ∈ 𝐹 ∧ 𝑥 ∈ 𝐷)) |
67 | 66 | imbi1i 339 |
. . . . . . . . . 10
⊢
((〈𝑥, 𝑧〉 ∈ ∪ 𝑎 ∈ 𝐷 (𝐹 ↾ {𝑎}) → 𝑧 = 𝑦) ↔ ((〈𝑥, 𝑧〉 ∈ 𝐹 ∧ 𝑥 ∈ 𝐷) → 𝑧 = 𝑦)) |
68 | 67 | albii 1747 |
. . . . . . . . 9
⊢
(∀𝑧(〈𝑥, 𝑧〉 ∈ ∪ 𝑎 ∈ 𝐷 (𝐹 ↾ {𝑎}) → 𝑧 = 𝑦) ↔ ∀𝑧((〈𝑥, 𝑧〉 ∈ 𝐹 ∧ 𝑥 ∈ 𝐷) → 𝑧 = 𝑦)) |
69 | 68 | exbii 1774 |
. . . . . . . 8
⊢
(∃𝑦∀𝑧(〈𝑥, 𝑧〉 ∈ ∪ 𝑎 ∈ 𝐷 (𝐹 ↾ {𝑎}) → 𝑧 = 𝑦) ↔ ∃𝑦∀𝑧((〈𝑥, 𝑧〉 ∈ 𝐹 ∧ 𝑥 ∈ 𝐷) → 𝑧 = 𝑦)) |
70 | 69 | albii 1747 |
. . . . . . 7
⊢
(∀𝑥∃𝑦∀𝑧(〈𝑥, 𝑧〉 ∈ ∪ 𝑎 ∈ 𝐷 (𝐹 ↾ {𝑎}) → 𝑧 = 𝑦) ↔ ∀𝑥∃𝑦∀𝑧((〈𝑥, 𝑧〉 ∈ 𝐹 ∧ 𝑥 ∈ 𝐷) → 𝑧 = 𝑦)) |
71 | 57, 70 | sylibr 224 |
. . . . . 6
⊢
(∀𝑎 ∈
𝐷 Fun (𝐹 ↾ {𝑎}) → ∀𝑥∃𝑦∀𝑧(〈𝑥, 𝑧〉 ∈ ∪ 𝑎 ∈ 𝐷 (𝐹 ↾ {𝑎}) → 𝑧 = 𝑦)) |
72 | | dffun5 5901 |
. . . . . 6
⊢ (Fun
∪ 𝑎 ∈ 𝐷 (𝐹 ↾ {𝑎}) ↔ (Rel ∪ 𝑎 ∈ 𝐷 (𝐹 ↾ {𝑎}) ∧ ∀𝑥∃𝑦∀𝑧(〈𝑥, 𝑧〉 ∈ ∪ 𝑎 ∈ 𝐷 (𝐹 ↾ {𝑎}) → 𝑧 = 𝑦))) |
73 | 10, 71, 72 | sylanbrc 698 |
. . . . 5
⊢
(∀𝑎 ∈
𝐷 Fun (𝐹 ↾ {𝑎}) → Fun ∪ 𝑎 ∈ 𝐷 (𝐹 ↾ {𝑎})) |
74 | 61 | eqcomi 2631 |
. . . . . . . 8
⊢ 𝐷 = ∪ 𝑎 ∈ 𝐷 {𝑎} |
75 | 74 | reseq2i 5393 |
. . . . . . 7
⊢ (𝐹 ↾ 𝐷) = (𝐹 ↾ ∪
𝑎 ∈ 𝐷 {𝑎}) |
76 | 75 | funeqi 5909 |
. . . . . 6
⊢ (Fun
(𝐹 ↾ 𝐷) ↔ Fun (𝐹 ↾ ∪
𝑎 ∈ 𝐷 {𝑎})) |
77 | 58 | funeqi 5909 |
. . . . . 6
⊢ (Fun
(𝐹 ↾ ∪ 𝑎 ∈ 𝐷 {𝑎}) ↔ Fun ∪ 𝑎 ∈ 𝐷 (𝐹 ↾ {𝑎})) |
78 | 76, 77 | bitri 264 |
. . . . 5
⊢ (Fun
(𝐹 ↾ 𝐷) ↔ Fun ∪ 𝑎 ∈ 𝐷 (𝐹 ↾ {𝑎})) |
79 | 73, 78 | sylibr 224 |
. . . 4
⊢
(∀𝑎 ∈
𝐷 Fun (𝐹 ↾ {𝑎}) → Fun (𝐹 ↾ 𝐷)) |
80 | 6, 79 | anim12i 590 |
. . 3
⊢
((∀𝑎 ∈
𝐷 𝑎 ∈ dom 𝐹 ∧ ∀𝑎 ∈ 𝐷 Fun (𝐹 ↾ {𝑎})) → (𝐷 ⊆ dom 𝐹 ∧ Fun (𝐹 ↾ 𝐷))) |
81 | 3, 80 | sylbi 207 |
. 2
⊢
(∀𝑎 ∈
𝐷 (𝑎 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝑎})) → (𝐷 ⊆ dom 𝐹 ∧ Fun (𝐹 ↾ 𝐷))) |
82 | 2, 81 | syl 17 |
1
⊢
(∀𝑎 ∈
𝐷 (𝐹‘𝑎) ≠ ∅ → (𝐷 ⊆ dom 𝐹 ∧ Fun (𝐹 ↾ 𝐷))) |