Metamath Proof Explorer

Theorem resabs1

Description: Absorption law for restriction. Exercise 17 of TakeutiZaring p. 25. (Contributed by NM, 9-Aug-1994)

Ref Expression
Assertion resabs1 
|- ( B C_ C -> ( ( A |` C ) |` B ) = ( A |` B ) )

Proof

Step Hyp Ref Expression
1 resres 
 |-  ( ( A |` C ) |` B ) = ( A |` ( C i^i B ) )
2 sseqin2 
 |-  ( B C_ C <-> ( C i^i B ) = B )
3 reseq2 
 |-  ( ( C i^i B ) = B -> ( A |` ( C i^i B ) ) = ( A |` B ) )
4 2 3 sylbi 
 |-  ( B C_ C -> ( A |` ( C i^i B ) ) = ( A |` B ) )
5 1 4 syl5eq 
 |-  ( B C_ C -> ( ( A |` C ) |` B ) = ( A |` B ) )