Proof of Theorem setsfun
| Step | Hyp | Ref
| Expression |
|---|
| 1 | | funres 5239 |
. . . 4
⊢ (Fun
𝐺 → Fun (𝐺 ↾ (V ∖ dom
{⟨𝐼, 𝐸⟩}))) |
| 2 | 1 | ad2antlr 486 |
. . 3
⊢ (((𝐺 ∈ 𝑉 ∧ Fun 𝐺) ∧ (𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊)) → Fun (𝐺 ↾ (V ∖ dom {⟨𝐼, 𝐸⟩}))) |
| 3 | | funsng 5244 |
. . . 4
⊢ ((𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊) → Fun {⟨𝐼, 𝐸⟩}) |
| 4 | 3 | adantl 275 |
. . 3
⊢ (((𝐺 ∈ 𝑉 ∧ Fun 𝐺) ∧ (𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊)) → Fun {⟨𝐼, 𝐸⟩}) |
| 5 | | dmres 4912 |
. . . . . 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 3487 |
. . . . . . . 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 3450 |
. . . . . 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 5242 |
. . 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 4213 |
. . . . 5
⊢ ((𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊) → ⟨𝐼, 𝐸⟩ ∈ V) |
| 20 | 19 | adantl 275 |
. . . 4
⊢ (((𝐺 ∈ 𝑉 ∧ Fun 𝐺) ∧ (𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊)) → ⟨𝐼, 𝐸⟩ ∈ V) |
| 21 | | setsvalg 12446 |
. . . 4
⊢ ((𝐺 ∈ 𝑉 ∧ ⟨𝐼, 𝐸⟩ ∈ V) → (𝐺 sSet ⟨𝐼, 𝐸⟩) = ((𝐺 ↾ (V ∖ dom {⟨𝐼, 𝐸⟩})) ∪ {⟨𝐼, 𝐸⟩})) |
| 22 | 18, 20, 21 | syl2anc 409 |
. . 3
⊢ (((𝐺 ∈ 𝑉 ∧ Fun 𝐺) ∧ (𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊)) → (𝐺 sSet ⟨𝐼, 𝐸⟩) = ((𝐺 ↾ (V ∖ dom {⟨𝐼, 𝐸⟩})) ∪ {⟨𝐼, 𝐸⟩})) |
| 23 | 22 | funeqd 5220 |
. 2
⊢ (((𝐺 ∈ 𝑉 ∧ Fun 𝐺) ∧ (𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊)) → (Fun (𝐺 sSet ⟨𝐼, 𝐸⟩) ↔ Fun ((𝐺 ↾ (V ∖ dom {⟨𝐼, 𝐸⟩})) ∪ {⟨𝐼, 𝐸⟩}))) |
| 24 | 17, 23 | mpbird 166 |
1
⊢ (((𝐺 ∈ 𝑉 ∧ Fun 𝐺) ∧ (𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊)) → Fun (𝐺 sSet ⟨𝐼, 𝐸⟩)) |
