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

Metamath Proof Explorer

Theorem raldmqsmo

Description: On the quotient carrier, "at most one" and "exactly one" coincide for coset witnesses. (Contributed by Peter Mazsa, 6-Feb-2026)

Ref Expression
Assertion raldmqsmo ( ∀ 𝑢 ∈ ( dom 𝑅 / 𝑅 ) ∃* 𝑡 ∈ dom 𝑅 𝑢 = [ 𝑡 ] 𝑅 ↔ ∀ 𝑢 ∈ ( dom 𝑅 / 𝑅 ) ∃! 𝑡 ∈ dom 𝑅 𝑢 = [ 𝑡 ] 𝑅 )

Proof

Step Hyp Ref Expression
1 df-qs ⊢ ( dom 𝑅 / 𝑅 ) = { 𝑢 ∣ ∃ 𝑡 ∈ dom 𝑅 𝑢 = [ 𝑡 ] 𝑅 }
2 1 eqabri ⊢ ( 𝑢 ∈ ( dom 𝑅 / 𝑅 ) ↔ ∃ 𝑡 ∈ dom 𝑅 𝑢 = [ 𝑡 ] 𝑅 )
3 2 biimpi ⊢ ( 𝑢 ∈ ( dom 𝑅 / 𝑅 ) → ∃ 𝑡 ∈ dom 𝑅 𝑢 = [ 𝑡 ] 𝑅 )
4 3 biantrurd ⊢ ( 𝑢 ∈ ( dom 𝑅 / 𝑅 ) → ( ∃* 𝑡 ∈ dom 𝑅 𝑢 = [ 𝑡 ] 𝑅 ↔ ( ∃ 𝑡 ∈ dom 𝑅 𝑢 = [ 𝑡 ] 𝑅 ∧ ∃* 𝑡 ∈ dom 𝑅 𝑢 = [ 𝑡 ] 𝑅 ) ) )
5 reu5 ⊢ ( ∃! 𝑡 ∈ dom 𝑅 𝑢 = [ 𝑡 ] 𝑅 ↔ ( ∃ 𝑡 ∈ dom 𝑅 𝑢 = [ 𝑡 ] 𝑅 ∧ ∃* 𝑡 ∈ dom 𝑅 𝑢 = [ 𝑡 ] 𝑅 ) )
6 4 5 bitr4di ⊢ ( 𝑢 ∈ ( dom 𝑅 / 𝑅 ) → ( ∃* 𝑡 ∈ dom 𝑅 𝑢 = [ 𝑡 ] 𝑅 ↔ ∃! 𝑡 ∈ dom 𝑅 𝑢 = [ 𝑡 ] 𝑅 ) )
7 6 ralbiia ⊢ ( ∀ 𝑢 ∈ ( dom 𝑅 / 𝑅 ) ∃* 𝑡 ∈ dom 𝑅 𝑢 = [ 𝑡 ] 𝑅 ↔ ∀ 𝑢 ∈ ( dom 𝑅 / 𝑅 ) ∃! 𝑡 ∈ dom 𝑅 𝑢 = [ 𝑡 ] 𝑅 )