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 [˙Base c / b]˙ [˙ Hom ⁡ c / h]˙ ¬ ∀ x ∈ b ∀ y ∈ b ∀ z ∈ b ∀ w ∈ b x h y ∩ z h w ≠ ∅ → 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 ⊢ Base SetCat ⁡ 2 𝑜 = Base SetCat ⁡ 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 ∈ Base SetCat ⁡ 2 𝑜 ∃ y ∈ Base SetCat ⁡ 2 𝑜 ∃ z ∈ Base SetCat ⁡ 2 𝑜 ∃ w ∈ Base SetCat ⁡ 2 𝑜 x Hom ⁡ SetCat ⁡ 2 𝑜 y ∩ z Hom ⁡ SetCat ⁡ 2 𝑜 w ≠ ∅ ∧ ¬ x = z ∧ y = w
20 19 mptru ⊢ ∃ x ∈ Base SetCat ⁡ 2 𝑜 ∃ y ∈ Base SetCat ⁡ 2 𝑜 ∃ z ∈ Base SetCat ⁡ 2 𝑜 ∃ w ∈ Base SetCat ⁡ 2 𝑜 x Hom ⁡ SetCat ⁡ 2 𝑜 y ∩ z Hom ⁡ SetCat ⁡ 2 𝑜 w ≠ ∅ ∧ ¬ x = z ∧ y = w
21 fvexd ⊢ c = SetCat ⁡ 2 𝑜 → Base c ∈ V
22 fveq2 ⊢ c = SetCat ⁡ 2 𝑜 → Base c = Base SetCat ⁡ 2 𝑜
23 fvexd ⊢ c = SetCat ⁡ 2 𝑜 ∧ b = Base SetCat ⁡ 2 𝑜 → Hom ⁡ c ∈ V
24 fveq2 ⊢ c = SetCat ⁡ 2 𝑜 → Hom ⁡ c = Hom ⁡ SetCat ⁡ 2 𝑜
25 24 adantr ⊢ c = SetCat ⁡ 2 𝑜 ∧ b = Base SetCat ⁡ 2 𝑜 → Hom ⁡ c = Hom ⁡ SetCat ⁡ 2 𝑜
26 oveq ⊢ h = Hom ⁡ SetCat ⁡ 2 𝑜 → x h y = x Hom ⁡ SetCat ⁡ 2 𝑜 y
27 oveq ⊢ h = Hom ⁡ SetCat ⁡ 2 𝑜 → z h w = z Hom ⁡ SetCat ⁡ 2 𝑜 w
28 26 27 ineq12d ⊢ h = Hom ⁡ SetCat ⁡ 2 𝑜 → x h y ∩ z h w = x Hom ⁡ SetCat ⁡ 2 𝑜 y ∩ z Hom ⁡ SetCat ⁡ 2 𝑜 w
29 28 neeq1d ⊢ h = Hom ⁡ SetCat ⁡ 2 𝑜 → x h y ∩ z h w ≠ ∅ ↔ x Hom ⁡ SetCat ⁡ 2 𝑜 y ∩ z Hom ⁡ SetCat ⁡ 2 𝑜 w ≠ ∅
30 29 anbi1d ⊢ h = Hom ⁡ SetCat ⁡ 2 𝑜 → x h y ∩ z h w ≠ ∅ ∧ ¬ x = z ∧ y = w ↔ x Hom ⁡ SetCat ⁡ 2 𝑜 y ∩ z Hom ⁡ SetCat ⁡ 2 𝑜 w ≠ ∅ ∧ ¬ x = z ∧ y = w
31 30 2rexbidv ⊢ h = Hom ⁡ SetCat ⁡ 2 𝑜 → ∃ z ∈ b ∃ w ∈ b x h y ∩ z h w ≠ ∅ ∧ ¬ x = z ∧ y = w ↔ ∃ z ∈ b ∃ w ∈ b x Hom ⁡ SetCat ⁡ 2 𝑜 y ∩ z Hom ⁡ SetCat ⁡ 2 𝑜 w ≠ ∅ ∧ ¬ x = z ∧ y = w
32 31 2rexbidv ⊢ h = Hom ⁡ SetCat ⁡ 2 𝑜 → ∃ x ∈ b ∃ y ∈ b ∃ z ∈ b ∃ w ∈ b x h y ∩ z h w ≠ ∅ ∧ ¬ x = z ∧ y = w ↔ ∃ x ∈ b ∃ y ∈ b ∃ z ∈ b ∃ w ∈ b x Hom ⁡ SetCat ⁡ 2 𝑜 y ∩ z Hom ⁡ SetCat ⁡ 2 𝑜 w ≠ ∅ ∧ ¬ x = z ∧ y = w
33 32 adantl ⊢ c = SetCat ⁡ 2 𝑜 ∧ b = Base SetCat ⁡ 2 𝑜 ∧ h = Hom ⁡ SetCat ⁡ 2 𝑜 → ∃ x ∈ b ∃ y ∈ b ∃ z ∈ b ∃ w ∈ b x h y ∩ z h w ≠ ∅ ∧ ¬ x = z ∧ y = w ↔ ∃ x ∈ b ∃ y ∈ b ∃ z ∈ b ∃ w ∈ b x Hom ⁡ SetCat ⁡ 2 𝑜 y ∩ z Hom ⁡ SetCat ⁡ 2 𝑜 w ≠ ∅ ∧ ¬ x = z ∧ y = w
34 pm4.61 ⊢ ¬ x h y ∩ z h w ≠ ∅ → x = z ∧ y = w ↔ x h y ∩ z h w ≠ ∅ ∧ ¬ x = z ∧ y = w
35 34 2rexbii ⊢ ∃ z ∈ b ∃ w ∈ b ¬ x h y ∩ z h w ≠ ∅ → x = z ∧ y = w ↔ ∃ z ∈ b ∃ w ∈ b x h y ∩ z h w ≠ ∅ ∧ ¬ x = z ∧ y = w
36 rexnal2 ⊢ ∃ z ∈ b ∃ w ∈ b ¬ x h y ∩ z h w ≠ ∅ → x = z ∧ y = w ↔ ¬ ∀ z ∈ b ∀ w ∈ b x h y ∩ z h w ≠ ∅ → x = z ∧ y = w
37 35 36 bitr3i ⊢ ∃ z ∈ b ∃ w ∈ b x h y ∩ z h w ≠ ∅ ∧ ¬ x = z ∧ y = w ↔ ¬ ∀ z ∈ b ∀ w ∈ b x h y ∩ z h w ≠ ∅ → x = z ∧ y = w
38 37 2rexbii ⊢ ∃ x ∈ b ∃ y ∈ b ∃ z ∈ b ∃ w ∈ b x h y ∩ z h w ≠ ∅ ∧ ¬ x = z ∧ y = w ↔ ∃ x ∈ b ∃ y ∈ b ¬ ∀ z ∈ b ∀ w ∈ b x h y ∩ z h w ≠ ∅ → x = z ∧ y = w
39 rexnal2 ⊢ ∃ x ∈ b ∃ y ∈ b ¬ ∀ z ∈ b ∀ w ∈ b x h y ∩ z h w ≠ ∅ → x = z ∧ y = w ↔ ¬ ∀ x ∈ b ∀ y ∈ b ∀ z ∈ b ∀ w ∈ b x h y ∩ z h w ≠ ∅ → x = z ∧ y = w
40 38 39 bitri ⊢ ∃ x ∈ b ∃ y ∈ b ∃ z ∈ b ∃ w ∈ b x h y ∩ z h w ≠ ∅ ∧ ¬ x = z ∧ y = w ↔ ¬ ∀ x ∈ b ∀ y ∈ b ∀ z ∈ b ∀ w ∈ b x h y ∩ z h w ≠ ∅ → x = z ∧ y = w
41 40 a1i ⊢ c = SetCat ⁡ 2 𝑜 ∧ b = Base SetCat ⁡ 2 𝑜 ∧ h = Hom ⁡ SetCat ⁡ 2 𝑜 → ∃ x ∈ b ∃ y ∈ b ∃ z ∈ b ∃ w ∈ b x h y ∩ z h w ≠ ∅ ∧ ¬ x = z ∧ y = w ↔ ¬ ∀ x ∈ b ∀ y ∈ b ∀ z ∈ b ∀ w ∈ b x h y ∩ z h w ≠ ∅ → x = z ∧ y = w
42 rexeq ⊢ b = Base SetCat ⁡ 2 𝑜 → ∃ w ∈ b x Hom ⁡ SetCat ⁡ 2 𝑜 y ∩ z Hom ⁡ SetCat ⁡ 2 𝑜 w ≠ ∅ ∧ ¬ x = z ∧ y = w ↔ ∃ w ∈ Base SetCat ⁡ 2 𝑜 x Hom ⁡ SetCat ⁡ 2 𝑜 y ∩ z Hom ⁡ SetCat ⁡ 2 𝑜 w ≠ ∅ ∧ ¬ x = z ∧ y = w
43 42 2rexbidv ⊢ b = Base SetCat ⁡ 2 𝑜 → ∃ y ∈ b ∃ z ∈ b ∃ w ∈ b x Hom ⁡ SetCat ⁡ 2 𝑜 y ∩ z Hom ⁡ SetCat ⁡ 2 𝑜 w ≠ ∅ ∧ ¬ x = z ∧ y = w ↔ ∃ y ∈ b ∃ z ∈ b ∃ w ∈ Base SetCat ⁡ 2 𝑜 x Hom ⁡ SetCat ⁡ 2 𝑜 y ∩ z Hom ⁡ SetCat ⁡ 2 𝑜 w ≠ ∅ ∧ ¬ x = z ∧ y = w
44 43 rexbidv ⊢ b = Base SetCat ⁡ 2 𝑜 → ∃ x ∈ b ∃ y ∈ b ∃ z ∈ b ∃ w ∈ b x Hom ⁡ SetCat ⁡ 2 𝑜 y ∩ z Hom ⁡ SetCat ⁡ 2 𝑜 w ≠ ∅ ∧ ¬ x = z ∧ y = w ↔ ∃ x ∈ b ∃ y ∈ b ∃ z ∈ b ∃ w ∈ Base SetCat ⁡ 2 𝑜 x Hom ⁡ SetCat ⁡ 2 𝑜 y ∩ z Hom ⁡ SetCat ⁡ 2 𝑜 w ≠ ∅ ∧ ¬ x = z ∧ y = w
45 rexeq ⊢ b = Base SetCat ⁡ 2 𝑜 → ∃ z ∈ b ∃ w ∈ Base SetCat ⁡ 2 𝑜 x Hom ⁡ SetCat ⁡ 2 𝑜 y ∩ z Hom ⁡ SetCat ⁡ 2 𝑜 w ≠ ∅ ∧ ¬ x = z ∧ y = w ↔ ∃ z ∈ Base SetCat ⁡ 2 𝑜 ∃ w ∈ Base SetCat ⁡ 2 𝑜 x Hom ⁡ SetCat ⁡ 2 𝑜 y ∩ z Hom ⁡ SetCat ⁡ 2 𝑜 w ≠ ∅ ∧ ¬ x = z ∧ y = w
46 45 2rexbidv ⊢ b = Base SetCat ⁡ 2 𝑜 → ∃ x ∈ b ∃ y ∈ b ∃ z ∈ b ∃ w ∈ Base SetCat ⁡ 2 𝑜 x Hom ⁡ SetCat ⁡ 2 𝑜 y ∩ z Hom ⁡ SetCat ⁡ 2 𝑜 w ≠ ∅ ∧ ¬ x = z ∧ y = w ↔ ∃ x ∈ b ∃ y ∈ b ∃ z ∈ Base SetCat ⁡ 2 𝑜 ∃ w ∈ Base SetCat ⁡ 2 𝑜 x Hom ⁡ SetCat ⁡ 2 𝑜 y ∩ z Hom ⁡ SetCat ⁡ 2 𝑜 w ≠ ∅ ∧ ¬ x = z ∧ y = w
47 rexeq ⊢ b = Base SetCat ⁡ 2 𝑜 → ∃ y ∈ b ∃ z ∈ Base SetCat ⁡ 2 𝑜 ∃ w ∈ Base SetCat ⁡ 2 𝑜 x Hom ⁡ SetCat ⁡ 2 𝑜 y ∩ z Hom ⁡ SetCat ⁡ 2 𝑜 w ≠ ∅ ∧ ¬ x = z ∧ y = w ↔ ∃ y ∈ Base SetCat ⁡ 2 𝑜 ∃ z ∈ Base SetCat ⁡ 2 𝑜 ∃ w ∈ Base SetCat ⁡ 2 𝑜 x Hom ⁡ SetCat ⁡ 2 𝑜 y ∩ z Hom ⁡ SetCat ⁡ 2 𝑜 w ≠ ∅ ∧ ¬ x = z ∧ y = w
48 47 rexeqbi1dv ⊢ b = Base SetCat ⁡ 2 𝑜 → ∃ x ∈ b ∃ y ∈ b ∃ z ∈ Base SetCat ⁡ 2 𝑜 ∃ w ∈ Base SetCat ⁡ 2 𝑜 x Hom ⁡ SetCat ⁡ 2 𝑜 y ∩ z Hom ⁡ SetCat ⁡ 2 𝑜 w ≠ ∅ ∧ ¬ x = z ∧ y = w ↔ ∃ x ∈ Base SetCat ⁡ 2 𝑜 ∃ y ∈ Base SetCat ⁡ 2 𝑜 ∃ z ∈ Base SetCat ⁡ 2 𝑜 ∃ w ∈ Base SetCat ⁡ 2 𝑜 x Hom ⁡ SetCat ⁡ 2 𝑜 y ∩ z Hom ⁡ SetCat ⁡ 2 𝑜 w ≠ ∅ ∧ ¬ x = z ∧ y = w
49 44 46 48 3bitrd ⊢ b = Base SetCat ⁡ 2 𝑜 → ∃ x ∈ b ∃ y ∈ b ∃ z ∈ b ∃ w ∈ b x Hom ⁡ SetCat ⁡ 2 𝑜 y ∩ z Hom ⁡ SetCat ⁡ 2 𝑜 w ≠ ∅ ∧ ¬ x = z ∧ y = w ↔ ∃ x ∈ Base SetCat ⁡ 2 𝑜 ∃ y ∈ Base SetCat ⁡ 2 𝑜 ∃ z ∈ Base SetCat ⁡ 2 𝑜 ∃ w ∈ Base SetCat ⁡ 2 𝑜 x Hom ⁡ SetCat ⁡ 2 𝑜 y ∩ z Hom ⁡ SetCat ⁡ 2 𝑜 w ≠ ∅ ∧ ¬ x = z ∧ y = w
50 49 ad2antlr ⊢ c = SetCat ⁡ 2 𝑜 ∧ b = Base SetCat ⁡ 2 𝑜 ∧ h = Hom ⁡ SetCat ⁡ 2 𝑜 → ∃ x ∈ b ∃ y ∈ b ∃ z ∈ b ∃ w ∈ b x Hom ⁡ SetCat ⁡ 2 𝑜 y ∩ z Hom ⁡ SetCat ⁡ 2 𝑜 w ≠ ∅ ∧ ¬ x = z ∧ y = w ↔ ∃ x ∈ Base SetCat ⁡ 2 𝑜 ∃ y ∈ Base SetCat ⁡ 2 𝑜 ∃ z ∈ Base SetCat ⁡ 2 𝑜 ∃ w ∈ Base SetCat ⁡ 2 𝑜 x Hom ⁡ SetCat ⁡ 2 𝑜 y ∩ z Hom ⁡ SetCat ⁡ 2 𝑜 w ≠ ∅ ∧ ¬ x = z ∧ y = w
51 33 41 50 3bitr3d ⊢ c = SetCat ⁡ 2 𝑜 ∧ b = Base SetCat ⁡ 2 𝑜 ∧ h = Hom ⁡ SetCat ⁡ 2 𝑜 → ¬ ∀ x ∈ b ∀ y ∈ b ∀ z ∈ b ∀ w ∈ b x h y ∩ z h w ≠ ∅ → x = z ∧ y = w ↔ ∃ x ∈ Base SetCat ⁡ 2 𝑜 ∃ y ∈ Base SetCat ⁡ 2 𝑜 ∃ z ∈ Base SetCat ⁡ 2 𝑜 ∃ w ∈ Base SetCat ⁡ 2 𝑜 x Hom ⁡ SetCat ⁡ 2 𝑜 y ∩ z Hom ⁡ SetCat ⁡ 2 𝑜 w ≠ ∅ ∧ ¬ x = z ∧ y = w
52 23 25 51 sbcied2 ⊢ c = SetCat ⁡ 2 𝑜 ∧ b = Base SetCat ⁡ 2 𝑜 → [˙ Hom ⁡ c / h]˙ ¬ ∀ x ∈ b ∀ y ∈ b ∀ z ∈ b ∀ w ∈ b x h y ∩ z h w ≠ ∅ → x = z ∧ y = w ↔ ∃ x ∈ Base SetCat ⁡ 2 𝑜 ∃ y ∈ Base SetCat ⁡ 2 𝑜 ∃ z ∈ Base SetCat ⁡ 2 𝑜 ∃ w ∈ Base SetCat ⁡ 2 𝑜 x Hom ⁡ SetCat ⁡ 2 𝑜 y ∩ z Hom ⁡ SetCat ⁡ 2 𝑜 w ≠ ∅ ∧ ¬ x = z ∧ y = w
53 21 22 52 sbcied2 ⊢ c = SetCat ⁡ 2 𝑜 → [˙Base c / b]˙ [˙ Hom ⁡ c / h]˙ ¬ ∀ x ∈ b ∀ y ∈ b ∀ z ∈ b ∀ w ∈ b x h y ∩ z h w ≠ ∅ → x = z ∧ y = w ↔ ∃ x ∈ Base SetCat ⁡ 2 𝑜 ∃ y ∈ Base SetCat ⁡ 2 𝑜 ∃ z ∈ Base SetCat ⁡ 2 𝑜 ∃ w ∈ Base SetCat ⁡ 2 𝑜 x Hom ⁡ SetCat ⁡ 2 𝑜 y ∩ z Hom ⁡ SetCat ⁡ 2 𝑜 w ≠ ∅ ∧ ¬ x = z ∧ y = w
54 53 rspcev ⊢ SetCat ⁡ 2 𝑜 ∈ Cat ∧ ∃ x ∈ Base SetCat ⁡ 2 𝑜 ∃ y ∈ Base SetCat ⁡ 2 𝑜 ∃ z ∈ Base SetCat ⁡ 2 𝑜 ∃ w ∈ Base SetCat ⁡ 2 𝑜 x Hom ⁡ SetCat ⁡ 2 𝑜 y ∩ z Hom ⁡ SetCat ⁡ 2 𝑜 w ≠ ∅ ∧ ¬ x = z ∧ y = w → ∃ c ∈ Cat [˙Base c / b]˙ [˙ Hom ⁡ c / h]˙ ¬ ∀ x ∈ b ∀ y ∈ b ∀ z ∈ b ∀ w ∈ b x h y ∩ z h w ≠ ∅ → x = z ∧ y = w
55 4 20 54 mp2an ⊢ ∃ c ∈ Cat [˙Base c / b]˙ [˙ Hom ⁡ c / h]˙ ¬ ∀ x ∈ b ∀ y ∈ b ∀ z ∈ b ∀ w ∈ b x h y ∩ z h w ≠ ∅ → x = z ∧ y = w