Metamath Proof Explorer

Theorem cat1

Description: The definition of category df-cat does not impose pairwise disjoint hom-sets as required in Axiom CAT 1 in Lang p. 53. See setc2obas and setc2ohom for a counterexample. For a version with pairwise disjoint hom-sets, see df-homa and its subsection. (Contributed by Zhi Wang, 15-Sep-2024)

Ref Expression
Assertion cat1 
|- E. c e. Cat [. ( Base ` c ) / b ]. [. ( Hom ` c ) / h ]. -. A. x e. b A. y e. b A. z e. b A. w e. b ( ( ( x h y ) i^i ( z h w ) ) =/= (/) -> ( x = z /\ y = w ) )

Proof

Step Hyp Ref Expression
1 2on 
 |-  2o e. On
2 eqid 
 |-  ( SetCat ` 2o ) = ( SetCat ` 2o )
3 2 setccat 
 |-  ( 2o e. On -> ( SetCat ` 2o ) e. Cat )
4 1 3 ax-mp 
 |-  ( SetCat ` 2o ) e. Cat
5 1 a1i 
 |-  ( T. -> 2o e. On )
6 eqid 
 |-  ( Base ` ( SetCat ` 2o ) ) = ( Base ` ( SetCat ` 2o ) )
7 eqid 
 |-  ( Hom ` ( SetCat ` 2o ) ) = ( Hom ` ( SetCat ` 2o ) )
8 0ex 
 |-  (/) e. _V
9 8 prid1 
 |-  (/) e. { (/) , { (/) } }
10 df2o2 
 |-  2o = { (/) , { (/) } }
11 9 10 eleqtrri 
 |-  (/) e. 2o
12 11 a1i 
 |-  ( T. -> (/) e. 2o )
13 p0ex 
 |-  { (/) } e. _V
14 13 prid2 
 |-  { (/) } e. { (/) , { (/) } }
15 14 10 eleqtrri 
 |-  { (/) } e. 2o
16 15 a1i 
 |-  ( T. -> { (/) } e. 2o )
17 0nep0 
 |-  (/) =/= { (/) }
18 17 a1i 
 |-  ( T. -> (/) =/= { (/) } )
19 2 5 6 7 12 16 18 cat1lem 
 |-  ( T. -> E. x e. ( Base ` ( SetCat ` 2o ) ) E. y e. ( Base ` ( SetCat ` 2o ) ) E. z e. ( Base ` ( SetCat ` 2o ) ) E. w e. ( Base ` ( SetCat ` 2o ) ) ( ( ( x ( Hom ` ( SetCat ` 2o ) ) y ) i^i ( z ( Hom ` ( SetCat ` 2o ) ) w ) ) =/= (/) /\ -. ( x = z /\ y = w ) ) )
20 19 mptru 
 |-  E. x e. ( Base ` ( SetCat ` 2o ) ) E. y e. ( Base ` ( SetCat ` 2o ) ) E. z e. ( Base ` ( SetCat ` 2o ) ) E. w e. ( Base ` ( SetCat ` 2o ) ) ( ( ( x ( Hom ` ( SetCat ` 2o ) ) y ) i^i ( z ( Hom ` ( SetCat ` 2o ) ) w ) ) =/= (/) /\ -. ( x = z /\ y = w ) )
21 fvexd 
 |-  ( c = ( SetCat ` 2o ) -> ( Base ` c ) e. _V )
22 fveq2 
 |-  ( c = ( SetCat ` 2o ) -> ( Base ` c ) = ( Base ` ( SetCat ` 2o ) ) )
23 fvexd 
 |-  ( ( c = ( SetCat ` 2o ) /\ b = ( Base ` ( SetCat ` 2o ) ) ) -> ( Hom ` c ) e. _V )
24 fveq2 
 |-  ( c = ( SetCat ` 2o ) -> ( Hom ` c ) = ( Hom ` ( SetCat ` 2o ) ) )
25 24 adantr 
 |-  ( ( c = ( SetCat ` 2o ) /\ b = ( Base ` ( SetCat ` 2o ) ) ) -> ( Hom ` c ) = ( Hom ` ( SetCat ` 2o ) ) )
26 oveq 
 |-  ( h = ( Hom ` ( SetCat ` 2o ) ) -> ( x h y ) = ( x ( Hom ` ( SetCat ` 2o ) ) y ) )
27 oveq 
 |-  ( h = ( Hom ` ( SetCat ` 2o ) ) -> ( z h w ) = ( z ( Hom ` ( SetCat ` 2o ) ) w ) )
