Metamath Proof Explorer

Theorem isssc

Description: Value of the subcategory subset relation when the arguments are known functions. (Contributed by Mario Carneiro, 6-Jan-2017)

Ref Expression
Hypotheses isssc.1 
|- ( ph -> H Fn ( S X. S ) )
isssc.2 
|- ( ph -> J Fn ( T X. T ) )
isssc.3 
|- ( ph -> T e. V )
Assertion isssc 
|- ( ph -> ( H C_cat J <-> ( S C_ T /\ A. x e. S A. y e. S ( x H y ) C_ ( x J y ) ) ) )

Proof

Step Hyp Ref Expression
1 isssc.1 
 |-  ( ph -> H Fn ( S X. S ) )
2 isssc.2 
 |-  ( ph -> J Fn ( T X. T ) )
3 isssc.3 
 |-  ( ph -> T e. V )
4 brssc 
 |-  ( H C_cat J <-> E. t ( J Fn ( t X. t ) /\ E. s e. ~P t H e. X_ z e. ( s X. s ) ~P ( J ` z ) ) )
5 fndm 
 |-  ( J Fn ( t X. t ) -> dom J = ( t X. t ) )
6 5 adantl 
 |-  ( ( ph /\ J Fn ( t X. t ) ) -> dom J = ( t X. t ) )
7 2 adantr 
 |-  ( ( ph /\ J Fn ( t X. t ) ) -> J Fn ( T X. T ) )
8 7 fndmd 
 |-  ( ( ph /\ J Fn ( t X. t ) ) -> dom J = ( T X. T ) )
9 6 8 eqtr3d 
 |-  ( ( ph /\ J Fn ( t X. t ) ) -> ( t X. t ) = ( T X. T ) )
10 9 dmeqd 
 |-  ( ( ph /\ J Fn ( t X. t ) ) -> dom ( t X. t ) = dom ( T X. T ) )
11 dmxpid 
 |-  dom ( t X. t ) = t
12 dmxpid 
 |-  dom ( T X. T ) = T
13 10 11 12 3eqtr3g 
 |-  ( ( ph /\ J Fn ( t X. t ) ) -> t = T )
14 13 ex 
 |-  ( ph -> ( J Fn ( t X. t ) -> t = T ) )
15 id 
 |-  ( t = T -> t = T )
16 15 sqxpeqd 
 |-  ( t = T -> ( t X. t ) = ( T X. T ) )
17 16 fneq2d 
 |-  ( t = T -> ( J Fn ( t X. t ) <-> J Fn ( T X. T ) ) )
18 2 17 syl5ibrcom 
 |-  ( ph -> ( t = T -> J Fn ( t X. t ) ) )
19 14 18 impbid 
 |-  ( ph -> ( J Fn ( t X. t ) <-> t = T ) )
20 19 anbi1d 
 |-  ( ph -> ( ( J Fn ( t X. t ) /\ E. s e. ~P t H e. X_ z e. ( s X. s ) ~P ( J ` z ) ) <-> ( t = T /\ E. s e. ~P t H e. X_ z e. ( s X. s ) ~P ( J ` z ) ) ) )
21 20 exbidv 
 |-  ( ph -> ( E. t ( J Fn ( t X. t ) /\ E. s e. ~P t H e. X_ z e. ( s X. s ) ~P ( J ` z ) ) <-> E. t ( t = T /\ E. s e. ~P t H e. X_ z e. ( s X. s ) ~P ( J ` z ) ) ) )
22 4 21 syl5bb 
 |-  ( ph -> ( H C_cat J <-> E. t ( t = T /\ E. s e. ~P t H e. X_ z e. ( s X. s ) ~P ( J ` z ) ) ) )
23 pweq 
 |-  ( t = T -> ~P t = ~P T )
24 23 rexeqdv 
 |-  ( t = T -> ( E. s e. ~P t H e. X_ z e. ( s X. s ) ~P ( J ` z ) <-> E. s e. ~P T H e. X_ z e. ( s X. s ) ~P ( J ` z ) ) )
