This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem elfuns

Description: Membership in the class of all functions. (Contributed by Scott Fenton, 18-Feb-2013)

Ref Expression
Hypothesis elfuns.1 
|- F e. _V
Assertion elfuns 
|- ( F e. Funs <-> Fun F )

Proof

Step Hyp Ref Expression
1 elfuns.1 
 |-  F e. _V
2 elrel 
 |-  ( ( Rel F /\ p e. F ) -> E. x E. y p = <. x , y >. )
3 2 ex 
 |-  ( Rel F -> ( p e. F -> E. x E. y p = <. x , y >. ) )
4 elrel 
 |-  ( ( Rel F /\ q e. F ) -> E. a E. z q = <. a , z >. )
5 4 ex 
 |-  ( Rel F -> ( q e. F -> E. a E. z q = <. a , z >. ) )
6 3 5 anim12d 
 |-  ( Rel F -> ( ( p e. F /\ q e. F ) -> ( E. x E. y p = <. x , y >. /\ E. a E. z q = <. a , z >. ) ) )
7 6 adantrd 
 |-  ( Rel F -> ( ( ( p e. F /\ q e. F ) /\ q ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) p ) -> ( E. x E. y p = <. x , y >. /\ E. a E. z q = <. a , z >. ) ) )
8 7 pm4.71rd 
 |-  ( Rel F -> ( ( ( p e. F /\ q e. F ) /\ q ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) p ) <-> ( ( E. x E. y p = <. x , y >. /\ E. a E. z q = <. a , z >. ) /\ ( ( p e. F /\ q e. F ) /\ q ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) p ) ) ) )
9 19.41vvvv 
 |-  ( E. x E. y E. a E. z ( ( p = <. x , y >. /\ q = <. a , z >. ) /\ ( ( p e. F /\ q e. F ) /\ q ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) p ) ) <-> ( E. x E. y E. a E. z ( p = <. x , y >. /\ q = <. a , z >. ) /\ ( ( p e. F /\ q e. F ) /\ q ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) p ) ) )
10 ee4anv 
 |-  ( E. x E. y E. a E. z ( p = <. x , y >. /\ q = <. a , z >. ) <-> ( E. x E. y p = <. x , y >. /\ E. a E. z q = <. a , z >. ) )
11 10 anbi1i 
 |-  ( ( E. x E. y E. a E. z ( p = <. x , y >. /\ q = <. a , z >. ) /\ ( ( p e. F /\ q e. F ) /\ q ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) p ) ) <-> ( ( E. x E. y p = <. x , y >. /\ E. a E. z q = <. a , z >. ) /\ ( ( p e. F /\ q e. F ) /\ q ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) p ) ) )
12 9 11 bitr2i 
 |-  ( ( ( E. x E. y p = <. x , y >. /\ E. a E. z q = <. a , z >. ) /\ ( ( p e. F /\ q e. F ) /\ q ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) p ) ) <-> E. x E. y E. a E. z ( ( p = <. x , y >. /\ q = <. a , z >. ) /\ ( ( p e. F /\ q e. F ) /\ q ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) p ) ) )
13 8 12 bitrdi 
 |-  ( Rel F -> ( ( ( p e. F /\ q e. F ) /\ q ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) p ) <-> E. x E. y E. a E. z ( ( p = <. x , y >. /\ q = <. a , z >. ) /\ ( ( p e. F /\ q e. F ) /\ q ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) p ) ) ) )
14 13 2exbidv 
 |-  ( Rel F -> ( E. p E. q ( ( p e. F /\ q e. F ) /\ q ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) p ) <-> E. p E. q E. x E. y E. a E. z ( ( p = <. x , y >. /\ q = <. a , z >. ) /\ ( ( p e. F /\ q e. F ) /\ q ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) p ) ) ) )
15 excom13 
 |-  ( E. p E. q E. x E. y E. a E. z ( ( p = <. x , y >. /\ q = <. a , z >. ) /\ ( ( p e. F /\ q e. F ) /\ q ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) p ) ) <-> E. x E. q E. p E. y E. a E. z ( ( p = <. x , y >. /\ q = <. a , z >. ) /\ ( ( p e. F /\ q e. F ) /\ q ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) p ) ) )
