Metamath Proof Explorer

Theorem yonffthlem

Description: Lemma for yonffth . (Contributed by Mario Carneiro, 29-Jan-2017)

Ref Expression
Hypotheses 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 Xc. 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 ) ) pairF ( Q 1stF O ) ) )
yoneda.c 
|- ( ph -> C e. Cat )
yoneda.w 
|- ( ph -> V e. W )
yoneda.u 
|- ( ph -> ran ( Homf ` C ) C_ U )
yoneda.v 
|- ( ph -> ( ran ( Homf ` 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 yonffthlem 
|- ( ph -> Y e. ( ( C Full Q ) i^i ( C Faith Q ) ) )

Proof

Step Hyp Ref Expression
1 yoneda.y 
 |-  Y = ( Yon ` C )
2 yoneda.b 
 |-  B = ( Base ` C )
3 yoneda.1 
 |-  .1. = ( Id ` C )
4 yoneda.o 
 |-  O = ( oppCat ` C )
5 yoneda.s 
 |-  S = ( SetCat ` U )
6 yoneda.t 
 |-  T = ( SetCat ` V )
7 yoneda.q 
 |-  Q = ( O FuncCat S )
8 yoneda.h 
 |-  H = ( HomF ` Q )
9 yoneda.r 
 |-  R = ( ( Q Xc. O ) FuncCat T )
10 yoneda.e 
 |-  E = ( O evalF S )
11 yoneda.z 
 |-  Z = ( H o.func ( ( <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. o.func ( Q 2ndF O ) ) pairF ( Q 1stF O ) ) )
12 yoneda.c 
 |-  ( ph -> C e. Cat )
13 yoneda.w 
 |-  ( ph -> V e. W )
14 yoneda.u 
 |-  ( ph -> ran ( Homf ` C ) C_ U )
15 yoneda.v 
 |-  ( ph -> ( ran ( Homf ` Q ) u. U ) C_ V )
16 yoneda.m 
 |-  M = ( f e. ( O Func S ) , x e. B |-> ( a e. ( ( ( 1st ` Y ) ` x ) ( O Nat S ) f ) |-> ( ( a ` x ) ` ( .1. ` x ) ) ) )
17 yonedainv.i 
 |-  I = ( Inv ` R )
18 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 ) ) ) ) )
19 relfunc 
 |-  Rel ( C Func Q )
20 15 unssbd 
 |-  ( ph -> U C_ V )
21 13 20 ssexd 
 |-  ( ph -> U e. _V )
22 1 12 4 5 7 21 14 yoncl 
 |-  ( ph -> Y e. ( C Func Q ) )
23 1st2nd 
 |-  ( ( Rel ( C Func Q ) /\ Y e. ( C Func Q ) ) -> Y = <. ( 1st ` Y ) , ( 2nd ` Y ) >. )
24 19 22 23 sylancr 
 |-  ( ph -> Y = <. ( 1st ` Y ) , ( 2nd ` Y ) >. )
25 1st2ndbr 
 |-  ( ( Rel ( C Func Q ) /\ Y e. ( C Func Q ) ) -> ( 1st ` Y ) ( C Func Q ) ( 2nd ` Y ) )
26 19 22 25 sylancr 
 |-  ( ph -> ( 1st ` Y ) ( C Func Q ) ( 2nd ` Y ) )
27 fveq2 
 |-  ( v = <. ( ( 1st ` Y ) ` w ) , z >. -> ( N ` v ) = ( N ` <. ( ( 1st ` Y ) ` w ) , z >. ) )
28 df-ov 
 |-  ( ( ( 1st ` Y ) ` w ) N z ) = ( N ` <. ( ( 1st ` Y ) ` w ) , z >. )
