This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 \in A, y \in B ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\})$
	Assertion	xpsff1o2	$⊢ F : A \times B \underset{1-1 onto}{⟶} ran F$

Proof

Step	Hyp	Ref	Expression
1		xpsff1o.f	$⊢ F = (x \in A, y \in B ⟼ \{⟨\emptyset, x⟩, ⟨1_{𝑜}, y⟩\})$
2	1	xpsff1o	$⊢ F : A \times B \underset{1-1 onto}{⟶} \underset{k \in 2_{𝑜}}{⨉} if (k = \emptyset, A, B)$
3		f1of1	$⊢ F : A \times B \underset{1-1 onto}{⟶} \underset{k \in 2_{𝑜}}{⨉} if (k = \emptyset, A, B) \to F : A \times B \underset{1-1}{⟶} \underset{k \in 2_{𝑜}}{⨉} if (k = \emptyset, A, B)$
4		f1f1orn	$⊢ F : A \times B \underset{1-1}{⟶} \underset{k \in 2_{𝑜}}{⨉} if (k = \emptyset, A, B) \to F : A \times B \underset{1-1 onto}{⟶} ran F$
5	2 3 4	mp2b	$⊢ F : A \times B \underset{1-1 onto}{⟶} ran F$