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

Metamath Proof Explorer

Theorem wunstr

Description: Closure of a structure index in a weak universe. (Contributed by Mario Carneiro, 12-Jan-2017)

Ref Expression
Hypotheses strfvss.e ⊢ E = Slot N
wunstr.u ⊢ φ → U ∈ WUni
wunstr.s ⊢ φ → S ∈ U
Assertion wunstr ⊢ φ → E ⁡ S ∈ U

Proof

Step Hyp Ref Expression
1 strfvss.e ⊢ E = Slot N
2 wunstr.u ⊢ φ → U ∈ WUni
3 wunstr.s ⊢ φ → S ∈ U
4 2 3 wunrn ⊢ φ → ran ⁡ S ∈ U
5 2 4 wununi ⊢ φ → ⋃ ran ⁡ S ∈ U
6 1 strfvss ⊢ E ⁡ S ⊆ ⋃ ran ⁡ S
7 6 a1i ⊢ φ → E ⁡ S ⊆ ⋃ ran ⁡ S
8 2 5 7 wunss ⊢ φ → E ⁡ S ∈ U