Metamath Proof Explorer

Theorem isthincd2

Description: The predicate " C is a thin category" without knowing C is a category (deduction form). The identity arrow operator is also provided as a byproduct. (Contributed by Zhi Wang, 17-Sep-2024)

Ref Expression
Hypotheses isthincd.b 
|- ( ph -> B = ( Base ` C ) )
isthincd.h 
|- ( ph -> H = ( Hom ` C ) )
isthincd.t 
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> E* f f e. ( x H y ) )
isthincd2.o 
|- ( ph -> .x. = ( comp ` C ) )
isthincd2.c 
|- ( ph -> C e. V )
isthincd2.ps 
|- ( ps <-> ( ( x e. B /\ y e. B /\ z e. B ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) ) ) )
isthincd2.1 
|- ( ( ph /\ y e. B ) -> .1. e. ( y H y ) )
isthincd2.2 
|- ( ( ph /\ ps ) -> ( g ( <. x , y >. .x. z ) f ) e. ( x H z ) )
Assertion isthincd2 
|- ( ph -> ( C e. ThinCat /\ ( Id ` C ) = ( y e. B |-> .1. ) ) )

Proof

Step Hyp Ref Expression
1 isthincd.b 
 |-  ( ph -> B = ( Base ` C ) )
2 isthincd.h 
 |-  ( ph -> H = ( Hom ` C ) )
