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

Theorem yonffthlem 16103
Description: Lemma for yonffth 16105. (Contributed by Mario Carneiro, 29-Jan-2017.)
Hypotheses
Ref Expression
yoneda.y  |-  Y  =  (Yon `  C )
yoneda.b  |-  B  =  ( Base `  C
)
yoneda.1  |-  .1.  =  ( Id `  C )
yoneda.o  |-  O  =  (oppCat `  C )
yoneda.s  |-  S  =  ( SetCat `  U )
yoneda.t  |-  T  =  ( SetCat `  V )
yoneda.q  |-  Q  =  ( O FuncCat  S )
yoneda.h  |-  H  =  (HomF
`  Q )
yoneda.r  |-  R  =  ( ( Q  X.c  O
) FuncCat  T )
yoneda.e  |-  E  =  ( O evalF  S )
yoneda.z  |-  Z  =  ( H  o.func  ( ( <. ( 1st `  Y
) , tpos  ( 2nd `  Y ) >.  o.func  ( Q  2ndF  O ) ) ⟨,⟩F  ( Q  1stF  O )
) )
yoneda.c  |-  ( ph  ->  C  e.  Cat )
yoneda.w  |-  ( ph  ->  V  e.  W )
yoneda.u  |-  ( ph  ->  ran  ( Hom f  `  C ) 
C_  U )
yoneda.v  |-  ( ph  ->  ( ran  ( Hom f  `  Q )  u.  U
)  C_  V )
yoneda.m  |-  M  =  ( f  e.  ( O  Func  S ) ,  x  e.  B  |->  ( a  e.  ( ( ( 1st `  Y
) `  x )
( O Nat  S ) f )  |->  ( ( a `  x ) `
 (  .1.  `  x ) ) ) )
yonedainv.i  |-  I  =  (Inv `  R )
yonedainv.n  |-  N  =  ( f  e.  ( O  Func  S ) ,  x  e.  B  |->  ( u  e.  ( ( 1st `  f
) `  x )  |->  ( y  e.  B  |->  ( g  e.  ( y ( Hom  `  C
) x )  |->  ( ( ( x ( 2nd `  f ) y ) `  g
) `  u )
) ) ) )
Assertion
Ref Expression
yonffthlem  |-  ( ph  ->  Y  e.  ( ( C Full  Q )  i^i  ( C Faith  Q ) ) )
Distinct variable groups:    f, a,
g, x, y,  .1.    u, a, g, y, C, f, x    E, a, f, g, u, y    B, a, f, g, u, x, y    N, a    O, a, f, g, u, x, y    S, a, f, g, u, x, y    g, M, u, y    Q, a, f, g, u, x    T, f, g, u, y    ph, a,
f, g, u, x, y    u, R    Y, a, f, g, u, x, y    Z, a, f, g, u, x, y
Allowed substitution hints:    Q( y)    R( x, y, f, g, a)    T( x, a)    U( x, y, u, f, g, a)    .1. ( u)    E( x)    H( x, y, u, f, g, a)    I( x, y, u, f, g, a)    M( x, f, a)    N( x, y, u, f, g)    V( x, y, u, f, g, a)    W( x, y, u, f, g, a)

Proof of Theorem yonffthlem
Dummy variables  h  w  z  v are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 relfunc 15703 . . 3  |-  Rel  ( C  Func  Q )
2 yoneda.y . . . 4  |-  Y  =  (Yon `  C )
3 yoneda.c . . . 4  |-  ( ph  ->  C  e.  Cat )
4 yoneda.o . . . 4  |-  O  =  (oppCat `  C )
5 yoneda.s . . . 4  |-  S  =  ( SetCat `  U )
6 yoneda.q . . . 4  |-  Q  =  ( O FuncCat  S )
7 yoneda.w . . . . 5  |-  ( ph  ->  V  e.  W )
8 yoneda.v . . . . . 6  |-  ( ph  ->  ( ran  ( Hom f  `  Q )  u.  U
)  C_  V )
98unssbd 3580 . . . . 5  |-  ( ph  ->  U  C_  V )
107, 9ssexd 4507 . . . 4  |-  ( ph  ->  U  e.  _V )
11 yoneda.u . . . 4  |-  ( ph  ->  ran  ( Hom f  `  C ) 
C_  U )
122, 3, 4, 5, 6, 10, 11yoncl 16083 . . 3  |-  ( ph  ->  Y  e.  ( C 
Func  Q ) )
13 1st2nd 6790 . . 3  |-  ( ( Rel  ( C  Func  Q )  /\  Y  e.  ( C  Func  Q
) )  ->  Y  =  <. ( 1st `  Y
) ,  ( 2nd `  Y ) >. )
141, 12, 13sylancr 667 . 2  |-  ( ph  ->  Y  =  <. ( 1st `  Y ) ,  ( 2nd `  Y
) >. )
15 1st2ndbr 6793 . . . . 5  |-  ( ( Rel  ( C  Func  Q )  /\  Y  e.  ( C  Func  Q
) )  ->  ( 1st `  Y ) ( C  Func  Q )
( 2nd `  Y
) )
161, 12, 15sylancr 667 . . . 4  |-  ( ph  ->  ( 1st `  Y
) ( C  Func  Q ) ( 2nd `  Y
) )
17 yoneda.b . . . . . . . . . . . . 13  |-  B  =  ( Base `  C
)
186fucbas 15801 . . . . . . . . . . . . 13  |-  ( O 
Func  S )  =  (
Base `  Q )
1917, 18, 16funcf1 15707 . . . . . . . . . . . 12  |-  ( ph  ->  ( 1st `  Y
) : B --> ( O 
Func  S ) )
2019adantr 466 . . . . . . . . . . 11  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B ) )  -> 
( 1st `  Y
) : B --> ( O 
Func  S ) )
21 simprr 764 . . . . . . . . . . 11  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B ) )  ->  w  e.  B )
2220, 21ffvelrnd 5975 . . . . . . . . . 10  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B ) )  -> 
( ( 1st `  Y
) `  w )  e.  ( O  Func  S
) )
23 simprl 762 . . . . . . . . . 10  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B ) )  -> 
z  e.  B )
24 opelxpi 4821 . . . . . . . . . 10  |-  ( ( ( ( 1st `  Y
) `  w )  e.  ( O  Func  S
)  /\  z  e.  B )  ->  <. (
( 1st `  Y
) `  w ) ,  z >.  e.  ( ( O  Func  S
)  X.  B ) )
2522, 23, 24syl2anc 665 . . . . . . . . 9  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B ) )  ->  <. ( ( 1st `  Y
) `  w ) ,  z >.  e.  ( ( O  Func  S
)  X.  B ) )
26 yoneda.r . . . . . . . . . . . . . 14  |-  R  =  ( ( Q  X.c  O
) FuncCat  T )
2726fucbas 15801 . . . . . . . . . . . . 13  |-  ( ( Q  X.c  O )  Func  T
)  =  ( Base `  R )
28 yonedainv.i . . . . . . . . . . . . 13  |-  I  =  (Inv `  R )
29 yoneda.1 . . . . . . . . . . . . . . . . . 18  |-  .1.  =  ( Id `  C )
30 yoneda.t . . . . . . . . . . . . . . . . . 18  |-  T  =  ( SetCat `  V )
31 yoneda.h . . . . . . . . . . . . . . . . . 18  |-  H  =  (HomF
`  Q )
32 yoneda.e . . . . . . . . . . . . . . . . . 18  |-  E  =  ( O evalF  S )
33 yoneda.z . . . . . . . . . . . . . . . . . 18  |-  Z  =  ( H  o.func  ( ( <. ( 1st `  Y
) , tpos  ( 2nd `  Y ) >.  o.func  ( Q  2ndF  O ) ) ⟨,⟩F  ( Q  1stF  O )
) )
342, 17, 29, 4, 5, 30, 6, 31, 26, 32, 33, 3, 7, 11, 8yonedalem1 16093 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( Z  e.  ( ( Q  X.c  O ) 
Func  T )  /\  E  e.  ( ( Q  X.c  O
)  Func  T )
) )
3534simpld 460 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  Z  e.  ( ( Q  X.c  O )  Func  T
) )
36 funcrcl 15704 . . . . . . . . . . . . . . . 16  |-  ( Z  e.  ( ( Q  X.c  O )  Func  T
)  ->  ( ( Q  X.c  O )  e.  Cat  /\  T  e.  Cat )
)
3735, 36syl 17 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( Q  X.c  O
)  e.  Cat  /\  T  e.  Cat )
)
3837simpld 460 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( Q  X.c  O )  e.  Cat )
3937simprd 464 . . . . . . . . . . . . . 14  |-  ( ph  ->  T  e.  Cat )
4026, 38, 39fuccat 15811 . . . . . . . . . . . . 13  |-  ( ph  ->  R  e.  Cat )
4134simprd 464 . . . . . . . . . . . . 13  |-  ( ph  ->  E  e.  ( ( Q  X.c  O )  Func  T
) )
42 eqid 2422 . . . . . . . . . . . . 13  |-  (  Iso  `  R )  =  (  Iso  `  R )
43 yoneda.m . . . . . . . . . . . . . 14  |-  M  =  ( f  e.  ( O  Func  S ) ,  x  e.  B  |->  ( a  e.  ( ( ( 1st `  Y
) `  x )
( O Nat  S ) f )  |->  ( ( a `  x ) `
 (  .1.  `  x ) ) ) )
