Metamath Proof Explorer

Theorem sscfn1

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 )
sscfn1.2 
|- ( ph -> S = dom dom H )
Assertion sscfn1 
|- ( ph -> H Fn ( S X. S ) )

Proof

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