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

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