Metamath Proof Explorer


Theorem dffv2

Description: Alternate definition of function value df-fv that doesn't require dummy variables. (Contributed by NM, 4-Aug-2010)

Ref Expression
Assertion dffv2
|- ( F ` A ) = U. ( ( F " { A } ) \ U. U. ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) )

Proof

Step Hyp Ref Expression
1 snidb
 |-  ( A e. _V <-> A e. { A } )
2 fvres
 |-  ( A e. { A } -> ( ( F |` { A } ) ` A ) = ( F ` A ) )
3 1 2 sylbi
 |-  ( A e. _V -> ( ( F |` { A } ) ` A ) = ( F ` A ) )
4 fvprc
 |-  ( -. A e. _V -> ( ( F |` { A } ) ` A ) = (/) )
5 fvprc
 |-  ( -. A e. _V -> ( F ` A ) = (/) )
6 4 5 eqtr4d
 |-  ( -. A e. _V -> ( ( F |` { A } ) ` A ) = ( F ` A ) )
7 3 6 pm2.61i
 |-  ( ( F |` { A } ) ` A ) = ( F ` A )
8 funfv
 |-  ( Fun ( F |` { A } ) -> ( ( F |` { A } ) ` A ) = U. ( ( F |` { A } ) " { A } ) )
9 resima
 |-  ( ( F |` { A } ) " { A } ) = ( F " { A } )
10 dif0
 |-  ( ( F " { A } ) \ (/) ) = ( F " { A } )
11 9 10 eqtr4i
 |-  ( ( F |` { A } ) " { A } ) = ( ( F " { A } ) \ (/) )
12 df-fun
 |-  ( Fun ( F |` { A } ) <-> ( Rel ( F |` { A } ) /\ ( ( F |` { A } ) o. `' ( F |` { A } ) ) C_ _I ) )
13 12 simprbi
 |-  ( Fun ( F |` { A } ) -> ( ( F |` { A } ) o. `' ( F |` { A } ) ) C_ _I )
14 ssdif0
 |-  ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) C_ _I <-> ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) = (/) )
15 13 14 sylib
 |-  ( Fun ( F |` { A } ) -> ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) = (/) )
16 15 unieqd
 |-  ( Fun ( F |` { A } ) -> U. ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) = U. (/) )
17 uni0
 |-  U. (/) = (/)
18 16 17 eqtrdi
 |-  ( Fun ( F |` { A } ) -> U. ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) = (/) )
19 18 unieqd
 |-  ( Fun ( F |` { A } ) -> U. U. ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) = U. (/) )
20 19 17 eqtrdi
 |-  ( Fun ( F |` { A } ) -> U. U. ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) = (/) )
21 20 difeq2d
 |-  ( Fun ( F |` { A } ) -> ( ( F " { A } ) \ U. U. ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) ) = ( ( F " { A } ) \ (/) ) )
22 11 21 eqtr4id
 |-  ( Fun ( F |` { A } ) -> ( ( F |` { A } ) " { A } ) = ( ( F " { A } ) \ U. U. ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) ) )
23 22 unieqd
 |-  ( Fun ( F |` { A } ) -> U. ( ( F |` { A } ) " { A } ) = U. ( ( F " { A } ) \ U. U. ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) ) )
24 8 23 eqtrd
 |-  ( Fun ( F |` { A } ) -> ( ( F |` { A } ) ` A ) = U. ( ( F " { A } ) \ U. U. ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) ) )
25 7 24 eqtr3id
 |-  ( Fun ( F |` { A } ) -> ( F ` A ) = U. ( ( F " { A } ) \ U. U. ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) ) )
26 nfunsn
 |-  ( -. Fun ( F |` { A } ) -> ( F ` A ) = (/) )
27 relres
 |-  Rel ( F |` { A } )