16 excom13 
 |-  ( E. q E. p E. y E. a E. z ( ( p = <. x , y >. /\ q = <. a , z >. ) /\ ( ( p e. F /\ q e. F ) /\ q ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) p ) ) <-> E. y E. p E. q E. a E. z ( ( p = <. x , y >. /\ q = <. a , z >. ) /\ ( ( p e. F /\ q e. F ) /\ q ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) p ) ) )
17 exrot4 
 |-  ( E. p E. q E. a E. z ( ( p = <. x , y >. /\ q = <. a , z >. ) /\ ( ( p e. F /\ q e. F ) /\ q ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) p ) ) <-> E. a E. z E. p E. q ( ( p = <. x , y >. /\ q = <. a , z >. ) /\ ( ( p e. F /\ q e. F ) /\ q ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) p ) ) )
18 excom 
 |-  ( E. a E. z E. p E. q ( ( p = <. x , y >. /\ q = <. a , z >. ) /\ ( ( p e. F /\ q e. F ) /\ q ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) p ) ) <-> E. z E. a E. p E. q ( ( p = <. x , y >. /\ q = <. a , z >. ) /\ ( ( p e. F /\ q e. F ) /\ q ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) p ) ) )
19 df-3an 
 |-  ( ( p = <. x , y >. /\ q = <. a , z >. /\ ( ( p e. F /\ q e. F ) /\ q ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) p ) ) <-> ( ( p = <. x , y >. /\ q = <. a , z >. ) /\ ( ( p e. F /\ q e. F ) /\ q ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) p ) ) )
20 19 2exbii 
 |-  ( E. p E. q ( p = <. x , y >. /\ q = <. a , z >. /\ ( ( p e. F /\ q e. F ) /\ q ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) p ) ) <-> E. p E. q ( ( p = <. x , y >. /\ q = <. a , z >. ) /\ ( ( p e. F /\ q e. F ) /\ q ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) p ) ) )
21 opex 
 |-  <. x , y >. e. _V
22 opex 
 |-  <. a , z >. e. _V
23 eleq1 
 |-  ( p = <. x , y >. -> ( p e. F <-> <. x , y >. e. F ) )
24 23 anbi1d 
 |-  ( p = <. x , y >. -> ( ( p e. F /\ q e. F ) <-> ( <. x , y >. e. F /\ q e. F ) ) )
25 breq2 
 |-  ( p = <. x , y >. -> ( q ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) p <-> q ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) <. x , y >. ) )
26 24 25 anbi12d 
 |-  ( p = <. x , y >. -> ( ( ( p e. F /\ q e. F ) /\ q ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) p ) <-> ( ( <. x , y >. e. F /\ q e. F ) /\ q ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) <. x , y >. ) ) )
27 eleq1 
 |-  ( q = <. a , z >. -> ( q e. F <-> <. a , z >. e. F ) )
28 27 anbi2d 
 |-  ( q = <. a , z >. -> ( ( <. x , y >. e. F /\ q e. F ) <-> ( <. x , y >. e. F /\ <. a , z >. e. F ) ) )
29 breq1 
 |-  ( q = <. a , z >. -> ( q ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) <. x , y >. <-> <. a , z >. ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) <. x , y >. ) )
30 vex 
 |-  x e. _V
31 vex 
 |-  y e. _V
32 22 30 31 brtxp 
 |-  ( <. a , z >. ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) <. x , y >. <-> ( <. a , z >. 1st x /\ <. a , z >. ( ( _V \ _I ) o. 2nd ) y ) )
33 vex 
 |-  a e. _V
34 vex 
 |-  z e. _V
35 33 34 br1steq 
 |-  ( <. a , z >. 1st x <-> x = a )
36 equcom 
 |-  ( x = a <-> a = x )
37 35 36 bitri 
 |-  ( <. a , z >. 1st x <-> a = x )
38 22 31 brco 
 |-  ( <. a , z >. ( ( _V \ _I ) o. 2nd ) y <-> E. x ( <. a , z >. 2nd x /\ x ( _V \ _I ) y ) )
39 33 34 br2ndeq 
 |-  ( <. a , z >. 2nd x <-> x = z )
