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

Theorem setrec2 42207
 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 42203 and setrec2v 42208 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 7038) 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 2762 . . . . . 6 𝑎𝑥
3 nfcv 2762 . . . . . 6 𝑎𝑢
42, 1, 3nfbr 4690 . . . . 5 𝑎 𝑥𝐹𝑢
54nfeu 2484 . . . 4 𝑎∃!𝑢 𝑥𝐹𝑢
65nfab 2766 . . 3 𝑎{𝑥 ∣ ∃!𝑢 𝑥𝐹𝑢}
71, 6nfres 5387 . 2 𝑎(𝐹 ↾ {𝑥 ∣ ∃!𝑢 𝑥𝐹𝑢})
8 setrec2.2 . . 3 𝐵 = setrecs(𝐹)
9 setrec2lem1 42205 . . . . . . . . . . . 12 ((𝐹 ↾ {𝑥 ∣ ∃!𝑢 𝑥𝐹𝑢})‘𝑤) = (𝐹𝑤)
109sseq1i 3621 . . . . . . . . . . 11 (((𝐹 ↾ {𝑥 ∣ ∃!𝑢 𝑥𝐹𝑢})‘𝑤) ⊆ 𝑧 ↔ (𝐹𝑤) ⊆ 𝑧)
1110imbi2i 326 . . . . . . . . . 10 ((𝑤𝑧 → ((𝐹 ↾ {𝑥 ∣ ∃!𝑢 𝑥𝐹𝑢})‘𝑤) ⊆ 𝑧) ↔ (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧))
1211imbi2i 326 . . . . . . . . 9 ((𝑤𝑦 → (𝑤𝑧 → ((𝐹 ↾ {𝑥 ∣ ∃!𝑢 𝑥𝐹𝑢})‘𝑤) ⊆ 𝑧)) ↔ (𝑤𝑦 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)))
1312albii 1745 . . . . . . . 8 (∀𝑤(𝑤𝑦 → (𝑤𝑧 → ((𝐹 ↾ {𝑥 ∣ ∃!𝑢 𝑥𝐹𝑢})‘𝑤) ⊆ 𝑧)) ↔ ∀𝑤(𝑤𝑦 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)))
1413imbi1i 339 . . . . . . 7 ((∀𝑤(𝑤𝑦 → (𝑤𝑧 → ((𝐹 ↾ {𝑥 ∣ ∃!𝑢 𝑥𝐹𝑢})‘𝑤) ⊆ 𝑧)) → 𝑦𝑧) ↔ (∀𝑤(𝑤𝑦 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑦𝑧))
1514albii 1745 . . . . . 6 (∀𝑧(∀𝑤(𝑤𝑦 → (𝑤𝑧 → ((𝐹 ↾ {𝑥 ∣ ∃!𝑢 𝑥𝐹𝑢})‘𝑤) ⊆ 𝑧)) → 𝑦𝑧) ↔ ∀𝑧(∀𝑤(𝑤𝑦 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑦𝑧))
1615abbii 2737 . . . . 5 {𝑦 ∣ ∀𝑧(∀𝑤(𝑤𝑦 → (𝑤𝑧 → ((𝐹 ↾ {𝑥 ∣ ∃!𝑢 𝑥𝐹𝑢})‘𝑤) ⊆ 𝑧)) → 𝑦𝑧)} = {𝑦 ∣ ∀𝑧(∀𝑤(𝑤𝑦 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑦𝑧)}
1716unieqi 4436 . . . 4 {𝑦 ∣ ∀𝑧(∀𝑤(𝑤𝑦 → (𝑤𝑧 → ((𝐹 ↾ {𝑥 ∣ ∃!𝑢 𝑥𝐹𝑢})‘𝑤) ⊆ 𝑧)) → 𝑦𝑧)} = {𝑦 ∣ ∀𝑧(∀𝑤(𝑤𝑦 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑦𝑧)}
18 df-setrecs 42196 . . . 4 setrecs((𝐹 ↾ {𝑥 ∣ ∃!𝑢 𝑥𝐹𝑢})) = {𝑦 ∣ ∀𝑧(∀𝑤(𝑤𝑦 → (𝑤𝑧 → ((𝐹 ↾ {𝑥 ∣ ∃!𝑢 𝑥𝐹𝑢})‘𝑤) ⊆ 𝑧)) → 𝑦𝑧)}
19 df-setrecs 42196 . . . 4 setrecs(𝐹) = {𝑦 ∣ ∀𝑧(∀𝑤(𝑤𝑦 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑦𝑧)}
2017, 18, 193eqtr4ri 2653 . . 3 setrecs(𝐹) = setrecs((𝐹 ↾ {𝑥 ∣ ∃!𝑢 𝑥𝐹𝑢}))
218, 20eqtri 2642 . 2 𝐵 = setrecs((𝐹 ↾ {𝑥 ∣ ∃!𝑢 𝑥𝐹𝑢}))
22 setrec2lem2 42206 . 2 Fun (𝐹 ↾ {𝑥 ∣ ∃!𝑢 𝑥𝐹𝑢})
23 setrec2.3 . . 3 (𝜑 → ∀𝑎(𝑎𝐶 → (𝐹𝑎) ⊆ 𝐶))
24 setrec2lem1 42205 . . . . . 6 ((𝐹 ↾ {𝑥 ∣ ∃!𝑢 𝑥𝐹𝑢})‘𝑎) = (𝐹𝑎)
2524sseq1i 3621 . . . . 5 (((𝐹 ↾ {𝑥 ∣ ∃!𝑢 𝑥𝐹𝑢})‘𝑎) ⊆ 𝐶 ↔ (𝐹𝑎) ⊆ 𝐶)
2625imbi2i 326 . . . 4 ((𝑎𝐶 → ((𝐹 ↾ {𝑥 ∣ ∃!𝑢 𝑥𝐹𝑢})‘𝑎) ⊆ 𝐶) ↔ (𝑎𝐶 → (𝐹𝑎) ⊆ 𝐶))
2726albii 1745 . . 3 (∀𝑎(𝑎𝐶 → ((𝐹 ↾ {𝑥 ∣ ∃!𝑢 𝑥𝐹𝑢})‘𝑎) ⊆ 𝐶) ↔ ∀𝑎(𝑎𝐶 → (𝐹𝑎) ⊆ 𝐶))
2823, 27sylibr 224 . 2 (𝜑 → ∀𝑎(𝑎𝐶 → ((𝐹 ↾ {𝑥 ∣ ∃!𝑢 𝑥𝐹𝑢})‘𝑎) ⊆ 𝐶))
297, 21, 22, 28setrec2fun 42204 1 (𝜑𝐵𝐶)
 Colors of variables: wff setvar class Syntax hints:   → wi 4  ∀wal 1479   = wceq 1481  ∃!weu 2468  {cab 2606  Ⅎwnfc 2749   ⊆ wss 3567  ∪ cuni 4427   class class class wbr 4644   ↾ cres 5106  ‘cfv 5876  setrecscsetrecs 42195 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-rep 4762  ax-sep 4772  ax-nul 4780  ax-pow 4834  ax-pr 4897  ax-un 6934 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ne 2792  df-ral 2914  df-rex 2915  df-rab 2918  df-v 3197  df-sbc 3430  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-pw 4151  df-sn 4169  df-pr 4171  df-op 4175  df-uni 4428  df-br 4645  df-opab 4704  df-id 5014  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-rn 5115  df-res 5116  df-ima 5117  df-iota 5839  df-fun 5878  df-fv 5884  df-setrecs 42196 This theorem is referenced by:  setrec2v  42208
 Copyright terms: Public domain W3C validator