| Step |
Hyp |
Ref |
Expression |
| 1 |
|
sectrcl.s |
|- S = ( Sect ` C ) |
| 2 |
|
sectrcl.f |
|- ( ph -> F ( X S Y ) G ) |
| 3 |
|
df-br |
|- ( F ( X S Y ) G <-> <. F , G >. e. ( X S Y ) ) |
| 4 |
|
df-ov |
|- ( X S Y ) = ( S ` <. X , Y >. ) |
| 5 |
4
|
eleq2i |
|- ( <. F , G >. e. ( X S Y ) <-> <. F , G >. e. ( S ` <. X , Y >. ) ) |
| 6 |
3 5
|
bitri |
|- ( F ( X S Y ) G <-> <. F , G >. e. ( S ` <. X , Y >. ) ) |
| 7 |
|
elfvne0 |
|- ( <. F , G >. e. ( S ` <. X , Y >. ) -> S =/= (/) ) |
| 8 |
6 7
|
sylbi |
|- ( F ( X S Y ) G -> S =/= (/) ) |
| 9 |
1
|
neeq1i |
|- ( S =/= (/) <-> ( Sect ` C ) =/= (/) ) |
| 10 |
|
n0 |
|- ( ( Sect ` C ) =/= (/) <-> E. x x e. ( Sect ` C ) ) |
| 11 |
9 10
|
bitri |
|- ( S =/= (/) <-> E. x x e. ( Sect ` C ) ) |
| 12 |
8 11
|
sylib |
|- ( F ( X S Y ) G -> E. x x e. ( Sect ` C ) ) |
| 13 |
|
df-sect |
|- Sect = ( c e. Cat |-> ( x e. ( Base ` c ) , y e. ( Base ` c ) |-> { <. f , g >. | [. ( Hom ` c ) / h ]. ( ( f e. ( x h y ) /\ g e. ( y h x ) ) /\ ( g ( <. x , y >. ( comp ` c ) x ) f ) = ( ( Id ` c ) ` x ) ) } ) ) |
| 14 |
13
|
mptrcl |
|- ( x e. ( Sect ` C ) -> C e. Cat ) |
| 15 |
14
|
exlimiv |
|- ( E. x x e. ( Sect ` C ) -> C e. Cat ) |
| 16 |
2 12 15
|
3syl |
|- ( ph -> C e. Cat ) |