28 26 27 ineq12d 
 |-  ( h = ( Hom ` ( SetCat ` 2o ) ) -> ( ( x h y ) i^i ( z h w ) ) = ( ( x ( Hom ` ( SetCat ` 2o ) ) y ) i^i ( z ( Hom ` ( SetCat ` 2o ) ) w ) ) )
29 28 neeq1d 
 |-  ( h = ( Hom ` ( SetCat ` 2o ) ) -> ( ( ( x h y ) i^i ( z h w ) ) =/= (/) <-> ( ( x ( Hom ` ( SetCat ` 2o ) ) y ) i^i ( z ( Hom ` ( SetCat ` 2o ) ) w ) ) =/= (/) ) )
30 29 anbi1d 
 |-  ( h = ( Hom ` ( SetCat ` 2o ) ) -> ( ( ( ( x h y ) i^i ( z h w ) ) =/= (/) /\ -. ( x = z /\ y = w ) ) <-> ( ( ( x ( Hom ` ( SetCat ` 2o ) ) y ) i^i ( z ( Hom ` ( SetCat ` 2o ) ) w ) ) =/= (/) /\ -. ( x = z /\ y = w ) ) ) )
31 30 2rexbidv 
 |-  ( h = ( Hom ` ( SetCat ` 2o ) ) -> ( E. z e. b E. w e. b ( ( ( x h y ) i^i ( z h w ) ) =/= (/) /\ -. ( x = z /\ y = w ) ) <-> E. z e. b E. w e. b ( ( ( x ( Hom ` ( SetCat ` 2o ) ) y ) i^i ( z ( Hom ` ( SetCat ` 2o ) ) w ) ) =/= (/) /\ -. ( x = z /\ y = w ) ) ) )
32 31 2rexbidv 
 |-  ( h = ( Hom ` ( SetCat ` 2o ) ) -> ( E. x e. b E. y e. b E. z e. b E. w e. b ( ( ( x h y ) i^i ( z h w ) ) =/= (/) /\ -. ( x = z /\ y = w ) ) <-> E. x e. b E. y e. b E. z e. b E. w e. b ( ( ( x ( Hom ` ( SetCat ` 2o ) ) y ) i^i ( z ( Hom ` ( SetCat ` 2o ) ) w ) ) =/= (/) /\ -. ( x = z /\ y = w ) ) ) )
