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 ( ∀ 𝑥 ∃* 𝑦 ∈ ran 𝑅 𝑥 𝑅 𝑦 ↔ ∀ 𝑥 ∃* 𝑦 𝑥 𝑅 𝑦 )

Proof

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