Theorem funcnv

Description: The converse of a class is a function iff the class is single-rooted, which means that for any y in the range of A there is at most one x such that x A y . Definition of single-rooted in Enderton p. 43. See funcnv2 for a simpler version. (Contributed by NM, 13-Aug-2004)

	Ref	Expression
Assertion	funcnv	⊢ ( Fun ◡ 𝐴 ↔ ∀ 𝑦 ∈ ran 𝐴 ∃* 𝑥 𝑥 𝐴 𝑦 )

Proof

Step	Hyp	Ref	Expression
1		vex	⊢ 𝑥 ∈ V
2		vex	⊢ 𝑦 ∈ V
3	1 2	brelrn	⊢ ( 𝑥 𝐴 𝑦 → 𝑦 ∈ ran 𝐴 )
4	3	pm4.71ri	⊢ ( 𝑥 𝐴 𝑦 ↔ ( 𝑦 ∈ ran 𝐴 ∧ 𝑥 𝐴 𝑦 ) )
5	4	mobii	⊢ ( ∃* 𝑥 𝑥 𝐴 𝑦 ↔ ∃* 𝑥 ( 𝑦 ∈ ran 𝐴 ∧ 𝑥 𝐴 𝑦 ) )
6		moanimv	⊢ ( ∃* 𝑥 ( 𝑦 ∈ ran 𝐴 ∧ 𝑥 𝐴 𝑦 ) ↔ ( 𝑦 ∈ ran 𝐴 → ∃* 𝑥 𝑥 𝐴 𝑦 ) )
7	5 6	bitri	⊢ ( ∃* 𝑥 𝑥 𝐴 𝑦 ↔ ( 𝑦 ∈ ran 𝐴 → ∃* 𝑥 𝑥 𝐴 𝑦 ) )
8	7	albii	⊢ ( ∀ 𝑦 ∃* 𝑥 𝑥 𝐴 𝑦 ↔ ∀ 𝑦 ( 𝑦 ∈ ran 𝐴 → ∃* 𝑥 𝑥 𝐴 𝑦 ) )
9		funcnv2	⊢ ( Fun ◡ 𝐴 ↔ ∀ 𝑦 ∃* 𝑥 𝑥 𝐴 𝑦 )
10		df-ral	⊢ ( ∀ 𝑦 ∈ ran 𝐴 ∃* 𝑥 𝑥 𝐴 𝑦 ↔ ∀ 𝑦 ( 𝑦 ∈ ran 𝐴 → ∃* 𝑥 𝑥 𝐴 𝑦 ) )
11	8 9 10	3bitr4i	⊢ ( Fun ◡ 𝐴 ↔ ∀ 𝑦 ∈ ran 𝐴 ∃* 𝑥 𝑥 𝐴 𝑦 )