Theorem wunfunc

Description: A weak universe is closed under the functor set operation. (Contributed by Mario Carneiro, 12-Jan-2017)

	Ref	Expression
Hypotheses	wunfunc.1	|- ( ph -> U e. WUni )
	wunfunc.2	|- ( ph -> C e. U )
	wunfunc.3	|- ( ph -> D e. U )
Assertion	wunfunc	|- ( ph -> ( C Func D ) e. U )

Proof

Step	Hyp	Ref	Expression
1		wunfunc.1	|- ( ph -> U e. WUni )
2		wunfunc.2	|- ( ph -> C e. U )
3		wunfunc.3	|- ( ph -> D e. U )
4		df-base	|- Base = Slot 1
5	4 1 3	wunstr	|- ( ph -> ( Base ` D ) e. U )
6	4 1 2	wunstr	|- ( ph -> ( Base ` C ) e. U )
7	1 5 6	wunmap	|- ( ph -> ( ( Base ` D ) ^m ( Base ` C ) ) e. U )
8		df-hom	|- Hom = Slot ; 1 4
9	8 1 2	wunstr	|- ( ph -> ( Hom ` C ) e. U )
10	1 9	wunrn	|- ( ph -> ran ( Hom ` C ) e. U )
11	1 10	wununi	|- ( ph -> U. ran ( Hom ` C ) e. U )
12	8 1 3	wunstr	|- ( ph -> ( Hom ` D ) e. U )
13	1 12	wunrn	|- ( ph -> ran ( Hom ` D ) e. U )
14	1 13	wununi	|- ( ph -> U. ran ( Hom ` D ) e. U )
15	1 11 14	wunxp	|- ( ph -> ( U. ran ( Hom ` C ) X. U. ran ( Hom ` D ) ) e. U )
16	1 15	wunpw	|- ( ph -> ~P ( U. ran ( Hom ` C ) X. U. ran ( Hom ` D ) ) e. U )
17	1 6 6	wunxp	|- ( ph -> ( ( Base ` C ) X. ( Base ` C ) ) e. U )
18	1 16 17	wunmap	|- ( ph -> ( ~P ( U. ran ( Hom ` C ) X. U. ran ( Hom ` D ) ) ^m ( ( Base ` C ) X. ( Base ` C ) ) ) e. U )
19	1 7 18	wunxp	|- ( ph -> ( ( ( Base ` D ) ^m ( Base ` C ) ) X. ( ~P ( U. ran ( Hom ` C ) X. U. ran ( Hom ` D ) ) ^m ( ( Base ` C ) X. ( Base ` C ) ) ) ) e. U )
20		relfunc	|- Rel ( C Func D )
21	20	a1i	|- ( ph -> Rel ( C Func D ) )
22		df-br	|- ( f ( C Func D ) g <-> <. f , g >. e. ( C Func D ) )
23		eqid	|- ( Base ` C ) = ( Base ` C )
24		eqid	|- ( Base ` D ) = ( Base ` D )
25		simpr	|- ( ( ph /\ f ( C Func D ) g ) -> f ( C Func D ) g )
26	23 24 25	funcf1	|- ( ( ph /\ f ( C Func D ) g ) -> f : ( Base ` C ) --> ( Base ` D ) )
27		fvex	|- ( Base ` D ) e. _V
28		fvex	|- ( Base ` C ) e. _V
29	27 28	elmap	|- ( f e. ( ( Base ` D ) ^m ( Base ` C ) ) <-> f : ( Base ` C ) --> ( Base ` D ) )
30	26 29	sylibr	|- ( ( ph /\ f ( C Func D ) g ) -> f e. ( ( Base ` D ) ^m ( Base ` C ) ) )
31		mapsspw	|- ( ( ( f ` ( 1st ` z ) ) ( Hom ` D ) ( f ` ( 2nd ` z ) ) ) ^m ( ( Hom ` C ) ` z ) ) C_ ~P ( ( ( Hom ` C ) ` z ) X. ( ( f ` ( 1st ` z ) ) ( Hom ` D ) ( f ` ( 2nd ` z ) ) ) )
32		fvssunirn	|- ( ( Hom ` C ) ` z ) C_ U. ran ( Hom ` C )
33		ovssunirn	|- ( ( f ` ( 1st ` z ) ) ( Hom ` D ) ( f ` ( 2nd ` z ) ) ) C_ U. ran ( Hom ` D )
34		xpss12	|- ( ( ( ( Hom ` C ) ` z ) C_ U. ran ( Hom ` C ) /\ ( ( f ` ( 1st ` z ) ) ( Hom ` D ) ( f ` ( 2nd ` z ) ) ) C_ U. ran ( Hom ` D ) ) -> ( ( ( Hom ` C ) ` z ) X. ( ( f ` ( 1st ` z ) ) ( Hom ` D ) ( f ` ( 2nd ` z ) ) ) ) C_ ( U. ran ( Hom ` C ) X. U. ran ( Hom ` D ) ) )
35	32 33 34	mp2an	|- ( ( ( Hom ` C ) ` z ) X. ( ( f ` ( 1st ` z ) ) ( Hom ` D ) ( f ` ( 2nd ` z ) ) ) ) C_ ( U. ran ( Hom ` C ) X. U. ran ( Hom ` D ) )
36	35	sspwi	|- ~P ( ( ( Hom ` C ) ` z ) X. ( ( f ` ( 1st ` z ) ) ( Hom ` D ) ( f ` ( 2nd ` z ) ) ) ) C_ ~P ( U. ran ( Hom ` C ) X. U. ran ( Hom ` D ) )
37	31 36	sstri	|- ( ( ( f ` ( 1st ` z ) ) ( Hom ` D ) ( f ` ( 2nd ` z ) ) ) ^m ( ( Hom ` C ) ` z ) ) C_ ~P ( U. ran ( Hom ` C ) X. U. ran ( Hom ` D ) )
38	37	rgenw	|- A. z e. ( ( Base ` C ) X. ( Base ` C ) ) ( ( ( f ` ( 1st ` z ) ) ( Hom ` D ) ( f ` ( 2nd ` z ) ) ) ^m ( ( Hom ` C ) ` z ) ) C_ ~P ( U. ran ( Hom ` C ) X. U. ran ( Hom ` D ) )
39		ss2ixp	|- ( A. z e. ( ( Base ` C ) X. ( Base ` C ) ) ( ( ( f ` ( 1st ` z ) ) ( Hom ` D ) ( f ` ( 2nd ` z ) ) ) ^m ( ( Hom ` C ) ` z ) ) C_ ~P ( U. ran ( Hom ` C ) X. U. ran ( Hom ` D ) ) -> X_ z e. ( ( Base ` C ) X. ( Base ` C ) ) ( ( ( f ` ( 1st ` z ) ) ( Hom ` D ) ( f ` ( 2nd ` z ) ) ) ^m ( ( Hom ` C ) ` z ) ) C_ X_ z e. ( ( Base ` C ) X. ( Base ` C ) ) ~P ( U. ran ( Hom ` C ) X. U. ran ( Hom ` D ) ) )
40	38 39	ax-mp	|- X_ z e. ( ( Base ` C ) X. ( Base ` C ) ) ( ( ( f ` ( 1st ` z ) ) ( Hom ` D ) ( f ` ( 2nd ` z ) ) ) ^m ( ( Hom ` C ) ` z ) ) C_ X_ z e. ( ( Base ` C ) X. ( Base ` C ) ) ~P ( U. ran ( Hom ` C ) X. U. ran ( Hom ` D ) )
41	28 28	xpex	|- ( ( Base ` C ) X. ( Base ` C ) ) e. _V
42		fvex	|- ( Hom ` C ) e. _V
43	42	rnex	|- ran ( Hom ` C ) e. _V
44	43	uniex	|- U. ran ( Hom ` C ) e. _V
45		fvex	|- ( Hom ` D ) e. _V
46	45	rnex	|- ran ( Hom ` D ) e. _V
47	46	uniex	|- U. ran ( Hom ` D ) e. _V
48	44 47	xpex	|- ( U. ran ( Hom ` C ) X. U. ran ( Hom ` D ) ) e. _V
49	48	pwex	|- ~P ( U. ran ( Hom ` C ) X. U. ran ( Hom ` D ) ) e. _V
50	41 49	ixpconst	|- X_ z e. ( ( Base ` C ) X. ( Base ` C ) ) ~P ( U. ran ( Hom ` C ) X. U. ran ( Hom ` D ) ) = ( ~P ( U. ran ( Hom ` C ) X. U. ran ( Hom ` D ) ) ^m ( ( Base ` C ) X. ( Base ` C ) ) )
51	40 50	sseqtri	|- X_ z e. ( ( Base ` C ) X. ( Base ` C ) ) ( ( ( f ` ( 1st ` z ) ) ( Hom ` D ) ( f ` ( 2nd ` z ) ) ) ^m ( ( Hom ` C ) ` z ) ) C_ ( ~P ( U. ran ( Hom ` C ) X. U. ran ( Hom ` D ) ) ^m ( ( Base ` C ) X. ( Base ` C ) ) )
52		eqid	|- ( Hom ` C ) = ( Hom ` C )
53		eqid	|- ( Hom ` D ) = ( Hom ` D )
54	23 52 53 25	funcixp	|- ( ( ph /\ f ( C Func D ) g ) -> g e. X_ z e. ( ( Base ` C ) X. ( Base ` C ) ) ( ( ( f ` ( 1st ` z ) ) ( Hom ` D ) ( f ` ( 2nd ` z ) ) ) ^m ( ( Hom ` C ) ` z ) ) )
55	51 54	sseldi	|- ( ( ph /\ f ( C Func D ) g ) -> g e. ( ~P ( U. ran ( Hom ` C ) X. U. ran ( Hom ` D ) ) ^m ( ( Base ` C ) X. ( Base ` C ) ) ) )
56	30 55	opelxpd	|- ( ( ph /\ f ( C Func D ) g ) -> <. f , g >. e. ( ( ( Base ` D ) ^m ( Base ` C ) ) X. ( ~P ( U. ran ( Hom ` C ) X. U. ran ( Hom ` D ) ) ^m ( ( Base ` C ) X. ( Base ` C ) ) ) ) )
57	56	ex	|- ( ph -> ( f ( C Func D ) g -> <. f , g >. e. ( ( ( Base ` D ) ^m ( Base ` C ) ) X. ( ~P ( U. ran ( Hom ` C ) X. U. ran ( Hom ` D ) ) ^m ( ( Base ` C ) X. ( Base ` C ) ) ) ) ) )
58	22 57	syl5bir	|- ( ph -> ( <. f , g >. e. ( C Func D ) -> <. f , g >. e. ( ( ( Base ` D ) ^m ( Base ` C ) ) X. ( ~P ( U. ran ( Hom ` C ) X. U. ran ( Hom ` D ) ) ^m ( ( Base ` C ) X. ( Base ` C ) ) ) ) ) )
59	21 58	relssdv	|- ( ph -> ( C Func D ) C_ ( ( ( Base ` D ) ^m ( Base ` C ) ) X. ( ~P ( U. ran ( Hom ` C ) X. U. ran ( Hom ` D ) ) ^m ( ( Base ` C ) X. ( Base ` C ) ) ) ) )
60	1 19 59	wunss	|- ( ph -> ( C Func D ) e. U )