| Step |
Hyp |
Ref |
Expression |
| 1 |
|
invrcl.n |
|- N = ( Inv ` C ) |
| 2 |
|
invrcl.f |
|- ( ph -> F ( X N Y ) G ) |
| 3 |
|
df-br |
|- ( F ( X N Y ) G <-> <. F , G >. e. ( X N Y ) ) |
| 4 |
|
df-ov |
|- ( X N Y ) = ( N ` <. X , Y >. ) |
| 5 |
4
|
eleq2i |
|- ( <. F , G >. e. ( X N Y ) <-> <. F , G >. e. ( N ` <. X , Y >. ) ) |
| 6 |
3 5
|
bitri |
|- ( F ( X N Y ) G <-> <. F , G >. e. ( N ` <. X , Y >. ) ) |
| 7 |
|
elfvne0 |
|- ( <. F , G >. e. ( N ` <. X , Y >. ) -> N =/= (/) ) |
| 8 |
6 7
|
sylbi |
|- ( F ( X N Y ) G -> N =/= (/) ) |
| 9 |
1
|
neeq1i |
|- ( N =/= (/) <-> ( Inv ` C ) =/= (/) ) |
| 10 |
|
n0 |
|- ( ( Inv ` C ) =/= (/) <-> E. x x e. ( Inv ` C ) ) |
| 11 |
9 10
|
bitri |
|- ( N =/= (/) <-> E. x x e. ( Inv ` C ) ) |
| 12 |
8 11
|
sylib |
|- ( F ( X N Y ) G -> E. x x e. ( Inv ` C ) ) |
| 13 |
|
df-inv |
|- Inv = ( c e. Cat |-> ( x e. ( Base ` c ) , y e. ( Base ` c ) |-> ( ( x ( Sect ` c ) y ) i^i `' ( y ( Sect ` c ) x ) ) ) ) |
| 14 |
13
|
mptrcl |
|- ( x e. ( Inv ` C ) -> C e. Cat ) |
| 15 |
14
|
exlimiv |
|- ( E. x x e. ( Inv ` C ) -> C e. Cat ) |
| 16 |
2 12 15
|
3syl |
|- ( ph -> C e. Cat ) |