Metamath Proof Explorer

Theorem pgindnf

Description: Version of pgind with extraneous not-free requirements. (Contributed by Emmett Weisz, 27-May-2024) (New usage is discouraged.)

Ref Expression
Hypotheses pgindnf.1 
|- F/ x ph
pgindnf.2 
|- F/ y ph
pgindnf.3 
|- ( x = y -> ( ps <-> ch ) )
pgindnf.4 
|- ( y = A -> ( ch <-> th ) )
pgindnf.5 
|- ( ph -> A. x ( A. y e. ( ( 1st ` x ) u. ( 2nd ` x ) ) ch -> ps ) )
Assertion pgindnf 
|- ( ph -> ( A e. Pg -> th ) )

Proof

Step Hyp Ref Expression
1 pgindnf.1 
 |-  F/ x ph
2 pgindnf.2 
 |-  F/ y ph
3 pgindnf.3 
 |-  ( x = y -> ( ps <-> ch ) )
4 pgindnf.4 
 |-  ( y = A -> ( ch <-> th ) )
5 pgindnf.5 
 |-  ( ph -> A. x ( A. y e. ( ( 1st ` x ) u. ( 2nd ` x ) ) ch -> ps ) )
6 df-pg 
 |-  Pg = setrecs ( ( a e. _V |-> ( ~P a X. ~P a ) ) )
7 nfv 
 |-  F/ x A. y e. z ch
8 1 7 nfan 
 |-  F/ x ( ph /\ A. y e. z ch )
9 pgindlem 
 |-  ( x e. ( ~P z X. ~P z ) -> ( ( 1st ` x ) u. ( 2nd ` x ) ) C_ z )
10 9 sseld 
 |-  ( x e. ( ~P z X. ~P z ) -> ( y e. ( ( 1st ` x ) u. ( 2nd ` x ) ) -> y e. z ) )
11 10 imim1d 
 |-  ( x e. ( ~P z X. ~P z ) -> ( ( y e. z -> ch ) -> ( y e. ( ( 1st ` x ) u. ( 2nd ` x ) ) -> ch ) ) )
12 11 ralimdv2 
 |-  ( x e. ( ~P z X. ~P z ) -> ( A. y e. z ch -> A. y e. ( ( 1st ` x ) u. ( 2nd ` x ) ) ch ) )
13 5 19.21bi 
 |-  ( ph -> ( A. y e. ( ( 1st ` x ) u. ( 2nd ` x ) ) ch -> ps ) )
14 12 13 sylan9r 
 |-  ( ( ph /\ x e. ( ~P z X. ~P z ) ) -> ( A. y e. z ch -> ps ) )
15 14 impancom 
 |-  ( ( ph /\ A. y e. z ch ) -> ( x e. ( ~P z X. ~P z ) -> ps ) )
16 8 15 ralrimi 
 |-  ( ( ph /\ A. y e. z ch ) -> A. x e. ( ~P z X. ~P z ) ps )
17 vex 
 |-  z e. _V
18 pweq 
 |-  ( a = z -> ~P a = ~P z )
19 18 sqxpeqd 
 |-  ( a = z -> ( ~P a X. ~P a ) = ( ~P z X. ~P z ) )
20 eqid 
 |-  ( a e. _V |-> ( ~P a X. ~P a ) ) = ( a e. _V |-> ( ~P a X. ~P a ) )
21 vpwex 
 |-  ~P z e. _V
22 21 21 xpex 
 |-  ( ~P z X. ~P z ) e. _V
23 19 20 22 fvmpt 
 |-  ( z e. _V -> ( ( a e. _V |-> ( ~P a X. ~P a ) ) ` z ) = ( ~P z X. ~P z ) )
24 17 23 ax-mp 
 |-  ( ( a e. _V |-> ( ~P a X. ~P a ) ) ` z ) = ( ~P z X. ~P z )
25 24 eqcomi 
 |-  ( ~P z X. ~P z ) = ( ( a e. _V |-> ( ~P a X. ~P a ) ) ` z )
26 25 a1i 
 |-  ( x = y -> ( ~P z X. ~P z ) = ( ( a e. _V |-> ( ~P a X. ~P a ) ) ` z ) )
27 3 26 cbvralv2 
 |-  ( A. x e. ( ~P z X. ~P z ) ps <-> A. y e. ( ( a e. _V |-> ( ~P a X. ~P a ) ) ` z ) ch )
28 16 27 sylib 
 |-  ( ( ph /\ A. y e. z ch ) -> A. y e. ( ( a e. _V |-> ( ~P a X. ~P a ) ) ` z ) ch )
29 28 ex 
 |-  ( ph -> ( A. y e. z ch -> A. y e. ( ( a e. _V |-> ( ~P a X. ~P a ) ) ` z ) ch ) )
30 29 alrimiv 
 |-  ( ph -> A. z ( A. y e. z ch -> A. y e. ( ( a e. _V |-> ( ~P a X. ~P a ) ) ` z ) ch ) )
31 6 4 30 setis 
 |-  ( ph -> ( A e. Pg -> th ) )