Metamath Proof Explorer


Theorem setrec2

Description: This is the second of two fundamental theorems about set recursion from which all other facts will be derived. It states that the class setrecs ( F ) is a subclass of all classes C that are closed under F . Taken together, Theorems setrec1 and setrec2v uniquely determine setrecs ( F ) to be the minimal class closed under F .

We express this by saying that if F respects the C_ relation and C is closed under F , then B C_ C . By substituting strategically constructed classes for C , we can easily prove many useful properties. Although this theorem cannot show equality between B and C , if we intend to prove equality between B and some particular class (such as On ), we first apply this theorem, then the relevant induction theorem (such as tfi ) to the other class.

(Contributed by Emmett Weisz, 2-Sep-2021)

Ref Expression
Hypotheses setrec2.1 _ a F
setrec2.2 B = setrecs F
setrec2.3 φ a a C F a C
Assertion setrec2 φ B C

Proof

Step Hyp Ref Expression
1 setrec2.1 _ a F
2 setrec2.2 B = setrecs F
3 setrec2.3 φ a a C F a C
4 nfcv _ a x
5 nfcv _ a u
6 4 1 5 nfbr a x F u
7 6 nfeuw a ∃! u x F u
8 7 nfab _ a x | ∃! u x F u
9 1 8 nfres _ a F x | ∃! u x F u
10 setrec2lem1 F x | ∃! u x F u w = F w
11 10 sseq1i F x | ∃! u x F u w z F w z
12 11 imbi2i w z F x | ∃! u x F u w z w z F w z
13 12 imbi2i w y w z F x | ∃! u x F u w z w y w z F w z
14 13 albii w w y w z F x | ∃! u x F u w z w w y w z F w z
15 14 imbi1i w w y w z F x | ∃! u x F u w z y z w w y w z F w z y z
16 15 albii z w w y w z F x | ∃! u x F u w z y z z w w y w z F w z y z
17 16 abbii y | z w w y w z F x | ∃! u x F u w z y z = y | z w w y w z F w z y z
18 17 unieqi y | z w w y w z F x | ∃! u x F u w z y z = y | z w w y w z F w z y z
19 df-setrecs setrecs F x | ∃! u x F u = y | z w w y w z F x | ∃! u x F u w z y z
20 df-setrecs setrecs F = y | z w w y w z F w z y z
21 18 19 20 3eqtr4ri setrecs F = setrecs F x | ∃! u x F u
22 2 21 eqtri B = setrecs F x | ∃! u x F u
23 setrec2lem2 Fun F x | ∃! u x F u
24 setrec2lem1 F x | ∃! u x F u a = F a
25 24 sseq1i F x | ∃! u x F u a C F a C
26 25 imbi2i a C F x | ∃! u x F u a C a C F a C
27 26 albii a a C F x | ∃! u x F u a C a a C F a C
28 3 27 sylibr φ a a C F x | ∃! u x F u a C
29 9 22 23 28 setrec2fun φ B C