Step |
Hyp |
Ref |
Expression |
1 |
|
iunfo.1 |
|- T = U_ x e. A ( { x } X. B ) |
2 |
|
fo2nd |
|- 2nd : _V -onto-> _V |
3 |
|
fof |
|- ( 2nd : _V -onto-> _V -> 2nd : _V --> _V ) |
4 |
|
ffn |
|- ( 2nd : _V --> _V -> 2nd Fn _V ) |
5 |
2 3 4
|
mp2b |
|- 2nd Fn _V |
6 |
|
ssv |
|- T C_ _V |
7 |
|
fnssres |
|- ( ( 2nd Fn _V /\ T C_ _V ) -> ( 2nd |` T ) Fn T ) |
8 |
5 6 7
|
mp2an |
|- ( 2nd |` T ) Fn T |
9 |
|
df-ima |
|- ( 2nd " T ) = ran ( 2nd |` T ) |
10 |
1
|
eleq2i |
|- ( z e. T <-> z e. U_ x e. A ( { x } X. B ) ) |
11 |
|
eliun |
|- ( z e. U_ x e. A ( { x } X. B ) <-> E. x e. A z e. ( { x } X. B ) ) |
12 |
10 11
|
bitri |
|- ( z e. T <-> E. x e. A z e. ( { x } X. B ) ) |
13 |
|
xp2nd |
|- ( z e. ( { x } X. B ) -> ( 2nd ` z ) e. B ) |
14 |
|
eleq1 |
|- ( ( 2nd ` z ) = y -> ( ( 2nd ` z ) e. B <-> y e. B ) ) |
15 |
13 14
|
syl5ib |
|- ( ( 2nd ` z ) = y -> ( z e. ( { x } X. B ) -> y e. B ) ) |
16 |
15
|
reximdv |
|- ( ( 2nd ` z ) = y -> ( E. x e. A z e. ( { x } X. B ) -> E. x e. A y e. B ) ) |
17 |
12 16
|
syl5bi |
|- ( ( 2nd ` z ) = y -> ( z e. T -> E. x e. A y e. B ) ) |
18 |
17
|
impcom |
|- ( ( z e. T /\ ( 2nd ` z ) = y ) -> E. x e. A y e. B ) |
19 |
18
|
rexlimiva |
|- ( E. z e. T ( 2nd ` z ) = y -> E. x e. A y e. B ) |
20 |
|
nfiu1 |
|- F/_ x U_ x e. A ( { x } X. B ) |
21 |
1 20
|
nfcxfr |
|- F/_ x T |
22 |
|
nfv |
|- F/ x ( 2nd ` z ) = y |
23 |
21 22
|
nfrex |
|- F/ x E. z e. T ( 2nd ` z ) = y |
24 |
|
ssiun2 |
|- ( x e. A -> ( { x } X. B ) C_ U_ x e. A ( { x } X. B ) ) |
25 |
24
|
adantr |
|- ( ( x e. A /\ y e. B ) -> ( { x } X. B ) C_ U_ x e. A ( { x } X. B ) ) |
26 |
|
simpr |
|- ( ( x e. A /\ y e. B ) -> y e. B ) |
27 |
|
vsnid |
|- x e. { x } |
28 |
|
opelxp |
|- ( <. x , y >. e. ( { x } X. B ) <-> ( x e. { x } /\ y e. B ) ) |
29 |
27 28
|
mpbiran |
|- ( <. x , y >. e. ( { x } X. B ) <-> y e. B ) |
30 |
26 29
|
sylibr |
|- ( ( x e. A /\ y e. B ) -> <. x , y >. e. ( { x } X. B ) ) |
31 |
25 30
|
sseldd |
|- ( ( x e. A /\ y e. B ) -> <. x , y >. e. U_ x e. A ( { x } X. B ) ) |
32 |
31 1
|
eleqtrrdi |
|- ( ( x e. A /\ y e. B ) -> <. x , y >. e. T ) |
33 |
|
vex |
|- x e. _V |
34 |
|
vex |
|- y e. _V |
35 |
33 34
|
op2nd |
|- ( 2nd ` <. x , y >. ) = y |
36 |
|
fveqeq2 |
|- ( z = <. x , y >. -> ( ( 2nd ` z ) = y <-> ( 2nd ` <. x , y >. ) = y ) ) |
37 |
36
|
rspcev |
|- ( ( <. x , y >. e. T /\ ( 2nd ` <. x , y >. ) = y ) -> E. z e. T ( 2nd ` z ) = y ) |
38 |
32 35 37
|
sylancl |
|- ( ( x e. A /\ y e. B ) -> E. z e. T ( 2nd ` z ) = y ) |
39 |
38
|
ex |
|- ( x e. A -> ( y e. B -> E. z e. T ( 2nd ` z ) = y ) ) |
40 |
23 39
|
rexlimi |
|- ( E. x e. A y e. B -> E. z e. T ( 2nd ` z ) = y ) |
41 |
19 40
|
impbii |
|- ( E. z e. T ( 2nd ` z ) = y <-> E. x e. A y e. B ) |
42 |
|
fvelimab |
|- ( ( 2nd Fn _V /\ T C_ _V ) -> ( y e. ( 2nd " T ) <-> E. z e. T ( 2nd ` z ) = y ) ) |
43 |
5 6 42
|
mp2an |
|- ( y e. ( 2nd " T ) <-> E. z e. T ( 2nd ` z ) = y ) |
44 |
|
eliun |
|- ( y e. U_ x e. A B <-> E. x e. A y e. B ) |
45 |
41 43 44
|
3bitr4i |
|- ( y e. ( 2nd " T ) <-> y e. U_ x e. A B ) |
46 |
45
|
eqriv |
|- ( 2nd " T ) = U_ x e. A B |
47 |
9 46
|
eqtr3i |
|- ran ( 2nd |` T ) = U_ x e. A B |
48 |
|
df-fo |
|- ( ( 2nd |` T ) : T -onto-> U_ x e. A B <-> ( ( 2nd |` T ) Fn T /\ ran ( 2nd |` T ) = U_ x e. A B ) ) |
49 |
8 47 48
|
mpbir2an |
|- ( 2nd |` T ) : T -onto-> U_ x e. A B |