Proof of Theorem sbthlem5
Step | Hyp | Ref
| Expression |
1 | | sbthlem.1 |
. . . . . . . . 9
⊢ 𝐴 ∈ V |
2 | | sbthlem.2 |
. . . . . . . . 9
⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))} |
3 | 1, 2 | sbthlem1 8070 |
. . . . . . . 8
⊢ ∪ 𝐷
⊆ (𝐴 ∖ (𝑔 “ (𝐵 ∖ (𝑓 “ ∪ 𝐷)))) |
4 | | difss 3737 |
. . . . . . . 8
⊢ (𝐴 ∖ (𝑔 “ (𝐵 ∖ (𝑓 “ ∪ 𝐷)))) ⊆ 𝐴 |
5 | 3, 4 | sstri 3612 |
. . . . . . 7
⊢ ∪ 𝐷
⊆ 𝐴 |
6 | | sseq2 3627 |
. . . . . . 7
⊢ (dom
𝑓 = 𝐴 → (∪ 𝐷 ⊆ dom 𝑓 ↔ ∪ 𝐷 ⊆ 𝐴)) |
7 | 5, 6 | mpbiri 248 |
. . . . . 6
⊢ (dom
𝑓 = 𝐴 → ∪ 𝐷 ⊆ dom 𝑓) |
8 | | dfss 3589 |
. . . . . 6
⊢ (∪ 𝐷
⊆ dom 𝑓 ↔ ∪ 𝐷 =
(∪ 𝐷 ∩ dom 𝑓)) |
9 | 7, 8 | sylib 208 |
. . . . 5
⊢ (dom
𝑓 = 𝐴 → ∪ 𝐷 = (∪
𝐷 ∩ dom 𝑓)) |
10 | 9 | uneq1d 3766 |
. . . 4
⊢ (dom
𝑓 = 𝐴 → (∪ 𝐷 ∪ (𝐴 ∖ ∪ 𝐷)) = ((∪ 𝐷
∩ dom 𝑓) ∪ (𝐴 ∖ ∪ 𝐷))) |
11 | 1, 2 | sbthlem3 8072 |
. . . . . . 7
⊢ (ran
𝑔 ⊆ 𝐴 → (𝑔 “ (𝐵 ∖ (𝑓 “ ∪ 𝐷))) = (𝐴 ∖ ∪ 𝐷)) |
12 | | imassrn 5477 |
. . . . . . 7
⊢ (𝑔 “ (𝐵 ∖ (𝑓 “ ∪ 𝐷))) ⊆ ran 𝑔 |
13 | 11, 12 | syl6eqssr 3656 |
. . . . . 6
⊢ (ran
𝑔 ⊆ 𝐴 → (𝐴 ∖ ∪ 𝐷) ⊆ ran 𝑔) |
14 | | dfss 3589 |
. . . . . 6
⊢ ((𝐴 ∖ ∪ 𝐷)
⊆ ran 𝑔 ↔ (𝐴 ∖ ∪ 𝐷) =
((𝐴 ∖ ∪ 𝐷)
∩ ran 𝑔)) |
15 | 13, 14 | sylib 208 |
. . . . 5
⊢ (ran
𝑔 ⊆ 𝐴 → (𝐴 ∖ ∪ 𝐷) = ((𝐴 ∖ ∪ 𝐷) ∩ ran 𝑔)) |
16 | 15 | uneq2d 3767 |
. . . 4
⊢ (ran
𝑔 ⊆ 𝐴 → ((∪ 𝐷 ∩ dom 𝑓) ∪ (𝐴 ∖ ∪ 𝐷)) = ((∪ 𝐷
∩ dom 𝑓) ∪ ((𝐴 ∖ ∪ 𝐷)
∩ ran 𝑔))) |
17 | 10, 16 | sylan9eq 2676 |
. . 3
⊢ ((dom
𝑓 = 𝐴 ∧ ran 𝑔 ⊆ 𝐴) → (∪ 𝐷 ∪ (𝐴 ∖ ∪ 𝐷)) = ((∪ 𝐷
∩ dom 𝑓) ∪ ((𝐴 ∖ ∪ 𝐷)
∩ ran 𝑔))) |
18 | | sbthlem.3 |
. . . . 5
⊢ 𝐻 = ((𝑓 ↾ ∪ 𝐷) ∪ (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) |
19 | 18 | dmeqi 5325 |
. . . 4
⊢ dom 𝐻 = dom ((𝑓 ↾ ∪ 𝐷) ∪ (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) |
20 | | dmun 5331 |
. . . . 5
⊢ dom
((𝑓 ↾ ∪ 𝐷)
∪ (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) = (dom (𝑓 ↾ ∪ 𝐷) ∪ dom (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) |
21 | | dmres 5419 |
. . . . . 6
⊢ dom
(𝑓 ↾ ∪ 𝐷) =
(∪ 𝐷 ∩ dom 𝑓) |
22 | | dmres 5419 |
. . . . . . 7
⊢ dom
(◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷)) = ((𝐴 ∖ ∪ 𝐷) ∩ dom ◡𝑔) |
23 | | df-rn 5125 |
. . . . . . . . 9
⊢ ran 𝑔 = dom ◡𝑔 |
24 | 23 | eqcomi 2631 |
. . . . . . . 8
⊢ dom ◡𝑔 = ran 𝑔 |
25 | 24 | ineq2i 3811 |
. . . . . . 7
⊢ ((𝐴 ∖ ∪ 𝐷)
∩ dom ◡𝑔) = ((𝐴 ∖ ∪ 𝐷) ∩ ran 𝑔) |
26 | 22, 25 | eqtri 2644 |
. . . . . 6
⊢ dom
(◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷)) = ((𝐴 ∖ ∪ 𝐷) ∩ ran 𝑔) |
27 | 21, 26 | uneq12i 3765 |
. . . . 5
⊢ (dom
(𝑓 ↾ ∪ 𝐷)
∪ dom (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) = ((∪ 𝐷
∩ dom 𝑓) ∪ ((𝐴 ∖ ∪ 𝐷)
∩ ran 𝑔)) |
28 | 20, 27 | eqtri 2644 |
. . . 4
⊢ dom
((𝑓 ↾ ∪ 𝐷)
∪ (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) = ((∪ 𝐷
∩ dom 𝑓) ∪ ((𝐴 ∖ ∪ 𝐷)
∩ ran 𝑔)) |
29 | 19, 28 | eqtri 2644 |
. . 3
⊢ dom 𝐻 = ((∪ 𝐷
∩ dom 𝑓) ∪ ((𝐴 ∖ ∪ 𝐷)
∩ ran 𝑔)) |
30 | 17, 29 | syl6reqr 2675 |
. 2
⊢ ((dom
𝑓 = 𝐴 ∧ ran 𝑔 ⊆ 𝐴) → dom 𝐻 = (∪ 𝐷 ∪ (𝐴 ∖ ∪ 𝐷))) |
31 | | undif 4049 |
. . 3
⊢ (∪ 𝐷
⊆ 𝐴 ↔ (∪ 𝐷
∪ (𝐴 ∖ ∪ 𝐷))
= 𝐴) |
32 | 5, 31 | mpbi 220 |
. 2
⊢ (∪ 𝐷
∪ (𝐴 ∖ ∪ 𝐷))
= 𝐴 |
33 | 30, 32 | syl6eq 2672 |
1
⊢ ((dom
𝑓 = 𝐴 ∧ ran 𝑔 ⊆ 𝐴) → dom 𝐻 = 𝐴) |