Metamath Proof Explorer

Theorem funcnv3

Description: A condition showing a class is single-rooted. (See funcnv ). (Contributed by NM, 26-May-2006)

Ref Expression
Assertion funcnv3 ⊢ Fun ⁡ A -1 ↔ ∀ y ∈ ran ⁡ A ∃! x ∈ dom ⁡ A x A y

Proof

Step Hyp Ref Expression
1 dfrn2 ⊢ ran ⁡ A = y | ∃ x x A y
2 1 abeq2i ⊢ y ∈ ran ⁡ A ↔ ∃ x x A y
3 2 biimpi ⊢ y ∈ ran ⁡ A → ∃ x x A y
4 3 biantrurd ⊢ y ∈ ran ⁡ A → ∃* x x A y ↔ ∃ x x A y ∧ ∃* x x A y
5 4 ralbiia ⊢ ∀ y ∈ ran ⁡ A ∃* x x A y ↔ ∀ y ∈ ran ⁡ A ∃ x x A y ∧ ∃* x x A y
6 funcnv ⊢ Fun ⁡ A -1 ↔ ∀ y ∈ ran ⁡ A ∃* x x A y
7 df-reu ⊢ ∃! x ∈ dom ⁡ A x A y ↔ ∃! x x ∈ dom ⁡ A ∧ x A y
8 vex ⊢ x ∈ V
9 vex ⊢ y ∈ V
10 8 9 breldm ⊢ x A y → x ∈ dom ⁡ A
11 10 pm4.71ri ⊢ x A y ↔ x ∈ dom ⁡ A ∧ x A y
12 11 eubii ⊢ ∃! x x A y ↔ ∃! x x ∈ dom ⁡ A ∧ x A y
13 df-eu ⊢ ∃! x x A y ↔ ∃ x x A y ∧ ∃* x x A y
14 7 12 13 3bitr2i ⊢ ∃! x ∈ dom ⁡ A x A y ↔ ∃ x x A y ∧ ∃* x x A y
15 14 ralbii ⊢ ∀ y ∈ ran ⁡ A ∃! x ∈ dom ⁡ A x A y ↔ ∀ y ∈ ran ⁡ A ∃ x x A y ∧ ∃* x x A y
16 5 6 15 3bitr4i ⊢ Fun ⁡ A -1 ↔ ∀ y ∈ ran ⁡ A ∃! x ∈ dom ⁡ A x A y