Metamath Proof Explorer

Theorem wfrdmcl

Description: Given F = wrecs ( R , A , X ) /\ X e. dom F , then its predecessor class is a subset of dom F . (Contributed by Scott Fenton, 21-Apr-2011)

Ref Expression
Hypothesis wfrlem6.1 
|- F = wrecs ( R , A , G )
Assertion wfrdmcl 
|- ( X e. dom F -> Pred ( R , A , X ) C_ dom F )

Proof

Step Hyp Ref Expression
1 wfrlem6.1 
 |-  F = wrecs ( R , A , G )
2 df-wrecs 
 |-  wrecs ( R , A , G ) = U. { f | E. x ( f Fn x /\ ( x C_ A /\ A. y e. x Pred ( R , A , y ) C_ x ) /\ A. y e. x ( f ` y ) = ( G ` ( f |` Pred ( R , A , y ) ) ) ) }
3 1 2 eqtri 
 |-  F = U. { f | E. x ( f Fn x /\ ( x C_ A /\ A. y e. x Pred ( R , A , y ) C_ x ) /\ A. y e. x ( f ` y ) = ( G ` ( f |` Pred ( R , A , y ) ) ) ) }
4 3 dmeqi 
 |-  dom F = dom U. { f | E. x ( f Fn x /\ ( x C_ A /\ A. y e. x Pred ( R , A , y ) C_ x ) /\ A. y e. x ( f ` y ) = ( G ` ( f |` Pred ( R , A , y ) ) ) ) }
5 dmuni 
 |-  dom U. { f | E. x ( f Fn x /\ ( x C_ A /\ A. y e. x Pred ( R , A , y ) C_ x ) /\ A. y e. x ( f ` y ) = ( G ` ( f |` Pred ( R , A , y ) ) ) ) } = U_ g e. { f | E. x ( f Fn x /\ ( x C_ A /\ A. y e. x Pred ( R , A , y ) C_ x ) /\ A. y e. x ( f ` y ) = ( G ` ( f |` Pred ( R , A , y ) ) ) ) } dom g
6 4 5 eqtri 
 |-  dom F = U_ g e. { f | E. x ( f Fn x /\ ( x C_ A /\ A. y e. x Pred ( R , A , y ) C_ x ) /\ A. y e. x ( f ` y ) = ( G ` ( f |` Pred ( R , A , y ) ) ) ) } dom g
7 6 eleq2i 
 |-  ( X e. dom F <-> X e. U_ g e. { f | E. x ( f Fn x /\ ( x C_ A /\ A. y e. x Pred ( R , A , y ) C_ x ) /\ A. y e. x ( f ` y ) = ( G ` ( f |` Pred ( R , A , y ) ) ) ) } dom g )
8 eliun 
 |-  ( X e. U_ g e. { f | E. x ( f Fn x /\ ( x C_ A /\ A. y e. x Pred ( R , A , y ) C_ x ) /\ A. y e. x ( f ` y ) = ( G ` ( f |` Pred ( R , A , y ) ) ) ) } dom g <-> E. g e. { f | E. x ( f Fn x /\ ( x C_ A /\ A. y e. x Pred ( R , A , y ) C_ x ) /\ A. y e. x ( f ` y ) = ( G ` ( f |` Pred ( R , A , y ) ) ) ) } X e. dom g )
9 7 8 bitri 
 |-  ( X e. dom F <-> E. g e. { f | E. x ( f Fn x /\ ( x C_ A /\ A. y e. x Pred ( R , A , y ) C_ x ) /\ A. y e. x ( f ` y ) = ( G ` ( f |` Pred ( R , A , y ) ) ) ) } X e. dom g )
10 eqid 
 |-  { f | E. x ( f Fn x /\ ( x C_ A /\ A. y e. x Pred ( R , A , y ) C_ x ) /\ A. y e. x ( f ` y ) = ( G ` ( f |` Pred ( R , A , y ) ) ) ) } = { f | E. x ( f Fn x /\ ( x C_ A /\ A. y e. x Pred ( R , A , y ) C_ x ) /\ A. y e. x ( f ` y ) = ( G ` ( f |` Pred ( R , A , y ) ) ) ) }
11 10 wfrlem1 
 |-  { f | E. x ( f Fn x /\ ( x C_ A /\ A. y e. x Pred ( R , A , y ) C_ x ) /\ A. y e. x ( f ` y ) = ( G ` ( f |` Pred ( R , A , y ) ) ) ) } = { g | E. z ( g Fn z /\ ( z C_ A /\ A. w e. z Pred ( R , A , w ) C_ z ) /\ A. w e. z ( g ` w ) = ( G ` ( g |` Pred ( R , A , w ) ) ) ) }
