Metamath Proof Explorer


Theorem sscfn2

Description: The subcategory subset relation is defined on functions with square domain. (Contributed by Mario Carneiro, 6-Jan-2017)

Ref Expression
Hypotheses sscfn1.1 φ H cat J
sscfn2.2 φ T = dom dom J
Assertion sscfn2 φ J Fn T × T

Proof

Step Hyp Ref Expression
1 sscfn1.1 φ H cat J
2 sscfn2.2 φ T = dom dom J
3 brssc H cat J t J Fn t × t y 𝒫 t H x y × y 𝒫 J x
4 1 3 sylib φ t J Fn t × t y 𝒫 t H x y × y 𝒫 J x
5 simpr φ J Fn t × t J Fn t × t
6 2 adantr φ J Fn t × t T = dom dom J
7 fndm J Fn t × t dom J = t × t
8 7 adantl φ J Fn t × t dom J = t × t
9 8 dmeqd φ J Fn t × t dom dom J = dom t × t
10 dmxpid dom t × t = t
11 9 10 eqtrdi φ J Fn t × t dom dom J = t
12 6 11 eqtr2d φ J Fn t × t t = T
13 12 sqxpeqd φ J Fn t × t t × t = T × T
14 13 fneq2d φ J Fn t × t J Fn t × t J Fn T × T
15 5 14 mpbid φ J Fn t × t J Fn T × T
16 15 ex φ J Fn t × t J Fn T × T
17 16 adantrd φ J Fn t × t y 𝒫 t H x y × y 𝒫 J x J Fn T × T
18 17 exlimdv φ t J Fn t × t y 𝒫 t H x y × y 𝒫 J x J Fn T × T
19 4 18 mpd φ J Fn T × T