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

Metamath Proof Explorer

Theorem raldmqseu

Description: Equivalence between "exactly one" on the quotient carrier and "at most one" globally. Provides a type-safe way to talk about unique representatives either as E! on the intended carrier or as a global E* statement. (Contributed by Peter Mazsa, 6-Feb-2026)

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

Proof

Step Hyp Ref Expression
1 raldmqsmo ⊢ ( ∀ 𝑢 ∈ ( dom 𝑅 / 𝑅 ) ∃* 𝑡 ∈ dom 𝑅 𝑢 = [ 𝑡 ] 𝑅 ↔ ∀ 𝑢 ∈ ( dom 𝑅 / 𝑅 ) ∃! 𝑡 ∈ dom 𝑅 𝑢 = [ 𝑡 ] 𝑅 )
2 ralrmo3 ⊢ ( ∀ 𝑢 ∈ ( dom 𝑅 / 𝑅 ) ∃* 𝑡 ∈ dom 𝑅 𝑢 = [ 𝑡 ] 𝑅 ↔ ∀ 𝑢 ∃* 𝑡 ∈ dom 𝑅 ( 𝑢 ∈ ( dom 𝑅 / 𝑅 ) ∧ 𝑢 = [ 𝑡 ] 𝑅 ) )
3 1 2 bitr3i ⊢ ( ∀ 𝑢 ∈ ( dom 𝑅 / 𝑅 ) ∃! 𝑡 ∈ dom 𝑅 𝑢 = [ 𝑡 ] 𝑅 ↔ ∀ 𝑢 ∃* 𝑡 ∈ dom 𝑅 ( 𝑢 ∈ ( dom 𝑅 / 𝑅 ) ∧ 𝑢 = [ 𝑡 ] 𝑅 ) )
4 eqelb ⊢ ( ( 𝑢 = [ 𝑡 ] 𝑅 ∧ 𝑢 ∈ ( dom 𝑅 / 𝑅 ) ) ↔ ( 𝑢 = [ 𝑡 ] 𝑅 ∧ [ 𝑡 ] 𝑅 ∈ ( dom 𝑅 / 𝑅 ) ) )
5 ancom ⊢ ( ( 𝑢 = [ 𝑡 ] 𝑅 ∧ 𝑢 ∈ ( dom 𝑅 / 𝑅 ) ) ↔ ( 𝑢 ∈ ( dom 𝑅 / 𝑅 ) ∧ 𝑢 = [ 𝑡 ] 𝑅 ) )
6 ancom ⊢ ( ( 𝑢 = [ 𝑡 ] 𝑅 ∧ [ 𝑡 ] 𝑅 ∈ ( dom 𝑅 / 𝑅 ) ) ↔ ( [ 𝑡 ] 𝑅 ∈ ( dom 𝑅 / 𝑅 ) ∧ 𝑢 = [ 𝑡 ] 𝑅 ) )
7 4 5 6 3bitr3i ⊢ ( ( 𝑢 ∈ ( dom 𝑅 / 𝑅 ) ∧ 𝑢 = [ 𝑡 ] 𝑅 ) ↔ ( [ 𝑡 ] 𝑅 ∈ ( dom 𝑅 / 𝑅 ) ∧ 𝑢 = [ 𝑡 ] 𝑅 ) )
8 eceldmqs ⊢ ( 𝑅 ∈ 𝑉 → ( [ 𝑡 ] 𝑅 ∈ ( dom 𝑅 / 𝑅 ) ↔ 𝑡 ∈ dom 𝑅 ) )
9 8 anbi1d ⊢ ( 𝑅 ∈ 𝑉 → ( ( [ 𝑡 ] 𝑅 ∈ ( dom 𝑅 / 𝑅 ) ∧ 𝑢 = [ 𝑡 ] 𝑅 ) ↔ ( 𝑡 ∈ dom 𝑅 ∧ 𝑢 = [ 𝑡 ] 𝑅 ) ) )
10 7 9 bitrid ⊢ ( 𝑅 ∈ 𝑉 → ( ( 𝑢 ∈ ( dom 𝑅 / 𝑅 ) ∧ 𝑢 = [ 𝑡 ] 𝑅 ) ↔ ( 𝑡 ∈ dom 𝑅 ∧ 𝑢 = [ 𝑡 ] 𝑅 ) ) )
11 10 rmobidv ⊢ ( 𝑅 ∈ 𝑉 → ( ∃* 𝑡 ∈ dom 𝑅 ( 𝑢 ∈ ( dom 𝑅 / 𝑅 ) ∧ 𝑢 = [ 𝑡 ] 𝑅 ) ↔ ∃* 𝑡 ∈ dom 𝑅 ( 𝑡 ∈ dom 𝑅 ∧ 𝑢 = [ 𝑡 ] 𝑅 ) ) )
12 rmoanid ⊢ ( ∃* 𝑡 ∈ dom 𝑅 ( 𝑡 ∈ dom 𝑅 ∧ 𝑢 = [ 𝑡 ] 𝑅 ) ↔ ∃* 𝑡 ∈ dom 𝑅 𝑢 = [ 𝑡 ] 𝑅 )
13 11 12 bitrdi ⊢ ( 𝑅 ∈ 𝑉 → ( ∃* 𝑡 ∈ dom 𝑅 ( 𝑢 ∈ ( dom 𝑅 / 𝑅 ) ∧ 𝑢 = [ 𝑡 ] 𝑅 ) ↔ ∃* 𝑡 ∈ dom 𝑅 𝑢 = [ 𝑡 ] 𝑅 ) )
14 13 albidv ⊢ ( 𝑅 ∈ 𝑉 → ( ∀ 𝑢 ∃* 𝑡 ∈ dom 𝑅 ( 𝑢 ∈ ( dom 𝑅 / 𝑅 ) ∧ 𝑢 = [ 𝑡 ] 𝑅 ) ↔ ∀ 𝑢 ∃* 𝑡 ∈ dom 𝑅 𝑢 = [ 𝑡 ] 𝑅 ) )
15 3 14 bitrid ⊢ ( 𝑅 ∈ 𝑉 → ( ∀ 𝑢 ∈ ( dom 𝑅 / 𝑅 ) ∃! 𝑡 ∈ dom 𝑅 𝑢 = [ 𝑡 ] 𝑅 ↔ ∀ 𝑢 ∃* 𝑡 ∈ dom 𝑅 𝑢 = [ 𝑡 ] 𝑅 ) )