This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cores2

Description: Absorption of a reverse (preimage) restriction of the second member of a class composition. (Contributed by NM, 11-Dec-2006)

Ref Expression
Assertion cores2 ⊢ dom ⁡ A ⊆ C → A ∘ B -1 ↾ C -1 = A ∘ B

Proof

Step Hyp Ref Expression
1 dfdm4 ⊢ dom ⁡ A = ran ⁡ A -1
2 1 sseq1i ⊢ dom ⁡ A ⊆ C ↔ ran ⁡ A -1 ⊆ C
3 cores ⊢ ran ⁡ A -1 ⊆ C → B -1 ↾ C ∘ A -1 = B -1 ∘ A -1
4 2 3 sylbi ⊢ dom ⁡ A ⊆ C → B -1 ↾ C ∘ A -1 = B -1 ∘ A -1
5 cnvco ⊢ A ∘ B -1 ↾ C -1 -1 = B -1 ↾ C -1 -1 ∘ A -1
6 cocnvcnv1 ⊢ B -1 ↾ C -1 -1 ∘ A -1 = B -1 ↾ C ∘ A -1
7 5 6 eqtri ⊢ A ∘ B -1 ↾ C -1 -1 = B -1 ↾ C ∘ A -1
8 cnvco ⊢ A ∘ B -1 = B -1 ∘ A -1
9 4 7 8 3eqtr4g ⊢ dom ⁡ A ⊆ C → A ∘ B -1 ↾ C -1 -1 = A ∘ B -1
10 9 cnveqd ⊢ dom ⁡ A ⊆ C → A ∘ B -1 ↾ C -1 -1 -1 = A ∘ B -1 -1
11 relco ⊢ Rel ⁡ A ∘ B -1 ↾ C -1
12 dfrel2 ⊢ Rel ⁡ A ∘ B -1 ↾ C -1 ↔ A ∘ B -1 ↾ C -1 -1 -1 = A ∘ B -1 ↾ C -1
13 11 12 mpbi ⊢ A ∘ B -1 ↾ C -1 -1 -1 = A ∘ B -1 ↾ C -1
14 relco ⊢ Rel ⁡ A ∘ B
15 dfrel2 ⊢ Rel ⁡ A ∘ B ↔ A ∘ B -1 -1 = A ∘ B
16 14 15 mpbi ⊢ A ∘ B -1 -1 = A ∘ B
17 10 13 16 3eqtr3g ⊢ dom ⁡ A ⊆ C → A ∘ B -1 ↾ C -1 = A ∘ B