Step |
Hyp |
Ref |
Expression |
1 |
|
vex |
|- y e. _V |
2 |
|
vex |
|- z e. _V |
3 |
1 2
|
op1sta |
|- U. dom { <. y , z >. } = y |
4 |
3
|
eleq1i |
|- ( U. dom { <. y , z >. } e. A <-> y e. A ) |
5 |
4
|
biimpri |
|- ( y e. A -> U. dom { <. y , z >. } e. A ) |
6 |
5
|
adantr |
|- ( ( y e. A /\ z e. B ) -> U. dom { <. y , z >. } e. A ) |
7 |
6
|
rgen2 |
|- A. y e. A A. z e. B U. dom { <. y , z >. } e. A |
8 |
|
sneq |
|- ( x = <. y , z >. -> { x } = { <. y , z >. } ) |
9 |
8
|
dmeqd |
|- ( x = <. y , z >. -> dom { x } = dom { <. y , z >. } ) |
10 |
9
|
unieqd |
|- ( x = <. y , z >. -> U. dom { x } = U. dom { <. y , z >. } ) |
11 |
10
|
eleq1d |
|- ( x = <. y , z >. -> ( U. dom { x } e. A <-> U. dom { <. y , z >. } e. A ) ) |
12 |
11
|
ralxp |
|- ( A. x e. ( A X. B ) U. dom { x } e. A <-> A. y e. A A. z e. B U. dom { <. y , z >. } e. A ) |
13 |
7 12
|
mpbir |
|- A. x e. ( A X. B ) U. dom { x } e. A |
14 |
|
df-1st |
|- 1st = ( x e. _V |-> U. dom { x } ) |
15 |
14
|
reseq1i |
|- ( 1st |` ( A X. B ) ) = ( ( x e. _V |-> U. dom { x } ) |` ( A X. B ) ) |
16 |
|
ssv |
|- ( A X. B ) C_ _V |
17 |
|
resmpt |
|- ( ( A X. B ) C_ _V -> ( ( x e. _V |-> U. dom { x } ) |` ( A X. B ) ) = ( x e. ( A X. B ) |-> U. dom { x } ) ) |
18 |
16 17
|
ax-mp |
|- ( ( x e. _V |-> U. dom { x } ) |` ( A X. B ) ) = ( x e. ( A X. B ) |-> U. dom { x } ) |
19 |
15 18
|
eqtri |
|- ( 1st |` ( A X. B ) ) = ( x e. ( A X. B ) |-> U. dom { x } ) |
20 |
19
|
fmpt |
|- ( A. x e. ( A X. B ) U. dom { x } e. A <-> ( 1st |` ( A X. B ) ) : ( A X. B ) --> A ) |
21 |
13 20
|
mpbi |
|- ( 1st |` ( A X. B ) ) : ( A X. B ) --> A |