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 = F A F A F A -1 I

Proof

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