Theorem mnuprssd

Description: A minimal universe contains pairs of subsets of an element of the universe. (Contributed by Rohan Ridenour, 13-Aug-2023)

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

Proof

Step	Hyp	Ref	Expression
1		mnuprssd.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		mnuprssd.2	|- ( ph -> U e. M )
3		mnuprssd.3	|- ( ph -> C e. U )
4		mnuprssd.4	|- ( ph -> A C_ C )
5		mnuprssd.5	|- ( ph -> B C_ C )
6	1 2 3	mnupwd	|- ( ph -> ~P C e. U )
7	3 4	sselpwd	|- ( ph -> A e. ~P C )
8	3 5	sselpwd	|- ( ph -> B e. ~P C )
9	7 8	prssd	|- ( ph -> { A , B } C_ ~P C )
10	1 2 6 9	mnussd	|- ( ph -> { A , B } e. U )