Metamath Proof Explorer

Theorem catprsc

Description: A construction of the preorder induced by a category. See catprs2 for details. See also catprsc2 for an alternate construction. (Contributed by Zhi Wang, 18-Sep-2024)

Ref Expression
Hypothesis catprsc.1 ⊢ φ → ≤ ˙ = x y | x ∈ B ∧ y ∈ B ∧ x H y ≠ ∅
Assertion catprsc ⊢ φ → ∀ z ∈ B ∀ w ∈ B z ≤ ˙ w ↔ z H w ≠ ∅

Proof

Step Hyp Ref Expression
1 catprsc.1 ⊢ φ → ≤ ˙ = x y | x ∈ B ∧ y ∈ B ∧ x H y ≠ ∅
2 1 breqd ⊢ φ → z ≤ ˙ w ↔ z x y | x ∈ B ∧ y ∈ B ∧ x H y ≠ ∅ w
3 vex ⊢ z ∈ V
4 vex ⊢ w ∈ V
5 simpl ⊢ x = z ∧ y = w → x = z
6 5 eleq1d ⊢ x = z ∧ y = w → x ∈ B ↔ z ∈ B
7 simpr ⊢ x = z ∧ y = w → y = w
8 7 eleq1d ⊢ x = z ∧ y = w → y ∈ B ↔ w ∈ B
9 oveq12 ⊢ x = z ∧ y = w → x H y = z H w
10 9 neeq1d ⊢ x = z ∧ y = w → x H y ≠ ∅ ↔ z H w ≠ ∅
11 6 8 10 3anbi123d ⊢ x = z ∧ y = w → x ∈ B ∧ y ∈ B ∧ x H y ≠ ∅ ↔ z ∈ B ∧ w ∈ B ∧ z H w ≠ ∅
12 df-3an ⊢ z ∈ B ∧ w ∈ B ∧ z H w ≠ ∅ ↔ z ∈ B ∧ w ∈ B ∧ z H w ≠ ∅
13 11 12 bitrdi ⊢ x = z ∧ y = w → x ∈ B ∧ y ∈ B ∧ x H y ≠ ∅ ↔ z ∈ B ∧ w ∈ B ∧ z H w ≠ ∅
14 eqid ⊢ x y | x ∈ B ∧ y ∈ B ∧ x H y ≠ ∅ = x y | x ∈ B ∧ y ∈ B ∧ x H y ≠ ∅
15 3 4 13 14 braba ⊢ z x y | x ∈ B ∧ y ∈ B ∧ x H y ≠ ∅ w ↔ z ∈ B ∧ w ∈ B ∧ z H w ≠ ∅
16 2 15 bitrdi ⊢ φ → z ≤ ˙ w ↔ z ∈ B ∧ w ∈ B ∧ z H w ≠ ∅
17 16 baibd ⊢ φ ∧ z ∈ B ∧ w ∈ B → z ≤ ˙ w ↔ z H w ≠ ∅
18 17 ralrimivva ⊢ φ → ∀ z ∈ B ∀ w ∈ B z ≤ ˙ w ↔ z H w ≠ ∅