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 𝐵 = setrecs ( 𝐹 )
setrec1.v ( 𝜑𝐴 ∈ V )
setrec1.a ( 𝜑𝐴𝐵 )
Assertion setrec1 ( 𝜑 → ( 𝐹𝐴 ) ⊆ 𝐵 )

Proof

Step Hyp Ref Expression
1 setrec1.b 𝐵 = setrecs ( 𝐹 )
2 setrec1.v ( 𝜑𝐴 ∈ V )
3 setrec1.a ( 𝜑𝐴𝐵 )
4 eqid { 𝑦 ∣ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤𝑦 → ( 𝑤𝑧 → ( 𝐹𝑤 ) ⊆ 𝑧 ) ) → 𝑦𝑧 ) } = { 𝑦 ∣ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤𝑦 → ( 𝑤𝑧 → ( 𝐹𝑤 ) ⊆ 𝑧 ) ) → 𝑦𝑧 ) }
5 3 sseld ( 𝜑 → ( 𝑎𝐴𝑎𝐵 ) )
6 5 imp ( ( 𝜑𝑎𝐴 ) → 𝑎𝐵 )
7 df-setrecs setrecs ( 𝐹 ) = { 𝑦 ∣ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤𝑦 → ( 𝑤𝑧 → ( 𝐹𝑤 ) ⊆ 𝑧 ) ) → 𝑦𝑧 ) }
8 1 7 eqtri 𝐵 = { 𝑦 ∣ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤𝑦 → ( 𝑤𝑧 → ( 𝐹𝑤 ) ⊆ 𝑧 ) ) → 𝑦𝑧 ) }
9 6 8 eleqtrdi ( ( 𝜑𝑎𝐴 ) → 𝑎 { 𝑦 ∣ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤𝑦 → ( 𝑤𝑧 → ( 𝐹𝑤 ) ⊆ 𝑧 ) ) → 𝑦𝑧 ) } )
10 eluni ( 𝑎 { 𝑦 ∣ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤𝑦 → ( 𝑤𝑧 → ( 𝐹𝑤 ) ⊆ 𝑧 ) ) → 𝑦𝑧 ) } ↔ ∃ 𝑥 ( 𝑎𝑥𝑥 ∈ { 𝑦 ∣ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤𝑦 → ( 𝑤𝑧 → ( 𝐹𝑤 ) ⊆ 𝑧 ) ) → 𝑦𝑧 ) } ) )
11 9 10 sylib ( ( 𝜑𝑎𝐴 ) → ∃ 𝑥 ( 𝑎𝑥𝑥 ∈ { 𝑦 ∣ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤𝑦 → ( 𝑤𝑧 → ( 𝐹𝑤 ) ⊆ 𝑧 ) ) → 𝑦𝑧 ) } ) )
12 11 ralrimiva ( 𝜑 → ∀ 𝑎𝐴𝑥 ( 𝑎𝑥𝑥 ∈ { 𝑦 ∣ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤𝑦 → ( 𝑤𝑧 → ( 𝐹𝑤 ) ⊆ 𝑧 ) ) → 𝑦𝑧 ) } ) )
13 4 2 12 setrec1lem3 ( 𝜑 → ∃ 𝑥 ( 𝐴𝑥𝑥 ∈ { 𝑦 ∣ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤𝑦 → ( 𝑤𝑧 → ( 𝐹𝑤 ) ⊆ 𝑧 ) ) → 𝑦𝑧 ) } ) )
14 nfv 𝑧 𝜑
15 nfv 𝑧 𝐴𝑥
16 nfaba1 𝑧 { 𝑦 ∣ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤𝑦 → ( 𝑤𝑧 → ( 𝐹𝑤 ) ⊆ 𝑧 ) ) → 𝑦𝑧 ) }
17 16 nfel2 𝑧 𝑥 ∈ { 𝑦 ∣ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤𝑦 → ( 𝑤𝑧 → ( 𝐹𝑤 ) ⊆ 𝑧 ) ) → 𝑦𝑧 ) }
18 15 17 nfan 𝑧 ( 𝐴𝑥𝑥 ∈ { 𝑦 ∣ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤𝑦 → ( 𝑤𝑧 → ( 𝐹𝑤 ) ⊆ 𝑧 ) ) → 𝑦𝑧 ) } )
19 14 18 nfan 𝑧 ( 𝜑 ∧ ( 𝐴𝑥𝑥 ∈ { 𝑦 ∣ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤𝑦 → ( 𝑤𝑧 → ( 𝐹𝑤 ) ⊆ 𝑧 ) ) → 𝑦𝑧 ) } ) )
20 2 adantr ( ( 𝜑 ∧ ( 𝐴𝑥𝑥 ∈ { 𝑦 ∣ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤𝑦 → ( 𝑤𝑧 → ( 𝐹𝑤 ) ⊆ 𝑧 ) ) → 𝑦𝑧 ) } ) ) → 𝐴 ∈ V )
21 simprl ( ( 𝜑 ∧ ( 𝐴𝑥𝑥 ∈ { 𝑦 ∣ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤𝑦 → ( 𝑤𝑧 → ( 𝐹𝑤 ) ⊆ 𝑧 ) ) → 𝑦𝑧 ) } ) ) → 𝐴𝑥 )
22 simprr ( ( 𝜑 ∧ ( 𝐴𝑥𝑥 ∈ { 𝑦 ∣ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤𝑦 → ( 𝑤𝑧 → ( 𝐹𝑤 ) ⊆ 𝑧 ) ) → 𝑦𝑧 ) } ) ) → 𝑥 ∈ { 𝑦 ∣ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤𝑦 → ( 𝑤𝑧 → ( 𝐹𝑤 ) ⊆ 𝑧 ) ) → 𝑦𝑧 ) } )
23 19 4 20 21 22 setrec1lem4 ( ( 𝜑 ∧ ( 𝐴𝑥𝑥 ∈ { 𝑦 ∣ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤𝑦 → ( 𝑤𝑧 → ( 𝐹𝑤 ) ⊆ 𝑧 ) ) → 𝑦𝑧 ) } ) ) → ( 𝑥 ∪ ( 𝐹𝐴 ) ) ∈ { 𝑦 ∣ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤𝑦 → ( 𝑤𝑧 → ( 𝐹𝑤 ) ⊆ 𝑧 ) ) → 𝑦𝑧 ) } )
24 ssun2 ( 𝐹𝐴 ) ⊆ ( 𝑥 ∪ ( 𝐹𝐴 ) )
25 23 24 jctil ( ( 𝜑 ∧ ( 𝐴𝑥𝑥 ∈ { 𝑦 ∣ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤𝑦 → ( 𝑤𝑧 → ( 𝐹𝑤 ) ⊆ 𝑧 ) ) → 𝑦𝑧 ) } ) ) → ( ( 𝐹𝐴 ) ⊆ ( 𝑥 ∪ ( 𝐹𝐴 ) ) ∧ ( 𝑥 ∪ ( 𝐹𝐴 ) ) ∈ { 𝑦 ∣ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤𝑦 → ( 𝑤𝑧 → ( 𝐹𝑤 ) ⊆ 𝑧 ) ) → 𝑦𝑧 ) } ) )
26 ssuni ( ( ( 𝐹𝐴 ) ⊆ ( 𝑥 ∪ ( 𝐹𝐴 ) ) ∧ ( 𝑥 ∪ ( 𝐹𝐴 ) ) ∈ { 𝑦 ∣ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤𝑦 → ( 𝑤𝑧 → ( 𝐹𝑤 ) ⊆ 𝑧 ) ) → 𝑦𝑧 ) } ) → ( 𝐹𝐴 ) ⊆ { 𝑦 ∣ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤𝑦 → ( 𝑤𝑧 → ( 𝐹𝑤 ) ⊆ 𝑧 ) ) → 𝑦𝑧 ) } )
27 25 26 syl ( ( 𝜑 ∧ ( 𝐴𝑥𝑥 ∈ { 𝑦 ∣ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤𝑦 → ( 𝑤𝑧 → ( 𝐹𝑤 ) ⊆ 𝑧 ) ) → 𝑦𝑧 ) } ) ) → ( 𝐹𝐴 ) ⊆ { 𝑦 ∣ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤𝑦 → ( 𝑤𝑧 → ( 𝐹𝑤 ) ⊆ 𝑧 ) ) → 𝑦𝑧 ) } )
28 13 27 exlimddv ( 𝜑 → ( 𝐹𝐴 ) ⊆ { 𝑦 ∣ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤𝑦 → ( 𝑤𝑧 → ( 𝐹𝑤 ) ⊆ 𝑧 ) ) → 𝑦𝑧 ) } )
29 28 8 sseqtrrdi ( 𝜑 → ( 𝐹𝐴 ) ⊆ 𝐵 )