Metamath Proof Explorer

Theorem elpglem3

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

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

Proof

Step Hyp Ref Expression
1 vex 
 |-  x e. _V
2 pweq 
 |-  ( y = x -> ~P y = ~P x )
3 2 sqxpeqd 
 |-  ( y = x -> ( ~P y X. ~P y ) = ( ~P x X. ~P x ) )
4 eqid 
 |-  ( y e. _V |-> ( ~P y X. ~P y ) ) = ( y e. _V |-> ( ~P y X. ~P y ) )
5 1 pwex 
 |-  ~P x e. _V
6 5 5 xpex 
 |-  ( ~P x X. ~P x ) e. _V
7 3 4 6 fvmpt 
 |-  ( x e. _V -> ( ( y e. _V |-> ( ~P y X. ~P y ) ) ` x ) = ( ~P x X. ~P x ) )
8 1 7 ax-mp 
 |-  ( ( y e. _V |-> ( ~P y X. ~P y ) ) ` x ) = ( ~P x X. ~P x )
9 8 eleq2i 
 |-  ( A e. ( ( y e. _V |-> ( ~P y X. ~P y ) ) ` x ) <-> A e. ( ~P x X. ~P x ) )
10 elxp7 
 |-  ( A e. ( ~P x X. ~P x ) <-> ( A e. ( _V X. _V ) /\ ( ( 1st ` A ) e. ~P x /\ ( 2nd ` A ) e. ~P x ) ) )
11 9 10 bitri 
 |-  ( A e. ( ( y e. _V |-> ( ~P y X. ~P y ) ) ` x ) <-> ( A e. ( _V X. _V ) /\ ( ( 1st ` A ) e. ~P x /\ ( 2nd ` A ) e. ~P x ) ) )
12 11 anbi2i 
 |-  ( ( x C_ Pg /\ A e. ( ( y e. _V |-> ( ~P y X. ~P y ) ) ` x ) ) <-> ( x C_ Pg /\ ( A e. ( _V X. _V ) /\ ( ( 1st ` A ) e. ~P x /\ ( 2nd ` A ) e. ~P x ) ) ) )
13 an12 
 |-  ( ( x C_ Pg /\ ( A e. ( _V X. _V ) /\ ( ( 1st ` A ) e. ~P x /\ ( 2nd ` A ) e. ~P x ) ) ) <-> ( A e. ( _V X. _V ) /\ ( x C_ Pg /\ ( ( 1st ` A ) e. ~P x /\ ( 2nd ` A ) e. ~P x ) ) ) )
14 12 13 bitri 
 |-  ( ( x C_ Pg /\ A e. ( ( y e. _V |-> ( ~P y X. ~P y ) ) ` x ) ) <-> ( A e. ( _V X. _V ) /\ ( x C_ Pg /\ ( ( 1st ` A ) e. ~P x /\ ( 2nd ` A ) e. ~P x ) ) ) )
15 14 exbii 
 |-  ( E. x ( x C_ Pg /\ A e. ( ( y e. _V |-> ( ~P y X. ~P y ) ) ` x ) ) <-> E. x ( A e. ( _V X. _V ) /\ ( x C_ Pg /\ ( ( 1st ` A ) e. ~P x /\ ( 2nd ` A ) e. ~P x ) ) ) )
16 19.42v 
 |-  ( E. x ( A e. ( _V X. _V ) /\ ( x C_ Pg /\ ( ( 1st ` A ) e. ~P x /\ ( 2nd ` A ) e. ~P x ) ) ) <-> ( A e. ( _V X. _V ) /\ E. x ( x C_ Pg /\ ( ( 1st ` A ) e. ~P x /\ ( 2nd ` A ) e. ~P x ) ) ) )
17 15 16 bitri 
 |-  ( E. x ( x C_ Pg /\ A e. ( ( y e. _V |-> ( ~P y X. ~P y ) ) ` x ) ) <-> ( A e. ( _V X. _V ) /\ E. x ( x C_ Pg /\ ( ( 1st ` A ) e. ~P x /\ ( 2nd ` A ) e. ~P x ) ) ) )