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	⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( 𝑧 ≤ 𝑤 ↔ ( 𝑧 𝐻 𝑤 ) ≠ ∅ ) )