44 yonedainv.n . . . . . . . . . . . . . 14  |-  N  =  ( f  e.  ( O  Func  S ) ,  x  e.  B  |->  ( u  e.  ( ( 1st `  f
) `  x )  |->  ( y  e.  B  |->  ( g  e.  ( y ( Hom  `  C
) x )  |->  ( ( ( x ( 2nd `  f ) y ) `  g
) `  u )
) ) ) )
452, 17, 29, 4, 5, 30, 6, 31, 26, 32, 33, 3, 7, 11, 8, 43, 28, 44yonedainv 16102 . . . . . . . . . . . . 13  |-  ( ph  ->  M ( Z I E ) N )
4627, 28, 40, 35, 41, 42, 45inviso2 15608 . . . . . . . . . . . 12  |-  ( ph  ->  N  e.  ( E (  Iso  `  R
) Z ) )
47 eqid 2422 . . . . . . . . . . . . . 14  |-  ( Q  X.c  O )  =  ( Q  X.c  O )
484, 17oppcbas 15559 . . . . . . . . . . . . . 14  |-  B  =  ( Base `  O
)
4947, 18, 48xpcbas 15999 . . . . . . . . . . . . 13  |-  ( ( O  Func  S )  X.  B )  =  (
Base `  ( Q  X.c  O ) )
50 eqid 2422 . . . . . . . . . . . . 13  |-  ( ( Q  X.c  O ) Nat  T )  =  ( ( Q  X.c  O ) Nat  T )
51 eqid 2422 . . . . . . . . . . . . 13  |-  (  Iso  `  T )  =  (  Iso  `  T )
5226, 49, 50, 41, 35, 42, 51fuciso 15816 . . . . . . . . . . . 12  |-  ( ph  ->  ( N  e.  ( E (  Iso  `  R
) Z )  <->  ( N  e.  ( E ( ( Q  X.c  O ) Nat  T ) Z )  /\  A. v  e.  ( ( O  Func  S )  X.  B ) ( N `
 v )  e.  ( ( ( 1st `  E ) `  v
) (  Iso  `  T
) ( ( 1st `  Z ) `  v
) ) ) ) )
5346, 52mpbid 213 . . . . . . . . . . 11  |-  ( ph  ->  ( N  e.  ( E ( ( Q  X.c  O ) Nat  T ) Z )  /\  A. v  e.  ( ( O  Func  S )  X.  B ) ( N `
 v )  e.  ( ( ( 1st `  E ) `  v
) (  Iso  `  T
) ( ( 1st `  Z ) `  v
) ) ) )
5453simprd 464 . . . . . . . . . 10  |-  ( ph  ->  A. v  e.  ( ( O  Func  S
)  X.  B ) ( N `  v
)  e.  ( ( ( 1st `  E
) `  v )
(  Iso  `  T ) ( ( 1st `  Z
) `  v )
) )
5554adantr 466 . . . . . . . . 9  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B ) )  ->  A. v  e.  (
( O  Func  S
)  X.  B ) ( N `  v
)  e.  ( ( ( 1st `  E
) `  v )
(  Iso  `  T ) ( ( 1st `  Z
) `  v )
) )
56 fveq2 5818 . . . . . . . . . . . 12  |-  ( v  =  <. ( ( 1st `  Y ) `  w
) ,  z >.  ->  ( N `  v
)  =  ( N `
 <. ( ( 1st `  Y ) `  w
) ,  z >.
) )
57 df-ov 6245 . . . . . . . . . . . 12  |-  ( ( ( 1st `  Y
) `  w ) N z )  =  ( N `  <. ( ( 1st `  Y
) `  w ) ,  z >. )
5856, 57syl6eqr 2474 . . . . . . . . . . 11  |-  ( v  =  <. ( ( 1st `  Y ) `  w
) ,  z >.  ->  ( N `  v
)  =  ( ( ( 1st `  Y
) `  w ) N z ) )
59 fveq2 5818 . . . . . . . . . . . . 13  |-  ( v  =  <. ( ( 1st `  Y ) `  w
) ,  z >.  ->  ( ( 1st `  E
) `  v )  =  ( ( 1st `  E ) `  <. ( ( 1st `  Y
) `  w ) ,  z >. )
)
60 df-ov 6245 . . . . . . . . . . . . 13  |-  ( ( ( 1st `  Y
) `  w )
( 1st `  E
) z )  =  ( ( 1st `  E
) `  <. ( ( 1st `  Y ) `
 w ) ,  z >. )
6159, 60syl6eqr 2474 . . . . . . . . . . . 12  |-  ( v  =  <. ( ( 1st `  Y ) `  w
) ,  z >.  ->  ( ( 1st `  E
) `  v )  =  ( ( ( 1st `  Y ) `
 w ) ( 1st `  E ) z ) )
