Users' Mathboxes Mathbox for Emmett Weisz < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  setrec2 Structured version   Visualization version   GIF version

Theorem setrec2 42767
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 42763 and setrec2v 42768 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 7095) 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.
StepHypRef Expression
1 setrec2.1 . . 3 𝑎𝐹
2 nfcv 2793 . . . . . 6 𝑎𝑥
3 nfcv 2793 . . . . . 6 𝑎𝑢
42, 1, 3nfbr 4732 . . . . 5 𝑎 𝑥𝐹𝑢
54nfeu 2514 . . . 4 𝑎∃!𝑢 𝑥𝐹𝑢
65nfab 2798 . . 3 𝑎{𝑥 ∣ ∃!𝑢 𝑥𝐹𝑢}
71, 6nfres 5430 . 2 𝑎(𝐹 ↾ {𝑥 ∣ ∃!𝑢 𝑥𝐹𝑢})
8 setrec2.2 . . 3 𝐵 = setrecs(𝐹)
9 setrec2lem1 42765 . . . . . . . . . . . 12 ((𝐹 ↾ {𝑥 ∣ ∃!𝑢 𝑥𝐹𝑢})‘𝑤) = (𝐹𝑤)
109sseq1i 3662 . . . . . . . . . . 11 (((𝐹 ↾ {𝑥 ∣ ∃!𝑢 𝑥𝐹𝑢})‘𝑤) ⊆ 𝑧 ↔ (𝐹𝑤) ⊆ 𝑧)
1110imbi2i 325 . . . . . . . . . 10 ((𝑤𝑧 → ((𝐹 ↾ {𝑥 ∣ ∃!𝑢 𝑥𝐹𝑢})‘𝑤) ⊆ 𝑧) ↔ (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧))
1211imbi2i 325 . . . . . . . . 9 ((𝑤𝑦 → (𝑤𝑧 → ((𝐹 ↾ {𝑥 ∣ ∃!𝑢 𝑥𝐹𝑢})‘𝑤) ⊆ 𝑧)) ↔ (𝑤𝑦 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)))
1312albii 1787 . . . . . . . 8 (∀𝑤(𝑤𝑦 → (𝑤𝑧 → ((𝐹 ↾ {𝑥 ∣ ∃!𝑢 𝑥𝐹𝑢})‘𝑤) ⊆ 𝑧)) ↔ ∀𝑤(𝑤𝑦 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)))
1413imbi1i 338 . . . . . . 7 ((∀𝑤(𝑤𝑦 → (𝑤𝑧 → ((𝐹 ↾ {𝑥 ∣ ∃!𝑢 𝑥𝐹𝑢})‘𝑤) ⊆ 𝑧)) → 𝑦𝑧) ↔ (∀𝑤(𝑤𝑦 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑦𝑧))
1514albii 1787 . . . . . 6 (∀𝑧(∀𝑤(𝑤𝑦 → (𝑤𝑧 → ((𝐹 ↾ {𝑥 ∣ ∃!𝑢 𝑥𝐹𝑢})‘𝑤) ⊆ 𝑧)) → 𝑦𝑧) ↔ ∀𝑧(∀𝑤(𝑤𝑦 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑦𝑧))
1615abbii 2768 . . . . 5 {𝑦 ∣ ∀𝑧(∀𝑤(𝑤𝑦 → (𝑤𝑧 → ((𝐹 ↾ {𝑥 ∣ ∃!𝑢 𝑥𝐹𝑢})‘𝑤) ⊆ 𝑧)) → 𝑦𝑧)} = {𝑦 ∣ ∀𝑧(∀𝑤(𝑤𝑦 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑦𝑧)}
1716unieqi 4477 . . . 4 {𝑦 ∣ ∀𝑧(∀𝑤(𝑤𝑦 → (𝑤𝑧 → ((𝐹 ↾ {𝑥 ∣ ∃!𝑢 𝑥𝐹𝑢})‘𝑤) ⊆ 𝑧)) → 𝑦𝑧)} = {𝑦 ∣ ∀𝑧(∀𝑤(𝑤𝑦 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑦𝑧)}
18 df-setrecs 42756 . . . 4 setrecs((𝐹 ↾ {𝑥 ∣ ∃!𝑢 𝑥𝐹𝑢})) = {𝑦 ∣ ∀𝑧(∀𝑤(𝑤𝑦 → (𝑤𝑧 → ((𝐹 ↾ {𝑥 ∣ ∃!𝑢 𝑥𝐹𝑢})‘𝑤) ⊆ 𝑧)) → 𝑦𝑧)}
19 df-setrecs 42756 . . . 4 setrecs(𝐹) = {𝑦 ∣ ∀𝑧(∀𝑤(𝑤𝑦 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑦𝑧)}
2017, 18, 193eqtr4ri 2684 . . 3 setrecs(𝐹) = setrecs((𝐹 ↾ {𝑥 ∣ ∃!𝑢 𝑥𝐹𝑢}))
218, 20eqtri 2673 . 2 𝐵 = setrecs((𝐹 ↾ {𝑥 ∣ ∃!𝑢 𝑥𝐹𝑢}))
22 setrec2lem2 42766 . 2 Fun (𝐹 ↾ {𝑥 ∣ ∃!𝑢 𝑥𝐹𝑢})
23 setrec2.3 . . 3 (𝜑 → ∀𝑎(𝑎𝐶 → (𝐹𝑎) ⊆ 𝐶))
24 setrec2lem1 42765 . . . . . 6 ((𝐹 ↾ {𝑥 ∣ ∃!𝑢 𝑥𝐹𝑢})‘𝑎) = (𝐹𝑎)
2524sseq1i 3662 . . . . 5 (((𝐹 ↾ {𝑥 ∣ ∃!𝑢 𝑥𝐹𝑢})‘𝑎) ⊆ 𝐶 ↔ (𝐹𝑎) ⊆ 𝐶)
2625imbi2i 325 . . . 4 ((𝑎𝐶 → ((𝐹 ↾ {𝑥 ∣ ∃!𝑢 𝑥𝐹𝑢})‘𝑎) ⊆ 𝐶) ↔ (𝑎𝐶 → (𝐹𝑎) ⊆ 𝐶))
2726albii 1787 . . 3 (∀𝑎(𝑎𝐶 → ((𝐹 ↾ {𝑥 ∣ ∃!𝑢 𝑥𝐹𝑢})‘𝑎) ⊆ 𝐶) ↔ ∀𝑎(𝑎𝐶 → (𝐹𝑎) ⊆ 𝐶))
2823, 27sylibr 224 . 2 (𝜑 → ∀𝑎(𝑎𝐶 → ((𝐹 ↾ {𝑥 ∣ ∃!𝑢 𝑥𝐹𝑢})‘𝑎) ⊆ 𝐶))
297, 21, 22, 28setrec2fun 42764 1 (𝜑𝐵𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1521   = wceq 1523  ∃!weu 2498  {cab 2637  wnfc 2780  wss 3607   cuni 4468   class class class wbr 4685  cres 5145  cfv 5926  setrecscsetrecs 42755
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-sbc 3469  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-opab 4746  df-id 5053  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-iota 5889  df-fun 5928  df-fv 5934  df-setrecs 42756
This theorem is referenced by:  setrec2v  42768
  Copyright terms: Public domain W3C validator