Theorem 1strwunOLD

Description: Obsolete version of 1strwun as of 17-Oct-2024. A constructed one-slot structure in a weak universe. (Contributed by AV, 27-Mar-2020) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	1str.g	|- G = { <. ( Base ` ndx ) , B >. }
	1strwun.u	|- ( ph -> U e. WUni )
	1strwun.o	|- ( ph -> _om e. U )
Assertion	1strwunOLD	|- ( ( 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		1strwun.o	|- ( ph -> _om e. U )
4		df-base	|- Base = Slot 1
5	2 3	wunndx	|- ( ph -> ndx e. U )
6	4 2 5	wunstr	|- ( ph -> ( Base ` ndx ) e. U )
7	1 2 6	1strwunbndx	|- ( ( ph /\ B e. U ) -> G e. U )