Metamath Proof Explorer

Theorem alrmomorn

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

Ref Expression
Assertion alrmomorn ⊢ ∀ x ∃* y ∈ ran ⁡ R x R y ↔ ∀ x ∃* y x R y

Proof

Step Hyp Ref Expression
1 df-rmo ⊢ ∃* y ∈ ran ⁡ R x R y ↔ ∃* y y ∈ ran ⁡ R ∧ x R y
2 cnvresrn ⊢ R -1 ↾ ran ⁡ R = R -1
3 2 breqi ⊢ y R -1 ↾ ran ⁡ R x ↔ y R -1 x
4 brres ⊢ x ∈ V → y R -1 ↾ ran ⁡ R x ↔ y ∈ ran ⁡ R ∧ y R -1 x
5 4 elv ⊢ y R -1 ↾ ran ⁡ R x ↔ y ∈ ran ⁡ R ∧ y R -1 x
6 brcnvg ⊢ y ∈ V ∧ x ∈ V → y R -1 x ↔ x R y
7 6 el2v ⊢ y R -1 x ↔ x R y
8 7 anbi2i ⊢ y ∈ ran ⁡ R ∧ y R -1 x ↔ y ∈ ran ⁡ R ∧ x R y
9 5 8 bitri ⊢ y R -1 ↾ ran ⁡ R x ↔ y ∈ ran ⁡ R ∧ x R y
10 3 9 7 3bitr3i ⊢ y ∈ ran ⁡ R ∧ x R y ↔ x R y
11 10 mobii ⊢ ∃* y y ∈ ran ⁡ R ∧ x R y ↔ ∃* y x R y
12 1 11 bitri ⊢ ∃* y ∈ ran ⁡ R x R y ↔ ∃* y x R y
13 12 albii ⊢ ∀ x ∃* y ∈ ran ⁡ R x R y ↔ ∀ x ∃* y x R y