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

Theorem catcfuccl 14191
Description: The category of categories for a weak universe is closed under the functor category operation. (Contributed by Mario Carneiro, 12-Jan-2017.)
Hypotheses
Ref Expression
catcfuccl.c  |-  C  =  (CatCat `  U )
catcfuccl.b  |-  B  =  ( Base `  C
)
catcfuccl.o  |-  Q  =  ( X FuncCat  Y )
catcfuccl.u  |-  ( ph  ->  U  e. WUni )
catcfuccl.1  |-  ( ph  ->  om  e.  U )
catcfuccl.x  |-  ( ph  ->  X  e.  B )
catcfuccl.y  |-  ( ph  ->  Y  e.  B )
Assertion
Ref Expression
catcfuccl  |-  ( ph  ->  Q  e.  B )

Proof of Theorem catcfuccl
Dummy variables  a 
b  f  g  h  v  x are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 catcfuccl.o . . . . 5  |-  Q  =  ( X FuncCat  Y )
2 eqid 2387 . . . . 5  |-  ( X 
Func  Y )  =  ( X  Func  Y )
3 eqid 2387 . . . . 5  |-  ( X Nat 
Y )  =  ( X Nat  Y )
4 eqid 2387 . . . . 5  |-  ( Base `  X )  =  (
Base `  X )
5 eqid 2387 . . . . 5  |-  (comp `  Y )  =  (comp `  Y )
6 inss2 3505 . . . . . 6  |-  ( U  i^i  Cat )  C_  Cat
7 catcfuccl.x . . . . . . 7  |-  ( ph  ->  X  e.  B )
8 catcfuccl.c . . . . . . . 8  |-  C  =  (CatCat `  U )
9 catcfuccl.b . . . . . . . 8  |-  B  =  ( Base `  C
)
10 catcfuccl.u . . . . . . . 8  |-  ( ph  ->  U  e. WUni )
118, 9, 10catcbas 14179 . . . . . . 7  |-  ( ph  ->  B  =  ( U  i^i  Cat ) )
127, 11eleqtrd 2463 . . . . . 6  |-  ( ph  ->  X  e.  ( U  i^i  Cat ) )
136, 12sseldi 3289 . . . . 5  |-  ( ph  ->  X  e.  Cat )
14 catcfuccl.y . . . . . . 7  |-  ( ph  ->  Y  e.  B )
1514, 11eleqtrd 2463 . . . . . 6  |-  ( ph  ->  Y  e.  ( U  i^i  Cat ) )
166, 15sseldi 3289 . . . . 5  |-  ( ph  ->  Y  e.  Cat )
17 eqidd 2388 . . . . 5  |-  ( ph  ->  ( v  e.  ( ( X  Func  Y
)  X.  ( X 
Func  Y ) ) ,  h  e.  ( X 
Func  Y )  |->  [_ ( 1st `  v )  / 
f ]_ [_ ( 2nd `  v )  /  g ]_ ( b  e.  ( g ( X Nat  Y
) h ) ,  a  e.  ( f ( X Nat  Y ) g )  |->  ( x  e.  ( Base `  X
)  |->  ( ( b `
 x ) (
<. ( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. (comp `  Y
) ( ( 1st `  h ) `  x
) ) ( a `
 x ) ) ) ) )  =  ( v  e.  ( ( X  Func  Y
)  X.  ( X 
Func  Y ) ) ,  h  e.  ( X 
Func  Y )  |->  [_ ( 1st `  v )  / 
f ]_ [_ ( 2nd `  v )  /  g ]_ ( b  e.  ( g ( X Nat  Y
) h ) ,  a  e.  ( f ( X Nat  Y ) g )  |->  ( x  e.  ( Base `  X
)  |->  ( ( b `
 x ) (
<. ( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. (comp `  Y
) ( ( 1st `  h ) `  x
) ) ( a `
 x ) ) ) ) ) )
