fntpg

Description: Function with a domain of three different values. (Contributed by Alexander van der Vekens, 5-Dec-2017)

		Ref	Expression
	Assertion	fntpg	$⊢ ((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 \{⟨X, A⟩, ⟨Y, B⟩, ⟨Z, C⟩\} Fn \{X, Y, Z\}$

Proof

Step	Hyp	Ref	Expression
1		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⟩\}$
2		dmsnopg	$⊢ A \in F \to dom \{⟨X, A⟩\} = \{X\}$
3	2	3ad2ant1	$⊢ (A \in F \land B \in G \land C \in H) \to dom \{⟨X, A⟩\} = \{X\}$
4		dmsnopg	$⊢ B \in G \to dom \{⟨Y, B⟩\} = \{Y\}$
5	4	3ad2ant2	$⊢ (A \in F \land B \in G \land C \in H) \to dom \{⟨Y, B⟩\} = \{Y\}$
6	3 5	jca	$⊢ (A \in F \land B \in G \land C \in H) \to (dom \{⟨X, A⟩\} = \{X\} \land dom \{⟨Y, B⟩\} = \{Y\})$
7	6	3ad2ant2	$⊢ ((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⟩\} = \{X\} \land dom \{⟨Y, B⟩\} = \{Y\})$
8		uneq12	$⊢ (dom \{⟨X, A⟩\} = \{X\} \land dom \{⟨Y, B⟩\} = \{Y\}) \to dom \{⟨X, A⟩\} \cup dom \{⟨Y, B⟩\} = \{X\} \cup \{Y\}$
9	7 8	syl	$⊢ ((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⟩\} \cup dom \{⟨Y, B⟩\} = \{X\} \cup \{Y\}$
10		df-pr	$⊢ \{X, Y\} = \{X\} \cup \{Y\}$
11	9 10	eqtr4di	$⊢ ((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⟩\} \cup dom \{⟨Y, B⟩\} = \{X, Y\}$
12		df-pr	$⊢ \{⟨X, A⟩, ⟨Y, B⟩\} = \{⟨X, A⟩\} \cup \{⟨Y, B⟩\}$
13	12	dmeqi	$⊢ dom \{⟨X, A⟩, ⟨Y, B⟩\} = dom (\{⟨X, A⟩\} \cup \{⟨Y, B⟩\})$
14	13	eqeq1i	$⊢ dom \{⟨X, A⟩, ⟨Y, B⟩\} = \{X, Y\} \leftrightarrow dom (\{⟨X, A⟩\} \cup \{⟨Y, B⟩\}) = \{X, Y\}$
15		dmun	$⊢ dom (\{⟨X, A⟩\} \cup \{⟨Y, B⟩\}) = dom \{⟨X, A⟩\} \cup dom \{⟨Y, B⟩\}$
16	15	eqeq1i	$⊢ dom (\{⟨X, A⟩\} \cup \{⟨Y, B⟩\}) = \{X, Y\} \leftrightarrow dom \{⟨X, A⟩\} \cup dom \{⟨Y, B⟩\} = \{X, Y\}$
17	14 16	bitri	$⊢ dom \{⟨X, A⟩, ⟨Y, B⟩\} = \{X, Y\} \leftrightarrow dom \{⟨X, A⟩\} \cup dom \{⟨Y, B⟩\} = \{X, Y\}$
18	11 17	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 dom \{⟨X, A⟩, ⟨Y, B⟩\} = \{X, Y\}$
19		dmsnopg	$⊢ C \in H \to dom \{⟨Z, C⟩\} = \{Z\}$
20	19	3ad2ant3	$⊢ (A \in F \land B \in G \land C \in H) \to dom \{⟨Z, C⟩\} = \{Z\}$
21	20	3ad2ant2	$⊢ ((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 \{⟨Z, C⟩\} = \{Z\}$
22	18 21	uneq12d	$⊢ ((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⟩\} \cup dom \{⟨Z, C⟩\} = \{X, Y\} \cup \{Z\}$
23		df-tp	$⊢ \{⟨X, A⟩, ⟨Y, B⟩, ⟨Z, C⟩\} = \{⟨X, A⟩, ⟨Y, B⟩\} \cup \{⟨Z, C⟩\}$
24	23	dmeqi	$⊢ dom \{⟨X, A⟩, ⟨Y, B⟩, ⟨Z, C⟩\} = dom (\{⟨X, A⟩, ⟨Y, B⟩\} \cup \{⟨Z, C⟩\})$
25		dmun	$⊢ dom (\{⟨X, A⟩, ⟨Y, B⟩\} \cup \{⟨Z, C⟩\}) = dom \{⟨X, A⟩, ⟨Y, B⟩\} \cup dom \{⟨Z, C⟩\}$
26	24 25	eqtri	$⊢ dom \{⟨X, A⟩, ⟨Y, B⟩, ⟨Z, C⟩\} = dom \{⟨X, A⟩, ⟨Y, B⟩\} \cup dom \{⟨Z, C⟩\}$
27		df-tp	$⊢ \{X, Y, Z\} = \{X, Y\} \cup \{Z\}$
28	22 26 27	3eqtr4g	$⊢ ((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⟩, ⟨Z, C⟩\} = \{X, Y, Z\}$
29		df-fn	$⊢ \{⟨X, A⟩, ⟨Y, B⟩, ⟨Z, C⟩\} Fn \{X, Y, Z\} \leftrightarrow (Fun \{⟨X, A⟩, ⟨Y, B⟩, ⟨Z, C⟩\} \land dom \{⟨X, A⟩, ⟨Y, B⟩, ⟨Z, C⟩\} = \{X, Y, Z\})$
30	1 28 29	sylanbrc	$⊢ ((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 \{⟨X, A⟩, ⟨Y, B⟩, ⟨Z, C⟩\} Fn \{X, Y, Z\}$

Metamath Proof Explorer

Theorem fntpg

Proof