Metamath Proof Explorer


Theorem xpsff1o2

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

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 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