Step |
Hyp |
Ref |
Expression |
1 |
|
inveq.b |
|- B = ( Base ` C ) |
2 |
|
inveq.n |
|- N = ( Inv ` C ) |
3 |
|
inveq.c |
|- ( ph -> C e. Cat ) |
4 |
|
inveq.x |
|- ( ph -> X e. B ) |
5 |
|
inveq.y |
|- ( ph -> Y e. B ) |
6 |
|
eqid |
|- ( Sect ` C ) = ( Sect ` C ) |
7 |
3
|
adantr |
|- ( ( ph /\ ( F ( X N Y ) G /\ F ( X N Y ) K ) ) -> C e. Cat ) |
8 |
5
|
adantr |
|- ( ( ph /\ ( F ( X N Y ) G /\ F ( X N Y ) K ) ) -> Y e. B ) |
9 |
4
|
adantr |
|- ( ( ph /\ ( F ( X N Y ) G /\ F ( X N Y ) K ) ) -> X e. B ) |
10 |
1 2 3 4 5 6
|
isinv |
|- ( ph -> ( F ( X N Y ) G <-> ( F ( X ( Sect ` C ) Y ) G /\ G ( Y ( Sect ` C ) X ) F ) ) ) |
11 |
|
simpr |
|- ( ( F ( X ( Sect ` C ) Y ) G /\ G ( Y ( Sect ` C ) X ) F ) -> G ( Y ( Sect ` C ) X ) F ) |
12 |
10 11
|
syl6bi |
|- ( ph -> ( F ( X N Y ) G -> G ( Y ( Sect ` C ) X ) F ) ) |
13 |
12
|
com12 |
|- ( F ( X N Y ) G -> ( ph -> G ( Y ( Sect ` C ) X ) F ) ) |
14 |
13
|
adantr |
|- ( ( F ( X N Y ) G /\ F ( X N Y ) K ) -> ( ph -> G ( Y ( Sect ` C ) X ) F ) ) |
15 |
14
|
impcom |
|- ( ( ph /\ ( F ( X N Y ) G /\ F ( X N Y ) K ) ) -> G ( Y ( Sect ` C ) X ) F ) |
16 |
1 2 3 4 5 6
|
isinv |
|- ( ph -> ( F ( X N Y ) K <-> ( F ( X ( Sect ` C ) Y ) K /\ K ( Y ( Sect ` C ) X ) F ) ) ) |
17 |
|
simpl |
|- ( ( F ( X ( Sect ` C ) Y ) K /\ K ( Y ( Sect ` C ) X ) F ) -> F ( X ( Sect ` C ) Y ) K ) |
18 |
16 17
|
syl6bi |
|- ( ph -> ( F ( X N Y ) K -> F ( X ( Sect ` C ) Y ) K ) ) |
19 |
18
|
adantld |
|- ( ph -> ( ( F ( X N Y ) G /\ F ( X N Y ) K ) -> F ( X ( Sect ` C ) Y ) K ) ) |
20 |
19
|
imp |
|- ( ( ph /\ ( F ( X N Y ) G /\ F ( X N Y ) K ) ) -> F ( X ( Sect ` C ) Y ) K ) |
21 |
1 6 7 8 9 15 20
|
sectcan |
|- ( ( ph /\ ( F ( X N Y ) G /\ F ( X N Y ) K ) ) -> G = K ) |
22 |
21
|
ex |
|- ( ph -> ( ( F ( X N Y ) G /\ F ( X N Y ) K ) -> G = K ) ) |