Metamath Proof Explorer

Theorem mapprop

Description: An unordered pair containing two ordered pairs as an element of the mapping operation. (Contributed by AV, 16-Apr-2019) (Proof shortened by AV, 2-Jun-2024)

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

Proof

Step	Hyp	Ref	Expression
1		mapprop.f	$⊢ F = \{⟨X, A⟩, ⟨Y, B⟩\}$
2		simp3r	$⊢ ((X \in V \land A \in R) \land (Y \in V \land B \in R) \land (X \neq Y \land R \in W)) \to R \in W$
3		simpl	$⊢ (X \in V \land A \in R) \to X \in V$
4		simpl	$⊢ (Y \in V \land B \in R) \to Y \in V$
5		simpl	$⊢ (X \neq Y \land R \in W) \to X \neq Y$
6	3 4 5	3anim123i	$⊢ ((X \in V \land A \in R) \land (Y \in V \land B \in R) \land (X \neq Y \land R \in W)) \to (X \in V \land Y \in V \land X \neq Y)$
7		simpr	$⊢ (X \in V \land A \in R) \to A \in R$
8		simpr	$⊢ (Y \in V \land B \in R) \to B \in R$
9	7 8	anim12i	$⊢ ((X \in V \land A \in R) \land (Y \in V \land B \in R)) \to (A \in R \land B \in R)$
10	9	3adant3	$⊢ ((X \in V \land A \in R) \land (Y \in V \land B \in R) \land (X \neq Y \land R \in W)) \to (A \in R \land B \in R)$
11		fprmappr	$⊢ (R \in W \land (X \in V \land Y \in V \land X \neq Y) \land (A \in R \land B \in R)) \to \{⟨X, A⟩, ⟨Y, B⟩\} \in (R^{\{X, Y\}})$
12	2 6 10 11	syl3anc	$⊢ ((X \in V \land A \in R) \land (Y \in V \land B \in R) \land (X \neq Y \land R \in W)) \to \{⟨X, A⟩, ⟨Y, B⟩\} \in (R^{\{X, Y\}})$
13	1 12	eqeltrid	$⊢ ((X \in V \land A \in R) \land (Y \in V \land B \in R) \land (X \neq Y \land R \in W)) \to F \in (R^{\{X, Y\}})$