Theorem mnussd

Description: Minimal universes are closed under subsets. (Contributed by Rohan Ridenour, 13-Aug-2023)

	Ref	Expression
Hypotheses	mnussd.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 ) ) ) ) }
	mnussd.2	|- ( ph -> U e. M )
	mnussd.3	|- ( ph -> A e. U )
	mnussd.4	|- ( ph -> B C_ A )
Assertion	mnussd	|- ( ph -> B e. U )

Proof

Step	Hyp	Ref	Expression
1		mnussd.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		mnussd.2	|- ( ph -> U e. M )
3		mnussd.3	|- ( ph -> A e. U )
4		mnussd.4	|- ( ph -> B C_ A )
5	1 2 3	mnuop123d	|- ( ph -> ( ~P A C_ U /\ A. f E. w e. U ( ~P A C_ w /\ A. i e. A ( E. v e. U ( i e. v /\ v e. f ) -> E. u e. f ( i e. u /\ U. u C_ w ) ) ) ) )
6	5	simpld	|- ( ph -> ~P A C_ U )
7	3 4	sselpwd	|- ( ph -> B e. ~P A )
8	6 7	sseldd	|- ( ph -> B e. U )