Metamath Proof Explorer

Theorem 2arwcat

Description: The condition for a structure with at most one object and at most two morphisms being a category. "2arwcat.2" to "2arwcat.5" are also necessary conditions if X , .0. , and .1. are all sets, due to catlid , catrid , and catcocl . (Contributed by Zhi Wang, 5-Nov-2025)

Ref Expression
Hypotheses 2arwcat.b 
|- ( ph -> { X } = ( Base ` C ) )
2arwcat.h 
|- ( ph -> H = ( Hom ` C ) )
2arwcat.x 
|- ( ph -> .x. = ( comp ` C ) )
2arwcat.1 
|- ( X H X ) = { .0. , .1. }
2arwcat.2 
|- ( ph -> ( .1. ( <. X , X >. .x. X ) .1. ) = .1. )
2arwcat.3 
|- ( ph -> ( .1. ( <. X , X >. .x. X ) .0. ) = .0. )
2arwcat.4 
|- ( ph -> ( .0. ( <. X , X >. .x. X ) .1. ) = .0. )
2arwcat.5 
|- ( ph -> ( .0. ( <. X , X >. .x. X ) .0. ) e. { .0. , .1. } )
Assertion 2arwcat 
|- ( ph -> ( C e. Cat /\ ( Id ` C ) = ( y e. { X } |-> .1. ) ) )

Proof

Step Hyp Ref Expression
1 2arwcat.b 
 |-  ( ph -> { X } = ( Base ` C ) )
2 2arwcat.h 
 |-  ( ph -> H = ( Hom ` C ) )
