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	⊢ ( 𝜑 → 𝑋 ≼ ω )
	nnfoctbdj.n0	⊢ ( 𝜑 → 𝑋 ≠ ∅ )
	nnfoctbdj.dj	⊢ ( 𝜑 → Disj 𝑦 ∈ 𝑋 𝑦 )
Assertion	nnfoctbdj	⊢ ( 𝜑 → ∃ 𝑓 ( 𝑓 : ℕ –onto→ ( 𝑋 ∪ { ∅ } ) ∧ Disj 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ) )

Proof

Step	Hyp	Ref	Expression
1		nnfoctbdj.ctb	⊢ ( 𝜑 → 𝑋 ≼ ω )
2		nnfoctbdj.n0	⊢ ( 𝜑 → 𝑋 ≠ ∅ )
3		nnfoctbdj.dj	⊢ ( 𝜑 → Disj 𝑦 ∈ 𝑋 𝑦 )
4		nnfoctb	⊢ ( ( 𝑋 ≼ ω ∧ 𝑋 ≠ ∅ ) → ∃ 𝑔 𝑔 : ℕ –onto→ 𝑋 )
5	1 2 4	syl2anc	⊢ ( 𝜑 → ∃ 𝑔 𝑔 : ℕ –onto→ 𝑋 )
6		fofn	⊢ ( 𝑔 : ℕ –onto→ 𝑋 → 𝑔 Fn ℕ )
7	6	adantl	⊢ ( ( 𝜑 ∧ 𝑔 : ℕ –onto→ 𝑋 ) → 𝑔 Fn ℕ )
8		nnex	⊢ ℕ ∈ V
9	8	a1i	⊢ ( ( 𝜑 ∧ 𝑔 : ℕ –onto→ 𝑋 ) → ℕ ∈ V )
10		ltwenn	⊢ < We ℕ
11	10	a1i	⊢ ( ( 𝜑 ∧ 𝑔 : ℕ –onto→ 𝑋 ) → < We ℕ )
12	7 9 11	wessf1orn	⊢ ( ( 𝜑 ∧ 𝑔 : ℕ –onto→ 𝑋 ) → ∃ 𝑥 ∈ 𝒫 ℕ ( 𝑔 ↾ 𝑥 ) : 𝑥 –1-1-onto→ ran 𝑔 )
13		elpwi	⊢ ( 𝑥 ∈ 𝒫 ℕ → 𝑥 ⊆ ℕ )
14	13	3ad2ant2	⊢ ( ( ( 𝜑 ∧ 𝑔 : ℕ –onto→ 𝑋 ) ∧ 𝑥 ∈ 𝒫 ℕ ∧ ( 𝑔 ↾ 𝑥 ) : 𝑥 –1-1-onto→ ran 𝑔 ) → 𝑥 ⊆ ℕ )
15		simpr	⊢ ( ( 𝑔 : ℕ –onto→ 𝑋 ∧ ( 𝑔 ↾ 𝑥 ) : 𝑥 –1-1-onto→ ran 𝑔 ) → ( 𝑔 ↾ 𝑥 ) : 𝑥 –1-1-onto→ ran 𝑔 )
16		forn	⊢ ( 𝑔 : ℕ –onto→ 𝑋 → ran 𝑔 = 𝑋 )
17	16	adantr	⊢ ( ( 𝑔 : ℕ –onto→ 𝑋 ∧ ( 𝑔 ↾ 𝑥 ) : 𝑥 –1-1-onto→ ran 𝑔 ) → ran 𝑔 = 𝑋 )
18	17	f1oeq3d	⊢ ( ( 𝑔 : ℕ –onto→ 𝑋 ∧ ( 𝑔 ↾ 𝑥 ) : 𝑥 –1-1-onto→ ran 𝑔 ) → ( ( 𝑔 ↾ 𝑥 ) : 𝑥 –1-1-onto→ ran 𝑔 ↔ ( 𝑔 ↾ 𝑥 ) : 𝑥 –1-1-onto→ 𝑋 ) )
19	15 18	mpbid	⊢ ( ( 𝑔 : ℕ –onto→ 𝑋 ∧ ( 𝑔 ↾ 𝑥 ) : 𝑥 –1-1-onto→ ran 𝑔 ) → ( 𝑔 ↾ 𝑥 ) : 𝑥 –1-1-onto→ 𝑋 )
20	19	adantll	⊢ ( ( ( 𝜑 ∧ 𝑔 : ℕ –onto→ 𝑋 ) ∧ ( 𝑔 ↾ 𝑥 ) : 𝑥 –1-1-onto→ ran 𝑔 ) → ( 𝑔 ↾ 𝑥 ) : 𝑥 –1-1-onto→ 𝑋 )
21	20	3adant2	⊢ ( ( ( 𝜑 ∧ 𝑔 : ℕ –onto→ 𝑋 ) ∧ 𝑥 ∈ 𝒫 ℕ ∧ ( 𝑔 ↾ 𝑥 ) : 𝑥 –1-1-onto→ ran 𝑔 ) → ( 𝑔 ↾ 𝑥 ) : 𝑥 –1-1-onto→ 𝑋 )
22	3	adantr	⊢ ( ( 𝜑 ∧ 𝑔 : ℕ –onto→ 𝑋 ) → Disj 𝑦 ∈ 𝑋 𝑦 )
23	22	3ad2ant1	⊢ ( ( ( 𝜑 ∧ 𝑔 : ℕ –onto→ 𝑋 ) ∧ 𝑥 ∈ 𝒫 ℕ ∧ ( 𝑔 ↾ 𝑥 ) : 𝑥 –1-1-onto→ ran 𝑔 ) → Disj 𝑦 ∈ 𝑋 𝑦 )
24		eqeq1	⊢ ( 𝑚 = 𝑛 → ( 𝑚 = 1 ↔ 𝑛 = 1 ) )
25		oveq1	⊢ ( 𝑚 = 𝑛 → ( 𝑚 − 1 ) = ( 𝑛 − 1 ) )
26	25	eleq1d	⊢ ( 𝑚 = 𝑛 → ( ( 𝑚 − 1 ) ∈ 𝑥 ↔ ( 𝑛 − 1 ) ∈ 𝑥 ) )
27	26	notbid	⊢ ( 𝑚 = 𝑛 → ( ¬ ( 𝑚 − 1 ) ∈ 𝑥 ↔ ¬ ( 𝑛 − 1 ) ∈ 𝑥 ) )
28	24 27	orbi12d	⊢ ( 𝑚 = 𝑛 → ( ( 𝑚 = 1 ∨ ¬ ( 𝑚 − 1 ) ∈ 𝑥 ) ↔ ( 𝑛 = 1 ∨ ¬ ( 𝑛 − 1 ) ∈ 𝑥 ) ) )
29		fvoveq1	⊢ ( 𝑚 = 𝑛 → ( ( 𝑔 ↾ 𝑥 ) ‘ ( 𝑚 − 1 ) ) = ( ( 𝑔 ↾ 𝑥 ) ‘ ( 𝑛 − 1 ) ) )
30	28 29	ifbieq2d	⊢ ( 𝑚 = 𝑛 → if ( ( 𝑚 = 1 ∨ ¬ ( 𝑚 − 1 ) ∈ 𝑥 ) , ∅ , ( ( 𝑔 ↾ 𝑥 ) ‘ ( 𝑚 − 1 ) ) ) = if ( ( 𝑛 = 1 ∨ ¬ ( 𝑛 − 1 ) ∈ 𝑥 ) , ∅ , ( ( 𝑔 ↾ 𝑥 ) ‘ ( 𝑛 − 1 ) ) ) )
31	30	cbvmptv	⊢ ( 𝑚 ∈ ℕ ↦ if ( ( 𝑚 = 1 ∨ ¬ ( 𝑚 − 1 ) ∈ 𝑥 ) , ∅ , ( ( 𝑔 ↾ 𝑥 ) ‘ ( 𝑚 − 1 ) ) ) ) = ( 𝑛 ∈ ℕ ↦ if ( ( 𝑛 = 1 ∨ ¬ ( 𝑛 − 1 ) ∈ 𝑥 ) , ∅ , ( ( 𝑔 ↾ 𝑥 ) ‘ ( 𝑛 − 1 ) ) ) )
32	14 21 23 31	nnfoctbdjlem	⊢ ( ( ( 𝜑 ∧ 𝑔 : ℕ –onto→ 𝑋 ) ∧ 𝑥 ∈ 𝒫 ℕ ∧ ( 𝑔 ↾ 𝑥 ) : 𝑥 –1-1-onto→ ran 𝑔 ) → ∃ 𝑓 ( 𝑓 : ℕ –onto→ ( 𝑋 ∪ { ∅ } ) ∧ Disj 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ) )
33	32	3exp	⊢ ( ( 𝜑 ∧ 𝑔 : ℕ –onto→ 𝑋 ) → ( 𝑥 ∈ 𝒫 ℕ → ( ( 𝑔 ↾ 𝑥 ) : 𝑥 –1-1-onto→ ran 𝑔 → ∃ 𝑓 ( 𝑓 : ℕ –onto→ ( 𝑋 ∪ { ∅ } ) ∧ Disj 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ) ) ) )
34	33	rexlimdv	⊢ ( ( 𝜑 ∧ 𝑔 : ℕ –onto→ 𝑋 ) → ( ∃ 𝑥 ∈ 𝒫 ℕ ( 𝑔 ↾ 𝑥 ) : 𝑥 –1-1-onto→ ran 𝑔 → ∃ 𝑓 ( 𝑓 : ℕ –onto→ ( 𝑋 ∪ { ∅ } ) ∧ Disj 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ) ) )
35	12 34	mpd	⊢ ( ( 𝜑 ∧ 𝑔 : ℕ –onto→ 𝑋 ) → ∃ 𝑓 ( 𝑓 : ℕ –onto→ ( 𝑋 ∪ { ∅ } ) ∧ Disj 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ) )
36	35	ex	⊢ ( 𝜑 → ( 𝑔 : ℕ –onto→ 𝑋 → ∃ 𝑓 ( 𝑓 : ℕ –onto→ ( 𝑋 ∪ { ∅ } ) ∧ Disj 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ) ) )
37	36	exlimdv	⊢ ( 𝜑 → ( ∃ 𝑔 𝑔 : ℕ –onto→ 𝑋 → ∃ 𝑓 ( 𝑓 : ℕ –onto→ ( 𝑋 ∪ { ∅ } ) ∧ Disj 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ) ) )
38	5 37	mpd	⊢ ( 𝜑 → ∃ 𝑓 ( 𝑓 : ℕ –onto→ ( 𝑋 ∪ { ∅ } ) ∧ Disj 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) ) )