funcnvqp

Description: The converse quadruple 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) (Proof shortened by JJ, 14-Jul-2021)

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

Proof

Step	Hyp	Ref	Expression
1		funcnvpr	$⊢ (A \in U \land C \in V \land B \neq D) \to Fun {\{⟨A, B⟩, ⟨C, D⟩\}}^{-1}$
2	1	3expa	$⊢ ((A \in U \land C \in V) \land B \neq D) \to Fun {\{⟨A, B⟩, ⟨C, D⟩\}}^{-1}$
3	2	3ad2antr1	$⊢ ((A \in U \land C \in V) \land (B \neq D \land B \neq F \land B \neq H)) \to Fun {\{⟨A, B⟩, ⟨C, D⟩\}}^{-1}$
4	3	ad2ant2r	$⊢ (((A \in U \land C \in V) \land (E \in W \land G \in T)) \land ((B \neq D \land B \neq F \land B \neq H) \land F \neq H)) \to Fun {\{⟨A, B⟩, ⟨C, D⟩\}}^{-1}$
5	4	3adantr2	$⊢ (((A \in U \land C \in V) \land (E \in W \land G \in T)) \land ((B \neq D \land B \neq F \land B \neq H) \land (D \neq F \land D \neq H) \land F \neq H)) \to Fun {\{⟨A, B⟩, ⟨C, D⟩\}}^{-1}$
6		funcnvpr	$⊢ (E \in W \land G \in T \land F \neq H) \to Fun {\{⟨E, F⟩, ⟨G, H⟩\}}^{-1}$
7	6	3expa	$⊢ ((E \in W \land G \in T) \land F \neq H) \to Fun {\{⟨E, F⟩, ⟨G, H⟩\}}^{-1}$
8	7	ad2ant2l	$⊢ (((A \in U \land C \in V) \land (E \in W \land G \in T)) \land ((B \neq D \land B \neq F \land B \neq H) \land F \neq H)) \to Fun {\{⟨E, F⟩, ⟨G, H⟩\}}^{-1}$
9	8	3adantr2	$⊢ (((A \in U \land C \in V) \land (E \in W \land G \in T)) \land ((B \neq D \land B \neq F \land B \neq H) \land (D \neq F \land D \neq H) \land F \neq H)) \to Fun {\{⟨E, F⟩, ⟨G, H⟩\}}^{-1}$
10		df-rn	$⊢ ran \{⟨A, B⟩, ⟨C, D⟩\} = dom {\{⟨A, B⟩, ⟨C, D⟩\}}^{-1}$
11		rnpropg	$⊢ (A \in U \land C \in V) \to ran \{⟨A, B⟩, ⟨C, D⟩\} = \{B, D\}$
12	10 11	eqtr3id	$⊢ (A \in U \land C \in V) \to dom {\{⟨A, B⟩, ⟨C, D⟩\}}^{-1} = \{B, D\}$
13		df-rn	$⊢ ran \{⟨E, F⟩, ⟨G, H⟩\} = dom {\{⟨E, F⟩, ⟨G, H⟩\}}^{-1}$
14		rnpropg	$⊢ (E \in W \land G \in T) \to ran \{⟨E, F⟩, ⟨G, H⟩\} = \{F, H\}$
15	13 14	eqtr3id	$⊢ (E \in W \land G \in T) \to dom {\{⟨E, F⟩, ⟨G, H⟩\}}^{-1} = \{F, H\}$
16	12 15	ineqan12d	$⊢ ((A \in U \land C \in V) \land (E \in W \land G \in T)) \to dom {\{⟨A, B⟩, ⟨C, D⟩\}}^{-1} \cap dom {\{⟨E, F⟩, ⟨G, H⟩\}}^{-1} = \{B, D\} \cap \{F, H\}$
17		disjpr2	$⊢ ((B \neq F \land D \neq F) \land (B \neq H \land D \neq H)) \to \{B, D\} \cap \{F, H\} = \emptyset$
18	17	an4s	$⊢ ((B \neq F \land B \neq H) \land (D \neq F \land D \neq H)) \to \{B, D\} \cap \{F, H\} = \emptyset$
19	18	3adantl1	$⊢ ((B \neq D \land B \neq F \land B \neq H) \land (D \neq F \land D \neq H)) \to \{B, D\} \cap \{F, H\} = \emptyset$
20	19	3adant3	$⊢ ((B \neq D \land B \neq F \land B \neq H) \land (D \neq F \land D \neq H) \land F \neq H) \to \{B, D\} \cap \{F, H\} = \emptyset$
21	16 20	sylan9eq	$⊢ (((A \in U \land C \in V) \land (E \in W \land G \in T)) \land ((B \neq D \land B \neq F \land B \neq H) \land (D \neq F \land D \neq H) \land F \neq H)) \to dom {\{⟨A, B⟩, ⟨C, D⟩\}}^{-1} \cap dom {\{⟨E, F⟩, ⟨G, H⟩\}}^{-1} = \emptyset$
22		funun	$⊢ ((Fun {\{⟨A, B⟩, ⟨C, D⟩\}}^{-1} \land Fun {\{⟨E, F⟩, ⟨G, H⟩\}}^{-1}) \land dom {\{⟨A, B⟩, ⟨C, D⟩\}}^{-1} \cap dom {\{⟨E, F⟩, ⟨G, H⟩\}}^{-1} = \emptyset) \to Fun ({\{⟨A, B⟩, ⟨C, D⟩\}}^{-1} \cup {\{⟨E, F⟩, ⟨G, H⟩\}}^{-1})$
23	5 9 21 22	syl21anc	$⊢ (((A \in U \land C \in V) \land (E \in W \land G \in T)) \land ((B \neq D \land B \neq F \land B \neq H) \land (D \neq F \land D \neq H) \land F \neq H)) \to Fun ({\{⟨A, B⟩, ⟨C, D⟩\}}^{-1} \cup {\{⟨E, F⟩, ⟨G, H⟩\}}^{-1})$
24		cnvun	$⊢ {(\{⟨A, B⟩, ⟨C, D⟩\} \cup \{⟨E, F⟩, ⟨G, H⟩\})}^{-1} = {\{⟨A, B⟩, ⟨C, D⟩\}}^{-1} \cup {\{⟨E, F⟩, ⟨G, H⟩\}}^{-1}$
25	24	funeqi	$⊢ Fun {(\{⟨A, B⟩, ⟨C, D⟩\} \cup \{⟨E, F⟩, ⟨G, H⟩\})}^{-1} \leftrightarrow Fun ({\{⟨A, B⟩, ⟨C, D⟩\}}^{-1} \cup {\{⟨E, F⟩, ⟨G, H⟩\}}^{-1})$
26	23 25	sylibr	$⊢ (((A \in U \land C \in V) \land (E \in W \land G \in T)) \land ((B \neq D \land B \neq F \land B \neq H) \land (D \neq F \land D \neq H) \land F \neq H)) \to Fun {(\{⟨A, B⟩, ⟨C, D⟩\} \cup \{⟨E, F⟩, ⟨G, H⟩\})}^{-1}$

Metamath Proof Explorer

Theorem funcnvqp

Proof