Metamath Proof Explorer

Theorem xpsff1o

Description: The function appearing in xpsval is a bijection from the cartesian product to the indexed cartesian product indexed on the pair 2o = { (/) , 1o } . (Contributed by Mario Carneiro, 15-Aug-2015)

Ref Expression
Hypothesis xpsff1o.f 
|- F = ( x e. A , y e. B |-> { <. (/) , x >. , <. 1o , y >. } )
Assertion xpsff1o 
|- F : ( A X. B ) -1-1-onto-> X_ k e. 2o if ( k = (/) , A , B )

Proof

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 imbitrrid 
 |-  ( ( 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 )