Metamath Proof Explorer


Theorem xpsfrn

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 )

Proof

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 )