Metamath Proof Explorer

Theorem elpglem1

Description: Lemma for elpg . (Contributed by Emmett Weisz, 28-Aug-2021)

Ref Expression
Assertion elpglem1 
|- ( E. x ( x C_ Pg /\ ( ( 1st ` A ) e. ~P x /\ ( 2nd ` A ) e. ~P x ) ) -> ( ( 1st ` A ) C_ Pg /\ ( 2nd ` A ) C_ Pg ) )

Proof

Step Hyp Ref Expression
1 elpwi 
 |-  ( ( 1st ` A ) e. ~P x -> ( 1st ` A ) C_ x )
2 1 adantl 
 |-  ( ( x C_ Pg /\ ( 1st ` A ) e. ~P x ) -> ( 1st ` A ) C_ x )
3 simpl 
 |-  ( ( x C_ Pg /\ ( 1st ` A ) e. ~P x ) -> x C_ Pg )
4 2 3 sstrd 
 |-  ( ( x C_ Pg /\ ( 1st ` A ) e. ~P x ) -> ( 1st ` A ) C_ Pg )
5 elpwi 
 |-  ( ( 2nd ` A ) e. ~P x -> ( 2nd ` A ) C_ x )
6 5 adantl 
 |-  ( ( x C_ Pg /\ ( 2nd ` A ) e. ~P x ) -> ( 2nd ` A ) C_ x )
7 simpl 
 |-  ( ( x C_ Pg /\ ( 2nd ` A ) e. ~P x ) -> x C_ Pg )
8 6 7 sstrd 
 |-  ( ( x C_ Pg /\ ( 2nd ` A ) e. ~P x ) -> ( 2nd ` A ) C_ Pg )
9 4 8 anim12dan 
 |-  ( ( x C_ Pg /\ ( ( 1st ` A ) e. ~P x /\ ( 2nd ` A ) e. ~P x ) ) -> ( ( 1st ` A ) C_ Pg /\ ( 2nd ` A ) C_ Pg ) )
10 9 exlimiv 
 |-  ( E. x ( x C_ Pg /\ ( ( 1st ` A ) e. ~P x /\ ( 2nd ` A ) e. ~P x ) ) -> ( ( 1st ` A ) C_ Pg /\ ( 2nd ` A ) C_ Pg ) )