3 isthincd.t 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> E* f f e. ( x H y ) )
4 isthincd2.o 
 |-  ( ph -> .x. = ( comp ` C ) )
5 isthincd2.c 
 |-  ( ph -> C e. V )
6 isthincd2.ps 
 |-  ( ps <-> ( ( x e. B /\ y e. B /\ z e. B ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) ) ) )
7 isthincd2.1 
 |-  ( ( ph /\ y e. B ) -> .1. e. ( y H y ) )
8 isthincd2.2 
 |-  ( ( ph /\ ps ) -> ( g ( <. x , y >. .x. z ) f ) e. ( x H z ) )
9 3an4anass 
 |-  ( ( ( x e. B /\ y e. B /\ z e. B ) /\ w e. B ) <-> ( ( x e. B /\ y e. B ) /\ ( z e. B /\ w e. B ) ) )
10 9 anbi1i 
 |-  ( ( ( ( x e. B /\ y e. B /\ z e. B ) /\ w e. B ) /\ ( ( f e. ( x H y ) /\ g e. ( y H z ) ) /\ k e. ( z H w ) ) ) <-> ( ( ( x e. B /\ y e. B ) /\ ( z e. B /\ w e. B ) ) /\ ( ( f e. ( x H y ) /\ g e. ( y H z ) ) /\ k e. ( z H w ) ) ) )
11 6 3anbi1i 
 |-  ( ( ps /\ w e. B /\ k e. ( z H w ) ) <-> ( ( ( x e. B /\ y e. B /\ z e. B ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) ) ) /\ w e. B /\ k e. ( z H w ) ) )
12 3anass 
 |-  ( ( ( ( x e. B /\ y e. B /\ z e. B ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) ) ) /\ w e. B /\ k e. ( z H w ) ) <-> ( ( ( x e. B /\ y e. B /\ z e. B ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) ) ) /\ ( w e. B /\ k e. ( z H w ) ) ) )
13 an4 
 |-  ( ( ( ( x e. B /\ y e. B /\ z e. B ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) ) ) /\ ( w e. B /\ k e. ( z H w ) ) ) <-> ( ( ( x e. B /\ y e. B /\ z e. B ) /\ w e. B ) /\ ( ( f e. ( x H y ) /\ g e. ( y H z ) ) /\ k e. ( z H w ) ) ) )
14 11 12 13 3bitri 
 |-  ( ( ps /\ w e. B /\ k e. ( z H w ) ) <-> ( ( ( x e. B /\ y e. B /\ z e. B ) /\ w e. B ) /\ ( ( f e. ( x H y ) /\ g e. ( y H z ) ) /\ k e. ( z H w ) ) ) )
15 df-3an 
 |-  ( ( f e. ( x H y ) /\ g e. ( y H z ) /\ k e. ( z H w ) ) <-> ( ( f e. ( x H y ) /\ g e. ( y H z ) ) /\ k e. ( z H w ) ) )
16 15 anbi2i 
 |-  ( ( ( ( x e. B /\ y e. B ) /\ ( z e. B /\ w e. B ) ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) /\ k e. ( z H w ) ) ) <-> ( ( ( x e. B /\ y e. B ) /\ ( z e. B /\ w e. B ) ) /\ ( ( f e. ( x H y ) /\ g e. ( y H z ) ) /\ k e. ( z H w ) ) ) )
17 10 14 16 3bitr4i 
 |-  ( ( ps /\ w e. B /\ k e. ( z H w ) ) <-> ( ( ( x e. B /\ y e. B ) /\ ( z e. B /\ w e. B ) ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) /\ k e. ( z H w ) ) ) )
18 df-3an 
 |-  ( ( ( x e. B /\ y e. B ) /\ ( z e. B /\ w e. B ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) /\ k e. ( z H w ) ) ) <-> ( ( ( x e. B /\ y e. B ) /\ ( z e. B /\ w e. B ) ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) /\ k e. ( z H w ) ) ) )
19 17 18 bitr4i 
 |-  ( ( ps /\ w e. B /\ k e. ( z H w ) ) <-> ( ( x e. B /\ y e. B ) /\ ( z e. B /\ w e. B ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) /\ k e. ( z H w ) ) ) )
20 simpr1l 
 |-  ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. B /\ w e. B ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) /\ k e. ( z H w ) ) ) ) -> x e. B )
21 simpr1r 
 |-  ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. B /\ w e. B ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) /\ k e. ( z H w ) ) ) ) -> y e. B )
22 simpr31 
 |-  ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. B /\ w e. B ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) /\ k e. ( z H w ) ) ) ) -> f e. ( x H y ) )
23 21 7 syldan 
 |-  ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. B /\ w e. B ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) /\ k e. ( z H w ) ) ) ) -> .1. e. ( y H y ) )
24 6 bianass 
 |-  ( ( ph /\ ps ) <-> ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) ) ) )
25 24 8 sylbir 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) ) ) -> ( g ( <. x , y >. .x. z ) f ) e. ( x H z ) )
26 25 ralrimivva 
 |-  ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) -> A. f e. ( x H y ) A. g e. ( y H z ) ( g ( <. x , y >. .x. z ) f ) e. ( x H z ) )
27 26 ralrimivvva 
 |-  ( ph -> A. x e. B A. y e. B A. z e. B A. f e. ( x H y ) A. g e. ( y H z ) ( g ( <. x , y >. .x. z ) f ) e. ( x H z ) )
28 27 adantr 
 |-  ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. B /\ w e. B ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) /\ k e. ( z H w ) ) ) ) -> A. x e. B A. y e. B A. z e. B A. f e. ( x H y ) A. g e. ( y H z ) ( g ( <. x , y >. .x. z ) f ) e. ( x H z ) )
29 20 21 21 22 23 28 isthincd2lem2 
 |-  ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. B /\ w e. B ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) /\ k e. ( z H w ) ) ) ) -> ( .1. ( <. x , y >. .x. y ) f ) e. ( x H y ) )
30 3 ralrimivva 
 |-  ( ph -> A. x e. B A. y e. B E* f f e. ( x H y ) )
31 30 adantr 
 |-  ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. B /\ w e. B ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) /\ k e. ( z H w ) ) ) ) -> A. x e. B A. y e. B E* f f e. ( x H y ) )
32 20 21 29 22 31 isthincd2lem1 
 |-  ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. B /\ w e. B ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) /\ k e. ( z H w ) ) ) ) -> ( .1. ( <. x , y >. .x. y ) f ) = f )
33 19 32 sylan2b 
 |-  ( ( ph /\ ( ps /\ w e. B /\ k e. ( z H w ) ) ) -> ( .1. ( <. x , y >. .x. y ) f ) = f )
34 simpr2l 
 |-  ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. B /\ w e. B ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) /\ k e. ( z H w ) ) ) ) -> z e. B )
35 simpr32 
 |-  ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. B /\ w e. B ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) /\ k e. ( z H w ) ) ) ) -> g e. ( y H z ) )
36 21 21 34 23 35 28 isthincd2lem2 
 |-  ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. B /\ w e. B ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) /\ k e. ( z H w ) ) ) ) -> ( g ( <. y , y >. .x. z ) .1. ) e. ( y H z ) )
37 21 34 36 35 31 isthincd2lem1 
 |-  ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. B /\ w e. B ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) /\ k e. ( z H w ) ) ) ) -> ( g ( <. y , y >. .x. z ) .1. ) = g )
38 19 37 sylan2b 
 |-  ( ( ph /\ ( ps /\ w e. B /\ k e. ( z H w ) ) ) -> ( g ( <. y , y >. .x. z ) .1. ) = g )
39 8 3ad2antr1 
 |-  ( ( ph /\ ( ps /\ w e. B /\ k e. ( z H w ) ) ) -> ( g ( <. x , y >. .x. z ) f ) e. ( x H z ) )
40 simpr2r 
 |-  ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. B /\ w e. B ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) /\ k e. ( z H w ) ) ) ) -> w e. B )
41 simpr33 
 |-  ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. B /\ w e. B ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) /\ k e. ( z H w ) ) ) ) -> k e. ( z H w ) )
42 21 34 40 35 41 28 isthincd2lem2 
 |-  ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. B /\ w e. B ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) /\ k e. ( z H w ) ) ) ) -> ( k ( <. y , z >. .x. w ) g ) e. ( y H w ) )
43 20 21 40 22 42 28 isthincd2lem2 
 |-  ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. B /\ w e. B ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) /\ k e. ( z H w ) ) ) ) -> ( ( k ( <. y , z >. .x. w ) g ) ( <. x , y >. .x. w ) f ) e. ( x H w ) )
44 19 39 sylan2br 
 |-  ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. B /\ w e. B ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) /\ k e. ( z H w ) ) ) ) -> ( g ( <. x , y >. .x. z ) f ) e. ( x H z ) )
45 20 34 40 44 41 28 isthincd2lem2 
 |-  ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. B /\ w e. B ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) /\ k e. ( z H w ) ) ) ) -> ( k ( <. x , z >. .x. w ) ( g ( <. x , y >. .x. z ) f ) ) e. ( x H w ) )
46 20 40 43 45 31 isthincd2lem1 
 |-  ( ( ph /\ ( ( x e. B /\ y e. B ) /\ ( z e. B /\ w e. B ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) /\ k e. ( z H w ) ) ) ) -> ( ( k ( <. y , z >. .x. w ) g ) ( <. x , y >. .x. w ) f ) = ( k ( <. x , z >. .x. w ) ( g ( <. x , y >. .x. z ) f ) ) )
47 19 46 sylan2b 
 |-  ( ( ph /\ ( ps /\ w e. B /\ k e. ( z H w ) ) ) -> ( ( k ( <. y , z >. .x. w ) g ) ( <. x , y >. .x. w ) f ) = ( k ( <. x , z >. .x. w ) ( g ( <. x , y >. .x. z ) f ) ) )
48 1 2 4 5 19 7 33 38 39 47 iscatd2 
 |-  ( ph -> ( C e. Cat /\ ( Id ` C ) = ( y e. B |-> .1. ) ) )
49 48 simpld 
 |-  ( ph -> C e. Cat )
50 1 2 3 49 isthincd 
 |-  ( ph -> C e. ThinCat )
51 48 simprd 
 |-  ( ph -> ( Id ` C ) = ( y e. B |-> .1. ) )
52 50 51 jca 
 |-  ( ph -> ( C e. ThinCat /\ ( Id ` C ) = ( y e. B |-> .1. ) ) )