Description: Closure of a structure index in a weak universe. (Contributed by Mario Carneiro, 12-Jan-2017)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ndxarg.1 | ||
wunstr.2 | |||
wunstr.3 | |||
Assertion | wunstr |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ndxarg.1 | ||
2 | wunstr.2 | ||
3 | wunstr.3 | ||
4 | 2 3 | wunrn | |
5 | 2 4 | wununi | |
6 | 1 | strfvss | |
7 | 6 | a1i | |
8 | 2 5 7 | wunss |