# Metamath Proof Explorer

## 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}\phantom{\rule{.4em}{0ex}}\left({f}:ℕ\underset{onto}{⟶}{X}\cup \left\{\varnothing \right\}\wedge \underset{{n}\in ℕ}{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 {g}\phantom{\rule{.4em}{0ex}}{g}:ℕ\underset{onto}{⟶}{X}$
5 1 2 4 syl2anc ${⊢}{\phi }\to \exists {g}\phantom{\rule{.4em}{0ex}}{g}:ℕ\underset{onto}{⟶}{X}$
6 fofn ${⊢}{g}:ℕ\underset{onto}{⟶}{X}\to {g}Fnℕ$
7 6 adantl ${⊢}\left({\phi }\wedge {g}:ℕ\underset{onto}{⟶}{X}\right)\to {g}Fnℕ$
8 nnex ${⊢}ℕ\in \mathrm{V}$
9 8 a1i ${⊢}\left({\phi }\wedge {g}:ℕ\underset{onto}{⟶}{X}\right)\to ℕ\in \mathrm{V}$
10 ltwenn ${⊢}<\mathrm{We}ℕ$
11 10 a1i ${⊢}\left({\phi }\wedge {g}:ℕ\underset{onto}{⟶}{X}\right)\to <\mathrm{We}ℕ$
12 7 9 11 wessf1orn ${⊢}\left({\phi }\wedge {g}:ℕ\underset{onto}{⟶}{X}\right)\to \exists {x}\in 𝒫ℕ\phantom{\rule{.4em}{0ex}}\left({{g}↾}_{{x}}\right):{x}\underset{1-1 onto}{⟶}\mathrm{ran}{g}$
13 elpwi ${⊢}{x}\in 𝒫ℕ\to {x}\subseteq ℕ$
14 13 3ad2ant2 ${⊢}\left(\left({\phi }\wedge {g}:ℕ\underset{onto}{⟶}{X}\right)\wedge {x}\in 𝒫ℕ\wedge \left({{g}↾}_{{x}}\right):{x}\underset{1-1 onto}{⟶}\mathrm{ran}{g}\right)\to {x}\subseteq ℕ$
15 simpr ${⊢}\left({g}:ℕ\underset{onto}{⟶}{X}\wedge \left({{g}↾}_{{x}}\right):{x}\underset{1-1 onto}{⟶}\mathrm{ran}{g}\right)\to \left({{g}↾}_{{x}}\right):{x}\underset{1-1 onto}{⟶}\mathrm{ran}{g}$
16 forn ${⊢}{g}:ℕ\underset{onto}{⟶}{X}\to \mathrm{ran}{g}={X}$
17 16 adantr ${⊢}\left({g}:ℕ\underset{onto}{⟶}{X}\wedge \left({{g}↾}_{{x}}\right):{x}\underset{1-1 onto}{⟶}\mathrm{ran}{g}\right)\to \mathrm{ran}{g}={X}$
18 17 f1oeq3d ${⊢}\left({g}:ℕ\underset{onto}{⟶}{X}\wedge \left({{g}↾}_{{x}}\right):{x}\underset{1-1 onto}{⟶}\mathrm{ran}{g}\right)\to \left(\left({{g}↾}_{{x}}\right):{x}\underset{1-1 onto}{⟶}\mathrm{ran}{g}↔\left({{g}↾}_{{x}}\right):{x}\underset{1-1 onto}{⟶}{X}\right)$
19 15 18 mpbid ${⊢}\left({g}:ℕ\underset{onto}{⟶}{X}\wedge \left({{g}↾}_{{x}}\right):{x}\underset{1-1 onto}{⟶}\mathrm{ran}{g}\right)\to \left({{g}↾}_{{x}}\right):{x}\underset{1-1 onto}{⟶}{X}$
20 19 adantll ${⊢}\left(\left({\phi }\wedge {g}:ℕ\underset{onto}{⟶}{X}\right)\wedge \left({{g}↾}_{{x}}\right):{x}\underset{1-1 onto}{⟶}\mathrm{ran}{g}\right)\to \left({{g}↾}_{{x}}\right):{x}\underset{1-1 onto}{⟶}{X}$
21 20 3adant2 ${⊢}\left(\left({\phi }\wedge {g}:ℕ\underset{onto}{⟶}{X}\right)\wedge {x}\in 𝒫ℕ\wedge \left({{g}↾}_{{x}}\right):{x}\underset{1-1 onto}{⟶}\mathrm{ran}{g}\right)\to \left({{g}↾}_{{x}}\right):{x}\underset{1-1 onto}{⟶}{X}$
22 3 adantr ${⊢}\left({\phi }\wedge {g}:ℕ\underset{onto}{⟶}{X}\right)\to \underset{{y}\in {X}}{Disj}{y}$
23 22 3ad2ant1 ${⊢}\left(\left({\phi }\wedge {g}:ℕ\underset{onto}{⟶}{X}\right)\wedge {x}\in 𝒫ℕ\wedge \left({{g}↾}_{{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↔{n}=1\right)$
25 oveq1 ${⊢}{m}={n}\to {m}-1={n}-1$
26 25 eleq1d ${⊢}{m}={n}\to \left({m}-1\in {x}↔{n}-1\in {x}\right)$
27 26 notbid ${⊢}{m}={n}\to \left(¬{m}-1\in {x}↔¬{n}-1\in {x}\right)$
28 24 27 orbi12d ${⊢}{m}={n}\to \left(\left({m}=1\vee ¬{m}-1\in {x}\right)↔\left({n}=1\vee ¬{n}-1\in {x}\right)\right)$
29 fvoveq1 ${⊢}{m}={n}\to \left({{g}↾}_{{x}}\right)\left({m}-1\right)=\left({{g}↾}_{{x}}\right)\left({n}-1\right)$
30 28 29 ifbieq2d ${⊢}{m}={n}\to if\left(\left({m}=1\vee ¬{m}-1\in {x}\right),\varnothing ,\left({{g}↾}_{{x}}\right)\left({m}-1\right)\right)=if\left(\left({n}=1\vee ¬{n}-1\in {x}\right),\varnothing ,\left({{g}↾}_{{x}}\right)\left({n}-1\right)\right)$
31 30 cbvmptv ${⊢}\left({m}\in ℕ⟼if\left(\left({m}=1\vee ¬{m}-1\in {x}\right),\varnothing ,\left({{g}↾}_{{x}}\right)\left({m}-1\right)\right)\right)=\left({n}\in ℕ⟼if\left(\left({n}=1\vee ¬{n}-1\in {x}\right),\varnothing ,\left({{g}↾}_{{x}}\right)\left({n}-1\right)\right)\right)$
32 14 21 23 31 nnfoctbdjlem ${⊢}\left(\left({\phi }\wedge {g}:ℕ\underset{onto}{⟶}{X}\right)\wedge {x}\in 𝒫ℕ\wedge \left({{g}↾}_{{x}}\right):{x}\underset{1-1 onto}{⟶}\mathrm{ran}{g}\right)\to \exists {f}\phantom{\rule{.4em}{0ex}}\left({f}:ℕ\underset{onto}{⟶}{X}\cup \left\{\varnothing \right\}\wedge \underset{{n}\in ℕ}{Disj}{f}\left({n}\right)\right)$
33 32 3exp ${⊢}\left({\phi }\wedge {g}:ℕ\underset{onto}{⟶}{X}\right)\to \left({x}\in 𝒫ℕ\to \left(\left({{g}↾}_{{x}}\right):{x}\underset{1-1 onto}{⟶}\mathrm{ran}{g}\to \exists {f}\phantom{\rule{.4em}{0ex}}\left({f}:ℕ\underset{onto}{⟶}{X}\cup \left\{\varnothing \right\}\wedge \underset{{n}\in ℕ}{Disj}{f}\left({n}\right)\right)\right)\right)$
34 33 rexlimdv ${⊢}\left({\phi }\wedge {g}:ℕ\underset{onto}{⟶}{X}\right)\to \left(\exists {x}\in 𝒫ℕ\phantom{\rule{.4em}{0ex}}\left({{g}↾}_{{x}}\right):{x}\underset{1-1 onto}{⟶}\mathrm{ran}{g}\to \exists {f}\phantom{\rule{.4em}{0ex}}\left({f}:ℕ\underset{onto}{⟶}{X}\cup \left\{\varnothing \right\}\wedge \underset{{n}\in ℕ}{Disj}{f}\left({n}\right)\right)\right)$
35 12 34 mpd ${⊢}\left({\phi }\wedge {g}:ℕ\underset{onto}{⟶}{X}\right)\to \exists {f}\phantom{\rule{.4em}{0ex}}\left({f}:ℕ\underset{onto}{⟶}{X}\cup \left\{\varnothing \right\}\wedge \underset{{n}\in ℕ}{Disj}{f}\left({n}\right)\right)$
36 35 ex ${⊢}{\phi }\to \left({g}:ℕ\underset{onto}{⟶}{X}\to \exists {f}\phantom{\rule{.4em}{0ex}}\left({f}:ℕ\underset{onto}{⟶}{X}\cup \left\{\varnothing \right\}\wedge \underset{{n}\in ℕ}{Disj}{f}\left({n}\right)\right)\right)$
37 36 exlimdv ${⊢}{\phi }\to \left(\exists {g}\phantom{\rule{.4em}{0ex}}{g}:ℕ\underset{onto}{⟶}{X}\to \exists {f}\phantom{\rule{.4em}{0ex}}\left({f}:ℕ\underset{onto}{⟶}{X}\cup \left\{\varnothing \right\}\wedge \underset{{n}\in ℕ}{Disj}{f}\left({n}\right)\right)\right)$
38 5 37 mpd ${⊢}{\phi }\to \exists {f}\phantom{\rule{.4em}{0ex}}\left({f}:ℕ\underset{onto}{⟶}{X}\cup \left\{\varnothing \right\}\wedge \underset{{n}\in ℕ}{Disj}{f}\left({n}\right)\right)$