Proof of Theorem setsfun
Step | Hyp | Ref
| Expression |
1 | | funres 5237 |
. . . 4
⊢ (Fun
𝐺 → Fun (𝐺 ↾ (V ∖ dom
{〈𝐼, 𝐸〉}))) |
2 | 1 | ad2antlr 486 |
. . 3
⊢ (((𝐺 ∈ 𝑉 ∧ Fun 𝐺) ∧ (𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊)) → Fun (𝐺 ↾ (V ∖ dom {〈𝐼, 𝐸〉}))) |
3 | | funsng 5242 |
. . . 4
⊢ ((𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊) → Fun {〈𝐼, 𝐸〉}) |
4 | 3 | adantl 275 |
. . 3
⊢ (((𝐺 ∈ 𝑉 ∧ Fun 𝐺) ∧ (𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊)) → Fun {〈𝐼, 𝐸〉}) |
5 | | dmres 4910 |
. . . . . 6
⊢ dom
(𝐺 ↾ (V ∖ dom
{〈𝐼, 𝐸〉})) = ((V ∖ dom {〈𝐼, 𝐸〉}) ∩ dom 𝐺) |
6 | 5 | ineq1i 3324 |
. . . . 5
⊢ (dom
(𝐺 ↾ (V ∖ dom
{〈𝐼, 𝐸〉})) ∩ dom {〈𝐼, 𝐸〉}) = (((V ∖ dom {〈𝐼, 𝐸〉}) ∩ dom 𝐺) ∩ dom {〈𝐼, 𝐸〉}) |
7 | | in32 3339 |
. . . . . 6
⊢ (((V
∖ dom {〈𝐼, 𝐸〉}) ∩ dom 𝐺) ∩ dom {〈𝐼, 𝐸〉}) = (((V ∖ dom {〈𝐼, 𝐸〉}) ∩ dom {〈𝐼, 𝐸〉}) ∩ dom 𝐺) |
8 | | incom 3319 |
. . . . . . . 8
⊢ ((V
∖ dom {〈𝐼, 𝐸〉}) ∩ dom {〈𝐼, 𝐸〉}) = (dom {〈𝐼, 𝐸〉} ∩ (V ∖ dom {〈𝐼, 𝐸〉})) |
9 | | disjdif 3486 |
. . . . . . . 8
⊢ (dom
{〈𝐼, 𝐸〉} ∩ (V ∖ dom {〈𝐼, 𝐸〉})) = ∅ |
10 | 8, 9 | eqtri 2191 |
. . . . . . 7
⊢ ((V
∖ dom {〈𝐼, 𝐸〉}) ∩ dom {〈𝐼, 𝐸〉}) = ∅ |
11 | 10 | ineq1i 3324 |
. . . . . 6
⊢ (((V
∖ dom {〈𝐼, 𝐸〉}) ∩ dom {〈𝐼, 𝐸〉}) ∩ dom 𝐺) = (∅ ∩ dom 𝐺) |
12 | | 0in 3449 |
. . . . . 6
⊢ (∅
∩ dom 𝐺) =
∅ |
13 | 7, 11, 12 | 3eqtri 2195 |
. . . . 5
⊢ (((V
∖ dom {〈𝐼, 𝐸〉}) ∩ dom 𝐺) ∩ dom {〈𝐼, 𝐸〉}) = ∅ |
14 | 6, 13 | eqtri 2191 |
. . . 4
⊢ (dom
(𝐺 ↾ (V ∖ dom
{〈𝐼, 𝐸〉})) ∩ dom {〈𝐼, 𝐸〉}) = ∅ |
15 | 14 | a1i 9 |
. . 3
⊢ (((𝐺 ∈ 𝑉 ∧ Fun 𝐺) ∧ (𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊)) → (dom (𝐺 ↾ (V ∖ dom {〈𝐼, 𝐸〉})) ∩ dom {〈𝐼, 𝐸〉}) = ∅) |
16 | | funun 5240 |
. . 3
⊢ (((Fun
(𝐺 ↾ (V ∖ dom
{〈𝐼, 𝐸〉})) ∧ Fun {〈𝐼, 𝐸〉}) ∧ (dom (𝐺 ↾ (V ∖ dom {〈𝐼, 𝐸〉})) ∩ dom {〈𝐼, 𝐸〉}) = ∅) → Fun ((𝐺 ↾ (V ∖ dom
{〈𝐼, 𝐸〉})) ∪ {〈𝐼, 𝐸〉})) |
17 | 2, 4, 15, 16 | syl21anc 1232 |
. 2
⊢ (((𝐺 ∈ 𝑉 ∧ Fun 𝐺) ∧ (𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊)) → Fun ((𝐺 ↾ (V ∖ dom {〈𝐼, 𝐸〉})) ∪ {〈𝐼, 𝐸〉})) |
18 | | simpll 524 |
. . . 4
⊢ (((𝐺 ∈ 𝑉 ∧ Fun 𝐺) ∧ (𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊)) → 𝐺 ∈ 𝑉) |
19 | | opexg 4211 |
. . . . 5
⊢ ((𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊) → 〈𝐼, 𝐸〉 ∈ V) |
20 | 19 | adantl 275 |
. . . 4
⊢ (((𝐺 ∈ 𝑉 ∧ Fun 𝐺) ∧ (𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊)) → 〈𝐼, 𝐸〉 ∈ V) |
21 | | setsvalg 12433 |
. . . 4
⊢ ((𝐺 ∈ 𝑉 ∧ 〈𝐼, 𝐸〉 ∈ V) → (𝐺 sSet 〈𝐼, 𝐸〉) = ((𝐺 ↾ (V ∖ dom {〈𝐼, 𝐸〉})) ∪ {〈𝐼, 𝐸〉})) |
22 | 18, 20, 21 | syl2anc 409 |
. . 3
⊢ (((𝐺 ∈ 𝑉 ∧ Fun 𝐺) ∧ (𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊)) → (𝐺 sSet 〈𝐼, 𝐸〉) = ((𝐺 ↾ (V ∖ dom {〈𝐼, 𝐸〉})) ∪ {〈𝐼, 𝐸〉})) |
23 | 22 | funeqd 5218 |
. 2
⊢ (((𝐺 ∈ 𝑉 ∧ Fun 𝐺) ∧ (𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊)) → (Fun (𝐺 sSet 〈𝐼, 𝐸〉) ↔ Fun ((𝐺 ↾ (V ∖ dom {〈𝐼, 𝐸〉})) ∪ {〈𝐼, 𝐸〉}))) |
24 | 17, 23 | mpbird 166 |
1
⊢ (((𝐺 ∈ 𝑉 ∧ Fun 𝐺) ∧ (𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊)) → Fun (𝐺 sSet 〈𝐼, 𝐸〉)) |