40 39 anbi1i 
 |-  ( ( <. a , z >. 2nd x /\ x ( _V \ _I ) y ) <-> ( x = z /\ x ( _V \ _I ) y ) )
41 40 exbii 
 |-  ( E. x ( <. a , z >. 2nd x /\ x ( _V \ _I ) y ) <-> E. x ( x = z /\ x ( _V \ _I ) y ) )
42 breq1 
 |-  ( x = z -> ( x ( _V \ _I ) y <-> z ( _V \ _I ) y ) )
43 brv 
 |-  z _V y
44 brdif 
 |-  ( z ( _V \ _I ) y <-> ( z _V y /\ -. z _I y ) )
45 43 44 mpbiran 
 |-  ( z ( _V \ _I ) y <-> -. z _I y )
46 31 ideq 
 |-  ( z _I y <-> z = y )
47 equcom 
 |-  ( z = y <-> y = z )
48 46 47 bitri 
 |-  ( z _I y <-> y = z )
49 48 notbii 
 |-  ( -. z _I y <-> -. y = z )
50 45 49 bitri 
 |-  ( z ( _V \ _I ) y <-> -. y = z )
51 42 50 bitrdi 
 |-  ( x = z -> ( x ( _V \ _I ) y <-> -. y = z ) )
52 51 equsexvw 
 |-  ( E. x ( x = z /\ x ( _V \ _I ) y ) <-> -. y = z )
53 38 41 52 3bitri 
 |-  ( <. a , z >. ( ( _V \ _I ) o. 2nd ) y <-> -. y = z )
54 37 53 anbi12i 
 |-  ( ( <. a , z >. 1st x /\ <. a , z >. ( ( _V \ _I ) o. 2nd ) y ) <-> ( a = x /\ -. y = z ) )
55 32 54 bitri 
 |-  ( <. a , z >. ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) <. x , y >. <-> ( a = x /\ -. y = z ) )
56 29 55 bitrdi 
 |-  ( q = <. a , z >. -> ( q ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) <. x , y >. <-> ( a = x /\ -. y = z ) ) )
57 28 56 anbi12d 
 |-  ( q = <. a , z >. -> ( ( ( <. x , y >. e. F /\ q e. F ) /\ q ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) <. x , y >. ) <-> ( ( <. x , y >. e. F /\ <. a , z >. e. F ) /\ ( a = x /\ -. y = z ) ) ) )
58 an12 
 |-  ( ( ( <. x , y >. e. F /\ <. a , z >. e. F ) /\ ( a = x /\ -. y = z ) ) <-> ( a = x /\ ( ( <. x , y >. e. F /\ <. a , z >. e. F ) /\ -. y = z ) ) )
59 57 58 bitrdi 
 |-  ( q = <. a , z >. -> ( ( ( <. x , y >. e. F /\ q e. F ) /\ q ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) <. x , y >. ) <-> ( a = x /\ ( ( <. x , y >. e. F /\ <. a , z >. e. F ) /\ -. y = z ) ) ) )
60 21 22 26 59 ceqsex2v 
 |-  ( E. p E. q ( p = <. x , y >. /\ q = <. a , z >. /\ ( ( p e. F /\ q e. F ) /\ q ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) p ) ) <-> ( a = x /\ ( ( <. x , y >. e. F /\ <. a , z >. e. F ) /\ -. y = z ) ) )
61 20 60 bitr3i 
 |-  ( E. p E. q ( ( p = <. x , y >. /\ q = <. a , z >. ) /\ ( ( p e. F /\ q e. F ) /\ q ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) p ) ) <-> ( a = x /\ ( ( <. x , y >. e. F /\ <. a , z >. e. F ) /\ -. y = z ) ) )
62 61 exbii 
 |-  ( E. a E. p E. q ( ( p = <. x , y >. /\ q = <. a , z >. ) /\ ( ( p e. F /\ q e. F ) /\ q ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) p ) ) <-> E. a ( a = x /\ ( ( <. x , y >. e. F /\ <. a , z >. e. F ) /\ -. y = z ) ) )
63 opeq1 
 |-  ( a = x -> <. a , z >. = <. x , z >. )
64 63 eleq1d 
 |-  ( a = x -> ( <. a , z >. e. F <-> <. x , z >. e. F ) )
