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 × S S V H T × T cat H

Proof

Step Hyp Ref Expression
1 inss1 S T S
2 simpl x S T y S T x S T
3 2 elin2d x S T y S T x T
4 simpr x S T y S T y S T
5 4 elin2d x S T y S T y T
6 3 5 ovresd x S T y S T x H T × T y = x H y
7 eqimss x H T × T y = x H y x H T × T y x H y
8 6 7 syl x S T y S T x H T × T y x H y
9 8 rgen2 x S T y S T x H T × T y x H y
10 1 9 pm3.2i S T S x S T y S T x H T × T y x H y
11 simpl H Fn S × S S V H Fn S × S
12 inss1 S × S T × T S × S
13 fnssres H Fn S × S S × S T × T S × S H S × S T × T Fn S × S T × T
14 11 12 13 sylancl H Fn S × S S V H S × S T × T Fn S × S T × T
15 resres H S × S T × T = H S × S T × T
16 fnresdm H Fn S × S H S × S = H
17 16 adantr H Fn S × S S V H S × S = H
18 17 reseq1d H Fn S × S S V H S × S T × T = H T × T
19 15 18 eqtr3id H Fn S × S S V H S × S T × T = H T × T
20 inxp S × S T × T = S T × S T
21 20 a1i H Fn S × S S V S × S T × T = S T × S T
22 19 21 fneq12d H Fn S × S S V H S × S T × T Fn S × S T × T H T × T Fn S T × S T
23 14 22 mpbid H Fn S × S S V H T × T Fn S T × S T
24 simpr H Fn S × S S V S V
25 23 11 24 isssc H Fn S × S S V H T × T cat H S T S x S T y S T x H T × T y x H y
26 10 25 mpbiri H Fn S × S S V H T × T cat H