Theorem setrec2 48926

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 48922 and setrec2v 48927 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 7874) 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 2903	. . . . . 6 ⊢ Ⅎ𝑎𝑥
3		nfcv 2903	. . . . . 6 ⊢ Ⅎ𝑎𝑢
4	2, 1, 3	nfbr 5195	. . . . 5 ⊢ Ⅎ𝑎 𝑥𝐹𝑢
5	4	nfeuw 2591	. . . 4 ⊢ Ⅎ𝑎∃!𝑢 𝑥𝐹𝑢
6	5	nfab 2909	. . 3 ⊢ Ⅎ𝑎{𝑥 ∣ ∃!𝑢 𝑥𝐹𝑢}
7	1, 6	nfres 6002	. 2 ⊢ Ⅎ𝑎(𝐹 ↾ {𝑥 ∣ ∃!𝑢 𝑥𝐹𝑢})
8		setrec2.2	. . 3 ⊢ 𝐵 = setrecs(𝐹)
9		setrec2lem1 48924	. . . . . . . . . . . 12 ⊢ ((𝐹 ↾ {𝑥 ∣ ∃!𝑢 𝑥𝐹𝑢})‘𝑤) = (𝐹‘𝑤)
10	9	sseq1i 4024	. . . . . . . . . . 11 ⊢ (((𝐹 ↾ {𝑥 ∣ ∃!𝑢 𝑥𝐹𝑢})‘𝑤) ⊆ 𝑧 ↔ (𝐹‘𝑤) ⊆ 𝑧)
11	10	imbi2i 336	. . . . . . . . . 10 ⊢ ((𝑤 ⊆ 𝑧 → ((𝐹 ↾ {𝑥 ∣ ∃!𝑢 𝑥𝐹𝑢})‘𝑤) ⊆ 𝑧) ↔ (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧))
12	11	imbi2i 336	. . . . . . . . 9 ⊢ ((𝑤 ⊆ 𝑦 → (𝑤 ⊆ 𝑧 → ((𝐹 ↾ {𝑥 ∣ ∃!𝑢 𝑥𝐹𝑢})‘𝑤) ⊆ 𝑧)) ↔ (𝑤 ⊆ 𝑦 → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)))
13	12	albii 1816	. . . . . . . 8 ⊢ (∀𝑤(𝑤 ⊆ 𝑦 → (𝑤 ⊆ 𝑧 → ((𝐹 ↾ {𝑥 ∣ ∃!𝑢 𝑥𝐹𝑢})‘𝑤) ⊆ 𝑧)) ↔ ∀𝑤(𝑤 ⊆ 𝑦 → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)))
14	13	imbi1i 349	. . . . . . 7 ⊢ ((∀𝑤(𝑤 ⊆ 𝑦 → (𝑤 ⊆ 𝑧 → ((𝐹 ↾ {𝑥 ∣ ∃!𝑢 𝑥𝐹𝑢})‘𝑤) ⊆ 𝑧)) → 𝑦 ⊆ 𝑧) ↔ (∀𝑤(𝑤 ⊆ 𝑦 → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)) → 𝑦 ⊆ 𝑧))
15	14	albii 1816	. . . . . 6 ⊢ (∀𝑧(∀𝑤(𝑤 ⊆ 𝑦 → (𝑤 ⊆ 𝑧 → ((𝐹 ↾ {𝑥 ∣ ∃!𝑢 𝑥𝐹𝑢})‘𝑤) ⊆ 𝑧)) → 𝑦 ⊆ 𝑧) ↔ ∀𝑧(∀𝑤(𝑤 ⊆ 𝑦 → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)) → 𝑦 ⊆ 𝑧))
16	15	abbii 2807	. . . . 5 ⊢ {𝑦 ∣ ∀𝑧(∀𝑤(𝑤 ⊆ 𝑦 → (𝑤 ⊆ 𝑧 → ((𝐹 ↾ {𝑥 ∣ ∃!𝑢 𝑥𝐹𝑢})‘𝑤) ⊆ 𝑧)) → 𝑦 ⊆ 𝑧)} = {𝑦 ∣ ∀𝑧(∀𝑤(𝑤 ⊆ 𝑦 → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)) → 𝑦 ⊆ 𝑧)}
17	16	unieqi 4924	. . . 4 ⊢ ∪ {𝑦 ∣ ∀𝑧(∀𝑤(𝑤 ⊆ 𝑦 → (𝑤 ⊆ 𝑧 → ((𝐹 ↾ {𝑥 ∣ ∃!𝑢 𝑥𝐹𝑢})‘𝑤) ⊆ 𝑧)) → 𝑦 ⊆ 𝑧)} = ∪ {𝑦 ∣ ∀𝑧(∀𝑤(𝑤 ⊆ 𝑦 → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)) → 𝑦 ⊆ 𝑧)}
18		df-setrecs 48915	. . . 4 ⊢ setrecs((𝐹 ↾ {𝑥 ∣ ∃!𝑢 𝑥𝐹𝑢})) = ∪ {𝑦 ∣ ∀𝑧(∀𝑤(𝑤 ⊆ 𝑦 → (𝑤 ⊆ 𝑧 → ((𝐹 ↾ {𝑥 ∣ ∃!𝑢 𝑥𝐹𝑢})‘𝑤) ⊆ 𝑧)) → 𝑦 ⊆ 𝑧)}
19		df-setrecs 48915	. . . 4 ⊢ setrecs(𝐹) = ∪ {𝑦 ∣ ∀𝑧(∀𝑤(𝑤 ⊆ 𝑦 → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)) → 𝑦 ⊆ 𝑧)}
20	17, 18, 19	3eqtr4ri 2774	. . 3 ⊢ setrecs(𝐹) = setrecs((𝐹 ↾ {𝑥 ∣ ∃!𝑢 𝑥𝐹𝑢}))
21	8, 20	eqtri 2763	. 2 ⊢ 𝐵 = setrecs((𝐹 ↾ {𝑥 ∣ ∃!𝑢 𝑥𝐹𝑢}))
22		setrec2lem2 48925	. 2 ⊢ Fun (𝐹 ↾ {𝑥 ∣ ∃!𝑢 𝑥𝐹𝑢})
23		setrec2.3	. . 3 ⊢ (𝜑 → ∀𝑎(𝑎 ⊆ 𝐶 → (𝐹‘𝑎) ⊆ 𝐶))
24		setrec2lem1 48924	. . . . . 6 ⊢ ((𝐹 ↾ {𝑥 ∣ ∃!𝑢 𝑥𝐹𝑢})‘𝑎) = (𝐹‘𝑎)
25	24	sseq1i 4024	. . . . 5 ⊢ (((𝐹 ↾ {𝑥 ∣ ∃!𝑢 𝑥𝐹𝑢})‘𝑎) ⊆ 𝐶 ↔ (𝐹‘𝑎) ⊆ 𝐶)
26	25	imbi2i 336	. . . 4 ⊢ ((𝑎 ⊆ 𝐶 → ((𝐹 ↾ {𝑥 ∣ ∃!𝑢 𝑥𝐹𝑢})‘𝑎) ⊆ 𝐶) ↔ (𝑎 ⊆ 𝐶 → (𝐹‘𝑎) ⊆ 𝐶))
27	26	albii 1816	. . 3 ⊢ (∀𝑎(𝑎 ⊆ 𝐶 → ((𝐹 ↾ {𝑥 ∣ ∃!𝑢 𝑥𝐹𝑢})‘𝑎) ⊆ 𝐶) ↔ ∀𝑎(𝑎 ⊆ 𝐶 → (𝐹‘𝑎) ⊆ 𝐶))
28	23, 27	sylibr 234	. 2 ⊢ (𝜑 → ∀𝑎(𝑎 ⊆ 𝐶 → ((𝐹 ↾ {𝑥 ∣ ∃!𝑢 𝑥𝐹𝑢})‘𝑎) ⊆ 𝐶))
29	7, 21, 22, 28	setrec2fun 48923	1 ⊢ (𝜑 → 𝐵 ⊆ 𝐶)

Syntax hints:   → wi 4  ∀wal 1535   = wceq 1537  ∃!weu 2566  {cab 2712  Ⅎwnfc 2888   ⊆ wss 3963  ∪ cuni 4912   class class class wbr 5148   ↾ cres 5691  ‘cfv 6563  setrecscsetrecs 48914

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-rep 5285  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-opab 5211  df-id 5583  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-iota 6516  df-fun 6565  df-fv 6571  df-setrecs 48915

This theorem is referenced by:  setrec2v  48927  setrec2mpt  48928