f1un

Description: The union of two one-to-one functions with disjoint domains and codomains. (Contributed by BTernaryTau, 3-Dec-2024)

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

Proof

Step	Hyp	Ref	Expression
1		f1f	$⊢ F : A \underset{1-1}{⟶} B \to F : A ⟶ B$
2	1	frnd	$⊢ F : A \underset{1-1}{⟶} B \to ran F \subseteq B$
3		f1f	$⊢ G : C \underset{1-1}{⟶} D \to G : C ⟶ D$
4	3	frnd	$⊢ G : C \underset{1-1}{⟶} D \to ran G \subseteq D$
5		unss12	$⊢ (ran F \subseteq B \land ran G \subseteq D) \to ran F \cup ran G \subseteq B \cup D$
6	2 4 5	syl2an	$⊢ (F : A \underset{1-1}{⟶} B \land G : C \underset{1-1}{⟶} D) \to ran F \cup ran G \subseteq B \cup D$
7		f1f1orn	$⊢ F : A \underset{1-1}{⟶} B \to F : A \underset{1-1 onto}{⟶} ran F$
8		f1f1orn	$⊢ G : C \underset{1-1}{⟶} D \to G : C \underset{1-1 onto}{⟶} ran G$
9	7 8	anim12i	$⊢ (F : A \underset{1-1}{⟶} B \land G : C \underset{1-1}{⟶} D) \to (F : A \underset{1-1 onto}{⟶} ran F \land G : C \underset{1-1 onto}{⟶} ran G)$
10		simprl	$⊢ ((F : A \underset{1-1}{⟶} B \land G : C \underset{1-1}{⟶} D) \land (A \cap C = \emptyset \land B \cap D = \emptyset)) \to A \cap C = \emptyset$
11		ss2in	$⊢ (ran F \subseteq B \land ran G \subseteq D) \to ran F \cap ran G \subseteq B \cap D$
12	2 4 11	syl2an	$⊢ (F : A \underset{1-1}{⟶} B \land G : C \underset{1-1}{⟶} D) \to ran F \cap ran G \subseteq B \cap D$
13		sseq0	$⊢ (ran F \cap ran G \subseteq B \cap D \land B \cap D = \emptyset) \to ran F \cap ran G = \emptyset$
14	12 13	sylan	$⊢ ((F : A \underset{1-1}{⟶} B \land G : C \underset{1-1}{⟶} D) \land B \cap D = \emptyset) \to ran F \cap ran G = \emptyset$
15	14	adantrl	$⊢ ((F : A \underset{1-1}{⟶} B \land G : C \underset{1-1}{⟶} D) \land (A \cap C = \emptyset \land B \cap D = \emptyset)) \to ran F \cap ran G = \emptyset$
16	10 15	jca	$⊢ ((F : A \underset{1-1}{⟶} B \land G : C \underset{1-1}{⟶} D) \land (A \cap C = \emptyset \land B \cap D = \emptyset)) \to (A \cap C = \emptyset \land ran F \cap ran G = \emptyset)$
17		f1oun	$⊢ ((F : A \underset{1-1 onto}{⟶} ran F \land G : C \underset{1-1 onto}{⟶} ran G) \land (A \cap C = \emptyset \land ran F \cap ran G = \emptyset)) \to (F \cup G) : A \cup C \underset{1-1 onto}{⟶} ran F \cup ran G$
18	9 16 17	syl2an2r	$⊢ ((F : A \underset{1-1}{⟶} B \land G : C \underset{1-1}{⟶} D) \land (A \cap C = \emptyset \land B \cap D = \emptyset)) \to (F \cup G) : A \cup C \underset{1-1 onto}{⟶} ran F \cup ran G$
19		f1of1	$⊢ (F \cup G) : A \cup C \underset{1-1 onto}{⟶} ran F \cup ran G \to (F \cup G) : A \cup C \underset{1-1}{⟶} ran F \cup ran G$
20	18 19	syl	$⊢ ((F : A \underset{1-1}{⟶} B \land G : C \underset{1-1}{⟶} D) \land (A \cap C = \emptyset \land B \cap D = \emptyset)) \to (F \cup G) : A \cup C \underset{1-1}{⟶} ran F \cup ran G$
21		f1ss	$⊢ ((F \cup G) : A \cup C \underset{1-1}{⟶} ran F \cup ran G \land ran F \cup ran G \subseteq B \cup D) \to (F \cup G) : A \cup C \underset{1-1}{⟶} B \cup D$
22	21	ancoms	$⊢ (ran F \cup ran G \subseteq B \cup D \land (F \cup G) : A \cup C \underset{1-1}{⟶} ran F \cup ran G) \to (F \cup G) : A \cup C \underset{1-1}{⟶} B \cup D$
23	6 20 22	syl2an2r	$⊢ ((F : A \underset{1-1}{⟶} B \land G : C \underset{1-1}{⟶} D) \land (A \cap C = \emptyset \land B \cap D = \emptyset)) \to (F \cup G) : A \cup C \underset{1-1}{⟶} B \cup D$

Metamath Proof Explorer

Theorem f1un

Proof