# Metamath Proof Explorer

## 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}↾}_{ℕ}$
4 1 2 wuncn ${⊢}{\phi }\to ℂ\in {U}$
5 nnsscn ${⊢}ℕ\subseteq ℂ$
6 5 a1i ${⊢}{\phi }\to ℕ\subseteq ℂ$
7 1 4 6 wunss ${⊢}{\phi }\to ℕ\in {U}$
8 f1oi ${⊢}\left({\mathrm{I}↾}_{ℕ}\right):ℕ\underset{1-1 onto}{⟶}ℕ$
9 f1of ${⊢}\left({\mathrm{I}↾}_{ℕ}\right):ℕ\underset{1-1 onto}{⟶}ℕ\to \left({\mathrm{I}↾}_{ℕ}\right):ℕ⟶ℕ$
10 8 9 mp1i ${⊢}{\phi }\to \left({\mathrm{I}↾}_{ℕ}\right):ℕ⟶ℕ$
11 1 7 7 10 wunf ${⊢}{\phi }\to {\mathrm{I}↾}_{ℕ}\in {U}$
12 3 11 eqeltrid ${⊢}{\phi }\to \mathrm{ndx}\in {U}$