33 32 adantl 
 |-  ( ( ( c = ( SetCat ` 2o ) /\ b = ( Base ` ( SetCat ` 2o ) ) ) /\ h = ( Hom ` ( SetCat ` 2o ) ) ) -> ( E. x e. b E. y e. b E. z e. b E. w e. b ( ( ( x h y ) i^i ( z h w ) ) =/= (/) /\ -. ( x = z /\ y = w ) ) <-> E. x e. b E. y e. b E. z e. b E. w e. b ( ( ( x ( Hom ` ( SetCat ` 2o ) ) y ) i^i ( z ( Hom ` ( SetCat ` 2o ) ) w ) ) =/= (/) /\ -. ( x = z /\ y = w ) ) ) )
34 pm4.61 
 |-  ( -. ( ( ( x h y ) i^i ( z h w ) ) =/= (/) -> ( x = z /\ y = w ) ) <-> ( ( ( x h y ) i^i ( z h w ) ) =/= (/) /\ -. ( x = z /\ y = w ) ) )
35 34 2rexbii 
 |-  ( E. z e. b E. w e. b -. ( ( ( x h y ) i^i ( z h w ) ) =/= (/) -> ( x = z /\ y = w ) ) <-> E. z e. b E. w e. b ( ( ( x h y ) i^i ( z h w ) ) =/= (/) /\ -. ( x = z /\ y = w ) ) )
36 rexnal2 
 |-  ( E. z e. b E. w e. b -. ( ( ( x h y ) i^i ( z h w ) ) =/= (/) -> ( x = z /\ y = w ) ) <-> -. A. z e. b A. w e. b ( ( ( x h y ) i^i ( z h w ) ) =/= (/) -> ( x = z /\ y = w ) ) )
37 35 36 bitr3i 
 |-  ( E. z e. b E. w e. b ( ( ( x h y ) i^i ( z h w ) ) =/= (/) /\ -. ( x = z /\ y = w ) ) <-> -. A. z e. b A. w e. b ( ( ( x h y ) i^i ( z h w ) ) =/= (/) -> ( x = z /\ y = w ) ) )
38 37 2rexbii 
 |-  ( E. x e. b E. y e. b E. z e. b E. w e. b ( ( ( x h y ) i^i ( z h w ) ) =/= (/) /\ -. ( x = z /\ y = w ) ) <-> E. x e. b E. y e. b -. A. z e. b A. w e. b ( ( ( x h y ) i^i ( z h w ) ) =/= (/) -> ( x = z /\ y = w ) ) )
39 rexnal2 
 |-  ( E. x e. b E. y e. b -. A. z e. b A. w e. b ( ( ( x h y ) i^i ( z h w ) ) =/= (/) -> ( x = z /\ y = w ) ) <-> -. A. x e. b A. y e. b A. z e. b A. w e. b ( ( ( x h y ) i^i ( z h w ) ) =/= (/) -> ( x = z /\ y = w ) ) )
40 38 39 bitri 
 |-  ( E. x e. b E. y e. b E. z e. b E. w e. b ( ( ( x h y ) i^i ( z h w ) ) =/= (/) /\ -. ( x = z /\ y = w ) ) <-> -. A. x e. b A. y e. b A. z e. b A. w e. b ( ( ( x h y ) i^i ( z h w ) ) =/= (/) -> ( x = z /\ y = w ) ) )
41 40 a1i 
 |-  ( ( ( c = ( SetCat ` 2o ) /\ b = ( Base ` ( SetCat ` 2o ) ) ) /\ h = ( Hom ` ( SetCat ` 2o ) ) ) -> ( E. x e. b E. y e. b E. z e. b E. w e. b ( ( ( x h y ) i^i ( z h w ) ) =/= (/) /\ -. ( x = z /\ y = w ) ) <-> -. A. x e. b A. y e. b A. z e. b A. w e. b ( ( ( x h y ) i^i ( z h w ) ) =/= (/) -> ( x = z /\ y = w ) ) ) )
42 rexeq 
 |-  ( b = ( Base ` ( SetCat ` 2o ) ) -> ( E. w e. b ( ( ( x ( Hom ` ( SetCat ` 2o ) ) y ) i^i ( z ( Hom ` ( SetCat ` 2o ) ) w ) ) =/= (/) /\ -. ( x = z /\ y = w ) ) <-> E. w e. ( Base ` ( SetCat ` 2o ) ) ( ( ( x ( Hom ` ( SetCat ` 2o ) ) y ) i^i ( z ( Hom ` ( SetCat ` 2o ) ) w ) ) =/= (/) /\ -. ( x = z /\ y = w ) ) ) )
43 42 2rexbidv 
 |-  ( b = ( Base ` ( SetCat ` 2o ) ) -> ( E. y e. b E. z e. b E. w e. b ( ( ( x ( Hom ` ( SetCat ` 2o ) ) y ) i^i ( z ( Hom ` ( SetCat ` 2o ) ) w ) ) =/= (/) /\ -. ( x = z /\ y = w ) ) <-> E. y e. b E. z e. b E. w e. ( Base ` ( SetCat ` 2o ) ) ( ( ( x ( Hom ` ( SetCat ` 2o ) ) y ) i^i ( z ( Hom ` ( SetCat ` 2o ) ) w ) ) =/= (/) /\ -. ( x = z /\ y = w ) ) ) )
44 43 rexbidv 
 |-  ( b = ( Base ` ( SetCat ` 2o ) ) -> ( E. x e. b E. y e. b E. z e. b E. w e. b ( ( ( x ( Hom ` ( SetCat ` 2o ) ) y ) i^i ( z ( Hom ` ( SetCat ` 2o ) ) w ) ) =/= (/) /\ -. ( x = z /\ y = w ) ) <-> E. x e. b E. y e. b E. z e. b E. w e. ( Base ` ( SetCat ` 2o ) ) ( ( ( x ( Hom ` ( SetCat ` 2o ) ) y ) i^i ( z ( Hom ` ( SetCat ` 2o ) ) w ) ) =/= (/) /\ -. ( x = z /\ y = w ) ) ) )
45 rexeq 
 |-  ( b = ( Base ` ( SetCat ` 2o ) ) -> ( E. z e. b E. w e. ( Base ` ( SetCat ` 2o ) ) ( ( ( x ( Hom ` ( SetCat ` 2o ) ) y ) i^i ( z ( Hom ` ( SetCat ` 2o ) ) w ) ) =/= (/) /\ -. ( x = z /\ y = w ) ) <-> E. z e. ( Base ` ( SetCat ` 2o ) ) E. w e. ( Base ` ( SetCat ` 2o ) ) ( ( ( x ( Hom ` ( SetCat ` 2o ) ) y ) i^i ( z ( Hom ` ( SetCat ` 2o ) ) w ) ) =/= (/) /\ -. ( x = z /\ y = w ) ) ) )
