Metamath Proof Explorer

Theorem funprg

Description: A set of two pairs is a function if their first members are different. (Contributed by FL, 26-Jun-2011) (Proof shortened by JJ, 14-Jul-2021)

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

Proof

Step	Hyp	Ref	Expression
1		funsng	$⊢ (A \in V \land C \in X) \to Fun \{⟨A, C⟩\}$
2		funsng	$⊢ (B \in W \land D \in Y) \to Fun \{⟨B, D⟩\}$
3	1 2	anim12i	$⊢ ((A \in V \land C \in X) \land (B \in W \land D \in Y)) \to (Fun \{⟨A, C⟩\} \land Fun \{⟨B, D⟩\})$
4	3	an4s	$⊢ ((A \in V \land B \in W) \land (C \in X \land D \in Y)) \to (Fun \{⟨A, C⟩\} \land Fun \{⟨B, D⟩\})$
5	4	3adant3	$⊢ ((A \in V \land B \in W) \land (C \in X \land D \in Y) \land A \neq B) \to (Fun \{⟨A, C⟩\} \land Fun \{⟨B, D⟩\})$
6		dmsnopg	$⊢ C \in X \to dom \{⟨A, C⟩\} = \{A\}$
7		dmsnopg	$⊢ D \in Y \to dom \{⟨B, D⟩\} = \{B\}$
8	6 7	ineqan12d	$⊢ (C \in X \land D \in Y) \to dom \{⟨A, C⟩\} \cap dom \{⟨B, D⟩\} = \{A\} \cap \{B\}$
9		disjsn2	$⊢ A \neq B \to \{A\} \cap \{B\} = \emptyset$
10	8 9	sylan9eq	$⊢ ((C \in X \land D \in Y) \land A \neq B) \to dom \{⟨A, C⟩\} \cap dom \{⟨B, D⟩\} = \emptyset$
11	10	3adant1	$⊢ ((A \in V \land B \in W) \land (C \in X \land D \in Y) \land A \neq B) \to dom \{⟨A, C⟩\} \cap dom \{⟨B, D⟩\} = \emptyset$
12		funun	$⊢ ((Fun \{⟨A, C⟩\} \land Fun \{⟨B, D⟩\}) \land dom \{⟨A, C⟩\} \cap dom \{⟨B, D⟩\} = \emptyset) \to Fun (\{⟨A, C⟩\} \cup \{⟨B, D⟩\})$
13	5 11 12	syl2anc	$⊢ ((A \in V \land B \in W) \land (C \in X \land D \in Y) \land A \neq B) \to Fun (\{⟨A, C⟩\} \cup \{⟨B, D⟩\})$
14		df-pr	$⊢ \{⟨A, C⟩, ⟨B, D⟩\} = \{⟨A, C⟩\} \cup \{⟨B, D⟩\}$
15	14	funeqi	$⊢ Fun \{⟨A, C⟩, ⟨B, D⟩\} \leftrightarrow Fun (\{⟨A, C⟩\} \cup \{⟨B, D⟩\})$
16	13 15	sylibr	$⊢ ((A \in V \land B \in W) \land (C \in X \land D \in Y) \land A \neq B) \to Fun \{⟨A, C⟩, ⟨B, D⟩\}$