Metamath Proof Explorer

Theorem dffun2

Description: Alternate definition of a function. (Contributed by NM, 29-Dec-1996)

Ref Expression
Assertion dffun2 ⊢ Fun ⁡ A ↔ Rel ⁡ A ∧ ∀ x ∀ y ∀ z x A y ∧ x A z → y = z

Proof

Step Hyp Ref Expression
1 df-fun ⊢ Fun ⁡ A ↔ Rel ⁡ A ∧ A ∘ A -1 ⊆ I
2 df-id ⊢ I = y z | y = z
3 2 sseq2i ⊢ A ∘ A -1 ⊆ I ↔ A ∘ A -1 ⊆ y z | y = z
4 df-co ⊢ A ∘ A -1 = y z | ∃ x y A -1 x ∧ x A z
5 4 sseq1i ⊢ A ∘ A -1 ⊆ y z | y = z ↔ y z | ∃ x y A -1 x ∧ x A z ⊆ y z | y = z
6 ssopab2bw ⊢ y z | ∃ x y A -1 x ∧ x A z ⊆ y z | y = z ↔ ∀ y ∀ z ∃ x y A -1 x ∧ x A z → y = z
7 3 5 6 3bitri ⊢ A ∘ A -1 ⊆ I ↔ ∀ y ∀ z ∃ x y A -1 x ∧ x A z → y = z
8 vex ⊢ y ∈ V
9 vex ⊢ x ∈ V
10 8 9 brcnv ⊢ y A -1 x ↔ x A y
11 10 anbi1i ⊢ y A -1 x ∧ x A z ↔ x A y ∧ x A z
12 11 exbii ⊢ ∃ x y A -1 x ∧ x A z ↔ ∃ x x A y ∧ x A z
13 12 imbi1i ⊢ ∃ x y A -1 x ∧ x A z → y = z ↔ ∃ x x A y ∧ x A z → y = z
14 19.23v ⊢ ∀ x x A y ∧ x A z → y = z ↔ ∃ x x A y ∧ x A z → y = z
15 13 14 bitr4i ⊢ ∃ x y A -1 x ∧ x A z → y = z ↔ ∀ x x A y ∧ x A z → y = z
16 15 albii ⊢ ∀ z ∃ x y A -1 x ∧ x A z → y = z ↔ ∀ z ∀ x x A y ∧ x A z → y = z
17 alcom ⊢ ∀ z ∀ x x A y ∧ x A z → y = z ↔ ∀ x ∀ z x A y ∧ x A z → y = z
18 16 17 bitri ⊢ ∀ z ∃ x y A -1 x ∧ x A z → y = z ↔ ∀ x ∀ z x A y ∧ x A z → y = z
19 18 albii ⊢ ∀ y ∀ z ∃ x y A -1 x ∧ x A z → y = z ↔ ∀ y ∀ x ∀ z x A y ∧ x A z → y = z
20 alcom ⊢ ∀ y ∀ x ∀ z x A y ∧ x A z → y = z ↔ ∀ x ∀ y ∀ z x A y ∧ x A z → y = z
21 7 19 20 3bitri ⊢ A ∘ A -1 ⊆ I ↔ ∀ x ∀ y ∀ z x A y ∧ x A z → y = z
22 21 anbi2i ⊢ Rel ⁡ A ∧ A ∘ A -1 ⊆ I ↔ Rel ⁡ A ∧ ∀ x ∀ y ∀ z x A y ∧ x A z → y = z
23 1 22 bitri ⊢ Fun ⁡ A ↔ Rel ⁡ A ∧ ∀ x ∀ y ∀ z x A y ∧ x A z → y = z