mapsnf1o

Description: A bijection between a set and single-point functions to it. (Contributed by Stefan O'Rear, 24-Jan-2015)

		Ref	Expression
	Hypothesis	ixpsnf1o.f	$⊢ F = (x \in A ⟼ \{I\} \times \{x\})$
	Assertion	mapsnf1o	$⊢ (A \in V \land I \in W) \to F : A \underset{1-1 onto}{⟶} A^{\{I\}}$

Step	Hyp	Ref	Expression
1		ixpsnf1o.f	$⊢ F = (x \in A ⟼ \{I\} \times \{x\})$
2	1	ixpsnf1o	$⊢ I \in W \to F : A \underset{1-1 onto}{⟶} \underset{y \in \{I\}}{⨉} A$
3	2	adantl	$⊢ (A \in V \land I \in W) \to F : A \underset{1-1 onto}{⟶} \underset{y \in \{I\}}{⨉} A$
4		snex	$⊢ \{I\} \in V$
5		ixpconstg	$⊢ (\{I\} \in V \land A \in V) \to \underset{y \in \{I\}}{⨉} A = A^{\{I\}}$
6	5	eqcomd	$⊢ (\{I\} \in V \land A \in V) \to A^{\{I\}} = \underset{y \in \{I\}}{⨉} A$
7	4 6	mpan	$⊢ A \in V \to A^{\{I\}} = \underset{y \in \{I\}}{⨉} A$
8	7	adantr	$⊢ (A \in V \land I \in W) \to A^{\{I\}} = \underset{y \in \{I\}}{⨉} A$
9	8	f1oeq3d	$⊢ (A \in V \land I \in W) \to (F : A \underset{1-1 onto}{⟶} A^{\{I\}} \leftrightarrow F : A \underset{1-1 onto}{⟶} \underset{y \in \{I\}}{⨉} A)$
10	3 9	mpbird	$⊢ (A \in V \land I \in W) \to F : A \underset{1-1 onto}{⟶} A^{\{I\}}$

Metamath Proof Explorer