65 64 anbi2d 
 |-  ( a = x -> ( ( <. x , y >. e. F /\ <. a , z >. e. F ) <-> ( <. x , y >. e. F /\ <. x , z >. e. F ) ) )
66 65 anbi1d 
 |-  ( a = x -> ( ( ( <. x , y >. e. F /\ <. a , z >. e. F ) /\ -. y = z ) <-> ( ( <. x , y >. e. F /\ <. x , z >. e. F ) /\ -. y = z ) ) )
67 66 equsexvw 
 |-  ( E. a ( a = x /\ ( ( <. x , y >. e. F /\ <. a , z >. e. F ) /\ -. y = z ) ) <-> ( ( <. x , y >. e. F /\ <. x , z >. e. F ) /\ -. y = z ) )
68 62 67 bitri 
 |-  ( E. a E. p E. q ( ( p = <. x , y >. /\ q = <. a , z >. ) /\ ( ( p e. F /\ q e. F ) /\ q ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) p ) ) <-> ( ( <. x , y >. e. F /\ <. x , z >. e. F ) /\ -. y = z ) )
69 68 exbii 
 |-  ( E. z E. a E. p E. q ( ( p = <. x , y >. /\ q = <. a , z >. ) /\ ( ( p e. F /\ q e. F ) /\ q ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) p ) ) <-> E. z ( ( <. x , y >. e. F /\ <. x , z >. e. F ) /\ -. y = z ) )
70 exanali 
 |-  ( E. z ( ( <. x , y >. e. F /\ <. x , z >. e. F ) /\ -. y = z ) <-> -. A. z ( ( <. x , y >. e. F /\ <. x , z >. e. F ) -> y = z ) )
71 69 70 bitri 
 |-  ( E. z E. a E. p E. q ( ( p = <. x , y >. /\ q = <. a , z >. ) /\ ( ( p e. F /\ q e. F ) /\ q ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) p ) ) <-> -. A. z ( ( <. x , y >. e. F /\ <. x , z >. e. F ) -> y = z ) )
72 17 18 71 3bitri 
 |-  ( E. p E. q E. a E. z ( ( p = <. x , y >. /\ q = <. a , z >. ) /\ ( ( p e. F /\ q e. F ) /\ q ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) p ) ) <-> -. A. z ( ( <. x , y >. e. F /\ <. x , z >. e. F ) -> y = z ) )
73 72 exbii 
 |-  ( E. y E. p E. q E. a E. z ( ( p = <. x , y >. /\ q = <. a , z >. ) /\ ( ( p e. F /\ q e. F ) /\ q ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) p ) ) <-> E. y -. A. z ( ( <. x , y >. e. F /\ <. x , z >. e. F ) -> y = z ) )
74 exnal 
 |-  ( E. y -. A. z ( ( <. x , y >. e. F /\ <. x , z >. e. F ) -> y = z ) <-> -. A. y A. z ( ( <. x , y >. e. F /\ <. x , z >. e. F ) -> y = z ) )
75 16 73 74 3bitri 
 |-  ( E. q E. p E. y E. a E. z ( ( p = <. x , y >. /\ q = <. a , z >. ) /\ ( ( p e. F /\ q e. F ) /\ q ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) p ) ) <-> -. A. y A. z ( ( <. x , y >. e. F /\ <. x , z >. e. F ) -> y = z ) )
76 75 exbii 
 |-  ( E. x E. q E. p E. y E. a E. z ( ( p = <. x , y >. /\ q = <. a , z >. ) /\ ( ( p e. F /\ q e. F ) /\ q ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) p ) ) <-> E. x -. A. y A. z ( ( <. x , y >. e. F /\ <. x , z >. e. F ) -> y = z ) )
77 exnal 
 |-  ( E. x -. A. y A. z ( ( <. x , y >. e. F /\ <. x , z >. e. F ) -> y = z ) <-> -. A. x A. y A. z ( ( <. x , y >. e. F /\ <. x , z >. e. F ) -> y = z ) )
78 15 76 77 3bitri 
 |-  ( E. p E. q E. x E. y E. a E. z ( ( p = <. x , y >. /\ q = <. a , z >. ) /\ ( ( p e. F /\ q e. F ) /\ q ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) p ) ) <-> -. A. x A. y A. z ( ( <. x , y >. e. F /\ <. x , z >. e. F ) -> y = z ) )
