Theorem wunndx

Description: Closure of the index extractor in an infinite weak universe. (Contributed by Mario Carneiro, 12-Jan-2017)

	Ref	Expression
Hypotheses	wunndx.1	$$⊢\phi \to U\in \mathrm{WUni}$$
	wunndx.2	$$⊢\phi \to \mathrm{\omega }\in U$$
Assertion	wunndx	$$⊢\phi \to \mathrm{ndx}\in U$$

Proof

Step	Hyp	Ref	Expression
1		wunndx.1	$$⊢\phi \to U\in \mathrm{WUni}$$
2		wunndx.2	$$⊢\phi \to \mathrm{\omega }\in U$$
3		df-ndx	$$⊢\mathrm{ndx}={\mathrm{I}\upharpoonright }_{\mathbb{N}}$$
4	1 2	wuncn	$$⊢\phi \to ℂ\in U$$
5		nnsscn	$$⊢\mathbb{N}\subseteq ℂ$$
6	5	a1i	$$⊢\phi \to \mathbb{N}\subseteq ℂ$$
7	1 4 6	wunss	$$⊢\phi \to \mathbb{N}\in U$$
8		f1oi	$$⊢\left({\mathrm{I}\upharpoonright }_{\mathbb{N}}\right):\mathbb{N}\underset{1-1\; onto}{⟶}\mathbb{N}$$
9		f1of	$$⊢\left({\mathrm{I}\upharpoonright }_{\mathbb{N}}\right):\mathbb{N}\underset{1-1\; onto}{⟶}\mathbb{N}\to \left({\mathrm{I}\upharpoonright }_{\mathbb{N}}\right):\mathbb{N}⟶\mathbb{N}$$
10	8 9	mp1i	$$⊢\phi \to \left({\mathrm{I}\upharpoonright }_{\mathbb{N}}\right):\mathbb{N}⟶\mathbb{N}$$
11	1 7 7 10	wunf	$$⊢\phi \to {\mathrm{I}\upharpoonright }_{\mathbb{N}}\in U$$
12	3 11	eqeltrid	$$⊢\phi \to \mathrm{ndx}\in U$$