Theorem setrec2 50170

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(𝐹) is a subclass of all classes 𝐶 that are closed under 𝐹. Taken together, Theorems setrec1 50166 and setrec2v 50171 uniquely determine setrecs(𝐹) to be the minimal class closed under 𝐹.

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

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

Hypotheses

Ref	Expression
setrec2.1	⊢ Ⅎ𝑎𝐹
setrec2.2	⊢ 𝐵 = setrecs(𝐹)
setrec2.3	⊢ (𝜑 → ∀𝑎(𝑎 ⊆ 𝐶 → (𝐹‘𝑎) ⊆ 𝐶))

Assertion

Ref	Expression
setrec2	⊢ (𝜑 → 𝐵 ⊆ 𝐶)

Distinct variable group:   𝐶,𝑎

Allowed substitution hints:   𝜑(𝑎)   𝐵(𝑎)   𝐹(𝑎)

Proof of Theorem setrec2

Dummy variables 𝑥 𝑤 𝑦 𝑧 𝑢 are mutually distinct and distinct from all other variables.

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

Syntax hints:   → wi 4  ∀wal 1540   = wceq 1542  ∃!weu 2568  {cab 2714  Ⅎwnfc 2883   ⊆ wss 3889  ∪ cuni 4850   class class class wbr 5085   ↾ cres 5633  ‘cfv 6498  setrecscsetrecs 50158

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-rep 5212  ax-sep 5231  ax-nul 5241  ax-pow 5307  ax-pr 5375  ax-un 7689

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6454  df-fun 6500  df-fv 6506  df-setrecs 50159

This theorem is referenced by:  setrec2v  50171  setrec2mpt  50172