Proof of Theorem sbthlem7
| Step | Hyp | Ref
| Expression |
| 1 | | funres 6608 |
. . 3
⊢ (Fun
𝑓 → Fun (𝑓 ↾ ∪ 𝐷)) |
| 2 | | funres 6608 |
. . 3
⊢ (Fun
◡𝑔 → Fun (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) |
| 3 | | dmres 6030 |
. . . . . . . . 9
⊢ dom
(𝑓 ↾ ∪ 𝐷) =
(∪ 𝐷 ∩ dom 𝑓) |
| 4 | | inss1 4237 |
. . . . . . . . 9
⊢ (∪ 𝐷
∩ dom 𝑓) ⊆ ∪ 𝐷 |
| 5 | 3, 4 | eqsstri 4030 |
. . . . . . . 8
⊢ dom
(𝑓 ↾ ∪ 𝐷)
⊆ ∪ 𝐷 |
| 6 | | ssrin 4242 |
. . . . . . . 8
⊢ (dom
(𝑓 ↾ ∪ 𝐷)
⊆ ∪ 𝐷 → (dom (𝑓 ↾ ∪ 𝐷) ∩ dom (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) ⊆ (∪ 𝐷
∩ dom (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷)))) |
| 7 | 5, 6 | ax-mp 5 |
. . . . . . 7
⊢ (dom
(𝑓 ↾ ∪ 𝐷)
∩ dom (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) ⊆ (∪ 𝐷
∩ dom (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) |
| 8 | | dmres 6030 |
. . . . . . . . 9
⊢ dom
(◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷)) = ((𝐴 ∖ ∪ 𝐷) ∩ dom ◡𝑔) |
| 9 | | inss1 4237 |
. . . . . . . . 9
⊢ ((𝐴 ∖ ∪ 𝐷)
∩ dom ◡𝑔) ⊆ (𝐴 ∖ ∪ 𝐷) |
| 10 | 8, 9 | eqsstri 4030 |
. . . . . . . 8
⊢ dom
(◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷)) ⊆ (𝐴 ∖ ∪ 𝐷) |
| 11 | | sslin 4243 |
. . . . . . . 8
⊢ (dom
(◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷)) ⊆ (𝐴 ∖ ∪ 𝐷) → (∪ 𝐷
∩ dom (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) ⊆ (∪ 𝐷
∩ (𝐴 ∖ ∪ 𝐷))) |
| 12 | 10, 11 | ax-mp 5 |
. . . . . . 7
⊢ (∪ 𝐷
∩ dom (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) ⊆ (∪ 𝐷
∩ (𝐴 ∖ ∪ 𝐷)) |
| 13 | 7, 12 | sstri 3993 |
. . . . . 6
⊢ (dom
(𝑓 ↾ ∪ 𝐷)
∩ dom (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) ⊆ (∪ 𝐷
∩ (𝐴 ∖ ∪ 𝐷)) |
| 14 | | disjdif 4472 |
. . . . . 6
⊢ (∪ 𝐷
∩ (𝐴 ∖ ∪ 𝐷))
= ∅ |
| 15 | 13, 14 | sseqtri 4032 |
. . . . 5
⊢ (dom
(𝑓 ↾ ∪ 𝐷)
∩ dom (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) ⊆
∅ |
| 16 | | ss0 4402 |
. . . . 5
⊢ ((dom
(𝑓 ↾ ∪ 𝐷)
∩ dom (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) ⊆ ∅ → (dom
(𝑓 ↾ ∪ 𝐷)
∩ dom (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) = ∅) |
| 17 | 15, 16 | ax-mp 5 |
. . . 4
⊢ (dom
(𝑓 ↾ ∪ 𝐷)
∩ dom (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) = ∅ |
| 18 | | funun 6612 |
. . . 4
⊢ (((Fun
(𝑓 ↾ ∪ 𝐷)
∧ Fun (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) ∧ (dom (𝑓 ↾ ∪ 𝐷)
∩ dom (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) = ∅) → Fun
((𝑓 ↾ ∪ 𝐷)
∪ (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷)))) |
| 19 | 17, 18 | mpan2 691 |
. . 3
⊢ ((Fun
(𝑓 ↾ ∪ 𝐷)
∧ Fun (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) → Fun ((𝑓 ↾ ∪ 𝐷)
∪ (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷)))) |
| 20 | 1, 2, 19 | syl2an 596 |
. 2
⊢ ((Fun
𝑓 ∧ Fun ◡𝑔) → Fun ((𝑓 ↾ ∪ 𝐷) ∪ (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷)))) |
| 21 | | sbthlem.3 |
. . 3
⊢ 𝐻 = ((𝑓 ↾ ∪ 𝐷) ∪ (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) |
| 22 | 21 | funeqi 6587 |
. 2
⊢ (Fun
𝐻 ↔ Fun ((𝑓 ↾ ∪ 𝐷)
∪ (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷)))) |
| 23 | 20, 22 | sylibr 234 |
1
⊢ ((Fun
𝑓 ∧ Fun ◡𝑔) → Fun 𝐻) |