Step | Hyp | Ref
| Expression |
1 | | funres 5224 |
. . . . 5
⊢ (Fun
(𝐺 ∖ {∅})
→ Fun ((𝐺 ∖
{∅}) ↾ (V ∖ dom {〈𝐼, 𝐸〉}))) |
2 | 1 | ad2antlr 481 |
. . . 4
⊢ (((𝐺 ∈ 𝑉 ∧ Fun (𝐺 ∖ {∅})) ∧ (𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊)) → Fun ((𝐺 ∖ {∅}) ↾ (V ∖ dom
{〈𝐼, 𝐸〉}))) |
3 | | funsng 5229 |
. . . . 5
⊢ ((𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊) → Fun {〈𝐼, 𝐸〉}) |
4 | 3 | adantl 275 |
. . . 4
⊢ (((𝐺 ∈ 𝑉 ∧ Fun (𝐺 ∖ {∅})) ∧ (𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊)) → Fun {〈𝐼, 𝐸〉}) |
5 | | dmres 4900 |
. . . . . . 7
⊢ dom
((𝐺 ∖ {∅})
↾ (V ∖ dom {〈𝐼, 𝐸〉})) = ((V ∖ dom {〈𝐼, 𝐸〉}) ∩ dom (𝐺 ∖ {∅})) |
6 | 5 | ineq1i 3315 |
. . . . . 6
⊢ (dom
((𝐺 ∖ {∅})
↾ (V ∖ dom {〈𝐼, 𝐸〉})) ∩ dom {〈𝐼, 𝐸〉}) = (((V ∖ dom {〈𝐼, 𝐸〉}) ∩ dom (𝐺 ∖ {∅})) ∩ dom {〈𝐼, 𝐸〉}) |
7 | | in32 3330 |
. . . . . . 7
⊢ (((V
∖ dom {〈𝐼, 𝐸〉}) ∩ dom (𝐺 ∖ {∅})) ∩ dom
{〈𝐼, 𝐸〉}) = (((V ∖ dom {〈𝐼, 𝐸〉}) ∩ dom {〈𝐼, 𝐸〉}) ∩ dom (𝐺 ∖ {∅})) |
8 | | incom 3310 |
. . . . . . . . 9
⊢ ((V
∖ dom {〈𝐼, 𝐸〉}) ∩ dom {〈𝐼, 𝐸〉}) = (dom {〈𝐼, 𝐸〉} ∩ (V ∖ dom {〈𝐼, 𝐸〉})) |
9 | | disjdif 3477 |
. . . . . . . . 9
⊢ (dom
{〈𝐼, 𝐸〉} ∩ (V ∖ dom {〈𝐼, 𝐸〉})) = ∅ |
10 | 8, 9 | eqtri 2185 |
. . . . . . . 8
⊢ ((V
∖ dom {〈𝐼, 𝐸〉}) ∩ dom {〈𝐼, 𝐸〉}) = ∅ |
11 | 10 | ineq1i 3315 |
. . . . . . 7
⊢ (((V
∖ dom {〈𝐼, 𝐸〉}) ∩ dom {〈𝐼, 𝐸〉}) ∩ dom (𝐺 ∖ {∅})) = (∅ ∩ dom
(𝐺 ∖
{∅})) |
12 | | 0in 3440 |
. . . . . . 7
⊢ (∅
∩ dom (𝐺 ∖
{∅})) = ∅ |
13 | 7, 11, 12 | 3eqtri 2189 |
. . . . . 6
⊢ (((V
∖ dom {〈𝐼, 𝐸〉}) ∩ dom (𝐺 ∖ {∅})) ∩ dom
{〈𝐼, 𝐸〉}) = ∅ |
14 | 6, 13 | eqtri 2185 |
. . . . 5
⊢ (dom
((𝐺 ∖ {∅})
↾ (V ∖ dom {〈𝐼, 𝐸〉})) ∩ dom {〈𝐼, 𝐸〉}) = ∅ |
15 | 14 | a1i 9 |
. . . 4
⊢ (((𝐺 ∈ 𝑉 ∧ Fun (𝐺 ∖ {∅})) ∧ (𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊)) → (dom ((𝐺 ∖ {∅}) ↾ (V ∖ dom
{〈𝐼, 𝐸〉})) ∩ dom {〈𝐼, 𝐸〉}) = ∅) |
16 | | funun 5227 |
. . . 4
⊢ (((Fun
((𝐺 ∖ {∅})
↾ (V ∖ dom {〈𝐼, 𝐸〉})) ∧ Fun {〈𝐼, 𝐸〉}) ∧ (dom ((𝐺 ∖ {∅}) ↾ (V ∖ dom
{〈𝐼, 𝐸〉})) ∩ dom {〈𝐼, 𝐸〉}) = ∅) → Fun (((𝐺 ∖ {∅}) ↾ (V
∖ dom {〈𝐼, 𝐸〉})) ∪ {〈𝐼, 𝐸〉})) |
17 | 2, 4, 15, 16 | syl21anc 1226 |
. . 3
⊢ (((𝐺 ∈ 𝑉 ∧ Fun (𝐺 ∖ {∅})) ∧ (𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊)) → Fun (((𝐺 ∖ {∅}) ↾ (V ∖ dom
{〈𝐼, 𝐸〉})) ∪ {〈𝐼, 𝐸〉})) |
18 | | difundir 3371 |
. . . . 5
⊢ (((𝐺 ↾ (V ∖ dom
{〈𝐼, 𝐸〉})) ∪ {〈𝐼, 𝐸〉}) ∖ {∅}) = (((𝐺 ↾ (V ∖ dom
{〈𝐼, 𝐸〉})) ∖ {∅}) ∪
({〈𝐼, 𝐸〉} ∖
{∅})) |
19 | | resdifcom 4897 |
. . . . . . 7
⊢ ((𝐺 ↾ (V ∖ dom
{〈𝐼, 𝐸〉})) ∖ {∅}) = ((𝐺 ∖ {∅}) ↾ (V
∖ dom {〈𝐼, 𝐸〉})) |
20 | 19 | a1i 9 |
. . . . . 6
⊢ (((𝐺 ∈ 𝑉 ∧ Fun (𝐺 ∖ {∅})) ∧ (𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊)) → ((𝐺 ↾ (V ∖ dom {〈𝐼, 𝐸〉})) ∖ {∅}) = ((𝐺 ∖ {∅}) ↾ (V
∖ dom {〈𝐼, 𝐸〉}))) |
21 | | elex 2733 |
. . . . . . . . 9
⊢ (𝐼 ∈ 𝑈 → 𝐼 ∈ V) |
22 | | elex 2733 |
. . . . . . . . 9
⊢ (𝐸 ∈ 𝑊 → 𝐸 ∈ V) |
23 | | opm 4207 |
. . . . . . . . . 10
⊢
(∃𝑥 𝑥 ∈ 〈𝐼, 𝐸〉 ↔ (𝐼 ∈ V ∧ 𝐸 ∈ V)) |
24 | | n0r 3418 |
. . . . . . . . . 10
⊢
(∃𝑥 𝑥 ∈ 〈𝐼, 𝐸〉 → 〈𝐼, 𝐸〉 ≠ ∅) |
25 | 23, 24 | sylbir 134 |
. . . . . . . . 9
⊢ ((𝐼 ∈ V ∧ 𝐸 ∈ V) → 〈𝐼, 𝐸〉 ≠ ∅) |
26 | 21, 22, 25 | syl2an 287 |
. . . . . . . 8
⊢ ((𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊) → 〈𝐼, 𝐸〉 ≠ ∅) |
27 | 26 | adantl 275 |
. . . . . . 7
⊢ (((𝐺 ∈ 𝑉 ∧ Fun (𝐺 ∖ {∅})) ∧ (𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊)) → 〈𝐼, 𝐸〉 ≠ ∅) |
28 | | disjsn2 3634 |
. . . . . . 7
⊢
(〈𝐼, 𝐸〉 ≠ ∅ →
({〈𝐼, 𝐸〉} ∩ {∅}) =
∅) |
29 | | disjdif2 3483 |
. . . . . . 7
⊢
(({〈𝐼, 𝐸〉} ∩ {∅}) =
∅ → ({〈𝐼,
𝐸〉} ∖ {∅})
= {〈𝐼, 𝐸〉}) |
30 | 27, 28, 29 | 3syl 17 |
. . . . . 6
⊢ (((𝐺 ∈ 𝑉 ∧ Fun (𝐺 ∖ {∅})) ∧ (𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊)) → ({〈𝐼, 𝐸〉} ∖ {∅}) = {〈𝐼, 𝐸〉}) |
31 | 20, 30 | uneq12d 3273 |
. . . . 5
⊢ (((𝐺 ∈ 𝑉 ∧ Fun (𝐺 ∖ {∅})) ∧ (𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊)) → (((𝐺 ↾ (V ∖ dom {〈𝐼, 𝐸〉})) ∖ {∅}) ∪
({〈𝐼, 𝐸〉} ∖ {∅})) =
(((𝐺 ∖ {∅})
↾ (V ∖ dom {〈𝐼, 𝐸〉})) ∪ {〈𝐼, 𝐸〉})) |
32 | 18, 31 | syl5eq 2209 |
. . . 4
⊢ (((𝐺 ∈ 𝑉 ∧ Fun (𝐺 ∖ {∅})) ∧ (𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊)) → (((𝐺 ↾ (V ∖ dom {〈𝐼, 𝐸〉})) ∪ {〈𝐼, 𝐸〉}) ∖ {∅}) = (((𝐺 ∖ {∅}) ↾ (V
∖ dom {〈𝐼, 𝐸〉})) ∪ {〈𝐼, 𝐸〉})) |
33 | 32 | funeqd 5205 |
. . 3
⊢ (((𝐺 ∈ 𝑉 ∧ Fun (𝐺 ∖ {∅})) ∧ (𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊)) → (Fun (((𝐺 ↾ (V ∖ dom {〈𝐼, 𝐸〉})) ∪ {〈𝐼, 𝐸〉}) ∖ {∅}) ↔ Fun
(((𝐺 ∖ {∅})
↾ (V ∖ dom {〈𝐼, 𝐸〉})) ∪ {〈𝐼, 𝐸〉}))) |
34 | 17, 33 | mpbird 166 |
. 2
⊢ (((𝐺 ∈ 𝑉 ∧ Fun (𝐺 ∖ {∅})) ∧ (𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊)) → Fun (((𝐺 ↾ (V ∖ dom {〈𝐼, 𝐸〉})) ∪ {〈𝐼, 𝐸〉}) ∖
{∅})) |
35 | | simpll 519 |
. . . . 5
⊢ (((𝐺 ∈ 𝑉 ∧ Fun (𝐺 ∖ {∅})) ∧ (𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊)) → 𝐺 ∈ 𝑉) |
36 | | opexg 4201 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊) → 〈𝐼, 𝐸〉 ∈ V) |
37 | 36 | adantl 275 |
. . . . 5
⊢ (((𝐺 ∈ 𝑉 ∧ Fun (𝐺 ∖ {∅})) ∧ (𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊)) → 〈𝐼, 𝐸〉 ∈ V) |
38 | | setsvalg 12378 |
. . . . 5
⊢ ((𝐺 ∈ 𝑉 ∧ 〈𝐼, 𝐸〉 ∈ V) → (𝐺 sSet 〈𝐼, 𝐸〉) = ((𝐺 ↾ (V ∖ dom {〈𝐼, 𝐸〉})) ∪ {〈𝐼, 𝐸〉})) |
39 | 35, 37, 38 | syl2anc 409 |
. . . 4
⊢ (((𝐺 ∈ 𝑉 ∧ Fun (𝐺 ∖ {∅})) ∧ (𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊)) → (𝐺 sSet 〈𝐼, 𝐸〉) = ((𝐺 ↾ (V ∖ dom {〈𝐼, 𝐸〉})) ∪ {〈𝐼, 𝐸〉})) |
40 | 39 | difeq1d 3235 |
. . 3
⊢ (((𝐺 ∈ 𝑉 ∧ Fun (𝐺 ∖ {∅})) ∧ (𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊)) → ((𝐺 sSet 〈𝐼, 𝐸〉) ∖ {∅}) = (((𝐺 ↾ (V ∖ dom
{〈𝐼, 𝐸〉})) ∪ {〈𝐼, 𝐸〉}) ∖
{∅})) |
41 | 40 | funeqd 5205 |
. 2
⊢ (((𝐺 ∈ 𝑉 ∧ Fun (𝐺 ∖ {∅})) ∧ (𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊)) → (Fun ((𝐺 sSet 〈𝐼, 𝐸〉) ∖ {∅}) ↔ Fun
(((𝐺 ↾ (V ∖ dom
{〈𝐼, 𝐸〉})) ∪ {〈𝐼, 𝐸〉}) ∖
{∅}))) |
42 | 34, 41 | mpbird 166 |
1
⊢ (((𝐺 ∈ 𝑉 ∧ Fun (𝐺 ∖ {∅})) ∧ (𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊)) → Fun ((𝐺 sSet 〈𝐼, 𝐸〉) ∖ {∅})) |