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 )