62 fveq2 5818 . . . . . . . . . . . . 13  |-  ( v  =  <. ( ( 1st `  Y ) `  w
) ,  z >.  ->  ( ( 1st `  Z
) `  v )  =  ( ( 1st `  Z ) `  <. ( ( 1st `  Y
) `  w ) ,  z >. )
)
63 df-ov 6245 . . . . . . . . . . . . 13  |-  ( ( ( 1st `  Y
) `  w )
( 1st `  Z
) z )  =  ( ( 1st `  Z
) `  <. ( ( 1st `  Y ) `
 w ) ,  z >. )
6462, 63syl6eqr 2474 . . . . . . . . . . . 12  |-  ( v  =  <. ( ( 1st `  Y ) `  w
) ,  z >.  ->  ( ( 1st `  Z
) `  v )  =  ( ( ( 1st `  Y ) `
 w ) ( 1st `  Z ) z ) )
6561, 64oveq12d 6260 . . . . . . . . . . 11  |-  ( v  =  <. ( ( 1st `  Y ) `  w
) ,  z >.  ->  ( ( ( 1st `  E ) `  v
) (  Iso  `  T
) ( ( 1st `  Z ) `  v
) )  =  ( ( ( ( 1st `  Y ) `  w
) ( 1st `  E
) z ) (  Iso  `  T )
( ( ( 1st `  Y ) `  w
) ( 1st `  Z
) z ) ) )
6658, 65eleq12d 2494 . . . . . . . . . 10  |-  ( v  =  <. ( ( 1st `  Y ) `  w
) ,  z >.  ->  ( ( N `  v )  e.  ( ( ( 1st `  E
) `  v )
(  Iso  `  T ) ( ( 1st `  Z
) `  v )
)  <->  ( ( ( 1st `  Y ) `
 w ) N z )  e.  ( ( ( ( 1st `  Y ) `  w
) ( 1st `  E
) z ) (  Iso  `  T )
( ( ( 1st `  Y ) `  w
) ( 1st `  Z
) z ) ) ) )
6766rspcv 3114 . . . . . . . . 9  |-  ( <.
( ( 1st `  Y
) `  w ) ,  z >.  e.  ( ( O  Func  S
)  X.  B )  ->  ( A. v  e.  ( ( O  Func  S )  X.  B ) ( N `  v
)  e.  ( ( ( 1st `  E
) `  v )
(  Iso  `  T ) ( ( 1st `  Z
) `  v )
)  ->  ( (
( 1st `  Y
) `  w ) N z )  e.  ( ( ( ( 1st `  Y ) `
 w ) ( 1st `  E ) z ) (  Iso  `  T ) ( ( ( 1st `  Y
) `  w )
( 1st `  Z
) z ) ) ) )
6825, 55, 67sylc 62 . . . . . . . 8  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B ) )  -> 
( ( ( 1st `  Y ) `  w
) N z )  e.  ( ( ( ( 1st `  Y
) `  w )
( 1st `  E
) z ) (  Iso  `  T )
( ( ( 1st `  Y ) `  w
) ( 1st `  Z
) z ) ) )
694oppccat 15563 . . . . . . . . . . . . 13  |-  ( C  e.  Cat  ->  O  e.  Cat )
703, 69syl 17 . . . . . . . . . . . 12  |-  ( ph  ->  O  e.  Cat )
7170adantr 466 . . . . . . . . . . 11  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B ) )  ->  O  e.  Cat )
725setccat 15916 . . . . . . . . . . . . 13  |-  ( U  e.  _V  ->  S  e.  Cat )
7310, 72syl 17 . . . . . . . . . . . 12  |-  ( ph  ->  S  e.  Cat )
7473adantr 466 . . . . . . . . . . 11  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B ) )  ->  S  e.  Cat )
7532, 71, 74, 48, 22, 23evlf1 16041 . . . . . . . . . 10  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B ) )  -> 
( ( ( 1st `  Y ) `  w
) ( 1st `  E
) z )  =  ( ( 1st `  (
( 1st `  Y
) `  w )
) `  z )
)
763adantr 466 . . . . . . . . . . 11  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B ) )  ->  C  e.  Cat )
77 eqid 2422 . . . . . . . . . . 11  |-  ( Hom  `  C )  =  ( Hom  `  C )
782, 17, 76, 21, 77, 23yon11 16085 . . . . . . . . . 10  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B ) )  -> 
( ( 1st `  (
( 1st `  Y
) `  w )
) `  z )  =  ( z ( Hom  `  C )
w ) )
7975, 78eqtrd 2456 . . . . . . . . 9  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B ) )  -> 
( ( ( 1st `  Y ) `  w
) ( 1st `  E
) z )  =  ( z ( Hom  `  C ) w ) )
807adantr 466 . . . . . . . . . 10  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B ) )  ->  V  e.  W )
8111adantr 466 . . . . . . . . . 10  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B ) )  ->  ran  ( Hom f  `  C )  C_  U )
828adantr 466 . . . . . . . . . 10  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B ) )  -> 
( ran  ( Hom f  `  Q
)  u.  U ) 
C_  V )
832, 17, 29, 4, 5, 30, 6, 31, 26, 32, 33, 76, 80, 81, 82, 22, 23yonedalem21 16094 . . . . . . . . 9  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B ) )  -> 
( ( ( 1st `  Y ) `  w
) ( 1st `  Z
) z )  =  ( ( ( 1st `  Y ) `  z
) ( O Nat  S
) ( ( 1st `  Y ) `  w
) ) )
8479, 83oveq12d 6260 . . . . . . . 8  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B ) )  -> 
( ( ( ( 1st `  Y ) `
 w ) ( 1st `  E ) z ) (  Iso  `  T ) ( ( ( 1st `  Y
) `  w )
( 1st `  Z
) z ) )  =  ( ( z ( Hom  `  C
) w ) (  Iso  `  T )
( ( ( 1st `  Y ) `  z
) ( O Nat  S
) ( ( 1st `  Y ) `  w
) ) ) )
8568, 84eleqtrd 2502 . . . . . . 7  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B ) )  -> 
( ( ( 1st `  Y ) `  w
) N z )  e.  ( ( z ( Hom  `  C
) w ) (  Iso  `  T )
( ( ( 1st `  Y ) `  z
) ( O Nat  S
) ( ( 1st `  Y ) `  w
) ) ) )
869adantr 466 . . . . . . . . 9  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B ) )  ->  U  C_  V )
87 eqid 2422 . . . . . . . . . . . . 13  |-  ( Base `  S )  =  (
Base `  S )
88 relfunc 15703 . . . . . . . . . . . . . 14  |-  Rel  ( O  Func  S )
89 1st2ndbr 6793 . . . . . . . . . . . . . 14  |-  ( ( Rel  ( O  Func  S )  /\  ( ( 1st `  Y ) `
 w )  e.  ( O  Func  S
) )  ->  ( 1st `  ( ( 1st `  Y ) `  w
) ) ( O 
Func  S ) ( 2nd `  ( ( 1st `  Y
) `  w )
) )
9088, 22, 89sylancr 667 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B ) )  -> 
( 1st `  (
( 1st `  Y
) `  w )
) ( O  Func  S ) ( 2nd `  (
( 1st `  Y
) `  w )
) )
9148, 87, 90funcf1 15707 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B ) )  -> 
( 1st `  (
( 1st `  Y
) `  w )
) : B --> ( Base `  S ) )
9291, 23ffvelrnd 5975 . . . . . . . . . . 11  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B ) )  -> 
( ( 1st `  (
( 1st `  Y
) `  w )
) `  z )  e.  ( Base `  S
) )
935, 10setcbas 15909 . . . . . . . . . . . 12  |-  ( ph  ->  U  =  ( Base `  S ) )
9493adantr 466 . . . . . . . . . . 11  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B ) )  ->  U  =  ( Base `  S ) )
9592, 94eleqtrrd 2503 . . . . . . . . . 10  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B ) )  -> 
( ( 1st `  (
( 1st `  Y
) `  w )
) `  z )  e.  U )
9678, 95eqeltrrd 2501 . . . . . . . . 9  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B ) )  -> 
( z ( Hom  `  C ) w )  e.  U )
9786, 96sseldd 3401 . . . . . . . 8  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B ) )  -> 
( z ( Hom  `  C ) w )  e.  V )
98 eqid 2422 . . . . . . . . . 10  |-  ( Hom f  `  Q )  =  ( Hom f  `  Q )
99 eqid 2422 . . . . . . . . . . 11  |-  ( O Nat 
S )  =  ( O Nat  S )
1006, 99fuchom 15802 . . . . . . . . . 10  |-  ( O Nat 
S )  =  ( Hom  `  Q )
10120, 23ffvelrnd 5975 . . . . . . . . . 10  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B ) )  -> 
( ( 1st `  Y
) `  z )  e.  ( O  Func  S
) )
10298, 18, 100, 101, 22homfval 15533 . . . . . . . . 9  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B ) )  -> 
( ( ( 1st `  Y ) `  z
) ( Hom f  `  Q ) ( ( 1st `  Y
) `  w )
)  =  ( ( ( 1st `  Y
) `  z )
( O Nat  S ) ( ( 1st `  Y
) `  w )
) )
1038unssad 3579 . . . . . . . . . . 11  |-  ( ph  ->  ran  ( Hom f  `  Q ) 
C_  V )
104103adantr 466 . . . . . . . . . 10  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B ) )  ->  ran  ( Hom f  `  Q )  C_  V )
10598, 18homffn 15534 . . . . . . . . . . . 12  |-  ( Hom f  `  Q )  Fn  (
( O  Func  S
)  X.  ( O 
Func  S ) )
106105a1i 11 . . . . . . . . . . 11  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B ) )  -> 
( Hom f  `  Q )  Fn  ( ( O  Func  S )  X.  ( O 
Func  S ) ) )
107 fnovrn 6395 . . . . . . . . . . 11  |-  ( ( ( Hom f  `  Q )  Fn  ( ( O  Func  S )  X.  ( O 
Func  S ) )  /\  ( ( 1st `  Y
) `  z )  e.  ( O  Func  S
)  /\  ( ( 1st `  Y ) `  w )  e.  ( O  Func  S )
)  ->  ( (
( 1st `  Y
) `  z )
( Hom f  `  Q ) ( ( 1st `  Y
) `  w )
)  e.  ran  ( Hom f  `  Q ) )
108106, 101, 22, 107syl3anc 1264 . . . . . . . . . 10  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B ) )  -> 
( ( ( 1st `  Y ) `  z
) ( Hom f  `  Q ) ( ( 1st `  Y
) `  w )
)  e.  ran  ( Hom f  `  Q ) )
109104, 108sseldd 3401 . . . . . . . . 9  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B ) )  -> 
( ( ( 1st `  Y ) `  z
) ( Hom f  `  Q ) ( ( 1st `  Y
) `  w )
)  e.  V )
110102, 109eqeltrrd 2501 . . . . . . . 8  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B ) )  -> 
( ( ( 1st `  Y ) `  z
) ( O Nat  S
) ( ( 1st `  Y ) `  w
) )  e.  V
)
11130, 80, 97, 110, 51setciso 15922 . . . . . . 7  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B ) )  -> 
( ( ( ( 1st `  Y ) `
 w ) N z )  e.  ( ( z ( Hom  `  C ) w ) (  Iso  `  T
) ( ( ( 1st `  Y ) `
 z ) ( O Nat  S ) ( ( 1st `  Y
) `  w )
) )  <->  ( (
( 1st `  Y
) `  w ) N z ) : ( z ( Hom  `  C ) w ) -1-1-onto-> ( ( ( 1st `  Y
) `  z )
( O Nat  S ) ( ( 1st `  Y
) `  w )
) ) )
11285, 111mpbid 213 . . . . . 6  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B ) )  -> 
( ( ( 1st `  Y ) `  w
) N z ) : ( z ( Hom  `  C )
w ) -1-1-onto-> ( ( ( 1st `  Y ) `  z
) ( O Nat  S
) ( ( 1st `  Y ) `  w
) ) )
11376adantr 466 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
z  e.  B  /\  w  e.  B )
)  /\  h  e.  ( z ( Hom  `  C ) w ) )  ->  C  e.  Cat )
114113adantr 466 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( z  e.  B  /\  w  e.  B
) )  /\  h  e.  ( z ( Hom  `  C ) w ) )  /\  y  e.  B )  ->  C  e.  Cat )
11523adantr 466 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
z  e.  B  /\  w  e.  B )
)  /\  h  e.  ( z ( Hom  `  C ) w ) )  ->  z  e.  B )
116115adantr 466 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( z  e.  B  /\  w  e.  B
) )  /\  h  e.  ( z ( Hom  `  C ) w ) )  /\  y  e.  B )  ->  z  e.  B )
117 simpr 462 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( z  e.  B  /\  w  e.  B
) )  /\  h  e.  ( z ( Hom  `  C ) w ) )  /\  y  e.  B )  ->  y  e.  B )
1182, 17, 114, 116, 77, 117yon11 16085 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  ( z  e.  B  /\  w  e.  B
) )  /\  h  e.  ( z ( Hom  `  C ) w ) )  /\  y  e.  B )  ->  (
( 1st `  (
( 1st `  Y
) `  z )
) `  y )  =  ( y ( Hom  `  C )
z ) )
119118eqcomd 2428 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  ( z  e.  B  /\  w  e.  B
) )  /\  h  e.  ( z ( Hom  `  C ) w ) )  /\  y  e.  B )  ->  (
y ( Hom  `  C
) z )  =  ( ( 1st `  (
( 1st `  Y
) `  z )
) `  y )
)
120114adantr 466 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ph  /\  ( z  e.  B  /\  w  e.  B
) )  /\  h  e.  ( z ( Hom  `  C ) w ) )  /\  y  e.  B )  /\  g  e.  ( y ( Hom  `  C ) z ) )  ->  C  e.  Cat )
12121ad3antrrr 734 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ph  /\  ( z  e.  B  /\  w  e.  B
) )  /\  h  e.  ( z ( Hom  `  C ) w ) )  /\  y  e.  B )  /\  g  e.  ( y ( Hom  `  C ) z ) )  ->  w  e.  B )
122116adantr 466 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ph  /\  ( z  e.  B  /\  w  e.  B
) )  /\  h  e.  ( z ( Hom  `  C ) w ) )  /\  y  e.  B )  /\  g  e.  ( y ( Hom  `  C ) z ) )  ->  z  e.  B )
123 eqid 2422 . . . . . . . . . . . . . . 15  |-  (comp `  C )  =  (comp `  C )
124117adantr 466 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ph  /\  ( z  e.  B  /\  w  e.  B
) )  /\  h  e.  ( z ( Hom  `  C ) w ) )  /\  y  e.  B )  /\  g  e.  ( y ( Hom  `  C ) z ) )  ->  y  e.  B )
125 simpr 462 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ph  /\  ( z  e.  B  /\  w  e.  B
) )  /\  h  e.  ( z ( Hom  `  C ) w ) )  /\  y  e.  B )  /\  g  e.  ( y ( Hom  `  C ) z ) )  ->  g  e.  ( y ( Hom  `  C ) z ) )
126 simpllr 767 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ph  /\  ( z  e.  B  /\  w  e.  B
) )  /\  h  e.  ( z ( Hom  `  C ) w ) )  /\  y  e.  B )  /\  g  e.  ( y ( Hom  `  C ) z ) )  ->  h  e.  ( z ( Hom  `  C ) w ) )
1272, 17, 120, 121, 77, 122, 123, 124, 125, 126yon12 16086 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ph  /\  ( z  e.  B  /\  w  e.  B
) )  /\  h  e.  ( z ( Hom  `  C ) w ) )  /\  y  e.  B )  /\  g  e.  ( y ( Hom  `  C ) z ) )  ->  ( (
( z ( 2nd `  ( ( 1st `  Y
) `  w )
) y ) `  g ) `  h
)  =  ( h ( <. y ,  z
>. (comp `  C )
w ) g ) )
1282, 17, 120, 122, 77, 121, 123, 124, 126, 125yon2 16087 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ph  /\  ( z  e.  B  /\  w  e.  B
) )  /\  h  e.  ( z ( Hom  `  C ) w ) )  /\  y  e.  B )  /\  g  e.  ( y ( Hom  `  C ) z ) )  ->  ( (
( ( z ( 2nd `  Y ) w ) `  h
) `  y ) `  g )  =  ( h ( <. y ,  z >. (comp `  C ) w ) g ) )
129127, 128eqtr4d 2459 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ph  /\  ( z  e.  B  /\  w  e.  B
) )  /\  h  e.  ( z ( Hom  `  C ) w ) )  /\  y  e.  B )  /\  g  e.  ( y ( Hom  `  C ) z ) )  ->  ( (
( z ( 2nd `  ( ( 1st `  Y
) `  w )
) y ) `  g ) `  h
)  =  ( ( ( ( z ( 2nd `  Y ) w ) `  h
) `  y ) `  g ) )
130119, 129mpteq12dva 4437 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ( z  e.  B  /\  w  e.  B
) )  /\  h  e.  ( z ( Hom  `  C ) w ) )  /\  y  e.  B )  ->  (
g  e.  ( y ( Hom  `  C
) z )  |->  ( ( ( z ( 2nd `  ( ( 1st `  Y ) `
 w ) ) y ) `  g
) `  h )
)  =  ( g  e.  ( ( 1st `  ( ( 1st `  Y
) `  z )
) `  y )  |->  ( ( ( ( z ( 2nd `  Y
) w ) `  h ) `  y
) `  g )
) )
13116adantr 466 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B ) )  -> 
( 1st `  Y
) ( C  Func  Q ) ( 2nd `  Y
) )
13217, 77, 100, 131, 23, 21funcf2 15709 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B ) )  -> 
( z ( 2nd `  Y ) w ) : ( z ( Hom  `  C )
w ) --> ( ( ( 1st `  Y
) `  z )
( O Nat  S ) ( ( 1st `  Y
) `  w )
) )
133132ffvelrnda 5974 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
z  e.  B  /\  w  e.  B )
)  /\  h  e.  ( z ( Hom  `  C ) w ) )  ->  ( (
z ( 2nd `  Y
) w ) `  h )  e.  ( ( ( 1st `  Y
) `  z )
( O Nat  S ) ( ( 1st `  Y
) `  w )
) )
13499, 133nat1st2nd 15792 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
z  e.  B  /\  w  e.  B )
)  /\  h  e.  ( z ( Hom  `  C ) w ) )  ->  ( (
z ( 2nd `  Y
) w ) `  h )  e.  (
<. ( 1st `  (
( 1st `  Y
) `  z )
) ,  ( 2nd `  ( ( 1st `  Y
) `  z )
) >. ( O Nat  S
) <. ( 1st `  (
( 1st `  Y
) `  w )
) ,  ( 2nd `  ( ( 1st `  Y
) `  w )
) >. ) )
135134adantr 466 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( z  e.  B  /\  w  e.  B
) )  /\  h  e.  ( z ( Hom  `  C ) w ) )  /\  y  e.  B )  ->  (
( z ( 2nd `  Y ) w ) `
 h )  e.  ( <. ( 1st `  (
( 1st `  Y
) `  z )
) ,  ( 2nd `  ( ( 1st `  Y
) `  z )
) >. ( O Nat  S
) <. ( 1st `  (
( 1st `  Y
) `  w )
) ,  ( 2nd `  ( ( 1st `  Y
) `  w )
) >. ) )
136 eqid 2422 . . . . . . . . . . . . . . 15  |-  ( Hom  `  S )  =  ( Hom  `  S )
13799, 135, 48, 136, 117natcl 15794 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  ( z  e.  B  /\  w  e.  B
) )  /\  h  e.  ( z ( Hom  `  C ) w ) )  /\  y  e.  B )  ->  (
( ( z ( 2nd `  Y ) w ) `  h
) `  y )  e.  ( ( ( 1st `  ( ( 1st `  Y
) `  z )
) `  y )
( Hom  `  S ) ( ( 1st `  (
( 1st `  Y
) `  w )
) `  y )
) )
13810adantr 466 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B ) )  ->  U  e.  _V )
139138ad2antrr 730 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( z  e.  B  /\  w  e.  B
) )  /\  h  e.  ( z ( Hom  `  C ) w ) )  /\  y  e.  B )  ->  U  e.  _V )
14019ad2antrr 730 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  (
z  e.  B  /\  w  e.  B )
)  /\  h  e.  ( z ( Hom  `  C ) w ) )  ->  ( 1st `  Y ) : B --> ( O  Func  S ) )
141140, 115ffvelrnd 5975 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
z  e.  B  /\  w  e.  B )
)  /\  h  e.  ( z ( Hom  `  C ) w ) )  ->  ( ( 1st `  Y ) `  z )  e.  ( O  Func  S )
)
142 1st2ndbr 6793 . . . . . . . . . . . . . . . . . . 19  |-  ( ( Rel  ( O  Func  S )  /\  ( ( 1st `  Y ) `
 z )  e.  ( O  Func  S
) )  ->  ( 1st `  ( ( 1st `  Y ) `  z
) ) ( O 
Func  S ) ( 2nd `  ( ( 1st `  Y
) `  z )
) )
14388, 141, 142sylancr 667 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
z  e.  B  /\  w  e.  B )
)  /\  h  e.  ( z ( Hom  `  C ) w ) )  ->  ( 1st `  ( ( 1st `  Y
) `  z )
) ( O  Func  S ) ( 2nd `  (
( 1st `  Y
) `  z )
) )
14448, 87, 143funcf1 15707 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
z  e.  B  /\  w  e.  B )
)  /\  h  e.  ( z ( Hom  `  C ) w ) )  ->  ( 1st `  ( ( 1st `  Y
) `  z )
) : B --> ( Base `  S ) )
145144ffvelrnda 5974 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  ( z  e.  B  /\  w  e.  B
) )  /\  h  e.  ( z ( Hom  `  C ) w ) )  /\  y  e.  B )  ->  (
( 1st `  (
( 1st `  Y
) `  z )
) `  y )  e.  ( Base `  S
) )
14694ad2antrr 730 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  ( z  e.  B  /\  w  e.  B
) )  /\  h  e.  ( z ( Hom  `  C ) w ) )  /\  y  e.  B )  ->  U  =  ( Base `  S
) )
147145, 146eleqtrrd 2503 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( z  e.  B  /\  w  e.  B
) )  /\  h  e.  ( z ( Hom  `  C ) w ) )  /\  y  e.  B )  ->  (
( 1st `  (
( 1st `  Y
) `  z )
) `  y )  e.  U )
14891adantr 466 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
z  e.  B  /\  w  e.  B )
)  /\  h  e.  ( z ( Hom  `  C ) w ) )  ->  ( 1st `  ( ( 1st `  Y
) `  w )
) : B --> ( Base `  S ) )
149148ffvelrnda 5974 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  ( z  e.  B  /\  w  e.  B
) )  /\  h  e.  ( z ( Hom  `  C ) w ) )  /\  y  e.  B )  ->  (
( 1st `  (
( 1st `  Y
) `  w )
) `  y )  e.  ( Base `  S
) )
150149, 146eleqtrrd 2503 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( z  e.  B  /\  w  e.  B
) )  /\  h  e.  ( z ( Hom  `  C ) w ) )  /\  y  e.  B )  ->  (
( 1st `  (
( 1st `  Y
) `  w )
) `  y )  e.  U )
1515, 139, 136, 147, 150elsetchom 15912 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  ( z  e.  B  /\  w  e.  B
) )  /\  h  e.  ( z ( Hom  `  C ) w ) )  /\  y  e.  B )  ->  (
( ( ( z ( 2nd `  Y
) w ) `  h ) `  y
)  e.  ( ( ( 1st `  (
( 1st `  Y
) `  z )
) `  y )
( Hom  `  S ) ( ( 1st `  (
( 1st `  Y
) `  w )
) `  y )
)  <->  ( ( ( z ( 2nd `  Y
) w ) `  h ) `  y
) : ( ( 1st `  ( ( 1st `  Y ) `
 z ) ) `
 y ) --> ( ( 1st `  (
( 1st `  Y
) `  w )
) `  y )
) )
152137, 151mpbid 213 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  ( z  e.  B  /\  w  e.  B
) )  /\  h  e.  ( z ( Hom  `  C ) w ) )  /\  y  e.  B )  ->  (
( ( z ( 2nd `  Y ) w ) `  h
) `  y ) : ( ( 1st `  ( ( 1st `  Y
) `  z )
) `  y ) --> ( ( 1st `  (
( 1st `  Y
) `  w )
) `  y )
)
153152feqmptd 5871 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ( z  e.  B  /\  w  e.  B
) )  /\  h  e.  ( z ( Hom  `  C ) w ) )  /\  y  e.  B )  ->  (
( ( z ( 2nd `  Y ) w ) `  h
) `  y )  =  ( g  e.  ( ( 1st `  (
( 1st `  Y
) `  z )
) `  y )  |->  ( ( ( ( z ( 2nd `  Y
) w ) `  h ) `  y
) `  g )
) )
154130, 153eqtr4d 2459 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  ( z  e.  B  /\  w  e.  B
) )  /\  h  e.  ( z ( Hom  `  C ) w ) )  /\  y  e.  B )  ->  (
g  e.  ( y ( Hom  `  C
) z )  |->  ( ( ( z ( 2nd `  ( ( 1st `  Y ) `
 w ) ) y ) `  g
) `  h )
)  =  ( ( ( z ( 2nd `  Y ) w ) `
 h ) `  y ) )
155154mpteq2dva 4446 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
z  e.  B  /\  w  e.  B )
)  /\  h  e.  ( z ( Hom  `  C ) w ) )  ->  ( y  e.  B  |->  ( g  e.  ( y ( Hom  `  C )
z )  |->  ( ( ( z ( 2nd `  ( ( 1st `  Y
) `  w )
) y ) `  g ) `  h
) ) )  =  ( y  e.  B  |->  ( ( ( z ( 2nd `  Y
) w ) `  h ) `  y
) ) )
15680adantr 466 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
z  e.  B  /\  w  e.  B )
)  /\  h  e.  ( z ( Hom  `  C ) w ) )  ->  V  e.  W )
15781adantr 466 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
z  e.  B  /\  w  e.  B )
)  /\  h  e.  ( z ( Hom  `  C ) w ) )  ->  ran  ( Hom f  `  C )  C_  U
)
15882adantr 466 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
z  e.  B  /\  w  e.  B )
)  /\  h  e.  ( z ( Hom  `  C ) w ) )  ->  ( ran  ( Hom f  `  Q )  u.  U
)  C_  V )
15922adantr 466 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
z  e.  B  /\  w  e.  B )
)  /\  h  e.  ( z ( Hom  `  C ) w ) )  ->  ( ( 1st `  Y ) `  w )  e.  ( O  Func  S )
)
16078eleq2d 2485 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B ) )  -> 
( h  e.  ( ( 1st `  (
( 1st `  Y
) `  w )
) `  z )  <->  h  e.  ( z ( Hom  `  C )
w ) ) )
161160biimpar 487 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
z  e.  B  /\  w  e.  B )
)  /\  h  e.  ( z ( Hom  `  C ) w ) )  ->  h  e.  ( ( 1st `  (
( 1st `  Y
) `  w )
) `  z )
)
1622, 17, 29, 4, 5, 30, 6, 31, 26, 32, 33, 113, 156, 157, 158, 159, 115, 44, 161yonedalem4a 16096 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
z  e.  B  /\  w  e.  B )
)  /\  h  e.  ( z ( Hom  `  C ) w ) )  ->  ( (
( ( 1st `  Y
) `  w ) N z ) `  h )  =  ( y  e.  B  |->  ( g  e.  ( y ( Hom  `  C
) z )  |->  ( ( ( z ( 2nd `  ( ( 1st `  Y ) `
 w ) ) y ) `  g
) `  h )
) ) )
16399, 134, 48natfn 15795 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
z  e.  B  /\  w  e.  B )
)  /\  h  e.  ( z ( Hom  `  C ) w ) )  ->  ( (
z ( 2nd `  Y
) w ) `  h )  Fn  B
)
164 dffn5 5863 . . . . . . . . . . 11  |-  ( ( ( z ( 2nd `  Y ) w ) `
 h )  Fn  B  <->  ( ( z ( 2nd `  Y
) w ) `  h )  =  ( y  e.  B  |->  ( ( ( z ( 2nd `  Y ) w ) `  h
) `  y )
) )
165163, 164sylib 199 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
z  e.  B  /\  w  e.  B )
)  /\  h  e.  ( z ( Hom  `  C ) w ) )  ->  ( (
z ( 2nd `  Y
) w ) `  h )  =  ( y  e.  B  |->  ( ( ( z ( 2nd `  Y ) w ) `  h
) `  y )
) )
166155, 162, 1653eqtr4d 2466 . . . . . . . . 9  |-  ( ( ( ph  /\  (
z  e.  B  /\  w  e.  B )
)  /\  h  e.  ( z ( Hom  `  C ) w ) )  ->  ( (
( ( 1st `  Y
) `  w ) N z ) `  h )  =  ( ( z ( 2nd `  Y ) w ) `
 h ) )
167166mpteq2dva 4446 . . . . . . . 8  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B ) )  -> 
( h  e.  ( z ( Hom  `  C
) w )  |->  ( ( ( ( 1st `  Y ) `  w
) N z ) `
 h ) )  =  ( h  e.  ( z ( Hom  `  C ) w ) 
|->  ( ( z ( 2nd `  Y ) w ) `  h
) ) )
168 f1of 5767 . . . . . . . . . 10  |-  ( ( ( ( 1st `  Y
) `  w ) N z ) : ( z ( Hom  `  C ) w ) -1-1-onto-> ( ( ( 1st `  Y
) `  z )
( O Nat  S ) ( ( 1st `  Y
) `  w )
)  ->  ( (
( 1st `  Y
) `  w ) N z ) : ( z ( Hom  `  C ) w ) --> ( ( ( 1st `  Y ) `  z
) ( O Nat  S
) ( ( 1st `  Y ) `  w
) ) )
169112, 168syl 17 . . . . . . . . 9  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B ) )  -> 
( ( ( 1st `  Y ) `  w
) N z ) : ( z ( Hom  `  C )
w ) --> ( ( ( 1st `  Y
) `  z )
( O Nat  S ) ( ( 1st `  Y
) `  w )
) )
170169feqmptd 5871 . . . . . . . 8  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B ) )  -> 
( ( ( 1st `  Y ) `  w
) N z )  =  ( h  e.  ( z ( Hom  `  C ) w ) 
|->  ( ( ( ( 1st `  Y ) `
 w ) N z ) `  h
) ) )
171132feqmptd 5871 . . . . . . . 8  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B ) )  -> 
( z ( 2nd `  Y ) w )  =  ( h  e.  ( z ( Hom  `  C ) w ) 
|->  ( ( z ( 2nd `  Y ) w ) `  h
) ) )
172167, 170, 1713eqtr4d 2466 . . . . . . 7  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B ) )  -> 
( ( ( 1st `  Y ) `  w
) N z )  =  ( z ( 2nd `  Y ) w ) )
173 f1oeq1 5758 . . . . . . 7  |-  ( ( ( ( 1st `  Y
) `  w ) N z )  =  ( z ( 2nd `  Y ) w )  ->  ( ( ( ( 1st `  Y
) `  w ) N z ) : ( z ( Hom  `  C ) w ) -1-1-onto-> ( ( ( 1st `  Y
) `  z )
( O Nat  S ) ( ( 1st `  Y
) `  w )
)  <->  ( z ( 2nd `  Y ) w ) : ( z ( Hom  `  C
) w ) -1-1-onto-> ( ( ( 1st `  Y
) `  z )
( O Nat  S ) ( ( 1st `  Y
) `  w )
) ) )
174172, 173syl 17 . . . . . 6  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B ) )  -> 
( ( ( ( 1st `  Y ) `
 w ) N z ) : ( z ( Hom  `  C
) w ) -1-1-onto-> ( ( ( 1st `  Y
) `  z )
( O Nat  S ) ( ( 1st `  Y
) `  w )
)  <->  ( z ( 2nd `  Y ) w ) : ( z ( Hom  `  C
) w ) -1-1-onto-> ( ( ( 1st `  Y
) `  z )
( O Nat  S ) ( ( 1st `  Y
) `  w )
) ) )
175112, 174mpbid 213 . . . . 5  |-  ( (
ph  /\  ( z  e.  B  /\  w  e.  B ) )  -> 
( z ( 2nd `  Y ) w ) : ( z ( Hom  `  C )
w ) -1-1-onto-> ( ( ( 1st `  Y ) `  z
) ( O Nat  S
) ( ( 1st `  Y ) `  w
) ) )
176175ralrimivva 2780 . . . 4  |-  ( ph  ->  A. z  e.  B  A. w  e.  B  ( z ( 2nd `  Y ) w ) : ( z ( Hom  `  C )
w ) -1-1-onto-> ( ( ( 1st `  Y ) `  z
) ( O Nat  S
) ( ( 1st `  Y ) `  w
) ) )
17717, 77, 100isffth2 15757 . . . 4  |-  ( ( 1st `  Y ) ( ( C Full  Q
)  i^i  ( C Faith  Q ) ) ( 2nd `  Y )  <->  ( ( 1st `  Y ) ( C  Func  Q )
( 2nd `  Y
)  /\  A. z  e.  B  A. w  e.  B  ( z
( 2nd `  Y
) w ) : ( z ( Hom  `  C ) w ) -1-1-onto-> ( ( ( 1st `  Y
) `  z )
( O Nat  S ) ( ( 1st `  Y
) `  w )
) ) )
17816, 176, 177sylanbrc 668 . . 3  |-  ( ph  ->  ( 1st `  Y
) ( ( C Full 
Q )  i^i  ( C Faith  Q ) ) ( 2nd `  Y ) )
179 df-br 4360 . . 3  |-  ( ( 1st `  Y ) ( ( C Full  Q
)  i^i  ( C Faith  Q ) ) ( 2nd `  Y )  <->  <. ( 1st `  Y ) ,  ( 2nd `  Y )
>.  e.  ( ( C Full 
Q )  i^i  ( C Faith  Q ) ) )
180178, 179sylib 199 . 2  |-  ( ph  -> 
<. ( 1st `  Y
) ,  ( 2nd `  Y ) >.  e.  ( ( C Full  Q )  i^i  ( C Faith  Q
) ) )
18114, 180eqeltrd 2500 1  |-  ( ph  ->  Y  e.  ( ( C Full  Q )  i^i  ( C Faith  Q ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    /\ wa 370    = wceq 1437    e. wcel 1872   A.wral 2708   _Vcvv 3016    u. cun 3370    i^i cin 3371    C_ wss 3372   <.cop 3940   class class class wbr 4359    |-> cmpt 4418    X. cxp 4787   ran crn 4790   Rel wrel 4794    Fn wfn 5532   -->wf 5533   -1-1-onto->wf1o 5536   ` cfv 5537  (class class class)co 6242    |-> cmpt2 6244   1stc1st 6742   2ndc2nd 6743  tpos ctpos 6920   Basecbs 15057   Hom chom 15137  compcco 15138   Catccat 15506   Idccid 15507   Hom f chomf 15508  oppCatcoppc 15552  Invcinv 15586    Iso ciso 15587    Func cfunc 15695    o.func ccofu 15697   Full cful 15743   Faith cfth 15744   Nat cnat 15782   FuncCat cfuc 15783   SetCatcsetc 15906    X.c cxpc 15989    1stF c1stf 15990    2ndF c2ndf 15991   ⟨,⟩F cprf 15992   evalF cevlf 16030  HomFchof 16069  Yoncyon 16070
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2402  ax-rep 4472  ax-sep 4482  ax-nul 4491  ax-pow 4538  ax-pr 4596  ax-un 6534  ax-cnex 9539  ax-resscn 9540  ax-1cn 9541  ax-icn 9542  ax-addcl 9543  ax-addrcl 9544  ax-mulcl 9545  ax-mulrcl 9546  ax-mulcom 9547  ax-addass 9548  ax-mulass 9549  ax-distr 9550  ax-i2m1 9551  ax-1ne0 9552  ax-1rid 9553  ax-rnegex 9554  ax-rrecex 9555  ax-cnre 9556  ax-pre-lttri 9557  ax-pre-lttrn 9558  ax-pre-ltadd 9559  ax-pre-mulgt0 9560
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-fal 1443  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2274  df-mo 2275  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2552  df-ne 2595  df-nel 2596  df-ral 2713  df-rex 2714  df-reu 2715  df-rmo 2716  df-rab 2717  df-v 3018  df-sbc 3236  df-csb 3332  df-dif 3375  df-un 3377  df-in 3379  df-ss 3386  df-pss 3388  df-nul 3698  df-if 3848  df-pw 3919  df-sn 3935  df-pr 3937  df-tp 3939  df-op 3941  df-uni 4156  df-int 4192  df-iun 4237  df-br 4360  df-opab 4419  df-mpt 4420  df-tr 4455  df-eprel 4700  df-id 4704  df-po 4710  df-so 4711  df-fr 4748  df-we 4750  df-xp 4795  df-rel 4796  df-cnv 4797  df-co 4798  df-dm 4799  df-rn 4800  df-res 4801  df-ima 4802  df-pred 5335  df-ord 5381  df-on 5382  df-lim 5383  df-suc 5384  df-iota 5501  df-fun 5539  df-fn 5540  df-f 5541  df-f1 5542  df-fo 5543  df-f1o 5544  df-fv 5545  df-riota 6204  df-ov 6245  df-oprab 6246  df-mpt2 6247  df-om 6644  df-1st 6744  df-2nd 6745  df-tpos 6921  df-wrecs 6976  df-recs 7038  df-rdg 7076  df-1o 7130  df-oadd 7134  df-er 7311  df-map 7422  df-pm 7423  df-ixp 7471  df-en 7518  df-dom 7519  df-sdom 7520  df-fin 7521  df-pnf 9621  df-mnf 9622  df-xr 9623  df-ltxr 9624  df-le 9625  df-sub 9806  df-neg 9807  df-nn 10554  df-2 10612  df-3 10613  df-4 10614  df-5 10615  df-6 10616  df-7 10617  df-8 10618  df-9 10619  df-10 10620  df-n0 10814  df-z 10882  df-dec 10996  df-uz 11104  df-fz 11729  df-struct 15059  df-ndx 15060  df-slot 15061  df-base 15062  df-sets 15063  df-ress 15064  df-hom 15150  df-cco 15151  df-cat 15510  df-cid 15511  df-homf 15512  df-comf 15513  df-oppc 15553  df-sect 15588  df-inv 15589  df-iso 15590  df-ssc 15651  df-resc 15652  df-subc 15653  df-func 15699  df-cofu 15701  df-full 15745  df-fth 15746  df-nat 15784  df-fuc 15785  df-setc 15907  df-xpc 15993  df-1stf 15994  df-2ndf 15995  df-prf 15996  df-evlf 16034  df-curf 16035  df-hof 16071  df-yon 16072
This theorem is referenced by:  yonffth  16105
  Copyright terms: Public domain W3C validator