funcnvtp

Description: The converse triple of ordered pairs is a function if the second members are pairwise different. Note that the second members need not be sets. (Contributed by AV, 23-Jan-2021)

		Ref	Expression
	Assertion	funcnvtp	$⊢ ((A \in U \land C \in V \land E \in W) \land (B \neq D \land B \neq F \land D \neq F)) \to Fun {\{⟨A, B⟩, ⟨C, D⟩, ⟨E, F⟩\}}^{-1}$

Proof

Step	Hyp	Ref	Expression
1		simp1	$⊢ (A \in U \land C \in V \land E \in W) \to A \in U$
2		simp2	$⊢ (A \in U \land C \in V \land E \in W) \to C \in V$
3		simp1	$⊢ (B \neq D \land B \neq F \land D \neq F) \to B \neq D$
4		funcnvpr	$⊢ (A \in U \land C \in V \land B \neq D) \to Fun {\{⟨A, B⟩, ⟨C, D⟩\}}^{-1}$
5	1 2 3 4	syl2an3an	$⊢ ((A \in U \land C \in V \land E \in W) \land (B \neq D \land B \neq F \land D \neq F)) \to Fun {\{⟨A, B⟩, ⟨C, D⟩\}}^{-1}$
6		funcnvsn	$⊢ Fun {\{⟨E, F⟩\}}^{-1}$
7	6	a1i	$⊢ ((A \in U \land C \in V \land E \in W) \land (B \neq D \land B \neq F \land D \neq F)) \to Fun {\{⟨E, F⟩\}}^{-1}$
8		df-rn	$⊢ ran \{⟨A, B⟩, ⟨C, D⟩\} = dom {\{⟨A, B⟩, ⟨C, D⟩\}}^{-1}$
9		rnpropg	$⊢ (A \in U \land C \in V) \to ran \{⟨A, B⟩, ⟨C, D⟩\} = \{B, D\}$
10	8 9	eqtr3id	$⊢ (A \in U \land C \in V) \to dom {\{⟨A, B⟩, ⟨C, D⟩\}}^{-1} = \{B, D\}$
11	10	3adant3	$⊢ (A \in U \land C \in V \land E \in W) \to dom {\{⟨A, B⟩, ⟨C, D⟩\}}^{-1} = \{B, D\}$
12		df-rn	$⊢ ran \{⟨E, F⟩\} = dom {\{⟨E, F⟩\}}^{-1}$
13		rnsnopg	$⊢ E \in W \to ran \{⟨E, F⟩\} = \{F\}$
14	12 13	eqtr3id	$⊢ E \in W \to dom {\{⟨E, F⟩\}}^{-1} = \{F\}$
15	14	3ad2ant3	$⊢ (A \in U \land C \in V \land E \in W) \to dom {\{⟨E, F⟩\}}^{-1} = \{F\}$
16	11 15	ineq12d	$⊢ (A \in U \land C \in V \land E \in W) \to dom {\{⟨A, B⟩, ⟨C, D⟩\}}^{-1} \cap dom {\{⟨E, F⟩\}}^{-1} = \{B, D\} \cap \{F\}$
17		disjprsn	$⊢ (B \neq F \land D \neq F) \to \{B, D\} \cap \{F\} = \emptyset$
18	17	3adant1	$⊢ (B \neq D \land B \neq F \land D \neq F) \to \{B, D\} \cap \{F\} = \emptyset$
19	16 18	sylan9eq	$⊢ ((A \in U \land C \in V \land E \in W) \land (B \neq D \land B \neq F \land D \neq F)) \to dom {\{⟨A, B⟩, ⟨C, D⟩\}}^{-1} \cap dom {\{⟨E, F⟩\}}^{-1} = \emptyset$
20		funun	$⊢ ((Fun {\{⟨A, B⟩, ⟨C, D⟩\}}^{-1} \land Fun {\{⟨E, F⟩\}}^{-1}) \land dom {\{⟨A, B⟩, ⟨C, D⟩\}}^{-1} \cap dom {\{⟨E, F⟩\}}^{-1} = \emptyset) \to Fun ({\{⟨A, B⟩, ⟨C, D⟩\}}^{-1} \cup {\{⟨E, F⟩\}}^{-1})$
21	5 7 19 20	syl21anc	$⊢ ((A \in U \land C \in V \land E \in W) \land (B \neq D \land B \neq F \land D \neq F)) \to Fun ({\{⟨A, B⟩, ⟨C, D⟩\}}^{-1} \cup {\{⟨E, F⟩\}}^{-1})$
22		df-tp	$⊢ \{⟨A, B⟩, ⟨C, D⟩, ⟨E, F⟩\} = \{⟨A, B⟩, ⟨C, D⟩\} \cup \{⟨E, F⟩\}$
23	22	cnveqi	$⊢ {\{⟨A, B⟩, ⟨C, D⟩, ⟨E, F⟩\}}^{-1} = {(\{⟨A, B⟩, ⟨C, D⟩\} \cup \{⟨E, F⟩\})}^{-1}$
24		cnvun	$⊢ {(\{⟨A, B⟩, ⟨C, D⟩\} \cup \{⟨E, F⟩\})}^{-1} = {\{⟨A, B⟩, ⟨C, D⟩\}}^{-1} \cup {\{⟨E, F⟩\}}^{-1}$
25	23 24	eqtri	$⊢ {\{⟨A, B⟩, ⟨C, D⟩, ⟨E, F⟩\}}^{-1} = {\{⟨A, B⟩, ⟨C, D⟩\}}^{-1} \cup {\{⟨E, F⟩\}}^{-1}$
26	25	funeqi	$⊢ Fun {\{⟨A, B⟩, ⟨C, D⟩, ⟨E, F⟩\}}^{-1} \leftrightarrow Fun ({\{⟨A, B⟩, ⟨C, D⟩\}}^{-1} \cup {\{⟨E, F⟩\}}^{-1})$
27	21 26	sylibr	$⊢ ((A \in U \land C \in V \land E \in W) \land (B \neq D \land B \neq F \land D \neq F)) \to Fun {\{⟨A, B⟩, ⟨C, D⟩, ⟨E, F⟩\}}^{-1}$

Metamath Proof Explorer

Theorem funcnvtp

Proof