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