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