Theorem founiiun0

Description: Union expressed as an indexed union, when a map onto is given. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Assertion	founiiun0	$$⊢F:A\underset{onto}{⟶}B\cup \left\{\varnothing \right\}\to \bigcup B=\bigcup _{x\in A}F\left(x\right)$$

Proof

Step	Hyp	Ref	Expression
1		uniiun	$$⊢\bigcup B=\bigcup _{y\in B}y$$
2		elun1	$$⊢y\in B\to y\in \left(B\cup \left\{\varnothing \right\}\right)$$
3		foelcdmi	$$⊢\left(F:A\underset{onto}{⟶}B\cup \left\{\varnothing \right\}\wedge y\in \left(B\cup \left\{\varnothing \right\}\right)\right)\to \exists x\in AF\left(x\right)=y$$
4	2 3	sylan2	$$⊢\left(F:A\underset{onto}{⟶}B\cup \left\{\varnothing \right\}\wedge y\in B\right)\to \exists x\in AF\left(x\right)=y$$
5		eqimss2	$$⊢F\left(x\right)=y\to y\subseteq F\left(x\right)$$
6	5	reximi	$$⊢\exists x\in AF\left(x\right)=y\to \exists x\in Ay\subseteq F\left(x\right)$$
7	4 6	syl	$$⊢\left(F:A\underset{onto}{⟶}B\cup \left\{\varnothing \right\}\wedge y\in B\right)\to \exists x\in Ay\subseteq F\left(x\right)$$
8	7	ralrimiva	$$⊢F:A\underset{onto}{⟶}B\cup \left\{\varnothing \right\}\to \forall y\in B\exists x\in Ay\subseteq F\left(x\right)$$
9		iunss2	$$⊢\forall y\in B\exists x\in Ay\subseteq F\left(x\right)\to \bigcup _{y\in B}y\subseteq \bigcup _{x\in A}F\left(x\right)$$
10	8 9	syl	$$⊢F:A\underset{onto}{⟶}B\cup \left\{\varnothing \right\}\to \bigcup _{y\in B}y\subseteq \bigcup _{x\in A}F\left(x\right)$$
11		simpl	$$⊢\left(F:A\underset{onto}{⟶}B\cup \left\{\varnothing \right\}\wedge B=\varnothing \right)\to F:A\underset{onto}{⟶}B\cup \left\{\varnothing \right\}$$
12		uneq1	$$⊢B=\varnothing \to B\cup \left\{\varnothing \right\}=\varnothing \cup \left\{\varnothing \right\}$$
13		0un	$$⊢\varnothing \cup \left\{\varnothing \right\}=\left\{\varnothing \right\}$$
14	12 13	eqtrdi	$$⊢B=\varnothing \to B\cup \left\{\varnothing \right\}=\left\{\varnothing \right\}$$
15	14	adantl	$$⊢\left(F:A\underset{onto}{⟶}B\cup \left\{\varnothing \right\}\wedge B=\varnothing \right)\to B\cup \left\{\varnothing \right\}=\left\{\varnothing \right\}$$
16		foeq3	$$⊢B\cup \left\{\varnothing \right\}=\left\{\varnothing \right\}\to \left(F:A\underset{onto}{⟶}B\cup \left\{\varnothing \right\}\leftrightarrow F:A\underset{onto}{⟶}\left\{\varnothing \right\}\right)$$
17	15 16	syl	$$⊢\left(F:A\underset{onto}{⟶}B\cup \left\{\varnothing \right\}\wedge B=\varnothing \right)\to \left(F:A\underset{onto}{⟶}B\cup \left\{\varnothing \right\}\leftrightarrow F:A\underset{onto}{⟶}\left\{\varnothing \right\}\right)$$
18	11 17	mpbid	$$⊢\left(F:A\underset{onto}{⟶}B\cup \left\{\varnothing \right\}\wedge B=\varnothing \right)\to F:A\underset{onto}{⟶}\left\{\varnothing \right\}$$
19		founiiun	$$⊢F:A\underset{onto}{⟶}\left\{\varnothing \right\}\to \bigcup \left\{\varnothing \right\}=\bigcup _{x\in A}F\left(x\right)$$
20		unisn0	$$⊢\bigcup \left\{\varnothing \right\}=\varnothing$$
21	19 20	eqtr3di	$$⊢F:A\underset{onto}{⟶}\left\{\varnothing \right\}\to \bigcup _{x\in A}F\left(x\right)=\varnothing$$
22		0ss	$$⊢\varnothing \subseteq \bigcup _{y\in B}y$$
23	21 22	eqsstrdi	$$⊢F:A\underset{onto}{⟶}\left\{\varnothing \right\}\to \bigcup _{x\in A}F\left(x\right)\subseteq \bigcup _{y\in B}y$$
24	18 23	syl	$$⊢\left(F:A\underset{onto}{⟶}B\cup \left\{\varnothing \right\}\wedge B=\varnothing \right)\to \bigcup _{x\in A}F\left(x\right)\subseteq \bigcup _{y\in B}y$$
25		ssid	$$⊢F\left(x\right)\subseteq F\left(x\right)$$
26		sseq2	$$⊢y=F\left(x\right)\to \left(F\left(x\right)\subseteq y\leftrightarrow F\left(x\right)\subseteq F\left(x\right)\right)$$
27	26	rspcev	$$⊢\left(F\left(x\right)\in B\wedge F\left(x\right)\subseteq F\left(x\right)\right)\to \exists y\in BF\left(x\right)\subseteq y$$
28	25 27	mpan2	$$⊢F\left(x\right)\in B\to \exists y\in BF\left(x\right)\subseteq y$$
29	28	adantl	$$⊢\left(\left(\left(F:A\underset{onto}{⟶}B\cup \left\{\varnothing \right\}\wedge \neg B=\varnothing \right)\wedge x\in A\right)\wedge F\left(x\right)\in B\right)\to \exists y\in BF\left(x\right)\subseteq y$$
30		fof	$$⊢F:A\underset{onto}{⟶}B\cup \left\{\varnothing \right\}\to F:A⟶B\cup \left\{\varnothing \right\}$$
31	30	ffvelcdmda	$$⊢\left(F:A\underset{onto}{⟶}B\cup \left\{\varnothing \right\}\wedge x\in A\right)\to F\left(x\right)\in \left(B\cup \left\{\varnothing \right\}\right)$$
32		elunnel1	$$⊢\left(F\left(x\right)\in \left(B\cup \left\{\varnothing \right\}\right)\wedge \neg F\left(x\right)\in B\right)\to F\left(x\right)\in \left\{\varnothing \right\}$$
33	31 32	sylan	$$⊢\left(\left(F:A\underset{onto}{⟶}B\cup \left\{\varnothing \right\}\wedge x\in A\right)\wedge \neg F\left(x\right)\in B\right)\to F\left(x\right)\in \left\{\varnothing \right\}$$
34		elsni	$$⊢F\left(x\right)\in \left\{\varnothing \right\}\to F\left(x\right)=\varnothing$$
35	33 34	syl	$$⊢\left(\left(F:A\underset{onto}{⟶}B\cup \left\{\varnothing \right\}\wedge x\in A\right)\wedge \neg F\left(x\right)\in B\right)\to F\left(x\right)=\varnothing$$
36	35	adantllr	$$⊢\left(\left(\left(F:A\underset{onto}{⟶}B\cup \left\{\varnothing \right\}\wedge \neg B=\varnothing \right)\wedge x\in A\right)\wedge \neg F\left(x\right)\in B\right)\to F\left(x\right)=\varnothing$$
37		neq0	$$⊢\neg B=\varnothing \leftrightarrow \exists yy\in B$$
38	37	biimpi	$$⊢\neg B=\varnothing \to \exists yy\in B$$
39	38	adantr	$$⊢\left(\neg B=\varnothing \wedge F\left(x\right)=\varnothing \right)\to \exists yy\in B$$
40		id	$$⊢F\left(x\right)=\varnothing \to F\left(x\right)=\varnothing$$
41		0ss	$$⊢\varnothing \subseteq y$$
42	40 41	eqsstrdi	$$⊢F\left(x\right)=\varnothing \to F\left(x\right)\subseteq y$$
43	42	anim1ci	$$⊢\left(F\left(x\right)=\varnothing \wedge y\in B\right)\to \left(y\in B\wedge F\left(x\right)\subseteq y\right)$$
44	43	ex	$$⊢F\left(x\right)=\varnothing \to \left(y\in B\to \left(y\in B\wedge F\left(x\right)\subseteq y\right)\right)$$
45	44	adantl	$$⊢\left(\neg B=\varnothing \wedge F\left(x\right)=\varnothing \right)\to \left(y\in B\to \left(y\in B\wedge F\left(x\right)\subseteq y\right)\right)$$
46	45	eximdv	$$⊢\left(\neg B=\varnothing \wedge F\left(x\right)=\varnothing \right)\to \left(\exists yy\in B\to \exists y\left(y\in B\wedge F\left(x\right)\subseteq y\right)\right)$$
47	39 46	mpd	$$⊢\left(\neg B=\varnothing \wedge F\left(x\right)=\varnothing \right)\to \exists y\left(y\in B\wedge F\left(x\right)\subseteq y\right)$$
48		df-rex	$$⊢\exists y\in BF\left(x\right)\subseteq y\leftrightarrow \exists y\left(y\in B\wedge F\left(x\right)\subseteq y\right)$$
49	47 48	sylibr	$$⊢\left(\neg B=\varnothing \wedge F\left(x\right)=\varnothing \right)\to \exists y\in BF\left(x\right)\subseteq y$$
50	49	ad4ant24	$$⊢\left(\left(\left(F:A\underset{onto}{⟶}B\cup \left\{\varnothing \right\}\wedge \neg B=\varnothing \right)\wedge x\in A\right)\wedge F\left(x\right)=\varnothing \right)\to \exists y\in BF\left(x\right)\subseteq y$$
51	36 50	syldan	$$⊢\left(\left(\left(F:A\underset{onto}{⟶}B\cup \left\{\varnothing \right\}\wedge \neg B=\varnothing \right)\wedge x\in A\right)\wedge \neg F\left(x\right)\in B\right)\to \exists y\in BF\left(x\right)\subseteq y$$
52	29 51	pm2.61dan	$$⊢\left(\left(F:A\underset{onto}{⟶}B\cup \left\{\varnothing \right\}\wedge \neg B=\varnothing \right)\wedge x\in A\right)\to \exists y\in BF\left(x\right)\subseteq y$$
53	52	ralrimiva	$$⊢\left(F:A\underset{onto}{⟶}B\cup \left\{\varnothing \right\}\wedge \neg B=\varnothing \right)\to \forall x\in A\exists y\in BF\left(x\right)\subseteq y$$
54		iunss2	$$⊢\forall x\in A\exists y\in BF\left(x\right)\subseteq y\to \bigcup _{x\in A}F\left(x\right)\subseteq \bigcup _{y\in B}y$$
55	53 54	syl	$$⊢\left(F:A\underset{onto}{⟶}B\cup \left\{\varnothing \right\}\wedge \neg B=\varnothing \right)\to \bigcup _{x\in A}F\left(x\right)\subseteq \bigcup _{y\in B}y$$
56	24 55	pm2.61dan	$$⊢F:A\underset{onto}{⟶}B\cup \left\{\varnothing \right\}\to \bigcup _{x\in A}F\left(x\right)\subseteq \bigcup _{y\in B}y$$
57	10 56	eqssd	$$⊢F:A\underset{onto}{⟶}B\cup \left\{\varnothing \right\}\to \bigcup _{y\in B}y=\bigcup _{x\in A}F\left(x\right)$$
58	1 57	eqtrid	$$⊢F:A\underset{onto}{⟶}B\cup \left\{\varnothing \right\}\to \bigcup B=\bigcup _{x\in A}F\left(x\right)$$