Theorem setrec2 50048

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 50044 and setrec2v 50049 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 7805) 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 2899	. . . . . 6 ⊢ Ⅎ𝑎𝑥
3		nfcv 2899	. . . . . 6 ⊢ Ⅎ𝑎𝑢
4	2, 1, 3	nfbr 5147	. . . . 5 ⊢ Ⅎ𝑎 𝑥𝐹𝑢
5	4	nfeuw 2594	. . . 4 ⊢ Ⅎ𝑎∃!𝑢 𝑥𝐹𝑢
6	5	nfab 2905	. . 3 ⊢ Ⅎ𝑎{𝑥 ∣ ∃!𝑢 𝑥𝐹𝑢}
7	1, 6	nfres 5948	. 2 ⊢ Ⅎ𝑎(𝐹 ↾ {𝑥 ∣ ∃!𝑢 𝑥𝐹𝑢})
8		setrec2.2	. . 3 ⊢ 𝐵 = setrecs(𝐹)
9		setrec2lem1 50046	. . . . . . . . . . . 12 ⊢ ((𝐹 ↾ {𝑥 ∣ ∃!𝑢 𝑥𝐹𝑢})‘𝑤) = (𝐹‘𝑤)
10	9	sseq1i 3964	. . . . . . . . . . 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 2804	. . . . 5 ⊢ {𝑦 ∣ ∀𝑧(∀𝑤(𝑤 ⊆ 𝑦 → (𝑤 ⊆ 𝑧 → ((𝐹 ↾ {𝑥 ∣ ∃!𝑢 𝑥𝐹𝑢})‘𝑤) ⊆ 𝑧)) → 𝑦 ⊆ 𝑧)} = {𝑦 ∣ ∀𝑧(∀𝑤(𝑤 ⊆ 𝑦 → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)) → 𝑦 ⊆ 𝑧)}
17	16	unieqi 4877	. . . 4 ⊢ ∪ {𝑦 ∣ ∀𝑧(∀𝑤(𝑤 ⊆ 𝑦 → (𝑤 ⊆ 𝑧 → ((𝐹 ↾ {𝑥 ∣ ∃!𝑢 𝑥𝐹𝑢})‘𝑤) ⊆ 𝑧)) → 𝑦 ⊆ 𝑧)} = ∪ {𝑦 ∣ ∀𝑧(∀𝑤(𝑤 ⊆ 𝑦 → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)) → 𝑦 ⊆ 𝑧)}
18		df-setrecs 50037	. . . 4 ⊢ setrecs((𝐹 ↾ {𝑥 ∣ ∃!𝑢 𝑥𝐹𝑢})) = ∪ {𝑦 ∣ ∀𝑧(∀𝑤(𝑤 ⊆ 𝑦 → (𝑤 ⊆ 𝑧 → ((𝐹 ↾ {𝑥 ∣ ∃!𝑢 𝑥𝐹𝑢})‘𝑤) ⊆ 𝑧)) → 𝑦 ⊆ 𝑧)}
19		df-setrecs 50037	. . . 4 ⊢ setrecs(𝐹) = ∪ {𝑦 ∣ ∀𝑧(∀𝑤(𝑤 ⊆ 𝑦 → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)) → 𝑦 ⊆ 𝑧)}
20	17, 18, 19	3eqtr4ri 2771	. . 3 ⊢ setrecs(𝐹) = setrecs((𝐹 ↾ {𝑥 ∣ ∃!𝑢 𝑥𝐹𝑢}))
21	8, 20	eqtri 2760	. 2 ⊢ 𝐵 = setrecs((𝐹 ↾ {𝑥 ∣ ∃!𝑢 𝑥𝐹𝑢}))
22		setrec2lem2 50047	. 2 ⊢ Fun (𝐹 ↾ {𝑥 ∣ ∃!𝑢 𝑥𝐹𝑢})
23		setrec2.3	. . 3 ⊢ (𝜑 → ∀𝑎(𝑎 ⊆ 𝐶 → (𝐹‘𝑎) ⊆ 𝐶))
24		setrec2lem1 50046	. . . . . 6 ⊢ ((𝐹 ↾ {𝑥 ∣ ∃!𝑢 𝑥𝐹𝑢})‘𝑎) = (𝐹‘𝑎)
25	24	sseq1i 3964	. . . . 5 ⊢ (((𝐹 ↾ {𝑥 ∣ ∃!𝑢 𝑥𝐹𝑢})‘𝑎) ⊆ 𝐶 ↔ (𝐹‘𝑎) ⊆ 𝐶)
26	25	imbi2i 336	. . . 4 ⊢ ((𝑎 ⊆ 𝐶 → ((𝐹 ↾ {𝑥 ∣ ∃!𝑢 𝑥𝐹𝑢})‘𝑎) ⊆ 𝐶) ↔ (𝑎 ⊆ 𝐶 → (𝐹‘𝑎) ⊆ 𝐶))
27	26	albii 1821	. . 3 ⊢ (∀𝑎(𝑎 ⊆ 𝐶 → ((𝐹 ↾ {𝑥 ∣ ∃!𝑢 𝑥𝐹𝑢})‘𝑎) ⊆ 𝐶) ↔ ∀𝑎(𝑎 ⊆ 𝐶 → (𝐹‘𝑎) ⊆ 𝐶))
28	23, 27	sylibr 234	. 2 ⊢ (𝜑 → ∀𝑎(𝑎 ⊆ 𝐶 → ((𝐹 ↾ {𝑥 ∣ ∃!𝑢 𝑥𝐹𝑢})‘𝑎) ⊆ 𝐶))
29	7, 21, 22, 28	setrec2fun 50045	1 ⊢ (𝜑 → 𝐵 ⊆ 𝐶)

Syntax hints:   → wi 4  ∀wal 1540   = wceq 1542  ∃!weu 2569  {cab 2715  Ⅎwnfc 2884   ⊆ wss 3903  ∪ cuni 4865   class class class wbr 5100   ↾ cres 5634  ‘cfv 6500  setrecscsetrecs 50036

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 2709  ax-rep 5226  ax-sep 5243  ax-nul 5253  ax-pow 5312  ax-pr 5379  ax-un 7690

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 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-iota 6456  df-fun 6502  df-fv 6508  df-setrecs 50037

This theorem is referenced by:  setrec2v  50049  setrec2mpt  50050