29 27 28 eqtr4di 
 |-  ( v = <. ( ( 1st ` Y ) ` w ) , z >. -> ( N ` v ) = ( ( ( 1st ` Y ) ` w ) N z ) )
30 fveq2 
 |-  ( v = <. ( ( 1st ` Y ) ` w ) , z >. -> ( ( 1st ` E ) ` v ) = ( ( 1st ` E ) ` <. ( ( 1st ` Y ) ` w ) , z >. ) )
31 df-ov 
 |-  ( ( ( 1st ` Y ) ` w ) ( 1st ` E ) z ) = ( ( 1st ` E ) ` <. ( ( 1st ` Y ) ` w ) , z >. )
32 30 31 eqtr4di 
 |-  ( v = <. ( ( 1st ` Y ) ` w ) , z >. -> ( ( 1st ` E ) ` v ) = ( ( ( 1st ` Y ) ` w ) ( 1st ` E ) z ) )
33 fveq2 
 |-  ( v = <. ( ( 1st ` Y ) ` w ) , z >. -> ( ( 1st ` Z ) ` v ) = ( ( 1st ` Z ) ` <. ( ( 1st ` Y ) ` w ) , z >. ) )
34 df-ov 
 |-  ( ( ( 1st ` Y ) ` w ) ( 1st ` Z ) z ) = ( ( 1st ` Z ) ` <. ( ( 1st ` Y ) ` w ) , z >. )
35 33 34 eqtr4di 
 |-  ( v = <. ( ( 1st ` Y ) ` w ) , z >. -> ( ( 1st ` Z ) ` v ) = ( ( ( 1st ` Y ) ` w ) ( 1st ` Z ) z ) )
36 32 35 oveq12d 
 |-  ( 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 ) ) )
37 29 36 eleq12d 
 |-  ( 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 ) ) ) )
38 9 fucbas 
 |-  ( ( Q Xc. O ) Func T ) = ( Base ` R )
39 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 yonedalem1 
 |-  ( ph -> ( Z e. ( ( Q Xc. O ) Func T ) /\ E e. ( ( Q Xc. O ) Func T ) ) )
40 39 simpld 
 |-  ( ph -> Z e. ( ( Q Xc. O ) Func T ) )
41 funcrcl 
 |-  ( Z e. ( ( Q Xc. O ) Func T ) -> ( ( Q Xc. O ) e. Cat /\ T e. Cat ) )
42 40 41 syl 
 |-  ( ph -> ( ( Q Xc. O ) e. Cat /\ T e. Cat ) )
43 42 simpld 
 |-  ( ph -> ( Q Xc. O ) e. Cat )
44 42 simprd 
 |-  ( ph -> T e. Cat )
45 9 43 44 fuccat 
 |-  ( ph -> R e. Cat )
46 39 simprd 
 |-  ( ph -> E e. ( ( Q Xc. O ) Func T ) )
47 eqid 
 |-  ( Iso ` R ) = ( Iso ` R )
48 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 yonedainv 
 |-  ( ph -> M ( Z I E ) N )
49 38 17 45 40 46 47 48 inviso2 
 |-  ( ph -> N e. ( E ( Iso ` R ) Z ) )
50 eqid 
 |-  ( Q Xc. O ) = ( Q Xc. O )
51 7 fucbas 
 |-  ( O Func S ) = ( Base ` Q )
52 4 2 oppcbas 
 |-  B = ( Base ` O )
53 50 51 52 xpcbas 
 |-  ( ( O Func S ) X. B ) = ( Base ` ( Q Xc. O ) )
54 eqid 
 |-  ( ( Q Xc. O ) Nat T ) = ( ( Q Xc. O ) Nat T )
55 eqid 
 |-  ( Iso ` T ) = ( Iso ` T )
56 9 53 54 46 40 47 55 fuciso 
 |-  ( ph -> ( N e. ( E ( Iso ` R ) Z ) <-> ( N e. ( E ( ( Q Xc. O ) Nat T ) Z ) /\ A. v e. ( ( O Func S ) X. B ) ( N ` v ) e. ( ( ( 1st ` E ) ` v ) ( Iso ` T ) ( ( 1st ` Z ) ` v ) ) ) ) )
57 49 56 mpbid 
 |-  ( ph -> ( N e. ( E ( ( Q Xc. O ) Nat T ) Z ) /\ A. v e. ( ( O Func S ) X. B ) ( N ` v ) e. ( ( ( 1st ` E ) ` v ) ( Iso ` T ) ( ( 1st ` Z ) ` v ) ) ) )
58 57 simprd 
 |-  ( ph -> A. v e. ( ( O Func S ) X. B ) ( N ` v ) e. ( ( ( 1st ` E ) ` v ) ( Iso ` T ) ( ( 1st ` Z ) ` v ) ) )
59 58 adantr 
 |-  ( ( 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 ) ) )
60 2 51 26 funcf1 
 |-  ( ph -> ( 1st ` Y ) : B --> ( O Func S ) )
61 60 adantr 
 |-  ( ( ph /\ ( z e. B /\ w e. B ) ) -> ( 1st ` Y ) : B --> ( O Func S ) )
62 simprr 
 |-  ( ( ph /\ ( z e. B /\ w e. B ) ) -> w e. B )
63 61 62 ffvelrnd 
 |-  ( ( ph /\ ( z e. B /\ w e. B ) ) -> ( ( 1st ` Y ) ` w ) e. ( O Func S ) )
64 simprl 
 |-  ( ( ph /\ ( z e. B /\ w e. B ) ) -> z e. B )
65 63 64 opelxpd 
 |-  ( ( ph /\ ( z e. B /\ w e. B ) ) -> <. ( ( 1st ` Y ) ` w ) , z >. e. ( ( O Func S ) X. B ) )
66 37 59 65 rspcdva 
 |-  ( ( 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 ) ) )
67 4 oppccat 
 |-  ( C e. Cat -> O e. Cat )
68 12 67 syl 
 |-  ( ph -> O e. Cat )
69 68 adantr 
 |-  ( ( ph /\ ( z e. B /\ w e. B ) ) -> O e. Cat )
70 5 setccat 
 |-  ( U e. _V -> S e. Cat )
71 21 70 syl 
 |-  ( ph -> S e. Cat )
72 71 adantr 
 |-  ( ( ph /\ ( z e. B /\ w e. B ) ) -> S e. Cat )
73 10 69 72 52 63 64 evlf1 
 |-  ( ( ph /\ ( z e. B /\ w e. B ) ) -> ( ( ( 1st ` Y ) ` w ) ( 1st ` E ) z ) = ( ( 1st ` ( ( 1st ` Y ) ` w ) ) ` z ) )
74 12 adantr 
 |-  ( ( ph /\ ( z e. B /\ w e. B ) ) -> C e. Cat )
75 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
76 1 2 74 62 75 64 yon11 
 |-  ( ( ph /\ ( z e. B /\ w e. B ) ) -> ( ( 1st ` ( ( 1st ` Y ) ` w ) ) ` z ) = ( z ( Hom ` C ) w ) )
77 73 76 eqtrd 
 |-  ( ( ph /\ ( z e. B /\ w e. B ) ) -> ( ( ( 1st ` Y ) ` w ) ( 1st ` E ) z ) = ( z ( Hom ` C ) w ) )
78 13 adantr 
 |-  ( ( ph /\ ( z e. B /\ w e. B ) ) -> V e. W )
79 14 adantr 
 |-  ( ( ph /\ ( z e. B /\ w e. B ) ) -> ran ( Homf ` C ) C_ U )
80 15 adantr 
 |-  ( ( ph /\ ( z e. B /\ w e. B ) ) -> ( ran ( Homf ` Q ) u. U ) C_ V )
81 1 2 3 4 5 6 7 8 9 10 11 74 78 79 80 63 64 yonedalem21 
 |-  ( ( ph /\ ( z e. B /\ w e. B ) ) -> ( ( ( 1st ` Y ) ` w ) ( 1st ` Z ) z ) = ( ( ( 1st ` Y ) ` z ) ( O Nat S ) ( ( 1st ` Y ) ` w ) ) )
82 77 81 oveq12d 
 |-  ( ( 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 ) ) ) )
83 66 82 eleqtrd 
 |-  ( ( 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 ) ) ) )
84 20 adantr 
 |-  ( ( ph /\ ( z e. B /\ w e. B ) ) -> U C_ V )
85 eqid 
 |-  ( Base ` S ) = ( Base ` S )
86 relfunc 
 |-  Rel ( O Func S )
87 1st2ndbr 
 |-  ( ( Rel ( O Func S ) /\ ( ( 1st ` Y ) ` w ) e. ( O Func S ) ) -> ( 1st ` ( ( 1st ` Y ) ` w ) ) ( O Func S ) ( 2nd ` ( ( 1st ` Y ) ` w ) ) )
88 86 63 87 sylancr 
 |-  ( ( ph /\ ( z e. B /\ w e. B ) ) -> ( 1st ` ( ( 1st ` Y ) ` w ) ) ( O Func S ) ( 2nd ` ( ( 1st ` Y ) ` w ) ) )
89 52 85 88 funcf1 
 |-  ( ( ph /\ ( z e. B /\ w e. B ) ) -> ( 1st ` ( ( 1st ` Y ) ` w ) ) : B --> ( Base ` S ) )
90 89 64 ffvelrnd 
 |-  ( ( ph /\ ( z e. B /\ w e. B ) ) -> ( ( 1st ` ( ( 1st ` Y ) ` w ) ) ` z ) e. ( Base ` S ) )
91 5 21 setcbas 
 |-  ( ph -> U = ( Base ` S ) )
92 91 adantr 
 |-  ( ( ph /\ ( z e. B /\ w e. B ) ) -> U = ( Base ` S ) )
93 90 92 eleqtrrd 
 |-  ( ( ph /\ ( z e. B /\ w e. B ) ) -> ( ( 1st ` ( ( 1st ` Y ) ` w ) ) ` z ) e. U )
94 76 93 eqeltrrd 
 |-  ( ( ph /\ ( z e. B /\ w e. B ) ) -> ( z ( Hom ` C ) w ) e. U )
95 84 94 sseldd 
 |-  ( ( ph /\ ( z e. B /\ w e. B ) ) -> ( z ( Hom ` C ) w ) e. V )
96 eqid 
 |-  ( Homf ` Q ) = ( Homf ` Q )
97 eqid 
 |-  ( O Nat S ) = ( O Nat S )
98 7 97 fuchom 
 |-  ( O Nat S ) = ( Hom ` Q )
99 61 64 ffvelrnd 
 |-  ( ( ph /\ ( z e. B /\ w e. B ) ) -> ( ( 1st ` Y ) ` z ) e. ( O Func S ) )
100 96 51 98 99 63 homfval 
 |-  ( ( ph /\ ( z e. B /\ w e. B ) ) -> ( ( ( 1st ` Y ) ` z ) ( Homf ` Q ) ( ( 1st ` Y ) ` w ) ) = ( ( ( 1st ` Y ) ` z ) ( O Nat S ) ( ( 1st ` Y ) ` w ) ) )
101 15 unssad 
 |-  ( ph -> ran ( Homf ` Q ) C_ V )
102 101 adantr 
 |-  ( ( ph /\ ( z e. B /\ w e. B ) ) -> ran ( Homf ` Q ) C_ V )
103 96 51 homffn 
 |-  ( Homf ` Q ) Fn ( ( O Func S ) X. ( O Func S ) )
104 fnovrn 
 |-  ( ( ( Homf ` 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 ) ( Homf ` Q ) ( ( 1st ` Y ) ` w ) ) e. ran ( Homf ` Q ) )
105 103 99 63 104 mp3an2i 
 |-  ( ( ph /\ ( z e. B /\ w e. B ) ) -> ( ( ( 1st ` Y ) ` z ) ( Homf ` Q ) ( ( 1st ` Y ) ` w ) ) e. ran ( Homf ` Q ) )
106 102 105 sseldd 
 |-  ( ( ph /\ ( z e. B /\ w e. B ) ) -> ( ( ( 1st ` Y ) ` z ) ( Homf ` Q ) ( ( 1st ` Y ) ` w ) ) e. V )
107 100 106 eqeltrrd 
 |-  ( ( ph /\ ( z e. B /\ w e. B ) ) -> ( ( ( 1st ` Y ) ` z ) ( O Nat S ) ( ( 1st ` Y ) ` w ) ) e. V )
108 6 78 95 107 55 setciso 
 |-  ( ( 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 ) ) ) )
109 83 108 mpbid 
 |-  ( ( 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 ) ) )
110 74 adantr 
 |-  ( ( ( ph /\ ( z e. B /\ w e. B ) ) /\ h e. ( z ( Hom ` C ) w ) ) -> C e. Cat )
111 110 adantr 
 |-  ( ( ( ( ph /\ ( z e. B /\ w e. B ) ) /\ h e. ( z ( Hom ` C ) w ) ) /\ y e. B ) -> C e. Cat )
112 64 adantr 
 |-  ( ( ( ph /\ ( z e. B /\ w e. B ) ) /\ h e. ( z ( Hom ` C ) w ) ) -> z e. B )
113 112 adantr 
 |-  ( ( ( ( ph /\ ( z e. B /\ w e. B ) ) /\ h e. ( z ( Hom ` C ) w ) ) /\ y e. B ) -> z e. B )
114 simpr 
 |-  ( ( ( ( ph /\ ( z e. B /\ w e. B ) ) /\ h e. ( z ( Hom ` C ) w ) ) /\ y e. B ) -> y e. B )
115 1 2 111 113 75 114 yon11 
 |-  ( ( ( ( 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 ) )
116 115 eqcomd 
 |-  ( ( ( ( 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 ) )
117 111 adantr 
 |-  ( ( ( ( ( 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 )
118 62 ad3antrrr 
 |-  ( ( ( ( ( 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 )
119 113 adantr 
 |-  ( ( ( ( ( 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 )
120 eqid 
 |-  ( comp ` C ) = ( comp ` C )
121 114 adantr 
 |-  ( ( ( ( ( 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 )
122 simpr 
 |-  ( ( ( ( ( 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 ) )
123 simpllr 
 |-  ( ( ( ( ( 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 ) )
124 1 2 117 118 75 119 120 121 122 123 yon12 
 |-  ( ( ( ( ( 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 ) )
125 1 2 117 119 75 118 120 121 123 122 yon2 
 |-  ( ( ( ( ( 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 ) )
126 124 125 eqtr4d 
 |-  ( ( ( ( ( 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 ) )
127 116 126 mpteq12dva 
 |-  ( ( ( ( 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 ) ) )
128 26 adantr 
 |-  ( ( ph /\ ( z e. B /\ w e. B ) ) -> ( 1st ` Y ) ( C Func Q ) ( 2nd ` Y ) )
129 2 75 98 128 64 62 funcf2 
 |-  ( ( ph /\ ( z e. B /\ w e. B ) ) -> ( z ( 2nd ` Y ) w ) : ( z ( Hom ` C ) w ) --> ( ( ( 1st ` Y ) ` z ) ( O Nat S ) ( ( 1st ` Y ) ` w ) ) )
130 129 ffvelrnda 
 |-  ( ( ( 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 ) ) )
131 97 130 nat1st2nd 
 |-  ( ( ( 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 ) ) >. ) )
132 131 adantr 
 |-  ( ( ( ( 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 ) ) >. ) )
133 eqid 
 |-  ( Hom ` S ) = ( Hom ` S )
134 97 132 52 133 114 natcl 
 |-  ( ( ( ( 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 ) ) )
135 21 adantr 
 |-  ( ( ph /\ ( z e. B /\ w e. B ) ) -> U e. _V )
136 135 ad2antrr 
 |-  ( ( ( ( ph /\ ( z e. B /\ w e. B ) ) /\ h e. ( z ( Hom ` C ) w ) ) /\ y e. B ) -> U e. _V )
137 60 ad2antrr 
 |-  ( ( ( ph /\ ( z e. B /\ w e. B ) ) /\ h e. ( z ( Hom ` C ) w ) ) -> ( 1st ` Y ) : B --> ( O Func S ) )
138 137 112 ffvelrnd 
 |-  ( ( ( ph /\ ( z e. B /\ w e. B ) ) /\ h e. ( z ( Hom ` C ) w ) ) -> ( ( 1st ` Y ) ` z ) e. ( O Func S ) )
139 1st2ndbr 
 |-  ( ( Rel ( O Func S ) /\ ( ( 1st ` Y ) ` z ) e. ( O Func S ) ) -> ( 1st ` ( ( 1st ` Y ) ` z ) ) ( O Func S ) ( 2nd ` ( ( 1st ` Y ) ` z ) ) )
140 86 138 139 sylancr 
 |-  ( ( ( ph /\ ( z e. B /\ w e. B ) ) /\ h e. ( z ( Hom ` C ) w ) ) -> ( 1st ` ( ( 1st ` Y ) ` z ) ) ( O Func S ) ( 2nd ` ( ( 1st ` Y ) ` z ) ) )
141 52 85 140 funcf1 
 |-  ( ( ( ph /\ ( z e. B /\ w e. B ) ) /\ h e. ( z ( Hom ` C ) w ) ) -> ( 1st ` ( ( 1st ` Y ) ` z ) ) : B --> ( Base ` S ) )
142 141 ffvelrnda 
 |-  ( ( ( ( ph /\ ( z e. B /\ w e. B ) ) /\ h e. ( z ( Hom ` C ) w ) ) /\ y e. B ) -> ( ( 1st ` ( ( 1st ` Y ) ` z ) ) ` y ) e. ( Base ` S ) )
143 92 ad2antrr 
 |-  ( ( ( ( ph /\ ( z e. B /\ w e. B ) ) /\ h e. ( z ( Hom ` C ) w ) ) /\ y e. B ) -> U = ( Base ` S ) )
144 142 143 eleqtrrd 
 |-  ( ( ( ( ph /\ ( z e. B /\ w e. B ) ) /\ h e. ( z ( Hom ` C ) w ) ) /\ y e. B ) -> ( ( 1st ` ( ( 1st ` Y ) ` z ) ) ` y ) e. U )
