f1oprg

Description: An unordered pair of ordered pairs with different elements is a one-to-one onto function, analogous to f1oprswap . (Contributed by Alexander van der Vekens, 14-Aug-2017)

		Ref	Expression
	Assertion	f1oprg	$⊢ ((A \in V \land B \in W) \land (C \in X \land D \in Y)) \to ((A \neq C \land B \neq D) \to \{⟨A, B⟩, ⟨C, D⟩\} : \{A, C\} \underset{1-1 onto}{⟶} \{B, D\})$

Proof

Step	Hyp	Ref	Expression
1		f1osng	$⊢ (A \in V \land B \in W) \to \{⟨A, B⟩\} : \{A\} \underset{1-1 onto}{⟶} \{B\}$
2	1	ad2antrr	$⊢ (((A \in V \land B \in W) \land (C \in X \land D \in Y)) \land (A \neq C \land B \neq D)) \to \{⟨A, B⟩\} : \{A\} \underset{1-1 onto}{⟶} \{B\}$
3		f1osng	$⊢ (C \in X \land D \in Y) \to \{⟨C, D⟩\} : \{C\} \underset{1-1 onto}{⟶} \{D\}$
4	3	ad2antlr	$⊢ (((A \in V \land B \in W) \land (C \in X \land D \in Y)) \land (A \neq C \land B \neq D)) \to \{⟨C, D⟩\} : \{C\} \underset{1-1 onto}{⟶} \{D\}$
5		disjsn2	$⊢ A \neq C \to \{A\} \cap \{C\} = \emptyset$
6	5	ad2antrl	$⊢ (((A \in V \land B \in W) \land (C \in X \land D \in Y)) \land (A \neq C \land B \neq D)) \to \{A\} \cap \{C\} = \emptyset$
7		disjsn2	$⊢ B \neq D \to \{B\} \cap \{D\} = \emptyset$
8	7	ad2antll	$⊢ (((A \in V \land B \in W) \land (C \in X \land D \in Y)) \land (A \neq C \land B \neq D)) \to \{B\} \cap \{D\} = \emptyset$
9		f1oun	$⊢ ((\{⟨A, B⟩\} : \{A\} \underset{1-1 onto}{⟶} \{B\} \land \{⟨C, D⟩\} : \{C\} \underset{1-1 onto}{⟶} \{D\}) \land (\{A\} \cap \{C\} = \emptyset \land \{B\} \cap \{D\} = \emptyset)) \to (\{⟨A, B⟩\} \cup \{⟨C, D⟩\}) : \{A\} \cup \{C\} \underset{1-1 onto}{⟶} \{B\} \cup \{D\}$
10	2 4 6 8 9	syl22anc	$⊢ (((A \in V \land B \in W) \land (C \in X \land D \in Y)) \land (A \neq C \land B \neq D)) \to (\{⟨A, B⟩\} \cup \{⟨C, D⟩\}) : \{A\} \cup \{C\} \underset{1-1 onto}{⟶} \{B\} \cup \{D\}$
11		df-pr	$⊢ \{⟨A, B⟩, ⟨C, D⟩\} = \{⟨A, B⟩\} \cup \{⟨C, D⟩\}$
12	11	eqcomi	$⊢ \{⟨A, B⟩\} \cup \{⟨C, D⟩\} = \{⟨A, B⟩, ⟨C, D⟩\}$
13	12	a1i	$⊢ (((A \in V \land B \in W) \land (C \in X \land D \in Y)) \land (A \neq C \land B \neq D)) \to \{⟨A, B⟩\} \cup \{⟨C, D⟩\} = \{⟨A, B⟩, ⟨C, D⟩\}$
14		df-pr	$⊢ \{A, C\} = \{A\} \cup \{C\}$
15	14	eqcomi	$⊢ \{A\} \cup \{C\} = \{A, C\}$
16	15	a1i	$⊢ (((A \in V \land B \in W) \land (C \in X \land D \in Y)) \land (A \neq C \land B \neq D)) \to \{A\} \cup \{C\} = \{A, C\}$
17		df-pr	$⊢ \{B, D\} = \{B\} \cup \{D\}$
18	17	eqcomi	$⊢ \{B\} \cup \{D\} = \{B, D\}$
19	18	a1i	$⊢ (((A \in V \land B \in W) \land (C \in X \land D \in Y)) \land (A \neq C \land B \neq D)) \to \{B\} \cup \{D\} = \{B, D\}$
20	13 16 19	f1oeq123d	$⊢ (((A \in V \land B \in W) \land (C \in X \land D \in Y)) \land (A \neq C \land B \neq D)) \to ((\{⟨A, B⟩\} \cup \{⟨C, D⟩\}) : \{A\} \cup \{C\} \underset{1-1 onto}{⟶} \{B\} \cup \{D\} \leftrightarrow \{⟨A, B⟩, ⟨C, D⟩\} : \{A, C\} \underset{1-1 onto}{⟶} \{B, D\})$
21	10 20	mpbid	$⊢ (((A \in V \land B \in W) \land (C \in X \land D \in Y)) \land (A \neq C \land B \neq D)) \to \{⟨A, B⟩, ⟨C, D⟩\} : \{A, C\} \underset{1-1 onto}{⟶} \{B, D\}$
22	21	ex	$⊢ ((A \in V \land B \in W) \land (C \in X \land D \in Y)) \to ((A \neq C \land B \neq D) \to \{⟨A, B⟩, ⟨C, D⟩\} : \{A, C\} \underset{1-1 onto}{⟶} \{B, D\})$

Metamath Proof Explorer

Theorem f1oprg

Proof