| Step |
Hyp |
Ref |
Expression |
| 1 |
|
invrcl.n |
|- N = ( Inv ` C ) |
| 2 |
|
invrcl.f |
|- ( ph -> F ( X N Y ) G ) |
| 3 |
|
invrcl2.b |
|- B = ( Base ` C ) |
| 4 |
|
df-br |
|- ( F ( X N Y ) G <-> <. F , G >. e. ( X N Y ) ) |
| 5 |
2 4
|
sylib |
|- ( ph -> <. F , G >. e. ( X N Y ) ) |
| 6 |
1 2
|
invrcl |
|- ( ph -> C e. Cat ) |
| 7 |
|
eqid |
|- ( Sect ` C ) = ( Sect ` C ) |
| 8 |
3 1 6 7
|
invffval |
|- ( ph -> N = ( x e. B , y e. B |-> ( ( x ( Sect ` C ) y ) i^i `' ( y ( Sect ` C ) x ) ) ) ) |
| 9 |
8
|
oveqd |
|- ( ph -> ( X N Y ) = ( X ( x e. B , y e. B |-> ( ( x ( Sect ` C ) y ) i^i `' ( y ( Sect ` C ) x ) ) ) Y ) ) |
| 10 |
5 9
|
eleqtrd |
|- ( ph -> <. F , G >. e. ( X ( x e. B , y e. B |-> ( ( x ( Sect ` C ) y ) i^i `' ( y ( Sect ` C ) x ) ) ) Y ) ) |
| 11 |
|
eqid |
|- ( x e. B , y e. B |-> ( ( x ( Sect ` C ) y ) i^i `' ( y ( Sect ` C ) x ) ) ) = ( x e. B , y e. B |-> ( ( x ( Sect ` C ) y ) i^i `' ( y ( Sect ` C ) x ) ) ) |
| 12 |
11
|
elmpocl |
|- ( <. F , G >. e. ( X ( x e. B , y e. B |-> ( ( x ( Sect ` C ) y ) i^i `' ( y ( Sect ` C ) x ) ) ) Y ) -> ( X e. B /\ Y e. B ) ) |
| 13 |
10 12
|
syl |
|- ( ph -> ( X e. B /\ Y e. B ) ) |