Theorem mnutrcld

Description: Minimal universes contain the elements of their elements. (Contributed by Rohan Ridenour, 13-Aug-2023)

	Ref	Expression
Hypotheses	mnutrcld.1	|- M = { k | A. l e. k ( ~P l C_ k /\ A. m E. n e. k ( ~P l C_ n /\ A. p e. l ( E. q e. k ( p e. q /\ q e. m ) -> E. r e. m ( p e. r /\ U. r C_ n ) ) ) ) }
	mnutrcld.2	|- ( ph -> U e. M )
	mnutrcld.3	|- ( ph -> A e. U )
	mnutrcld.4	|- ( ph -> B e. A )
Assertion	mnutrcld	|- ( ph -> B e. U )

Proof

Step	Hyp	Ref	Expression
1		mnutrcld.1	|- M = { k | A. l e. k ( ~P l C_ k /\ A. m E. n e. k ( ~P l C_ n /\ A. p e. l ( E. q e. k ( p e. q /\ q e. m ) -> E. r e. m ( p e. r /\ U. r C_ n ) ) ) ) }
2		mnutrcld.2	|- ( ph -> U e. M )
3		mnutrcld.3	|- ( ph -> A e. U )
4		mnutrcld.4	|- ( ph -> B e. A )
5	1 2 3	mnuunid	|- ( ph -> U. A e. U )
6		elssuni	|- ( B e. A -> B C_ U. A )
7	4 6	syl	|- ( ph -> B C_ U. A )
8	1 2 5 7	mnussd	|- ( ph -> B e. U )