Metamath Proof Explorer

Theorem isisod

Description: The predicate "is an isomorphism" (deduction form). (Contributed by Zhi Wang, 16-Sep-2025)

Ref Expression
Hypotheses isisod.b 
|- B = ( Base ` C )
isisod.h 
|- H = ( Hom ` C )
isisod.o 
|- .x. = ( comp ` C )
isisod.i 
|- I = ( Iso ` C )
isisod.1 
|- .1. = ( Id ` C )
isisod.c 
|- ( ph -> C e. Cat )
isisod.x 
|- ( ph -> X e. B )
isisod.y 
|- ( ph -> Y e. B )
isisod.f 
|- ( ph -> F e. ( X H Y ) )
isisod.g 
|- ( ph -> G e. ( Y H X ) )
isisod.gf 
|- ( ph -> ( G ( <. X , Y >. .x. X ) F ) = ( .1. ` X ) )
isisod.fg 
|- ( ph -> ( F ( <. Y , X >. .x. Y ) G ) = ( .1. ` Y ) )
Assertion isisod 
|- ( ph -> F e. ( X I Y ) )

Proof

Step Hyp Ref Expression
1 isisod.b 
 |-  B = ( Base ` C )
2 isisod.h 
 |-  H = ( Hom ` C )
3 isisod.o 
 |-  .x. = ( comp ` C )
4 isisod.i 
 |-  I = ( Iso ` C )
5 isisod.1 
 |-  .1. = ( Id ` C )
6 isisod.c 
 |-  ( ph -> C e. Cat )
7 isisod.x 
 |-  ( ph -> X e. B )
8 isisod.y 
 |-  ( ph -> Y e. B )
9 isisod.f 
 |-  ( ph -> F e. ( X H Y ) )
10 isisod.g 
 |-  ( ph -> G e. ( Y H X ) )
11 isisod.gf 
 |-  ( ph -> ( G ( <. X , Y >. .x. X ) F ) = ( .1. ` X ) )
12 isisod.fg 
 |-  ( ph -> ( F ( <. Y , X >. .x. Y ) G ) = ( .1. ` Y ) )
13 simpr 
 |-  ( ( ph /\ g = G ) -> g = G )
14 13 oveq1d 
 |-  ( ( ph /\ g = G ) -> ( g ( <. X , Y >. .x. X ) F ) = ( G ( <. X , Y >. .x. X ) F ) )
15 14 eqeq1d 
 |-  ( ( ph /\ g = G ) -> ( ( g ( <. X , Y >. .x. X ) F ) = ( .1. ` X ) <-> ( G ( <. X , Y >. .x. X ) F ) = ( .1. ` X ) ) )
16 13 oveq2d 
 |-  ( ( ph /\ g = G ) -> ( F ( <. Y , X >. .x. Y ) g ) = ( F ( <. Y , X >. .x. Y ) G ) )
17 16 eqeq1d 
 |-  ( ( ph /\ g = G ) -> ( ( F ( <. Y , X >. .x. Y ) g ) = ( .1. ` Y ) <-> ( F ( <. Y , X >. .x. Y ) G ) = ( .1. ` Y ) ) )
18 15 17 anbi12d 
 |-  ( ( ph /\ g = G ) -> ( ( ( g ( <. X , Y >. .x. X ) F ) = ( .1. ` X ) /\ ( F ( <. Y , X >. .x. Y ) g ) = ( .1. ` Y ) ) <-> ( ( G ( <. X , Y >. .x. X ) F ) = ( .1. ` X ) /\ ( F ( <. Y , X >. .x. Y ) G ) = ( .1. ` Y ) ) ) )
19 10 18 rspcedv 
 |-  ( ph -> ( ( ( G ( <. X , Y >. .x. X ) F ) = ( .1. ` X ) /\ ( F ( <. Y , X >. .x. Y ) G ) = ( .1. ` Y ) ) -> E. g e. ( Y H X ) ( ( g ( <. X , Y >. .x. X ) F ) = ( .1. ` X ) /\ ( F ( <. Y , X >. .x. Y ) g ) = ( .1. ` Y ) ) ) )
20 11 12 19 mp2and 
 |-  ( ph -> E. g e. ( Y H X ) ( ( g ( <. X , Y >. .x. X ) F ) = ( .1. ` X ) /\ ( F ( <. Y , X >. .x. Y ) g ) = ( .1. ` Y ) ) )
21 3 oveqi 
 |-  ( <. X , Y >. .x. X ) = ( <. X , Y >. ( comp ` C ) X )
22 3 oveqi 
 |-  ( <. Y , X >. .x. Y ) = ( <. Y , X >. ( comp ` C ) Y )
23 1 2 6 4 7 8 9 5 21 22 dfiso2 
 |-  ( ph -> ( F e. ( X I Y ) <-> E. g e. ( Y H X ) ( ( g ( <. X , Y >. .x. X ) F ) = ( .1. ` X ) /\ ( F ( <. Y , X >. .x. Y ) g ) = ( .1. ` Y ) ) ) )
24 20 23 mpbird 
 |-  ( ph -> F e. ( X I Y ) )