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 ⊢ R ∈ V → ∀ u ∈ dom ⁡ R / R ∃! t ∈ dom ⁡ R u = t R ↔ ∀ u ∃* t ∈ dom ⁡ R u = t R

Proof

Step Hyp Ref Expression
1 raldmqsmo ⊢ ∀ u ∈ dom ⁡ R / R ∃* t ∈ dom ⁡ R u = t R ↔ ∀ u ∈ dom ⁡ R / R ∃! t ∈ dom ⁡ R u = t R
2 ralrmo3 ⊢ ∀ u ∈ dom ⁡ R / R ∃* t ∈ dom ⁡ R u = t R ↔ ∀ u ∃* t ∈ dom ⁡ R u ∈ dom ⁡ R / R ∧ u = t R
3 1 2 bitr3i ⊢ ∀ u ∈ dom ⁡ R / R ∃! t ∈ dom ⁡ R u = t R ↔ ∀ u ∃* t ∈ dom ⁡ R u ∈ dom ⁡ R / R ∧ u = t R
4 eqelb ⊢ u = t R ∧ u ∈ dom ⁡ R / R ↔ u = t R ∧ t R ∈ dom ⁡ R / R
5 ancom ⊢ u = t R ∧ u ∈ dom ⁡ R / R ↔ u ∈ dom ⁡ R / R ∧ u = t R
6 ancom ⊢ u = t R ∧ t R ∈ dom ⁡ R / R ↔ t R ∈ dom ⁡ R / R ∧ u = t R
7 4 5 6 3bitr3i ⊢ u ∈ dom ⁡ R / R ∧ u = t R ↔ t R ∈ dom ⁡ R / R ∧ u = t R
8 eceldmqs ⊢ R ∈ V → t R ∈ dom ⁡ R / R ↔ t ∈ dom ⁡ R
9 8 anbi1d ⊢ R ∈ V → t R ∈ dom ⁡ R / R ∧ u = t R ↔ t ∈ dom ⁡ R ∧ u = t R
10 7 9 bitrid ⊢ R ∈ V → u ∈ dom ⁡ R / R ∧ u = t R ↔ t ∈ dom ⁡ R ∧ u = t R
11 10 rmobidv ⊢ R ∈ V → ∃* t ∈ dom ⁡ R u ∈ dom ⁡ R / R ∧ u = t R ↔ ∃* t ∈ dom ⁡ R t ∈ dom ⁡ R ∧ u = t R
12 rmoanid ⊢ ∃* t ∈ dom ⁡ R t ∈ dom ⁡ R ∧ u = t R ↔ ∃* t ∈ dom ⁡ R u = t R
13 11 12 bitrdi ⊢ R ∈ V → ∃* t ∈ dom ⁡ R u ∈ dom ⁡ R / R ∧ u = t R ↔ ∃* t ∈ dom ⁡ R u = t R
14 13 albidv ⊢ R ∈ V → ∀ u ∃* t ∈ dom ⁡ R u ∈ dom ⁡ R / R ∧ u = t R ↔ ∀ u ∃* t ∈ dom ⁡ R u = t R
15 3 14 bitrid ⊢ R ∈ V → ∀ u ∈ dom ⁡ R / R ∃! t ∈ dom ⁡ R u = t R ↔ ∀ u ∃* t ∈ dom ⁡ R u = t R