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