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 ⊢ φ → U ∈ V
cat1lem.3 ⊢ B = Base C
cat1lem.4 ⊢ H = Hom ⁡ C
cat1lem.5 ⊢ φ → ∅ ∈ U
cat1lem.6 ⊢ φ → Y ∈ U
cat1lem.7 ⊢ φ → ∅ ≠ Y
Assertion cat1lem ⊢ φ → ∃ x ∈ B ∃ y ∈ B ∃ z ∈ B ∃ w ∈ B x H y ∩ z H w ≠ ∅ ∧ ¬ x = z ∧ y = w

Proof

Step Hyp Ref Expression
1 cat1lem.1 ⊢ C = SetCat ⁡ U
2 cat1lem.2 ⊢ φ → U ∈ V
3 cat1lem.3 ⊢ B = Base C
4 cat1lem.4 ⊢ H = Hom ⁡ C
5 cat1lem.5 ⊢ φ → ∅ ∈ U
6 cat1lem.6 ⊢ φ → Y ∈ U
7 cat1lem.7 ⊢ φ → ∅ ≠ Y
8 1 2 setcbas ⊢ φ → U = Base C
9 8 3 eqtr4di ⊢ φ → U = B
10 5 9 eleqtrd ⊢ φ → ∅ ∈ B
11 6 9 eleqtrd ⊢ φ → Y ∈ B
12 f0 ⊢ ∅ : ∅ ⟶ ∅
13 1 2 4 5 5 elsetchom ⊢ φ → ∅ ∈ ∅ H ∅ ↔ ∅ : ∅ ⟶ ∅
14 12 13 mpbiri ⊢ φ → ∅ ∈ ∅ H ∅
15 f0 ⊢ ∅ : ∅ ⟶ Y
16 1 2 4 5 6 elsetchom ⊢ φ → ∅ ∈ ∅ H Y ↔ ∅ : ∅ ⟶ Y
17 15 16 mpbiri ⊢ φ → ∅ ∈ ∅ H Y
18 inelcm ⊢ ∅ ∈ ∅ H ∅ ∧ ∅ ∈ ∅ H Y → ∅ H ∅ ∩ ∅ H Y ≠ ∅
19 14 17 18 syl2anc ⊢ φ → ∅ H ∅ ∩ ∅ H Y ≠ ∅
20 7 neneqd ⊢ φ → ¬ ∅ = Y
21 20 intnand ⊢ φ → ¬ ∅ = ∅ ∧ ∅ = Y
22 oveq1 ⊢ z = ∅ → z H w = ∅ H w
23 22 ineq2d ⊢ z = ∅ → ∅ H ∅ ∩ z H w = ∅ H ∅ ∩ ∅ H w
24 23 neeq1d ⊢ z = ∅ → ∅ H ∅ ∩ z H w ≠ ∅ ↔ ∅ H ∅ ∩ ∅ 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 ∅ ∩ z H w ≠ ∅ ∧ ¬ ∅ = z ∧ ∅ = w ↔ ∅ H ∅ ∩ ∅ H w ≠ ∅ ∧ ¬ ∅ = ∅ ∧ ∅ = w
29 oveq2 ⊢ w = Y → ∅ H w = ∅ H Y
30 29 ineq2d ⊢ w = Y → ∅ H ∅ ∩ ∅ H w = ∅ H ∅ ∩ ∅ H Y
31 30 neeq1d ⊢ w = Y → ∅ H ∅ ∩ ∅ H w ≠ ∅ ↔ ∅ H ∅ ∩ ∅ 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 ∅ ∩ ∅ H w ≠ ∅ ∧ ¬ ∅ = ∅ ∧ ∅ = w ↔ ∅ H ∅ ∩ ∅ H Y ≠ ∅ ∧ ¬ ∅ = ∅ ∧ ∅ = Y
36 28 35 rspc2ev ⊢ ∅ ∈ B ∧ Y ∈ B ∧ ∅ H ∅ ∩ ∅ H Y ≠ ∅ ∧ ¬ ∅ = ∅ ∧ ∅ = Y → ∃ z ∈ B ∃ w ∈ B ∅ H ∅ ∩ z H w ≠ ∅ ∧ ¬ ∅ = z ∧ ∅ = w
37 10 11 19 21 36 syl112anc ⊢ φ → ∃ z ∈ B ∃ w ∈ B ∅ H ∅ ∩ z H w ≠ ∅ ∧ ¬ ∅ = z ∧ ∅ = w
38 oveq1 ⊢ x = ∅ → x H y = ∅ H y
39 38 ineq1d ⊢ x = ∅ → x H y ∩ z H w = ∅ H y ∩ z H w
40 39 neeq1d ⊢ x = ∅ → x H y ∩ z H w ≠ ∅ ↔ ∅ H y ∩ 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 ∩ z H w ≠ ∅ ∧ ¬ x = z ∧ y = w ↔ ∅ H y ∩ z H w ≠ ∅ ∧ ¬ ∅ = z ∧ y = w
45 44 2rexbidv ⊢ x = ∅ → ∃ z ∈ B ∃ w ∈ B x H y ∩ z H w ≠ ∅ ∧ ¬ x = z ∧ y = w ↔ ∃ z ∈ B ∃ w ∈ B ∅ H y ∩ z H w ≠ ∅ ∧ ¬ ∅ = z ∧ y = w
46 oveq2 ⊢ y = ∅ → ∅ H y = ∅ H ∅
47 46 ineq1d ⊢ y = ∅ → ∅ H y ∩ z H w = ∅ H ∅ ∩ z H w
48 47 neeq1d ⊢ y = ∅ → ∅ H y ∩ z H w ≠ ∅ ↔ ∅ H ∅ ∩ 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 ∩ z H w ≠ ∅ ∧ ¬ ∅ = z ∧ y = w ↔ ∅ H ∅ ∩ z H w ≠ ∅ ∧ ¬ ∅ = z ∧ ∅ = w
53 52 2rexbidv ⊢ y = ∅ → ∃ z ∈ B ∃ w ∈ B ∅ H y ∩ z H w ≠ ∅ ∧ ¬ ∅ = z ∧ y = w ↔ ∃ z ∈ B ∃ w ∈ B ∅ H ∅ ∩ z H w ≠ ∅ ∧ ¬ ∅ = z ∧ ∅ = w
54 45 53 rspc2ev ⊢ ∅ ∈ B ∧ ∅ ∈ B ∧ ∃ z ∈ B ∃ w ∈ B ∅ H ∅ ∩ z H w ≠ ∅ ∧ ¬ ∅ = z ∧ ∅ = w → ∃ x ∈ B ∃ y ∈ B ∃ z ∈ B ∃ w ∈ B x H y ∩ z H w ≠ ∅ ∧ ¬ x = z ∧ y = w
55 10 10 37 54 syl3anc ⊢ φ → ∃ x ∈ B ∃ y ∈ B ∃ z ∈ B ∃ w ∈ B x H y ∩ z H w ≠ ∅ ∧ ¬ x = z ∧ y = w