3 2arwcat.x 
 |-  ( ph -> .x. = ( comp ` C ) )
4 2arwcat.1 
 |-  ( X H X ) = { .0. , .1. }
5 2arwcat.2 
 |-  ( ph -> ( .1. ( <. X , X >. .x. X ) .1. ) = .1. )
6 2arwcat.3 
 |-  ( ph -> ( .1. ( <. X , X >. .x. X ) .0. ) = .0. )
7 2arwcat.4 
 |-  ( ph -> ( .0. ( <. X , X >. .x. X ) .1. ) = .0. )
8 2arwcat.5 
 |-  ( ph -> ( .0. ( <. X , X >. .x. X ) .0. ) e. { .0. , .1. } )
9 ovex 
 |-  ( .1. ( <. X , X >. .x. X ) .1. ) e. _V
10 5 9 eqeltrrdi 
 |-  ( ph -> .1. e. _V )
11 prid2g 
 |-  ( .1. e. _V -> .1. e. { .0. , .1. } )
12 10 11 syl 
 |-  ( ph -> .1. e. { .0. , .1. } )
13 12 4 eleqtrrdi 
 |-  ( ph -> .1. e. ( X H X ) )
14 df-ov 
 |-  ( X H X ) = ( H ` <. X , X >. )
15 2 fveq1d 
 |-  ( ph -> ( H ` <. X , X >. ) = ( ( Hom ` C ) ` <. X , X >. ) )
16 14 15 eqtrid 
 |-  ( ph -> ( X H X ) = ( ( Hom ` C ) ` <. X , X >. ) )
17 13 16 eleqtrd 
 |-  ( ph -> .1. e. ( ( Hom ` C ) ` <. X , X >. ) )
18 elfv2ex 
 |-  ( .1. e. ( ( Hom ` C ) ` <. X , X >. ) -> C e. _V )
19 17 18 syl 
 |-  ( ph -> C e. _V )
20 4 2arwcatlem1 
 |-  ( ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) /\ ( ( f = .0. \/ f = .1. ) /\ ( g = .0. \/ g = .1. ) /\ ( k = .0. \/ k = .1. ) ) ) <-> ( ( x e. { X } /\ y e. { X } ) /\ ( z e. { X } /\ w e. { X } ) /\ ( f e. ( x H y ) /\ g e. ( y H z ) /\ k e. ( z H w ) ) ) )
21 12 adantr 
 |-  ( ( ph /\ y e. { X } ) -> .1. e. { .0. , .1. } )
22 velsn 
 |-  ( y e. { X } <-> y = X )
23 id 
 |-  ( y = X -> y = X )
24 23 23 oveq12d 
 |-  ( y = X -> ( y H y ) = ( X H X ) )
25 24 4 eqtrdi 
 |-  ( y = X -> ( y H y ) = { .0. , .1. } )
26 22 25 sylbi 
 |-  ( y e. { X } -> ( y H y ) = { .0. , .1. } )
27 26 adantl 
 |-  ( ( ph /\ y e. { X } ) -> ( y H y ) = { .0. , .1. } )
28 21 27 eleqtrrd 
 |-  ( ( ph /\ y e. { X } ) -> .1. e. ( y H y ) )
29 simprll 
 |-  ( ( ph /\ ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) /\ ( ( f = .0. \/ f = .1. ) /\ ( g = .0. \/ g = .1. ) /\ ( k = .0. \/ k = .1. ) ) ) ) -> ( x = X /\ y = X ) )
30 29 simpld 
 |-  ( ( ph /\ ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) /\ ( ( f = .0. \/ f = .1. ) /\ ( g = .0. \/ g = .1. ) /\ ( k = .0. \/ k = .1. ) ) ) ) -> x = X )
31 29 simprd 
 |-  ( ( ph /\ ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) /\ ( ( f = .0. \/ f = .1. ) /\ ( g = .0. \/ g = .1. ) /\ ( k = .0. \/ k = .1. ) ) ) ) -> y = X )
32 simprr1 
 |-  ( ( ph /\ ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) /\ ( ( f = .0. \/ f = .1. ) /\ ( g = .0. \/ g = .1. ) /\ ( k = .0. \/ k = .1. ) ) ) ) -> ( f = .0. \/ f = .1. ) )
33 5 adantr 
 |-  ( ( ph /\ ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) /\ ( ( f = .0. \/ f = .1. ) /\ ( g = .0. \/ g = .1. ) /\ ( k = .0. \/ k = .1. ) ) ) ) -> ( .1. ( <. X , X >. .x. X ) .1. ) = .1. )
34 6 adantr 
 |-  ( ( ph /\ ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) /\ ( ( f = .0. \/ f = .1. ) /\ ( g = .0. \/ g = .1. ) /\ ( k = .0. \/ k = .1. ) ) ) ) -> ( .1. ( <. X , X >. .x. X ) .0. ) = .0. )
35 30 31 31 32 33 34 2arwcatlem2 
 |-  ( ( ph /\ ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) /\ ( ( f = .0. \/ f = .1. ) /\ ( g = .0. \/ g = .1. ) /\ ( k = .0. \/ k = .1. ) ) ) ) -> ( .1. ( <. x , y >. .x. y ) f ) = f )
36 simprlr 
 |-  ( ( ph /\ ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) /\ ( ( f = .0. \/ f = .1. ) /\ ( g = .0. \/ g = .1. ) /\ ( k = .0. \/ k = .1. ) ) ) ) -> ( z = X /\ w = X ) )
37 36 simpld 
 |-  ( ( ph /\ ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) /\ ( ( f = .0. \/ f = .1. ) /\ ( g = .0. \/ g = .1. ) /\ ( k = .0. \/ k = .1. ) ) ) ) -> z = X )
38 simprr2 
 |-  ( ( ph /\ ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) /\ ( ( f = .0. \/ f = .1. ) /\ ( g = .0. \/ g = .1. ) /\ ( k = .0. \/ k = .1. ) ) ) ) -> ( g = .0. \/ g = .1. ) )
39 7 adantr 
 |-  ( ( ph /\ ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) /\ ( ( f = .0. \/ f = .1. ) /\ ( g = .0. \/ g = .1. ) /\ ( k = .0. \/ k = .1. ) ) ) ) -> ( .0. ( <. X , X >. .x. X ) .1. ) = .0. )
40 31 31 37 38 33 39 2arwcatlem3 
 |-  ( ( ph /\ ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) /\ ( ( f = .0. \/ f = .1. ) /\ ( g = .0. \/ g = .1. ) /\ ( k = .0. \/ k = .1. ) ) ) ) -> ( g ( <. y , y >. .x. z ) .1. ) = g )
41 8 adantr 
 |-  ( ( ph /\ ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) /\ ( ( f = .0. \/ f = .1. ) /\ ( g = .0. \/ g = .1. ) /\ ( k = .0. \/ k = .1. ) ) ) ) -> ( .0. ( <. X , X >. .x. X ) .0. ) e. { .0. , .1. } )
42 30 31 37 32 33 39 34 41 38 2arwcatlem4 
 |-  ( ( ph /\ ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) /\ ( ( f = .0. \/ f = .1. ) /\ ( g = .0. \/ g = .1. ) /\ ( k = .0. \/ k = .1. ) ) ) ) -> ( g ( <. x , y >. .x. z ) f ) e. { .0. , .1. } )
43 30 37 oveq12d 
 |-  ( ( ph /\ ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) /\ ( ( f = .0. \/ f = .1. ) /\ ( g = .0. \/ g = .1. ) /\ ( k = .0. \/ k = .1. ) ) ) ) -> ( x H z ) = ( X H X ) )
44 43 4 eqtrdi 
 |-  ( ( ph /\ ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) /\ ( ( f = .0. \/ f = .1. ) /\ ( g = .0. \/ g = .1. ) /\ ( k = .0. \/ k = .1. ) ) ) ) -> ( x H z ) = { .0. , .1. } )
45 42 44 eleqtrrd 
 |-  ( ( ph /\ ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) /\ ( ( f = .0. \/ f = .1. ) /\ ( g = .0. \/ g = .1. ) /\ ( k = .0. \/ k = .1. ) ) ) ) -> ( g ( <. x , y >. .x. z ) f ) e. ( x H z ) )
46 6 7 8 2arwcatlem5 
 |-  ( ph -> ( ( .0. ( <. X , X >. .x. X ) .0. ) ( <. X , X >. .x. X ) .0. ) = ( .0. ( <. X , X >. .x. X ) ( .0. ( <. X , X >. .x. X ) .0. ) ) )
47 46 ad4antr 
 |-  ( ( ( ( ( ph /\ ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) /\ ( ( f = .0. \/ f = .1. ) /\ ( g = .0. \/ g = .1. ) /\ ( k = .0. \/ k = .1. ) ) ) ) /\ f = .0. ) /\ g = .0. ) /\ k = .0. ) -> ( ( .0. ( <. X , X >. .x. X ) .0. ) ( <. X , X >. .x. X ) .0. ) = ( .0. ( <. X , X >. .x. X ) ( .0. ( <. X , X >. .x. X ) .0. ) ) )
48 simpr 
 |-  ( ( ( ( ( ph /\ ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) /\ ( ( f = .0. \/ f = .1. ) /\ ( g = .0. \/ g = .1. ) /\ ( k = .0. \/ k = .1. ) ) ) ) /\ f = .0. ) /\ g = .0. ) /\ k = .0. ) -> k = .0. )
49 simplr 
 |-  ( ( ( ( ( ph /\ ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) /\ ( ( f = .0. \/ f = .1. ) /\ ( g = .0. \/ g = .1. ) /\ ( k = .0. \/ k = .1. ) ) ) ) /\ f = .0. ) /\ g = .0. ) /\ k = .0. ) -> g = .0. )
50 48 49 oveq12d 
 |-  ( ( ( ( ( ph /\ ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) /\ ( ( f = .0. \/ f = .1. ) /\ ( g = .0. \/ g = .1. ) /\ ( k = .0. \/ k = .1. ) ) ) ) /\ f = .0. ) /\ g = .0. ) /\ k = .0. ) -> ( k ( <. X , X >. .x. X ) g ) = ( .0. ( <. X , X >. .x. X ) .0. ) )
51 simpr 
 |-  ( ( ( ph /\ ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) /\ ( ( f = .0. \/ f = .1. ) /\ ( g = .0. \/ g = .1. ) /\ ( k = .0. \/ k = .1. ) ) ) ) /\ f = .0. ) -> f = .0. )
52 51 ad2antrr 
 |-  ( ( ( ( ( ph /\ ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) /\ ( ( f = .0. \/ f = .1. ) /\ ( g = .0. \/ g = .1. ) /\ ( k = .0. \/ k = .1. ) ) ) ) /\ f = .0. ) /\ g = .0. ) /\ k = .0. ) -> f = .0. )
53 50 52 oveq12d 
 |-  ( ( ( ( ( ph /\ ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) /\ ( ( f = .0. \/ f = .1. ) /\ ( g = .0. \/ g = .1. ) /\ ( k = .0. \/ k = .1. ) ) ) ) /\ f = .0. ) /\ g = .0. ) /\ k = .0. ) -> ( ( k ( <. X , X >. .x. X ) g ) ( <. X , X >. .x. X ) f ) = ( ( .0. ( <. X , X >. .x. X ) .0. ) ( <. X , X >. .x. X ) .0. ) )
54 49 52 oveq12d 
 |-  ( ( ( ( ( ph /\ ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) /\ ( ( f = .0. \/ f = .1. ) /\ ( g = .0. \/ g = .1. ) /\ ( k = .0. \/ k = .1. ) ) ) ) /\ f = .0. ) /\ g = .0. ) /\ k = .0. ) -> ( g ( <. X , X >. .x. X ) f ) = ( .0. ( <. X , X >. .x. X ) .0. ) )
55 48 54 oveq12d 
 |-  ( ( ( ( ( ph /\ ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) /\ ( ( f = .0. \/ f = .1. ) /\ ( g = .0. \/ g = .1. ) /\ ( k = .0. \/ k = .1. ) ) ) ) /\ f = .0. ) /\ g = .0. ) /\ k = .0. ) -> ( k ( <. X , X >. .x. X ) ( g ( <. X , X >. .x. X ) f ) ) = ( .0. ( <. X , X >. .x. X ) ( .0. ( <. X , X >. .x. X ) .0. ) ) )
56 47 53 55 3eqtr4d 
 |-  ( ( ( ( ( ph /\ ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) /\ ( ( f = .0. \/ f = .1. ) /\ ( g = .0. \/ g = .1. ) /\ ( k = .0. \/ k = .1. ) ) ) ) /\ f = .0. ) /\ g = .0. ) /\ k = .0. ) -> ( ( k ( <. X , X >. .x. X ) g ) ( <. X , X >. .x. X ) f ) = ( k ( <. X , X >. .x. X ) ( g ( <. X , X >. .x. X ) f ) ) )
57 eqidd 
 |-  ( ( ph /\ ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) /\ ( ( f = .0. \/ f = .1. ) /\ ( g = .0. \/ g = .1. ) /\ ( k = .0. \/ k = .1. ) ) ) ) -> X = X )
58 30 31 opeq12d 
 |-  ( ( ph /\ ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) /\ ( ( f = .0. \/ f = .1. ) /\ ( g = .0. \/ g = .1. ) /\ ( k = .0. \/ k = .1. ) ) ) ) -> <. x , y >. = <. X , X >. )
59 58 37 oveq12d 
 |-  ( ( ph /\ ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) /\ ( ( f = .0. \/ f = .1. ) /\ ( g = .0. \/ g = .1. ) /\ ( k = .0. \/ k = .1. ) ) ) ) -> ( <. x , y >. .x. z ) = ( <. X , X >. .x. X ) )
60 59 oveqd 
 |-  ( ( ph /\ ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) /\ ( ( f = .0. \/ f = .1. ) /\ ( g = .0. \/ g = .1. ) /\ ( k = .0. \/ k = .1. ) ) ) ) -> ( g ( <. x , y >. .x. z ) f ) = ( g ( <. X , X >. .x. X ) f ) )
61 60 42 eqeltrrd 
 |-  ( ( ph /\ ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) /\ ( ( f = .0. \/ f = .1. ) /\ ( g = .0. \/ g = .1. ) /\ ( k = .0. \/ k = .1. ) ) ) ) -> ( g ( <. X , X >. .x. X ) f ) e. { .0. , .1. } )
62 ovex 
 |-  ( g ( <. X , X >. .x. X ) f ) e. _V
63 62 elpr 
 |-  ( ( g ( <. X , X >. .x. X ) f ) e. { .0. , .1. } <-> ( ( g ( <. X , X >. .x. X ) f ) = .0. \/ ( g ( <. X , X >. .x. X ) f ) = .1. ) )
64 61 63 sylib 
 |-  ( ( ph /\ ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) /\ ( ( f = .0. \/ f = .1. ) /\ ( g = .0. \/ g = .1. ) /\ ( k = .0. \/ k = .1. ) ) ) ) -> ( ( g ( <. X , X >. .x. X ) f ) = .0. \/ ( g ( <. X , X >. .x. X ) f ) = .1. ) )
65 57 57 57 64 33 34 2arwcatlem2 
 |-  ( ( ph /\ ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) /\ ( ( f = .0. \/ f = .1. ) /\ ( g = .0. \/ g = .1. ) /\ ( k = .0. \/ k = .1. ) ) ) ) -> ( .1. ( <. X , X >. .x. X ) ( g ( <. X , X >. .x. X ) f ) ) = ( g ( <. X , X >. .x. X ) f ) )
66 65 ad3antrrr 
 |-  ( ( ( ( ( ph /\ ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) /\ ( ( f = .0. \/ f = .1. ) /\ ( g = .0. \/ g = .1. ) /\ ( k = .0. \/ k = .1. ) ) ) ) /\ f = .0. ) /\ g = .0. ) /\ k = .1. ) -> ( .1. ( <. X , X >. .x. X ) ( g ( <. X , X >. .x. X ) f ) ) = ( g ( <. X , X >. .x. X ) f ) )
67 simpr 
 |-  ( ( ( ( ( ph /\ ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) /\ ( ( f = .0. \/ f = .1. ) /\ ( g = .0. \/ g = .1. ) /\ ( k = .0. \/ k = .1. ) ) ) ) /\ f = .0. ) /\ g = .0. ) /\ k = .1. ) -> k = .1. )
68 67 oveq1d 
 |-  ( ( ( ( ( ph /\ ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) /\ ( ( f = .0. \/ f = .1. ) /\ ( g = .0. \/ g = .1. ) /\ ( k = .0. \/ k = .1. ) ) ) ) /\ f = .0. ) /\ g = .0. ) /\ k = .1. ) -> ( k ( <. X , X >. .x. X ) ( g ( <. X , X >. .x. X ) f ) ) = ( .1. ( <. X , X >. .x. X ) ( g ( <. X , X >. .x. X ) f ) ) )
69 67 oveq1d 
 |-  ( ( ( ( ( ph /\ ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) /\ ( ( f = .0. \/ f = .1. ) /\ ( g = .0. \/ g = .1. ) /\ ( k = .0. \/ k = .1. ) ) ) ) /\ f = .0. ) /\ g = .0. ) /\ k = .1. ) -> ( k ( <. X , X >. .x. X ) g ) = ( .1. ( <. X , X >. .x. X ) g ) )
70 57 57 57 38 33 34 2arwcatlem2 
 |-  ( ( ph /\ ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) /\ ( ( f = .0. \/ f = .1. ) /\ ( g = .0. \/ g = .1. ) /\ ( k = .0. \/ k = .1. ) ) ) ) -> ( .1. ( <. X , X >. .x. X ) g ) = g )
71 70 ad3antrrr 
 |-  ( ( ( ( ( ph /\ ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) /\ ( ( f = .0. \/ f = .1. ) /\ ( g = .0. \/ g = .1. ) /\ ( k = .0. \/ k = .1. ) ) ) ) /\ f = .0. ) /\ g = .0. ) /\ k = .1. ) -> ( .1. ( <. X , X >. .x. X ) g ) = g )
72 69 71 eqtrd 
 |-  ( ( ( ( ( ph /\ ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) /\ ( ( f = .0. \/ f = .1. ) /\ ( g = .0. \/ g = .1. ) /\ ( k = .0. \/ k = .1. ) ) ) ) /\ f = .0. ) /\ g = .0. ) /\ k = .1. ) -> ( k ( <. X , X >. .x. X ) g ) = g )
73 72 oveq1d 
 |-  ( ( ( ( ( ph /\ ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) /\ ( ( f = .0. \/ f = .1. ) /\ ( g = .0. \/ g = .1. ) /\ ( k = .0. \/ k = .1. ) ) ) ) /\ f = .0. ) /\ g = .0. ) /\ k = .1. ) -> ( ( k ( <. X , X >. .x. X ) g ) ( <. X , X >. .x. X ) f ) = ( g ( <. X , X >. .x. X ) f ) )
74 66 68 73 3eqtr4rd 
 |-  ( ( ( ( ( ph /\ ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) /\ ( ( f = .0. \/ f = .1. ) /\ ( g = .0. \/ g = .1. ) /\ ( k = .0. \/ k = .1. ) ) ) ) /\ f = .0. ) /\ g = .0. ) /\ k = .1. ) -> ( ( k ( <. X , X >. .x. X ) g ) ( <. X , X >. .x. X ) f ) = ( k ( <. X , X >. .x. X ) ( g ( <. X , X >. .x. X ) f ) ) )
75 simprr3 
 |-  ( ( ph /\ ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) /\ ( ( f = .0. \/ f = .1. ) /\ ( g = .0. \/ g = .1. ) /\ ( k = .0. \/ k = .1. ) ) ) ) -> ( k = .0. \/ k = .1. ) )
76 75 ad2antrr 
 |-  ( ( ( ( ph /\ ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) /\ ( ( f = .0. \/ f = .1. ) /\ ( g = .0. \/ g = .1. ) /\ ( k = .0. \/ k = .1. ) ) ) ) /\ f = .0. ) /\ g = .0. ) -> ( k = .0. \/ k = .1. ) )
77 56 74 76 mpjaodan 
 |-  ( ( ( ( ph /\ ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) /\ ( ( f = .0. \/ f = .1. ) /\ ( g = .0. \/ g = .1. ) /\ ( k = .0. \/ k = .1. ) ) ) ) /\ f = .0. ) /\ g = .0. ) -> ( ( k ( <. X , X >. .x. X ) g ) ( <. X , X >. .x. X ) f ) = ( k ( <. X , X >. .x. X ) ( g ( <. X , X >. .x. X ) f ) ) )
78 simpr 
 |-  ( ( ( ( ph /\ ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) /\ ( ( f = .0. \/ f = .1. ) /\ ( g = .0. \/ g = .1. ) /\ ( k = .0. \/ k = .1. ) ) ) ) /\ f = .0. ) /\ g = .1. ) -> g = .1. )
79 78 oveq2d 
 |-  ( ( ( ( ph /\ ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) /\ ( ( f = .0. \/ f = .1. ) /\ ( g = .0. \/ g = .1. ) /\ ( k = .0. \/ k = .1. ) ) ) ) /\ f = .0. ) /\ g = .1. ) -> ( k ( <. X , X >. .x. X ) g ) = ( k ( <. X , X >. .x. X ) .1. ) )
80 57 57 57 75 33 39 2arwcatlem3 
 |-  ( ( ph /\ ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) /\ ( ( f = .0. \/ f = .1. ) /\ ( g = .0. \/ g = .1. ) /\ ( k = .0. \/ k = .1. ) ) ) ) -> ( k ( <. X , X >. .x. X ) .1. ) = k )
81 80 ad2antrr 
 |-  ( ( ( ( ph /\ ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) /\ ( ( f = .0. \/ f = .1. ) /\ ( g = .0. \/ g = .1. ) /\ ( k = .0. \/ k = .1. ) ) ) ) /\ f = .0. ) /\ g = .1. ) -> ( k ( <. X , X >. .x. X ) .1. ) = k )
82 79 81 eqtrd 
 |-  ( ( ( ( ph /\ ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) /\ ( ( f = .0. \/ f = .1. ) /\ ( g = .0. \/ g = .1. ) /\ ( k = .0. \/ k = .1. ) ) ) ) /\ f = .0. ) /\ g = .1. ) -> ( k ( <. X , X >. .x. X ) g ) = k )
83 82 oveq1d 
 |-  ( ( ( ( ph /\ ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) /\ ( ( f = .0. \/ f = .1. ) /\ ( g = .0. \/ g = .1. ) /\ ( k = .0. \/ k = .1. ) ) ) ) /\ f = .0. ) /\ g = .1. ) -> ( ( k ( <. X , X >. .x. X ) g ) ( <. X , X >. .x. X ) f ) = ( k ( <. X , X >. .x. X ) f ) )
84 78 oveq1d 
 |-  ( ( ( ( ph /\ ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) /\ ( ( f = .0. \/ f = .1. ) /\ ( g = .0. \/ g = .1. ) /\ ( k = .0. \/ k = .1. ) ) ) ) /\ f = .0. ) /\ g = .1. ) -> ( g ( <. X , X >. .x. X ) f ) = ( .1. ( <. X , X >. .x. X ) f ) )
85 57 57 57 32 33 34 2arwcatlem2 
 |-  ( ( ph /\ ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) /\ ( ( f = .0. \/ f = .1. ) /\ ( g = .0. \/ g = .1. ) /\ ( k = .0. \/ k = .1. ) ) ) ) -> ( .1. ( <. X , X >. .x. X ) f ) = f )
86 85 ad2antrr 
 |-  ( ( ( ( ph /\ ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) /\ ( ( f = .0. \/ f = .1. ) /\ ( g = .0. \/ g = .1. ) /\ ( k = .0. \/ k = .1. ) ) ) ) /\ f = .0. ) /\ g = .1. ) -> ( .1. ( <. X , X >. .x. X ) f ) = f )
87 84 86 eqtrd 
 |-  ( ( ( ( ph /\ ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) /\ ( ( f = .0. \/ f = .1. ) /\ ( g = .0. \/ g = .1. ) /\ ( k = .0. \/ k = .1. ) ) ) ) /\ f = .0. ) /\ g = .1. ) -> ( g ( <. X , X >. .x. X ) f ) = f )
88 87 oveq2d 
 |-  ( ( ( ( ph /\ ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) /\ ( ( f = .0. \/ f = .1. ) /\ ( g = .0. \/ g = .1. ) /\ ( k = .0. \/ k = .1. ) ) ) ) /\ f = .0. ) /\ g = .1. ) -> ( k ( <. X , X >. .x. X ) ( g ( <. X , X >. .x. X ) f ) ) = ( k ( <. X , X >. .x. X ) f ) )
89 83 88 eqtr4d 
 |-  ( ( ( ( ph /\ ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) /\ ( ( f = .0. \/ f = .1. ) /\ ( g = .0. \/ g = .1. ) /\ ( k = .0. \/ k = .1. ) ) ) ) /\ f = .0. ) /\ g = .1. ) -> ( ( k ( <. X , X >. .x. X ) g ) ( <. X , X >. .x. X ) f ) = ( k ( <. X , X >. .x. X ) ( g ( <. X , X >. .x. X ) f ) ) )
90 38 adantr 
 |-  ( ( ( ph /\ ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) /\ ( ( f = .0. \/ f = .1. ) /\ ( g = .0. \/ g = .1. ) /\ ( k = .0. \/ k = .1. ) ) ) ) /\ f = .0. ) -> ( g = .0. \/ g = .1. ) )
91 77 89 90 mpjaodan 
 |-  ( ( ( ph /\ ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) /\ ( ( f = .0. \/ f = .1. ) /\ ( g = .0. \/ g = .1. ) /\ ( k = .0. \/ k = .1. ) ) ) ) /\ f = .0. ) -> ( ( k ( <. X , X >. .x. X ) g ) ( <. X , X >. .x. X ) f ) = ( k ( <. X , X >. .x. X ) ( g ( <. X , X >. .x. X ) f ) ) )
92 57 57 57 38 33 39 34 41 75 2arwcatlem4 
 |-  ( ( ph /\ ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) /\ ( ( f = .0. \/ f = .1. ) /\ ( g = .0. \/ g = .1. ) /\ ( k = .0. \/ k = .1. ) ) ) ) -> ( k ( <. X , X >. .x. X ) g ) e. { .0. , .1. } )
93 ovex 
 |-  ( k ( <. X , X >. .x. X ) g ) e. _V
94 93 elpr 
 |-  ( ( k ( <. X , X >. .x. X ) g ) e. { .0. , .1. } <-> ( ( k ( <. X , X >. .x. X ) g ) = .0. \/ ( k ( <. X , X >. .x. X ) g ) = .1. ) )
95 92 94 sylib 
 |-  ( ( ph /\ ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) /\ ( ( f = .0. \/ f = .1. ) /\ ( g = .0. \/ g = .1. ) /\ ( k = .0. \/ k = .1. ) ) ) ) -> ( ( k ( <. X , X >. .x. X ) g ) = .0. \/ ( k ( <. X , X >. .x. X ) g ) = .1. ) )
96 57 57 57 95 33 39 2arwcatlem3 
 |-  ( ( ph /\ ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) /\ ( ( f = .0. \/ f = .1. ) /\ ( g = .0. \/ g = .1. ) /\ ( k = .0. \/ k = .1. ) ) ) ) -> ( ( k ( <. X , X >. .x. X ) g ) ( <. X , X >. .x. X ) .1. ) = ( k ( <. X , X >. .x. X ) g ) )
97 96 adantr 
 |-  ( ( ( ph /\ ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) /\ ( ( f = .0. \/ f = .1. ) /\ ( g = .0. \/ g = .1. ) /\ ( k = .0. \/ k = .1. ) ) ) ) /\ f = .1. ) -> ( ( k ( <. X , X >. .x. X ) g ) ( <. X , X >. .x. X ) .1. ) = ( k ( <. X , X >. .x. X ) g ) )
98 simpr 
 |-  ( ( ( ph /\ ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) /\ ( ( f = .0. \/ f = .1. ) /\ ( g = .0. \/ g = .1. ) /\ ( k = .0. \/ k = .1. ) ) ) ) /\ f = .1. ) -> f = .1. )
99 98 oveq2d 
 |-  ( ( ( ph /\ ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) /\ ( ( f = .0. \/ f = .1. ) /\ ( g = .0. \/ g = .1. ) /\ ( k = .0. \/ k = .1. ) ) ) ) /\ f = .1. ) -> ( ( k ( <. X , X >. .x. X ) g ) ( <. X , X >. .x. X ) f ) = ( ( k ( <. X , X >. .x. X ) g ) ( <. X , X >. .x. X ) .1. ) )
100 98 oveq2d 
 |-  ( ( ( ph /\ ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) /\ ( ( f = .0. \/ f = .1. ) /\ ( g = .0. \/ g = .1. ) /\ ( k = .0. \/ k = .1. ) ) ) ) /\ f = .1. ) -> ( g ( <. X , X >. .x. X ) f ) = ( g ( <. X , X >. .x. X ) .1. ) )
101 57 57 57 38 33 39 2arwcatlem3 
 |-  ( ( ph /\ ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) /\ ( ( f = .0. \/ f = .1. ) /\ ( g = .0. \/ g = .1. ) /\ ( k = .0. \/ k = .1. ) ) ) ) -> ( g ( <. X , X >. .x. X ) .1. ) = g )
102 101 adantr 
 |-  ( ( ( ph /\ ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) /\ ( ( f = .0. \/ f = .1. ) /\ ( g = .0. \/ g = .1. ) /\ ( k = .0. \/ k = .1. ) ) ) ) /\ f = .1. ) -> ( g ( <. X , X >. .x. X ) .1. ) = g )
103 100 102 eqtrd 
 |-  ( ( ( ph /\ ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) /\ ( ( f = .0. \/ f = .1. ) /\ ( g = .0. \/ g = .1. ) /\ ( k = .0. \/ k = .1. ) ) ) ) /\ f = .1. ) -> ( g ( <. X , X >. .x. X ) f ) = g )
104 103 oveq2d 
 |-  ( ( ( ph /\ ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) /\ ( ( f = .0. \/ f = .1. ) /\ ( g = .0. \/ g = .1. ) /\ ( k = .0. \/ k = .1. ) ) ) ) /\ f = .1. ) -> ( k ( <. X , X >. .x. X ) ( g ( <. X , X >. .x. X ) f ) ) = ( k ( <. X , X >. .x. X ) g ) )
105 97 99 104 3eqtr4d 
 |-  ( ( ( ph /\ ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) /\ ( ( f = .0. \/ f = .1. ) /\ ( g = .0. \/ g = .1. ) /\ ( k = .0. \/ k = .1. ) ) ) ) /\ f = .1. ) -> ( ( k ( <. X , X >. .x. X ) g ) ( <. X , X >. .x. X ) f ) = ( k ( <. X , X >. .x. X ) ( g ( <. X , X >. .x. X ) f ) ) )
106 91 105 32 mpjaodan 
 |-  ( ( ph /\ ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) /\ ( ( f = .0. \/ f = .1. ) /\ ( g = .0. \/ g = .1. ) /\ ( k = .0. \/ k = .1. ) ) ) ) -> ( ( k ( <. X , X >. .x. X ) g ) ( <. X , X >. .x. X ) f ) = ( k ( <. X , X >. .x. X ) ( g ( <. X , X >. .x. X ) f ) ) )
107 36 simprd 
 |-  ( ( ph /\ ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) /\ ( ( f = .0. \/ f = .1. ) /\ ( g = .0. \/ g = .1. ) /\ ( k = .0. \/ k = .1. ) ) ) ) -> w = X )
108 58 107 oveq12d 
 |-  ( ( ph /\ ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) /\ ( ( f = .0. \/ f = .1. ) /\ ( g = .0. \/ g = .1. ) /\ ( k = .0. \/ k = .1. ) ) ) ) -> ( <. x , y >. .x. w ) = ( <. X , X >. .x. X ) )
109 31 37 opeq12d 
 |-  ( ( ph /\ ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) /\ ( ( f = .0. \/ f = .1. ) /\ ( g = .0. \/ g = .1. ) /\ ( k = .0. \/ k = .1. ) ) ) ) -> <. y , z >. = <. X , X >. )
110 109 107 oveq12d 
 |-  ( ( ph /\ ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) /\ ( ( f = .0. \/ f = .1. ) /\ ( g = .0. \/ g = .1. ) /\ ( k = .0. \/ k = .1. ) ) ) ) -> ( <. y , z >. .x. w ) = ( <. X , X >. .x. X ) )
111 110 oveqd 
 |-  ( ( ph /\ ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) /\ ( ( f = .0. \/ f = .1. ) /\ ( g = .0. \/ g = .1. ) /\ ( k = .0. \/ k = .1. ) ) ) ) -> ( k ( <. y , z >. .x. w ) g ) = ( k ( <. X , X >. .x. X ) g ) )
112 eqidd 
 |-  ( ( ph /\ ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) /\ ( ( f = .0. \/ f = .1. ) /\ ( g = .0. \/ g = .1. ) /\ ( k = .0. \/ k = .1. ) ) ) ) -> f = f )
113 108 111 112 oveq123d 
 |-  ( ( ph /\ ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) /\ ( ( f = .0. \/ f = .1. ) /\ ( g = .0. \/ g = .1. ) /\ ( k = .0. \/ k = .1. ) ) ) ) -> ( ( k ( <. y , z >. .x. w ) g ) ( <. x , y >. .x. w ) f ) = ( ( k ( <. X , X >. .x. X ) g ) ( <. X , X >. .x. X ) f ) )
114 30 37 opeq12d 
 |-  ( ( ph /\ ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) /\ ( ( f = .0. \/ f = .1. ) /\ ( g = .0. \/ g = .1. ) /\ ( k = .0. \/ k = .1. ) ) ) ) -> <. x , z >. = <. X , X >. )
115 114 107 oveq12d 
 |-  ( ( ph /\ ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) /\ ( ( f = .0. \/ f = .1. ) /\ ( g = .0. \/ g = .1. ) /\ ( k = .0. \/ k = .1. ) ) ) ) -> ( <. x , z >. .x. w ) = ( <. X , X >. .x. X ) )
116 eqidd 
 |-  ( ( ph /\ ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) /\ ( ( f = .0. \/ f = .1. ) /\ ( g = .0. \/ g = .1. ) /\ ( k = .0. \/ k = .1. ) ) ) ) -> k = k )
117 115 116 60 oveq123d 
 |-  ( ( ph /\ ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) /\ ( ( f = .0. \/ f = .1. ) /\ ( g = .0. \/ g = .1. ) /\ ( k = .0. \/ k = .1. ) ) ) ) -> ( k ( <. x , z >. .x. w ) ( g ( <. x , y >. .x. z ) f ) ) = ( k ( <. X , X >. .x. X ) ( g ( <. X , X >. .x. X ) f ) ) )
118 106 113 117 3eqtr4d 
 |-  ( ( ph /\ ( ( ( x = X /\ y = X ) /\ ( z = X /\ w = X ) ) /\ ( ( f = .0. \/ f = .1. ) /\ ( g = .0. \/ g = .1. ) /\ ( k = .0. \/ k = .1. ) ) ) ) -> ( ( k ( <. y , z >. .x. w ) g ) ( <. x , y >. .x. w ) f ) = ( k ( <. x , z >. .x. w ) ( g ( <. x , y >. .x. z ) f ) ) )
119 1 2 3 19 20 28 35 40 45 118 iscatd2 
 |-  ( ph -> ( C e. Cat /\ ( Id ` C ) = ( y e. { X } |-> .1. ) ) )