Metamath Proof Explorer


Theorem 1strwunbndx

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 )

Proof

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 )