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 
|- ( ph -> H C_cat J )
sscfn2.2 
|- ( ph -> T = dom dom J )
Assertion sscfn2 
|- ( ph -> J Fn ( T X. T ) )

Proof

Step Hyp Ref Expression
1 sscfn1.1 
 |-  ( ph -> H C_cat J )
2 sscfn2.2 
 |-  ( ph -> T = dom dom J )
3 brssc 
 |-  ( H C_cat J <-> E. t ( J Fn ( t X. t ) /\ E. y e. ~P t H e. X_ x e. ( y X. y ) ~P ( J ` x ) ) )
4 1 3 sylib 
 |-  ( ph -> E. t ( J Fn ( t X. t ) /\ E. y e. ~P t H e. X_ x e. ( y X. y ) ~P ( J ` x ) ) )
5 simpr 
 |-  ( ( ph /\ J Fn ( t X. t ) ) -> J Fn ( t X. t ) )
6 2 adantr 
 |-  ( ( ph /\ J Fn ( t X. t ) ) -> T = dom dom J )
7 fndm 
 |-  ( J Fn ( t X. t ) -> dom J = ( t X. t ) )
8 7 adantl 
 |-  ( ( ph /\ J Fn ( t X. t ) ) -> dom J = ( t X. t ) )
9 8 dmeqd 
 |-  ( ( ph /\ J Fn ( t X. t ) ) -> dom dom J = dom ( t X. t ) )
10 dmxpid 
 |-  dom ( t X. t ) = t
11 9 10 eqtrdi 
 |-  ( ( ph /\ J Fn ( t X. t ) ) -> dom dom J = t )
12 6 11 eqtr2d 
 |-  ( ( ph /\ J Fn ( t X. t ) ) -> t = T )
13 12 sqxpeqd 
 |-  ( ( ph /\ J Fn ( t X. t ) ) -> ( t X. t ) = ( T X. T ) )
14 13 fneq2d 
 |-  ( ( ph /\ J Fn ( t X. t ) ) -> ( J Fn ( t X. t ) <-> J Fn ( T X. T ) ) )
15 5 14 mpbid 
 |-  ( ( ph /\ J Fn ( t X. t ) ) -> J Fn ( T X. T ) )
16 15 ex 
 |-  ( ph -> ( J Fn ( t X. t ) -> J Fn ( T X. T ) ) )
17 16 adantrd 
 |-  ( ph -> ( ( J Fn ( t X. t ) /\ E. y e. ~P t H e. X_ x e. ( y X. y ) ~P ( J ` x ) ) -> J Fn ( T X. T ) ) )
18 17 exlimdv 
 |-  ( ph -> ( E. t ( J Fn ( t X. t ) /\ E. y e. ~P t H e. X_ x e. ( y X. y ) ~P ( J ` x ) ) -> J Fn ( T X. T ) ) )
19 4 18 mpd 
 |-  ( ph -> J Fn ( T X. T ) )