Theorem mnuprss2d

Description: Special case of mnuprssd . (Contributed by Rohan Ridenour, 13-Aug-2023)

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

Proof

Step	Hyp	Ref	Expression
1		mnuprss2d.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		mnuprss2d.2	|- ( ph -> U e. M )
3		mnuprss2d.3	|- ( ph -> C e. U )
4		mnuprss2d.4	|- A C_ C
5		mnuprss2d.5	|- B C_ C
6	4	a1i	|- ( ph -> A C_ C )
7	5	a1i	|- ( ph -> B C_ C )
8	1 2 3 6 7	mnuprssd	|- ( ph -> { A , B } e. U )