Metamath Proof Explorer

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 ⁡ A -1 ↔ ∀ y ∈ ran ⁡ A ∃* x x A y

Proof

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