ftpg

Description: A function with a domain of three elements. (Contributed by Alexander van der Vekens, 4-Dec-2017)

		Ref	Expression
	Assertion	ftpg	$⊢ ((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⟩\} : \{X, Y, Z\} ⟶ \{A, B, 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		fprg	$⊢ ((X \in U \land Y \in V) \land (A \in F \land B \in G) \land X \neq Y) \to \{⟨X, A⟩, ⟨Y, B⟩\} : \{X, Y\} ⟶ \{A, 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 \{⟨X, A⟩, ⟨Y, B⟩\} : \{X, Y\} ⟶ \{A, B\}$
6		eqidd	$⊢ ((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 \{⟨Z, C⟩\} = \{⟨Z, C⟩\}$
7		simp3	$⊢ (X \in U \land Y \in V \land Z \in W) \to Z \in W$
8		simp3	$⊢ (A \in F \land B \in G \land C \in H) \to C \in H$
9	7 8	anim12i	$⊢ ((X \in U \land Y \in V \land Z \in W) \land (A \in F \land B \in G \land C \in H)) \to (Z \in W \land C \in H)$
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 (Z \in W \land C \in H)$
11		fsng	$⊢ (Z \in W \land C \in H) \to (\{⟨Z, C⟩\} : \{Z\} ⟶ \{C\} \leftrightarrow \{⟨Z, C⟩\} = \{⟨Z, C⟩\})$
12	10 11	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 (\{⟨Z, C⟩\} : \{Z\} ⟶ \{C\} \leftrightarrow \{⟨Z, C⟩\} = \{⟨Z, C⟩\})$
13	6 12	mpbird	$⊢ ((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 \{⟨Z, C⟩\} : \{Z\} ⟶ \{C\}$
14		elpri	$⊢ Z \in \{X, Y\} \to (Z = X \lor Z = Y)$
15		eqcom	$⊢ Z = X \leftrightarrow X = Z$
16		nne	$⊢ \neg X \neq Z \leftrightarrow X = Z$
17	15 16	bitr4i	$⊢ Z = X \leftrightarrow \neg X \neq Z$
18		eqcom	$⊢ Z = Y \leftrightarrow Y = Z$
19		nne	$⊢ \neg Y \neq Z \leftrightarrow Y = Z$
20	18 19	bitr4i	$⊢ Z = Y \leftrightarrow \neg Y \neq Z$
21	17 20	orbi12i	$⊢ (Z = X \lor Z = Y) \leftrightarrow (\neg X \neq Z \lor \neg Y \neq Z)$
22		ianor	$⊢ \neg (X \neq Z \land Y \neq Z) \leftrightarrow (\neg X \neq Z \lor \neg Y \neq Z)$
23	21 22	sylbb2	$⊢ (Z = X \lor Z = Y) \to \neg (X \neq Z \land Y \neq Z)$
24	14 23	syl	$⊢ Z \in \{X, Y\} \to \neg (X \neq Z \land Y \neq Z)$
25	24	con2i	$⊢ (X \neq Z \land Y \neq Z) \to \neg Z \in \{X, Y\}$
26	25	3adant1	$⊢ (X \neq Y \land X \neq Z \land Y \neq Z) \to \neg Z \in \{X, Y\}$
27	26	3ad2ant3	$⊢ ((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 \neg Z \in \{X, Y\}$
28		disjsn	$⊢ \{X, Y\} \cap \{Z\} = \emptyset \leftrightarrow \neg Z \in \{X, Y\}$
29	27 28	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 \{X, Y\} \cap \{Z\} = \emptyset$
30		fun	$⊢ ((\{⟨X, A⟩, ⟨Y, B⟩\} : \{X, Y\} ⟶ \{A, B\} \land \{⟨Z, C⟩\} : \{Z\} ⟶ \{C\}) \land \{X, Y\} \cap \{Z\} = \emptyset) \to (\{⟨X, A⟩, ⟨Y, B⟩\} \cup \{⟨Z, C⟩\}) : \{X, Y\} \cup \{Z\} ⟶ \{A, B\} \cup \{C\}$
31	5 13 29 30	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 (\{⟨X, A⟩, ⟨Y, B⟩\} \cup \{⟨Z, C⟩\}) : \{X, Y\} \cup \{Z\} ⟶ \{A, B\} \cup \{C\}$
32		df-tp	$⊢ \{⟨X, A⟩, ⟨Y, B⟩, ⟨Z, C⟩\} = \{⟨X, A⟩, ⟨Y, B⟩\} \cup \{⟨Z, C⟩\}$
33	32	feq1i	$⊢ \{⟨X, A⟩, ⟨Y, B⟩, ⟨Z, C⟩\} : \{X, Y, Z\} ⟶ \{A, B, C\} \leftrightarrow (\{⟨X, A⟩, ⟨Y, B⟩\} \cup \{⟨Z, C⟩\}) : \{X, Y, Z\} ⟶ \{A, B, C\}$
34		df-tp	$⊢ \{X, Y, Z\} = \{X, Y\} \cup \{Z\}$
35		df-tp	$⊢ \{A, B, C\} = \{A, B\} \cup \{C\}$
36	34 35	feq23i	$⊢ (\{⟨X, A⟩, ⟨Y, B⟩\} \cup \{⟨Z, C⟩\}) : \{X, Y, Z\} ⟶ \{A, B, C\} \leftrightarrow (\{⟨X, A⟩, ⟨Y, B⟩\} \cup \{⟨Z, C⟩\}) : \{X, Y\} \cup \{Z\} ⟶ \{A, B\} \cup \{C\}$
37	33 36	bitri	$⊢ \{⟨X, A⟩, ⟨Y, B⟩, ⟨Z, C⟩\} : \{X, Y, Z\} ⟶ \{A, B, C\} \leftrightarrow (\{⟨X, A⟩, ⟨Y, B⟩\} \cup \{⟨Z, C⟩\}) : \{X, Y\} \cup \{Z\} ⟶ \{A, B\} \cup \{C\}$
38	31 37	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 \{⟨X, A⟩, ⟨Y, B⟩, ⟨Z, C⟩\} : \{X, Y, Z\} ⟶ \{A, B, C\}$

Metamath Proof Explorer

Theorem ftpg

Proof