Proof of Theorem sbthlem4
Step | Hyp | Ref
| Expression |
1 | | df-ima 5601 |
. 2
⊢ (◡𝑔 “ (𝐴 ∖ ∪ 𝐷)) = ran (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷)) |
2 | | difss 4070 |
. . . . . . 7
⊢ (𝐵 ∖ (𝑓 “ ∪ 𝐷)) ⊆ 𝐵 |
3 | | sseq2 3951 |
. . . . . . 7
⊢ (dom
𝑔 = 𝐵 → ((𝐵 ∖ (𝑓 “ ∪ 𝐷)) ⊆ dom 𝑔 ↔ (𝐵 ∖ (𝑓 “ ∪ 𝐷)) ⊆ 𝐵)) |
4 | 2, 3 | mpbiri 257 |
. . . . . 6
⊢ (dom
𝑔 = 𝐵 → (𝐵 ∖ (𝑓 “ ∪ 𝐷)) ⊆ dom 𝑔) |
5 | | ssdmres 5911 |
. . . . . 6
⊢ ((𝐵 ∖ (𝑓 “ ∪ 𝐷)) ⊆ dom 𝑔 ↔ dom (𝑔 ↾ (𝐵 ∖ (𝑓 “ ∪ 𝐷))) = (𝐵 ∖ (𝑓 “ ∪ 𝐷))) |
6 | 4, 5 | sylib 217 |
. . . . 5
⊢ (dom
𝑔 = 𝐵 → dom (𝑔 ↾ (𝐵 ∖ (𝑓 “ ∪ 𝐷))) = (𝐵 ∖ (𝑓 “ ∪ 𝐷))) |
7 | | dfdm4 5801 |
. . . . 5
⊢ dom
(𝑔 ↾ (𝐵 ∖ (𝑓 “ ∪ 𝐷))) = ran ◡(𝑔 ↾ (𝐵 ∖ (𝑓 “ ∪ 𝐷))) |
8 | 6, 7 | eqtr3di 2794 |
. . . 4
⊢ (dom
𝑔 = 𝐵 → (𝐵 ∖ (𝑓 “ ∪ 𝐷)) = ran ◡(𝑔 ↾ (𝐵 ∖ (𝑓 “ ∪ 𝐷)))) |
9 | | funcnvres 6508 |
. . . . . 6
⊢ (Fun
◡𝑔 → ◡(𝑔 ↾ (𝐵 ∖ (𝑓 “ ∪ 𝐷))) = (◡𝑔 ↾ (𝑔 “ (𝐵 ∖ (𝑓 “ ∪ 𝐷))))) |
10 | | sbthlem.1 |
. . . . . . . 8
⊢ 𝐴 ∈ V |
11 | | sbthlem.2 |
. . . . . . . 8
⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))} |
12 | 10, 11 | sbthlem3 8841 |
. . . . . . 7
⊢ (ran
𝑔 ⊆ 𝐴 → (𝑔 “ (𝐵 ∖ (𝑓 “ ∪ 𝐷))) = (𝐴 ∖ ∪ 𝐷)) |
13 | 12 | reseq2d 5888 |
. . . . . 6
⊢ (ran
𝑔 ⊆ 𝐴 → (◡𝑔 ↾ (𝑔 “ (𝐵 ∖ (𝑓 “ ∪ 𝐷)))) = (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) |
14 | 9, 13 | sylan9eqr 2801 |
. . . . 5
⊢ ((ran
𝑔 ⊆ 𝐴 ∧ Fun ◡𝑔) → ◡(𝑔 ↾ (𝐵 ∖ (𝑓 “ ∪ 𝐷))) = (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) |
15 | 14 | rneqd 5844 |
. . . 4
⊢ ((ran
𝑔 ⊆ 𝐴 ∧ Fun ◡𝑔) → ran ◡(𝑔 ↾ (𝐵 ∖ (𝑓 “ ∪ 𝐷))) = ran (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) |
16 | 8, 15 | sylan9eq 2799 |
. . 3
⊢ ((dom
𝑔 = 𝐵 ∧ (ran 𝑔 ⊆ 𝐴 ∧ Fun ◡𝑔)) → (𝐵 ∖ (𝑓 “ ∪ 𝐷)) = ran (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) |
17 | 16 | anassrs 467 |
. 2
⊢ (((dom
𝑔 = 𝐵 ∧ ran 𝑔 ⊆ 𝐴) ∧ Fun ◡𝑔) → (𝐵 ∖ (𝑓 “ ∪ 𝐷)) = ran (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) |
18 | 1, 17 | eqtr4id 2798 |
1
⊢ (((dom
𝑔 = 𝐵 ∧ ran 𝑔 ⊆ 𝐴) ∧ Fun ◡𝑔) → (◡𝑔 “ (𝐴 ∖ ∪ 𝐷)) = (𝐵 ∖ (𝑓 “ ∪ 𝐷))) |