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 ⊢φ→≤˙=xy|x∈B∧y∈B∧xHy≠∅
Assertion catprsc ⊢φ→∀z∈B∀w∈Bz≤˙w↔zHw≠∅

Proof

Step Hyp Ref Expression
1 catprsc.1 ⊢φ→≤˙=xy|x∈B∧y∈B∧xHy≠∅
2 1 breqd ⊢φ→z≤˙w↔zxy|x∈B∧y∈B∧xHy≠∅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→xHy=zHw
10 9 neeq1d ⊢x=z∧y=w→xHy≠∅↔zHw≠∅
11 6 8 10 3anbi123d ⊢x=z∧y=w→x∈B∧y∈B∧xHy≠∅↔z∈B∧w∈B∧zHw≠∅
12 df-3an ⊢z∈B∧w∈B∧zHw≠∅↔z∈B∧w∈B∧zHw≠∅
13 11 12 bitrdi ⊢x=z∧y=w→x∈B∧y∈B∧xHy≠∅↔z∈B∧w∈B∧zHw≠∅
14 eqid ⊢xy|x∈B∧y∈B∧xHy≠∅=xy|x∈B∧y∈B∧xHy≠∅
15 3 4 13 14 braba ⊢zxy|x∈B∧y∈B∧xHy≠∅w↔z∈B∧w∈B∧zHw≠∅
16 2 15 bitrdi ⊢φ→z≤˙w↔z∈B∧w∈B∧zHw≠∅
17 16 baibd ⊢φ∧z∈B∧w∈B→z≤˙w↔zHw≠∅
18 17 ralrimivva ⊢φ→∀z∈B∀w∈Bz≤˙w↔zHw≠∅