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 ) ) ) )