Step |
Hyp |
Ref |
Expression |
1 |
|
elvv |
|- ( A e. ( _V X. _V ) <-> E. w E. v A = <. w , v >. ) |
2 |
|
fveq2 |
|- ( A = <. w , v >. -> ( { <. <. x , y >. , z >. | z = x } ` A ) = ( { <. <. x , y >. , z >. | z = x } ` <. w , v >. ) ) |
3 |
|
df-ov |
|- ( w { <. <. x , y >. , z >. | z = x } v ) = ( { <. <. x , y >. , z >. | z = x } ` <. w , v >. ) |
4 |
|
simpl |
|- ( ( x = w /\ y = v ) -> x = w ) |
5 |
|
mpov |
|- ( x e. _V , y e. _V |-> x ) = { <. <. x , y >. , z >. | z = x } |
6 |
5
|
eqcomi |
|- { <. <. x , y >. , z >. | z = x } = ( x e. _V , y e. _V |-> x ) |
7 |
|
vex |
|- w e. _V |
8 |
4 6 7
|
ovmpoa |
|- ( ( w e. _V /\ v e. _V ) -> ( w { <. <. x , y >. , z >. | z = x } v ) = w ) |
9 |
8
|
el2v |
|- ( w { <. <. x , y >. , z >. | z = x } v ) = w |
10 |
3 9
|
eqtr3i |
|- ( { <. <. x , y >. , z >. | z = x } ` <. w , v >. ) = w |
11 |
2 10
|
eqtrdi |
|- ( A = <. w , v >. -> ( { <. <. x , y >. , z >. | z = x } ` A ) = w ) |
12 |
|
vex |
|- v e. _V |
13 |
7 12
|
op1std |
|- ( A = <. w , v >. -> ( 1st ` A ) = w ) |
14 |
11 13
|
eqtr4d |
|- ( A = <. w , v >. -> ( { <. <. x , y >. , z >. | z = x } ` A ) = ( 1st ` A ) ) |
15 |
14
|
exlimivv |
|- ( E. w E. v A = <. w , v >. -> ( { <. <. x , y >. , z >. | z = x } ` A ) = ( 1st ` A ) ) |
16 |
1 15
|
sylbi |
|- ( A e. ( _V X. _V ) -> ( { <. <. x , y >. , z >. | z = x } ` A ) = ( 1st ` A ) ) |
17 |
|
vex |
|- x e. _V |
18 |
|
vex |
|- y e. _V |
19 |
17 18
|
pm3.2i |
|- ( x e. _V /\ y e. _V ) |
20 |
|
ax6ev |
|- E. z z = x |
21 |
19 20
|
2th |
|- ( ( x e. _V /\ y e. _V ) <-> E. z z = x ) |
22 |
21
|
opabbii |
|- { <. x , y >. | ( x e. _V /\ y e. _V ) } = { <. x , y >. | E. z z = x } |
23 |
|
df-xp |
|- ( _V X. _V ) = { <. x , y >. | ( x e. _V /\ y e. _V ) } |
24 |
|
dmoprab |
|- dom { <. <. x , y >. , z >. | z = x } = { <. x , y >. | E. z z = x } |
25 |
22 23 24
|
3eqtr4ri |
|- dom { <. <. x , y >. , z >. | z = x } = ( _V X. _V ) |
26 |
25
|
eleq2i |
|- ( A e. dom { <. <. x , y >. , z >. | z = x } <-> A e. ( _V X. _V ) ) |
27 |
|
ndmfv |
|- ( -. A e. dom { <. <. x , y >. , z >. | z = x } -> ( { <. <. x , y >. , z >. | z = x } ` A ) = (/) ) |
28 |
26 27
|
sylnbir |
|- ( -. A e. ( _V X. _V ) -> ( { <. <. x , y >. , z >. | z = x } ` A ) = (/) ) |
29 |
|
dmsnn0 |
|- ( A e. ( _V X. _V ) <-> dom { A } =/= (/) ) |
30 |
29
|
biimpri |
|- ( dom { A } =/= (/) -> A e. ( _V X. _V ) ) |
31 |
30
|
necon1bi |
|- ( -. A e. ( _V X. _V ) -> dom { A } = (/) ) |
32 |
31
|
unieqd |
|- ( -. A e. ( _V X. _V ) -> U. dom { A } = U. (/) ) |
33 |
|
uni0 |
|- U. (/) = (/) |
34 |
32 33
|
eqtrdi |
|- ( -. A e. ( _V X. _V ) -> U. dom { A } = (/) ) |
35 |
28 34
|
eqtr4d |
|- ( -. A e. ( _V X. _V ) -> ( { <. <. x , y >. , z >. | z = x } ` A ) = U. dom { A } ) |
36 |
|
1stval |
|- ( 1st ` A ) = U. dom { A } |
37 |
35 36
|
eqtr4di |
|- ( -. A e. ( _V X. _V ) -> ( { <. <. x , y >. , z >. | z = x } ` A ) = ( 1st ` A ) ) |
38 |
16 37
|
pm2.61i |
|- ( { <. <. x , y >. , z >. | z = x } ` A ) = ( 1st ` A ) |