Metamath Proof Explorer

Theorem cat1lem

Description: The category of sets in a "universe" containing the empty set and another set does not have pairwise disjoint hom-sets as required in Axiom CAT 1 in Lang p. 53. Lemma for cat1 . (Contributed by Zhi Wang, 15-Sep-2024)

Ref Expression
Hypotheses cat1lem.1 
|- C = ( SetCat ` U )
cat1lem.2 
|- ( ph -> U e. V )
cat1lem.3 
|- B = ( Base ` C )
cat1lem.4 
|- H = ( Hom ` C )
cat1lem.5 
|- ( ph -> (/) e. U )
cat1lem.6 
|- ( ph -> Y e. U )
cat1lem.7 
|- ( ph -> (/) =/= Y )
Assertion cat1lem 
|- ( ph -> 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 ) ) )

Proof

Step Hyp Ref Expression
1 cat1lem.1 
 |-  C = ( SetCat ` U )
2 cat1lem.2 
 |-  ( ph -> U e. V )
3 cat1lem.3 
 |-  B = ( Base ` C )
4 cat1lem.4 
 |-  H = ( Hom ` C )
5 cat1lem.5 
 |-  ( ph -> (/) e. U )
6 cat1lem.6 
 |-  ( ph -> Y e. U )
7 cat1lem.7 
 |-  ( ph -> (/) =/= Y )
