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, 24-Jan-2015)
Ref | Expression | ||
---|---|---|---|
Hypothesis | xpsff1o.f | |- F = ( x e. A , y e. B |-> { <. (/) , x >. , <. 1o , y >. } ) |
|
Assertion | xpsff1o2 | |- F : ( A X. B ) -1-1-onto-> ran F |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | xpsff1o.f | |- F = ( x e. A , y e. B |-> { <. (/) , x >. , <. 1o , y >. } ) |
|
2 | 1 | xpsff1o | |- F : ( A X. B ) -1-1-onto-> X_ k e. 2o if ( k = (/) , A , B ) |
3 | f1of1 | |- ( 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 ) ) |
|
4 | f1f1orn | |- ( F : ( A X. B ) -1-1-> X_ k e. 2o if ( k = (/) , A , B ) -> F : ( A X. B ) -1-1-onto-> ran F ) |
|
5 | 2 3 4 | mp2b | |- F : ( A X. B ) -1-1-onto-> ran F |