145 89 adantr 
 |-  ( ( ( ph /\ ( z e. B /\ w e. B ) ) /\ h e. ( z ( Hom ` C ) w ) ) -> ( 1st ` ( ( 1st ` Y ) ` w ) ) : B --> ( Base ` S ) )
146 145 ffvelrnda 
 |-  ( ( ( ( ph /\ ( z e. B /\ w e. B ) ) /\ h e. ( z ( Hom ` C ) w ) ) /\ y e. B ) -> ( ( 1st ` ( ( 1st ` Y ) ` w ) ) ` y ) e. ( Base ` S ) )
147 146 143 eleqtrrd 
 |-  ( ( ( ( ph /\ ( z e. B /\ w e. B ) ) /\ h e. ( z ( Hom ` C ) w ) ) /\ y e. B ) -> ( ( 1st ` ( ( 1st ` Y ) ` w ) ) ` y ) e. U )
148 5 136 133 144 147 elsetchom 
 |-  ( ( ( ( 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 ) ) )
149 134 148 mpbid 
 |-  ( ( ( ( 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 ) )
150 149 feqmptd 
 |-  ( ( ( ( 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 ) ) )
151 127 150 eqtr4d 
 |-  ( ( ( ( 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 ) )
152 151 mpteq2dva 
 |-  ( ( ( 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 ) ) )
153 78 adantr 
 |-  ( ( ( ph /\ ( z e. B /\ w e. B ) ) /\ h e. ( z ( Hom ` C ) w ) ) -> V e. W )
154 79 adantr 
 |-  ( ( ( ph /\ ( z e. B /\ w e. B ) ) /\ h e. ( z ( Hom ` C ) w ) ) -> ran ( Homf ` C ) C_ U )
155 80 adantr 
 |-  ( ( ( ph /\ ( z e. B /\ w e. B ) ) /\ h e. ( z ( Hom ` C ) w ) ) -> ( ran ( Homf ` Q ) u. U ) C_ V )
156 63 adantr 
 |-  ( ( ( ph /\ ( z e. B /\ w e. B ) ) /\ h e. ( z ( Hom ` C ) w ) ) -> ( ( 1st ` Y ) ` w ) e. ( O Func S ) )
157 76 eleq2d 
 |-  ( ( ph /\ ( z e. B /\ w e. B ) ) -> ( h e. ( ( 1st ` ( ( 1st ` Y ) ` w ) ) ` z ) <-> h e. ( z ( Hom ` C ) w ) ) )
158 157 biimpar 
 |-  ( ( ( ph /\ ( z e. B /\ w e. B ) ) /\ h e. ( z ( Hom ` C ) w ) ) -> h e. ( ( 1st ` ( ( 1st ` Y ) ` w ) ) ` z ) )
159 1 2 3 4 5 6 7 8 9 10 11 110 153 154 155 156 112 18 158 yonedalem4a 
 |-  ( ( ( 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 ) ) ) )
160 97 131 52 natfn 
 |-  ( ( ( ph /\ ( z e. B /\ w e. B ) ) /\ h e. ( z ( Hom ` C ) w ) ) -> ( ( z ( 2nd ` Y ) w ) ` h ) Fn B )
161 dffn5 
 |-  ( ( ( z ( 2nd ` Y ) w ) ` h ) Fn B <-> ( ( z ( 2nd ` Y ) w ) ` h ) = ( y e. B |-> ( ( ( z ( 2nd ` Y ) w ) ` h ) ` y ) ) )
