Proof of Theorem sbthlemi8
Step | Hyp | Ref
| Expression |
1 | | funres11 5245 |
. . . 4
⊢ (Fun
◡𝑓 → Fun ◡(𝑓 ↾ ∪ 𝐷)) |
2 | 1 | ad2antlr 481 |
. . 3
⊢
(((EXMID ∧ Fun ◡𝑓) ∧ (((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔 ⊆ 𝐴) ∧ Fun ◡𝑔)) → Fun ◡(𝑓 ↾ ∪ 𝐷)) |
3 | | funcnvcnv 5232 |
. . . . . 6
⊢ (Fun
𝑔 → Fun ◡◡𝑔) |
4 | | funres11 5245 |
. . . . . 6
⊢ (Fun
◡◡𝑔 → Fun ◡(◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) |
5 | 3, 4 | syl 14 |
. . . . 5
⊢ (Fun
𝑔 → Fun ◡(◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) |
6 | 5 | ad2antrr 480 |
. . . 4
⊢ (((Fun
𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔 ⊆ 𝐴) → Fun ◡(◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) |
7 | 6 | ad2antrl 482 |
. . 3
⊢
(((EXMID ∧ Fun ◡𝑓) ∧ (((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔 ⊆ 𝐴) ∧ Fun ◡𝑔)) → Fun ◡(◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) |
8 | | simpll 519 |
. . . 4
⊢
(((EXMID ∧ Fun ◡𝑓) ∧ (((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔 ⊆ 𝐴) ∧ Fun ◡𝑔)) →
EXMID) |
9 | | simprll 527 |
. . . . 5
⊢
(((EXMID ∧ Fun ◡𝑓) ∧ (((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔 ⊆ 𝐴) ∧ Fun ◡𝑔)) → (Fun 𝑔 ∧ dom 𝑔 = 𝐵)) |
10 | 9 | simprd 113 |
. . . 4
⊢
(((EXMID ∧ Fun ◡𝑓) ∧ (((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔 ⊆ 𝐴) ∧ Fun ◡𝑔)) → dom 𝑔 = 𝐵) |
11 | | simprlr 528 |
. . . 4
⊢
(((EXMID ∧ Fun ◡𝑓) ∧ (((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔 ⊆ 𝐴) ∧ Fun ◡𝑔)) → ran 𝑔 ⊆ 𝐴) |
12 | | simprr 522 |
. . . 4
⊢
(((EXMID ∧ Fun ◡𝑓) ∧ (((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔 ⊆ 𝐴) ∧ Fun ◡𝑔)) → Fun ◡𝑔) |
13 | | df-ima 4602 |
. . . . . . 7
⊢ (𝑓 “ ∪ 𝐷) =
ran (𝑓 ↾ ∪ 𝐷) |
14 | | df-rn 4600 |
. . . . . . 7
⊢ ran
(𝑓 ↾ ∪ 𝐷) =
dom ◡(𝑓 ↾ ∪ 𝐷) |
15 | 13, 14 | eqtr2i 2179 |
. . . . . 6
⊢ dom ◡(𝑓 ↾ ∪ 𝐷) = (𝑓 “ ∪ 𝐷) |
16 | | df-ima 4602 |
. . . . . . . 8
⊢ (◡𝑔 “ (𝐴 ∖ ∪ 𝐷)) = ran (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷)) |
17 | | df-rn 4600 |
. . . . . . . 8
⊢ ran
(◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷)) = dom ◡(◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷)) |
18 | 16, 17 | eqtri 2178 |
. . . . . . 7
⊢ (◡𝑔 “ (𝐴 ∖ ∪ 𝐷)) = dom ◡(◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷)) |
19 | | sbthlem.1 |
. . . . . . . 8
⊢ 𝐴 ∈ V |
20 | | sbthlem.2 |
. . . . . . . 8
⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))} |
21 | 19, 20 | sbthlemi4 6907 |
. . . . . . 7
⊢
((EXMID ∧ (dom 𝑔 = 𝐵 ∧ ran 𝑔 ⊆ 𝐴) ∧ Fun ◡𝑔) → (◡𝑔 “ (𝐴 ∖ ∪ 𝐷)) = (𝐵 ∖ (𝑓 “ ∪ 𝐷))) |
22 | 18, 21 | eqtr3id 2204 |
. . . . . 6
⊢
((EXMID ∧ (dom 𝑔 = 𝐵 ∧ ran 𝑔 ⊆ 𝐴) ∧ Fun ◡𝑔) → dom ◡(◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷)) = (𝐵 ∖ (𝑓 “ ∪ 𝐷))) |
23 | | ineq12 3304 |
. . . . . 6
⊢ ((dom
◡(𝑓 ↾ ∪ 𝐷) = (𝑓 “ ∪ 𝐷) ∧ dom ◡(◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷)) = (𝐵 ∖ (𝑓 “ ∪ 𝐷))) → (dom ◡(𝑓 ↾ ∪ 𝐷) ∩ dom ◡(◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) = ((𝑓 “ ∪ 𝐷) ∩ (𝐵 ∖ (𝑓 “ ∪ 𝐷)))) |
24 | 15, 22, 23 | sylancr 411 |
. . . . 5
⊢
((EXMID ∧ (dom 𝑔 = 𝐵 ∧ ran 𝑔 ⊆ 𝐴) ∧ Fun ◡𝑔) → (dom ◡(𝑓 ↾ ∪ 𝐷) ∩ dom ◡(◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) = ((𝑓 “ ∪ 𝐷) ∩ (𝐵 ∖ (𝑓 “ ∪ 𝐷)))) |
25 | | disjdif 3467 |
. . . . 5
⊢ ((𝑓 “ ∪ 𝐷)
∩ (𝐵 ∖ (𝑓 “ ∪ 𝐷)))
= ∅ |
26 | 24, 25 | eqtrdi 2206 |
. . . 4
⊢
((EXMID ∧ (dom 𝑔 = 𝐵 ∧ ran 𝑔 ⊆ 𝐴) ∧ Fun ◡𝑔) → (dom ◡(𝑓 ↾ ∪ 𝐷) ∩ dom ◡(◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) = ∅) |
27 | 8, 10, 11, 12, 26 | syl121anc 1225 |
. . 3
⊢
(((EXMID ∧ Fun ◡𝑓) ∧ (((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔 ⊆ 𝐴) ∧ Fun ◡𝑔)) → (dom ◡(𝑓 ↾ ∪ 𝐷) ∩ dom ◡(◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) = ∅) |
28 | | funun 5217 |
. . 3
⊢ (((Fun
◡(𝑓 ↾ ∪ 𝐷) ∧ Fun ◡(◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) ∧ (dom ◡(𝑓 ↾ ∪ 𝐷) ∩ dom ◡(◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) = ∅) → Fun (◡(𝑓 ↾ ∪ 𝐷) ∪ ◡(◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷)))) |
29 | 2, 7, 27, 28 | syl21anc 1219 |
. 2
⊢
(((EXMID ∧ Fun ◡𝑓) ∧ (((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔 ⊆ 𝐴) ∧ Fun ◡𝑔)) → Fun (◡(𝑓 ↾ ∪ 𝐷) ∪ ◡(◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷)))) |
30 | | sbthlem.3 |
. . . . 5
⊢ 𝐻 = ((𝑓 ↾ ∪ 𝐷) ∪ (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) |
31 | 30 | cnveqi 4764 |
. . . 4
⊢ ◡𝐻 = ◡((𝑓 ↾ ∪ 𝐷) ∪ (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) |
32 | | cnvun 4994 |
. . . 4
⊢ ◡((𝑓 ↾ ∪ 𝐷) ∪ (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) = (◡(𝑓 ↾ ∪ 𝐷) ∪ ◡(◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) |
33 | 31, 32 | eqtri 2178 |
. . 3
⊢ ◡𝐻 = (◡(𝑓 ↾ ∪ 𝐷) ∪ ◡(◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) |
34 | 33 | funeqi 5194 |
. 2
⊢ (Fun
◡𝐻 ↔ Fun (◡(𝑓 ↾ ∪ 𝐷) ∪ ◡(◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷)))) |
35 | 29, 34 | sylibr 133 |
1
⊢
(((EXMID ∧ Fun ◡𝑓) ∧ (((Fun 𝑔 ∧ dom 𝑔 = 𝐵) ∧ ran 𝑔 ⊆ 𝐴) ∧ Fun ◡𝑔)) → Fun ◡𝐻) |