8 1 2 setcbas 
 |-  ( ph -> U = ( Base ` C ) )
9 8 3 eqtr4di 
 |-  ( ph -> U = B )
10 5 9 eleqtrd 
 |-  ( ph -> (/) e. B )
11 6 9 eleqtrd 
 |-  ( ph -> Y e. B )
12 f0 
 |-  (/) : (/) --> (/)
13 1 2 4 5 5 elsetchom 
 |-  ( ph -> ( (/) e. ( (/) H (/) ) <-> (/) : (/) --> (/) ) )
14 12 13 mpbiri 
 |-  ( ph -> (/) e. ( (/) H (/) ) )
15 f0 
 |-  (/) : (/) --> Y
16 1 2 4 5 6 elsetchom 
 |-  ( ph -> ( (/) e. ( (/) H Y ) <-> (/) : (/) --> Y ) )
17 15 16 mpbiri 
 |-  ( ph -> (/) e. ( (/) H Y ) )
18 inelcm 
 |-  ( ( (/) e. ( (/) H (/) ) /\ (/) e. ( (/) H Y ) ) -> ( ( (/) H (/) ) i^i ( (/) H Y ) ) =/= (/) )
19 14 17 18 syl2anc 
 |-  ( ph -> ( ( (/) H (/) ) i^i ( (/) H Y ) ) =/= (/) )
20 7 neneqd 
 |-  ( ph -> -. (/) = Y )
21 20 intnand 
 |-  ( ph -> -. ( (/) = (/) /\ (/) = Y ) )
22 oveq1 
 |-  ( z = (/) -> ( z H w ) = ( (/) H w ) )
23 22 ineq2d 
 |-  ( z = (/) -> ( ( (/) H (/) ) i^i ( z H w ) ) = ( ( (/) H (/) ) i^i ( (/) H w ) ) )
24 23 neeq1d 
 |-  ( z = (/) -> ( ( ( (/) H (/) ) i^i ( z H w ) ) =/= (/) <-> ( ( (/) H (/) ) i^i ( (/) H w ) ) =/= (/) ) )
25 eqeq2 
 |-  ( z = (/) -> ( (/) = z <-> (/) = (/) ) )
26 25 anbi1d 
 |-  ( z = (/) -> ( ( (/) = z /\ (/) = w ) <-> ( (/) = (/) /\ (/) = w ) ) )
27 26 notbid 
 |-  ( z = (/) -> ( -. ( (/) = z /\ (/) = w ) <-> -. ( (/) = (/) /\ (/) = w ) ) )
28 24 27 anbi12d 
 |-  ( z = (/) -> ( ( ( ( (/) H (/) ) i^i ( z H w ) ) =/= (/) /\ -. ( (/) = z /\ (/) = w ) ) <-> ( ( ( (/) H (/) ) i^i ( (/) H w ) ) =/= (/) /\ -. ( (/) = (/) /\ (/) = w ) ) ) )
29 oveq2 
 |-  ( w = Y -> ( (/) H w ) = ( (/) H Y ) )
30 29 ineq2d 
 |-  ( w = Y -> ( ( (/) H (/) ) i^i ( (/) H w ) ) = ( ( (/) H (/) ) i^i ( (/) H Y ) ) )
31 30 neeq1d 
 |-  ( w = Y -> ( ( ( (/) H (/) ) i^i ( (/) H w ) ) =/= (/) <-> ( ( (/) H (/) ) i^i ( (/) H Y ) ) =/= (/) ) )
32 eqeq2 
 |-  ( w = Y -> ( (/) = w <-> (/) = Y ) )
33 32 anbi2d 
 |-  ( w = Y -> ( ( (/) = (/) /\ (/) = w ) <-> ( (/) = (/) /\ (/) = Y ) ) )
34 33 notbid 
 |-  ( w = Y -> ( -. ( (/) = (/) /\ (/) = w ) <-> -. ( (/) = (/) /\ (/) = Y ) ) )
35 31 34 anbi12d 
 |-  ( w = Y -> ( ( ( ( (/) H (/) ) i^i ( (/) H w ) ) =/= (/) /\ -. ( (/) = (/) /\ (/) = w ) ) <-> ( ( ( (/) H (/) ) i^i ( (/) H Y ) ) =/= (/) /\ -. ( (/) = (/) /\ (/) = Y ) ) ) )
36 28 35 rspc2ev 
 |-  ( ( (/) e. B /\ Y e. B /\ ( ( ( (/) H (/) ) i^i ( (/) H Y ) ) =/= (/) /\ -. ( (/) = (/) /\ (/) = Y ) ) ) -> E. z e. B E. w e. B ( ( ( (/) H (/) ) i^i ( z H w ) ) =/= (/) /\ -. ( (/) = z /\ (/) = w ) ) )
37 10 11 19 21 36 syl112anc 
 |-  ( ph -> E. z e. B E. w e. B ( ( ( (/) H (/) ) i^i ( z H w ) ) =/= (/) /\ -. ( (/) = z /\ (/) = w ) ) )
38 oveq1 
 |-  ( x = (/) -> ( x H y ) = ( (/) H y ) )
39 38 ineq1d 
 |-  ( x = (/) -> ( ( x H y ) i^i ( z H w ) ) = ( ( (/) H y ) i^i ( z H w ) ) )
40 39 neeq1d 
 |-  ( x = (/) -> ( ( ( x H y ) i^i ( z H w ) ) =/= (/) <-> ( ( (/) H y ) i^i ( z H w ) ) =/= (/) ) )
41 eqeq1 
 |-  ( x = (/) -> ( x = z <-> (/) = z ) )
42 41 anbi1d 
 |-  ( x = (/) -> ( ( x = z /\ y = w ) <-> ( (/) = z /\ y = w ) ) )
43 42 notbid 
 |-  ( x = (/) -> ( -. ( x = z /\ y = w ) <-> -. ( (/) = z /\ y = w ) ) )
44 40 43 anbi12d 
 |-  ( x = (/) -> ( ( ( ( x H y ) i^i ( z H w ) ) =/= (/) /\ -. ( x = z /\ y = w ) ) <-> ( ( ( (/) H y ) i^i ( z H w ) ) =/= (/) /\ -. ( (/) = z /\ y = w ) ) ) )
45 44 2rexbidv 
 |-  ( x = (/) -> ( 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 ( ( ( (/) H y ) i^i ( z H w ) ) =/= (/) /\ -. ( (/) = z /\ y = w ) ) ) )
46 oveq2 
 |-  ( y = (/) -> ( (/) H y ) = ( (/) H (/) ) )
47 46 ineq1d 
 |-  ( y = (/) -> ( ( (/) H y ) i^i ( z H w ) ) = ( ( (/) H (/) ) i^i ( z H w ) ) )
48 47 neeq1d 
 |-  ( y = (/) -> ( ( ( (/) H y ) i^i ( z H w ) ) =/= (/) <-> ( ( (/) H (/) ) i^i ( z H w ) ) =/= (/) ) )
49 eqeq1 
 |-  ( y = (/) -> ( y = w <-> (/) = w ) )
50 49 anbi2d 
 |-  ( y = (/) -> ( ( (/) = z /\ y = w ) <-> ( (/) = z /\ (/) = w ) ) )
51 50 notbid 
 |-  ( y = (/) -> ( -. ( (/) = z /\ y = w ) <-> -. ( (/) = z /\ (/) = w ) ) )
52 48 51 anbi12d 
 |-  ( y = (/) -> ( ( ( ( (/) H y ) i^i ( z H w ) ) =/= (/) /\ -. ( (/) = z /\ y = w ) ) <-> ( ( ( (/) H (/) ) i^i ( z H w ) ) =/= (/) /\ -. ( (/) = z /\ (/) = w ) ) ) )
53 52 2rexbidv 
 |-  ( y = (/) -> ( E. z e. B E. w e. B ( ( ( (/) H y ) i^i ( z H w ) ) =/= (/) /\ -. ( (/) = z /\ y = w ) ) <-> E. z e. B E. w e. B ( ( ( (/) H (/) ) i^i ( z H w ) ) =/= (/) /\ -. ( (/) = z /\ (/) = w ) ) ) )
54 45 53 rspc2ev 
 |-  ( ( (/) e. B /\ (/) e. B /\ E. z e. B E. w e. B ( ( ( (/) H (/) ) i^i ( z H w ) ) =/= (/) /\ -. ( (/) = z /\ (/) = w ) ) ) -> 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 ) ) )
55 10 10 37 54 syl3anc 
 |-  ( ph -> 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 ) ) )