Metamath Proof Explorer


Theorem mnuss2d

Description: mnussd with arguments provided with an existential quantifier. (Contributed by Rohan Ridenour, 13-Aug-2023)

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

Proof

Step Hyp Ref Expression
1 mnuss2d.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 mnuss2d.2
 |-  ( ph -> U e. M )
3 mnuss2d.3
 |-  ( ph -> E. x e. U A C_ x )
4 2 adantr
 |-  ( ( ph /\ ( x e. U /\ A C_ x ) ) -> U e. M )
5 simprl
 |-  ( ( ph /\ ( x e. U /\ A C_ x ) ) -> x e. U )
6 simprr
 |-  ( ( ph /\ ( x e. U /\ A C_ x ) ) -> A C_ x )
7 1 4 5 6 mnussd
 |-  ( ( ph /\ ( x e. U /\ A C_ x ) ) -> A e. U )
8 3 7 rexlimddv
 |-  ( ph -> A e. U )