Proof of Theorem sbthlem8
Step | Hyp | Ref
| Expression |
1 | | funres11 6513 |
. . . 4
⊢ (Fun
◡𝑓 → Fun ◡(𝑓 ↾ ∪ 𝐷)) |
2 | | funcnvcnv 6503 |
. . . . . 6
⊢ (Fun
𝑔 → Fun ◡◡𝑔) |
3 | | funres11 6513 |
. . . . . 6
⊢ (Fun
◡◡𝑔 → Fun ◡(◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) |
4 | 2, 3 | syl 17 |
. . . . 5
⊢ (Fun
𝑔 → Fun ◡(◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) |
5 | 4 | ad3antrrr 727 |
. . . 4
⊢ ((((Fun
𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔 ⊆ 𝐴) ∧ Fun ◡𝑔) → Fun ◡(◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) |
6 | 1, 5 | anim12i 613 |
. . 3
⊢ ((Fun
◡𝑓 ∧ (((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔 ⊆ 𝐴) ∧ Fun ◡𝑔)) → (Fun ◡(𝑓 ↾ ∪ 𝐷) ∧ Fun ◡(◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷)))) |
7 | | df-ima 5604 |
. . . . . . . 8
⊢ (𝑓 “ ∪ 𝐷) =
ran (𝑓 ↾ ∪ 𝐷) |
8 | | df-rn 5602 |
. . . . . . . 8
⊢ ran
(𝑓 ↾ ∪ 𝐷) =
dom ◡(𝑓 ↾ ∪ 𝐷) |
9 | 7, 8 | eqtr2i 2767 |
. . . . . . 7
⊢ dom ◡(𝑓 ↾ ∪ 𝐷) = (𝑓 “ ∪ 𝐷) |
10 | | df-ima 5604 |
. . . . . . . . 9
⊢ (◡𝑔 “ (𝐴 ∖ ∪ 𝐷)) = ran (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷)) |
11 | | df-rn 5602 |
. . . . . . . . 9
⊢ ran
(◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷)) = dom ◡(◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷)) |
12 | 10, 11 | eqtri 2766 |
. . . . . . . 8
⊢ (◡𝑔 “ (𝐴 ∖ ∪ 𝐷)) = dom ◡(◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷)) |
13 | | sbthlem.1 |
. . . . . . . . 9
⊢ 𝐴 ∈ V |
14 | | sbthlem.2 |
. . . . . . . . 9
⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))} |
15 | 13, 14 | sbthlem4 8871 |
. . . . . . . 8
⊢ (((dom
𝑔 = 𝐵 ∧ ran 𝑔 ⊆ 𝐴) ∧ Fun ◡𝑔) → (◡𝑔 “ (𝐴 ∖ ∪ 𝐷)) = (𝐵 ∖ (𝑓 “ ∪ 𝐷))) |
16 | 12, 15 | eqtr3id 2792 |
. . . . . . 7
⊢ (((dom
𝑔 = 𝐵 ∧ ran 𝑔 ⊆ 𝐴) ∧ Fun ◡𝑔) → dom ◡(◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷)) = (𝐵 ∖ (𝑓 “ ∪ 𝐷))) |
17 | | ineq12 4143 |
. . . . . . 7
⊢ ((dom
◡(𝑓 ↾ ∪ 𝐷) = (𝑓 “ ∪ 𝐷) ∧ dom ◡(◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷)) = (𝐵 ∖ (𝑓 “ ∪ 𝐷))) → (dom ◡(𝑓 ↾ ∪ 𝐷) ∩ dom ◡(◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) = ((𝑓 “ ∪ 𝐷) ∩ (𝐵 ∖ (𝑓 “ ∪ 𝐷)))) |
18 | 9, 16, 17 | sylancr 587 |
. . . . . 6
⊢ (((dom
𝑔 = 𝐵 ∧ ran 𝑔 ⊆ 𝐴) ∧ Fun ◡𝑔) → (dom ◡(𝑓 ↾ ∪ 𝐷) ∩ dom ◡(◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) = ((𝑓 “ ∪ 𝐷) ∩ (𝐵 ∖ (𝑓 “ ∪ 𝐷)))) |
19 | | disjdif 4407 |
. . . . . 6
⊢ ((𝑓 “ ∪ 𝐷)
∩ (𝐵 ∖ (𝑓 “ ∪ 𝐷)))
= ∅ |
20 | 18, 19 | eqtrdi 2794 |
. . . . 5
⊢ (((dom
𝑔 = 𝐵 ∧ ran 𝑔 ⊆ 𝐴) ∧ Fun ◡𝑔) → (dom ◡(𝑓 ↾ ∪ 𝐷) ∩ dom ◡(◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) = ∅) |
21 | 20 | adantlll 715 |
. . . 4
⊢ ((((Fun
𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔 ⊆ 𝐴) ∧ Fun ◡𝑔) → (dom ◡(𝑓 ↾ ∪ 𝐷) ∩ dom ◡(◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) = ∅) |
22 | 21 | adantl 482 |
. . 3
⊢ ((Fun
◡𝑓 ∧ (((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔 ⊆ 𝐴) ∧ Fun ◡𝑔)) → (dom ◡(𝑓 ↾ ∪ 𝐷) ∩ dom ◡(◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) = ∅) |
23 | | funun 6482 |
. . 3
⊢ (((Fun
◡(𝑓 ↾ ∪ 𝐷) ∧ Fun ◡(◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) ∧ (dom ◡(𝑓 ↾ ∪ 𝐷) ∩ dom ◡(◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) = ∅) → Fun (◡(𝑓 ↾ ∪ 𝐷) ∪ ◡(◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷)))) |
24 | 6, 22, 23 | syl2anc 584 |
. 2
⊢ ((Fun
◡𝑓 ∧ (((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔 ⊆ 𝐴) ∧ Fun ◡𝑔)) → Fun (◡(𝑓 ↾ ∪ 𝐷) ∪ ◡(◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷)))) |
25 | | sbthlem.3 |
. . . . 5
⊢ 𝐻 = ((𝑓 ↾ ∪ 𝐷) ∪ (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) |
26 | 25 | cnveqi 5785 |
. . . 4
⊢ ◡𝐻 = ◡((𝑓 ↾ ∪ 𝐷) ∪ (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) |
27 | | cnvun 6048 |
. . . 4
⊢ ◡((𝑓 ↾ ∪ 𝐷) ∪ (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) = (◡(𝑓 ↾ ∪ 𝐷) ∪ ◡(◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) |
28 | 26, 27 | eqtri 2766 |
. . 3
⊢ ◡𝐻 = (◡(𝑓 ↾ ∪ 𝐷) ∪ ◡(◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) |
29 | 28 | funeqi 6457 |
. 2
⊢ (Fun
◡𝐻 ↔ Fun (◡(𝑓 ↾ ∪ 𝐷) ∪ ◡(◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷)))) |
30 | 24, 29 | sylibr 233 |
1
⊢ ((Fun
◡𝑓 ∧ (((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔 ⊆ 𝐴) ∧ Fun ◡𝑔)) → Fun ◡𝐻) |