This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem wunfunc

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

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 baseid 
 |-  Base = Slot ( Base ` ndx )
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 homid 
 |-  Hom = Slot ( Hom ` ndx )
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 sselid 
 |-  ( ( 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 biimtrrid 
 |-  ( 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 )