Description: A constructed one-slot structure in a weak universe containing the index of the base set extractor. (Contributed by AV, 27-Mar-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | 1str.g | |- G = { <. ( Base ` ndx ) , B >. } |
|
1strwun.u | |- ( ph -> U e. WUni ) |
||
1strwunbndx.b | |- ( ph -> ( Base ` ndx ) e. U ) |
||
Assertion | 1strwunbndx | |- ( ( ph /\ B e. U ) -> G e. U ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 1str.g | |- G = { <. ( Base ` ndx ) , B >. } |
|
2 | 1strwun.u | |- ( ph -> U e. WUni ) |
|
3 | 1strwunbndx.b | |- ( ph -> ( Base ` ndx ) e. U ) |
|
4 | 2 | adantr | |- ( ( ph /\ B e. U ) -> U e. WUni ) |
5 | 3 | adantr | |- ( ( ph /\ B e. U ) -> ( Base ` ndx ) e. U ) |
6 | simpr | |- ( ( ph /\ B e. U ) -> B e. U ) |
|
7 | 4 5 6 | wunop | |- ( ( ph /\ B e. U ) -> <. ( Base ` ndx ) , B >. e. U ) |
8 | 4 7 | wunsn | |- ( ( ph /\ B e. U ) -> { <. ( Base ` ndx ) , B >. } e. U ) |
9 | 1 8 | eqeltrid | |- ( ( ph /\ B e. U ) -> G e. U ) |