Metamath Proof Explorer

Theorem frrlem8

Description: Lemma for well-founded recursion. dom F is closed under predecessor classes. (Contributed by Scott Fenton, 6-Dec-2022)

Ref Expression
Hypotheses frrlem5.1 
|- B = { 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 ) = ( y G ( f |` Pred ( R , A , y ) ) ) ) }
frrlem5.2 
|- F = frecs ( R , A , G )
Assertion frrlem8 
|- ( z e. dom F -> Pred ( R , A , z ) C_ dom F )

Proof

Step Hyp Ref Expression
1 frrlem5.1 
 |-  B = { 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 ) = ( y G ( f |` Pred ( R , A , y ) ) ) ) }
2 frrlem5.2 
 |-  F = frecs ( R , A , G )
3 vex 
 |-  z e. _V
4 3 eldm2 
 |-  ( z e. dom F <-> E. w <. z , w >. e. F )
5 1 2 frrlem5 
 |-  F = U. B
6 1 frrlem1 
 |-  B = { g | E. a ( g Fn a /\ ( a C_ A /\ A. z e. a Pred ( R , A , z ) C_ a ) /\ A. z e. a ( g ` z ) = ( z G ( g |` Pred ( R , A , z ) ) ) ) }
7 6 unieqi 
 |-  U. B = U. { g | E. a ( g Fn a /\ ( a C_ A /\ A. z e. a Pred ( R , A , z ) C_ a ) /\ A. z e. a ( g ` z ) = ( z G ( g |` Pred ( R , A , z ) ) ) ) }
8 5 7 eqtri 
 |-  F = U. { g | E. a ( g Fn a /\ ( a C_ A /\ A. z e. a Pred ( R , A , z ) C_ a ) /\ A. z e. a ( g ` z ) = ( z G ( g |` Pred ( R , A , z ) ) ) ) }
9 8 eleq2i 
 |-  ( <. z , w >. e. F <-> <. z , w >. e. U. { g | E. a ( g Fn a /\ ( a C_ A /\ A. z e. a Pred ( R , A , z ) C_ a ) /\ A. z e. a ( g ` z ) = ( z G ( g |` Pred ( R , A , z ) ) ) ) } )
10 eluniab 
 |-  ( <. z , w >. e. U. { g | E. a ( g Fn a /\ ( a C_ A /\ A. z e. a Pred ( R , A , z ) C_ a ) /\ A. z e. a ( g ` z ) = ( z G ( g |` Pred ( R , A , z ) ) ) ) } <-> E. g ( <. z , w >. e. g /\ E. a ( g Fn a /\ ( a C_ A /\ A. z e. a Pred ( R , A , z ) C_ a ) /\ A. z e. a ( g ` z ) = ( z G ( g |` Pred ( R , A , z ) ) ) ) ) )
11 9 10 bitri 
 |-  ( <. z , w >. e. F <-> E. g ( <. z , w >. e. g /\ E. a ( g Fn a /\ ( a C_ A /\ A. z e. a Pred ( R , A , z ) C_ a ) /\ A. z e. a ( g ` z ) = ( z G ( g |` Pred ( R , A , z ) ) ) ) ) )
12 simpr2r 
 |-  ( ( <. z , w >. e. g /\ ( g Fn a /\ ( a C_ A /\ A. z e. a Pred ( R , A , z ) C_ a ) /\ A. z e. a ( g ` z ) = ( z G ( g |` Pred ( R , A , z ) ) ) ) ) -> A. z e. a Pred ( R , A , z ) C_ a )
13 vex 
 |-  w e. _V
14 3 13 opeldm 
 |-  ( <. z , w >. e. g -> z e. dom g )
15 14 adantr 
 |-  ( ( <. z , w >. e. g /\ ( g Fn a /\ ( a C_ A /\ A. z e. a Pred ( R , A , z ) C_ a ) /\ A. z e. a ( g ` z ) = ( z G ( g |` Pred ( R , A , z ) ) ) ) ) -> z e. dom g )
16 simpr1 
 |-  ( ( <. z , w >. e. g /\ ( g Fn a /\ ( a C_ A /\ A. z e. a Pred ( R , A , z ) C_ a ) /\ A. z e. a ( g ` z ) = ( z G ( g |` Pred ( R , A , z ) ) ) ) ) -> g Fn a )
17 16 fndmd 
 |-  ( ( <. z , w >. e. g /\ ( g Fn a /\ ( a C_ A /\ A. z e. a Pred ( R , A , z ) C_ a ) /\ A. z e. a ( g ` z ) = ( z G ( g |` Pred ( R , A , z ) ) ) ) ) -> dom g = a )
18 15 17 eleqtrd 
 |-  ( ( <. z , w >. e. g /\ ( g Fn a /\ ( a C_ A /\ A. z e. a Pred ( R , A , z ) C_ a ) /\ A. z e. a ( g ` z ) = ( z G ( g |` Pred ( R , A , z ) ) ) ) ) -> z e. a )
19 rsp 
 |-  ( A. z e. a Pred ( R , A , z ) C_ a -> ( z e. a -> Pred ( R , A , z ) C_ a ) )
20 12 18 19 sylc 
 |-  ( ( <. z , w >. e. g /\ ( g Fn a /\ ( a C_ A /\ A. z e. a Pred ( R , A , z ) C_ a ) /\ A. z e. a ( g ` z ) = ( z G ( g |` Pred ( R , A , z ) ) ) ) ) -> Pred ( R , A , z ) C_ a )