12 11 abeq2i 
 |-  ( g e. { f | E. x ( f Fn x /\ ( x C_ A /\ A. y e. x Pred ( R , A , y ) C_ x ) /\ A. y e. x ( f ` y ) = ( G ` ( f |` Pred ( R , A , y ) ) ) ) } <-> E. z ( g Fn z /\ ( z C_ A /\ A. w e. z Pred ( R , A , w ) C_ z ) /\ A. w e. z ( g ` w ) = ( G ` ( g |` Pred ( R , A , w ) ) ) ) )
13 predeq3 
 |-  ( w = X -> Pred ( R , A , w ) = Pred ( R , A , X ) )
14 13 sseq1d 
 |-  ( w = X -> ( Pred ( R , A , w ) C_ z <-> Pred ( R , A , X ) C_ z ) )
15 14 rspccv 
 |-  ( A. w e. z Pred ( R , A , w ) C_ z -> ( X e. z -> Pred ( R , A , X ) C_ z ) )
16 15 adantl 
 |-  ( ( g Fn z /\ A. w e. z Pred ( R , A , w ) C_ z ) -> ( X e. z -> Pred ( R , A , X ) C_ z ) )
17 fndm 
 |-  ( g Fn z -> dom g = z )
18 17 eleq2d 
 |-  ( g Fn z -> ( X e. dom g <-> X e. z ) )
19 17 sseq2d 
 |-  ( g Fn z -> ( Pred ( R , A , X ) C_ dom g <-> Pred ( R , A , X ) C_ z ) )
20 18 19 imbi12d 
 |-  ( g Fn z -> ( ( X e. dom g -> Pred ( R , A , X ) C_ dom g ) <-> ( X e. z -> Pred ( R , A , X ) C_ z ) ) )
21 20 adantr 
 |-  ( ( g Fn z /\ A. w e. z Pred ( R , A , w ) C_ z ) -> ( ( X e. dom g -> Pred ( R , A , X ) C_ dom g ) <-> ( X e. z -> Pred ( R , A , X ) C_ z ) ) )
22 16 21 mpbird 
 |-  ( ( g Fn z /\ A. w e. z Pred ( R , A , w ) C_ z ) -> ( X e. dom g -> Pred ( R , A , X ) C_ dom g ) )
23 22 adantrl 
 |-  ( ( g Fn z /\ ( z C_ A /\ A. w e. z Pred ( R , A , w ) C_ z ) ) -> ( X e. dom g -> Pred ( R , A , X ) C_ dom g ) )
24 23 3adant3 
 |-  ( ( g Fn z /\ ( z C_ A /\ A. w e. z Pred ( R , A , w ) C_ z ) /\ A. w e. z ( g ` w ) = ( G ` ( g |` Pred ( R , A , w ) ) ) ) -> ( X e. dom g -> Pred ( R , A , X ) C_ dom g ) )
25 24 exlimiv 
 |-  ( E. z ( g Fn z /\ ( z C_ A /\ A. w e. z Pred ( R , A , w ) C_ z ) /\ A. w e. z ( g ` w ) = ( G ` ( g |` Pred ( R , A , w ) ) ) ) -> ( X e. dom g -> Pred ( R , A , X ) C_ dom g ) )
26 12 25 sylbi 
 |-  ( g e. { f | E. x ( f Fn x /\ ( x C_ A /\ A. y e. x Pred ( R , A , y ) C_ x ) /\ A. y e. x ( f ` y ) = ( G ` ( f |` Pred ( R , A , y ) ) ) ) } -> ( X e. dom g -> Pred ( R , A , X ) C_ dom g ) )
27 26 reximia 
 |-  ( E. g e. { f | E. x ( f Fn x /\ ( x C_ A /\ A. y e. x Pred ( R , A , y ) C_ x ) /\ A. y e. x ( f ` y ) = ( G ` ( f |` Pred ( R , A , y ) ) ) ) } X e. dom g -> E. g e. { f | E. x ( f Fn x /\ ( x C_ A /\ A. y e. x Pred ( R , A , y ) C_ x ) /\ A. y e. x ( f ` y ) = ( G ` ( f |` Pred ( R , A , y ) ) ) ) } Pred ( R , A , X ) C_ dom g )
28 ssiun 
 |-  ( E. g e. { f | E. x ( f Fn x /\ ( x C_ A /\ A. y e. x Pred ( R , A , y ) C_ x ) /\ A. y e. x ( f ` y ) = ( G ` ( f |` Pred ( R , A , y ) ) ) ) } Pred ( R , A , X ) C_ dom g -> Pred ( R , A , X ) C_ U_ g e. { f | E. x ( f Fn x /\ ( x C_ A /\ A. y e. x Pred ( R , A , y ) C_ x ) /\ A. y e. x ( f ` y ) = ( G ` ( f |` Pred ( R , A , y ) ) ) ) } dom g )
29 27 28 syl 
 |-  ( E. g e. { f | E. x ( f Fn x /\ ( x C_ A /\ A. y e. x Pred ( R , A , y ) C_ x ) /\ A. y e. x ( f ` y ) = ( G ` ( f |` Pred ( R , A , y ) ) ) ) } X e. dom g -> Pred ( R , A , X ) C_ U_ g e. { f | E. x ( f Fn x /\ ( x C_ A /\ A. y e. x Pred ( R , A , y ) C_ x ) /\ A. y e. x ( f ` y ) = ( G ` ( f |` Pred ( R , A , y ) ) ) ) } dom g )
30 9 29 sylbi 
 |-  ( X e. dom F -> Pred ( R , A , X ) C_ U_ g e. { f | E. x ( f Fn x /\ ( x C_ A /\ A. y e. x Pred ( R , A , y ) C_ x ) /\ A. y e. x ( f ` y ) = ( G ` ( f |` Pred ( R , A , y ) ) ) ) } dom g )
31 30 6 sseqtrrdi 
 |-  ( X e. dom F -> Pred ( R , A , X ) C_ dom F )