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

Metamath Proof Explorer

Theorem qmapeldisjs

Description: When R is a set (e.g., when it is an element of the class of relations df-rels ), the quotient map element of the class of disjoint relations and the disjoint relation predicate for quotient maps are the same. (Contributed by Peter Mazsa, 12-Feb-2026)

		Ref	Expression
	Assertion	qmapeldisjs	⊢ ( 𝑅 ∈ 𝑉 → ( QMap 𝑅 ∈ Disjs ↔ Disj QMap 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		qmapex	⊢ ( 𝑅 ∈ 𝑉 → QMap 𝑅 ∈ V )
2		eldisjsdisj	⊢ ( QMap 𝑅 ∈ V → ( QMap 𝑅 ∈ Disjs ↔ Disj QMap 𝑅 ) )
3	1 2	syl	⊢ ( 𝑅 ∈ 𝑉 → ( QMap 𝑅 ∈ Disjs ↔ Disj QMap 𝑅 ) )