# Metamath Proof Explorer

## Theorem dffun10

Description: Another potential definition of functionhood. Based on statements in http://people.math.gatech.edu/~belinfan/research/autoreas/otter/sum/fs/ . (Contributed by Scott Fenton, 30-Aug-2017)

Ref Expression
Assertion dffun10 ${⊢}\mathrm{Fun}{F}↔{F}\subseteq \mathrm{I}\circ \left(\mathrm{V}\setminus \left(\left(\mathrm{V}\setminus \mathrm{I}\right)\circ {F}\right)\right)$

### Proof

Step Hyp Ref Expression
1 ssrel ${⊢}\mathrm{Rel}{F}\to \left({F}\subseteq \mathrm{V}\setminus \left(\left(\mathrm{V}\setminus \mathrm{I}\right)\circ {F}\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(⟨{x},{y}⟩\in {F}\to ⟨{x},{y}⟩\in \left(\mathrm{V}\setminus \left(\left(\mathrm{V}\setminus \mathrm{I}\right)\circ {F}\right)\right)\right)\right)$
2 impexp ${⊢}\left(\left(⟨{x},{y}⟩\in {F}\wedge ⟨{x},{z}⟩\in {F}\right)\to {y}={z}\right)↔\left(⟨{x},{y}⟩\in {F}\to \left(⟨{x},{z}⟩\in {F}\to {y}={z}\right)\right)$
3 2 albii ${⊢}\forall {z}\phantom{\rule{.4em}{0ex}}\left(\left(⟨{x},{y}⟩\in {F}\wedge ⟨{x},{z}⟩\in {F}\right)\to {y}={z}\right)↔\forall {z}\phantom{\rule{.4em}{0ex}}\left(⟨{x},{y}⟩\in {F}\to \left(⟨{x},{z}⟩\in {F}\to {y}={z}\right)\right)$
4 19.21v ${⊢}\forall {z}\phantom{\rule{.4em}{0ex}}\left(⟨{x},{y}⟩\in {F}\to \left(⟨{x},{z}⟩\in {F}\to {y}={z}\right)\right)↔\left(⟨{x},{y}⟩\in {F}\to \forall {z}\phantom{\rule{.4em}{0ex}}\left(⟨{x},{z}⟩\in {F}\to {y}={z}\right)\right)$
5 vex ${⊢}{x}\in \mathrm{V}$
6 vex ${⊢}{y}\in \mathrm{V}$
7 5 6 opelco ${⊢}⟨{x},{y}⟩\in \left(\left(\mathrm{V}\setminus \mathrm{I}\right)\circ {F}\right)↔\exists {z}\phantom{\rule{.4em}{0ex}}\left({x}{F}{z}\wedge {z}\left(\mathrm{V}\setminus \mathrm{I}\right){y}\right)$
8 df-br ${⊢}{x}{F}{z}↔⟨{x},{z}⟩\in {F}$
9 brv ${⊢}{z}\mathrm{V}{y}$
10 brdif ${⊢}{z}\left(\mathrm{V}\setminus \mathrm{I}\right){y}↔\left({z}\mathrm{V}{y}\wedge ¬{z}\mathrm{I}{y}\right)$
11 9 10 mpbiran ${⊢}{z}\left(\mathrm{V}\setminus \mathrm{I}\right){y}↔¬{z}\mathrm{I}{y}$
12 6 ideq ${⊢}{z}\mathrm{I}{y}↔{z}={y}$
13 equcom ${⊢}{z}={y}↔{y}={z}$
14 12 13 bitri ${⊢}{z}\mathrm{I}{y}↔{y}={z}$
15 11 14 xchbinx ${⊢}{z}\left(\mathrm{V}\setminus \mathrm{I}\right){y}↔¬{y}={z}$
16 8 15 anbi12i ${⊢}\left({x}{F}{z}\wedge {z}\left(\mathrm{V}\setminus \mathrm{I}\right){y}\right)↔\left(⟨{x},{z}⟩\in {F}\wedge ¬{y}={z}\right)$
17 16 exbii ${⊢}\exists {z}\phantom{\rule{.4em}{0ex}}\left({x}{F}{z}\wedge {z}\left(\mathrm{V}\setminus \mathrm{I}\right){y}\right)↔\exists {z}\phantom{\rule{.4em}{0ex}}\left(⟨{x},{z}⟩\in {F}\wedge ¬{y}={z}\right)$
18 exanali ${⊢}\exists {z}\phantom{\rule{.4em}{0ex}}\left(⟨{x},{z}⟩\in {F}\wedge ¬{y}={z}\right)↔¬\forall {z}\phantom{\rule{.4em}{0ex}}\left(⟨{x},{z}⟩\in {F}\to {y}={z}\right)$
19 7 17 18 3bitri ${⊢}⟨{x},{y}⟩\in \left(\left(\mathrm{V}\setminus \mathrm{I}\right)\circ {F}\right)↔¬\forall {z}\phantom{\rule{.4em}{0ex}}\left(⟨{x},{z}⟩\in {F}\to {y}={z}\right)$
20 19 con2bii ${⊢}\forall {z}\phantom{\rule{.4em}{0ex}}\left(⟨{x},{z}⟩\in {F}\to {y}={z}\right)↔¬⟨{x},{y}⟩\in \left(\left(\mathrm{V}\setminus \mathrm{I}\right)\circ {F}\right)$
21 opex ${⊢}⟨{x},{y}⟩\in \mathrm{V}$
22 eldif ${⊢}⟨{x},{y}⟩\in \left(\mathrm{V}\setminus \left(\left(\mathrm{V}\setminus \mathrm{I}\right)\circ {F}\right)\right)↔\left(⟨{x},{y}⟩\in \mathrm{V}\wedge ¬⟨{x},{y}⟩\in \left(\left(\mathrm{V}\setminus \mathrm{I}\right)\circ {F}\right)\right)$
23 21 22 mpbiran ${⊢}⟨{x},{y}⟩\in \left(\mathrm{V}\setminus \left(\left(\mathrm{V}\setminus \mathrm{I}\right)\circ {F}\right)\right)↔¬⟨{x},{y}⟩\in \left(\left(\mathrm{V}\setminus \mathrm{I}\right)\circ {F}\right)$
24 20 23 bitr4i ${⊢}\forall {z}\phantom{\rule{.4em}{0ex}}\left(⟨{x},{z}⟩\in {F}\to {y}={z}\right)↔⟨{x},{y}⟩\in \left(\mathrm{V}\setminus \left(\left(\mathrm{V}\setminus \mathrm{I}\right)\circ {F}\right)\right)$
25 24 imbi2i ${⊢}\left(⟨{x},{y}⟩\in {F}\to \forall {z}\phantom{\rule{.4em}{0ex}}\left(⟨{x},{z}⟩\in {F}\to {y}={z}\right)\right)↔\left(⟨{x},{y}⟩\in {F}\to ⟨{x},{y}⟩\in \left(\mathrm{V}\setminus \left(\left(\mathrm{V}\setminus \mathrm{I}\right)\circ {F}\right)\right)\right)$
26 3 4 25 3bitri ${⊢}\forall {z}\phantom{\rule{.4em}{0ex}}\left(\left(⟨{x},{y}⟩\in {F}\wedge ⟨{x},{z}⟩\in {F}\right)\to {y}={z}\right)↔\left(⟨{x},{y}⟩\in {F}\to ⟨{x},{y}⟩\in \left(\mathrm{V}\setminus \left(\left(\mathrm{V}\setminus \mathrm{I}\right)\circ {F}\right)\right)\right)$
27 26 2albii ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left(\left(⟨{x},{y}⟩\in {F}\wedge ⟨{x},{z}⟩\in {F}\right)\to {y}={z}\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(⟨{x},{y}⟩\in {F}\to ⟨{x},{y}⟩\in \left(\mathrm{V}\setminus \left(\left(\mathrm{V}\setminus \mathrm{I}\right)\circ {F}\right)\right)\right)$
28 1 27 syl6rbbr ${⊢}\mathrm{Rel}{F}\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left(\left(⟨{x},{y}⟩\in {F}\wedge ⟨{x},{z}⟩\in {F}\right)\to {y}={z}\right)↔{F}\subseteq \mathrm{V}\setminus \left(\left(\mathrm{V}\setminus \mathrm{I}\right)\circ {F}\right)\right)$
29 28 pm5.32i ${⊢}\left(\mathrm{Rel}{F}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left(\left(⟨{x},{y}⟩\in {F}\wedge ⟨{x},{z}⟩\in {F}\right)\to {y}={z}\right)\right)↔\left(\mathrm{Rel}{F}\wedge {F}\subseteq \mathrm{V}\setminus \left(\left(\mathrm{V}\setminus \mathrm{I}\right)\circ {F}\right)\right)$
30 dffun4 ${⊢}\mathrm{Fun}{F}↔\left(\mathrm{Rel}{F}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left(\left(⟨{x},{y}⟩\in {F}\wedge ⟨{x},{z}⟩\in {F}\right)\to {y}={z}\right)\right)$
31 sscoid ${⊢}{F}\subseteq \mathrm{I}\circ \left(\mathrm{V}\setminus \left(\left(\mathrm{V}\setminus \mathrm{I}\right)\circ {F}\right)\right)↔\left(\mathrm{Rel}{F}\wedge {F}\subseteq \mathrm{V}\setminus \left(\left(\mathrm{V}\setminus \mathrm{I}\right)\circ {F}\right)\right)$
32 29 30 31 3bitr4i ${⊢}\mathrm{Fun}{F}↔{F}\subseteq \mathrm{I}\circ \left(\mathrm{V}\setminus \left(\left(\mathrm{V}\setminus \mathrm{I}\right)\circ {F}\right)\right)$