Metamath Proof Explorer


Theorem dffun10

Description: Another potential definition of functionality. 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 C_ ( _I o. ( _V \ ( ( _V \ _I ) o. F ) ) ) )

Proof

Step Hyp Ref Expression
1 impexp
 |-  ( ( ( <. x , y >. e. F /\ <. x , z >. e. F ) -> y = z ) <-> ( <. x , y >. e. F -> ( <. x , z >. e. F -> y = z ) ) )
2 1 albii
 |-  ( A. z ( ( <. x , y >. e. F /\ <. x , z >. e. F ) -> y = z ) <-> A. z ( <. x , y >. e. F -> ( <. x , z >. e. F -> y = z ) ) )
3 19.21v
 |-  ( A. z ( <. x , y >. e. F -> ( <. x , z >. e. F -> y = z ) ) <-> ( <. x , y >. e. F -> A. z ( <. x , z >. e. F -> y = z ) ) )
4 vex
 |-  x e. _V
5 vex
 |-  y e. _V
6 4 5 opelco
 |-  ( <. x , y >. e. ( ( _V \ _I ) o. F ) <-> E. z ( x F z /\ z ( _V \ _I ) y ) )
7 df-br
 |-  ( x F z <-> <. x , z >. e. F )
8 brv
 |-  z _V y
9 brdif
 |-  ( z ( _V \ _I ) y <-> ( z _V y /\ -. z _I y ) )
10 8 9 mpbiran
 |-  ( z ( _V \ _I ) y <-> -. z _I y )
11 5 ideq
 |-  ( z _I y <-> z = y )
12 equcom
 |-  ( z = y <-> y = z )
13 11 12 bitri
 |-  ( z _I y <-> y = z )
14 10 13 xchbinx
 |-  ( z ( _V \ _I ) y <-> -. y = z )
15 7 14 anbi12i
 |-  ( ( x F z /\ z ( _V \ _I ) y ) <-> ( <. x , z >. e. F /\ -. y = z ) )
16 15 exbii
 |-  ( E. z ( x F z /\ z ( _V \ _I ) y ) <-> E. z ( <. x , z >. e. F /\ -. y = z ) )
17 exanali
 |-  ( E. z ( <. x , z >. e. F /\ -. y = z ) <-> -. A. z ( <. x , z >. e. F -> y = z ) )
18 6 16 17 3bitri
 |-  ( <. x , y >. e. ( ( _V \ _I ) o. F ) <-> -. A. z ( <. x , z >. e. F -> y = z ) )
19 18 con2bii
 |-  ( A. z ( <. x , z >. e. F -> y = z ) <-> -. <. x , y >. e. ( ( _V \ _I ) o. F ) )
20 opex
 |-  <. x , y >. e. _V
21 eldif
 |-  ( <. x , y >. e. ( _V \ ( ( _V \ _I ) o. F ) ) <-> ( <. x , y >. e. _V /\ -. <. x , y >. e. ( ( _V \ _I ) o. F ) ) )
22 20 21 mpbiran
 |-  ( <. x , y >. e. ( _V \ ( ( _V \ _I ) o. F ) ) <-> -. <. x , y >. e. ( ( _V \ _I ) o. F ) )
23 19 22 bitr4i
 |-  ( A. z ( <. x , z >. e. F -> y = z ) <-> <. x , y >. e. ( _V \ ( ( _V \ _I ) o. F ) ) )
24 23 imbi2i
 |-  ( ( <. x , y >. e. F -> A. z ( <. x , z >. e. F -> y = z ) ) <-> ( <. x , y >. e. F -> <. x , y >. e. ( _V \ ( ( _V \ _I ) o. F ) ) ) )
25 2 3 24 3bitri
 |-  ( A. z ( ( <. x , y >. e. F /\ <. x , z >. e. F ) -> y = z ) <-> ( <. x , y >. e. F -> <. x , y >. e. ( _V \ ( ( _V \ _I ) o. F ) ) ) )
26 25 2albii
 |-  ( A. x A. y A. z ( ( <. x , y >. e. F /\ <. x , z >. e. F ) -> y = z ) <-> A. x A. y ( <. x , y >. e. F -> <. x , y >. e. ( _V \ ( ( _V \ _I ) o. F ) ) ) )
27 ssrel
 |-  ( Rel F -> ( F C_ ( _V \ ( ( _V \ _I ) o. F ) ) <-> A. x A. y ( <. x , y >. e. F -> <. x , y >. e. ( _V \ ( ( _V \ _I ) o. F ) ) ) ) )
28 26 27 bitr4id
 |-  ( Rel F -> ( A. x A. y A. z ( ( <. x , y >. e. F /\ <. x , z >. e. F ) -> y = z ) <-> F C_ ( _V \ ( ( _V \ _I ) o. F ) ) ) )
29 28 pm5.32i
 |-  ( ( Rel F /\ A. x A. y A. z ( ( <. x , y >. e. F /\ <. x , z >. e. F ) -> y = z ) ) <-> ( Rel F /\ F C_ ( _V \ ( ( _V \ _I ) o. F ) ) ) )
30 dffun4
 |-  ( Fun F <-> ( Rel F /\ A. x A. y A. z ( ( <. x , y >. e. F /\ <. x , z >. e. F ) -> y = z ) ) )
31 sscoid
 |-  ( F C_ ( _I o. ( _V \ ( ( _V \ _I ) o. F ) ) ) <-> ( Rel F /\ F C_ ( _V \ ( ( _V \ _I ) o. F ) ) ) )
32 29 30 31 3bitr4i
 |-  ( Fun F <-> F C_ ( _I o. ( _V \ ( ( _V \ _I ) o. F ) ) ) )