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	|- ( ph -> U e. WUni )
	wunndx.2	|- ( ph -> _om e. U )
Assertion	wunndx	|- ( ph -> ndx e. U )

Proof

Step	Hyp	Ref	Expression
1		wunndx.1	|- ( ph -> U e. WUni )
2		wunndx.2	|- ( ph -> _om e. U )
3		df-ndx	|- ndx = ( _I |` NN )
4	1 2	wuncn	|- ( ph -> CC e. U )
5		nnsscn	|- NN C_ CC
6	5	a1i	|- ( ph -> NN C_ CC )
7	1 4 6	wunss	|- ( ph -> NN e. U )
8		f1oi	|- ( _I |` NN ) : NN -1-1-onto-> NN
9		f1of	|- ( ( _I |` NN ) : NN -1-1-onto-> NN -> ( _I |` NN ) : NN --> NN )
10	8 9	mp1i	|- ( ph -> ( _I |` NN ) : NN --> NN )
11	1 7 7 10	wunf	|- ( ph -> ( _I |` NN ) e. U )
12	3 11	eqeltrid	|- ( ph -> ndx e. U )