wunndx

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

Step	Hyp	Ref	Expression
1		wunndx.1	$⊢ φ \to U \in WUni$
2		wunndx.2	$⊢ φ \to ω \in U$
3		df-ndx	$⊢ ndx = {I ↾}_{ℕ}$
4	1 2	wuncn	$⊢ φ \to ℂ \in U$
5		nnsscn	$⊢ ℕ \subseteq ℂ$
6	5	a1i	$⊢ φ \to ℕ \subseteq ℂ$
7	1 4 6	wunss	$⊢ φ \to ℕ \in U$
8		f1oi	$⊢ ({I ↾}_{ℕ}) : ℕ \underset{1-1 onto}{⟶} ℕ$
9		f1of	$⊢ ({I ↾}_{ℕ}) : ℕ \underset{1-1 onto}{⟶} ℕ \to ({I ↾}_{ℕ}) : ℕ ⟶ ℕ$
10	8 9	mp1i	$⊢ φ \to ({I ↾}_{ℕ}) : ℕ ⟶ ℕ$
11	1 7 7 10	wunf	$⊢ φ \to {I ↾}_{ℕ} \in U$
12	3 11	eqeltrid	$⊢ φ \to ndx \in U$

Metamath Proof Explorer