This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( 𝜑 → ≤ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ ( 𝑥 𝐻 𝑦 ) ≠ ∅ ) } )
Assertion catprsc ( 𝜑 → ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( 𝑧 ≤ 𝑤 ↔ ( 𝑧 𝐻 𝑤 ) ≠ ∅ ) )

Proof

Step Hyp Ref Expression
1 catprsc.1 ⊢ ( 𝜑 → ≤ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ ( 𝑥 𝐻 𝑦 ) ≠ ∅ ) } )
2 1 breqd ⊢ ( 𝜑 → ( 𝑧 ≤ 𝑤 ↔ 𝑧 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ ( 𝑥 𝐻 𝑦 ) ≠ ∅ ) } 𝑤 ) )
3 vex ⊢ 𝑧 ∈ V
4 vex ⊢ 𝑤 ∈ V
5 simpl ⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → 𝑥 = 𝑧 )
6 5 eleq1d ⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( 𝑥 ∈ 𝐵 ↔ 𝑧 ∈ 𝐵 ) )
7 simpr ⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → 𝑦 = 𝑤 )
8 7 eleq1d ⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( 𝑦 ∈ 𝐵 ↔ 𝑤 ∈ 𝐵 ) )
9 oveq12 ⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( 𝑥 𝐻 𝑦 ) = ( 𝑧 𝐻 𝑤 ) )
10 9 neeq1d ⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( ( 𝑥 𝐻 𝑦 ) ≠ ∅ ↔ ( 𝑧 𝐻 𝑤 ) ≠ ∅ ) )
11 6 8 10 3anbi123d ⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ ( 𝑥 𝐻 𝑦 ) ≠ ∅ ) ↔ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ( 𝑧 𝐻 𝑤 ) ≠ ∅ ) ) )
12 df-3an ⊢ ( ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ∧ ( 𝑧 𝐻 𝑤 ) ≠ ∅ ) ↔ ( ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑧 𝐻 𝑤 ) ≠ ∅ ) )
13 11 12 bitrdi ⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ ( 𝑥 𝐻 𝑦 ) ≠ ∅ ) ↔ ( ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑧 𝐻 𝑤 ) ≠ ∅ ) ) )
14 eqid ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ ( 𝑥 𝐻 𝑦 ) ≠ ∅ ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ ( 𝑥 𝐻 𝑦 ) ≠ ∅ ) }
15 3 4 13 14 braba ⊢ ( 𝑧 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ ( 𝑥 𝐻 𝑦 ) ≠ ∅ ) } 𝑤 ↔ ( ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑧 𝐻 𝑤 ) ≠ ∅ ) )
16 2 15 bitrdi ⊢ ( 𝜑 → ( 𝑧 ≤ 𝑤 ↔ ( ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝑧 𝐻 𝑤 ) ≠ ∅ ) ) )
17 16 baibd ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( 𝑧 ≤ 𝑤 ↔ ( 𝑧 𝐻 𝑤 ) ≠ ∅ ) )
18 17 ralrimivva ⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( 𝑧 ≤ 𝑤 ↔ ( 𝑧 𝐻 𝑤 ) ≠ ∅ ) )