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	⊢ Ⅎ 𝑎 𝐹
	setrec2.2	⊢ 𝐵 = setrecs ( 𝐹 )
	setrec2.3	⊢ ( 𝜑 → ∀ 𝑎 ( 𝑎 ⊆ 𝐶 → ( 𝐹 ‘ 𝑎 ) ⊆ 𝐶 ) )
Assertion	setrec2	⊢ ( 𝜑 → 𝐵 ⊆ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		setrec2.1	⊢ Ⅎ 𝑎 𝐹
2		setrec2.2	⊢ 𝐵 = setrecs ( 𝐹 )
3		setrec2.3	⊢ ( 𝜑 → ∀ 𝑎 ( 𝑎 ⊆ 𝐶 → ( 𝐹 ‘ 𝑎 ) ⊆ 𝐶 ) )
4		nfcv	⊢ Ⅎ 𝑎 𝑥
5		nfcv	⊢ Ⅎ 𝑎 𝑢
6	4 1 5	nfbr	⊢ Ⅎ 𝑎 𝑥 𝐹 𝑢
7	6	nfeuw	⊢ Ⅎ 𝑎 ∃! 𝑢 𝑥 𝐹 𝑢
8	7	nfab	⊢ Ⅎ 𝑎 { 𝑥 ∣ ∃! 𝑢 𝑥 𝐹 𝑢 }
9	1 8	nfres	⊢ Ⅎ 𝑎 ( 𝐹 ↾ { 𝑥 ∣ ∃! 𝑢 𝑥 𝐹 𝑢 } )
10		setrec2lem1	⊢ ( ( 𝐹 ↾ { 𝑥 ∣ ∃! 𝑢 𝑥 𝐹 𝑢 } ) ‘ 𝑤 ) = ( 𝐹 ‘ 𝑤 )
11	10	sseq1i	⊢ ( ( ( 𝐹 ↾ { 𝑥 ∣ ∃! 𝑢 𝑥 𝐹 𝑢 } ) ‘ 𝑤 ) ⊆ 𝑧 ↔ ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 )
12	11	imbi2i	⊢ ( ( 𝑤 ⊆ 𝑧 → ( ( 𝐹 ↾ { 𝑥 ∣ ∃! 𝑢 𝑥 𝐹 𝑢 } ) ‘ 𝑤 ) ⊆ 𝑧 ) ↔ ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) )
13	12	imbi2i	⊢ ( ( 𝑤 ⊆ 𝑦 → ( 𝑤 ⊆ 𝑧 → ( ( 𝐹 ↾ { 𝑥 ∣ ∃! 𝑢 𝑥 𝐹 𝑢 } ) ‘ 𝑤 ) ⊆ 𝑧 ) ) ↔ ( 𝑤 ⊆ 𝑦 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) )
14	13	albii	⊢ ( ∀ 𝑤 ( 𝑤 ⊆ 𝑦 → ( 𝑤 ⊆ 𝑧 → ( ( 𝐹 ↾ { 𝑥 ∣ ∃! 𝑢 𝑥 𝐹 𝑢 } ) ‘ 𝑤 ) ⊆ 𝑧 ) ) ↔ ∀ 𝑤 ( 𝑤 ⊆ 𝑦 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) )
15	14	imbi1i	⊢ ( ( ∀ 𝑤 ( 𝑤 ⊆ 𝑦 → ( 𝑤 ⊆ 𝑧 → ( ( 𝐹 ↾ { 𝑥 ∣ ∃! 𝑢 𝑥 𝐹 𝑢 } ) ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑦 ⊆ 𝑧 ) ↔ ( ∀ 𝑤 ( 𝑤 ⊆ 𝑦 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑦 ⊆ 𝑧 ) )
16	15	albii	⊢ ( ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑦 → ( 𝑤 ⊆ 𝑧 → ( ( 𝐹 ↾ { 𝑥 ∣ ∃! 𝑢 𝑥 𝐹 𝑢 } ) ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑦 ⊆ 𝑧 ) ↔ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑦 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑦 ⊆ 𝑧 ) )
17	16	abbii	⊢ { 𝑦 ∣ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑦 → ( 𝑤 ⊆ 𝑧 → ( ( 𝐹 ↾ { 𝑥 ∣ ∃! 𝑢 𝑥 𝐹 𝑢 } ) ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑦 ⊆ 𝑧 ) } = { 𝑦 ∣ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑦 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑦 ⊆ 𝑧 ) }
18	17	unieqi	⊢ ∪ { 𝑦 ∣ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑦 → ( 𝑤 ⊆ 𝑧 → ( ( 𝐹 ↾ { 𝑥 ∣ ∃! 𝑢 𝑥 𝐹 𝑢 } ) ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑦 ⊆ 𝑧 ) } = ∪ { 𝑦 ∣ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑦 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑦 ⊆ 𝑧 ) }
19		df-setrecs	⊢ setrecs ( ( 𝐹 ↾ { 𝑥 ∣ ∃! 𝑢 𝑥 𝐹 𝑢 } ) ) = ∪ { 𝑦 ∣ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑦 → ( 𝑤 ⊆ 𝑧 → ( ( 𝐹 ↾ { 𝑥 ∣ ∃! 𝑢 𝑥 𝐹 𝑢 } ) ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑦 ⊆ 𝑧 ) }
20		df-setrecs	⊢ setrecs ( 𝐹 ) = ∪ { 𝑦 ∣ ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑦 → ( 𝑤 ⊆ 𝑧 → ( 𝐹 ‘ 𝑤 ) ⊆ 𝑧 ) ) → 𝑦 ⊆ 𝑧 ) }
21	18 19 20	3eqtr4ri	⊢ setrecs ( 𝐹 ) = setrecs ( ( 𝐹 ↾ { 𝑥 ∣ ∃! 𝑢 𝑥 𝐹 𝑢 } ) )
22	2 21	eqtri	⊢ 𝐵 = setrecs ( ( 𝐹 ↾ { 𝑥 ∣ ∃! 𝑢 𝑥 𝐹 𝑢 } ) )
23		setrec2lem2	⊢ Fun ( 𝐹 ↾ { 𝑥 ∣ ∃! 𝑢 𝑥 𝐹 𝑢 } )
24		setrec2lem1	⊢ ( ( 𝐹 ↾ { 𝑥 ∣ ∃! 𝑢 𝑥 𝐹 𝑢 } ) ‘ 𝑎 ) = ( 𝐹 ‘ 𝑎 )
25	24	sseq1i	⊢ ( ( ( 𝐹 ↾ { 𝑥 ∣ ∃! 𝑢 𝑥 𝐹 𝑢 } ) ‘ 𝑎 ) ⊆ 𝐶 ↔ ( 𝐹 ‘ 𝑎 ) ⊆ 𝐶 )
26	25	imbi2i	⊢ ( ( 𝑎 ⊆ 𝐶 → ( ( 𝐹 ↾ { 𝑥 ∣ ∃! 𝑢 𝑥 𝐹 𝑢 } ) ‘ 𝑎 ) ⊆ 𝐶 ) ↔ ( 𝑎 ⊆ 𝐶 → ( 𝐹 ‘ 𝑎 ) ⊆ 𝐶 ) )
27	26	albii	⊢ ( ∀ 𝑎 ( 𝑎 ⊆ 𝐶 → ( ( 𝐹 ↾ { 𝑥 ∣ ∃! 𝑢 𝑥 𝐹 𝑢 } ) ‘ 𝑎 ) ⊆ 𝐶 ) ↔ ∀ 𝑎 ( 𝑎 ⊆ 𝐶 → ( 𝐹 ‘ 𝑎 ) ⊆ 𝐶 ) )
28	3 27	sylibr	⊢ ( 𝜑 → ∀ 𝑎 ( 𝑎 ⊆ 𝐶 → ( ( 𝐹 ↾ { 𝑥 ∣ ∃! 𝑢 𝑥 𝐹 𝑢 } ) ‘ 𝑎 ) ⊆ 𝐶 ) )
29	9 22 23 28	setrec2fun	⊢ ( 𝜑 → 𝐵 ⊆ 𝐶 )