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

Metamath Proof Explorer

Theorem disjqmap

Description: Disjointness of QMap equals unique generation of the quotient carrier. The cleaned, carrier-respecting version of disjqmap2 . This is the statement "each equivalence class has a unique representative" for the general coset carrier ( dom R /. R ) . (Contributed by Peter Mazsa, 12-Feb-2026)

		Ref	Expression
	Assertion	disjqmap	⊢ ( 𝑅 ∈ 𝑉 → ( Disj QMap 𝑅 ↔ ∀ 𝑢 ∈ ( dom 𝑅 / 𝑅 ) ∃! 𝑡 ∈ dom 𝑅 𝑢 = [ 𝑡 ] 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		disjqmap2	⊢ ( 𝑅 ∈ 𝑉 → ( Disj QMap 𝑅 ↔ ∀ 𝑢 ∃* 𝑡 ∈ dom 𝑅 𝑢 = [ 𝑡 ] 𝑅 ) )
2		raldmqseu	⊢ ( 𝑅 ∈ 𝑉 → ( ∀ 𝑢 ∈ ( dom 𝑅 / 𝑅 ) ∃! 𝑡 ∈ dom 𝑅 𝑢 = [ 𝑡 ] 𝑅 ↔ ∀ 𝑢 ∃* 𝑡 ∈ dom 𝑅 𝑢 = [ 𝑡 ] 𝑅 ) )
3	1 2	bitr4d	⊢ ( 𝑅 ∈ 𝑉 → ( Disj QMap 𝑅 ↔ ∀ 𝑢 ∈ ( dom 𝑅 / 𝑅 ) ∃! 𝑡 ∈ dom 𝑅 𝑢 = [ 𝑡 ] 𝑅 ) )