Theorem sscpwex 14724

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

Step	Hyp	Ref	Expression
1		ovex 6115	. 2 |- ( ~P U. ran J ^pm dom J ) e. _V
2		brssc 14723	. . . 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 454	. . . . . . . . . 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 2973	. . . . . . . . . . 11 |- t e. _V
5	4, 4	xpex 6507	. . . . . . . . . 10 |- ( t X. t ) e. _V
6		fnex 5941	. . . . . . . . . 10 |- ( ( J Fn ( t X. t ) /\ ( t X. t ) e. _V ) -> J e. _V )
7	3, 5, 6	sylancl 657	. . . . . . . . 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 6509	. . . . . . . . 9 |- ( J e. _V -> ran J e. _V )
9		uniexg 6376	. . . . . . . . 9 |- ( ran J e. _V -> U. ran J e. _V )
10		pwexg 4473	. . . . . . . . 9 |- ( U. ran J e. _V -> ~P U. ran J e. _V )
11	7, 8, 9, 10	4syl 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 5507	. . . . . . . . . 10 |- ( J Fn ( t X. t ) -> dom J = ( t X. t ) )
13	12	adantr 462	. . . . . . . . 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 ) )
14	13, 5	syl6eqel 2529	. . . . . . . 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 7272	. . . . . . . . . . 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 5710	. . . . . . . . . . . . 13 |- ( J ` x ) C_ U. ran J
17		sspwb 4538	. . . . . . . . . . . . 13 |- ( ( J ` x ) C_ U. ran J <-> ~P ( J ` x ) C_ ~P U. ran J )
18	16, 17	mpbi 208	. . . . . . . . . . . 12 |- ~P ( J ` x ) C_ ~P U. ran J
19	18	a1i 11	. . . . . . . . . . 11 |- ( x e. ( s X. s ) -> ~P ( J ` x ) C_ ~P U. ran J )
20	15, 19	mprg 2783	. . . . . . . . . 10 |- X_ x e. ( s X. s ) ~P ( J ` x ) C_ X_ x e. ( s X. s ) ~P U. ran J
21		simprr 751	. . . . . . . . . 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 ) )
22	20, 21	sseldi 3351	. . . . . . . . 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 2973	. . . . . . . . . 10 |- h e. _V
24	23	elixpconst 7267	. . . . . . . . 9 |- ( h e. X_ x e. ( s X. s ) ~P U. ran J <-> h : ( s X. s ) --> ~P U. ran J )
25	22, 24	sylib 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 3866	. . . . . . . . . . 11 |- ( s e. ~P t -> s C_ t )
27	26	ad2antrl 722	. . . . . . . . . 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 4941	. . . . . . . . . 10 |- ( ( s C_ t /\ s C_ t ) -> ( s X. s ) C_ ( t X. t ) )
29	27, 27, 28	syl2anc 656	. . . . . . . . 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 ) )
30	29, 13	sseqtr4d 3390	. . . . . . . 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 7226	. . . . . . . 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 ) )
32	11, 14, 25, 30, 31	syl22anc 1214	. . . . . . 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 ) )
33	32	rexlimdvaa 2840	. . . . . 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 ) ) )
34	33	imp 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 ) )
35	34	exlimiv 1693	. . . 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 ) )
36	2, 35	sylbi 195	. . 3 |- ( h C_cat J -> h e. ( ~P U. ran J ^pm dom J ) )
37	36	abssi 3424	. 2 |- { h | h C_cat J } C_ ( ~P U. ran J ^pm dom J )
38	1, 37	ssexi 4434	1 |- { h | h C_cat J } e. _V

Syntax hints:   /\ wa 369   = wceq 1364   E.wex 1591   e. wcel 1761   {cab 2427   E.wrex 2714   _Vcvv 2970   C_ wss 3325   ~Pcpw 3857   U.cuni 4088   class class class wbr 4289   X. cxp 4834   dom cdm 4836   ran crn 4837   Fn wfn 5410   -->wf 5411   ` cfv 5415  (class class class)co 6090   ^pm cpm 7211   X_cixp 7259   C__cat cssc 14716

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-8 1763  ax-9 1765  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422  ax-rep 4400  ax-sep 4410  ax-nul 4418  ax-pow 4467  ax-pr 4528  ax-un 6371

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-eu 2263  df-mo 2264  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-ral 2718  df-rex 2719  df-reu 2720  df-rab 2722  df-v 2972  df-sbc 3184  df-csb 3286  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-nul 3635  df-if 3789  df-pw 3859  df-sn 3875  df-pr 3877  df-op 3881  df-uni 4089  df-iun 4170  df-br 4290  df-opab 4348  df-mpt 4349  df-id 4632  df-xp 4842  df-rel 4843  df-cnv 4844  df-co 4845  df-dm 4846  df-rn 4847  df-res 4848  df-ima 4849  df-iota 5378  df-fun 5417  df-fn 5418  df-f 5419  df-f1 5420  df-fo 5421  df-f1o 5422  df-fv 5423  df-ov 6093  df-oprab 6094  df-mpt2 6095  df-pm 7213  df-ixp 7260  df-ssc 14719

This theorem is referenced by:  issubc  14744