Metamath Proof Explorer

Theorem elpglem2

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

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

Proof

Step Hyp Ref Expression
1 fvex 
 |-  ( 1st ` A ) e. _V
2 fvex 
 |-  ( 2nd ` A ) e. _V
3 1 2 unex 
 |-  ( ( 1st ` A ) u. ( 2nd ` A ) ) e. _V
4 3 isseti 
 |-  E. x x = ( ( 1st ` A ) u. ( 2nd ` A ) )
5 sseq1 
 |-  ( x = ( ( 1st ` A ) u. ( 2nd ` A ) ) -> ( x C_ Pg <-> ( ( 1st ` A ) u. ( 2nd ` A ) ) C_ Pg ) )
6 unss 
 |-  ( ( ( 1st ` A ) C_ Pg /\ ( 2nd ` A ) C_ Pg ) <-> ( ( 1st ` A ) u. ( 2nd ` A ) ) C_ Pg )
7 5 6 bitr4di 
 |-  ( x = ( ( 1st ` A ) u. ( 2nd ` A ) ) -> ( x C_ Pg <-> ( ( 1st ` A ) C_ Pg /\ ( 2nd ` A ) C_ Pg ) ) )
8 7 biimprd 
 |-  ( x = ( ( 1st ` A ) u. ( 2nd ` A ) ) -> ( ( ( 1st ` A ) C_ Pg /\ ( 2nd ` A ) C_ Pg ) -> x C_ Pg ) )
9 ssun1 
 |-  ( 1st ` A ) C_ ( ( 1st ` A ) u. ( 2nd ` A ) )
10 id 
 |-  ( x = ( ( 1st ` A ) u. ( 2nd ` A ) ) -> x = ( ( 1st ` A ) u. ( 2nd ` A ) ) )
11 9 10 sseqtrrid 
 |-  ( x = ( ( 1st ` A ) u. ( 2nd ` A ) ) -> ( 1st ` A ) C_ x )
12 vex 
 |-  x e. _V
13 12 elpw2 
 |-  ( ( 1st ` A ) e. ~P x <-> ( 1st ` A ) C_ x )
14 11 13 sylibr 
 |-  ( x = ( ( 1st ` A ) u. ( 2nd ` A ) ) -> ( 1st ` A ) e. ~P x )
15 ssun2 
 |-  ( 2nd ` A ) C_ ( ( 1st ` A ) u. ( 2nd ` A ) )
16 15 10 sseqtrrid 
 |-  ( x = ( ( 1st ` A ) u. ( 2nd ` A ) ) -> ( 2nd ` A ) C_ x )
17 12 elpw2 
 |-  ( ( 2nd ` A ) e. ~P x <-> ( 2nd ` A ) C_ x )
18 16 17 sylibr 
 |-  ( x = ( ( 1st ` A ) u. ( 2nd ` A ) ) -> ( 2nd ` A ) e. ~P x )
19 14 18 jca 
 |-  ( x = ( ( 1st ` A ) u. ( 2nd ` A ) ) -> ( ( 1st ` A ) e. ~P x /\ ( 2nd ` A ) e. ~P x ) )
20 8 19 jctird 
 |-  ( x = ( ( 1st ` A ) u. ( 2nd ` A ) ) -> ( ( ( 1st ` A ) C_ Pg /\ ( 2nd ` A ) C_ Pg ) -> ( x C_ Pg /\ ( ( 1st ` A ) e. ~P x /\ ( 2nd ` A ) e. ~P x ) ) ) )
21 4 20 eximii 
 |-  E. x ( ( ( 1st ` A ) C_ Pg /\ ( 2nd ` A ) C_ Pg ) -> ( x C_ Pg /\ ( ( 1st ` A ) e. ~P x /\ ( 2nd ` A ) e. ~P x ) ) )
22 21 19.37iv 
 |-  ( ( ( 1st ` A ) C_ Pg /\ ( 2nd ` A ) C_ Pg ) -> E. x ( x C_ Pg /\ ( ( 1st ` A ) e. ~P x /\ ( 2nd ` A ) e. ~P x ) ) )