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	⊢ ( 𝜑 → 𝑈 ∈ WUni )
	wunndx.2	⊢ ( 𝜑 → ω ∈ 𝑈 )
Assertion	wunndx	⊢ ( 𝜑 → ndx ∈ 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		wunndx.1	⊢ ( 𝜑 → 𝑈 ∈ WUni )
2		wunndx.2	⊢ ( 𝜑 → ω ∈ 𝑈 )
3		df-ndx	⊢ ndx = ( I ↾ ℕ )
4	1 2	wuncn	⊢ ( 𝜑 → ℂ ∈ 𝑈 )
5		nnsscn	⊢ ℕ ⊆ ℂ
6	5	a1i	⊢ ( 𝜑 → ℕ ⊆ ℂ )
7	1 4 6	wunss	⊢ ( 𝜑 → ℕ ∈ 𝑈 )
8		f1oi	⊢ ( I ↾ ℕ ) : ℕ –1-1-onto→ ℕ
9		f1of	⊢ ( ( I ↾ ℕ ) : ℕ –1-1-onto→ ℕ → ( I ↾ ℕ ) : ℕ ⟶ ℕ )
10	8 9	mp1i	⊢ ( 𝜑 → ( I ↾ ℕ ) : ℕ ⟶ ℕ )
11	1 7 7 10	wunf	⊢ ( 𝜑 → ( I ↾ ℕ ) ∈ 𝑈 )
12	3 11	eqeltrid	⊢ ( 𝜑 → ndx ∈ 𝑈 )