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 Fun F F I V V I F

Proof

Step Hyp Ref Expression
1 ssrel Rel F F V V I F x y x y F x y V V I F
2 impexp x y F x z F y = z x y F x z F y = z
3 2 albii z x y F x z F y = z z x y F x z F y = z
4 19.21v z x y F x z F y = z x y F z x z F y = z
5 vex x V
6 vex y V
7 5 6 opelco x y V I F z x F z z V I y
8 df-br x F z x z F
9 brv z V y
10 brdif z V I y z V y ¬ z I y
11 9 10 mpbiran z V I y ¬ z I y
12 6 ideq z I y z = y
13 equcom z = y y = z
14 12 13 bitri z I y y = z
15 11 14 xchbinx z V I y ¬ y = z
16 8 15 anbi12i x F z z V I y x z F ¬ y = z
17 16 exbii z x F z z V I y z x z F ¬ y = z
18 exanali z x z F ¬ y = z ¬ z x z F y = z
19 7 17 18 3bitri x y V I F ¬ z x z F y = z
20 19 con2bii z x z F y = z ¬ x y V I F
21 opex x y V
22 eldif x y V V I F x y V ¬ x y V I F
23 21 22 mpbiran x y V V I F ¬ x y V I F
24 20 23 bitr4i z x z F y = z x y V V I F
25 24 imbi2i x y F z x z F y = z x y F x y V V I F
26 3 4 25 3bitri z x y F x z F y = z x y F x y V V I F
27 26 2albii x y z x y F x z F y = z x y x y F x y V V I F
28 1 27 syl6rbbr Rel F x y z x y F x z F y = z F V V I F
29 28 pm5.32i Rel F x y z x y F x z F y = z Rel F F V V I F
30 dffun4 Fun F Rel F x y z x y F x z F y = z
31 sscoid F I V V I F Rel F F V V I F
32 29 30 31 3bitr4i Fun F F I V V I F