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 44723
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 44722 and setrec2v 44727 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 7557) 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 44715 . . 3 setrecs(𝐹) = {𝑦 ∣ ∀𝑧(∀𝑤(𝑤𝑦 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑦𝑧)}
31, 2eqtri 2841 . 2 𝐵 = {𝑦 ∣ ∀𝑧(∀𝑤(𝑤𝑦 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑦𝑧)}
4 eqid 2818 . . . . . 6 {𝑦 ∣ ∀𝑧(∀𝑤(𝑤𝑦 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑦𝑧)} = {𝑦 ∣ ∀𝑧(∀𝑤(𝑤𝑦 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑦𝑧)}
5 vex 3495 . . . . . . 7 𝑥 ∈ V
65a1i 11 . . . . . 6 (𝜑𝑥 ∈ V)
74, 6setrec1lem1 44718 . . . . 5 (𝜑 → (𝑥 ∈ {𝑦 ∣ ∀𝑧(∀𝑤(𝑤𝑦 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑦𝑧)} ↔ ∀𝑧(∀𝑤(𝑤𝑥 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑥𝑧)))
8 id 22 . . . . . . . . . . . . . . 15 (𝑤 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)) → 𝑤 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)))
9 inss1 4202 . . . . . . . . . . . . . . 15 (𝐶 (𝐹 “ 𝒫 𝑥)) ⊆ 𝐶
108, 9sstrdi 3976 . . . . . . . . . . . . . 14 (𝑤 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)) → 𝑤𝐶)
11 setrec2fun.4 . . . . . . . . . . . . . . 15 (𝜑 → ∀𝑎(𝑎𝐶 → (𝐹𝑎) ⊆ 𝐶))
12 nfv 1906 . . . . . . . . . . . . . . . . 17 𝑎 𝑤𝐶
13 setrec2fun.1 . . . . . . . . . . . . . . . . . . 19 𝑎𝐹
14 nfcv 2974 . . . . . . . . . . . . . . . . . . 19 𝑎𝑤
1513, 14nffv 6673 . . . . . . . . . . . . . . . . . 18 𝑎(𝐹𝑤)
16 nfcv 2974 . . . . . . . . . . . . . . . . . 18 𝑎𝐶
1715, 16nfss 3957 . . . . . . . . . . . . . . . . 17 𝑎(𝐹𝑤) ⊆ 𝐶
1812, 17nfim 1888 . . . . . . . . . . . . . . . 16 𝑎(𝑤𝐶 → (𝐹𝑤) ⊆ 𝐶)
19 sseq1 3989 . . . . . . . . . . . . . . . . . 18 (𝑎 = 𝑤 → (𝑎𝐶𝑤𝐶))
20 fveq2 6663 . . . . . . . . . . . . . . . . . . 19 (𝑎 = 𝑤 → (𝐹𝑎) = (𝐹𝑤))
2120sseq1d 3995 . . . . . . . . . . . . . . . . . 18 (𝑎 = 𝑤 → ((𝐹𝑎) ⊆ 𝐶 ↔ (𝐹𝑤) ⊆ 𝐶))
2219, 21imbi12d 346 . . . . . . . . . . . . . . . . 17 (𝑎 = 𝑤 → ((𝑎𝐶 → (𝐹𝑎) ⊆ 𝐶) ↔ (𝑤𝐶 → (𝐹𝑤) ⊆ 𝐶)))
2322biimpd 230 . . . . . . . . . . . . . . . 16 (𝑎 = 𝑤 → ((𝑎𝐶 → (𝐹𝑎) ⊆ 𝐶) → (𝑤𝐶 → (𝐹𝑤) ⊆ 𝐶)))
2418, 23spimfv 2231 . . . . . . . . . . . . . . 15 (∀𝑎(𝑎𝐶 → (𝐹𝑎) ⊆ 𝐶) → (𝑤𝐶 → (𝐹𝑤) ⊆ 𝐶))
2511, 24syl 17 . . . . . . . . . . . . . 14 (𝜑 → (𝑤𝐶 → (𝐹𝑤) ⊆ 𝐶))
2610, 25syl5 34 . . . . . . . . . . . . 13 (𝜑 → (𝑤 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)) → (𝐹𝑤) ⊆ 𝐶))
2726imp 407 . . . . . . . . . . . 12 ((𝜑𝑤 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥))) → (𝐹𝑤) ⊆ 𝐶)
28273adant2 1123 . . . . . . . . . . 11 ((𝜑𝑤𝑥𝑤 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥))) → (𝐹𝑤) ⊆ 𝐶)
29 velpw 4543 . . . . . . . . . . . . . . 15 (𝑤 ∈ 𝒫 𝑥𝑤𝑥)
30 eliman0 6698 . . . . . . . . . . . . . . . 16 ((𝑤 ∈ 𝒫 𝑥 ∧ ¬ (𝐹𝑤) = ∅) → (𝐹𝑤) ∈ (𝐹 “ 𝒫 𝑥))
3130ex 413 . . . . . . . . . . . . . . 15 (𝑤 ∈ 𝒫 𝑥 → (¬ (𝐹𝑤) = ∅ → (𝐹𝑤) ∈ (𝐹 “ 𝒫 𝑥)))
3229, 31sylbir 236 . . . . . . . . . . . . . 14 (𝑤𝑥 → (¬ (𝐹𝑤) = ∅ → (𝐹𝑤) ∈ (𝐹 “ 𝒫 𝑥)))
33 elssuni 4859 . . . . . . . . . . . . . 14 ((𝐹𝑤) ∈ (𝐹 “ 𝒫 𝑥) → (𝐹𝑤) ⊆ (𝐹 “ 𝒫 𝑥))
3432, 33syl6 35 . . . . . . . . . . . . 13 (𝑤𝑥 → (¬ (𝐹𝑤) = ∅ → (𝐹𝑤) ⊆ (𝐹 “ 𝒫 𝑥)))
35 id 22 . . . . . . . . . . . . . 14 ((𝐹𝑤) = ∅ → (𝐹𝑤) = ∅)
36 0ss 4347 . . . . . . . . . . . . . 14 ∅ ⊆ (𝐹 “ 𝒫 𝑥)
3735, 36eqsstrdi 4018 . . . . . . . . . . . . 13 ((𝐹𝑤) = ∅ → (𝐹𝑤) ⊆ (𝐹 “ 𝒫 𝑥))
3834, 37pm2.61d2 182 . . . . . . . . . . . 12 (𝑤𝑥 → (𝐹𝑤) ⊆ (𝐹 “ 𝒫 𝑥))
39383ad2ant2 1126 . . . . . . . . . . 11 ((𝜑𝑤𝑥𝑤 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥))) → (𝐹𝑤) ⊆ (𝐹 “ 𝒫 𝑥))
4028, 39ssind 4206 . . . . . . . . . 10 ((𝜑𝑤𝑥𝑤 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥))) → (𝐹𝑤) ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)))
41403exp 1111 . . . . . . . . 9 (𝜑 → (𝑤𝑥 → (𝑤 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)) → (𝐹𝑤) ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)))))
4241alrimiv 1919 . . . . . . . 8 (𝜑 → ∀𝑤(𝑤𝑥 → (𝑤 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)) → (𝐹𝑤) ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)))))
43 setrec2fun.3 . . . . . . . . . . . 12 Fun 𝐹
445pwex 5272 . . . . . . . . . . . . 13 𝒫 𝑥 ∈ V
4544funimaex 6434 . . . . . . . . . . . 12 (Fun 𝐹 → (𝐹 “ 𝒫 𝑥) ∈ V)
4643, 45ax-mp 5 . . . . . . . . . . 11 (𝐹 “ 𝒫 𝑥) ∈ V
4746uniex 7454 . . . . . . . . . 10 (𝐹 “ 𝒫 𝑥) ∈ V
4847inex2 5213 . . . . . . . . 9 (𝐶 (𝐹 “ 𝒫 𝑥)) ∈ V
49 sseq2 3990 . . . . . . . . . . . . 13 (𝑧 = (𝐶 (𝐹 “ 𝒫 𝑥)) → (𝑤𝑧𝑤 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥))))
50 sseq2 3990 . . . . . . . . . . . . 13 (𝑧 = (𝐶 (𝐹 “ 𝒫 𝑥)) → ((𝐹𝑤) ⊆ 𝑧 ↔ (𝐹𝑤) ⊆ (𝐶 (𝐹 “ 𝒫 𝑥))))
5149, 50imbi12d 346 . . . . . . . . . . . 12 (𝑧 = (𝐶 (𝐹 “ 𝒫 𝑥)) → ((𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧) ↔ (𝑤 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)) → (𝐹𝑤) ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)))))
5251imbi2d 342 . . . . . . . . . . 11 (𝑧 = (𝐶 (𝐹 “ 𝒫 𝑥)) → ((𝑤𝑥 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) ↔ (𝑤𝑥 → (𝑤 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)) → (𝐹𝑤) ⊆ (𝐶 (𝐹 “ 𝒫 𝑥))))))
5352albidv 1912 . . . . . . . . . 10 (𝑧 = (𝐶 (𝐹 “ 𝒫 𝑥)) → (∀𝑤(𝑤𝑥 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) ↔ ∀𝑤(𝑤𝑥 → (𝑤 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)) → (𝐹𝑤) ⊆ (𝐶 (𝐹 “ 𝒫 𝑥))))))
54 sseq2 3990 . . . . . . . . . 10 (𝑧 = (𝐶 (𝐹 “ 𝒫 𝑥)) → (𝑥𝑧𝑥 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥))))
5553, 54imbi12d 346 . . . . . . . . 9 (𝑧 = (𝐶 (𝐹 “ 𝒫 𝑥)) → ((∀𝑤(𝑤𝑥 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑥𝑧) ↔ (∀𝑤(𝑤𝑥 → (𝑤 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)) → (𝐹𝑤) ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)))) → 𝑥 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)))))
5648, 55spcv 3603 . . . . . . . 8 (∀𝑧(∀𝑤(𝑤𝑥 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑥𝑧) → (∀𝑤(𝑤𝑥 → (𝑤 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)) → (𝐹𝑤) ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)))) → 𝑥 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥))))
5742, 56mpan9 507 . . . . . . 7 ((𝜑 ∧ ∀𝑧(∀𝑤(𝑤𝑥 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑥𝑧)) → 𝑥 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)))
5857, 9sstrdi 3976 . . . . . 6 ((𝜑 ∧ ∀𝑧(∀𝑤(𝑤𝑥 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑥𝑧)) → 𝑥𝐶)
5958ex 413 . . . . 5 (𝜑 → (∀𝑧(∀𝑤(𝑤𝑥 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑥𝑧) → 𝑥𝐶))
607, 59sylbid 241 . . . 4 (𝜑 → (𝑥 ∈ {𝑦 ∣ ∀𝑧(∀𝑤(𝑤𝑦 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑦𝑧)} → 𝑥𝐶))
6160ralrimiv 3178 . . 3 (𝜑 → ∀𝑥 ∈ {𝑦 ∣ ∀𝑧(∀𝑤(𝑤𝑦 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑦𝑧)}𝑥𝐶)
62 unissb 4861 . . 3 ( {𝑦 ∣ ∀𝑧(∀𝑤(𝑤𝑦 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑦𝑧)} ⊆ 𝐶 ↔ ∀𝑥 ∈ {𝑦 ∣ ∀𝑧(∀𝑤(𝑤𝑦 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑦𝑧)}𝑥𝐶)
6361, 62sylibr 235 . 2 (𝜑 {𝑦 ∣ ∀𝑧(∀𝑤(𝑤𝑦 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑦𝑧)} ⊆ 𝐶)
643, 63eqsstrid 4012 1 (𝜑𝐵𝐶)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396  w3a 1079  wal 1526   = wceq 1528  wcel 2105  {cab 2796  wnfc 2958  wral 3135  Vcvv 3492  cin 3932  wss 3933  c0 4288  𝒫 cpw 4535   cuni 4830  cima 5551  Fun wfun 6342  cfv 6348  setrecscsetrecs 44714
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-rep 5181  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-ral 3140  df-rex 3141  df-rab 3144  df-v 3494  df-sbc 3770  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4831  df-br 5058  df-opab 5120  df-id 5453  df-xp 5554  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-iota 6307  df-fun 6350  df-fv 6356  df-setrecs 44715
This theorem is referenced by:  setrec2  44726
  Copyright terms: Public domain W3C validator