Metamath Proof Explorer

Theorem setrec1

Description: This is the first of two fundamental theorems about set recursion from which all other facts will be derived. It states that the class setrecs ( F ) is closed under F . This effectively sets the actual value of setrecs ( F ) as a lower bound for setrecs ( F ) , as it implies that any set generated by successive applications of F is a member of B . This theorem "gets off the ground" because we can start by letting A = (/) , and the hypotheses of the theorem will hold trivially.

Variable B represents an abbreviation of setrecs ( F ) or another name of setrecs ( F ) (for an example of the latter, see theorem setrecon).

Proof summary: Assume that A C_ B , meaning that all elements of A are in some set recursively generated by F . Then by setrec1lem3 , A is a subset of some set recursively generated by F . (It turns out that A itself is recursively generated by F , but we don't need this fact. See the comment to setrec1lem3 .) Therefore, by setrec1lem4 , ( FA ) is a subset of some set recursively generated by F . Thus, by ssuni , it is a subset of the union of all sets recursively generated by F .

See df-setrecs for a detailed description of how the setrecs definition works.

(Contributed by Emmett Weisz, 9-Oct-2020)

Ref Expression
Hypotheses setrec1.b 
|- B = setrecs ( F )
setrec1.v 
|- ( ph -> A e. _V )
setrec1.a 
|- ( ph -> A C_ B )
Assertion setrec1 
|- ( ph -> ( F ` A ) C_ B )

Proof

Step Hyp Ref Expression
1 setrec1.b 
 |-  B = setrecs ( F )
2 setrec1.v 
 |-  ( ph -> A e. _V )
3 setrec1.a 
 |-  ( ph -> A C_ B )
4 eqid 
 |-  { y | A. z ( A. w ( w C_ y -> ( w C_ z -> ( F ` w ) C_ z ) ) -> y C_ z ) } = { y | A. z ( A. w ( w C_ y -> ( w C_ z -> ( F ` w ) C_ z ) ) -> y C_ z ) }
5 3 sseld 
 |-  ( ph -> ( a e. A -> a e. B ) )
6 5 imp 
 |-  ( ( ph /\ a e. A ) -> a e. B )
7 df-setrecs 
 |-  setrecs ( F ) = U. { y | A. z ( A. w ( w C_ y -> ( w C_ z -> ( F ` w ) C_ z ) ) -> y C_ z ) }
8 1 7 eqtri 
 |-  B = U. { y | A. z ( A. w ( w C_ y -> ( w C_ z -> ( F ` w ) C_ z ) ) -> y C_ z ) }
9 6 8 eleqtrdi 
 |-  ( ( ph /\ a e. A ) -> a e. U. { y | A. z ( A. w ( w C_ y -> ( w C_ z -> ( F ` w ) C_ z ) ) -> y C_ z ) } )
10 eluni 
 |-  ( a e. U. { y | A. z ( A. w ( w C_ y -> ( w C_ z -> ( F ` w ) C_ z ) ) -> y C_ z ) } <-> E. x ( a e. x /\ x e. { y | A. z ( A. w ( w C_ y -> ( w C_ z -> ( F ` w ) C_ z ) ) -> y C_ z ) } ) )
11 9 10 sylib 
 |-  ( ( ph /\ a e. A ) -> E. x ( a e. x /\ x e. { y | A. z ( A. w ( w C_ y -> ( w C_ z -> ( F ` w ) C_ z ) ) -> y C_ z ) } ) )
12 11 ralrimiva 
 |-  ( ph -> A. a e. A E. x ( a e. x /\ x e. { y | A. z ( A. w ( w C_ y -> ( w C_ z -> ( F ` w ) C_ z ) ) -> y C_ z ) } ) )
