Theorem nnfoctbdj

Description: There exists a mapping from NN onto any (nonempty) countable set of disjoint sets, such that elements in the range of the map are disjoint. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	nnfoctbdj.ctb	$$⊢\phi \to X\preccurlyeq \mathrm{\omega }$$
	nnfoctbdj.n0	$$⊢\phi \to X\ne \varnothing$$
	nnfoctbdj.dj	$$⊢\phi \to \underset{y\in X}{Disj}y$$
Assertion	nnfoctbdj	$$⊢\phi \to \exists f\left(f:\mathbb{N}\underset{onto}{⟶}X\cup \left\{\varnothing \right\}\wedge \underset{n\in \mathbb{N}}{Disj}f\left(n\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		nnfoctbdj.ctb	$$⊢\phi \to X\preccurlyeq \mathrm{\omega }$$
2		nnfoctbdj.n0	$$⊢\phi \to X\ne \varnothing$$
3		nnfoctbdj.dj	$$⊢\phi \to \underset{y\in X}{Disj}y$$
4		nnfoctb	$$⊢\left(X\preccurlyeq \mathrm{\omega }\wedge X\ne \varnothing \right)\to \exists gg:\mathbb{N}\underset{onto}{⟶}X$$
5	1 2 4	syl2anc	$$⊢\phi \to \exists gg:\mathbb{N}\underset{onto}{⟶}X$$
6		fofn	$$⊢g:\mathbb{N}\underset{onto}{⟶}X\to gFn\mathbb{N}$$
7	6	adantl	$$⊢\left(\phi \wedge g:\mathbb{N}\underset{onto}{⟶}X\right)\to gFn\mathbb{N}$$
8		nnex	$$⊢\mathbb{N}\in \mathrm{V}$$
9	8	a1i	$$⊢\left(\phi \wedge g:\mathbb{N}\underset{onto}{⟶}X\right)\to \mathbb{N}\in \mathrm{V}$$
10		ltwenn	$$⊢<\mathrm{We}\mathbb{N}$$
11	10	a1i	$$⊢\left(\phi \wedge g:\mathbb{N}\underset{onto}{⟶}X\right)\to <\mathrm{We}\mathbb{N}$$
12	7 9 11	wessf1orn	$$⊢\left(\phi \wedge g:\mathbb{N}\underset{onto}{⟶}X\right)\to \exists x\in 𝒫\mathbb{N}\left({g\upharpoonright }_x\right):x\underset{1-1\; onto}{⟶}\mathrm{ran}g$$
13		elpwi	$$⊢x\in 𝒫\mathbb{N}\to x\subseteq \mathbb{N}$$
14	13	3ad2ant2	$$⊢\left(\left(\phi \wedge g:\mathbb{N}\underset{onto}{⟶}X\right)\wedge x\in 𝒫\mathbb{N}\wedge \left({g\upharpoonright }_x\right):x\underset{1-1\; onto}{⟶}\mathrm{ran}g\right)\to x\subseteq \mathbb{N}$$
15		simpr	$$⊢\left(g:\mathbb{N}\underset{onto}{⟶}X\wedge \left({g\upharpoonright }_x\right):x\underset{1-1\; onto}{⟶}\mathrm{ran}g\right)\to \left({g\upharpoonright }_x\right):x\underset{1-1\; onto}{⟶}\mathrm{ran}g$$
16		forn	$$⊢g:\mathbb{N}\underset{onto}{⟶}X\to \mathrm{ran}g=X$$
17	16	adantr	$$⊢\left(g:\mathbb{N}\underset{onto}{⟶}X\wedge \left({g\upharpoonright }_x\right):x\underset{1-1\; onto}{⟶}\mathrm{ran}g\right)\to \mathrm{ran}g=X$$
18	17	f1oeq3d	$$⊢\left(g:\mathbb{N}\underset{onto}{⟶}X\wedge \left({g\upharpoonright }_x\right):x\underset{1-1\; onto}{⟶}\mathrm{ran}g\right)\to \left(\left({g\upharpoonright }_x\right):x\underset{1-1\; onto}{⟶}\mathrm{ran}g\leftrightarrow \left({g\upharpoonright }_x\right):x\underset{1-1\; onto}{⟶}X\right)$$
19	15 18	mpbid	$$⊢\left(g:\mathbb{N}\underset{onto}{⟶}X\wedge \left({g\upharpoonright }_x\right):x\underset{1-1\; onto}{⟶}\mathrm{ran}g\right)\to \left({g\upharpoonright }_x\right):x\underset{1-1\; onto}{⟶}X$$
20	19	adantll	$$⊢\left(\left(\phi \wedge g:\mathbb{N}\underset{onto}{⟶}X\right)\wedge \left({g\upharpoonright }_x\right):x\underset{1-1\; onto}{⟶}\mathrm{ran}g\right)\to \left({g\upharpoonright }_x\right):x\underset{1-1\; onto}{⟶}X$$
21	20	3adant2	$$⊢\left(\left(\phi \wedge g:\mathbb{N}\underset{onto}{⟶}X\right)\wedge x\in 𝒫\mathbb{N}\wedge \left({g\upharpoonright }_x\right):x\underset{1-1\; onto}{⟶}\mathrm{ran}g\right)\to \left({g\upharpoonright }_x\right):x\underset{1-1\; onto}{⟶}X$$
22	3	adantr	$$⊢\left(\phi \wedge g:\mathbb{N}\underset{onto}{⟶}X\right)\to \underset{y\in X}{Disj}y$$
23	22	3ad2ant1	$$⊢\left(\left(\phi \wedge g:\mathbb{N}\underset{onto}{⟶}X\right)\wedge x\in 𝒫\mathbb{N}\wedge \left({g\upharpoonright }_x\right):x\underset{1-1\; onto}{⟶}\mathrm{ran}g\right)\to \underset{y\in X}{Disj}y$$
24		eqeq1	$$⊢m=n\to \left(m=1\leftrightarrow n=1\right)$$
25		oveq1	$$⊢m=n\to m-1=n-1$$
26	25	eleq1d	$$⊢m=n\to \left(m-1\in x\leftrightarrow n-1\in x\right)$$
27	26	notbid	$$⊢m=n\to \left(\neg m-1\in x\leftrightarrow \neg n-1\in x\right)$$
28	24 27	orbi12d	$$⊢m=n\to \left(\left(m=1\vee \neg m-1\in x\right)\leftrightarrow \left(n=1\vee \neg n-1\in x\right)\right)$$
29		fvoveq1	$$⊢m=n\to \left({g\upharpoonright }_x\right)\left(m-1\right)=\left({g\upharpoonright }_x\right)\left(n-1\right)$$
30	28 29	ifbieq2d	$$⊢m=n\to if\left(\left(m=1\vee \neg m-1\in x\right),\varnothing ,\left({g\upharpoonright }_x\right)\left(m-1\right)\right)=if\left(\left(n=1\vee \neg n-1\in x\right),\varnothing ,\left({g\upharpoonright }_x\right)\left(n-1\right)\right)$$
31	30	cbvmptv	$$⊢\left(m\in \mathbb{N}⟼if\left(\left(m=1\vee \neg m-1\in x\right),\varnothing ,\left({g\upharpoonright }_x\right)\left(m-1\right)\right)\right)=\left(n\in \mathbb{N}⟼if\left(\left(n=1\vee \neg n-1\in x\right),\varnothing ,\left({g\upharpoonright }_x\right)\left(n-1\right)\right)\right)$$
32	14 21 23 31	nnfoctbdjlem	$$⊢\left(\left(\phi \wedge g:\mathbb{N}\underset{onto}{⟶}X\right)\wedge x\in 𝒫\mathbb{N}\wedge \left({g\upharpoonright }_x\right):x\underset{1-1\; onto}{⟶}\mathrm{ran}g\right)\to \exists f\left(f:\mathbb{N}\underset{onto}{⟶}X\cup \left\{\varnothing \right\}\wedge \underset{n\in \mathbb{N}}{Disj}f\left(n\right)\right)$$
33	32	3exp	$$⊢\left(\phi \wedge g:\mathbb{N}\underset{onto}{⟶}X\right)\to \left(x\in 𝒫\mathbb{N}\to \left(\left({g\upharpoonright }_x\right):x\underset{1-1\; onto}{⟶}\mathrm{ran}g\to \exists f\left(f:\mathbb{N}\underset{onto}{⟶}X\cup \left\{\varnothing \right\}\wedge \underset{n\in \mathbb{N}}{Disj}f\left(n\right)\right)\right)\right)$$
34	33	rexlimdv	$$⊢\left(\phi \wedge g:\mathbb{N}\underset{onto}{⟶}X\right)\to \left(\exists x\in 𝒫\mathbb{N}\left({g\upharpoonright }_x\right):x\underset{1-1\; onto}{⟶}\mathrm{ran}g\to \exists f\left(f:\mathbb{N}\underset{onto}{⟶}X\cup \left\{\varnothing \right\}\wedge \underset{n\in \mathbb{N}}{Disj}f\left(n\right)\right)\right)$$
35	12 34	mpd	$$⊢\left(\phi \wedge g:\mathbb{N}\underset{onto}{⟶}X\right)\to \exists f\left(f:\mathbb{N}\underset{onto}{⟶}X\cup \left\{\varnothing \right\}\wedge \underset{n\in \mathbb{N}}{Disj}f\left(n\right)\right)$$
36	35	ex	$$⊢\phi \to \left(g:\mathbb{N}\underset{onto}{⟶}X\to \exists f\left(f:\mathbb{N}\underset{onto}{⟶}X\cup \left\{\varnothing \right\}\wedge \underset{n\in \mathbb{N}}{Disj}f\left(n\right)\right)\right)$$
37	36	exlimdv	$$⊢\phi \to \left(\exists gg:\mathbb{N}\underset{onto}{⟶}X\to \exists f\left(f:\mathbb{N}\underset{onto}{⟶}X\cup \left\{\varnothing \right\}\wedge \underset{n\in \mathbb{N}}{Disj}f\left(n\right)\right)\right)$$
38	5 37	mpd	$$⊢\phi \to \exists f\left(f:\mathbb{N}\underset{onto}{⟶}X\cup \left\{\varnothing \right\}\wedge \underset{n\in \mathbb{N}}{Disj}f\left(n\right)\right)$$