Proof of Theorem mvdco
| Step | Hyp | Ref
| Expression |
| 1 | | inundif 4479 |
. . . . . . . 8
⊢ ((𝐺 ∩ I ) ∪ (𝐺 ∖ I )) = 𝐺 |
| 2 | 1 | coeq2i 5871 |
. . . . . . 7
⊢ (𝐹 ∘ ((𝐺 ∩ I ) ∪ (𝐺 ∖ I ))) = (𝐹 ∘ 𝐺) |
| 3 | | coundi 6267 |
. . . . . . 7
⊢ (𝐹 ∘ ((𝐺 ∩ I ) ∪ (𝐺 ∖ I ))) = ((𝐹 ∘ (𝐺 ∩ I )) ∪ (𝐹 ∘ (𝐺 ∖ I ))) |
| 4 | 2, 3 | eqtr3i 2767 |
. . . . . 6
⊢ (𝐹 ∘ 𝐺) = ((𝐹 ∘ (𝐺 ∩ I )) ∪ (𝐹 ∘ (𝐺 ∖ I ))) |
| 5 | 4 | difeq1i 4122 |
. . . . 5
⊢ ((𝐹 ∘ 𝐺) ∖ I ) = (((𝐹 ∘ (𝐺 ∩ I )) ∪ (𝐹 ∘ (𝐺 ∖ I ))) ∖ I ) |
| 6 | | difundir 4291 |
. . . . 5
⊢ (((𝐹 ∘ (𝐺 ∩ I )) ∪ (𝐹 ∘ (𝐺 ∖ I ))) ∖ I ) = (((𝐹 ∘ (𝐺 ∩ I )) ∖ I ) ∪ ((𝐹 ∘ (𝐺 ∖ I )) ∖ I )) |
| 7 | 5, 6 | eqtri 2765 |
. . . 4
⊢ ((𝐹 ∘ 𝐺) ∖ I ) = (((𝐹 ∘ (𝐺 ∩ I )) ∖ I ) ∪ ((𝐹 ∘ (𝐺 ∖ I )) ∖ I )) |
| 8 | 7 | dmeqi 5915 |
. . 3
⊢ dom
((𝐹 ∘ 𝐺) ∖ I ) = dom (((𝐹 ∘ (𝐺 ∩ I )) ∖ I ) ∪ ((𝐹 ∘ (𝐺 ∖ I )) ∖ I )) |
| 9 | | dmun 5921 |
. . 3
⊢ dom
(((𝐹 ∘ (𝐺 ∩ I )) ∖ I ) ∪
((𝐹 ∘ (𝐺 ∖ I )) ∖ I )) =
(dom ((𝐹 ∘ (𝐺 ∩ I )) ∖ I ) ∪
dom ((𝐹 ∘ (𝐺 ∖ I )) ∖ I
)) |
| 10 | 8, 9 | eqtri 2765 |
. 2
⊢ dom
((𝐹 ∘ 𝐺) ∖ I ) = (dom ((𝐹 ∘ (𝐺 ∩ I )) ∖ I ) ∪ dom ((𝐹 ∘ (𝐺 ∖ I )) ∖ I )) |
| 11 | | inss2 4238 |
. . . . . 6
⊢ (𝐺 ∩ I ) ⊆
I |
| 12 | | coss2 5867 |
. . . . . 6
⊢ ((𝐺 ∩ I ) ⊆ I →
(𝐹 ∘ (𝐺 ∩ I )) ⊆ (𝐹 ∘ I )) |
| 13 | 11, 12 | ax-mp 5 |
. . . . 5
⊢ (𝐹 ∘ (𝐺 ∩ I )) ⊆ (𝐹 ∘ I ) |
| 14 | | cocnvcnv1 6277 |
. . . . . . 7
⊢ (◡◡𝐹 ∘ I ) = (𝐹 ∘ I ) |
| 15 | | relcnv 6122 |
. . . . . . . 8
⊢ Rel ◡◡𝐹 |
| 16 | | coi1 6282 |
. . . . . . . 8
⊢ (Rel
◡◡𝐹 → (◡◡𝐹 ∘ I ) = ◡◡𝐹) |
| 17 | 15, 16 | ax-mp 5 |
. . . . . . 7
⊢ (◡◡𝐹 ∘ I ) = ◡◡𝐹 |
| 18 | 14, 17 | eqtr3i 2767 |
. . . . . 6
⊢ (𝐹 ∘ I ) = ◡◡𝐹 |
| 19 | | cnvcnvss 6214 |
. . . . . 6
⊢ ◡◡𝐹 ⊆ 𝐹 |
| 20 | 18, 19 | eqsstri 4030 |
. . . . 5
⊢ (𝐹 ∘ I ) ⊆ 𝐹 |
| 21 | 13, 20 | sstri 3993 |
. . . 4
⊢ (𝐹 ∘ (𝐺 ∩ I )) ⊆ 𝐹 |
| 22 | | ssdif 4144 |
. . . 4
⊢ ((𝐹 ∘ (𝐺 ∩ I )) ⊆ 𝐹 → ((𝐹 ∘ (𝐺 ∩ I )) ∖ I ) ⊆ (𝐹 ∖ I )) |
| 23 | | dmss 5913 |
. . . 4
⊢ (((𝐹 ∘ (𝐺 ∩ I )) ∖ I ) ⊆ (𝐹 ∖ I ) → dom ((𝐹 ∘ (𝐺 ∩ I )) ∖ I ) ⊆ dom (𝐹 ∖ I )) |
| 24 | 21, 22, 23 | mp2b 10 |
. . 3
⊢ dom
((𝐹 ∘ (𝐺 ∩ I )) ∖ I ) ⊆
dom (𝐹 ∖ I
) |
| 25 | | difss 4136 |
. . . . 5
⊢ ((𝐹 ∘ (𝐺 ∖ I )) ∖ I ) ⊆ (𝐹 ∘ (𝐺 ∖ I )) |
| 26 | | dmss 5913 |
. . . . 5
⊢ (((𝐹 ∘ (𝐺 ∖ I )) ∖ I ) ⊆ (𝐹 ∘ (𝐺 ∖ I )) → dom ((𝐹 ∘ (𝐺 ∖ I )) ∖ I ) ⊆ dom (𝐹 ∘ (𝐺 ∖ I ))) |
| 27 | 25, 26 | ax-mp 5 |
. . . 4
⊢ dom
((𝐹 ∘ (𝐺 ∖ I )) ∖ I )
⊆ dom (𝐹 ∘
(𝐺 ∖ I
)) |
| 28 | | dmcoss 5985 |
. . . 4
⊢ dom
(𝐹 ∘ (𝐺 ∖ I )) ⊆ dom (𝐺 ∖ I ) |
| 29 | 27, 28 | sstri 3993 |
. . 3
⊢ dom
((𝐹 ∘ (𝐺 ∖ I )) ∖ I )
⊆ dom (𝐺 ∖ I
) |
| 30 | | unss12 4188 |
. . 3
⊢ ((dom
((𝐹 ∘ (𝐺 ∩ I )) ∖ I ) ⊆
dom (𝐹 ∖ I ) ∧
dom ((𝐹 ∘ (𝐺 ∖ I )) ∖ I )
⊆ dom (𝐺 ∖ I ))
→ (dom ((𝐹 ∘
(𝐺 ∩ I )) ∖ I )
∪ dom ((𝐹 ∘
(𝐺 ∖ I )) ∖ I
)) ⊆ (dom (𝐹 ∖
I ) ∪ dom (𝐺 ∖ I
))) |
| 31 | 24, 29, 30 | mp2an 692 |
. 2
⊢ (dom
((𝐹 ∘ (𝐺 ∩ I )) ∖ I ) ∪
dom ((𝐹 ∘ (𝐺 ∖ I )) ∖ I ))
⊆ (dom (𝐹 ∖ I )
∪ dom (𝐺 ∖ I
)) |
| 32 | 10, 31 | eqsstri 4030 |
1
⊢ dom
((𝐹 ∘ 𝐺) ∖ I ) ⊆ (dom
(𝐹 ∖ I ) ∪ dom
(𝐺 ∖ I
)) |