Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  sscfn1 Structured version   Unicode version

Theorem sscfn1 14019
 Description: The subcategory subset relation is defined on functions with square domain. (Contributed by Mario Carneiro, 6-Jan-2017.)
Hypotheses
Ref Expression
sscfn1.1 cat
sscfn1.2
Assertion
Ref Expression
sscfn1

Proof of Theorem sscfn1
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 sscfn1.1 . . 3 cat
2 brssc 14016 . . 3 cat
31, 2sylib 190 . 2
4 ixpfn 7070 . . . . . 6
5 simpr 449 . . . . . . . 8
6 sscfn1.2 . . . . . . . . . . . 12
76adantr 453 . . . . . . . . . . 11
8 fndm 5546 . . . . . . . . . . . . . 14
98adantl 454 . . . . . . . . . . . . 13
109dmeqd 5074 . . . . . . . . . . . 12
11 dmxpid 5091 . . . . . . . . . . . 12
1210, 11syl6eq 2486 . . . . . . . . . . 11
137, 12eqtr2d 2471 . . . . . . . . . 10
1413, 13xpeq12d 4905 . . . . . . . . 9
1514fneq2d 5539 . . . . . . . 8
165, 15mpbid 203 . . . . . . 7
1716ex 425 . . . . . 6
184, 17syl5 31 . . . . 5
1918rexlimdvw 2835 . . . 4