| Step |
Hyp |
Ref |
Expression |
| 1 |
|
invfval.b |
|- B = ( Base ` C ) |
| 2 |
|
invfval.n |
|- N = ( Inv ` C ) |
| 3 |
|
invfval.c |
|- ( ph -> C e. Cat ) |
| 4 |
|
invfval.x |
|- ( ph -> X e. B ) |
| 5 |
|
invfval.y |
|- ( ph -> Y e. B ) |
| 6 |
|
invfval.s |
|- S = ( Sect ` C ) |
| 7 |
1 2 3 6
|
invffval |
|- ( ph -> N = ( x e. B , y e. B |-> ( ( x S y ) i^i `' ( y S x ) ) ) ) |
| 8 |
|
simprl |
|- ( ( ph /\ ( x = X /\ y = Y ) ) -> x = X ) |
| 9 |
|
simprr |
|- ( ( ph /\ ( x = X /\ y = Y ) ) -> y = Y ) |
| 10 |
8 9
|
oveq12d |
|- ( ( ph /\ ( x = X /\ y = Y ) ) -> ( x S y ) = ( X S Y ) ) |
| 11 |
9 8
|
oveq12d |
|- ( ( ph /\ ( x = X /\ y = Y ) ) -> ( y S x ) = ( Y S X ) ) |
| 12 |
11
|
cnveqd |
|- ( ( ph /\ ( x = X /\ y = Y ) ) -> `' ( y S x ) = `' ( Y S X ) ) |
| 13 |
10 12
|
ineq12d |
|- ( ( ph /\ ( x = X /\ y = Y ) ) -> ( ( x S y ) i^i `' ( y S x ) ) = ( ( X S Y ) i^i `' ( Y S X ) ) ) |
| 14 |
|
ovex |
|- ( X S Y ) e. _V |
| 15 |
14
|
inex1 |
|- ( ( X S Y ) i^i `' ( Y S X ) ) e. _V |
| 16 |
15
|
a1i |
|- ( ph -> ( ( X S Y ) i^i `' ( Y S X ) ) e. _V ) |
| 17 |
7 13 4 5 16
|
ovmpod |
|- ( ph -> ( X N Y ) = ( ( X S Y ) i^i `' ( Y S X ) ) ) |