28 dffun3
 |-  ( Fun ( F |` { A } ) <-> ( Rel ( F |` { A } ) /\ A. x E. y A. z ( x ( F |` { A } ) z -> z = y ) ) )
29 27 28 mpbiran
 |-  ( Fun ( F |` { A } ) <-> A. x E. y A. z ( x ( F |` { A } ) z -> z = y ) )
30 iman
 |-  ( ( x ( F |` { A } ) z -> z = y ) <-> -. ( x ( F |` { A } ) z /\ -. z = y ) )
31 30 albii
 |-  ( A. z ( x ( F |` { A } ) z -> z = y ) <-> A. z -. ( x ( F |` { A } ) z /\ -. z = y ) )
32 alnex
 |-  ( A. z -. ( x ( F |` { A } ) z /\ -. z = y ) <-> -. E. z ( x ( F |` { A } ) z /\ -. z = y ) )
33 31 32 bitri
 |-  ( A. z ( x ( F |` { A } ) z -> z = y ) <-> -. E. z ( x ( F |` { A } ) z /\ -. z = y ) )
34 33 exbii
 |-  ( E. y A. z ( x ( F |` { A } ) z -> z = y ) <-> E. y -. E. z ( x ( F |` { A } ) z /\ -. z = y ) )
35 exnal
 |-  ( E. y -. E. z ( x ( F |` { A } ) z /\ -. z = y ) <-> -. A. y E. z ( x ( F |` { A } ) z /\ -. z = y ) )
36 34 35 bitri
 |-  ( E. y A. z ( x ( F |` { A } ) z -> z = y ) <-> -. A. y E. z ( x ( F |` { A } ) z /\ -. z = y ) )
37 36 albii
 |-  ( A. x E. y A. z ( x ( F |` { A } ) z -> z = y ) <-> A. x -. A. y E. z ( x ( F |` { A } ) z /\ -. z = y ) )
38 alnex
 |-  ( A. x -. A. y E. z ( x ( F |` { A } ) z /\ -. z = y ) <-> -. E. x A. y E. z ( x ( F |` { A } ) z /\ -. z = y ) )
39 29 37 38 3bitrri
 |-  ( -. E. x A. y E. z ( x ( F |` { A } ) z /\ -. z = y ) <-> Fun ( F |` { A } ) )
40 39 con1bii
 |-  ( -. Fun ( F |` { A } ) <-> E. x A. y E. z ( x ( F |` { A } ) z /\ -. z = y ) )
41 sp
 |-  ( A. y E. z ( x ( F |` { A } ) z /\ -. z = y ) -> E. z ( x ( F |` { A } ) z /\ -. z = y ) )
42 41 eximi
 |-  ( E. x A. y E. z ( x ( F |` { A } ) z /\ -. z = y ) -> E. x E. z ( x ( F |` { A } ) z /\ -. z = y ) )
43 40 42 sylbi
 |-  ( -. Fun ( F |` { A } ) -> E. x E. z ( x ( F |` { A } ) z /\ -. z = y ) )
44 snssi
 |-  ( A e. dom ( F |` { A } ) -> { A } C_ dom ( F |` { A } ) )
45 residm
 |-  ( ( F |` { A } ) |` { A } ) = ( F |` { A } )
46 45 dmeqi
 |-  dom ( ( F |` { A } ) |` { A } ) = dom ( F |` { A } )
47 ssdmres
 |-  ( { A } C_ dom ( F |` { A } ) <-> dom ( ( F |` { A } ) |` { A } ) = { A } )
48 47 biimpi
 |-  ( { A } C_ dom ( F |` { A } ) -> dom ( ( F |` { A } ) |` { A } ) = { A } )
49 46 48 eqtr3id
 |-  ( { A } C_ dom ( F |` { A } ) -> dom ( F |` { A } ) = { A } )
50 44 49 syl
 |-  ( A e. dom ( F |` { A } ) -> dom ( F |` { A } ) = { A } )
51 vex
 |-  x e. _V
52 vex
 |-  z e. _V
53 51 52 breldm
 |-  ( x ( F |` { A } ) z -> x e. dom ( F |` { A } ) )
54 eleq2
 |-  ( dom ( F |` { A } ) = { A } -> ( x e. dom ( F |` { A } ) <-> x e. { A } ) )
55 velsn
 |-  ( x e. { A } <-> x = A )
56 54 55 bitrdi
 |-  ( dom ( F |` { A } ) = { A } -> ( x e. dom ( F |` { A } ) <-> x = A ) )
57 56 biimpa
 |-  ( ( dom ( F |` { A } ) = { A } /\ x e. dom ( F |` { A } ) ) -> x = A )
58 50 53 57 syl2an
 |-  ( ( A e. dom ( F |` { A } ) /\ x ( F |` { A } ) z ) -> x = A )
59 58 breq1d
 |-  ( ( A e. dom ( F |` { A } ) /\ x ( F |` { A } ) z ) -> ( x ( F |` { A } ) z <-> A ( F |` { A } ) z ) )
60 59 biimpd
 |-  ( ( A e. dom ( F |` { A } ) /\ x ( F |` { A } ) z ) -> ( x ( F |` { A } ) z -> A ( F |` { A } ) z ) )
61 60 ex
 |-  ( A e. dom ( F |` { A } ) -> ( x ( F |` { A } ) z -> ( x ( F |` { A } ) z -> A ( F |` { A } ) z ) ) )
62 61 pm2.43d
 |-  ( A e. dom ( F |` { A } ) -> ( x ( F |` { A } ) z -> A ( F |` { A } ) z ) )
63 62 anim1d
 |-  ( A e. dom ( F |` { A } ) -> ( ( x ( F |` { A } ) z /\ -. z = y ) -> ( A ( F |` { A } ) z /\ -. z = y ) ) )
64 63 eximdv
 |-  ( A e. dom ( F |` { A } ) -> ( E. z ( x ( F |` { A } ) z /\ -. z = y ) -> E. z ( A ( F |` { A } ) z /\ -. z = y ) ) )
65 64 exlimdv
 |-  ( A e. dom ( F |` { A } ) -> ( E. x E. z ( x ( F |` { A } ) z /\ -. z = y ) -> E. z ( A ( F |` { A } ) z /\ -. z = y ) ) )
66 43 65 mpan9
 |-  ( ( -. Fun ( F |` { A } ) /\ A e. dom ( F |` { A } ) ) -> E. z ( A ( F |` { A } ) z /\ -. z = y ) )
67 9 eleq2i
 |-  ( y e. ( ( F |` { A } ) " { A } ) <-> y e. ( F " { A } ) )
68 elimasni
 |-  ( y e. ( ( F |` { A } ) " { A } ) -> A ( F |` { A } ) y )
69 67 68 sylbir
 |-  ( y e. ( F " { A } ) -> A ( F |` { A } ) y )
70 vex
 |-  y e. _V
71 70 52 uniop
 |-  U. <. y , z >. = { y , z }
72 opex
 |-  <. y , z >. e. _V
73 72 unisn
 |-  U. { <. y , z >. } = <. y , z >.
74 27 brrelex1i
 |-  ( A ( F |` { A } ) z -> A e. _V )
75 brcnvg
 |-  ( ( y e. _V /\ A e. _V ) -> ( y `' ( F |` { A } ) A <-> A ( F |` { A } ) y ) )
76 70 74 75 sylancr
 |-  ( A ( F |` { A } ) z -> ( y `' ( F |` { A } ) A <-> A ( F |` { A } ) y ) )
77 76 biimpar
 |-  ( ( A ( F |` { A } ) z /\ A ( F |` { A } ) y ) -> y `' ( F |` { A } ) A )
78 74 adantl
 |-  ( ( y `' ( F |` { A } ) A /\ A ( F |` { A } ) z ) -> A e. _V )
79 breq2
 |-  ( x = A -> ( y `' ( F |` { A } ) x <-> y `' ( F |` { A } ) A ) )
80 breq1
 |-  ( x = A -> ( x ( F |` { A } ) z <-> A ( F |` { A } ) z ) )
81 79 80 anbi12d
 |-  ( x = A -> ( ( y `' ( F |` { A } ) x /\ x ( F |` { A } ) z ) <-> ( y `' ( F |` { A } ) A /\ A ( F |` { A } ) z ) ) )
82 81 rspcev
 |-  ( ( A e. _V /\ ( y `' ( F |` { A } ) A /\ A ( F |` { A } ) z ) ) -> E. x e. _V ( y `' ( F |` { A } ) x /\ x ( F |` { A } ) z ) )
83 78 82 mpancom
 |-  ( ( y `' ( F |` { A } ) A /\ A ( F |` { A } ) z ) -> E. x e. _V ( y `' ( F |` { A } ) x /\ x ( F |` { A } ) z ) )
84 83 ancoms
 |-  ( ( A ( F |` { A } ) z /\ y `' ( F |` { A } ) A ) -> E. x e. _V ( y `' ( F |` { A } ) x /\ x ( F |` { A } ) z ) )
85 77 84 syldan
 |-  ( ( A ( F |` { A } ) z /\ A ( F |` { A } ) y ) -> E. x e. _V ( y `' ( F |` { A } ) x /\ x ( F |` { A } ) z ) )
86 85 anim1i
 |-  ( ( ( A ( F |` { A } ) z /\ A ( F |` { A } ) y ) /\ -. z = y ) -> ( E. x e. _V ( y `' ( F |` { A } ) x /\ x ( F |` { A } ) z ) /\ -. z = y ) )
87 86 an32s
 |-  ( ( ( A ( F |` { A } ) z /\ -. z = y ) /\ A ( F |` { A } ) y ) -> ( E. x e. _V ( y `' ( F |` { A } ) x /\ x ( F |` { A } ) z ) /\ -. z = y ) )
88 eldif
 |-  ( <. y , z >. e. ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) <-> ( <. y , z >. e. ( ( F |` { A } ) o. `' ( F |` { A } ) ) /\ -. <. y , z >. e. _I ) )
89 rexv
 |-  ( E. x e. _V ( y `' ( F |` { A } ) x /\ x ( F |` { A } ) z ) <-> E. x ( y `' ( F |` { A } ) x /\ x ( F |` { A } ) z ) )
90 70 52 brco
 |-  ( y ( ( F |` { A } ) o. `' ( F |` { A } ) ) z <-> E. x ( y `' ( F |` { A } ) x /\ x ( F |` { A } ) z ) )
91 df-br
 |-  ( y ( ( F |` { A } ) o. `' ( F |` { A } ) ) z <-> <. y , z >. e. ( ( F |` { A } ) o. `' ( F |` { A } ) ) )
92 89 90 91 3bitr2ri
 |-  ( <. y , z >. e. ( ( F |` { A } ) o. `' ( F |` { A } ) ) <-> E. x e. _V ( y `' ( F |` { A } ) x /\ x ( F |` { A } ) z ) )
93 52 ideq
 |-  ( y _I z <-> y = z )
94 df-br
 |-  ( y _I z <-> <. y , z >. e. _I )
95 equcom
 |-  ( y = z <-> z = y )
96 93 94 95 3bitr3i
 |-  ( <. y , z >. e. _I <-> z = y )
97 96 notbii
 |-  ( -. <. y , z >. e. _I <-> -. z = y )
98 92 97 anbi12i
 |-  ( ( <. y , z >. e. ( ( F |` { A } ) o. `' ( F |` { A } ) ) /\ -. <. y , z >. e. _I ) <-> ( E. x e. _V ( y `' ( F |` { A } ) x /\ x ( F |` { A } ) z ) /\ -. z = y ) )
99 88 98 bitr2i
 |-  ( ( E. x e. _V ( y `' ( F |` { A } ) x /\ x ( F |` { A } ) z ) /\ -. z = y ) <-> <. y , z >. e. ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) )
100 87 99 sylib
 |-  ( ( ( A ( F |` { A } ) z /\ -. z = y ) /\ A ( F |` { A } ) y ) -> <. y , z >. e. ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) )
101 snssi
 |-  ( <. y , z >. e. ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) -> { <. y , z >. } C_ ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) )
102 uniss
 |-  ( { <. y , z >. } C_ ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) -> U. { <. y , z >. } C_ U. ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) )
103 100 101 102 3syl
 |-  ( ( ( A ( F |` { A } ) z /\ -. z = y ) /\ A ( F |` { A } ) y ) -> U. { <. y , z >. } C_ U. ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) )
104 73 103 eqsstrrid
 |-  ( ( ( A ( F |` { A } ) z /\ -. z = y ) /\ A ( F |` { A } ) y ) -> <. y , z >. C_ U. ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) )
105 104 unissd
 |-  ( ( ( A ( F |` { A } ) z /\ -. z = y ) /\ A ( F |` { A } ) y ) -> U. <. y , z >. C_ U. U. ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) )
106 71 105 eqsstrrid
 |-  ( ( ( A ( F |` { A } ) z /\ -. z = y ) /\ A ( F |` { A } ) y ) -> { y , z } C_ U. U. ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) )
107 70 52 prss
 |-  ( ( y e. U. U. ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) /\ z e. U. U. ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) ) <-> { y , z } C_ U. U. ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) )
108 106 107 sylibr
 |-  ( ( ( A ( F |` { A } ) z /\ -. z = y ) /\ A ( F |` { A } ) y ) -> ( y e. U. U. ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) /\ z e. U. U. ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) ) )
109 108 simpld
 |-  ( ( ( A ( F |` { A } ) z /\ -. z = y ) /\ A ( F |` { A } ) y ) -> y e. U. U. ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) )
110 109 ex
 |-  ( ( A ( F |` { A } ) z /\ -. z = y ) -> ( A ( F |` { A } ) y -> y e. U. U. ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) ) )
111 69 110 syl5
 |-  ( ( A ( F |` { A } ) z /\ -. z = y ) -> ( y e. ( F " { A } ) -> y e. U. U. ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) ) )
112 111 exlimiv
 |-  ( E. z ( A ( F |` { A } ) z /\ -. z = y ) -> ( y e. ( F " { A } ) -> y e. U. U. ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) ) )
113 66 112 syl
 |-  ( ( -. Fun ( F |` { A } ) /\ A e. dom ( F |` { A } ) ) -> ( y e. ( F " { A } ) -> y e. U. U. ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) ) )
114 113 ssrdv
 |-  ( ( -. Fun ( F |` { A } ) /\ A e. dom ( F |` { A } ) ) -> ( F " { A } ) C_ U. U. ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) )
115 ssdif0
 |-  ( ( F " { A } ) C_ U. U. ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) <-> ( ( F " { A } ) \ U. U. ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) ) = (/) )
116 114 115 sylib
 |-  ( ( -. Fun ( F |` { A } ) /\ A e. dom ( F |` { A } ) ) -> ( ( F " { A } ) \ U. U. ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) ) = (/) )
117 116 ex
 |-  ( -. Fun ( F |` { A } ) -> ( A e. dom ( F |` { A } ) -> ( ( F " { A } ) \ U. U. ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) ) = (/) ) )
118 ndmima
 |-  ( -. A e. dom ( F |` { A } ) -> ( ( F |` { A } ) " { A } ) = (/) )
119 9 118 eqtr3id
 |-  ( -. A e. dom ( F |` { A } ) -> ( F " { A } ) = (/) )
120 119 difeq1d
 |-  ( -. A e. dom ( F |` { A } ) -> ( ( F " { A } ) \ U. U. ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) ) = ( (/) \ U. U. ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) ) )
121 0dif
 |-  ( (/) \ U. U. ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) ) = (/)
122 120 121 eqtrdi
 |-  ( -. A e. dom ( F |` { A } ) -> ( ( F " { A } ) \ U. U. ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) ) = (/) )
123 117 122 pm2.61d1
 |-  ( -. Fun ( F |` { A } ) -> ( ( F " { A } ) \ U. U. ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) ) = (/) )
124 123 unieqd
 |-  ( -. Fun ( F |` { A } ) -> U. ( ( F " { A } ) \ U. U. ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) ) = U. (/) )
125 124 17 eqtrdi
 |-  ( -. Fun ( F |` { A } ) -> U. ( ( F " { A } ) \ U. U. ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) ) = (/) )
126 26 125 eqtr4d
 |-  ( -. Fun ( F |` { A } ) -> ( F ` A ) = U. ( ( F " { A } ) \ U. U. ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) ) )
127 25 126 pm2.61i
 |-  ( F ` A ) = U. ( ( F " { A } ) \ U. U. ( ( ( F |` { A } ) o. `' ( F |` { A } ) ) \ _I ) )