181, 2, 3, 4, 5, 13, 16, 17fucval 14082 . . . 4  |-  ( ph  ->  Q  =  { <. (
Base `  ndx ) ,  ( X  Func  Y
) >. ,  <. (  Hom  `  ndx ) ,  ( X Nat  Y )
>. ,  <. (comp `  ndx ) ,  ( v  e.  ( ( X 
Func  Y )  X.  ( X  Func  Y ) ) ,  h  e.  ( X  Func  Y )  |-> 
[_ ( 1st `  v
)  /  f ]_ [_ ( 2nd `  v
)  /  g ]_ ( b  e.  ( g ( X Nat  Y
) h ) ,  a  e.  ( f ( X Nat  Y ) g )  |->  ( x  e.  ( Base `  X
)  |->  ( ( b `
 x ) (
<. ( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. (comp `  Y
) ( ( 1st `  h ) `  x
) ) ( a `
 x ) ) ) ) ) >. } )
19 df-base 13401 . . . . . . 7  |-  Base  = Slot  1
20 catcfuccl.1 . . . . . . . 8  |-  ( ph  ->  om  e.  U )
2110, 20wunndx 13412 . . . . . . 7  |-  ( ph  ->  ndx  e.  U )
2219, 10, 21wunstr 13415 . . . . . 6  |-  ( ph  ->  ( Base `  ndx )  e.  U )
23 inss1 3504 . . . . . . . 8  |-  ( U  i^i  Cat )  C_  U
2423, 12sseldi 3289 . . . . . . 7  |-  ( ph  ->  X  e.  U )
2523, 15sseldi 3289 . . . . . . 7  |-  ( ph  ->  Y  e.  U )
2610, 24, 25wunfunc 14023 . . . . . 6  |-  ( ph  ->  ( X  Func  Y
)  e.  U )
2710, 22, 26wunop 8530 . . . . 5  |-  ( ph  -> 
<. ( Base `  ndx ) ,  ( X  Func  Y ) >.  e.  U
)
28 df-hom 13480 . . . . . . 7  |-  Hom  = Slot ; 1 4
2928, 10, 21wunstr 13415 . . . . . 6  |-  ( ph  ->  (  Hom  `  ndx )  e.  U )
3010, 24, 25wunnat 14080 . . . . . 6  |-  ( ph  ->  ( X Nat  Y )  e.  U )
3110, 29, 30wunop 8530 . . . . 5  |-  ( ph  -> 
<. (  Hom  `  ndx ) ,  ( X Nat  Y ) >.  e.  U
)
32 df-cco 13481 . . . . . . 7  |- comp  = Slot ; 1 5
3332, 10, 21wunstr 13415 . . . . . 6  |-  ( ph  ->  (comp `  ndx )  e.  U )
3410, 26, 26wunxp 8532 . . . . . . . 8  |-  ( ph  ->  ( ( X  Func  Y )  X.  ( X 
Func  Y ) )  e.  U )
3510, 34, 26wunxp 8532 . . . . . . 7  |-  ( ph  ->  ( ( ( X 
Func  Y )  X.  ( X  Func  Y ) )  X.  ( X  Func  Y ) )  e.  U
)
3632, 10, 25wunstr 13415 . . . . . . . . . . . . . 14  |-  ( ph  ->  (comp `  Y )  e.  U )
3710, 36wunrn 8537 . . . . . . . . . . . . 13  |-  ( ph  ->  ran  (comp `  Y
)  e.  U )
3810, 37wununi 8514 . . . . . . . . . . . 12  |-  ( ph  ->  U. ran  (comp `  Y )  e.  U
)
3910, 38wunrn 8537 . . . . . . . . . . 11  |-  ( ph  ->  ran  U. ran  (comp `  Y )  e.  U
)
4010, 39wununi 8514 . . . . . . . . . 10  |-  ( ph  ->  U. ran  U. ran  (comp `  Y )  e.  U )
4110, 40wunpw 8515 . . . . . . . . 9  |-  ( ph  ->  ~P U. ran  U. ran  (comp `  Y )  e.  U )
4219, 10, 24wunstr 13415 . . . . . . . . 9  |-  ( ph  ->  ( Base `  X
)  e.  U )
4310, 41, 42wunmap 8534 . . . . . . . 8  |-  ( ph  ->  ( ~P U. ran  U.
ran  (comp `  Y )  ^m  ( Base `  X
) )  e.  U
)
4410, 30wunrn 8537 . . . . . . . . . 10  |-  ( ph  ->  ran  ( X Nat  Y
)  e.  U )
4510, 44wununi 8514 . . . . . . . . 9  |-  ( ph  ->  U. ran  ( X Nat 
Y )  e.  U
)
4610, 45, 45wunxp 8532 . . . . . . . 8  |-  ( ph  ->  ( U. ran  ( X Nat  Y )  X.  U. ran  ( X Nat  Y ) )  e.  U )
4710, 43, 46wunpm 8533 . . . . . . 7  |-  ( ph  ->  ( ( ~P U. ran  U. ran  (comp `  Y )  ^m  ( Base `  X ) ) 
^pm  ( U. ran  ( X Nat  Y )  X.  U. ran  ( X Nat 
Y ) ) )  e.  U )
48 fvex 5682 . . . . . . . . . . 11  |-  ( 1st `  v )  e.  _V
49 fvex 5682 . . . . . . . . . . . . . 14  |-  ( 2nd `  v )  e.  _V
50 ovex 6045 . . . . . . . . . . . . . . . . 17  |-  ( ~P
U. ran  U. ran  (comp `  Y )  ^m  ( Base `  X ) )  e.  _V
51 ovex 6045 . . . . . . . . . . . . . . . . . . . 20  |-  ( X Nat 
Y )  e.  _V
5251rnex 5073 . . . . . . . . . . . . . . . . . . 19  |-  ran  ( X Nat  Y )  e.  _V
5352uniex 4645 . . . . . . . . . . . . . . . . . 18  |-  U. ran  ( X Nat  Y )  e.  _V
5453, 53xpex 4930 . . . . . . . . . . . . . . . . 17  |-  ( U. ran  ( X Nat  Y )  X.  U. ran  ( X Nat  Y ) )  e. 
_V
55 eqid 2387 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  ( Base `  X
)  |->  ( ( b `
 x ) (
<. ( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. (comp `  Y
) ( ( 1st `  h ) `  x
) ) ( a `
 x ) ) )  =  ( x  e.  ( Base `  X
)  |->  ( ( b `
 x ) (
<. ( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. (comp `  Y
) ( ( 1st `  h ) `  x
) ) ( a `
 x ) ) )
56 ovssunirn 6046 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( b `  x ) ( <. ( ( 1st `  f ) `  x
) ,  ( ( 1st `  g ) `
 x ) >.
(comp `  Y )
( ( 1st `  h
) `  x )
) ( a `  x ) )  C_  U.
ran  ( <. (
( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. (comp `  Y
) ( ( 1st `  h ) `  x
) )
57 ovssunirn 6046 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( <.
( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. (comp `  Y
) ( ( 1st `  h ) `  x
) )  C_  U. ran  (comp `  Y )
58 rnss 5038 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
<. ( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. (comp `  Y
) ( ( 1st `  h ) `  x
) )  C_  U. ran  (comp `  Y )  ->  ran  ( <. ( ( 1st `  f ) `  x
) ,  ( ( 1st `  g ) `
 x ) >.
(comp `  Y )
( ( 1st `  h
) `  x )
)  C_  ran  U. ran  (comp `  Y ) )
59 uniss 3978 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ran  ( <. ( ( 1st `  f ) `  x
) ,  ( ( 1st `  g ) `
 x ) >.
(comp `  Y )
( ( 1st `  h
) `  x )
)  C_  ran  U. ran  (comp `  Y )  ->  U. ran  ( <. (
( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. (comp `  Y
) ( ( 1st `  h ) `  x
) )  C_  U. ran  U.
ran  (comp `  Y )
)
6057, 58, 59mp2b 10 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  U. ran  ( <. ( ( 1st `  f ) `  x
) ,  ( ( 1st `  g ) `
 x ) >.
(comp `  Y )
( ( 1st `  h
) `  x )
)  C_  U. ran  U. ran  (comp `  Y )
6156, 60sstri 3300 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( b `  x ) ( <. ( ( 1st `  f ) `  x
) ,  ( ( 1st `  g ) `
 x ) >.
(comp `  Y )
( ( 1st `  h
) `  x )
) ( a `  x ) )  C_  U.
ran  U. ran  (comp `  Y )
62 ovex 6045 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( b `  x ) ( <. ( ( 1st `  f ) `  x
) ,  ( ( 1st `  g ) `
 x ) >.
(comp `  Y )
( ( 1st `  h
) `  x )
) ( a `  x ) )  e. 
_V
6362elpw 3748 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( b `  x
) ( <. (
( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. (comp `  Y
) ( ( 1st `  h ) `  x
) ) ( a `
 x ) )  e.  ~P U. ran  U.
ran  (comp `  Y )  <->  ( ( b `  x
) ( <. (
( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. (comp `  Y
) ( ( 1st `  h ) `  x
) ) ( a `
 x ) ) 
C_  U. ran  U. ran  (comp `  Y ) )
6461, 63mpbir 201 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( b `  x ) ( <. ( ( 1st `  f ) `  x
) ,  ( ( 1st `  g ) `
 x ) >.
(comp `  Y )
( ( 1st `  h
) `  x )
) ( a `  x ) )  e. 
~P U. ran  U. ran  (comp `  Y )
6564a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  ( Base `  X
)  ->  ( (
b `  x )
( <. ( ( 1st `  f ) `  x
) ,  ( ( 1st `  g ) `
 x ) >.
(comp `  Y )
( ( 1st `  h
) `  x )
) ( a `  x ) )  e. 
~P U. ran  U. ran  (comp `  Y ) )
6655, 65fmpti 5831 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  ( Base `  X
)  |->  ( ( b `
 x ) (
<. ( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. (comp `  Y
) ( ( 1st `  h ) `  x
) ) ( a `
 x ) ) ) : ( Base `  X ) --> ~P U. ran  U. ran  (comp `  Y )
67 fvex 5682 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  (comp `  Y )  e.  _V
6867rnex 5073 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ran  (comp `  Y )  e.  _V
6968uniex 4645 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  U. ran  (comp `  Y )  e. 
_V
7069rnex 5073 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ran  U. ran  (comp `  Y )  e.  _V
7170uniex 4645 . . . . . . . . . . . . . . . . . . . . . 22  |-  U. ran  U.
ran  (comp `  Y )  e.  _V
7271pwex 4323 . . . . . . . . . . . . . . . . . . . . 21  |-  ~P U. ran  U. ran  (comp `  Y )  e.  _V
73 fvex 5682 . . . . . . . . . . . . . . . . . . . . 21  |-  ( Base `  X )  e.  _V
7472, 73elmap 6978 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( x  e.  ( Base `  X )  |->  ( ( b `  x ) ( <. ( ( 1st `  f ) `  x
) ,  ( ( 1st `  g ) `
 x ) >.
(comp `  Y )
( ( 1st `  h
) `  x )
) ( a `  x ) ) )  e.  ( ~P U. ran  U. ran  (comp `  Y )  ^m  ( Base `  X ) )  <-> 
( x  e.  (
Base `  X )  |->  ( ( b `  x ) ( <.
( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. (comp `  Y
) ( ( 1st `  h ) `  x
) ) ( a `
 x ) ) ) : ( Base `  X ) --> ~P U. ran  U. ran  (comp `  Y ) )
7566, 74mpbir 201 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  ( Base `  X
)  |->  ( ( b `
 x ) (
<. ( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. (comp `  Y
) ( ( 1st `  h ) `  x
) ) ( a `
 x ) ) )  e.  ( ~P
U. ran  U. ran  (comp `  Y )  ^m  ( Base `  X ) )
7675rgen2w 2717 . . . . . . . . . . . . . . . . . 18  |-  A. b  e.  ( g ( X Nat 
Y ) h ) A. a  e.  ( f ( X Nat  Y
) g ) ( x  e.  ( Base `  X )  |->  ( ( b `  x ) ( <. ( ( 1st `  f ) `  x
) ,  ( ( 1st `  g ) `
 x ) >.
(comp `  Y )
( ( 1st `  h
) `  x )
) ( a `  x ) ) )  e.  ( ~P U. ran  U. ran  (comp `  Y )  ^m  ( Base `  X ) )
77 eqid 2387 . . . . . . . . . . . . . . . . . . 19  |-  ( b  e.  ( g ( X Nat  Y ) h ) ,  a  e.  ( f ( X Nat 
Y ) g ) 
|->  ( x  e.  (
Base `  X )  |->  ( ( b `  x ) ( <.
( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. (comp `  Y
) ( ( 1st `  h ) `  x
) ) ( a `
 x ) ) ) )  =  ( b  e.  ( g ( X Nat  Y ) h ) ,  a  e.  ( f ( X Nat  Y ) g )  |->  ( x  e.  ( Base `  X
)  |->  ( ( b `
 x ) (
<. ( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. (comp `  Y
) ( ( 1st `  h ) `  x
) ) ( a `
 x ) ) ) )
7877fmpt2 6357 . . . . . . . . . . . . . . . . . 18  |-  ( A. b  e.  ( g
( X Nat  Y ) h ) A. a  e.  ( f ( X Nat 
Y ) g ) ( x  e.  (
Base `  X )  |->  ( ( b `  x ) ( <.
( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. (comp `  Y
) ( ( 1st `  h ) `  x
) ) ( a `
 x ) ) )  e.  ( ~P
U. ran  U. ran  (comp `  Y )  ^m  ( Base `  X ) )  <-> 
( b  e.  ( g ( X Nat  Y
) h ) ,  a  e.  ( f ( X Nat  Y ) g )  |->  ( x  e.  ( Base `  X
)  |->  ( ( b `
 x ) (
<. ( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. (comp `  Y
) ( ( 1st `  h ) `  x
) ) ( a `
 x ) ) ) ) : ( ( g ( X Nat 
Y ) h )  X.  ( f ( X Nat  Y ) g ) ) --> ( ~P
U. ran  U. ran  (comp `  Y )  ^m  ( Base `  X ) ) )
7976, 78mpbi 200 . . . . . . . . . . . . . . . . 17  |-  ( b  e.  ( g ( X Nat  Y ) h ) ,  a  e.  ( f ( X Nat 
Y ) g ) 
|->  ( x  e.  (
Base `  X )  |->  ( ( b `  x ) ( <.
( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. (comp `  Y
) ( ( 1st `  h ) `  x
) ) ( a `
 x ) ) ) ) : ( ( g ( X Nat 
Y ) h )  X.  ( f ( X Nat  Y ) g ) ) --> ( ~P
U. ran  U. ran  (comp `  Y )  ^m  ( Base `  X ) )
80 ovssunirn 6046 . . . . . . . . . . . . . . . . . 18  |-  ( g ( X Nat  Y ) h )  C_  U. ran  ( X Nat  Y )
81 ovssunirn 6046 . . . . . . . . . . . . . . . . . 18  |-  ( f ( X Nat  Y ) g )  C_  U. ran  ( X Nat  Y )
82 xpss12 4921 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( g ( X Nat 
Y ) h ) 
C_  U. ran  ( X Nat 
Y )  /\  (
f ( X Nat  Y
) g )  C_  U.
ran  ( X Nat  Y
) )  ->  (
( g ( X Nat 
Y ) h )  X.  ( f ( X Nat  Y ) g ) )  C_  ( U. ran  ( X Nat  Y
)  X.  U. ran  ( X Nat  Y )
) )
8380, 81, 82mp2an 654 . . . . . . . . . . . . . . . . 17  |-  ( ( g ( X Nat  Y
) h )  X.  ( f ( X Nat 
Y ) g ) )  C_  ( U. ran  ( X Nat  Y )  X.  U. ran  ( X Nat  Y ) )
84 elpm2r 6970 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ~P U. ran  U. ran  (comp `  Y )  ^m  ( Base `  X ) )  e.  _V  /\  ( U. ran  ( X Nat  Y
)  X.  U. ran  ( X Nat  Y )
)  e.  _V )  /\  ( ( b  e.  ( g ( X Nat 
Y ) h ) ,  a  e.  ( f ( X Nat  Y
) g )  |->  ( x  e.  ( Base `  X )  |->  ( ( b `  x ) ( <. ( ( 1st `  f ) `  x
) ,  ( ( 1st `  g ) `
 x ) >.
(comp `  Y )
( ( 1st `  h
) `  x )
) ( a `  x ) ) ) ) : ( ( g ( X Nat  Y
) h )  X.  ( f ( X Nat 
Y ) g ) ) --> ( ~P U. ran  U. ran  (comp `  Y )  ^m  ( Base `  X ) )  /\  ( ( g ( X Nat  Y ) h )  X.  (
f ( X Nat  Y
) g ) ) 
C_  ( U. ran  ( X Nat  Y )  X.  U. ran  ( X Nat 
Y ) ) ) )  ->  ( b  e.  ( g ( X Nat 
Y ) h ) ,  a  e.  ( f ( X Nat  Y
) g )  |->  ( x  e.  ( Base `  X )  |->  ( ( b `  x ) ( <. ( ( 1st `  f ) `  x
) ,  ( ( 1st `  g ) `
 x ) >.
(comp `  Y )
( ( 1st `  h
) `  x )
) ( a `  x ) ) ) )  e.  ( ( ~P U. ran  U. ran  (comp `  Y )  ^m  ( Base `  X
) )  ^pm  ( U. ran  ( X Nat  Y
)  X.  U. ran  ( X Nat  Y )
) ) )
8550, 54, 79, 83, 84mp4an 655 . . . . . . . . . . . . . . . 16  |-  ( b  e.  ( g ( X Nat  Y ) h ) ,  a  e.  ( f ( X Nat 
Y ) g ) 
|->  ( x  e.  (
Base `  X )  |->  ( ( b `  x ) ( <.
( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. (comp `  Y
) ( ( 1st `  h ) `  x
) ) ( a `
 x ) ) ) )  e.  ( ( ~P U. ran  U.
ran  (comp `  Y )  ^m  ( Base `  X
) )  ^pm  ( U. ran  ( X Nat  Y
)  X.  U. ran  ( X Nat  Y )
) )
8685sbcth 3118 . . . . . . . . . . . . . . 15  |-  ( ( 2nd `  v )  e.  _V  ->  [. ( 2nd `  v )  / 
g ]. ( b  e.  ( g ( X Nat 
Y ) h ) ,  a  e.  ( f ( X Nat  Y
) g )  |->  ( x  e.  ( Base `  X )  |->  ( ( b `  x ) ( <. ( ( 1st `  f ) `  x
) ,  ( ( 1st `  g ) `
 x ) >.
(comp `  Y )
( ( 1st `  h
) `  x )
) ( a `  x ) ) ) )  e.  ( ( ~P U. ran  U. ran  (comp `  Y )  ^m  ( Base `  X
) )  ^pm  ( U. ran  ( X Nat  Y
)  X.  U. ran  ( X Nat  Y )
) ) )
87 sbcel1g 3213 . . . . . . . . . . . . . . 15  |-  ( ( 2nd `  v )  e.  _V  ->  ( [. ( 2nd `  v
)  /  g ]. ( b  e.  ( g ( X Nat  Y
) h ) ,  a  e.  ( f ( X Nat  Y ) g )  |->  ( x  e.  ( Base `  X
)  |->  ( ( b `
 x ) (
<. ( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. (comp `  Y
) ( ( 1st `  h ) `  x
) ) ( a `
 x ) ) ) )  e.  ( ( ~P U. ran  U.
ran  (comp `  Y )  ^m  ( Base `  X
) )  ^pm  ( U. ran  ( X Nat  Y
)  X.  U. ran  ( X Nat  Y )
) )  <->  [_ ( 2nd `  v )  /  g ]_ ( b  e.  ( g ( X Nat  Y
) h ) ,  a  e.  ( f ( X Nat  Y ) g )  |->  ( x  e.  ( Base `  X
)  |->  ( ( b `
 x ) (
<. ( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. (comp `  Y
) ( ( 1st `  h ) `  x
) ) ( a `
 x ) ) ) )  e.  ( ( ~P U. ran  U.
ran  (comp `  Y )  ^m  ( Base `  X
) )  ^pm  ( U. ran  ( X Nat  Y
)  X.  U. ran  ( X Nat  Y )
) ) ) )
8886, 87mpbid 202 . . . . . . . . . . . . . 14  |-  ( ( 2nd `  v )  e.  _V  ->  [_ ( 2nd `  v )  / 
g ]_ ( b  e.  ( g ( X Nat 
Y ) h ) ,  a  e.  ( f ( X Nat  Y
) g )  |->  ( x  e.  ( Base `  X )  |->  ( ( b `  x ) ( <. ( ( 1st `  f ) `  x
) ,  ( ( 1st `  g ) `
 x ) >.
(comp `  Y )
( ( 1st `  h
) `  x )
) ( a `  x ) ) ) )  e.  ( ( ~P U. ran  U. ran  (comp `  Y )  ^m  ( Base `  X
) )  ^pm  ( U. ran  ( X Nat  Y
)  X.  U. ran  ( X Nat  Y )
) ) )
8949, 88ax-mp 8 . . . . . . . . . . . . 13  |-  [_ ( 2nd `  v )  / 
g ]_ ( b  e.  ( g ( X Nat 
Y ) h ) ,  a  e.  ( f ( X Nat  Y
) g )  |->  ( x  e.  ( Base `  X )  |->  ( ( b `  x ) ( <. ( ( 1st `  f ) `  x
) ,  ( ( 1st `  g ) `
 x ) >.
(comp `  Y )
( ( 1st `  h
) `  x )
) ( a `  x ) ) ) )  e.  ( ( ~P U. ran  U. ran  (comp `  Y )  ^m  ( Base `  X
) )  ^pm  ( U. ran  ( X Nat  Y
)  X.  U. ran  ( X Nat  Y )
) )
9089sbcth 3118 . . . . . . . . . . . 12  |-  ( ( 1st `  v )  e.  _V  ->  [. ( 1st `  v )  / 
f ]. [_ ( 2nd `  v )  /  g ]_ ( b  e.  ( g ( X Nat  Y
) h ) ,  a  e.  ( f ( X Nat  Y ) g )  |->  ( x  e.  ( Base `  X
)  |->  ( ( b `
 x ) (
<. ( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. (comp `  Y
) ( ( 1st `  h ) `  x
) ) ( a `
 x ) ) ) )  e.  ( ( ~P U. ran  U.
ran  (comp `  Y )  ^m  ( Base `  X
) )  ^pm  ( U. ran  ( X Nat  Y
)  X.  U. ran  ( X Nat  Y )
) ) )
91 sbcel1g 3213 . . . . . . . . . . . 12  |-  ( ( 1st `  v )  e.  _V  ->  ( [. ( 1st `  v
)  /  f ]. [_ ( 2nd `  v
)  /  g ]_ ( b  e.  ( g ( X Nat  Y
) h ) ,  a  e.  ( f ( X Nat  Y ) g )  |->  ( x  e.  ( Base `  X
)  |->  ( ( b `
 x ) (
<. ( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. (comp `  Y
) ( ( 1st `  h ) `  x
) ) ( a `
 x ) ) ) )  e.  ( ( ~P U. ran  U.
ran  (comp `  Y )  ^m  ( Base `  X
) )  ^pm  ( U. ran  ( X Nat  Y
)  X.  U. ran  ( X Nat  Y )
) )  <->  [_ ( 1st `  v )  /  f ]_ [_ ( 2nd `  v
)  /  g ]_ ( b  e.  ( g ( X Nat  Y
) h ) ,  a  e.  ( f ( X Nat  Y ) g )  |->  ( x  e.  ( Base `  X
)  |->  ( ( b `
 x ) (
<. ( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. (comp `  Y
) ( ( 1st `  h ) `  x
) ) ( a `
 x ) ) ) )  e.  ( ( ~P U. ran  U.
ran  (comp `  Y )  ^m  ( Base `  X
) )  ^pm  ( U. ran  ( X Nat  Y
)  X.  U. ran  ( X Nat  Y )
) ) ) )
9290, 91mpbid 202 . . . . . . . . . . 11  |-  ( ( 1st `  v )  e.  _V  ->  [_ ( 1st `  v )  / 
f ]_ [_ ( 2nd `  v )  /  g ]_ ( b  e.  ( g ( X Nat  Y
) h ) ,  a  e.  ( f ( X Nat  Y ) g )  |->  ( x  e.  ( Base `  X
)  |->  ( ( b `
 x ) (
<. ( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. (comp `  Y
) ( ( 1st `  h ) `  x
) ) ( a `
 x ) ) ) )  e.  ( ( ~P U. ran  U.
ran  (comp `  Y )  ^m  ( Base `  X
) )  ^pm  ( U. ran  ( X Nat  Y
)  X.  U. ran  ( X Nat  Y )
) ) )
9348, 92ax-mp 8 . . . . . . . . . 10  |-  [_ ( 1st `  v )  / 
f ]_ [_ ( 2nd `  v )  /  g ]_ ( b  e.  ( g ( X Nat  Y
) h ) ,  a  e.  ( f ( X Nat  Y ) g )  |->  ( x  e.  ( Base `  X
)  |->  ( ( b `
 x ) (
<. ( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. (comp `  Y
) ( ( 1st `  h ) `  x
) ) ( a `
 x ) ) ) )  e.  ( ( ~P U. ran  U.
ran  (comp `  Y )  ^m  ( Base `  X
) )  ^pm  ( U. ran  ( X Nat  Y
)  X.  U. ran  ( X Nat  Y )
) )
9493rgen2w 2717 . . . . . . . . 9  |-  A. v  e.  ( ( X  Func  Y )  X.  ( X 
Func  Y ) ) A. h  e.  ( X  Func  Y ) [_ ( 1st `  v )  / 
f ]_ [_ ( 2nd `  v )  /  g ]_ ( b  e.  ( g ( X Nat  Y
) h ) ,  a  e.  ( f ( X Nat  Y ) g )  |->  ( x  e.  ( Base `  X
)  |->  ( ( b `
 x ) (
<. ( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. (comp `  Y
) ( ( 1st `  h ) `  x
) ) ( a `
 x ) ) ) )  e.  ( ( ~P U. ran  U.
ran  (comp `  Y )  ^m  ( Base `  X
) )  ^pm  ( U. ran  ( X Nat  Y
)  X.  U. ran  ( X Nat  Y )
) )
95 eqid 2387 . . . . . . . . . 10  |-  ( v  e.  ( ( X 
Func  Y )  X.  ( X  Func  Y ) ) ,  h  e.  ( X  Func  Y )  |-> 
[_ ( 1st `  v
)  /  f ]_ [_ ( 2nd `  v
)  /  g ]_ ( b  e.  ( g ( X Nat  Y
) h ) ,  a  e.  ( f ( X Nat  Y ) g )  |->  ( x  e.  ( Base `  X
)  |->  ( ( b `
 x ) (
<. ( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. (comp `  Y
) ( ( 1st `  h ) `  x
) ) ( a `
 x ) ) ) ) )  =  ( v  e.  ( ( X  Func  Y
)  X.  ( X 
Func  Y ) ) ,  h  e.  ( X 
Func  Y )  |->  [_ ( 1st `  v )  / 
f ]_ [_ ( 2nd `  v )  /  g ]_ ( b  e.  ( g ( X Nat  Y
) h ) ,  a  e.  ( f ( X Nat  Y ) g )  |->  ( x  e.  ( Base `  X
)  |->  ( ( b `
 x ) (
<. ( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. (comp `  Y
) ( ( 1st `  h ) `  x
) ) ( a `
 x ) ) ) ) )
9695fmpt2 6357 . . . . . . . . 9  |-  ( A. v  e.  ( ( X  Func  Y )  X.  ( X  Func  Y
) ) A. h  e.  ( X  Func  Y
) [_ ( 1st `  v
)  /  f ]_ [_ ( 2nd `  v
)  /  g ]_ ( b  e.  ( g ( X Nat  Y
) h ) ,  a  e.  ( f ( X Nat  Y ) g )  |->  ( x  e.  ( Base `  X
)  |->  ( ( b `
 x ) (
<. ( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. (comp `  Y
) ( ( 1st `  h ) `  x
) ) ( a `
 x ) ) ) )  e.  ( ( ~P U. ran  U.
ran  (comp `  Y )  ^m  ( Base `  X
) )  ^pm  ( U. ran  ( X Nat  Y
)  X.  U. ran  ( X Nat  Y )
) )  <->  ( v  e.  ( ( X  Func  Y )  X.  ( X 
Func  Y ) ) ,  h  e.  ( X 
Func  Y )  |->  [_ ( 1st `  v )  / 
f ]_ [_ ( 2nd `  v )  /  g ]_ ( b  e.  ( g ( X Nat  Y
) h ) ,  a  e.  ( f ( X Nat  Y ) g )  |->  ( x  e.  ( Base `  X
)  |->  ( ( b `
 x ) (
<. ( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. (comp `  Y
) ( ( 1st `  h ) `  x
) ) ( a `
 x ) ) ) ) ) : ( ( ( X 
Func  Y )  X.  ( X  Func  Y ) )  X.  ( X  Func  Y ) ) --> ( ( ~P U. ran  U. ran  (comp `  Y )  ^m  ( Base `  X
) )  ^pm  ( U. ran  ( X Nat  Y
)  X.  U. ran  ( X Nat  Y )
) ) )
9794, 96mpbi 200 . . . . . . . 8  |-  ( v  e.  ( ( X 
Func  Y )  X.  ( X  Func  Y ) ) ,  h  e.  ( X  Func  Y )  |-> 
[_ ( 1st `  v
)  /  f ]_ [_ ( 2nd `  v
)  /  g ]_ ( b  e.  ( g ( X Nat  Y
) h ) ,  a  e.  ( f ( X Nat  Y ) g )  |->  ( x  e.  ( Base `  X
)  |->  ( ( b `
 x ) (
<. ( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. (comp `  Y
) ( ( 1st `  h ) `  x
) ) ( a `
 x ) ) ) ) ) : ( ( ( X 
Func  Y )  X.  ( X  Func  Y ) )  X.  ( X  Func  Y ) ) --> ( ( ~P U. ran  U. ran  (comp `  Y )  ^m  ( Base `  X
) )  ^pm  ( U. ran  ( X Nat  Y
)  X.  U. ran  ( X Nat  Y )
) )
9897a1i 11 . . . . . . 7  |-  ( ph  ->  ( v  e.  ( ( X  Func  Y
)  X.  ( X 
Func  Y ) ) ,  h  e.  ( X 
Func  Y )  |->  [_ ( 1st `  v )  / 
f ]_ [_ ( 2nd `  v )  /  g ]_ ( b  e.  ( g ( X Nat  Y
) h ) ,  a  e.  ( f ( X Nat  Y ) g )  |->  ( x  e.  ( Base `  X
)  |->  ( ( b `
 x ) (
<. ( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. (comp `  Y
) ( ( 1st `  h ) `  x
) ) ( a `
 x ) ) ) ) ) : ( ( ( X 
Func  Y )  X.  ( X  Func  Y ) )  X.  ( X  Func  Y ) ) --> ( ( ~P U. ran  U. ran  (comp `  Y )  ^m  ( Base `  X
) )  ^pm  ( U. ran  ( X Nat  Y
)  X.  U. ran  ( X Nat  Y )
) ) )
9910, 35, 47, 98wunf 8535 . . . . . 6  |-  ( ph  ->  ( v  e.  ( ( X  Func  Y
)  X.  ( X 
Func  Y ) ) ,  h  e.  ( X 
Func  Y )  |->  [_ ( 1st `  v )  / 
f ]_ [_ ( 2nd `  v )  /  g ]_ ( b  e.  ( g ( X Nat  Y
) h ) ,  a  e.  ( f ( X Nat  Y ) g )  |->  ( x  e.  ( Base `  X
)  |->  ( ( b `
 x ) (
<. ( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. (comp `  Y
) ( ( 1st `  h ) `  x
) ) ( a `
 x ) ) ) ) )  e.  U )
10010, 33, 99wunop 8530 . . . . 5  |-  ( ph  -> 
<. (comp `  ndx ) ,  ( v  e.  ( ( X  Func  Y
)  X.  ( X 
Func  Y ) ) ,  h  e.  ( X 
Func  Y )  |->  [_ ( 1st `  v )  / 
f ]_ [_ ( 2nd `  v )  /  g ]_ ( b  e.  ( g ( X Nat  Y
) h ) ,  a  e.  ( f ( X Nat  Y ) g )  |->  ( x  e.  ( Base `  X
)  |->  ( ( b `
 x ) (
<. ( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. (comp `  Y
) ( ( 1st `  h ) `  x
) ) ( a `
 x ) ) ) ) ) >.  e.  U )
10110, 27, 31, 100wuntp 8519 . . . 4  |-  ( ph  ->  { <. ( Base `  ndx ) ,  ( X  Func  Y ) >. ,  <. (  Hom  `  ndx ) ,  ( X Nat  Y )
>. ,  <. (comp `  ndx ) ,  ( v  e.  ( ( X 
Func  Y )  X.  ( X  Func  Y ) ) ,  h  e.  ( X  Func  Y )  |-> 
[_ ( 1st `  v
)  /  f ]_ [_ ( 2nd `  v
)  /  g ]_ ( b  e.  ( g ( X Nat  Y
) h ) ,  a  e.  ( f ( X Nat  Y ) g )  |->  ( x  e.  ( Base `  X
)  |->  ( ( b `
 x ) (
<. ( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. (comp `  Y
) ( ( 1st `  h ) `  x
) ) ( a `
 x ) ) ) ) ) >. }  e.  U )
10218, 101eqeltrd 2461 . . 3  |-  ( ph  ->  Q  e.  U )
1031, 13, 16fuccat 14094 . . 3  |-  ( ph  ->  Q  e.  Cat )
104 elin 3473 . . 3  |-  ( Q  e.  ( U  i^i  Cat )  <->  ( Q  e.  U  /\  Q  e. 
Cat ) )
105102, 103, 104sylanbrc 646 . 2  |-  ( ph  ->  Q  e.  ( U  i^i  Cat ) )
106105, 11eleqtrrd 2464 1  |-  ( ph  ->  Q  e.  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649    e. wcel 1717   A.wral 2649   _Vcvv 2899   [.wsbc 3104   [_csb 3194    i^i cin 3262    C_ wss 3263   ~Pcpw 3742   {ctp 3759   <.cop 3760   U.cuni 3957    e. cmpt 4207   omcom 4785    X. cxp 4816   ran crn 4819   -->wf 5390   ` cfv 5394  (class class class)co 6020    e. cmpt2 6022   1stc1st 6286   2ndc2nd 6287    ^m cmap 6954    ^pm cpm 6955  WUnicwun 8508   1c1 8924   4c4 9983   5c5 9984  ;cdc 10314   ndxcnx 13393   Basecbs 13396    Hom chom 13467  compcco 13468   Catccat 13816    Func cfunc 13978   Nat cnat 14065   FuncCat cfuc 14066  CatCatccatc 14176
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-13 1719  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368  ax-rep 4261  ax-sep 4271  ax-nul 4279  ax-pow 4318  ax-pr 4344  ax-un 4641  ax-inf2 7529  ax-cnex 8979  ax-resscn 8980  ax-1cn 8981  ax-icn 8982  ax-addcl 8983  ax-addrcl 8984  ax-mulcl 8985  ax-mulrcl 8986  ax-mulcom 8987  ax-addass 8988  ax-mulass 8989  ax-distr 8990  ax-i2m1 8991  ax-1ne0 8992  ax-1rid 8993  ax-rnegex 8994  ax-rrecex 8995  ax-cnre 8996  ax-pre-lttri 8997  ax-pre-lttrn 8998  ax-pre-ltadd 8999  ax-pre-mulgt0 9000
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2242  df-mo 2243  df-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-ne 2552  df-nel 2553  df-ral 2654  df-rex 2655  df-reu 2656  df-rmo 2657  df-rab 2658  df-v 2901  df-sbc 3105  df-csb 3195  df-dif 3266  df-un 3268  df-in 3270  df-ss 3277  df-pss 3279  df-nul 3572  df-if 3683  df-pw 3744  df-sn 3763  df-pr 3764  df-tp 3765  df-op 3766  df-uni 3958  df-int 3993  df-iun 4037  df-br 4154  df-opab 4208  df-mpt 4209  df-tr 4244  df-eprel 4435  df-id 4439  df-po 4444  df-so 4445  df-fr 4482  df-we 4484  df-ord 4525  df-on 4526  df-lim 4527  df-suc 4528  df-om 4786  df-xp 4824  df-rel 4825  df-cnv 4826  df-co 4827  df-dm 4828  df-rn 4829  df-res 4830  df-ima 4831  df-iota 5358  df-fun 5396  df-fn 5397  df-f 5398  df-f1 5399  df-fo 5400  df-f1o 5401  df-fv 5402  df-ov 6023  df-oprab 6024  df-mpt2 6025  df-1st 6288  df-2nd 6289  df-riota 6485  df-recs 6569  df-rdg 6604  df-1o 6660  df-oadd 6664  df-omul 6665  df-er 6841  df-ec 6843  df-qs 6847  df-map 6956  df-pm 6957  df-ixp 7000  df-en 7046  df-dom 7047  df-sdom 7048  df-fin 7049  df-wun 8510  df-ni 8682  df-pli 8683  df-mi 8684  df-lti 8685  df-plpq 8718  df-mpq 8719  df-ltpq 8720  df-enq 8721  df-nq 8722  df-erq 8723  df-plq 8724  df-mq 8725  df-1nq 8726  df-rq 8727  df-ltnq 8728  df-np 8791  df-plp 8793  df-ltp 8795  df-enr 8867  df-nr 8868  df-c 8929  df-pnf 9055  df-mnf 9056  df-xr 9057  df-ltxr 9058  df-le 9059  df-sub 9225  df-neg 9226  df-nn 9933  df-2 9990  df-3 9991  df-4 9992  df-5 9993  df-6 9994  df-7 9995  df-8 9996  df-9 9997  df-10 9998  df-n0 10154  df-z 10215  df-dec 10315  df-uz 10421  df-fz 10976  df-struct 13398  df-ndx 13399  df-slot 13400  df-base 13401  df-hom 13480  df-cco 13481  df-cat 13820  df-cid 13821  df-func 13982  df-nat 14067  df-fuc 14068  df-catc 14177
  Copyright terms: Public domain W3C validator