Metamath Proof Explorer

Theorem isoval

Description: The isomorphisms are the domain of the inverse relation. (Contributed by Mario Carneiro, 2-Jan-2017) (Proof shortened by AV, 21-May-2020)

Ref Expression
Hypotheses invfval.b 
|- B = ( Base ` C )
invfval.n 
|- N = ( Inv ` C )
invfval.c 
|- ( ph -> C e. Cat )
invfval.x 
|- ( ph -> X e. B )
invfval.y 
|- ( ph -> Y e. B )
isoval.n 
|- I = ( Iso ` C )
Assertion isoval 
|- ( ph -> ( X I Y ) = dom ( X N Y ) )

Proof

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 isoval.n 
 |-  I = ( Iso ` C )
7 isofval 
 |-  ( C e. Cat -> ( Iso ` C ) = ( ( z e. _V |-> dom z ) o. ( Inv ` C ) ) )
8 3 7 syl 
 |-  ( ph -> ( Iso ` C ) = ( ( z e. _V |-> dom z ) o. ( Inv ` C ) ) )
9 2 coeq2i 
 |-  ( ( z e. _V |-> dom z ) o. N ) = ( ( z e. _V |-> dom z ) o. ( Inv ` C ) )
10 8 6 9 3eqtr4g 
 |-  ( ph -> I = ( ( z e. _V |-> dom z ) o. N ) )
11 10 oveqd 
 |-  ( ph -> ( X I Y ) = ( X ( ( z e. _V |-> dom z ) o. N ) Y ) )
12 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 ) ) )
13 ovex 
 |-  ( x ( Sect ` C ) y ) e. _V
14 13 inex1 
 |-  ( ( x ( Sect ` C ) y ) i^i `' ( y ( Sect ` C ) x ) ) e. _V
15 12 14 fnmpoi 
 |-  ( x e. B , y e. B |-> ( ( x ( Sect ` C ) y ) i^i `' ( y ( Sect ` C ) x ) ) ) Fn ( B X. B )
16 eqid 
 |-  ( Sect ` C ) = ( Sect ` C )
17 1 2 3 4 5 16 invffval 
 |-  ( ph -> N = ( x e. B , y e. B |-> ( ( x ( Sect ` C ) y ) i^i `' ( y ( Sect ` C ) x ) ) ) )
18 17 fneq1d 
 |-  ( ph -> ( N Fn ( B X. B ) <-> ( x e. B , y e. B |-> ( ( x ( Sect ` C ) y ) i^i `' ( y ( Sect ` C ) x ) ) ) Fn ( B X. B ) ) )
19 15 18 mpbiri 
 |-  ( ph -> N Fn ( B X. B ) )
20 4 5 opelxpd 
 |-  ( ph -> <. X , Y >. e. ( B X. B ) )
21 fvco2 
 |-  ( ( N Fn ( B X. B ) /\ <. X , Y >. e. ( B X. B ) ) -> ( ( ( z e. _V |-> dom z ) o. N ) ` <. X , Y >. ) = ( ( z e. _V |-> dom z ) ` ( N ` <. X , Y >. ) ) )
22 19 20 21 syl2anc 
 |-  ( ph -> ( ( ( z e. _V |-> dom z ) o. N ) ` <. X , Y >. ) = ( ( z e. _V |-> dom z ) ` ( N ` <. X , Y >. ) ) )
23 df-ov 
 |-  ( X ( ( z e. _V |-> dom z ) o. N ) Y ) = ( ( ( z e. _V |-> dom z ) o. N ) ` <. X , Y >. )
24 ovex 
 |-  ( X N Y ) e. _V
25 dmeq 
 |-  ( z = ( X N Y ) -> dom z = dom ( X N Y ) )
26 eqid 
 |-  ( z e. _V |-> dom z ) = ( z e. _V |-> dom z )
27 24 dmex 
 |-  dom ( X N Y ) e. _V
28 25 26 27 fvmpt 
 |-  ( ( X N Y ) e. _V -> ( ( z e. _V |-> dom z ) ` ( X N Y ) ) = dom ( X N Y ) )
29 24 28 ax-mp 
 |-  ( ( z e. _V |-> dom z ) ` ( X N Y ) ) = dom ( X N Y )
30 df-ov 
 |-  ( X N Y ) = ( N ` <. X , Y >. )
31 30 fveq2i 
 |-  ( ( z e. _V |-> dom z ) ` ( X N Y ) ) = ( ( z e. _V |-> dom z ) ` ( N ` <. X , Y >. ) )
32 29 31 eqtr3i 
 |-  dom ( X N Y ) = ( ( z e. _V |-> dom z ) ` ( N ` <. X , Y >. ) )
33 22 23 32 3eqtr4g 
 |-  ( ph -> ( X ( ( z e. _V |-> dom z ) o. N ) Y ) = dom ( X N Y ) )
34 11 33 eqtrd 
 |-  ( ph -> ( X I Y ) = dom ( X N Y ) )