79 14 78 bitrdi 
 |-  ( Rel F -> ( E. p E. q ( ( p e. F /\ q e. F ) /\ q ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) p ) <-> -. A. x A. y A. z ( ( <. x , y >. e. F /\ <. x , z >. e. F ) -> y = z ) ) )
80 79 con2bid 
 |-  ( Rel F -> ( A. x A. y A. z ( ( <. x , y >. e. F /\ <. x , z >. e. F ) -> y = z ) <-> -. E. p E. q ( ( p e. F /\ q e. F ) /\ q ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) p ) ) )
81 80 pm5.32i 
 |-  ( ( Rel F /\ A. x A. y A. z ( ( <. x , y >. e. F /\ <. x , z >. e. F ) -> y = z ) ) <-> ( Rel F /\ -. E. p E. q ( ( p e. F /\ q e. F ) /\ q ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) p ) ) )
82 dffun4 
 |-  ( Fun F <-> ( Rel F /\ A. x A. y A. z ( ( <. x , y >. e. F /\ <. x , z >. e. F ) -> y = z ) ) )
83 df-funs 
 |-  Funs = ( ~P ( _V X. _V ) \ Fix ( _E o. ( ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) o. `' _E ) ) )
84 83 eleq2i 
 |-  ( F e. Funs <-> F e. ( ~P ( _V X. _V ) \ Fix ( _E o. ( ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) o. `' _E ) ) ) )
85 eldif 
 |-  ( F e. ( ~P ( _V X. _V ) \ Fix ( _E o. ( ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) o. `' _E ) ) ) <-> ( F e. ~P ( _V X. _V ) /\ -. F e. Fix ( _E o. ( ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) o. `' _E ) ) ) )
86 1 elpw 
 |-  ( F e. ~P ( _V X. _V ) <-> F C_ ( _V X. _V ) )
87 df-rel 
 |-  ( Rel F <-> F C_ ( _V X. _V ) )
88 86 87 bitr4i 
 |-  ( F e. ~P ( _V X. _V ) <-> Rel F )
89 1 elfix 
 |-  ( F e. Fix ( _E o. ( ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) o. `' _E ) ) <-> F ( _E o. ( ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) o. `' _E ) ) F )
90 1 1 coep 
 |-  ( F ( _E o. ( ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) o. `' _E ) ) F <-> E. p e. F F ( ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) o. `' _E ) p )
91 vex 
 |-  p e. _V
92 1 91 coepr 
 |-  ( F ( ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) o. `' _E ) p <-> E. q e. F q ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) p )
93 92 rexbii 
 |-  ( E. p e. F F ( ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) o. `' _E ) p <-> E. p e. F E. q e. F q ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) p )
94 90 93 bitri 
 |-  ( F ( _E o. ( ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) o. `' _E ) ) F <-> E. p e. F E. q e. F q ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) p )
95 r2ex 
 |-  ( E. p e. F E. q e. F q ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) p <-> E. p E. q ( ( p e. F /\ q e. F ) /\ q ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) p ) )
96 89 94 95 3bitri 
 |-  ( F e. Fix ( _E o. ( ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) o. `' _E ) ) <-> E. p E. q ( ( p e. F /\ q e. F ) /\ q ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) p ) )
97 96 notbii 
 |-  ( -. F e. Fix ( _E o. ( ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) o. `' _E ) ) <-> -. E. p E. q ( ( p e. F /\ q e. F ) /\ q ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) p ) )
98 88 97 anbi12i 
 |-  ( ( F e. ~P ( _V X. _V ) /\ -. F e. Fix ( _E o. ( ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) o. `' _E ) ) ) <-> ( Rel F /\ -. E. p E. q ( ( p e. F /\ q e. F ) /\ q ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) p ) ) )
99 84 85 98 3bitri 
 |-  ( F e. Funs <-> ( Rel F /\ -. E. p E. q ( ( p e. F /\ q e. F ) /\ q ( 1st (x) ( ( _V \ _I ) o. 2nd ) ) p ) ) )
100 81 82 99 3bitr4ri 
 |-  ( F e. Funs <-> Fun F )