funtpg

Description: A set of three pairs is a function if their first members are different. (Contributed by Alexander van der Vekens, 5-Dec-2017) (Proof shortened by JJ, 14-Jul-2021)

		Ref	Expression
	Assertion	funtpg	$⊢ ((X \in U \land Y \in V \land Z \in W) \land (A \in F \land B \in G \land C \in H) \land (X \neq Y \land X \neq Z \land Y \neq Z)) \to Fun \{⟨X, A⟩, ⟨Y, B⟩, ⟨Z, C⟩\}$

Proof

Step	Hyp	Ref	Expression
1		3simpa	$⊢ (X \in U \land Y \in V \land Z \in W) \to (X \in U \land Y \in V)$
2		3simpa	$⊢ (A \in F \land B \in G \land C \in H) \to (A \in F \land B \in G)$
3		simp1	$⊢ (X \neq Y \land X \neq Z \land Y \neq Z) \to X \neq Y$
4		funprg	$⊢ ((X \in U \land Y \in V) \land (A \in F \land B \in G) \land X \neq Y) \to Fun \{⟨X, A⟩, ⟨Y, B⟩\}$
5	1 2 3 4	syl3an	$⊢ ((X \in U \land Y \in V \land Z \in W) \land (A \in F \land B \in G \land C \in H) \land (X \neq Y \land X \neq Z \land Y \neq Z)) \to Fun \{⟨X, A⟩, ⟨Y, B⟩\}$
6		simp3	$⊢ (X \in U \land Y \in V \land Z \in W) \to Z \in W$
7		simp3	$⊢ (A \in F \land B \in G \land C \in H) \to C \in H$
8		funsng	$⊢ (Z \in W \land C \in H) \to Fun \{⟨Z, C⟩\}$
9	6 7 8	syl2an	$⊢ ((X \in U \land Y \in V \land Z \in W) \land (A \in F \land B \in G \land C \in H)) \to Fun \{⟨Z, C⟩\}$
10	9	3adant3	$⊢ ((X \in U \land Y \in V \land Z \in W) \land (A \in F \land B \in G \land C \in H) \land (X \neq Y \land X \neq Z \land Y \neq Z)) \to Fun \{⟨Z, C⟩\}$
11		dmpropg	$⊢ (A \in F \land B \in G) \to dom \{⟨X, A⟩, ⟨Y, B⟩\} = \{X, Y\}$
12		dmsnopg	$⊢ C \in H \to dom \{⟨Z, C⟩\} = \{Z\}$
13	11 12	ineqan12d	$⊢ ((A \in F \land B \in G) \land C \in H) \to dom \{⟨X, A⟩, ⟨Y, B⟩\} \cap dom \{⟨Z, C⟩\} = \{X, Y\} \cap \{Z\}$
14	13	3impa	$⊢ (A \in F \land B \in G \land C \in H) \to dom \{⟨X, A⟩, ⟨Y, B⟩\} \cap dom \{⟨Z, C⟩\} = \{X, Y\} \cap \{Z\}$
15		disjprsn	$⊢ (X \neq Z \land Y \neq Z) \to \{X, Y\} \cap \{Z\} = \emptyset$
16	15	3adant1	$⊢ (X \neq Y \land X \neq Z \land Y \neq Z) \to \{X, Y\} \cap \{Z\} = \emptyset$
17	14 16	sylan9eq	$⊢ ((A \in F \land B \in G \land C \in H) \land (X \neq Y \land X \neq Z \land Y \neq Z)) \to dom \{⟨X, A⟩, ⟨Y, B⟩\} \cap dom \{⟨Z, C⟩\} = \emptyset$
18	17	3adant1	$⊢ ((X \in U \land Y \in V \land Z \in W) \land (A \in F \land B \in G \land C \in H) \land (X \neq Y \land X \neq Z \land Y \neq Z)) \to dom \{⟨X, A⟩, ⟨Y, B⟩\} \cap dom \{⟨Z, C⟩\} = \emptyset$
19		funun	$⊢ ((Fun \{⟨X, A⟩, ⟨Y, B⟩\} \land Fun \{⟨Z, C⟩\}) \land dom \{⟨X, A⟩, ⟨Y, B⟩\} \cap dom \{⟨Z, C⟩\} = \emptyset) \to Fun (\{⟨X, A⟩, ⟨Y, B⟩\} \cup \{⟨Z, C⟩\})$
20	5 10 18 19	syl21anc	$⊢ ((X \in U \land Y \in V \land Z \in W) \land (A \in F \land B \in G \land C \in H) \land (X \neq Y \land X \neq Z \land Y \neq Z)) \to Fun (\{⟨X, A⟩, ⟨Y, B⟩\} \cup \{⟨Z, C⟩\})$
21		df-tp	$⊢ \{⟨X, A⟩, ⟨Y, B⟩, ⟨Z, C⟩\} = \{⟨X, A⟩, ⟨Y, B⟩\} \cup \{⟨Z, C⟩\}$
22	21	funeqi	$⊢ Fun \{⟨X, A⟩, ⟨Y, B⟩, ⟨Z, C⟩\} \leftrightarrow Fun (\{⟨X, A⟩, ⟨Y, B⟩\} \cup \{⟨Z, C⟩\})$
23	20 22	sylibr	$⊢ ((X \in U \land Y \in V \land Z \in W) \land (A \in F \land B \in G \land C \in H) \land (X \neq Y \land X \neq Z \land Y \neq Z)) \to Fun \{⟨X, A⟩, ⟨Y, B⟩, ⟨Z, C⟩\}$

Metamath Proof Explorer

Theorem funtpg

Proof