Metamath Proof Explorer

Theorem thincciso4

Description: Two isomorphic categories are either both thin or neither. Note that "thincciso2.u" is redundant thanks to elbasfv . (Contributed by Zhi Wang, 18-Oct-2025)

Ref Expression
Hypotheses thincciso2.c 
|- C = ( CatCat ` U )
thincciso2.b 
|- B = ( Base ` C )
thincciso2.u 
|- ( ph -> U e. V )
thincciso2.x 
|- ( ph -> X e. B )
thincciso2.y 
|- ( ph -> Y e. B )
thincciso4.i 
|- ( ph -> X ( ~=c ` C ) Y )
Assertion thincciso4 
|- ( ph -> ( X e. ThinCat <-> Y e. ThinCat ) )

Proof

Step Hyp Ref Expression
1 thincciso2.c 
 |-  C = ( CatCat ` U )
2 thincciso2.b 
 |-  B = ( Base ` C )
3 thincciso2.u 
 |-  ( ph -> U e. V )
4 thincciso2.x 
 |-  ( ph -> X e. B )
5 thincciso2.y 
 |-  ( ph -> Y e. B )
6 thincciso4.i 
 |-  ( ph -> X ( ~=c ` C ) Y )
7 eqid 
 |-  ( Iso ` C ) = ( Iso ` C )
8 1 catccat 
 |-  ( U e. V -> C e. Cat )
9 3 8 syl 
 |-  ( ph -> C e. Cat )
10 7 2 9 4 5 cic 
 |-  ( ph -> ( X ( ~=c ` C ) Y <-> E. f f e. ( X ( Iso ` C ) Y ) ) )
11 6 10 mpbid 
 |-  ( ph -> E. f f e. ( X ( Iso ` C ) Y ) )
12 11 adantr 
 |-  ( ( ph /\ X e. ThinCat ) -> E. f f e. ( X ( Iso ` C ) Y ) )
13 3 ad2antrr 
 |-  ( ( ( ph /\ X e. ThinCat ) /\ f e. ( X ( Iso ` C ) Y ) ) -> U e. V )
14 4 ad2antrr 
 |-  ( ( ( ph /\ X e. ThinCat ) /\ f e. ( X ( Iso ` C ) Y ) ) -> X e. B )
15 5 ad2antrr 
 |-  ( ( ( ph /\ X e. ThinCat ) /\ f e. ( X ( Iso ` C ) Y ) ) -> Y e. B )
16 simpr 
 |-  ( ( ( ph /\ X e. ThinCat ) /\ f e. ( X ( Iso ` C ) Y ) ) -> f e. ( X ( Iso ` C ) Y ) )
17 simplr 
 |-  ( ( ( ph /\ X e. ThinCat ) /\ f e. ( X ( Iso ` C ) Y ) ) -> X e. ThinCat )
18 1 2 13 14 15 7 16 17 thincciso3 
 |-  ( ( ( ph /\ X e. ThinCat ) /\ f e. ( X ( Iso ` C ) Y ) ) -> Y e. ThinCat )
19 12 18 exlimddv 
 |-  ( ( ph /\ X e. ThinCat ) -> Y e. ThinCat )
20 11 adantr 
 |-  ( ( ph /\ Y e. ThinCat ) -> E. f f e. ( X ( Iso ` C ) Y ) )
21 3 ad2antrr 
 |-  ( ( ( ph /\ Y e. ThinCat ) /\ f e. ( X ( Iso ` C ) Y ) ) -> U e. V )
22 4 ad2antrr 
 |-  ( ( ( ph /\ Y e. ThinCat ) /\ f e. ( X ( Iso ` C ) Y ) ) -> X e. B )
23 5 ad2antrr 
 |-  ( ( ( ph /\ Y e. ThinCat ) /\ f e. ( X ( Iso ` C ) Y ) ) -> Y e. B )
24 simpr 
 |-  ( ( ( ph /\ Y e. ThinCat ) /\ f e. ( X ( Iso ` C ) Y ) ) -> f e. ( X ( Iso ` C ) Y ) )
25 simplr 
 |-  ( ( ( ph /\ Y e. ThinCat ) /\ f e. ( X ( Iso ` C ) Y ) ) -> Y e. ThinCat )
26 1 2 21 22 23 7 24 25 thincciso2 
 |-  ( ( ( ph /\ Y e. ThinCat ) /\ f e. ( X ( Iso ` C ) Y ) ) -> X e. ThinCat )
27 20 26 exlimddv 
 |-  ( ( ph /\ Y e. ThinCat ) -> X e. ThinCat )
28 19 27 impbida 
 |-  ( ph -> ( X e. ThinCat <-> Y e. ThinCat ) )