13 4 2 12 setrec1lem3 
 |-  ( ph -> E. x ( A C_ x /\ x e. { y | A. z ( A. w ( w C_ y -> ( w C_ z -> ( F ` w ) C_ z ) ) -> y C_ z ) } ) )
14 nfv 
 |-  F/ z ph
15 nfv 
 |-  F/ z A C_ x
16 nfaba1 
 |-  F/_ z { y | A. z ( A. w ( w C_ y -> ( w C_ z -> ( F ` w ) C_ z ) ) -> y C_ z ) }
17 16 nfel2 
 |-  F/ z x e. { y | A. z ( A. w ( w C_ y -> ( w C_ z -> ( F ` w ) C_ z ) ) -> y C_ z ) }
18 15 17 nfan 
 |-  F/ z ( A C_ x /\ x e. { y | A. z ( A. w ( w C_ y -> ( w C_ z -> ( F ` w ) C_ z ) ) -> y C_ z ) } )
19 14 18 nfan 
 |-  F/ z ( ph /\ ( A C_ x /\ x e. { y | A. z ( A. w ( w C_ y -> ( w C_ z -> ( F ` w ) C_ z ) ) -> y C_ z ) } ) )
20 2 adantr 
 |-  ( ( ph /\ ( A C_ x /\ x e. { y | A. z ( A. w ( w C_ y -> ( w C_ z -> ( F ` w ) C_ z ) ) -> y C_ z ) } ) ) -> A e. _V )
21 simprl 
 |-  ( ( ph /\ ( A C_ x /\ x e. { y | A. z ( A. w ( w C_ y -> ( w C_ z -> ( F ` w ) C_ z ) ) -> y C_ z ) } ) ) -> A C_ x )
22 simprr 
 |-  ( ( ph /\ ( A C_ x /\ x e. { y | A. z ( A. w ( w C_ y -> ( w C_ z -> ( F ` w ) C_ z ) ) -> y C_ z ) } ) ) -> x e. { y | A. z ( A. w ( w C_ y -> ( w C_ z -> ( F ` w ) C_ z ) ) -> y C_ z ) } )
23 19 4 20 21 22 setrec1lem4 
 |-  ( ( ph /\ ( A C_ x /\ x e. { y | A. z ( A. w ( w C_ y -> ( w C_ z -> ( F ` w ) C_ z ) ) -> y C_ z ) } ) ) -> ( x u. ( F ` A ) ) e. { y | A. z ( A. w ( w C_ y -> ( w C_ z -> ( F ` w ) C_ z ) ) -> y C_ z ) } )
24 ssun2 
 |-  ( F ` A ) C_ ( x u. ( F ` A ) )
25 23 24 jctil 
 |-  ( ( ph /\ ( A C_ x /\ x e. { y | A. z ( A. w ( w C_ y -> ( w C_ z -> ( F ` w ) C_ z ) ) -> y C_ z ) } ) ) -> ( ( F ` A ) C_ ( x u. ( F ` A ) ) /\ ( x u. ( F ` A ) ) e. { y | A. z ( A. w ( w C_ y -> ( w C_ z -> ( F ` w ) C_ z ) ) -> y C_ z ) } ) )
26 ssuni 
 |-  ( ( ( F ` A ) C_ ( x u. ( F ` A ) ) /\ ( x u. ( F ` A ) ) e. { y | A. z ( A. w ( w C_ y -> ( w C_ z -> ( F ` w ) C_ z ) ) -> y C_ z ) } ) -> ( F ` A ) C_ U. { y | A. z ( A. w ( w C_ y -> ( w C_ z -> ( F ` w ) C_ z ) ) -> y C_ z ) } )
27 25 26 syl 
 |-  ( ( ph /\ ( A C_ x /\ x e. { y | A. z ( A. w ( w C_ y -> ( w C_ z -> ( F ` w ) C_ z ) ) -> y C_ z ) } ) ) -> ( F ` A ) C_ U. { y | A. z ( A. w ( w C_ y -> ( w C_ z -> ( F ` w ) C_ z ) ) -> y C_ z ) } )
28 13 27 exlimddv 
 |-  ( ph -> ( F ` A ) C_ U. { y | A. z ( A. w ( w C_ y -> ( w C_ z -> ( F ` w ) C_ z ) ) -> y C_ z ) } )
29 28 8 sseqtrrdi 
 |-  ( ph -> ( F ` A ) C_ B )