MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  isssc Structured version   Unicode version

Theorem isssc 15668
Description: Value of the subcategory subset relation when the arguments are known functions. (Contributed by Mario Carneiro, 6-Jan-2017.)
Hypotheses
Ref Expression
isssc.1  |-  ( ph  ->  H  Fn  ( S  X.  S ) )
isssc.2  |-  ( ph  ->  J  Fn  ( T  X.  T ) )
isssc.3  |-  ( ph  ->  T  e.  V )
Assertion
Ref Expression
isssc  |-  ( ph  ->  ( H  C_cat  J  <->  ( S  C_  T  /\  A. x  e.  S  A. y  e.  S  ( x H y )  C_  ( x J y ) ) ) )
Distinct variable groups:    x, y, H    x, J, y    x, S, y
Allowed substitution hints:    ph( x, y)    T( x, y)    V( x, y)

Proof of Theorem isssc
Dummy variables  t 
s  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 brssc 15662 . . . 4  |-  ( 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 ) ) )
2 fndm 5636 . . . . . . . . . . . 12  |-  ( J  Fn  ( t  X.  t )  ->  dom  J  =  ( t  X.  t ) )
32adantl 467 . . . . . . . . . . 11  |-  ( (
ph  /\  J  Fn  ( t  X.  t
) )  ->  dom  J  =  ( t  X.  t ) )
4 isssc.2 . . . . . . . . . . . . 13  |-  ( ph  ->  J  Fn  ( T  X.  T ) )
54adantr 466 . . . . . . . . . . . 12  |-  ( (
ph  /\  J  Fn  ( t  X.  t
) )  ->  J  Fn  ( T  X.  T
) )
6 fndm 5636 . . . . . . . . . . . 12  |-  ( J  Fn  ( T  X.  T )  ->  dom  J  =  ( T  X.  T ) )
75, 6syl 17 . . . . . . . . . . 11  |-  ( (
ph  /\  J  Fn  ( t  X.  t
) )  ->  dom  J  =  ( T  X.  T ) )
83, 7eqtr3d 2464 . . . . . . . . . 10  |-  ( (
ph  /\  J  Fn  ( t  X.  t
) )  ->  (
t  X.  t )  =  ( T  X.  T ) )
98dmeqd 4999 . . . . . . . . 9  |-  ( (
ph  /\  J  Fn  ( t  X.  t
) )  ->  dom  ( t  X.  t
)  =  dom  ( T  X.  T ) )
10 dmxpid 5016 . . . . . . . . 9  |-  dom  (
t  X.  t )  =  t
11 dmxpid 5016 . . . . . . . . 9  |-  dom  ( T  X.  T )  =  T
129, 10, 113eqtr3g 2485 . . . . . . . 8  |-  ( (
ph  /\  J  Fn  ( t  X.  t
) )  ->  t  =  T )
1312ex 435 . . . . . . 7  |-  ( ph  ->  ( J  Fn  (
t  X.  t )  ->  t  =  T ) )
14 id 22 . . . . . . . . . 10  |-  ( t  =  T  ->  t  =  T )
1514sqxpeqd 4822 . . . . . . . . 9  |-  ( t  =  T  ->  (
t  X.  t )  =  ( T  X.  T ) )
1615fneq2d 5628 . . . . . . . 8  |-  ( t  =  T  ->  ( J  Fn  ( t  X.  t )  <->  J  Fn  ( T  X.  T
) ) )
174, 16syl5ibrcom 225 . . . . . . 7  |-  ( ph  ->  ( t  =  T  ->  J  Fn  (
t  X.  t ) ) )
1813, 17impbid 193 . . . . . 6  |-  ( ph  ->  ( J  Fn  (
t  X.  t )  <-> 
t  =  T ) )
1918anbi1d 709 . . . . 5  |-  ( 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 ) ) ) )
2019exbidv 1762 . . . 4  |-  ( 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 ) ) ) )
211, 20syl5bb 260 . . 3  |-  ( 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 ) ) ) )
22 isssc.3 . . . 4  |-  ( ph  ->  T  e.  V )
23 pweq 3927 . . . . . 6  |-  ( t  =  T  ->  ~P t  =  ~P T
)
2423rexeqdv 2971 . . . . 5  |-  ( 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 ) ) )
2524ceqsexgv 3146 . . . 4  |-  ( 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 ) ) )
2622, 25syl 17 . . 3  |-  ( 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 ) ) )
2721, 26bitrd 256 . 2  |-  ( ph  ->  ( H  C_cat  J  <->  E. s  e.  ~P  T H  e.  X_ z  e.  (
s  X.  s ) ~P ( J `  z ) ) )
28 df-rex 2720 . . 3  |-  ( 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 986 . . . . . . . 8  |-  ( ( 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 7481 . . . . . . . 8  |-  ( 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 3025 . . . . . . . . . . . 12  |-  s  e. 
_V
3231, 31xpex 6553 . . . . . . . . . . 11  |-  ( s  X.  s )  e. 
_V
33 fnex 6091 . . . . . . . . . . 11  |-  ( ( H  Fn  ( s  X.  s )  /\  ( s  X.  s
)  e.  _V )  ->  H  e.  _V )
3432, 33mpan2 675 . . . . . . . . . 10  |-  ( H  Fn  ( s  X.  s )  ->  H  e.  _V )
3534adantr 466 . . . . . . . . 9  |-  ( ( H  Fn  ( s  X.  s )  /\  A. z  e.  ( s  X.  s ) ( H `  z )  e.  ~P ( J `
 z ) )  ->  H  e.  _V )
3635pm4.71ri 637 . . . . . . . 8  |-  ( ( 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 ) ) ) )
3729, 30, 363bitr4i 280 . . . . . . 7  |-  ( 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 5636 . . . . . . . . . . . . . 14  |-  ( H  Fn  ( s  X.  s )  ->  dom  H  =  ( s  X.  s ) )
3938adantl 467 . . . . . . . . . . . . 13  |-  ( (
ph  /\  H  Fn  ( s  X.  s
) )  ->  dom  H  =  ( s  X.  s ) )
40 isssc.1 . . . . . . . . . . . . . . 15  |-  ( ph  ->  H  Fn  ( S  X.  S ) )
4140adantr 466 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  H  Fn  ( s  X.  s
) )  ->  H  Fn  ( S  X.  S
) )
42 fndm 5636 . . . . . . . . . . . . . 14  |-  ( H  Fn  ( S  X.  S )  ->  dom  H  =  ( S  X.  S ) )
4341, 42syl 17 . . . . . . . . . . . . 13  |-  ( (
ph  /\  H  Fn  ( s  X.  s
) )  ->  dom  H  =  ( S  X.  S ) )
4439, 43eqtr3d 2464 . . . . . . . . . . . 12  |-  ( (
ph  /\  H  Fn  ( s  X.  s
) )  ->  (
s  X.  s )  =  ( S  X.  S ) )
4544dmeqd 4999 . . . . . . . . . . 11  |-  ( (
ph  /\  H  Fn  ( s  X.  s
) )  ->  dom  ( s  X.  s
)  =  dom  ( S  X.  S ) )
46 dmxpid 5016 . . . . . . . . . . 11  |-  dom  (
s  X.  s )  =  s
47 dmxpid 5016 . . . . . . . . . . 11  |-  dom  ( S  X.  S )  =  S
4845, 46, 473eqtr3g 2485 . . . . . . . . . 10  |-  ( (
ph  /\  H  Fn  ( s  X.  s
) )  ->  s  =  S )
4948ex 435 . . . . . . . . 9  |-  ( ph  ->  ( H  Fn  (
s  X.  s )  ->  s  =  S ) )
50 id 22 . . . . . . . . . . . 12  |-  ( s  =  S  ->  s  =  S )
5150sqxpeqd 4822 . . . . . . . . . . 11  |-  ( s  =  S  ->  (
s  X.  s )  =  ( S  X.  S ) )
5251fneq2d 5628 . . . . . . . . . 10  |-  ( s  =  S  ->  ( H  Fn  ( s  X.  s )  <->  H  Fn  ( S  X.  S
) ) )
5340, 52syl5ibrcom 225 . . . . . . . . 9  |-  ( ph  ->  ( s  =  S  ->  H  Fn  (
s  X.  s ) ) )
5449, 53impbid 193 . . . . . . . 8  |-  ( ph  ->  ( H  Fn  (
s  X.  s )  <-> 
s  =  S ) )
5554anbi1d 709 . . . . . . 7  |-  ( 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 ) ) ) )
5637, 55syl5bb 260 . . . . . 6  |-  ( 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 ) ) ) )
5756anbi2d 708 . . . . 5  |-  ( 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 ) ) ) ) )
58 an12 804 . . . . 5  |-  ( ( 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 )
) ) )
5957, 58syl6bb 264 . . . 4  |-  ( 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 )
) ) ) )
6059exbidv 1762 . . 3  |-  ( 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 ) ) ) ) )
6128, 60syl5bb 260 . 2  |-  ( 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 ) ) ) ) )
62 exsimpl 1723 . . . . 5  |-  ( E. s ( s  =  S  /\  ( s  e.  ~P T  /\  A. z  e.  ( s  X.  s ) ( H `  z )  e.  ~P ( J `
 z ) ) )  ->  E. s 
s  =  S )
63 isset 3026 . . . . 5  |-  ( S  e.  _V  <->  E. s 
s  =  S )
6462, 63sylibr 215 . . . 4  |-  ( E. s ( s  =  S  /\  ( s  e.  ~P T  /\  A. z  e.  ( s  X.  s ) ( H `  z )  e.  ~P ( J `
 z ) ) )  ->  S  e.  _V )
6564a1i 11 . . 3  |-  ( ph  ->  ( E. s ( s  =  S  /\  ( s  e.  ~P T  /\  A. z  e.  ( s  X.  s
) ( H `  z )  e.  ~P ( J `  z ) ) )  ->  S  e.  _V ) )
66 ssexg 4513 . . . . . 6  |-  ( ( S  C_  T  /\  T  e.  V )  ->  S  e.  _V )
6766expcom 436 . . . . 5  |-  ( T  e.  V  ->  ( S  C_  T  ->  S  e.  _V ) )
6822, 67syl 17 . . . 4  |-  ( ph  ->  ( S  C_  T  ->  S  e.  _V )
)
6968adantrd 469 . . 3  |-  ( ph  ->  ( ( S  C_  T  /\  A. x  e.  S  A. y  e.  S  ( x H y )  C_  (
x J y ) )  ->  S  e.  _V ) )
7031elpw 3930 . . . . . . 7  |-  ( s  e.  ~P T  <->  s  C_  T )
71 sseq1 3428 . . . . . . 7  |-  ( s  =  S  ->  (
s  C_  T  <->  S  C_  T
) )
7270, 71syl5bb 260 . . . . . 6  |-  ( s  =  S  ->  (
s  e.  ~P T  <->  S 
C_  T ) )
7351raleqdv 2970 . . . . . . 7  |-  ( 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 ) ) )
74 fvex 5835 . . . . . . . . . 10  |-  ( H `
 z )  e. 
_V
7574elpw 3930 . . . . . . . . 9  |-  ( ( H `  z )  e.  ~P ( J `
 z )  <->  ( H `  z )  C_  ( J `  z )
)
76 fveq2 5825 . . . . . . . . . . 11  |-  ( z  =  <. x ,  y
>.  ->  ( H `  z )  =  ( H `  <. x ,  y >. )
)
77 df-ov 6252 . . . . . . . . . . 11  |-  ( x H y )  =  ( H `  <. x ,  y >. )
7876, 77syl6eqr 2480 . . . . . . . . . 10  |-  ( z  =  <. x ,  y
>.  ->  ( H `  z )  =  ( x H y ) )
79 fveq2 5825 . . . . . . . . . . 11  |-  ( z  =  <. x ,  y
>.  ->  ( J `  z )  =  ( J `  <. x ,  y >. )
)
80 df-ov 6252 . . . . . . . . . . 11  |-  ( x J y )  =  ( J `  <. x ,  y >. )
8179, 80syl6eqr 2480 . . . . . . . . . 10  |-  ( z  =  <. x ,  y
>.  ->  ( J `  z )  =  ( x J y ) )
8278, 81sseq12d 3436 . . . . . . . . 9  |-  ( z  =  <. x ,  y
>.  ->  ( ( H `
 z )  C_  ( J `  z )  <-> 
( x H y )  C_  ( x J y ) ) )
8375, 82syl5bb 260 . . . . . . . 8  |-  ( z  =  <. x ,  y
>.  ->  ( ( H `
 z )  e. 
~P ( J `  z )  <->  ( x H y )  C_  ( x J y ) ) )
8483ralxp 4938 . . . . . . 7  |-  ( 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 ) )
8573, 84syl6bb 264 . . . . . 6  |-  ( 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 ) ) )
8672, 85anbi12d 715 . . . . 5  |-  ( 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 ) ) ) )
8786ceqsexgv 3146 . . . 4  |-  ( 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 ) ) ) )
8887a1i 11 . . 3  |-  ( 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 ) ) ) ) )
8965, 69, 88pm5.21ndd 355 . 2  |-  ( 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 ) ) ) )
9027, 61, 893bitrd 282 1  |-  ( ph  ->  ( H  C_cat  J  <->  ( S  C_  T  /\  A. x  e.  S  A. y  e.  S  ( x H y )  C_  ( x J y ) ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    /\ wa 370    /\ w3a 982    = wceq 1437   E.wex 1657    e. wcel 1872   A.wral 2714   E.wrex 2715   _Vcvv 3022    C_ wss 3379   ~Pcpw 3924   <.cop 3947   class class class wbr 4366    X. cxp 4794   dom cdm 4796    Fn wfn 5539   ` cfv 5544  (class class class)co 6249   X_cixp 7477    C_cat cssc 15655
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408  ax-rep 4479  ax-sep 4489  ax-nul 4498  ax-pow 4545  ax-pr 4603  ax-un 6541
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2280  df-mo 2281  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-ne 2601  df-ral 2719  df-rex 2720  df-reu 2721  df-rab 2723  df-v 3024  df-sbc 3243  df-csb 3339  df-dif 3382  df-un 3384  df-in 3386  df-ss 3393  df-nul 3705  df-if 3855  df-pw 3926  df-sn 3942  df-pr 3944  df-op 3948  df-uni 4163  df-iun 4244  df-br 4367  df-opab 4426  df-mpt 4427  df-id 4711  df-xp 4802  df-rel 4803  df-cnv 4804  df-co 4805  df-dm 4806  df-rn 4807  df-res 4808  df-ima 4809  df-iota 5508  df-fun 5546  df-fn 5547  df-f 5548  df-f1 5549  df-fo 5550  df-f1o 5551  df-fv 5552  df-ov 6252  df-ixp 7478  df-ssc 15658
This theorem is referenced by:  ssc1  15669  ssc2  15670  sscres  15671  ssctr  15673  0ssc  15685  catsubcat  15687  rnghmsscmap2  39566  rnghmsscmap  39567  rhmsscmap2  39612  rhmsscmap  39613  rhmsscrnghm  39619  srhmsubc  39669  fldhmsubc  39677  srhmsubcALTV  39688  fldhmsubcALTV  39696
  Copyright terms: Public domain W3C validator