Theorem mnusnd

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

	Ref	Expression
Hypotheses	mnusnd.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 ) ) ) ) }
	mnusnd.2	|- ( ph -> U e. M )
	mnusnd.3	|- ( ph -> A e. U )
Assertion	mnusnd	|- ( ph -> { A } e. U )

Proof

Step	Hyp	Ref	Expression
1		mnusnd.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		mnusnd.2	|- ( ph -> U e. M )
3		mnusnd.3	|- ( ph -> A e. U )
4	1 2 3	mnupwd	|- ( ph -> ~P A e. U )
5		snsspw	|- { A } C_ ~P A
6	5	a1i	|- ( ph -> { A } C_ ~P A )
7	1 2 4 6	mnussd	|- ( ph -> { A } e. U )