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

Theorem sscpwex 14728
Description: An analogue of pwex 4475 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 6116 . 2  |-  ( ~P
U. ran  J  ^pm  dom 
J )  e.  _V
2 brssc 14727 . . . 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 2975 . . . . . . . . . . 11  |-  t  e. 
_V
54, 4xpex 6508 . . . . . . . . . 10  |-  ( t  X.  t )  e. 
_V
6 fnex 5944 . . . . . . . . . 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 6510 . . . . . . . . 9  |-  ( J  e.  _V  ->  ran  J  e.  _V )
9 uniexg 6377 . . . . . . . . 9  |-  ( ran 
J  e.  _V  ->  U.
ran  J  e.  _V )
10 pwexg 4476 . . . . . . . . 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 5510 . . . . . . . . . 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 2531 . . . . . . . 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 7276 . . . . . . . . . . 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 5713 . . . . . . . . . . . . 13  |-  ( J `
 x )  C_  U.
ran  J
17 sspwb 4541 . . . . . . . . . . . . 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 2785 . . . . . . . . . 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 3354 . . . . . . . . 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 2975 . . . . . . . . . 10  |-  h  e. 
_V
2423elixpconst 7271 . . . . . . . . 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 3869 . . . . . . . . . . 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 4945 . . . . . . . . . 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 3393 . . . . . . . 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 7230 . . . . . . . 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 1219 . . . . . . 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 2842 . . . . . 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 1688 . . . 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 3427 . 2  |-  { h  |  h  C_cat  J }  C_  ( ~P U. ran  J 
^pm  dom  J )
381, 37ssexi 4437 1  |-  { h  |  h  C_cat  J }  e.  _V
Colors of variables: wff setvar class
Syntax hints:    /\ wa 369    = wceq 1369   E.wex 1586    e. wcel 1756   {cab 2429   E.wrex 2716   _Vcvv 2972    C_ wss 3328   ~Pcpw 3860   U.cuni 4091   class class class wbr 4292    X. cxp 4838   dom cdm 4840   ran crn 4841    Fn wfn 5413   -->wf 5414   ` cfv 5418  (class class class)co 6091    ^pm cpm 7215   X_cixp 7263    C_cat cssc 14720
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-rep 4403  ax-sep 4413  ax-nul 4421  ax-pow 4470  ax-pr 4531  ax-un 6372
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-ral 2720  df-rex 2721  df-reu 2722  df-rab 2724  df-v 2974  df-sbc 3187  df-csb 3289  df-dif 3331  df-un 3333  df-in 3335  df-ss 3342  df-nul 3638  df-if 3792  df-pw 3862  df-sn 3878  df-pr 3880  df-op 3884  df-uni 4092  df-iun 4173  df-br 4293  df-opab 4351  df-mpt 4352  df-id 4636  df-xp 4846  df-rel 4847  df-cnv 4848  df-co 4849  df-dm 4850  df-rn 4851  df-res 4852  df-ima 4853  df-iota 5381  df-fun 5420  df-fn 5421  df-f 5422  df-f1 5423  df-fo 5424  df-f1o 5425  df-fv 5426  df-ov 6094  df-oprab 6095  df-mpt2 6096  df-pm 7217  df-ixp 7264  df-ssc 14723
This theorem is referenced by:  issubc  14748
  Copyright terms: Public domain W3C validator