162 160 161 sylib 
 |-  ( ( ( 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 ) ) )
163 152 159 162 3eqtr4d 
 |-  ( ( ( ph /\ ( z e. B /\ w e. B ) ) /\ h e. ( z ( Hom ` C ) w ) ) -> ( ( ( ( 1st ` Y ) ` w ) N z ) ` h ) = ( ( z ( 2nd ` Y ) w ) ` h ) )
164 163 mpteq2dva 
 |-  ( ( 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 ) ) )
165 f1of 
 |-  ( ( ( ( 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 ) ) )
166 109 165 syl 
 |-  ( ( 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 ) ) )
167 166 feqmptd 
 |-  ( ( ph /\ ( z e. B /\ w e. B ) ) -> ( ( ( 1st ` Y ) ` w ) N z ) = ( h e. ( z ( Hom ` C ) w ) |-> ( ( ( ( 1st ` Y ) ` w ) N z ) ` h ) ) )
168 129 feqmptd 
 |-  ( ( ph /\ ( z e. B /\ w e. B ) ) -> ( z ( 2nd ` Y ) w ) = ( h e. ( z ( Hom ` C ) w ) |-> ( ( z ( 2nd ` Y ) w ) ` h ) ) )
169 164 167 168 3eqtr4d 
 |-  ( ( ph /\ ( z e. B /\ w e. B ) ) -> ( ( ( 1st ` Y ) ` w ) N z ) = ( z ( 2nd ` Y ) w ) )
170 169 f1oeq1d 
 |-  ( ( 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 ) ) ) )
171 109 170 mpbid 
 |-  ( ( 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 ) ) )
172 171 ralrimivva 
 |-  ( 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 ) ) )
173 2 75 98 isffth2 
 |-  ( ( 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 ) ) ) )
174 26 172 173 sylanbrc 
 |-  ( ph -> ( 1st ` Y ) ( ( C Full Q ) i^i ( C Faith Q ) ) ( 2nd ` Y ) )
175 df-br 
 |-  ( ( 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 ) ) )
176 174 175 sylib 
 |-  ( ph -> <. ( 1st ` Y ) , ( 2nd ` Y ) >. e. ( ( C Full Q ) i^i ( C Faith Q ) ) )
177 24 176 eqeltrd 
 |-  ( ph -> Y e. ( ( C Full Q ) i^i ( C Faith Q ) ) )