46 45 2rexbidv 
 |-  ( b = ( Base ` ( SetCat ` 2o ) ) -> ( E. x e. b E. y e. b E. z e. b E. w e. ( Base ` ( SetCat ` 2o ) ) ( ( ( x ( Hom ` ( SetCat ` 2o ) ) y ) i^i ( z ( Hom ` ( SetCat ` 2o ) ) w ) ) =/= (/) /\ -. ( x = z /\ y = w ) ) <-> E. x e. b E. y e. b E. z e. ( Base ` ( SetCat ` 2o ) ) E. w e. ( Base ` ( SetCat ` 2o ) ) ( ( ( x ( Hom ` ( SetCat ` 2o ) ) y ) i^i ( z ( Hom ` ( SetCat ` 2o ) ) w ) ) =/= (/) /\ -. ( x = z /\ y = w ) ) ) )
47 rexeq 
 |-  ( b = ( Base ` ( SetCat ` 2o ) ) -> ( E. y e. b E. z e. ( Base ` ( SetCat ` 2o ) ) E. w e. ( Base ` ( SetCat ` 2o ) ) ( ( ( x ( Hom ` ( SetCat ` 2o ) ) y ) i^i ( z ( Hom ` ( SetCat ` 2o ) ) w ) ) =/= (/) /\ -. ( x = z /\ y = w ) ) <-> E. y e. ( Base ` ( SetCat ` 2o ) ) E. z e. ( Base ` ( SetCat ` 2o ) ) E. w e. ( Base ` ( SetCat ` 2o ) ) ( ( ( x ( Hom ` ( SetCat ` 2o ) ) y ) i^i ( z ( Hom ` ( SetCat ` 2o ) ) w ) ) =/= (/) /\ -. ( x = z /\ y = w ) ) ) )
48 47 rexeqbi1dv 
 |-  ( b = ( Base ` ( SetCat ` 2o ) ) -> ( E. x e. b E. y e. b E. z e. ( Base ` ( SetCat ` 2o ) ) E. w e. ( Base ` ( SetCat ` 2o ) ) ( ( ( x ( Hom ` ( SetCat ` 2o ) ) y ) i^i ( z ( Hom ` ( SetCat ` 2o ) ) w ) ) =/= (/) /\ -. ( x = z /\ y = w ) ) <-> E. x e. ( Base ` ( SetCat ` 2o ) ) E. y e. ( Base ` ( SetCat ` 2o ) ) E. z e. ( Base ` ( SetCat ` 2o ) ) E. w e. ( Base ` ( SetCat ` 2o ) ) ( ( ( x ( Hom ` ( SetCat ` 2o ) ) y ) i^i ( z ( Hom ` ( SetCat ` 2o ) ) w ) ) =/= (/) /\ -. ( x = z /\ y = w ) ) ) )
49 44 46 48 3bitrd 
 |-  ( b = ( Base ` ( SetCat ` 2o ) ) -> ( E. x e. b E. y e. b E. z e. b E. w e. b ( ( ( x ( Hom ` ( SetCat ` 2o ) ) y ) i^i ( z ( Hom ` ( SetCat ` 2o ) ) w ) ) =/= (/) /\ -. ( x = z /\ y = w ) ) <-> E. x e. ( Base ` ( SetCat ` 2o ) ) E. y e. ( Base ` ( SetCat ` 2o ) ) E. z e. ( Base ` ( SetCat ` 2o ) ) E. w e. ( Base ` ( SetCat ` 2o ) ) ( ( ( x ( Hom ` ( SetCat ` 2o ) ) y ) i^i ( z ( Hom ` ( SetCat ` 2o ) ) w ) ) =/= (/) /\ -. ( x = z /\ y = w ) ) ) )
