catprsc2

Description: An alternate construction of the preorder induced by a category. See catprs2 for details. See also catprsc for a different construction. The two constructions are different because df-cat does not require the domain of H to be B X. B . (Contributed by Zhi Wang, 23-Sep-2024)

		Ref	Expression
	Hypothesis	catprsc2.1	⊢ ( 𝜑 → ≤ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 𝐻 𝑦 ) ≠ ∅ } )
	Assertion	catprsc2	⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( 𝑧 ≤ 𝑤 ↔ ( 𝑧 𝐻 𝑤 ) ≠ ∅ ) )

Proof

Step	Hyp	Ref	Expression
1		catprsc2.1	⊢ ( 𝜑 → ≤ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 𝐻 𝑦 ) ≠ ∅ } )
2	1	breqd	⊢ ( 𝜑 → ( 𝑧 ≤ 𝑤 ↔ 𝑧 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 𝐻 𝑦 ) ≠ ∅ } 𝑤 ) )
3		vex	⊢ 𝑧 ∈ V
4		vex	⊢ 𝑤 ∈ V
5		oveq12	⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( 𝑥 𝐻 𝑦 ) = ( 𝑧 𝐻 𝑤 ) )
6	5	neeq1d	⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → ( ( 𝑥 𝐻 𝑦 ) ≠ ∅ ↔ ( 𝑧 𝐻 𝑤 ) ≠ ∅ ) )
7		eqid	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 𝐻 𝑦 ) ≠ ∅ } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 𝐻 𝑦 ) ≠ ∅ }
8	3 4 6 7	braba	⊢ ( 𝑧 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 𝐻 𝑦 ) ≠ ∅ } 𝑤 ↔ ( 𝑧 𝐻 𝑤 ) ≠ ∅ )
9	2 8	bitrdi	⊢ ( 𝜑 → ( 𝑧 ≤ 𝑤 ↔ ( 𝑧 𝐻 𝑤 ) ≠ ∅ ) )
10	9	adantr	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( 𝑧 ≤ 𝑤 ↔ ( 𝑧 𝐻 𝑤 ) ≠ ∅ ) )
11	10	ralrimivva	⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( 𝑧 ≤ 𝑤 ↔ ( 𝑧 𝐻 𝑤 ) ≠ ∅ ) )

Metamath Proof Explorer

Theorem catprsc2

Proof