Metamath Proof Explorer

Theorem fprmappr

Description: A function with a domain of two elements as element of the mapping operator applied to a pair. (Contributed by AV, 20-May-2024)

		Ref	Expression
	Assertion	fprmappr	$⊢ (X \in V \land (A \in U \land B \in W \land A \neq B) \land (C \in X \land D \in X)) \to \{⟨A, C⟩, ⟨B, D⟩\} \in (X^{\{A, B\}})$

Proof

Step	Hyp	Ref	Expression
1		3simpa	$⊢ (A \in U \land B \in W \land A \neq B) \to (A \in U \land B \in W)$
2	1	adantr	$⊢ ((A \in U \land B \in W \land A \neq B) \land (C \in X \land D \in X)) \to (A \in U \land B \in W)$
3		simpr	$⊢ ((A \in U \land B \in W \land A \neq B) \land (C \in X \land D \in X)) \to (C \in X \land D \in X)$
4		simpl3	$⊢ ((A \in U \land B \in W \land A \neq B) \land (C \in X \land D \in X)) \to A \neq B$
5		fprg	$⊢ ((A \in U \land B \in W) \land (C \in X \land D \in X) \land A \neq B) \to \{⟨A, C⟩, ⟨B, D⟩\} : \{A, B\} ⟶ \{C, D\}$
6	2 3 4 5	syl3anc	$⊢ ((A \in U \land B \in W \land A \neq B) \land (C \in X \land D \in X)) \to \{⟨A, C⟩, ⟨B, D⟩\} : \{A, B\} ⟶ \{C, D\}$
7		prssi	$⊢ (C \in X \land D \in X) \to \{C, D\} \subseteq X$
8	7	adantl	$⊢ ((A \in U \land B \in W \land A \neq B) \land (C \in X \land D \in X)) \to \{C, D\} \subseteq X$
9	6 8	fssd	$⊢ ((A \in U \land B \in W \land A \neq B) \land (C \in X \land D \in X)) \to \{⟨A, C⟩, ⟨B, D⟩\} : \{A, B\} ⟶ X$
10	9	3adant1	$⊢ (X \in V \land (A \in U \land B \in W \land A \neq B) \land (C \in X \land D \in X)) \to \{⟨A, C⟩, ⟨B, D⟩\} : \{A, B\} ⟶ X$
11		simp1	$⊢ (X \in V \land (A \in U \land B \in W \land A \neq B) \land (C \in X \land D \in X)) \to X \in V$
12		prex	$⊢ \{A, B\} \in V$
13	12	a1i	$⊢ (X \in V \land (A \in U \land B \in W \land A \neq B) \land (C \in X \land D \in X)) \to \{A, B\} \in V$
14	11 13	elmapd	$⊢ (X \in V \land (A \in U \land B \in W \land A \neq B) \land (C \in X \land D \in X)) \to (\{⟨A, C⟩, ⟨B, D⟩\} \in (X^{\{A, B\}}) \leftrightarrow \{⟨A, C⟩, ⟨B, D⟩\} : \{A, B\} ⟶ X)$
15	10 14	mpbird	$⊢ (X \in V \land (A \in U \land B \in W \land A \neq B) \land (C \in X \land D \in X)) \to \{⟨A, C⟩, ⟨B, D⟩\} \in (X^{\{A, B\}})$