Theorem metakunt17

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

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

Proof

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