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 ) ) ) )