Step | Hyp | Ref
| Expression |
1 | | funres 6547 |
. . . . . 6
⊢ (Fun
(𝐺 ∖ {∅})
→ Fun ((𝐺 ∖
{∅}) ↾ (V ∖ dom {⟨𝐼, 𝐸⟩}))) |
2 | 1 | adantl 483 |
. . . . 5
⊢ ((𝐺 ∈ 𝑉 ∧ Fun (𝐺 ∖ {∅})) → Fun ((𝐺 ∖ {∅}) ↾ (V
∖ dom {⟨𝐼, 𝐸⟩}))) |
3 | 2 | adantr 482 |
. . . 4
⊢ (((𝐺 ∈ 𝑉 ∧ Fun (𝐺 ∖ {∅})) ∧ (𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊)) → Fun ((𝐺 ∖ {∅}) ↾ (V ∖ dom
{⟨𝐼, 𝐸⟩}))) |
4 | | funsng 6556 |
. . . . 5
⊢ ((𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊) → Fun {⟨𝐼, 𝐸⟩}) |
5 | 4 | adantl 483 |
. . . 4
⊢ (((𝐺 ∈ 𝑉 ∧ Fun (𝐺 ∖ {∅})) ∧ (𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊)) → Fun {⟨𝐼, 𝐸⟩}) |
6 | | dmres 5963 |
. . . . . . 7
⊢ dom
((𝐺 ∖ {∅})
↾ (V ∖ dom {⟨𝐼, 𝐸⟩})) = ((V ∖ dom {⟨𝐼, 𝐸⟩}) ∩ dom (𝐺 ∖ {∅})) |
7 | 6 | ineq1i 4172 |
. . . . . 6
⊢ (dom
((𝐺 ∖ {∅})
↾ (V ∖ dom {⟨𝐼, 𝐸⟩})) ∩ dom {⟨𝐼, 𝐸⟩}) = (((V ∖ dom {⟨𝐼, 𝐸⟩}) ∩ dom (𝐺 ∖ {∅})) ∩ dom {⟨𝐼, 𝐸⟩}) |
8 | | in32 4185 |
. . . . . . 7
⊢ (((V
∖ dom {⟨𝐼, 𝐸⟩}) ∩ dom (𝐺 ∖ {∅})) ∩ dom
{⟨𝐼, 𝐸⟩}) = (((V ∖ dom {⟨𝐼, 𝐸⟩}) ∩ dom {⟨𝐼, 𝐸⟩}) ∩ dom (𝐺 ∖ {∅})) |
9 | | disjdifr 4436 |
. . . . . . . 8
⊢ ((V
∖ dom {⟨𝐼, 𝐸⟩}) ∩ dom {⟨𝐼, 𝐸⟩}) = ∅ |
10 | 9 | ineq1i 4172 |
. . . . . . 7
⊢ (((V
∖ dom {⟨𝐼, 𝐸⟩}) ∩ dom {⟨𝐼, 𝐸⟩}) ∩ dom (𝐺 ∖ {∅})) = (∅ ∩ dom
(𝐺 ∖
{∅})) |
11 | | 0in 4357 |
. . . . . . 7
⊢ (∅
∩ dom (𝐺 ∖
{∅})) = ∅ |
12 | 8, 10, 11 | 3eqtri 2765 |
. . . . . 6
⊢ (((V
∖ dom {⟨𝐼, 𝐸⟩}) ∩ dom (𝐺 ∖ {∅})) ∩ dom
{⟨𝐼, 𝐸⟩}) = ∅ |
13 | 7, 12 | eqtri 2761 |
. . . . 5
⊢ (dom
((𝐺 ∖ {∅})
↾ (V ∖ dom {⟨𝐼, 𝐸⟩})) ∩ dom {⟨𝐼, 𝐸⟩}) = ∅ |
14 | 13 | a1i 11 |
. . . 4
⊢ (((𝐺 ∈ 𝑉 ∧ Fun (𝐺 ∖ {∅})) ∧ (𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊)) → (dom ((𝐺 ∖ {∅}) ↾ (V ∖ dom
{⟨𝐼, 𝐸⟩})) ∩ dom {⟨𝐼, 𝐸⟩}) = ∅) |
15 | | funun 6551 |
. . . 4
⊢ (((Fun
((𝐺 ∖ {∅})
↾ (V ∖ dom {⟨𝐼, 𝐸⟩})) ∧ Fun {⟨𝐼, 𝐸⟩}) ∧ (dom ((𝐺 ∖ {∅}) ↾ (V ∖ dom
{⟨𝐼, 𝐸⟩})) ∩ dom {⟨𝐼, 𝐸⟩}) = ∅) → Fun (((𝐺 ∖ {∅}) ↾ (V
∖ dom {⟨𝐼, 𝐸⟩})) ∪ {⟨𝐼, 𝐸⟩})) |
16 | 3, 5, 14, 15 | syl21anc 837 |
. . 3
⊢ (((𝐺 ∈ 𝑉 ∧ Fun (𝐺 ∖ {∅})) ∧ (𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊)) → Fun (((𝐺 ∖ {∅}) ↾ (V ∖ dom
{⟨𝐼, 𝐸⟩})) ∪ {⟨𝐼, 𝐸⟩})) |
17 | | difundir 4244 |
. . . . 5
⊢ (((𝐺 ↾ (V ∖ dom
{⟨𝐼, 𝐸⟩})) ∪ {⟨𝐼, 𝐸⟩}) ∖ {∅}) = (((𝐺 ↾ (V ∖ dom
{⟨𝐼, 𝐸⟩})) ∖ {∅}) ∪
({⟨𝐼, 𝐸⟩} ∖
{∅})) |
18 | | resdifcom 5960 |
. . . . . . 7
⊢ ((𝐺 ↾ (V ∖ dom
{⟨𝐼, 𝐸⟩})) ∖ {∅}) = ((𝐺 ∖ {∅}) ↾ (V
∖ dom {⟨𝐼, 𝐸⟩})) |
19 | 18 | a1i 11 |
. . . . . 6
⊢ (((𝐺 ∈ 𝑉 ∧ Fun (𝐺 ∖ {∅})) ∧ (𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊)) → ((𝐺 ↾ (V ∖ dom {⟨𝐼, 𝐸⟩})) ∖ {∅}) = ((𝐺 ∖ {∅}) ↾ (V
∖ dom {⟨𝐼, 𝐸⟩}))) |
20 | | elex 3465 |
. . . . . . . . . 10
⊢ (𝐼 ∈ 𝑈 → 𝐼 ∈ V) |
21 | | elex 3465 |
. . . . . . . . . 10
⊢ (𝐸 ∈ 𝑊 → 𝐸 ∈ V) |
22 | 20, 21 | anim12i 614 |
. . . . . . . . 9
⊢ ((𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊) → (𝐼 ∈ V ∧ 𝐸 ∈ V)) |
23 | | opnz 5434 |
. . . . . . . . 9
⊢
(⟨𝐼, 𝐸⟩ ≠ ∅ ↔
(𝐼 ∈ V ∧ 𝐸 ∈ V)) |
24 | 22, 23 | sylibr 233 |
. . . . . . . 8
⊢ ((𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊) → ⟨𝐼, 𝐸⟩ ≠ ∅) |
25 | 24 | adantl 483 |
. . . . . . 7
⊢ (((𝐺 ∈ 𝑉 ∧ Fun (𝐺 ∖ {∅})) ∧ (𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊)) → ⟨𝐼, 𝐸⟩ ≠ ∅) |
26 | | disjsn2 4677 |
. . . . . . 7
⊢
(⟨𝐼, 𝐸⟩ ≠ ∅ →
({⟨𝐼, 𝐸⟩} ∩ {∅}) =
∅) |
27 | | disjdif2 4443 |
. . . . . . 7
⊢
(({⟨𝐼, 𝐸⟩} ∩ {∅}) =
∅ → ({⟨𝐼,
𝐸⟩} ∖ {∅})
= {⟨𝐼, 𝐸⟩}) |
28 | 25, 26, 27 | 3syl 18 |
. . . . . 6
⊢ (((𝐺 ∈ 𝑉 ∧ Fun (𝐺 ∖ {∅})) ∧ (𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊)) → ({⟨𝐼, 𝐸⟩} ∖ {∅}) = {⟨𝐼, 𝐸⟩}) |
29 | 19, 28 | uneq12d 4128 |
. . . . 5
⊢ (((𝐺 ∈ 𝑉 ∧ Fun (𝐺 ∖ {∅})) ∧ (𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊)) → (((𝐺 ↾ (V ∖ dom {⟨𝐼, 𝐸⟩})) ∖ {∅}) ∪
({⟨𝐼, 𝐸⟩} ∖ {∅})) =
(((𝐺 ∖ {∅})
↾ (V ∖ dom {⟨𝐼, 𝐸⟩})) ∪ {⟨𝐼, 𝐸⟩})) |
30 | 17, 29 | eqtrid 2785 |
. . . 4
⊢ (((𝐺 ∈ 𝑉 ∧ Fun (𝐺 ∖ {∅})) ∧ (𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊)) → (((𝐺 ↾ (V ∖ dom {⟨𝐼, 𝐸⟩})) ∪ {⟨𝐼, 𝐸⟩}) ∖ {∅}) = (((𝐺 ∖ {∅}) ↾ (V
∖ dom {⟨𝐼, 𝐸⟩})) ∪ {⟨𝐼, 𝐸⟩})) |
31 | 30 | funeqd 6527 |
. . 3
⊢ (((𝐺 ∈ 𝑉 ∧ Fun (𝐺 ∖ {∅})) ∧ (𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊)) → (Fun (((𝐺 ↾ (V ∖ dom {⟨𝐼, 𝐸⟩})) ∪ {⟨𝐼, 𝐸⟩}) ∖ {∅}) ↔ Fun
(((𝐺 ∖ {∅})
↾ (V ∖ dom {⟨𝐼, 𝐸⟩})) ∪ {⟨𝐼, 𝐸⟩}))) |
32 | 16, 31 | mpbird 257 |
. 2
⊢ (((𝐺 ∈ 𝑉 ∧ Fun (𝐺 ∖ {∅})) ∧ (𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊)) → Fun (((𝐺 ↾ (V ∖ dom {⟨𝐼, 𝐸⟩})) ∪ {⟨𝐼, 𝐸⟩}) ∖
{∅})) |
33 | | opex 5425 |
. . . . . . 7
⊢
⟨𝐼, 𝐸⟩ ∈ V |
34 | 33 | a1i 11 |
. . . . . 6
⊢ (Fun
(𝐺 ∖ {∅})
→ ⟨𝐼, 𝐸⟩ ∈
V) |
35 | | setsvalg 17046 |
. . . . . 6
⊢ ((𝐺 ∈ 𝑉 ∧ ⟨𝐼, 𝐸⟩ ∈ V) → (𝐺 sSet ⟨𝐼, 𝐸⟩) = ((𝐺 ↾ (V ∖ dom {⟨𝐼, 𝐸⟩})) ∪ {⟨𝐼, 𝐸⟩})) |
36 | 34, 35 | sylan2 594 |
. . . . 5
⊢ ((𝐺 ∈ 𝑉 ∧ Fun (𝐺 ∖ {∅})) → (𝐺 sSet ⟨𝐼, 𝐸⟩) = ((𝐺 ↾ (V ∖ dom {⟨𝐼, 𝐸⟩})) ∪ {⟨𝐼, 𝐸⟩})) |
37 | 36 | difeq1d 4085 |
. . . 4
⊢ ((𝐺 ∈ 𝑉 ∧ Fun (𝐺 ∖ {∅})) → ((𝐺 sSet ⟨𝐼, 𝐸⟩) ∖ {∅}) = (((𝐺 ↾ (V ∖ dom
{⟨𝐼, 𝐸⟩})) ∪ {⟨𝐼, 𝐸⟩}) ∖
{∅})) |
38 | 37 | funeqd 6527 |
. . 3
⊢ ((𝐺 ∈ 𝑉 ∧ Fun (𝐺 ∖ {∅})) → (Fun ((𝐺 sSet ⟨𝐼, 𝐸⟩) ∖ {∅}) ↔ Fun
(((𝐺 ↾ (V ∖ dom
{⟨𝐼, 𝐸⟩})) ∪ {⟨𝐼, 𝐸⟩}) ∖
{∅}))) |
39 | 38 | adantr 482 |
. 2
⊢ (((𝐺 ∈ 𝑉 ∧ Fun (𝐺 ∖ {∅})) ∧ (𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊)) → (Fun ((𝐺 sSet ⟨𝐼, 𝐸⟩) ∖ {∅}) ↔ Fun
(((𝐺 ↾ (V ∖ dom
{⟨𝐼, 𝐸⟩})) ∪ {⟨𝐼, 𝐸⟩}) ∖
{∅}))) |
40 | 32, 39 | mpbird 257 |
1
⊢ (((𝐺 ∈ 𝑉 ∧ Fun (𝐺 ∖ {∅})) ∧ (𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊)) → Fun ((𝐺 sSet ⟨𝐼, 𝐸⟩) ∖ {∅})) |