ssnnf1octb

Description: There exists a bijection between a subset of NN and a given nonempty countable set. (Contributed by Glauco Siliprandi, 11-Oct-2020)

		Ref	Expression
	Assertion	ssnnf1octb	$⊢ (A ≼ ω \land A \neq \emptyset) \to \exists f (dom f \subseteq ℕ \land f : dom f \underset{1-1 onto}{⟶} A)$

Proof

Step	Hyp	Ref	Expression
1		nnfoctb	$⊢ (A ≼ ω \land A \neq \emptyset) \to \exists g g : ℕ \underset{onto}{⟶} A$
2		fofn	$⊢ g : ℕ \underset{onto}{⟶} A \to g Fn ℕ$
3		nnex	$⊢ ℕ \in V$
4	3	a1i	$⊢ g : ℕ \underset{onto}{⟶} A \to ℕ \in V$
5		ltwenn	$⊢ < We ℕ$
6	5	a1i	$⊢ g : ℕ \underset{onto}{⟶} A \to < We ℕ$
7	2 4 6	wessf1orn	$⊢ g : ℕ \underset{onto}{⟶} A \to \exists x \in 𝒫 ℕ ({g ↾}_{x}) : x \underset{1-1 onto}{⟶} ran g$
8		f1odm	$⊢ ({g ↾}_{x}) : x \underset{1-1 onto}{⟶} ran g \to dom ({g ↾}_{x}) = x$
9	8	adantl	$⊢ (x \in 𝒫 ℕ \land ({g ↾}_{x}) : x \underset{1-1 onto}{⟶} ran g) \to dom ({g ↾}_{x}) = x$
10		elpwi	$⊢ x \in 𝒫 ℕ \to x \subseteq ℕ$
11	10	adantr	$⊢ (x \in 𝒫 ℕ \land ({g ↾}_{x}) : x \underset{1-1 onto}{⟶} ran g) \to x \subseteq ℕ$
12	9 11	eqsstrd	$⊢ (x \in 𝒫 ℕ \land ({g ↾}_{x}) : x \underset{1-1 onto}{⟶} ran g) \to dom ({g ↾}_{x}) \subseteq ℕ$
13	12	3adant1	$⊢ (g : ℕ \underset{onto}{⟶} A \land x \in 𝒫 ℕ \land ({g ↾}_{x}) : x \underset{1-1 onto}{⟶} ran g) \to dom ({g ↾}_{x}) \subseteq ℕ$
14		simpr	$⊢ (g : ℕ \underset{onto}{⟶} A \land ({g ↾}_{x}) : x \underset{1-1 onto}{⟶} ran g) \to ({g ↾}_{x}) : x \underset{1-1 onto}{⟶} ran g$
15		eqidd	$⊢ (g : ℕ \underset{onto}{⟶} A \land ({g ↾}_{x}) : x \underset{1-1 onto}{⟶} ran g) \to {g ↾}_{x} = {g ↾}_{x}$
16	8	eqcomd	$⊢ ({g ↾}_{x}) : x \underset{1-1 onto}{⟶} ran g \to x = dom ({g ↾}_{x})$
17	16	adantl	$⊢ (g : ℕ \underset{onto}{⟶} A \land ({g ↾}_{x}) : x \underset{1-1 onto}{⟶} ran g) \to x = dom ({g ↾}_{x})$
18		forn	$⊢ g : ℕ \underset{onto}{⟶} A \to ran g = A$
19	18	adantr	$⊢ (g : ℕ \underset{onto}{⟶} A \land ({g ↾}_{x}) : x \underset{1-1 onto}{⟶} ran g) \to ran g = A$
20	15 17 19	f1oeq123d	$⊢ (g : ℕ \underset{onto}{⟶} A \land ({g ↾}_{x}) : x \underset{1-1 onto}{⟶} ran g) \to (({g ↾}_{x}) : x \underset{1-1 onto}{⟶} ran g \leftrightarrow ({g ↾}_{x}) : dom ({g ↾}_{x}) \underset{1-1 onto}{⟶} A)$
21	14 20	mpbid	$⊢ (g : ℕ \underset{onto}{⟶} A \land ({g ↾}_{x}) : x \underset{1-1 onto}{⟶} ran g) \to ({g ↾}_{x}) : dom ({g ↾}_{x}) \underset{1-1 onto}{⟶} A$
22	21	3adant2	$⊢ (g : ℕ \underset{onto}{⟶} A \land x \in 𝒫 ℕ \land ({g ↾}_{x}) : x \underset{1-1 onto}{⟶} ran g) \to ({g ↾}_{x}) : dom ({g ↾}_{x}) \underset{1-1 onto}{⟶} A$
23		vex	$⊢ g \in V$
24	23	resex	$⊢ {g ↾}_{x} \in V$
25		dmeq	$⊢ f = {g ↾}_{x} \to dom f = dom ({g ↾}_{x})$
26	25	sseq1d	$⊢ f = {g ↾}_{x} \to (dom f \subseteq ℕ \leftrightarrow dom ({g ↾}_{x}) \subseteq ℕ)$
27		id	$⊢ f = {g ↾}_{x} \to f = {g ↾}_{x}$
28		eqidd	$⊢ f = {g ↾}_{x} \to A = A$
29	27 25 28	f1oeq123d	$⊢ f = {g ↾}_{x} \to (f : dom f \underset{1-1 onto}{⟶} A \leftrightarrow ({g ↾}_{x}) : dom ({g ↾}_{x}) \underset{1-1 onto}{⟶} A)$
30	26 29	anbi12d	$⊢ f = {g ↾}_{x} \to ((dom f \subseteq ℕ \land f : dom f \underset{1-1 onto}{⟶} A) \leftrightarrow (dom ({g ↾}_{x}) \subseteq ℕ \land ({g ↾}_{x}) : dom ({g ↾}_{x}) \underset{1-1 onto}{⟶} A))$
31	24 30	spcev	$⊢ (dom ({g ↾}_{x}) \subseteq ℕ \land ({g ↾}_{x}) : dom ({g ↾}_{x}) \underset{1-1 onto}{⟶} A) \to \exists f (dom f \subseteq ℕ \land f : dom f \underset{1-1 onto}{⟶} A)$
32	13 22 31	syl2anc	$⊢ (g : ℕ \underset{onto}{⟶} A \land x \in 𝒫 ℕ \land ({g ↾}_{x}) : x \underset{1-1 onto}{⟶} ran g) \to \exists f (dom f \subseteq ℕ \land f : dom f \underset{1-1 onto}{⟶} A)$
33	32	3exp	$⊢ g : ℕ \underset{onto}{⟶} A \to (x \in 𝒫 ℕ \to (({g ↾}_{x}) : x \underset{1-1 onto}{⟶} ran g \to \exists f (dom f \subseteq ℕ \land f : dom f \underset{1-1 onto}{⟶} A)))$
34	33	rexlimdv	$⊢ g : ℕ \underset{onto}{⟶} A \to (\exists x \in 𝒫 ℕ ({g ↾}_{x}) : x \underset{1-1 onto}{⟶} ran g \to \exists f (dom f \subseteq ℕ \land f : dom f \underset{1-1 onto}{⟶} A))$
35	7 34	mpd	$⊢ g : ℕ \underset{onto}{⟶} A \to \exists f (dom f \subseteq ℕ \land f : dom f \underset{1-1 onto}{⟶} A)$
36	35	a1i	$⊢ (A ≼ ω \land A \neq \emptyset) \to (g : ℕ \underset{onto}{⟶} A \to \exists f (dom f \subseteq ℕ \land f : dom f \underset{1-1 onto}{⟶} A))$
37	36	exlimdv	$⊢ (A ≼ ω \land A \neq \emptyset) \to (\exists g g : ℕ \underset{onto}{⟶} A \to \exists f (dom f \subseteq ℕ \land f : dom f \underset{1-1 onto}{⟶} A))$
38	1 37	mpd	$⊢ (A ≼ ω \land A \neq \emptyset) \to \exists f (dom f \subseteq ℕ \land f : dom f \underset{1-1 onto}{⟶} A)$

Metamath Proof Explorer

Theorem ssnnf1octb

Proof