50 49 ad2antlr 
 |-  ( ( ( c = ( SetCat ` 2o ) /\ b = ( Base ` ( SetCat ` 2o ) ) ) /\ h = ( Hom ` ( SetCat ` 2o ) ) ) -> ( E. x e. b E. y e. b E. z e. b E. w e. b ( ( ( x ( Hom ` ( SetCat ` 2o ) ) y ) i^i ( z ( Hom ` ( SetCat ` 2o ) ) w ) ) =/= (/) /\ -. ( x = z /\ y = w ) ) <-> E. x e. ( Base ` ( SetCat ` 2o ) ) E. y e. ( Base ` ( SetCat ` 2o ) ) E. z e. ( Base ` ( SetCat ` 2o ) ) E. w e. ( Base ` ( SetCat ` 2o ) ) ( ( ( x ( Hom ` ( SetCat ` 2o ) ) y ) i^i ( z ( Hom ` ( SetCat ` 2o ) ) w ) ) =/= (/) /\ -. ( x = z /\ y = w ) ) ) )
51 33 41 50 3bitr3d 
 |-  ( ( ( c = ( SetCat ` 2o ) /\ b = ( Base ` ( SetCat ` 2o ) ) ) /\ h = ( Hom ` ( SetCat ` 2o ) ) ) -> ( -. A. x e. b A. y e. b A. z e. b A. w e. b ( ( ( x h y ) i^i ( z h w ) ) =/= (/) -> ( x = z /\ y = w ) ) <-> E. x e. ( Base ` ( SetCat ` 2o ) ) E. y e. ( Base ` ( SetCat ` 2o ) ) E. z e. ( Base ` ( SetCat ` 2o ) ) E. w e. ( Base ` ( SetCat ` 2o ) ) ( ( ( x ( Hom ` ( SetCat ` 2o ) ) y ) i^i ( z ( Hom ` ( SetCat ` 2o ) ) w ) ) =/= (/) /\ -. ( x = z /\ y = w ) ) ) )
52 23 25 51 sbcied2 
 |-  ( ( c = ( SetCat ` 2o ) /\ b = ( Base ` ( SetCat ` 2o ) ) ) -> ( [. ( Hom ` c ) / h ]. -. A. x e. b A. y e. b A. z e. b A. w e. b ( ( ( x h y ) i^i ( z h w ) ) =/= (/) -> ( x = z /\ y = w ) ) <-> E. x e. ( Base ` ( SetCat ` 2o ) ) E. y e. ( Base ` ( SetCat ` 2o ) ) E. z e. ( Base ` ( SetCat ` 2o ) ) E. w e. ( Base ` ( SetCat ` 2o ) ) ( ( ( x ( Hom ` ( SetCat ` 2o ) ) y ) i^i ( z ( Hom ` ( SetCat ` 2o ) ) w ) ) =/= (/) /\ -. ( x = z /\ y = w ) ) ) )
53 21 22 52 sbcied2 
 |-  ( c = ( SetCat ` 2o ) -> ( [. ( Base ` c ) / b ]. [. ( Hom ` c ) / h ]. -. A. x e. b A. y e. b A. z e. b A. w e. b ( ( ( x h y ) i^i ( z h w ) ) =/= (/) -> ( x = z /\ y = w ) ) <-> E. x e. ( Base ` ( SetCat ` 2o ) ) E. y e. ( Base ` ( SetCat ` 2o ) ) E. z e. ( Base ` ( SetCat ` 2o ) ) E. w e. ( Base ` ( SetCat ` 2o ) ) ( ( ( x ( Hom ` ( SetCat ` 2o ) ) y ) i^i ( z ( Hom ` ( SetCat ` 2o ) ) w ) ) =/= (/) /\ -. ( x = z /\ y = w ) ) ) )
54 53 rspcev 
 |-  ( ( ( SetCat ` 2o ) e. Cat /\ E. x e. ( Base ` ( SetCat ` 2o ) ) E. y e. ( Base ` ( SetCat ` 2o ) ) E. z e. ( Base ` ( SetCat ` 2o ) ) E. w e. ( Base ` ( SetCat ` 2o ) ) ( ( ( x ( Hom ` ( SetCat ` 2o ) ) y ) i^i ( z ( Hom ` ( SetCat ` 2o ) ) w ) ) =/= (/) /\ -. ( x = z /\ y = w ) ) ) -> E. c e. Cat [. ( Base ` c ) / b ]. [. ( Hom ` c ) / h ]. -. A. x e. b A. y e. b A. z e. b A. w e. b ( ( ( x h y ) i^i ( z h w ) ) =/= (/) -> ( x = z /\ y = w ) ) )
55 4 20 54 mp2an 
 |-  E. c e. Cat [. ( Base ` c ) / b ]. [. ( Hom ` c ) / h ]. -. A. x e. b A. y e. b A. z e. b A. w e. b ( ( ( x h y ) i^i ( z h w ) ) =/= (/) -> ( x = z /\ y = w ) )