This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( 𝜑 → 𝑈 ∈ 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 ∈ 𝑈 )