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 𝐴 ⊆ 𝐶 → ( 𝐴 ∘ ◡ ( ◡ 𝐵 ↾ 𝐶 ) ) = ( 𝐴 ∘ 𝐵 ) )

Proof

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