| Step |
Hyp |
Ref |
Expression |
| 1 |
|
epel |
|- ( z _E x <-> z e. x ) |
| 2 |
|
brvdif |
|- ( z ( _V \ _E ) y <-> -. z _E y ) |
| 3 |
|
epel |
|- ( z _E y <-> z e. y ) |
| 4 |
2 3
|
xchbinx |
|- ( z ( _V \ _E ) y <-> -. z e. y ) |
| 5 |
1 4
|
anbi12i |
|- ( ( z _E x /\ z ( _V \ _E ) y ) <-> ( z e. x /\ -. z e. y ) ) |
| 6 |
5
|
exbii |
|- ( E. z ( z _E x /\ z ( _V \ _E ) y ) <-> E. z ( z e. x /\ -. z e. y ) ) |
| 7 |
6
|
notbii |
|- ( -. E. z ( z _E x /\ z ( _V \ _E ) y ) <-> -. E. z ( z e. x /\ -. z e. y ) ) |
| 8 |
|
dfss6 |
|- ( x C_ y <-> -. E. z ( z e. x /\ -. z e. y ) ) |
| 9 |
7 8
|
bitr4i |
|- ( -. E. z ( z _E x /\ z ( _V \ _E ) y ) <-> x C_ y ) |
| 10 |
9
|
opabbii |
|- { <. x , y >. | -. E. z ( z _E x /\ z ( _V \ _E ) y ) } = { <. x , y >. | x C_ y } |
| 11 |
|
rnxrn |
|- ran ( _E |X. ( _V \ _E ) ) = { <. x , y >. | E. z ( z _E x /\ z ( _V \ _E ) y ) } |
| 12 |
11
|
difeq2i |
|- ( ( _V X. _V ) \ ran ( _E |X. ( _V \ _E ) ) ) = ( ( _V X. _V ) \ { <. x , y >. | E. z ( z _E x /\ z ( _V \ _E ) y ) } ) |
| 13 |
|
vvdifopab |
|- ( ( _V X. _V ) \ { <. x , y >. | E. z ( z _E x /\ z ( _V \ _E ) y ) } ) = { <. x , y >. | -. E. z ( z _E x /\ z ( _V \ _E ) y ) } |
| 14 |
12 13
|
eqtri |
|- ( ( _V X. _V ) \ ran ( _E |X. ( _V \ _E ) ) ) = { <. x , y >. | -. E. z ( z _E x /\ z ( _V \ _E ) y ) } |
| 15 |
|
df-ssr |
|- _S = { <. x , y >. | x C_ y } |
| 16 |
10 14 15
|
3eqtr4ri |
|- _S = ( ( _V X. _V ) \ ran ( _E |X. ( _V \ _E ) ) ) |