This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem thinccic

Description: In a thin category, two objects are isomorphic iff there are morphisms between them in both directions. (Contributed by Zhi Wang, 25-Sep-2024)

Ref Expression
Hypotheses thincsect.c 
|- ( ph -> C e. ThinCat )
thincsect.b 
|- B = ( Base ` C )
thincsect.x 
|- ( ph -> X e. B )
thincsect.y 
|- ( ph -> Y e. B )
thinciso.h 
|- H = ( Hom ` C )
Assertion thinccic 
|- ( ph -> ( X ( ~=c ` C ) Y <-> ( ( X H Y ) =/= (/) /\ ( Y H X ) =/= (/) ) ) )

Proof

Step Hyp Ref Expression
1 thincsect.c 
 |-  ( ph -> C e. ThinCat )
2 thincsect.b 
 |-  B = ( Base ` C )
3 thincsect.x 
 |-  ( ph -> X e. B )
4 thincsect.y 
 |-  ( ph -> Y e. B )
5 thinciso.h 
 |-  H = ( Hom ` C )
6 eqid 
 |-  ( Iso ` C ) = ( Iso ` C )
7 1 thinccd 
 |-  ( ph -> C e. Cat )
8 2 5 6 7 3 4 isohom 
 |-  ( ph -> ( X ( Iso ` C ) Y ) C_ ( X H Y ) )
9 8 sselda 
 |-  ( ( ph /\ f e. ( X ( Iso ` C ) Y ) ) -> f e. ( X H Y ) )
10 1 adantr 
 |-  ( ( ph /\ f e. ( X H Y ) ) -> C e. ThinCat )
11 3 adantr 
 |-  ( ( ph /\ f e. ( X H Y ) ) -> X e. B )
12 4 adantr 
 |-  ( ( ph /\ f e. ( X H Y ) ) -> Y e. B )
13 simpr 
 |-  ( ( ph /\ f e. ( X H Y ) ) -> f e. ( X H Y ) )
14 10 2 11 12 5 6 13 thinciso 
 |-  ( ( ph /\ f e. ( X H Y ) ) -> ( f e. ( X ( Iso ` C ) Y ) <-> ( Y H X ) =/= (/) ) )
15 9 14 biadanid 
 |-  ( ph -> ( f e. ( X ( Iso ` C ) Y ) <-> ( f e. ( X H Y ) /\ ( Y H X ) =/= (/) ) ) )
16 15 exbidv 
 |-  ( ph -> ( E. f f e. ( X ( Iso ` C ) Y ) <-> E. f ( f e. ( X H Y ) /\ ( Y H X ) =/= (/) ) ) )
17 6 2 7 3 4 cic 
 |-  ( ph -> ( X ( ~=c ` C ) Y <-> E. f f e. ( X ( Iso ` C ) Y ) ) )
18 n0 
 |-  ( ( X H Y ) =/= (/) <-> E. f f e. ( X H Y ) )
19 18 anbi1i 
 |-  ( ( ( X H Y ) =/= (/) /\ ( Y H X ) =/= (/) ) <-> ( E. f f e. ( X H Y ) /\ ( Y H X ) =/= (/) ) )
20 19.41v 
 |-  ( E. f ( f e. ( X H Y ) /\ ( Y H X ) =/= (/) ) <-> ( E. f f e. ( X H Y ) /\ ( Y H X ) =/= (/) ) )
21 19 20 bitr4i 
 |-  ( ( ( X H Y ) =/= (/) /\ ( Y H X ) =/= (/) ) <-> E. f ( f e. ( X H Y ) /\ ( Y H X ) =/= (/) ) )
22 21 a1i 
 |-  ( ph -> ( ( ( X H Y ) =/= (/) /\ ( Y H X ) =/= (/) ) <-> E. f ( f e. ( X H Y ) /\ ( Y H X ) =/= (/) ) ) )
23 16 17 22 3bitr4d 
 |-  ( ph -> ( X ( ~=c ` C ) Y <-> ( ( X H Y ) =/= (/) /\ ( Y H X ) =/= (/) ) ) )