Description: A short expression for the indexed cartesian product on two indices. (Contributed by Mario Carneiro, 15-Aug-2015)
Ref | Expression | ||
---|---|---|---|
Hypothesis | xpsff1o.f | |- F = ( x e. A , y e. B |-> { <. (/) , x >. , <. 1o , y >. } ) |
|
Assertion | xpsfrn | |- ran F = X_ k e. 2o if ( k = (/) , A , B ) |
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 | f1ofo | |- ( F : ( A X. B ) -1-1-onto-> X_ k e. 2o if ( k = (/) , A , B ) -> F : ( A X. B ) -onto-> X_ k e. 2o if ( k = (/) , A , B ) ) |
|
4 | forn | |- ( F : ( A X. B ) -onto-> X_ k e. 2o if ( k = (/) , A , B ) -> ran F = X_ k e. 2o if ( k = (/) , A , B ) ) |
|
5 | 2 3 4 | mp2b | |- ran F = X_ k e. 2o if ( k = (/) , A , B ) |