Metamath Proof Explorer

Theorem sscres

Description: Any function restricted to a square domain is a subcategory subset of the original. (Contributed by Mario Carneiro, 6-Jan-2017)

Ref Expression
Assertion sscres 
|- ( ( H Fn ( S X. S ) /\ S e. V ) -> ( H |` ( T X. T ) ) C_cat H )

Proof

Step Hyp Ref Expression
1 inss1 
 |-  ( S i^i T ) C_ S
2 simpl 
 |-  ( ( x e. ( S i^i T ) /\ y e. ( S i^i T ) ) -> x e. ( S i^i T ) )
3 2 elin2d 
 |-  ( ( x e. ( S i^i T ) /\ y e. ( S i^i T ) ) -> x e. T )
4 simpr 
 |-  ( ( x e. ( S i^i T ) /\ y e. ( S i^i T ) ) -> y e. ( S i^i T ) )
5 4 elin2d 
 |-  ( ( x e. ( S i^i T ) /\ y e. ( S i^i T ) ) -> y e. T )
6 3 5 ovresd 
 |-  ( ( x e. ( S i^i T ) /\ y e. ( S i^i T ) ) -> ( x ( H |` ( T X. T ) ) y ) = ( x H y ) )
7 eqimss 
 |-  ( ( x ( H |` ( T X. T ) ) y ) = ( x H y ) -> ( x ( H |` ( T X. T ) ) y ) C_ ( x H y ) )
8 6 7 syl 
 |-  ( ( x e. ( S i^i T ) /\ y e. ( S i^i T ) ) -> ( x ( H |` ( T X. T ) ) y ) C_ ( x H y ) )
9 8 rgen2 
 |-  A. x e. ( S i^i T ) A. y e. ( S i^i T ) ( x ( H |` ( T X. T ) ) y ) C_ ( x H y )
10 1 9 pm3.2i 
 |-  ( ( S i^i T ) C_ S /\ A. x e. ( S i^i T ) A. y e. ( S i^i T ) ( x ( H |` ( T X. T ) ) y ) C_ ( x H y ) )
11 simpl 
 |-  ( ( H Fn ( S X. S ) /\ S e. V ) -> H Fn ( S X. S ) )
12 inss1 
 |-  ( ( S X. S ) i^i ( T X. T ) ) C_ ( S X. S )
13 fnssres 
 |-  ( ( H Fn ( S X. S ) /\ ( ( S X. S ) i^i ( T X. T ) ) C_ ( S X. S ) ) -> ( H |` ( ( S X. S ) i^i ( T X. T ) ) ) Fn ( ( S X. S ) i^i ( T X. T ) ) )
14 11 12 13 sylancl 
 |-  ( ( H Fn ( S X. S ) /\ S e. V ) -> ( H |` ( ( S X. S ) i^i ( T X. T ) ) ) Fn ( ( S X. S ) i^i ( T X. T ) ) )
15 resres 
 |-  ( ( H |` ( S X. S ) ) |` ( T X. T ) ) = ( H |` ( ( S X. S ) i^i ( T X. T ) ) )
16 fnresdm 
 |-  ( H Fn ( S X. S ) -> ( H |` ( S X. S ) ) = H )
17 16 adantr 
 |-  ( ( H Fn ( S X. S ) /\ S e. V ) -> ( H |` ( S X. S ) ) = H )
18 17 reseq1d 
 |-  ( ( H Fn ( S X. S ) /\ S e. V ) -> ( ( H |` ( S X. S ) ) |` ( T X. T ) ) = ( H |` ( T X. T ) ) )
19 15 18 eqtr3id 
 |-  ( ( H Fn ( S X. S ) /\ S e. V ) -> ( H |` ( ( S X. S ) i^i ( T X. T ) ) ) = ( H |` ( T X. T ) ) )
20 inxp 
 |-  ( ( S X. S ) i^i ( T X. T ) ) = ( ( S i^i T ) X. ( S i^i T ) )
21 20 a1i 
 |-  ( ( H Fn ( S X. S ) /\ S e. V ) -> ( ( S X. S ) i^i ( T X. T ) ) = ( ( S i^i T ) X. ( S i^i T ) ) )
22 19 21 fneq12d 
 |-  ( ( H Fn ( S X. S ) /\ S e. V ) -> ( ( H |` ( ( S X. S ) i^i ( T X. T ) ) ) Fn ( ( S X. S ) i^i ( T X. T ) ) <-> ( H |` ( T X. T ) ) Fn ( ( S i^i T ) X. ( S i^i T ) ) ) )
23 14 22 mpbid 
 |-  ( ( H Fn ( S X. S ) /\ S e. V ) -> ( H |` ( T X. T ) ) Fn ( ( S i^i T ) X. ( S i^i T ) ) )
24 simpr 
 |-  ( ( H Fn ( S X. S ) /\ S e. V ) -> S e. V )
25 23 11 24 isssc 
 |-  ( ( H Fn ( S X. S ) /\ S e. V ) -> ( ( H |` ( T X. T ) ) C_cat H <-> ( ( S i^i T ) C_ S /\ A. x e. ( S i^i T ) A. y e. ( S i^i T ) ( x ( H |` ( T X. T ) ) y ) C_ ( x H y ) ) ) )
26 10 25 mpbiri 
 |-  ( ( H Fn ( S X. S ) /\ S e. V ) -> ( H |` ( T X. T ) ) C_cat H )