Proof of Theorem setsfun
Step | Hyp | Ref
| Expression |
1 | | funres 6375 |
. . . . 5
⊢ (Fun
𝐺 → Fun (𝐺 ↾ (V ∖ dom
{〈𝐼, 𝐸〉}))) |
2 | 1 | adantl 485 |
. . . 4
⊢ ((𝐺 ∈ 𝑉 ∧ Fun 𝐺) → Fun (𝐺 ↾ (V ∖ dom {〈𝐼, 𝐸〉}))) |
3 | 2 | adantr 484 |
. . 3
⊢ (((𝐺 ∈ 𝑉 ∧ Fun 𝐺) ∧ (𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊)) → Fun (𝐺 ↾ (V ∖ dom {〈𝐼, 𝐸〉}))) |
4 | | funsng 6384 |
. . . 4
⊢ ((𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊) → Fun {〈𝐼, 𝐸〉}) |
5 | 4 | adantl 485 |
. . 3
⊢ (((𝐺 ∈ 𝑉 ∧ Fun 𝐺) ∧ (𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊)) → Fun {〈𝐼, 𝐸〉}) |
6 | | dmres 5841 |
. . . . . 6
⊢ dom
(𝐺 ↾ (V ∖ dom
{〈𝐼, 𝐸〉})) = ((V ∖ dom {〈𝐼, 𝐸〉}) ∩ dom 𝐺) |
7 | 6 | ineq1i 4097 |
. . . . 5
⊢ (dom
(𝐺 ↾ (V ∖ dom
{〈𝐼, 𝐸〉})) ∩ dom {〈𝐼, 𝐸〉}) = (((V ∖ dom {〈𝐼, 𝐸〉}) ∩ dom 𝐺) ∩ dom {〈𝐼, 𝐸〉}) |
8 | | in32 4110 |
. . . . . 6
⊢ (((V
∖ dom {〈𝐼, 𝐸〉}) ∩ dom 𝐺) ∩ dom {〈𝐼, 𝐸〉}) = (((V ∖ dom {〈𝐼, 𝐸〉}) ∩ dom {〈𝐼, 𝐸〉}) ∩ dom 𝐺) |
9 | | disjdifr 4359 |
. . . . . . 7
⊢ ((V
∖ dom {〈𝐼, 𝐸〉}) ∩ dom {〈𝐼, 𝐸〉}) = ∅ |
10 | 9 | ineq1i 4097 |
. . . . . 6
⊢ (((V
∖ dom {〈𝐼, 𝐸〉}) ∩ dom {〈𝐼, 𝐸〉}) ∩ dom 𝐺) = (∅ ∩ dom 𝐺) |
11 | | 0in 4279 |
. . . . . 6
⊢ (∅
∩ dom 𝐺) =
∅ |
12 | 8, 10, 11 | 3eqtri 2765 |
. . . . 5
⊢ (((V
∖ dom {〈𝐼, 𝐸〉}) ∩ dom 𝐺) ∩ dom {〈𝐼, 𝐸〉}) = ∅ |
13 | 7, 12 | eqtri 2761 |
. . . 4
⊢ (dom
(𝐺 ↾ (V ∖ dom
{〈𝐼, 𝐸〉})) ∩ dom {〈𝐼, 𝐸〉}) = ∅ |
14 | 13 | a1i 11 |
. . 3
⊢ (((𝐺 ∈ 𝑉 ∧ Fun 𝐺) ∧ (𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊)) → (dom (𝐺 ↾ (V ∖ dom {〈𝐼, 𝐸〉})) ∩ dom {〈𝐼, 𝐸〉}) = ∅) |
15 | | funun 6379 |
. . 3
⊢ (((Fun
(𝐺 ↾ (V ∖ dom
{〈𝐼, 𝐸〉})) ∧ Fun {〈𝐼, 𝐸〉}) ∧ (dom (𝐺 ↾ (V ∖ dom {〈𝐼, 𝐸〉})) ∩ dom {〈𝐼, 𝐸〉}) = ∅) → Fun ((𝐺 ↾ (V ∖ dom
{〈𝐼, 𝐸〉})) ∪ {〈𝐼, 𝐸〉})) |
16 | 3, 5, 14, 15 | syl21anc 837 |
. 2
⊢ (((𝐺 ∈ 𝑉 ∧ Fun 𝐺) ∧ (𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊)) → Fun ((𝐺 ↾ (V ∖ dom {〈𝐼, 𝐸〉})) ∪ {〈𝐼, 𝐸〉})) |
17 | | opex 5319 |
. . . . . 6
⊢
〈𝐼, 𝐸〉 ∈ V |
18 | 17 | a1i 11 |
. . . . 5
⊢ (Fun
𝐺 → 〈𝐼, 𝐸〉 ∈ V) |
19 | | setsvalg 16608 |
. . . . 5
⊢ ((𝐺 ∈ 𝑉 ∧ 〈𝐼, 𝐸〉 ∈ V) → (𝐺 sSet 〈𝐼, 𝐸〉) = ((𝐺 ↾ (V ∖ dom {〈𝐼, 𝐸〉})) ∪ {〈𝐼, 𝐸〉})) |
20 | 18, 19 | sylan2 596 |
. . . 4
⊢ ((𝐺 ∈ 𝑉 ∧ Fun 𝐺) → (𝐺 sSet 〈𝐼, 𝐸〉) = ((𝐺 ↾ (V ∖ dom {〈𝐼, 𝐸〉})) ∪ {〈𝐼, 𝐸〉})) |
21 | 20 | funeqd 6355 |
. . 3
⊢ ((𝐺 ∈ 𝑉 ∧ Fun 𝐺) → (Fun (𝐺 sSet 〈𝐼, 𝐸〉) ↔ Fun ((𝐺 ↾ (V ∖ dom {〈𝐼, 𝐸〉})) ∪ {〈𝐼, 𝐸〉}))) |
22 | 21 | adantr 484 |
. 2
⊢ (((𝐺 ∈ 𝑉 ∧ Fun 𝐺) ∧ (𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊)) → (Fun (𝐺 sSet 〈𝐼, 𝐸〉) ↔ Fun ((𝐺 ↾ (V ∖ dom {〈𝐼, 𝐸〉})) ∪ {〈𝐼, 𝐸〉}))) |
23 | 16, 22 | mpbird 260 |
1
⊢ (((𝐺 ∈ 𝑉 ∧ Fun 𝐺) ∧ (𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊)) → Fun (𝐺 sSet 〈𝐼, 𝐸〉)) |