mapsnop

Description: A singleton of an ordered pair as an element of the mapping operation. (Contributed by AV, 12-Apr-2019)

		Ref	Expression
	Hypothesis	mapsnop.f	$⊢ F = \{⟨X, Y⟩\}$
	Assertion	mapsnop	$⊢ (X \in V \land Y \in R \land R \in W) \to F \in (R^{\{X\}})$

Step	Hyp	Ref	Expression
1		mapsnop.f	$⊢ F = \{⟨X, Y⟩\}$
2		fsng	$⊢ (X \in V \land Y \in R) \to (F : \{X\} ⟶ \{Y\} \leftrightarrow F = \{⟨X, Y⟩\})$
3	2	3adant3	$⊢ (X \in V \land Y \in R \land R \in W) \to (F : \{X\} ⟶ \{Y\} \leftrightarrow F = \{⟨X, Y⟩\})$
4	1 3	mpbiri	$⊢ (X \in V \land Y \in R \land R \in W) \to F : \{X\} ⟶ \{Y\}$
5		snssi	$⊢ Y \in R \to \{Y\} \subseteq R$
6	5	3ad2ant2	$⊢ (X \in V \land Y \in R \land R \in W) \to \{Y\} \subseteq R$
7	4 6	fssd	$⊢ (X \in V \land Y \in R \land R \in W) \to F : \{X\} ⟶ R$
8		simp3	$⊢ (X \in V \land Y \in R \land R \in W) \to R \in W$
9		snex	$⊢ \{X\} \in V$
10		elmapg	$⊢ (R \in W \land \{X\} \in V) \to (F \in (R^{\{X\}}) \leftrightarrow F : \{X\} ⟶ R)$
11	8 9 10	sylancl	$⊢ (X \in V \land Y \in R \land R \in W) \to (F \in (R^{\{X\}}) \leftrightarrow F : \{X\} ⟶ R)$
12	7 11	mpbird	$⊢ (X \in V \land Y \in R \land R \in W) \to F \in (R^{\{X\}})$

Metamath Proof Explorer