Step |
Hyp |
Ref |
Expression |
1 |
|
xpsff1o.f |
|- F = ( x e. A , y e. B |-> { <. (/) , x >. , <. 1o , y >. } ) |
2 |
|
xpsfrnel2 |
|- ( { <. (/) , x >. , <. 1o , y >. } e. X_ k e. 2o if ( k = (/) , A , B ) <-> ( x e. A /\ y e. B ) ) |
3 |
2
|
biimpri |
|- ( ( x e. A /\ y e. B ) -> { <. (/) , x >. , <. 1o , y >. } e. X_ k e. 2o if ( k = (/) , A , B ) ) |
4 |
3
|
rgen2 |
|- A. x e. A A. y e. B { <. (/) , x >. , <. 1o , y >. } e. X_ k e. 2o if ( k = (/) , A , B ) |
5 |
1
|
fmpo |
|- ( A. x e. A A. y e. B { <. (/) , x >. , <. 1o , y >. } e. X_ k e. 2o if ( k = (/) , A , B ) <-> F : ( A X. B ) --> X_ k e. 2o if ( k = (/) , A , B ) ) |
6 |
4 5
|
mpbi |
|- F : ( A X. B ) --> X_ k e. 2o if ( k = (/) , A , B ) |
7 |
|
1st2nd2 |
|- ( z e. ( A X. B ) -> z = <. ( 1st ` z ) , ( 2nd ` z ) >. ) |
8 |
7
|
fveq2d |
|- ( z e. ( A X. B ) -> ( F ` z ) = ( F ` <. ( 1st ` z ) , ( 2nd ` z ) >. ) ) |
9 |
|
df-ov |
|- ( ( 1st ` z ) F ( 2nd ` z ) ) = ( F ` <. ( 1st ` z ) , ( 2nd ` z ) >. ) |
10 |
|
xp1st |
|- ( z e. ( A X. B ) -> ( 1st ` z ) e. A ) |
11 |
|
xp2nd |
|- ( z e. ( A X. B ) -> ( 2nd ` z ) e. B ) |
12 |
1
|
xpsfval |
|- ( ( ( 1st ` z ) e. A /\ ( 2nd ` z ) e. B ) -> ( ( 1st ` z ) F ( 2nd ` z ) ) = { <. (/) , ( 1st ` z ) >. , <. 1o , ( 2nd ` z ) >. } ) |
13 |
10 11 12
|
syl2anc |
|- ( z e. ( A X. B ) -> ( ( 1st ` z ) F ( 2nd ` z ) ) = { <. (/) , ( 1st ` z ) >. , <. 1o , ( 2nd ` z ) >. } ) |
14 |
9 13
|
eqtr3id |
|- ( z e. ( A X. B ) -> ( F ` <. ( 1st ` z ) , ( 2nd ` z ) >. ) = { <. (/) , ( 1st ` z ) >. , <. 1o , ( 2nd ` z ) >. } ) |
15 |
8 14
|
eqtrd |
|- ( z e. ( A X. B ) -> ( F ` z ) = { <. (/) , ( 1st ` z ) >. , <. 1o , ( 2nd ` z ) >. } ) |
16 |
|
1st2nd2 |
|- ( w e. ( A X. B ) -> w = <. ( 1st ` w ) , ( 2nd ` w ) >. ) |
17 |
16
|
fveq2d |
|- ( w e. ( A X. B ) -> ( F ` w ) = ( F ` <. ( 1st ` w ) , ( 2nd ` w ) >. ) ) |
18 |
|
df-ov |
|- ( ( 1st ` w ) F ( 2nd ` w ) ) = ( F ` <. ( 1st ` w ) , ( 2nd ` w ) >. ) |
19 |
|
xp1st |
|- ( w e. ( A X. B ) -> ( 1st ` w ) e. A ) |
20 |
|
xp2nd |
|- ( w e. ( A X. B ) -> ( 2nd ` w ) e. B ) |
21 |
1
|
xpsfval |
|- ( ( ( 1st ` w ) e. A /\ ( 2nd ` w ) e. B ) -> ( ( 1st ` w ) F ( 2nd ` w ) ) = { <. (/) , ( 1st ` w ) >. , <. 1o , ( 2nd ` w ) >. } ) |
22 |
19 20 21
|
syl2anc |
|- ( w e. ( A X. B ) -> ( ( 1st ` w ) F ( 2nd ` w ) ) = { <. (/) , ( 1st ` w ) >. , <. 1o , ( 2nd ` w ) >. } ) |
23 |
18 22
|
eqtr3id |
|- ( w e. ( A X. B ) -> ( F ` <. ( 1st ` w ) , ( 2nd ` w ) >. ) = { <. (/) , ( 1st ` w ) >. , <. 1o , ( 2nd ` w ) >. } ) |
24 |
17 23
|
eqtrd |
|- ( w e. ( A X. B ) -> ( F ` w ) = { <. (/) , ( 1st ` w ) >. , <. 1o , ( 2nd ` w ) >. } ) |
25 |
15 24
|
eqeqan12d |
|- ( ( z e. ( A X. B ) /\ w e. ( A X. B ) ) -> ( ( F ` z ) = ( F ` w ) <-> { <. (/) , ( 1st ` z ) >. , <. 1o , ( 2nd ` z ) >. } = { <. (/) , ( 1st ` w ) >. , <. 1o , ( 2nd ` w ) >. } ) ) |
26 |
|
fveq1 |
|- ( { <. (/) , ( 1st ` z ) >. , <. 1o , ( 2nd ` z ) >. } = { <. (/) , ( 1st ` w ) >. , <. 1o , ( 2nd ` w ) >. } -> ( { <. (/) , ( 1st ` z ) >. , <. 1o , ( 2nd ` z ) >. } ` (/) ) = ( { <. (/) , ( 1st ` w ) >. , <. 1o , ( 2nd ` w ) >. } ` (/) ) ) |
27 |
|
fvex |
|- ( 1st ` z ) e. _V |
28 |
|
fvpr0o |
|- ( ( 1st ` z ) e. _V -> ( { <. (/) , ( 1st ` z ) >. , <. 1o , ( 2nd ` z ) >. } ` (/) ) = ( 1st ` z ) ) |
29 |
27 28
|
ax-mp |
|- ( { <. (/) , ( 1st ` z ) >. , <. 1o , ( 2nd ` z ) >. } ` (/) ) = ( 1st ` z ) |
30 |
|
fvex |
|- ( 1st ` w ) e. _V |
31 |
|
fvpr0o |
|- ( ( 1st ` w ) e. _V -> ( { <. (/) , ( 1st ` w ) >. , <. 1o , ( 2nd ` w ) >. } ` (/) ) = ( 1st ` w ) ) |
32 |
30 31
|
ax-mp |
|- ( { <. (/) , ( 1st ` w ) >. , <. 1o , ( 2nd ` w ) >. } ` (/) ) = ( 1st ` w ) |
33 |
26 29 32
|
3eqtr3g |
|- ( { <. (/) , ( 1st ` z ) >. , <. 1o , ( 2nd ` z ) >. } = { <. (/) , ( 1st ` w ) >. , <. 1o , ( 2nd ` w ) >. } -> ( 1st ` z ) = ( 1st ` w ) ) |
34 |
|
fveq1 |
|- ( { <. (/) , ( 1st ` z ) >. , <. 1o , ( 2nd ` z ) >. } = { <. (/) , ( 1st ` w ) >. , <. 1o , ( 2nd ` w ) >. } -> ( { <. (/) , ( 1st ` z ) >. , <. 1o , ( 2nd ` z ) >. } ` 1o ) = ( { <. (/) , ( 1st ` w ) >. , <. 1o , ( 2nd ` w ) >. } ` 1o ) ) |
35 |
|
fvex |
|- ( 2nd ` z ) e. _V |
36 |
|
fvpr1o |
|- ( ( 2nd ` z ) e. _V -> ( { <. (/) , ( 1st ` z ) >. , <. 1o , ( 2nd ` z ) >. } ` 1o ) = ( 2nd ` z ) ) |
37 |
35 36
|
ax-mp |
|- ( { <. (/) , ( 1st ` z ) >. , <. 1o , ( 2nd ` z ) >. } ` 1o ) = ( 2nd ` z ) |
38 |
|
fvex |
|- ( 2nd ` w ) e. _V |
39 |
|
fvpr1o |
|- ( ( 2nd ` w ) e. _V -> ( { <. (/) , ( 1st ` w ) >. , <. 1o , ( 2nd ` w ) >. } ` 1o ) = ( 2nd ` w ) ) |
40 |
38 39
|
ax-mp |
|- ( { <. (/) , ( 1st ` w ) >. , <. 1o , ( 2nd ` w ) >. } ` 1o ) = ( 2nd ` w ) |
41 |
34 37 40
|
3eqtr3g |
|- ( { <. (/) , ( 1st ` z ) >. , <. 1o , ( 2nd ` z ) >. } = { <. (/) , ( 1st ` w ) >. , <. 1o , ( 2nd ` w ) >. } -> ( 2nd ` z ) = ( 2nd ` w ) ) |
42 |
33 41
|
opeq12d |
|- ( { <. (/) , ( 1st ` z ) >. , <. 1o , ( 2nd ` z ) >. } = { <. (/) , ( 1st ` w ) >. , <. 1o , ( 2nd ` w ) >. } -> <. ( 1st ` z ) , ( 2nd ` z ) >. = <. ( 1st ` w ) , ( 2nd ` w ) >. ) |
43 |
7 16
|
eqeqan12d |
|- ( ( z e. ( A X. B ) /\ w e. ( A X. B ) ) -> ( z = w <-> <. ( 1st ` z ) , ( 2nd ` z ) >. = <. ( 1st ` w ) , ( 2nd ` w ) >. ) ) |
44 |
42 43
|
syl5ibr |
|- ( ( z e. ( A X. B ) /\ w e. ( A X. B ) ) -> ( { <. (/) , ( 1st ` z ) >. , <. 1o , ( 2nd ` z ) >. } = { <. (/) , ( 1st ` w ) >. , <. 1o , ( 2nd ` w ) >. } -> z = w ) ) |
45 |
25 44
|
sylbid |
|- ( ( z e. ( A X. B ) /\ w e. ( A X. B ) ) -> ( ( F ` z ) = ( F ` w ) -> z = w ) ) |
46 |
45
|
rgen2 |
|- A. z e. ( A X. B ) A. w e. ( A X. B ) ( ( F ` z ) = ( F ` w ) -> z = w ) |
47 |
|
dff13 |
|- ( F : ( A X. B ) -1-1-> X_ k e. 2o if ( k = (/) , A , B ) <-> ( F : ( A X. B ) --> X_ k e. 2o if ( k = (/) , A , B ) /\ A. z e. ( A X. B ) A. w e. ( A X. B ) ( ( F ` z ) = ( F ` w ) -> z = w ) ) ) |
48 |
6 46 47
|
mpbir2an |
|- F : ( A X. B ) -1-1-> X_ k e. 2o if ( k = (/) , A , B ) |
49 |
|
xpsfrnel |
|- ( z e. X_ k e. 2o if ( k = (/) , A , B ) <-> ( z Fn 2o /\ ( z ` (/) ) e. A /\ ( z ` 1o ) e. B ) ) |
50 |
49
|
simp2bi |
|- ( z e. X_ k e. 2o if ( k = (/) , A , B ) -> ( z ` (/) ) e. A ) |
51 |
49
|
simp3bi |
|- ( z e. X_ k e. 2o if ( k = (/) , A , B ) -> ( z ` 1o ) e. B ) |
52 |
1
|
xpsfval |
|- ( ( ( z ` (/) ) e. A /\ ( z ` 1o ) e. B ) -> ( ( z ` (/) ) F ( z ` 1o ) ) = { <. (/) , ( z ` (/) ) >. , <. 1o , ( z ` 1o ) >. } ) |
53 |
50 51 52
|
syl2anc |
|- ( z e. X_ k e. 2o if ( k = (/) , A , B ) -> ( ( z ` (/) ) F ( z ` 1o ) ) = { <. (/) , ( z ` (/) ) >. , <. 1o , ( z ` 1o ) >. } ) |
54 |
|
ixpfn |
|- ( z e. X_ k e. 2o if ( k = (/) , A , B ) -> z Fn 2o ) |
55 |
|
xpsfeq |
|- ( z Fn 2o -> { <. (/) , ( z ` (/) ) >. , <. 1o , ( z ` 1o ) >. } = z ) |
56 |
54 55
|
syl |
|- ( z e. X_ k e. 2o if ( k = (/) , A , B ) -> { <. (/) , ( z ` (/) ) >. , <. 1o , ( z ` 1o ) >. } = z ) |
57 |
53 56
|
eqtr2d |
|- ( z e. X_ k e. 2o if ( k = (/) , A , B ) -> z = ( ( z ` (/) ) F ( z ` 1o ) ) ) |
58 |
|
rspceov |
|- ( ( ( z ` (/) ) e. A /\ ( z ` 1o ) e. B /\ z = ( ( z ` (/) ) F ( z ` 1o ) ) ) -> E. a e. A E. b e. B z = ( a F b ) ) |
59 |
50 51 57 58
|
syl3anc |
|- ( z e. X_ k e. 2o if ( k = (/) , A , B ) -> E. a e. A E. b e. B z = ( a F b ) ) |
60 |
59
|
rgen |
|- A. z e. X_ k e. 2o if ( k = (/) , A , B ) E. a e. A E. b e. B z = ( a F b ) |
61 |
|
foov |
|- ( F : ( A X. B ) -onto-> X_ k e. 2o if ( k = (/) , A , B ) <-> ( F : ( A X. B ) --> X_ k e. 2o if ( k = (/) , A , B ) /\ A. z e. X_ k e. 2o if ( k = (/) , A , B ) E. a e. A E. b e. B z = ( a F b ) ) ) |
62 |
6 60 61
|
mpbir2an |
|- F : ( A X. B ) -onto-> X_ k e. 2o if ( k = (/) , A , B ) |
63 |
|
df-f1o |
|- ( F : ( A X. B ) -1-1-onto-> X_ k e. 2o if ( k = (/) , A , B ) <-> ( F : ( A X. B ) -1-1-> X_ k e. 2o if ( k = (/) , A , B ) /\ F : ( A X. B ) -onto-> X_ k e. 2o if ( k = (/) , A , B ) ) ) |
64 |
48 62 63
|
mpbir2an |
|- F : ( A X. B ) -1-1-onto-> X_ k e. 2o if ( k = (/) , A , B ) |