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

Theorem setrec2fun 47639
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 47638 and setrec2v 47643 say that setrecs(𝐹) is 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 7837) to the other class. (Contributed by Emmett Weisz, 15-Feb-2021.) (New usage is discouraged.)

Hypotheses
Ref Expression
setrec2fun.1 𝑎𝐹
setrec2fun.2 𝐵 = setrecs(𝐹)
setrec2fun.3 Fun 𝐹
setrec2fun.4 (𝜑 → ∀𝑎(𝑎𝐶 → (𝐹𝑎) ⊆ 𝐶))
Assertion
Ref Expression
setrec2fun (𝜑𝐵𝐶)
Distinct variable group:   𝐶,𝑎
Allowed substitution hints:   𝜑(𝑎)   𝐵(𝑎)   𝐹(𝑎)

Proof of Theorem setrec2fun
Dummy variables 𝑥 𝑤 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 setrec2fun.2 . . 3 𝐵 = setrecs(𝐹)
2 df-setrecs 47631 . . 3 setrecs(𝐹) = {𝑦 ∣ ∀𝑧(∀𝑤(𝑤𝑦 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑦𝑧)}
31, 2eqtri 2761 . 2 𝐵 = {𝑦 ∣ ∀𝑧(∀𝑤(𝑤𝑦 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑦𝑧)}
4 eqid 2733 . . . . . 6 {𝑦 ∣ ∀𝑧(∀𝑤(𝑤𝑦 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑦𝑧)} = {𝑦 ∣ ∀𝑧(∀𝑤(𝑤𝑦 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑦𝑧)}
5 vex 3479 . . . . . . 7 𝑥 ∈ V
65a1i 11 . . . . . 6 (𝜑𝑥 ∈ V)
74, 6setrec1lem1 47634 . . . . 5 (𝜑 → (𝑥 ∈ {𝑦 ∣ ∀𝑧(∀𝑤(𝑤𝑦 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑦𝑧)} ↔ ∀𝑧(∀𝑤(𝑤𝑥 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑥𝑧)))
8 id 22 . . . . . . . . . . . . . . 15 (𝑤 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)) → 𝑤 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)))
9 inss1 4227 . . . . . . . . . . . . . . 15 (𝐶 (𝐹 “ 𝒫 𝑥)) ⊆ 𝐶
108, 9sstrdi 3993 . . . . . . . . . . . . . 14 (𝑤 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)) → 𝑤𝐶)
11 setrec2fun.4 . . . . . . . . . . . . . . 15 (𝜑 → ∀𝑎(𝑎𝐶 → (𝐹𝑎) ⊆ 𝐶))
12 nfv 1918 . . . . . . . . . . . . . . . . 17 𝑎 𝑤𝐶
13 setrec2fun.1 . . . . . . . . . . . . . . . . . . 19 𝑎𝐹
14 nfcv 2904 . . . . . . . . . . . . . . . . . . 19 𝑎𝑤
1513, 14nffv 6898 . . . . . . . . . . . . . . . . . 18 𝑎(𝐹𝑤)
16 nfcv 2904 . . . . . . . . . . . . . . . . . 18 𝑎𝐶
1715, 16nfss 3973 . . . . . . . . . . . . . . . . 17 𝑎(𝐹𝑤) ⊆ 𝐶
1812, 17nfim 1900 . . . . . . . . . . . . . . . 16 𝑎(𝑤𝐶 → (𝐹𝑤) ⊆ 𝐶)
19 sseq1 4006 . . . . . . . . . . . . . . . . . 18 (𝑎 = 𝑤 → (𝑎𝐶𝑤𝐶))
20 fveq2 6888 . . . . . . . . . . . . . . . . . . 19 (𝑎 = 𝑤 → (𝐹𝑎) = (𝐹𝑤))
2120sseq1d 4012 . . . . . . . . . . . . . . . . . 18 (𝑎 = 𝑤 → ((𝐹𝑎) ⊆ 𝐶 ↔ (𝐹𝑤) ⊆ 𝐶))
2219, 21imbi12d 345 . . . . . . . . . . . . . . . . 17 (𝑎 = 𝑤 → ((𝑎𝐶 → (𝐹𝑎) ⊆ 𝐶) ↔ (𝑤𝐶 → (𝐹𝑤) ⊆ 𝐶)))
2322biimpd 228 . . . . . . . . . . . . . . . 16 (𝑎 = 𝑤 → ((𝑎𝐶 → (𝐹𝑎) ⊆ 𝐶) → (𝑤𝐶 → (𝐹𝑤) ⊆ 𝐶)))
2418, 23spimfv 2233 . . . . . . . . . . . . . . 15 (∀𝑎(𝑎𝐶 → (𝐹𝑎) ⊆ 𝐶) → (𝑤𝐶 → (𝐹𝑤) ⊆ 𝐶))
2511, 24syl 17 . . . . . . . . . . . . . 14 (𝜑 → (𝑤𝐶 → (𝐹𝑤) ⊆ 𝐶))
2610, 25syl5 34 . . . . . . . . . . . . 13 (𝜑 → (𝑤 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)) → (𝐹𝑤) ⊆ 𝐶))
2726imp 408 . . . . . . . . . . . 12 ((𝜑𝑤 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥))) → (𝐹𝑤) ⊆ 𝐶)
28273adant2 1132 . . . . . . . . . . 11 ((𝜑𝑤𝑥𝑤 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥))) → (𝐹𝑤) ⊆ 𝐶)
29 velpw 4606 . . . . . . . . . . . . . . 15 (𝑤 ∈ 𝒫 𝑥𝑤𝑥)
30 eliman0 6928 . . . . . . . . . . . . . . . 16 ((𝑤 ∈ 𝒫 𝑥 ∧ ¬ (𝐹𝑤) = ∅) → (𝐹𝑤) ∈ (𝐹 “ 𝒫 𝑥))
3130ex 414 . . . . . . . . . . . . . . 15 (𝑤 ∈ 𝒫 𝑥 → (¬ (𝐹𝑤) = ∅ → (𝐹𝑤) ∈ (𝐹 “ 𝒫 𝑥)))
3229, 31sylbir 234 . . . . . . . . . . . . . 14 (𝑤𝑥 → (¬ (𝐹𝑤) = ∅ → (𝐹𝑤) ∈ (𝐹 “ 𝒫 𝑥)))
33 elssuni 4940 . . . . . . . . . . . . . 14 ((𝐹𝑤) ∈ (𝐹 “ 𝒫 𝑥) → (𝐹𝑤) ⊆ (𝐹 “ 𝒫 𝑥))
3432, 33syl6 35 . . . . . . . . . . . . 13 (𝑤𝑥 → (¬ (𝐹𝑤) = ∅ → (𝐹𝑤) ⊆ (𝐹 “ 𝒫 𝑥)))
35 id 22 . . . . . . . . . . . . . 14 ((𝐹𝑤) = ∅ → (𝐹𝑤) = ∅)
36 0ss 4395 . . . . . . . . . . . . . 14 ∅ ⊆ (𝐹 “ 𝒫 𝑥)
3735, 36eqsstrdi 4035 . . . . . . . . . . . . 13 ((𝐹𝑤) = ∅ → (𝐹𝑤) ⊆ (𝐹 “ 𝒫 𝑥))
3834, 37pm2.61d2 181 . . . . . . . . . . . 12 (𝑤𝑥 → (𝐹𝑤) ⊆ (𝐹 “ 𝒫 𝑥))
39383ad2ant2 1135 . . . . . . . . . . 11 ((𝜑𝑤𝑥𝑤 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥))) → (𝐹𝑤) ⊆ (𝐹 “ 𝒫 𝑥))
4028, 39ssind 4231 . . . . . . . . . 10 ((𝜑𝑤𝑥𝑤 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥))) → (𝐹𝑤) ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)))
41403exp 1120 . . . . . . . . 9 (𝜑 → (𝑤𝑥 → (𝑤 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)) → (𝐹𝑤) ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)))))
4241alrimiv 1931 . . . . . . . 8 (𝜑 → ∀𝑤(𝑤𝑥 → (𝑤 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)) → (𝐹𝑤) ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)))))
43 setrec2fun.3 . . . . . . . . . . . 12 Fun 𝐹
445pwex 5377 . . . . . . . . . . . . 13 𝒫 𝑥 ∈ V
4544funimaex 6633 . . . . . . . . . . . 12 (Fun 𝐹 → (𝐹 “ 𝒫 𝑥) ∈ V)
4643, 45ax-mp 5 . . . . . . . . . . 11 (𝐹 “ 𝒫 𝑥) ∈ V
4746uniex 7726 . . . . . . . . . 10 (𝐹 “ 𝒫 𝑥) ∈ V
4847inex2 5317 . . . . . . . . 9 (𝐶 (𝐹 “ 𝒫 𝑥)) ∈ V
49 sseq2 4007 . . . . . . . . . . . . 13 (𝑧 = (𝐶 (𝐹 “ 𝒫 𝑥)) → (𝑤𝑧𝑤 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥))))
50 sseq2 4007 . . . . . . . . . . . . 13 (𝑧 = (𝐶 (𝐹 “ 𝒫 𝑥)) → ((𝐹𝑤) ⊆ 𝑧 ↔ (𝐹𝑤) ⊆ (𝐶 (𝐹 “ 𝒫 𝑥))))
5149, 50imbi12d 345 . . . . . . . . . . . 12 (𝑧 = (𝐶 (𝐹 “ 𝒫 𝑥)) → ((𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧) ↔ (𝑤 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)) → (𝐹𝑤) ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)))))
5251imbi2d 341 . . . . . . . . . . 11 (𝑧 = (𝐶 (𝐹 “ 𝒫 𝑥)) → ((𝑤𝑥 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) ↔ (𝑤𝑥 → (𝑤 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)) → (𝐹𝑤) ⊆ (𝐶 (𝐹 “ 𝒫 𝑥))))))
5352albidv 1924 . . . . . . . . . 10 (𝑧 = (𝐶 (𝐹 “ 𝒫 𝑥)) → (∀𝑤(𝑤𝑥 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) ↔ ∀𝑤(𝑤𝑥 → (𝑤 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)) → (𝐹𝑤) ⊆ (𝐶 (𝐹 “ 𝒫 𝑥))))))
54 sseq2 4007 . . . . . . . . . 10 (𝑧 = (𝐶 (𝐹 “ 𝒫 𝑥)) → (𝑥𝑧𝑥 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥))))
5553, 54imbi12d 345 . . . . . . . . 9 (𝑧 = (𝐶 (𝐹 “ 𝒫 𝑥)) → ((∀𝑤(𝑤𝑥 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑥𝑧) ↔ (∀𝑤(𝑤𝑥 → (𝑤 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)) → (𝐹𝑤) ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)))) → 𝑥 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)))))
5648, 55spcv 3595 . . . . . . . 8 (∀𝑧(∀𝑤(𝑤𝑥 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑥𝑧) → (∀𝑤(𝑤𝑥 → (𝑤 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)) → (𝐹𝑤) ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)))) → 𝑥 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥))))
5742, 56mpan9 508 . . . . . . 7 ((𝜑 ∧ ∀𝑧(∀𝑤(𝑤𝑥 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑥𝑧)) → 𝑥 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)))
5857, 9sstrdi 3993 . . . . . 6 ((𝜑 ∧ ∀𝑧(∀𝑤(𝑤𝑥 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑥𝑧)) → 𝑥𝐶)
5958ex 414 . . . . 5 (𝜑 → (∀𝑧(∀𝑤(𝑤𝑥 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑥𝑧) → 𝑥𝐶))
607, 59sylbid 239 . . . 4 (𝜑 → (𝑥 ∈ {𝑦 ∣ ∀𝑧(∀𝑤(𝑤𝑦 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑦𝑧)} → 𝑥𝐶))
6160ralrimiv 3146 . . 3 (𝜑 → ∀𝑥 ∈ {𝑦 ∣ ∀𝑧(∀𝑤(𝑤𝑦 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑦𝑧)}𝑥𝐶)
62 unissb 4942 . . 3 ( {𝑦 ∣ ∀𝑧(∀𝑤(𝑤𝑦 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑦𝑧)} ⊆ 𝐶 ↔ ∀𝑥 ∈ {𝑦 ∣ ∀𝑧(∀𝑤(𝑤𝑦 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑦𝑧)}𝑥𝐶)
6361, 62sylibr 233 . 2 (𝜑 {𝑦 ∣ ∀𝑧(∀𝑤(𝑤𝑦 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑦𝑧)} ⊆ 𝐶)
643, 63eqsstrid 4029 1 (𝜑𝐵𝐶)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 397  w3a 1088  wal 1540   = wceq 1542  wcel 2107  {cab 2710  wnfc 2884  wral 3062  Vcvv 3475  cin 3946  wss 3947  c0 4321  𝒫 cpw 4601   cuni 4907  cima 5678  Fun wfun 6534  cfv 6540  setrecscsetrecs 47630
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7720
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6492  df-fun 6542  df-fv 6548  df-setrecs 47631
This theorem is referenced by:  setrec2  47642
  Copyright terms: Public domain W3C validator