Metamath Proof Explorer

Theorem f1oun

Description: The union of two one-to-one onto functions with disjoint domains and ranges. (Contributed by NM, 26-Mar-1998)

		Ref	Expression
	Assertion	f1oun	$⊢ ((F : A \underset{1-1 onto}{⟶} B \land G : C \underset{1-1 onto}{⟶} D) \land (A \cap C = \emptyset \land B \cap D = \emptyset)) \to (F \cup G) : A \cup C \underset{1-1 onto}{⟶} B \cup D$

Proof

Step	Hyp	Ref	Expression
1		dff1o4	$⊢ F : A \underset{1-1 onto}{⟶} B \leftrightarrow (F Fn A \land F^{-1} Fn B)$
2		dff1o4	$⊢ G : C \underset{1-1 onto}{⟶} D \leftrightarrow (G Fn C \land G^{-1} Fn D)$
3		fnun	$⊢ ((F Fn A \land G Fn C) \land A \cap C = \emptyset) \to (F \cup G) Fn (A \cup C)$
4	3	ex	$⊢ (F Fn A \land G Fn C) \to (A \cap C = \emptyset \to (F \cup G) Fn (A \cup C))$
5		fnun	$⊢ ((F^{-1} Fn B \land G^{-1} Fn D) \land B \cap D = \emptyset) \to (F^{-1} \cup G^{-1}) Fn (B \cup D)$
6		cnvun	$⊢ {(F \cup G)}^{-1} = F^{-1} \cup G^{-1}$
7	6	fneq1i	$⊢ {(F \cup G)}^{-1} Fn (B \cup D) \leftrightarrow (F^{-1} \cup G^{-1}) Fn (B \cup D)$
8	5 7	sylibr	$⊢ ((F^{-1} Fn B \land G^{-1} Fn D) \land B \cap D = \emptyset) \to {(F \cup G)}^{-1} Fn (B \cup D)$
9	8	ex	$⊢ (F^{-1} Fn B \land G^{-1} Fn D) \to (B \cap D = \emptyset \to {(F \cup G)}^{-1} Fn (B \cup D))$
10	4 9	im2anan9	$⊢ ((F Fn A \land G Fn C) \land (F^{-1} Fn B \land G^{-1} Fn D)) \to ((A \cap C = \emptyset \land B \cap D = \emptyset) \to ((F \cup G) Fn (A \cup C) \land {(F \cup G)}^{-1} Fn (B \cup D)))$
11	10	an4s	$⊢ ((F Fn A \land F^{-1} Fn B) \land (G Fn C \land G^{-1} Fn D)) \to ((A \cap C = \emptyset \land B \cap D = \emptyset) \to ((F \cup G) Fn (A \cup C) \land {(F \cup G)}^{-1} Fn (B \cup D)))$
12	1 2 11	syl2anb	$⊢ (F : A \underset{1-1 onto}{⟶} B \land G : C \underset{1-1 onto}{⟶} D) \to ((A \cap C = \emptyset \land B \cap D = \emptyset) \to ((F \cup G) Fn (A \cup C) \land {(F \cup G)}^{-1} Fn (B \cup D)))$
13		dff1o4	$⊢ (F \cup G) : A \cup C \underset{1-1 onto}{⟶} B \cup D \leftrightarrow ((F \cup G) Fn (A \cup C) \land {(F \cup G)}^{-1} Fn (B \cup D))$
14	12 13	imbitrrdi	$⊢ (F : A \underset{1-1 onto}{⟶} B \land G : C \underset{1-1 onto}{⟶} D) \to ((A \cap C = \emptyset \land B \cap D = \emptyset) \to (F \cup G) : A \cup C \underset{1-1 onto}{⟶} B \cup D)$
15	14	imp	$⊢ ((F : A \underset{1-1 onto}{⟶} B \land G : C \underset{1-1 onto}{⟶} D) \land (A \cap C = \emptyset \land B \cap D = \emptyset)) \to (F \cup G) : A \cup C \underset{1-1 onto}{⟶} B \cup D$