25 24 ceqsexgv 
 |-  ( T e. V -> ( E. t ( t = T /\ E. s e. ~P t H e. X_ z e. ( s X. s ) ~P ( J ` z ) ) <-> E. s e. ~P T H e. X_ z e. ( s X. s ) ~P ( J ` z ) ) )
26 3 25 syl 
 |-  ( ph -> ( E. t ( t = T /\ E. s e. ~P t H e. X_ z e. ( s X. s ) ~P ( J ` z ) ) <-> E. s e. ~P T H e. X_ z e. ( s X. s ) ~P ( J ` z ) ) )
27 22 26 bitrd 
 |-  ( ph -> ( H C_cat J <-> E. s e. ~P T H e. X_ z e. ( s X. s ) ~P ( J ` z ) ) )
28 df-rex 
 |-  ( E. s e. ~P T H e. X_ z e. ( s X. s ) ~P ( J ` z ) <-> E. s ( s e. ~P T /\ H e. X_ z e. ( s X. s ) ~P ( J ` z ) ) )
29 3anass 
 |-  ( ( H e. _V /\ H Fn ( s X. s ) /\ A. z e. ( s X. s ) ( H ` z ) e. ~P ( J ` z ) ) <-> ( H e. _V /\ ( H Fn ( s X. s ) /\ A. z e. ( s X. s ) ( H ` z ) e. ~P ( J ` z ) ) ) )
30 elixp2 
 |-  ( H e. X_ z e. ( s X. s ) ~P ( J ` z ) <-> ( H e. _V /\ H Fn ( s X. s ) /\ A. z e. ( s X. s ) ( H ` z ) e. ~P ( J ` z ) ) )
31 vex 
 |-  s e. _V
32 31 31 xpex 
 |-  ( s X. s ) e. _V
33 fnex 
 |-  ( ( H Fn ( s X. s ) /\ ( s X. s ) e. _V ) -> H e. _V )
34 32 33 mpan2 
 |-  ( H Fn ( s X. s ) -> H e. _V )
35 34 adantr 
 |-  ( ( H Fn ( s X. s ) /\ A. z e. ( s X. s ) ( H ` z ) e. ~P ( J ` z ) ) -> H e. _V )
36 35 pm4.71ri 
 |-  ( ( H Fn ( s X. s ) /\ A. z e. ( s X. s ) ( H ` z ) e. ~P ( J ` z ) ) <-> ( H e. _V /\ ( H Fn ( s X. s ) /\ A. z e. ( s X. s ) ( H ` z ) e. ~P ( J ` z ) ) ) )
37 29 30 36 3bitr4i 
 |-  ( H e. X_ z e. ( s X. s ) ~P ( J ` z ) <-> ( H Fn ( s X. s ) /\ A. z e. ( s X. s ) ( H ` z ) e. ~P ( J ` z ) ) )
38 fndm 
 |-  ( H Fn ( s X. s ) -> dom H = ( s X. s ) )
39 38 adantl 
 |-  ( ( ph /\ H Fn ( s X. s ) ) -> dom H = ( s X. s ) )
40 1 adantr 
 |-  ( ( ph /\ H Fn ( s X. s ) ) -> H Fn ( S X. S ) )
41 40 fndmd 
 |-  ( ( ph /\ H Fn ( s X. s ) ) -> dom H = ( S X. S ) )
42 39 41 eqtr3d 
 |-  ( ( ph /\ H Fn ( s X. s ) ) -> ( s X. s ) = ( S X. S ) )
43 42 dmeqd 
 |-  ( ( ph /\ H Fn ( s X. s ) ) -> dom ( s X. s ) = dom ( S X. S ) )
44 dmxpid 
 |-  dom ( s X. s ) = s
45 dmxpid 
 |-  dom ( S X. S ) = S
46 43 44 45 3eqtr3g 
 |-  ( ( ph /\ H Fn ( s X. s ) ) -> s = S )
47 46 ex 
 |-  ( ph -> ( H Fn ( s X. s ) -> s = S ) )
48 id 
 |-  ( s = S -> s = S )
49 48 sqxpeqd 
 |-  ( s = S -> ( s X. s ) = ( S X. S ) )
50 49 fneq2d 
 |-  ( s = S -> ( H Fn ( s X. s ) <-> H Fn ( S X. S ) ) )
51 1 50 syl5ibrcom 
 |-  ( ph -> ( s = S -> H Fn ( s X. s ) ) )
52 47 51 impbid 
 |-  ( ph -> ( H Fn ( s X. s ) <-> s = S ) )
53 52 anbi1d 
 |-  ( ph -> ( ( H Fn ( s X. s ) /\ A. z e. ( s X. s ) ( H ` z ) e. ~P ( J ` z ) ) <-> ( s = S /\ A. z e. ( s X. s ) ( H ` z ) e. ~P ( J ` z ) ) ) )
54 37 53 syl5bb 
 |-  ( ph -> ( H e. X_ z e. ( s X. s ) ~P ( J ` z ) <-> ( s = S /\ A. z e. ( s X. s ) ( H ` z ) e. ~P ( J ` z ) ) ) )
55 54 anbi2d 
 |-  ( ph -> ( ( s e. ~P T /\ H e. X_ z e. ( s X. s ) ~P ( J ` z ) ) <-> ( s e. ~P T /\ ( s = S /\ A. z e. ( s X. s ) ( H ` z ) e. ~P ( J ` z ) ) ) ) )
56 an12 
 |-  ( ( s e. ~P T /\ ( s = S /\ A. z e. ( s X. s ) ( H ` z ) e. ~P ( J ` z ) ) ) <-> ( s = S /\ ( s e. ~P T /\ A. z e. ( s X. s ) ( H ` z ) e. ~P ( J ` z ) ) ) )
57 55 56 bitrdi 
 |-  ( ph -> ( ( s e. ~P T /\ H e. X_ z e. ( s X. s ) ~P ( J ` z ) ) <-> ( s = S /\ ( s e. ~P T /\ A. z e. ( s X. s ) ( H ` z ) e. ~P ( J ` z ) ) ) ) )
58 57 exbidv 
 |-  ( ph -> ( E. s ( s e. ~P T /\ H e. X_ z e. ( s X. s ) ~P ( J ` z ) ) <-> E. s ( s = S /\ ( s e. ~P T /\ A. z e. ( s X. s ) ( H ` z ) e. ~P ( J ` z ) ) ) ) )
59 28 58 syl5bb 
 |-  ( ph -> ( E. s e. ~P T H e. X_ z e. ( s X. s ) ~P ( J ` z ) <-> E. s ( s = S /\ ( s e. ~P T /\ A. z e. ( s X. s ) ( H ` z ) e. ~P ( J ` z ) ) ) ) )
60 exsimpl 
 |-  ( E. s ( s = S /\ ( s e. ~P T /\ A. z e. ( s X. s ) ( H ` z ) e. ~P ( J ` z ) ) ) -> E. s s = S )
61 isset 
 |-  ( S e. _V <-> E. s s = S )
62 60 61 sylibr 
 |-  ( E. s ( s = S /\ ( s e. ~P T /\ A. z e. ( s X. s ) ( H ` z ) e. ~P ( J ` z ) ) ) -> S e. _V )
63 62 a1i 
 |-  ( ph -> ( E. s ( s = S /\ ( s e. ~P T /\ A. z e. ( s X. s ) ( H ` z ) e. ~P ( J ` z ) ) ) -> S e. _V ) )
64 ssexg 
 |-  ( ( S C_ T /\ T e. V ) -> S e. _V )
65 64 expcom 
 |-  ( T e. V -> ( S C_ T -> S e. _V ) )
66 3 65 syl 
 |-  ( ph -> ( S C_ T -> S e. _V ) )
67 66 adantrd 
 |-  ( ph -> ( ( S C_ T /\ A. x e. S A. y e. S ( x H y ) C_ ( x J y ) ) -> S e. _V ) )
68 31 elpw 
 |-  ( s e. ~P T <-> s C_ T )
69 sseq1 
 |-  ( s = S -> ( s C_ T <-> S C_ T ) )
70 68 69 syl5bb 
 |-  ( s = S -> ( s e. ~P T <-> S C_ T ) )
71 49 raleqdv 
 |-  ( s = S -> ( A. z e. ( s X. s ) ( H ` z ) e. ~P ( J ` z ) <-> A. z e. ( S X. S ) ( H ` z ) e. ~P ( J ` z ) ) )
72 fvex 
 |-  ( H ` z ) e. _V
73 72 elpw 
 |-  ( ( H ` z ) e. ~P ( J ` z ) <-> ( H ` z ) C_ ( J ` z ) )
74 fveq2 
 |-  ( z = <. x , y >. -> ( H ` z ) = ( H ` <. x , y >. ) )
75 df-ov 
 |-  ( x H y ) = ( H ` <. x , y >. )
76 74 75 eqtr4di 
 |-  ( z = <. x , y >. -> ( H ` z ) = ( x H y ) )
77 fveq2 
 |-  ( z = <. x , y >. -> ( J ` z ) = ( J ` <. x , y >. ) )
78 df-ov 
 |-  ( x J y ) = ( J ` <. x , y >. )
79 77 78 eqtr4di 
 |-  ( z = <. x , y >. -> ( J ` z ) = ( x J y ) )
80 76 79 sseq12d 
 |-  ( z = <. x , y >. -> ( ( H ` z ) C_ ( J ` z ) <-> ( x H y ) C_ ( x J y ) ) )
81 73 80 syl5bb 
 |-  ( z = <. x , y >. -> ( ( H ` z ) e. ~P ( J ` z ) <-> ( x H y ) C_ ( x J y ) ) )
82 81 ralxp 
 |-  ( A. z e. ( S X. S ) ( H ` z ) e. ~P ( J ` z ) <-> A. x e. S A. y e. S ( x H y ) C_ ( x J y ) )
83 71 82 bitrdi 
 |-  ( s = S -> ( A. z e. ( s X. s ) ( H ` z ) e. ~P ( J ` z ) <-> A. x e. S A. y e. S ( x H y ) C_ ( x J y ) ) )
84 70 83 anbi12d 
 |-  ( s = S -> ( ( s e. ~P T /\ A. z e. ( s X. s ) ( H ` z ) e. ~P ( J ` z ) ) <-> ( S C_ T /\ A. x e. S A. y e. S ( x H y ) C_ ( x J y ) ) ) )
85 84 ceqsexgv 
 |-  ( S e. _V -> ( E. s ( s = S /\ ( s e. ~P T /\ A. z e. ( s X. s ) ( H ` z ) e. ~P ( J ` z ) ) ) <-> ( S C_ T /\ A. x e. S A. y e. S ( x H y ) C_ ( x J y ) ) ) )
86 85 a1i 
 |-  ( ph -> ( S e. _V -> ( E. s ( s = S /\ ( s e. ~P T /\ A. z e. ( s X. s ) ( H ` z ) e. ~P ( J ` z ) ) ) <-> ( S C_ T /\ A. x e. S A. y e. S ( x H y ) C_ ( x J y ) ) ) ) )
87 63 67 86 pm5.21ndd 
 |-  ( ph -> ( E. s ( s = S /\ ( s e. ~P T /\ A. z e. ( s X. s ) ( H ` z ) e. ~P ( J ` z ) ) ) <-> ( S C_ T /\ A. x e. S A. y e. S ( x H y ) C_ ( x J y ) ) ) )
88 27 59 87 3bitrd 
 |-  ( ph -> ( H C_cat J <-> ( S C_ T /\ A. x e. S A. y e. S ( x H y ) C_ ( x J y ) ) ) )