metakunt17

Description: The union of three disjoint bijections is a bijection. (Contributed by metakunt, 28-May-2024)

	Ref	Expression
Hypotheses	metakunt17.1	$⊢ φ \to G : A \underset{1-1 onto}{⟶} X$
	metakunt17.2	$⊢ φ \to H : B \underset{1-1 onto}{⟶} Y$
	metakunt17.3	$⊢ φ \to I : C \underset{1-1 onto}{⟶} Z$
	metakunt17.4	$⊢ φ \to A \cap B = \emptyset$
	metakunt17.5	$⊢ φ \to A \cap C = \emptyset$
	metakunt17.6	$⊢ φ \to B \cap C = \emptyset$
	metakunt17.7	$⊢ φ \to X \cap Y = \emptyset$
	metakunt17.8	$⊢ φ \to X \cap Z = \emptyset$
	metakunt17.9	$⊢ φ \to Y \cap Z = \emptyset$
	metakunt17.10	$⊢ φ \to F = (G \cup H) \cup I$
	metakunt17.11	$⊢ φ \to D = (A \cup B) \cup C$
	metakunt17.12	$⊢ φ \to W = (X \cup Y) \cup Z$
Assertion	metakunt17	$⊢ φ \to F : D \underset{1-1 onto}{⟶} W$

Proof

Step	Hyp	Ref	Expression
1		metakunt17.1	$⊢ φ \to G : A \underset{1-1 onto}{⟶} X$
2		metakunt17.2	$⊢ φ \to H : B \underset{1-1 onto}{⟶} Y$
3		metakunt17.3	$⊢ φ \to I : C \underset{1-1 onto}{⟶} Z$
4		metakunt17.4	$⊢ φ \to A \cap B = \emptyset$
5		metakunt17.5	$⊢ φ \to A \cap C = \emptyset$
6		metakunt17.6	$⊢ φ \to B \cap C = \emptyset$
7		metakunt17.7	$⊢ φ \to X \cap Y = \emptyset$
8		metakunt17.8	$⊢ φ \to X \cap Z = \emptyset$
9		metakunt17.9	$⊢ φ \to Y \cap Z = \emptyset$
10		metakunt17.10	$⊢ φ \to F = (G \cup H) \cup I$
11		metakunt17.11	$⊢ φ \to D = (A \cup B) \cup C$
12		metakunt17.12	$⊢ φ \to W = (X \cup Y) \cup Z$
13	4 7	jca	$⊢ φ \to (A \cap B = \emptyset \land X \cap Y = \emptyset)$
14	1 2 13	jca31	$⊢ φ \to ((G : A \underset{1-1 onto}{⟶} X \land H : B \underset{1-1 onto}{⟶} Y) \land (A \cap B = \emptyset \land X \cap Y = \emptyset))$
15		f1oun	$⊢ ((G : A \underset{1-1 onto}{⟶} X \land H : B \underset{1-1 onto}{⟶} Y) \land (A \cap B = \emptyset \land X \cap Y = \emptyset)) \to (G \cup H) : A \cup B \underset{1-1 onto}{⟶} X \cup Y$
16	14 15	syl	$⊢ φ \to (G \cup H) : A \cup B \underset{1-1 onto}{⟶} X \cup Y$
17		indir	$⊢ (A \cup B) \cap C = (A \cap C) \cup (B \cap C)$
18	5 6	uneq12d	$⊢ φ \to (A \cap C) \cup (B \cap C) = \emptyset \cup \emptyset$
19		0un	$⊢ \emptyset \cup \emptyset = \emptyset$
20	19	a1i	$⊢ φ \to \emptyset \cup \emptyset = \emptyset$
21	18 20	eqtrd	$⊢ φ \to (A \cap C) \cup (B \cap C) = \emptyset$
22	17 21	syl5eq	$⊢ φ \to (A \cup B) \cap C = \emptyset$
23		indir	$⊢ (X \cup Y) \cap Z = (X \cap Z) \cup (Y \cap Z)$
24	8 9	uneq12d	$⊢ φ \to (X \cap Z) \cup (Y \cap Z) = \emptyset \cup \emptyset$
25	24 20	eqtrd	$⊢ φ \to (X \cap Z) \cup (Y \cap Z) = \emptyset$
26	23 25	syl5eq	$⊢ φ \to (X \cup Y) \cap Z = \emptyset$
27	22 26	jca	$⊢ φ \to ((A \cup B) \cap C = \emptyset \land (X \cup Y) \cap Z = \emptyset)$
28	16 3 27	jca31	$⊢ φ \to (((G \cup H) : A \cup B \underset{1-1 onto}{⟶} X \cup Y \land I : C \underset{1-1 onto}{⟶} Z) \land ((A \cup B) \cap C = \emptyset \land (X \cup Y) \cap Z = \emptyset))$
29		f1oun	$⊢ (((G \cup H) : A \cup B \underset{1-1 onto}{⟶} X \cup Y \land I : C \underset{1-1 onto}{⟶} Z) \land ((A \cup B) \cap C = \emptyset \land (X \cup Y) \cap Z = \emptyset)) \to ((G \cup H) \cup I) : (A \cup B) \cup C \underset{1-1 onto}{⟶} (X \cup Y) \cup Z$
30	28 29	syl	$⊢ φ \to ((G \cup H) \cup I) : (A \cup B) \cup C \underset{1-1 onto}{⟶} (X \cup Y) \cup Z$
31	10 11 12	f1oeq123d	$⊢ φ \to (F : D \underset{1-1 onto}{⟶} W \leftrightarrow ((G \cup H) \cup I) : (A \cup B) \cup C \underset{1-1 onto}{⟶} (X \cup Y) \cup Z)$
32	30 31	mpbird	$⊢ φ \to F : D \underset{1-1 onto}{⟶} W$

Metamath Proof Explorer

Theorem metakunt17

Proof