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

Theorem sscpwex 15045
Description: An analogue of pwex 4630 for the subcategory subset relation: The collection of subcategory subsets of a given set  J is a set. (Contributed by Mario Carneiro, 6-Jan-2017.)
Assertion
Ref Expression
sscpwex  |-  { h  |  h  C_cat  J }  e.  _V
Distinct variable group:    h, J

Proof of Theorem sscpwex
Dummy variables  s 
t  x are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ovex 6309 . 2  |-  ( ~P
U. ran  J  ^pm  dom 
J )  e.  _V
2 brssc 15044 . . . 4  |-  ( 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 ) ) )
3 simpl 457 . . . . . . . . . 10  |-  ( ( J  Fn  ( t  X.  t )  /\  ( s  e.  ~P t  /\  h  e.  X_ x  e.  ( s  X.  s ) ~P ( J `  x )
) )  ->  J  Fn  ( t  X.  t
) )
4 vex 3116 . . . . . . . . . . 11  |-  t  e. 
_V
54, 4xpex 6588 . . . . . . . . . 10  |-  ( t  X.  t )  e. 
_V
6 fnex 6127 . . . . . . . . . 10  |-  ( ( J  Fn  ( t  X.  t )  /\  ( t  X.  t
)  e.  _V )  ->  J  e.  _V )
73, 5, 6sylancl 662 . . . . . . . . 9  |-  ( ( J  Fn  ( t  X.  t )  /\  ( s  e.  ~P t  /\  h  e.  X_ x  e.  ( s  X.  s ) ~P ( J `  x )
) )  ->  J  e.  _V )
8 rnexg 6716 . . . . . . . . 9  |-  ( J  e.  _V  ->  ran  J  e.  _V )
9 uniexg 6581 . . . . . . . . 9  |-  ( ran 
J  e.  _V  ->  U.
ran  J  e.  _V )
10 pwexg 4631 . . . . . . . . 9  |-  ( U. ran  J  e.  _V  ->  ~P
U. ran  J  e.  _V )
117, 8, 9, 104syl 21 . . . . . . . 8  |-  ( ( J  Fn  ( t  X.  t )  /\  ( s  e.  ~P t  /\  h  e.  X_ x  e.  ( s  X.  s ) ~P ( J `  x )
) )  ->  ~P U.
ran  J  e.  _V )
12 fndm 5680 . . . . . . . . . 10  |-  ( J  Fn  ( t  X.  t )  ->  dom  J  =  ( t  X.  t ) )
1312adantr 465 . . . . . . . . 9  |-  ( ( J  Fn  ( t  X.  t )  /\  ( s  e.  ~P t  /\  h  e.  X_ x  e.  ( s  X.  s ) ~P ( J `  x )
) )  ->  dom  J  =  ( t  X.  t ) )
1413, 5syl6eqel 2563 . . . . . . . 8  |-  ( ( J  Fn  ( t  X.  t )  /\  ( s  e.  ~P t  /\  h  e.  X_ x  e.  ( s  X.  s ) ~P ( J `  x )
) )  ->  dom  J  e.  _V )
15 ss2ixp 7482 . . . . . . . . . . 11  |-  ( A. x  e.  ( s  X.  s ) ~P ( J `  x )  C_ 
~P U. ran  J  ->  X_ x  e.  ( s  X.  s ) ~P ( J `  x
)  C_  X_ x  e.  ( s  X.  s
) ~P U. ran  J )
16 fvssunirn 5889 . . . . . . . . . . . . 13  |-  ( J `
 x )  C_  U.
ran  J
17 sspwb 4696 . . . . . . . . . . . . 13  |-  ( ( J `  x ) 
C_  U. ran  J  <->  ~P ( J `  x )  C_ 
~P U. ran  J )
1816, 17mpbi 208 . . . . . . . . . . . 12  |-  ~P ( J `  x )  C_ 
~P U. ran  J
1918a1i 11 . . . . . . . . . . 11  |-  ( x  e.  ( s  X.  s )  ->  ~P ( J `  x ) 
C_  ~P U. ran  J
)
2015, 19mprg 2827 . . . . . . . . . 10  |-  X_ x  e.  ( s  X.  s
) ~P ( J `
 x )  C_  X_ x  e.  ( s  X.  s ) ~P
U. ran  J
21 simprr 756 . . . . . . . . . 10  |-  ( ( J  Fn  ( t  X.  t )  /\  ( s  e.  ~P t  /\  h  e.  X_ x  e.  ( s  X.  s ) ~P ( J `  x )
) )  ->  h  e.  X_ x  e.  ( s  X.  s ) ~P ( J `  x ) )
2220, 21sseldi 3502 . . . . . . . . 9  |-  ( ( J  Fn  ( t  X.  t )  /\  ( s  e.  ~P t  /\  h  e.  X_ x  e.  ( s  X.  s ) ~P ( J `  x )
) )  ->  h  e.  X_ x  e.  ( s  X.  s ) ~P U. ran  J
)
23 vex 3116 . . . . . . . . . 10  |-  h  e. 
_V
2423elixpconst 7477 . . . . . . . . 9  |-  ( h  e.  X_ x  e.  ( s  X.  s ) ~P U. ran  J  <->  h : ( s  X.  s ) --> ~P U. ran  J )
2522, 24sylib 196 . . . . . . . 8  |-  ( ( J  Fn  ( t  X.  t )  /\  ( s  e.  ~P t  /\  h  e.  X_ x  e.  ( s  X.  s ) ~P ( J `  x )
) )  ->  h : ( s  X.  s ) --> ~P U. ran  J )
26 elpwi 4019 . . . . . . . . . . 11  |-  ( s  e.  ~P t  -> 
s  C_  t )
2726ad2antrl 727 . . . . . . . . . 10  |-  ( ( J  Fn  ( t  X.  t )  /\  ( s  e.  ~P t  /\  h  e.  X_ x  e.  ( s  X.  s ) ~P ( J `  x )
) )  ->  s  C_  t )
28 xpss12 5108 . . . . . . . . . 10  |-  ( ( s  C_  t  /\  s  C_  t )  -> 
( s  X.  s
)  C_  ( t  X.  t ) )
2927, 27, 28syl2anc 661 . . . . . . . . 9  |-  ( ( J  Fn  ( t  X.  t )  /\  ( s  e.  ~P t  /\  h  e.  X_ x  e.  ( s  X.  s ) ~P ( J `  x )
) )  ->  (
s  X.  s ) 
C_  ( t  X.  t ) )
3029, 13sseqtr4d 3541 . . . . . . . 8  |-  ( ( J  Fn  ( t  X.  t )  /\  ( s  e.  ~P t  /\  h  e.  X_ x  e.  ( s  X.  s ) ~P ( J `  x )
) )  ->  (
s  X.  s ) 
C_  dom  J )
31 elpm2r 7436 . . . . . . . 8  |-  ( ( ( ~P U. ran  J  e.  _V  /\  dom  J  e.  _V )  /\  ( h : ( s  X.  s ) --> ~P U. ran  J  /\  ( s  X.  s
)  C_  dom  J ) )  ->  h  e.  ( ~P U. ran  J  ^pm  dom  J ) )
3211, 14, 25, 30, 31syl22anc 1229 . . . . . . 7  |-  ( ( J  Fn  ( t  X.  t )  /\  ( s  e.  ~P t  /\  h  e.  X_ x  e.  ( s  X.  s ) ~P ( J `  x )
) )  ->  h  e.  ( ~P U. ran  J 
^pm  dom  J ) )
3332rexlimdvaa 2956 . . . . . 6  |-  ( J  Fn  ( t  X.  t )  ->  ( E. s  e.  ~P  t h  e.  X_ x  e.  ( s  X.  s
) ~P ( J `
 x )  ->  h  e.  ( ~P U.
ran  J  ^pm  dom  J
) ) )
3433imp 429 . . . . 5  |-  ( ( J  Fn  ( t  X.  t )  /\  E. s  e.  ~P  t
h  e.  X_ x  e.  ( s  X.  s
) ~P ( J `
 x ) )  ->  h  e.  ( ~P U. ran  J  ^pm  dom  J ) )
3534exlimiv 1698 . . . 4  |-  ( E. t ( J  Fn  ( t  X.  t
)  /\  E. s  e.  ~P  t h  e.  X_ x  e.  (
s  X.  s ) ~P ( J `  x ) )  ->  h  e.  ( ~P U.
ran  J  ^pm  dom  J
) )
362, 35sylbi 195 . . 3  |-  ( h 
C_cat  J  ->  h  e.  ( ~P U. ran  J  ^pm  dom  J ) )
3736abssi 3575 . 2  |-  { h  |  h  C_cat  J }  C_  ( ~P U. ran  J 
^pm  dom  J )
381, 37ssexi 4592 1  |-  { h  |  h  C_cat  J }  e.  _V
Colors of variables: wff setvar class
Syntax hints:    /\ wa 369    = wceq 1379   E.wex 1596    e. wcel 1767   {cab 2452   E.wrex 2815   _Vcvv 3113    C_ wss 3476   ~Pcpw 4010   U.cuni 4245   class class class wbr 4447    X. cxp 4997   dom cdm 4999   ran crn 5000    Fn wfn 5583   -->wf 5584   ` cfv 5588  (class class class)co 6284    ^pm cpm 7421   X_cixp 7469    C_cat cssc 15037
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-rep 4558  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6576
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-reu 2821  df-rab 2823  df-v 3115  df-sbc 3332  df-csb 3436  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-op 4034  df-uni 4246  df-iun 4327  df-br 4448  df-opab 4506  df-mpt 4507  df-id 4795  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5551  df-fun 5590  df-fn 5591  df-f 5592  df-f1 5593  df-fo 5594  df-f1o 5595  df-fv 5596  df-ov 6287  df-oprab 6288  df-mpt2 6289  df-pm 7423  df-ixp 7470  df-ssc 15040
This theorem is referenced by:  issubc  15065
  Copyright terms: Public domain W3C validator