| Step |
Hyp |
Ref |
Expression |
| 1 |
|
elin |
|- ( v e. ( ( { w } X. w ) i^i y ) <-> ( v e. ( { w } X. w ) /\ v e. y ) ) |
| 2 |
|
elxp |
|- ( v e. ( { w } X. w ) <-> E. t E. g ( v = <. t , g >. /\ ( t e. { w } /\ g e. w ) ) ) |
| 3 |
|
excom |
|- ( E. t E. g ( v = <. t , g >. /\ ( t e. { w } /\ g e. w ) ) <-> E. g E. t ( v = <. t , g >. /\ ( t e. { w } /\ g e. w ) ) ) |
| 4 |
2 3
|
bitri |
|- ( v e. ( { w } X. w ) <-> E. g E. t ( v = <. t , g >. /\ ( t e. { w } /\ g e. w ) ) ) |
| 5 |
4
|
anbi1i |
|- ( ( v e. ( { w } X. w ) /\ v e. y ) <-> ( E. g E. t ( v = <. t , g >. /\ ( t e. { w } /\ g e. w ) ) /\ v e. y ) ) |
| 6 |
|
19.41vv |
|- ( E. g E. t ( ( v = <. t , g >. /\ ( t e. { w } /\ g e. w ) ) /\ v e. y ) <-> ( E. g E. t ( v = <. t , g >. /\ ( t e. { w } /\ g e. w ) ) /\ v e. y ) ) |
| 7 |
|
an32 |
|- ( ( ( v = <. t , g >. /\ ( t e. { w } /\ g e. w ) ) /\ v e. y ) <-> ( ( v = <. t , g >. /\ v e. y ) /\ ( t e. { w } /\ g e. w ) ) ) |
| 8 |
|
eleq1 |
|- ( v = <. t , g >. -> ( v e. y <-> <. t , g >. e. y ) ) |
| 9 |
8
|
pm5.32i |
|- ( ( v = <. t , g >. /\ v e. y ) <-> ( v = <. t , g >. /\ <. t , g >. e. y ) ) |
| 10 |
|
velsn |
|- ( t e. { w } <-> t = w ) |
| 11 |
10
|
anbi1i |
|- ( ( t e. { w } /\ g e. w ) <-> ( t = w /\ g e. w ) ) |
| 12 |
9 11
|
anbi12i |
|- ( ( ( v = <. t , g >. /\ v e. y ) /\ ( t e. { w } /\ g e. w ) ) <-> ( ( v = <. t , g >. /\ <. t , g >. e. y ) /\ ( t = w /\ g e. w ) ) ) |
| 13 |
|
an4 |
|- ( ( ( v = <. t , g >. /\ <. t , g >. e. y ) /\ ( t = w /\ g e. w ) ) <-> ( ( v = <. t , g >. /\ t = w ) /\ ( <. t , g >. e. y /\ g e. w ) ) ) |
| 14 |
|
ancom |
|- ( ( v = <. t , g >. /\ t = w ) <-> ( t = w /\ v = <. t , g >. ) ) |
| 15 |
|
ancom |
|- ( ( <. t , g >. e. y /\ g e. w ) <-> ( g e. w /\ <. t , g >. e. y ) ) |
| 16 |
14 15
|
anbi12i |
|- ( ( ( v = <. t , g >. /\ t = w ) /\ ( <. t , g >. e. y /\ g e. w ) ) <-> ( ( t = w /\ v = <. t , g >. ) /\ ( g e. w /\ <. t , g >. e. y ) ) ) |
| 17 |
|
anass |
|- ( ( ( t = w /\ v = <. t , g >. ) /\ ( g e. w /\ <. t , g >. e. y ) ) <-> ( t = w /\ ( v = <. t , g >. /\ ( g e. w /\ <. t , g >. e. y ) ) ) ) |
| 18 |
13 16 17
|
3bitri |
|- ( ( ( v = <. t , g >. /\ <. t , g >. e. y ) /\ ( t = w /\ g e. w ) ) <-> ( t = w /\ ( v = <. t , g >. /\ ( g e. w /\ <. t , g >. e. y ) ) ) ) |
| 19 |
7 12 18
|
3bitri |
|- ( ( ( v = <. t , g >. /\ ( t e. { w } /\ g e. w ) ) /\ v e. y ) <-> ( t = w /\ ( v = <. t , g >. /\ ( g e. w /\ <. t , g >. e. y ) ) ) ) |
| 20 |
19
|
exbii |
|- ( E. t ( ( v = <. t , g >. /\ ( t e. { w } /\ g e. w ) ) /\ v e. y ) <-> E. t ( t = w /\ ( v = <. t , g >. /\ ( g e. w /\ <. t , g >. e. y ) ) ) ) |
| 21 |
|
opeq1 |
|- ( t = w -> <. t , g >. = <. w , g >. ) |
| 22 |
21
|
eqeq2d |
|- ( t = w -> ( v = <. t , g >. <-> v = <. w , g >. ) ) |
| 23 |
21
|
eleq1d |
|- ( t = w -> ( <. t , g >. e. y <-> <. w , g >. e. y ) ) |
| 24 |
23
|
anbi2d |
|- ( t = w -> ( ( g e. w /\ <. t , g >. e. y ) <-> ( g e. w /\ <. w , g >. e. y ) ) ) |
| 25 |
22 24
|
anbi12d |
|- ( t = w -> ( ( v = <. t , g >. /\ ( g e. w /\ <. t , g >. e. y ) ) <-> ( v = <. w , g >. /\ ( g e. w /\ <. w , g >. e. y ) ) ) ) |
| 26 |
25
|
equsexvw |
|- ( E. t ( t = w /\ ( v = <. t , g >. /\ ( g e. w /\ <. t , g >. e. y ) ) ) <-> ( v = <. w , g >. /\ ( g e. w /\ <. w , g >. e. y ) ) ) |
| 27 |
20 26
|
bitri |
|- ( E. t ( ( v = <. t , g >. /\ ( t e. { w } /\ g e. w ) ) /\ v e. y ) <-> ( v = <. w , g >. /\ ( g e. w /\ <. w , g >. e. y ) ) ) |
| 28 |
27
|
exbii |
|- ( E. g E. t ( ( v = <. t , g >. /\ ( t e. { w } /\ g e. w ) ) /\ v e. y ) <-> E. g ( v = <. w , g >. /\ ( g e. w /\ <. w , g >. e. y ) ) ) |
| 29 |
6 28
|
bitr3i |
|- ( ( E. g E. t ( v = <. t , g >. /\ ( t e. { w } /\ g e. w ) ) /\ v e. y ) <-> E. g ( v = <. w , g >. /\ ( g e. w /\ <. w , g >. e. y ) ) ) |
| 30 |
1 5 29
|
3bitri |
|- ( v e. ( ( { w } X. w ) i^i y ) <-> E. g ( v = <. w , g >. /\ ( g e. w /\ <. w , g >. e. y ) ) ) |
| 31 |
30
|
eubii |
|- ( E! v v e. ( ( { w } X. w ) i^i y ) <-> E! v E. g ( v = <. w , g >. /\ ( g e. w /\ <. w , g >. e. y ) ) ) |
| 32 |
|
vex |
|- w e. _V |
| 33 |
32
|
euop2 |
|- ( E! v E. g ( v = <. w , g >. /\ ( g e. w /\ <. w , g >. e. y ) ) <-> E! g ( g e. w /\ <. w , g >. e. y ) ) |
| 34 |
31 33
|
bitri |
|- ( E! v v e. ( ( { w } X. w ) i^i y ) <-> E! g ( g e. w /\ <. w , g >. e. y ) ) |