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 ⊢∃c∈Cat[˙Basec/b]˙[˙Hom⁡c/h]˙¬∀x∈b∀y∈b∀z∈b∀w∈bxhy∩zhw≠∅→x=z∧y=w

Proof

Step Hyp Ref Expression
1 2on ⊢2𝑜∈On
2 eqid ⊢SetCat⁡2𝑜=SetCat⁡2𝑜
3 2 setccat ⊢2𝑜∈On→SetCat⁡2𝑜∈Cat
4 1 3 ax-mp ⊢SetCat⁡2𝑜∈Cat
5 1 a1i ⊢⊤→2𝑜∈On
6 eqid ⊢BaseSetCat⁡2𝑜=BaseSetCat⁡2𝑜
7 eqid ⊢Hom⁡SetCat⁡2𝑜=Hom⁡SetCat⁡2𝑜
8 0ex ⊢∅∈V
9 8 prid1 ⊢∅∈∅∅
10 df2o2 ⊢2𝑜=∅∅
11 9 10 eleqtrri ⊢∅∈2𝑜
12 11 a1i ⊢⊤→∅∈2𝑜
13 p0ex ⊢∅∈V
14 13 prid2 ⊢∅∈∅∅
15 14 10 eleqtrri ⊢∅∈2𝑜
16 15 a1i ⊢⊤→∅∈2𝑜
17 0nep0 ⊢∅≠∅
18 17 a1i ⊢⊤→∅≠∅
19 2 5 6 7 12 16 18 cat1lem ⊢⊤→∃x∈BaseSetCat⁡2𝑜∃y∈BaseSetCat⁡2𝑜∃z∈BaseSetCat⁡2𝑜∃w∈BaseSetCat⁡2𝑜xHom⁡SetCat⁡2𝑜y∩zHom⁡SetCat⁡2𝑜w≠∅∧¬x=z∧y=w
20 19 mptru ⊢∃x∈BaseSetCat⁡2𝑜∃y∈BaseSetCat⁡2𝑜∃z∈BaseSetCat⁡2𝑜∃w∈BaseSetCat⁡2𝑜xHom⁡SetCat⁡2𝑜y∩zHom⁡SetCat⁡2𝑜w≠∅∧¬x=z∧y=w
21 fvexd ⊢c=SetCat⁡2𝑜→Basec∈V
22 fveq2 ⊢c=SetCat⁡2𝑜→Basec=BaseSetCat⁡2𝑜
23 fvexd ⊢c=SetCat⁡2𝑜∧b=BaseSetCat⁡2𝑜→Hom⁡c∈V
24 fveq2 ⊢c=SetCat⁡2𝑜→Hom⁡c=Hom⁡SetCat⁡2𝑜
25 24 adantr ⊢c=SetCat⁡2𝑜∧b=BaseSetCat⁡2𝑜→Hom⁡c=Hom⁡SetCat⁡2𝑜
26 oveq ⊢h=Hom⁡SetCat⁡2𝑜→xhy=xHom⁡SetCat⁡2𝑜y
27 oveq ⊢h=Hom⁡SetCat⁡2𝑜→zhw=zHom⁡SetCat⁡2𝑜w
28 26 27 ineq12d ⊢h=Hom⁡SetCat⁡2𝑜→xhy∩zhw=xHom⁡SetCat⁡2𝑜y∩zHom⁡SetCat⁡2𝑜w
29 28 neeq1d ⊢h=Hom⁡SetCat⁡2𝑜→xhy∩zhw≠∅↔xHom⁡SetCat⁡2𝑜y∩zHom⁡SetCat⁡2𝑜w≠∅
30 29 anbi1d ⊢h=Hom⁡SetCat⁡2𝑜→xhy∩zhw≠∅∧¬x=z∧y=w↔xHom⁡SetCat⁡2𝑜y∩zHom⁡SetCat⁡2𝑜w≠∅∧¬x=z∧y=w
31 30 2rexbidv ⊢h=Hom⁡SetCat⁡2𝑜→∃z∈b∃w∈bxhy∩zhw≠∅∧¬x=z∧y=w↔∃z∈b∃w∈bxHom⁡SetCat⁡2𝑜y∩zHom⁡SetCat⁡2𝑜w≠∅∧¬x=z∧y=w
32 31 2rexbidv ⊢h=Hom⁡SetCat⁡2𝑜→∃x∈b∃y∈b∃z∈b∃w∈bxhy∩zhw≠∅∧¬x=z∧y=w↔∃x∈b∃y∈b∃z∈b∃w∈bxHom⁡SetCat⁡2𝑜y∩zHom⁡SetCat⁡2𝑜w≠∅∧¬x=z∧y=w
33 32 adantl ⊢c=SetCat⁡2𝑜∧b=BaseSetCat⁡2𝑜∧h=Hom⁡SetCat⁡2𝑜→∃x∈b∃y∈b∃z∈b∃w∈bxhy∩zhw≠∅∧¬x=z∧y=w↔∃x∈b∃y∈b∃z∈b∃w∈bxHom⁡SetCat⁡2𝑜y∩zHom⁡SetCat⁡2𝑜w≠∅∧¬x=z∧y=w
34 pm4.61 ⊢¬xhy∩zhw≠∅→x=z∧y=w↔xhy∩zhw≠∅∧¬x=z∧y=w
35 34 2rexbii ⊢∃z∈b∃w∈b¬xhy∩zhw≠∅→x=z∧y=w↔∃z∈b∃w∈bxhy∩zhw≠∅∧¬x=z∧y=w
36 rexnal2 ⊢∃z∈b∃w∈b¬xhy∩zhw≠∅→x=z∧y=w↔¬∀z∈b∀w∈bxhy∩zhw≠∅→x=z∧y=w
37 35 36 bitr3i ⊢∃z∈b∃w∈bxhy∩zhw≠∅∧¬x=z∧y=w↔¬∀z∈b∀w∈bxhy∩zhw≠∅→x=z∧y=w
38 37 2rexbii ⊢∃x∈b∃y∈b∃z∈b∃w∈bxhy∩zhw≠∅∧¬x=z∧y=w↔∃x∈b∃y∈b¬∀z∈b∀w∈bxhy∩zhw≠∅→x=z∧y=w
39 rexnal2 ⊢∃x∈b∃y∈b¬∀z∈b∀w∈bxhy∩zhw≠∅→x=z∧y=w↔¬∀x∈b∀y∈b∀z∈b∀w∈bxhy∩zhw≠∅→x=z∧y=w
40 38 39 bitri ⊢∃x∈b∃y∈b∃z∈b∃w∈bxhy∩zhw≠∅∧¬x=z∧y=w↔¬∀x∈b∀y∈b∀z∈b∀w∈bxhy∩zhw≠∅→x=z∧y=w
41 40 a1i ⊢c=SetCat⁡2𝑜∧b=BaseSetCat⁡2𝑜∧h=Hom⁡SetCat⁡2𝑜→∃x∈b∃y∈b∃z∈b∃w∈bxhy∩zhw≠∅∧¬x=z∧y=w↔¬∀x∈b∀y∈b∀z∈b∀w∈bxhy∩zhw≠∅→x=z∧y=w
42 rexeq ⊢b=BaseSetCat⁡2𝑜→∃w∈bxHom⁡SetCat⁡2𝑜y∩zHom⁡SetCat⁡2𝑜w≠∅∧¬x=z∧y=w↔∃w∈BaseSetCat⁡2𝑜xHom⁡SetCat⁡2𝑜y∩zHom⁡SetCat⁡2𝑜w≠∅∧¬x=z∧y=w
43 42 2rexbidv ⊢b=BaseSetCat⁡2𝑜→∃y∈b∃z∈b∃w∈bxHom⁡SetCat⁡2𝑜y∩zHom⁡SetCat⁡2𝑜w≠∅∧¬x=z∧y=w↔∃y∈b∃z∈b∃w∈BaseSetCat⁡2𝑜xHom⁡SetCat⁡2𝑜y∩zHom⁡SetCat⁡2𝑜w≠∅∧¬x=z∧y=w
44 43 rexbidv ⊢b=BaseSetCat⁡2𝑜→∃x∈b∃y∈b∃z∈b∃w∈bxHom⁡SetCat⁡2𝑜y∩zHom⁡SetCat⁡2𝑜w≠∅∧¬x=z∧y=w↔∃x∈b∃y∈b∃z∈b∃w∈BaseSetCat⁡2𝑜xHom⁡SetCat⁡2𝑜y∩zHom⁡SetCat⁡2𝑜w≠∅∧¬x=z∧y=w
45 rexeq ⊢b=BaseSetCat⁡2𝑜→∃z∈b∃w∈BaseSetCat⁡2𝑜xHom⁡SetCat⁡2𝑜y∩zHom⁡SetCat⁡2𝑜w≠∅∧¬x=z∧y=w↔∃z∈BaseSetCat⁡2𝑜∃w∈BaseSetCat⁡2𝑜xHom⁡SetCat⁡2𝑜y∩zHom⁡SetCat⁡2𝑜w≠∅∧¬x=z∧y=w
46 45 2rexbidv ⊢b=BaseSetCat⁡2𝑜→∃x∈b∃y∈b∃z∈b∃w∈BaseSetCat⁡2𝑜xHom⁡SetCat⁡2𝑜y∩zHom⁡SetCat⁡2𝑜w≠∅∧¬x=z∧y=w↔∃x∈b∃y∈b∃z∈BaseSetCat⁡2𝑜∃w∈BaseSetCat⁡2𝑜xHom⁡SetCat⁡2𝑜y∩zHom⁡SetCat⁡2𝑜w≠∅∧¬x=z∧y=w
47 rexeq ⊢b=BaseSetCat⁡2𝑜→∃y∈b∃z∈BaseSetCat⁡2𝑜∃w∈BaseSetCat⁡2𝑜xHom⁡SetCat⁡2𝑜y∩zHom⁡SetCat⁡2𝑜w≠∅∧¬x=z∧y=w↔∃y∈BaseSetCat⁡2𝑜∃z∈BaseSetCat⁡2𝑜∃w∈BaseSetCat⁡2𝑜xHom⁡SetCat⁡2𝑜y∩zHom⁡SetCat⁡2𝑜w≠∅∧¬x=z∧y=w
48 47 rexeqbi1dv ⊢b=BaseSetCat⁡2𝑜→∃x∈b∃y∈b∃z∈BaseSetCat⁡2𝑜∃w∈BaseSetCat⁡2𝑜xHom⁡SetCat⁡2𝑜y∩zHom⁡SetCat⁡2𝑜w≠∅∧¬x=z∧y=w↔∃x∈BaseSetCat⁡2𝑜∃y∈BaseSetCat⁡2𝑜∃z∈BaseSetCat⁡2𝑜∃w∈BaseSetCat⁡2𝑜xHom⁡SetCat⁡2𝑜y∩zHom⁡SetCat⁡2𝑜w≠∅∧¬x=z∧y=w
49 44 46 48 3bitrd ⊢b=BaseSetCat⁡2𝑜→∃x∈b∃y∈b∃z∈b∃w∈bxHom⁡SetCat⁡2𝑜y∩zHom⁡SetCat⁡2𝑜w≠∅∧¬x=z∧y=w↔∃x∈BaseSetCat⁡2𝑜∃y∈BaseSetCat⁡2𝑜∃z∈BaseSetCat⁡2𝑜∃w∈BaseSetCat⁡2𝑜xHom⁡SetCat⁡2𝑜y∩zHom⁡SetCat⁡2𝑜w≠∅∧¬x=z∧y=w
50 49 ad2antlr ⊢c=SetCat⁡2𝑜∧b=BaseSetCat⁡2𝑜∧h=Hom⁡SetCat⁡2𝑜→∃x∈b∃y∈b∃z∈b∃w∈bxHom⁡SetCat⁡2𝑜y∩zHom⁡SetCat⁡2𝑜w≠∅∧¬x=z∧y=w↔∃x∈BaseSetCat⁡2𝑜∃y∈BaseSetCat⁡2𝑜∃z∈BaseSetCat⁡2𝑜∃w∈BaseSetCat⁡2𝑜xHom⁡SetCat⁡2𝑜y∩zHom⁡SetCat⁡2𝑜w≠∅∧¬x=z∧y=w
51 33 41 50 3bitr3d ⊢c=SetCat⁡2𝑜∧b=BaseSetCat⁡2𝑜∧h=Hom⁡SetCat⁡2𝑜→¬∀x∈b∀y∈b∀z∈b∀w∈bxhy∩zhw≠∅→x=z∧y=w↔∃x∈BaseSetCat⁡2𝑜∃y∈BaseSetCat⁡2𝑜∃z∈BaseSetCat⁡2𝑜∃w∈BaseSetCat⁡2𝑜xHom⁡SetCat⁡2𝑜y∩zHom⁡SetCat⁡2𝑜w≠∅∧¬x=z∧y=w
52 23 25 51 sbcied2 ⊢c=SetCat⁡2𝑜∧b=BaseSetCat⁡2𝑜→[˙Hom⁡c/h]˙¬∀x∈b∀y∈b∀z∈b∀w∈bxhy∩zhw≠∅→x=z∧y=w↔∃x∈BaseSetCat⁡2𝑜∃y∈BaseSetCat⁡2𝑜∃z∈BaseSetCat⁡2𝑜∃w∈BaseSetCat⁡2𝑜xHom⁡SetCat⁡2𝑜y∩zHom⁡SetCat⁡2𝑜w≠∅∧¬x=z∧y=w
53 21 22 52 sbcied2 ⊢c=SetCat⁡2𝑜→[˙Basec/b]˙[˙Hom⁡c/h]˙¬∀x∈b∀y∈b∀z∈b∀w∈bxhy∩zhw≠∅→x=z∧y=w↔∃x∈BaseSetCat⁡2𝑜∃y∈BaseSetCat⁡2𝑜∃z∈BaseSetCat⁡2𝑜∃w∈BaseSetCat⁡2𝑜xHom⁡SetCat⁡2𝑜y∩zHom⁡SetCat⁡2𝑜w≠∅∧¬x=z∧y=w
54 53 rspcev ⊢SetCat⁡2𝑜∈Cat∧∃x∈BaseSetCat⁡2𝑜∃y∈BaseSetCat⁡2𝑜∃z∈BaseSetCat⁡2𝑜∃w∈BaseSetCat⁡2𝑜xHom⁡SetCat⁡2𝑜y∩zHom⁡SetCat⁡2𝑜w≠∅∧¬x=z∧y=w→∃c∈Cat[˙Basec/b]˙[˙Hom⁡c/h]˙¬∀x∈b∀y∈b∀z∈b∀w∈bxhy∩zhw≠∅→x=z∧y=w
55 4 20 54 mp2an ⊢∃c∈Cat[˙Basec/b]˙[˙Hom⁡c/h]˙¬∀x∈b∀y∈b∀z∈b∀w∈bxhy∩zhw≠∅→x=z∧y=w