21 20 17 sseqtrrd 
 |-  ( ( <. z , w >. e. g /\ ( g Fn a /\ ( a C_ A /\ A. z e. a Pred ( R , A , z ) C_ a ) /\ A. z e. a ( g ` z ) = ( z G ( g |` Pred ( R , A , z ) ) ) ) ) -> Pred ( R , A , z ) C_ dom g )
22 19.8a 
 |-  ( ( g Fn a /\ ( a C_ A /\ A. z e. a Pred ( R , A , z ) C_ a ) /\ A. z e. a ( g ` z ) = ( z G ( g |` Pred ( R , A , z ) ) ) ) -> E. a ( g Fn a /\ ( a C_ A /\ A. z e. a Pred ( R , A , z ) C_ a ) /\ A. z e. a ( g ` z ) = ( z G ( g |` Pred ( R , A , z ) ) ) ) )
23 6 abeq2i 
 |-  ( g e. B <-> E. a ( g Fn a /\ ( a C_ A /\ A. z e. a Pred ( R , A , z ) C_ a ) /\ A. z e. a ( g ` z ) = ( z G ( g |` Pred ( R , A , z ) ) ) ) )
24 22 23 sylibr 
 |-  ( ( g Fn a /\ ( a C_ A /\ A. z e. a Pred ( R , A , z ) C_ a ) /\ A. z e. a ( g ` z ) = ( z G ( g |` Pred ( R , A , z ) ) ) ) -> g e. B )
25 24 adantl 
 |-  ( ( <. z , w >. e. g /\ ( g Fn a /\ ( a C_ A /\ A. z e. a Pred ( R , A , z ) C_ a ) /\ A. z e. a ( g ` z ) = ( z G ( g |` Pred ( R , A , z ) ) ) ) ) -> g e. B )
26 elssuni 
 |-  ( g e. B -> g C_ U. B )
27 25 26 syl 
 |-  ( ( <. z , w >. e. g /\ ( g Fn a /\ ( a C_ A /\ A. z e. a Pred ( R , A , z ) C_ a ) /\ A. z e. a ( g ` z ) = ( z G ( g |` Pred ( R , A , z ) ) ) ) ) -> g C_ U. B )
28 27 5 sseqtrrdi 
 |-  ( ( <. z , w >. e. g /\ ( g Fn a /\ ( a C_ A /\ A. z e. a Pred ( R , A , z ) C_ a ) /\ A. z e. a ( g ` z ) = ( z G ( g |` Pred ( R , A , z ) ) ) ) ) -> g C_ F )
29 dmss 
 |-  ( g C_ F -> dom g C_ dom F )
30 28 29 syl 
 |-  ( ( <. z , w >. e. g /\ ( g Fn a /\ ( a C_ A /\ A. z e. a Pred ( R , A , z ) C_ a ) /\ A. z e. a ( g ` z ) = ( z G ( g |` Pred ( R , A , z ) ) ) ) ) -> dom g C_ dom F )
31 21 30 sstrd 
 |-  ( ( <. z , w >. e. g /\ ( g Fn a /\ ( a C_ A /\ A. z e. a Pred ( R , A , z ) C_ a ) /\ A. z e. a ( g ` z ) = ( z G ( g |` Pred ( R , A , z ) ) ) ) ) -> Pred ( R , A , z ) C_ dom F )
32 31 expcom 
 |-  ( ( g Fn a /\ ( a C_ A /\ A. z e. a Pred ( R , A , z ) C_ a ) /\ A. z e. a ( g ` z ) = ( z G ( g |` Pred ( R , A , z ) ) ) ) -> ( <. z , w >. e. g -> Pred ( R , A , z ) C_ dom F ) )
33 32 exlimiv 
 |-  ( E. a ( g Fn a /\ ( a C_ A /\ A. z e. a Pred ( R , A , z ) C_ a ) /\ A. z e. a ( g ` z ) = ( z G ( g |` Pred ( R , A , z ) ) ) ) -> ( <. z , w >. e. g -> Pred ( R , A , z ) C_ dom F ) )
34 33 impcom 
 |-  ( ( <. z , w >. e. g /\ E. a ( g Fn a /\ ( a C_ A /\ A. z e. a Pred ( R , A , z ) C_ a ) /\ A. z e. a ( g ` z ) = ( z G ( g |` Pred ( R , A , z ) ) ) ) ) -> Pred ( R , A , z ) C_ dom F )
35 34 exlimiv 
 |-  ( E. g ( <. z , w >. e. g /\ E. a ( g Fn a /\ ( a C_ A /\ A. z e. a Pred ( R , A , z ) C_ a ) /\ A. z e. a ( g ` z ) = ( z G ( g |` Pred ( R , A , z ) ) ) ) ) -> Pred ( R , A , z ) C_ dom F )
36 11 35 sylbi 
 |-  ( <. z , w >. e. F -> Pred ( R , A , z ) C_ dom F )
37 36 exlimiv 
 |-  ( E. w <. z , w >. e. F -> Pred ( R , A , z ) C_ dom F )
38 4 37 sylbi 
 |-  ( z e. dom F -> Pred ( R , A , z ) C_ dom F )