Metamath Proof Explorer

Theorem sscpwex

Description: An analogue of pwex 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)

Ref Expression
Assertion sscpwex 
|- { h | h C_cat J } e. _V

Proof

Step Hyp Ref Expression
1 ovex 
 |-  ( ~P U. ran J ^pm dom J ) e. _V
2 brssc 
 |-  ( 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 
 |-  ( ( 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 
 |-  t e. _V
5 4 4 xpex 
 |-  ( t X. t ) e. _V
6 fnex 
 |-  ( ( J Fn ( t X. t ) /\ ( t X. t ) e. _V ) -> J e. _V )
7 3 5 6 sylancl 
 |-  ( ( 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 
 |-  ( J e. _V -> ran J e. _V )
9 uniexg 
 |-  ( ran J e. _V -> U. ran J e. _V )
10 pwexg 
 |-  ( U. ran J e. _V -> ~P U. ran J e. _V )
11 7 8 9 10 4syl 
 |-  ( ( 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 
 |-  ( J Fn ( t X. t ) -> dom J = ( t X. t ) )
13 12 adantr 
 |-  ( ( 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 ) )
14 13 5 eqeltrdi 
 |-  ( ( 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 
 |-  ( 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 
 |-  ( J ` x ) C_ U. ran J
17 16 sspwi 
 |-  ~P ( J ` x ) C_ ~P U. ran J
18 17 a1i 
 |-  ( x e. ( s X. s ) -> ~P ( J ` x ) C_ ~P U. ran J )
19 15 18 mprg 
 |-  X_ x e. ( s X. s ) ~P ( J ` x ) C_ X_ x e. ( s X. s ) ~P U. ran J
20 simprr 
 |-  ( ( 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 ) )
21 19 20 sselid 
 |-  ( ( 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 )
22 vex 
 |-  h e. _V
23 22 elixpconst 
 |-  ( h e. X_ x e. ( s X. s ) ~P U. ran J <-> h : ( s X. s ) --> ~P U. ran J )
24 21 23 sylib 
 |-  ( ( 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 )
25 elpwi 
 |-  ( s e. ~P t -> s C_ t )
26 25 ad2antrl 
 |-  ( ( J Fn ( t X. t ) /\ ( s e. ~P t /\ h e. X_ x e. ( s X. s ) ~P ( J ` x ) ) ) -> s C_ t )
27 xpss12 
 |-  ( ( s C_ t /\ s C_ t ) -> ( s X. s ) C_ ( t X. t ) )
28 26 26 27 syl2anc 
 |-  ( ( 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 ) )
29 28 13 sseqtrrd 
 |-  ( ( 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 )
30 elpm2r 
 |-  ( ( ( ~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 ) )
31 11 14 24 29 30 syl22anc 
 |-  ( ( 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 ) )
32 31 rexlimdvaa 
 |-  ( 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 ) ) )
33 32 imp 
 |-  ( ( 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 ) )
34 33 exlimiv 
 |-  ( 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 ) )
35 2 34 sylbi 
 |-  ( h C_cat J -> h e. ( ~P U. ran J ^pm dom J ) )
36 35 abssi 
 |-  { h | h C_cat J } C_ ( ~P U. ran J ^pm dom J )
37 1 36 ssexi 
 |-  { h | h C_cat J } e. _V