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

Metamath Proof Explorer

Theorem inecmo3

Description: Equivalence of a double universal quantification restricted to the domain and an "at most one" inside a universal quantification. (Contributed by Peter Mazsa, 5-Sep-2021)

Ref Expression
Assertion inecmo3 ⊢ ∀ u ∈ dom ⁡ R ∀ v ∈ dom ⁡ R u = v ∨ u R ∩ v R = ∅ ∧ Rel ⁡ R ↔ ∀ x ∃* u u R x ∧ Rel ⁡ R

Proof

Step Hyp Ref Expression
1 inecmo2 ⊢ ∀ u ∈ dom ⁡ R ∀ v ∈ dom ⁡ R u = v ∨ u R ∩ v R = ∅ ∧ Rel ⁡ R ↔ ∀ x ∃* u ∈ dom ⁡ R u R x ∧ Rel ⁡ R
2 alrmomodm ⊢ Rel ⁡ R → ∀ x ∃* u ∈ dom ⁡ R u R x ↔ ∀ x ∃* u u R x
3 2 pm5.32ri ⊢ ∀ x ∃* u ∈ dom ⁡ R u R x ∧ Rel ⁡ R ↔ ∀ x ∃* u u R x ∧ Rel ⁡ R
4 1 3 bitri ⊢ ∀ u ∈ dom ⁡ R ∀ v ∈ dom ⁡ R u = v ∨ u R ∩ v R = ∅ ∧ Rel ⁡ R ↔ ∀ x ∃* u u R x ∧ Rel ⁡ R