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 45161
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 45160 and setrec2v 45165 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 7553) 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 45153 . . 3 setrecs(𝐹) = {𝑦 ∣ ∀𝑧(∀𝑤(𝑤𝑦 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑦𝑧)}
31, 2eqtri 2845 . 2 𝐵 = {𝑦 ∣ ∀𝑧(∀𝑤(𝑤𝑦 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑦𝑧)}
4 eqid 2822 . . . . . 6 {𝑦 ∣ ∀𝑧(∀𝑤(𝑤𝑦 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑦𝑧)} = {𝑦 ∣ ∀𝑧(∀𝑤(𝑤𝑦 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑦𝑧)}
5 vex 3472 . . . . . . 7 𝑥 ∈ V
65a1i 11 . . . . . 6 (𝜑𝑥 ∈ V)
74, 6setrec1lem1 45156 . . . . 5 (𝜑 → (𝑥 ∈ {𝑦 ∣ ∀𝑧(∀𝑤(𝑤𝑦 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑦𝑧)} ↔ ∀𝑧(∀𝑤(𝑤𝑥 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑥𝑧)))
8 id 22 . . . . . . . . . . . . . . 15 (𝑤 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)) → 𝑤 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)))
9 inss1 4179 . . . . . . . . . . . . . . 15 (𝐶 (𝐹 “ 𝒫 𝑥)) ⊆ 𝐶
108, 9sstrdi 3954 . . . . . . . . . . . . . 14 (𝑤 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)) → 𝑤𝐶)
11 setrec2fun.4 . . . . . . . . . . . . . . 15 (𝜑 → ∀𝑎(𝑎𝐶 → (𝐹𝑎) ⊆ 𝐶))
12 nfv 1915 . . . . . . . . . . . . . . . . 17 𝑎 𝑤𝐶
13 setrec2fun.1 . . . . . . . . . . . . . . . . . . 19 𝑎𝐹
14 nfcv 2979 . . . . . . . . . . . . . . . . . . 19 𝑎𝑤
1513, 14nffv 6662 . . . . . . . . . . . . . . . . . 18 𝑎(𝐹𝑤)
16 nfcv 2979 . . . . . . . . . . . . . . . . . 18 𝑎𝐶
1715, 16nfss 3934 . . . . . . . . . . . . . . . . 17 𝑎(𝐹𝑤) ⊆ 𝐶
1812, 17nfim 1897 . . . . . . . . . . . . . . . 16 𝑎(𝑤𝐶 → (𝐹𝑤) ⊆ 𝐶)
19 sseq1 3967 . . . . . . . . . . . . . . . . . 18 (𝑎 = 𝑤 → (𝑎𝐶𝑤𝐶))
20 fveq2 6652 . . . . . . . . . . . . . . . . . . 19 (𝑎 = 𝑤 → (𝐹𝑎) = (𝐹𝑤))
2120sseq1d 3973 . . . . . . . . . . . . . . . . . 18 (𝑎 = 𝑤 → ((𝐹𝑎) ⊆ 𝐶 ↔ (𝐹𝑤) ⊆ 𝐶))
2219, 21imbi12d 348 . . . . . . . . . . . . . . . . 17 (𝑎 = 𝑤 → ((𝑎𝐶 → (𝐹𝑎) ⊆ 𝐶) ↔ (𝑤𝐶 → (𝐹𝑤) ⊆ 𝐶)))
2322biimpd 232 . . . . . . . . . . . . . . . 16 (𝑎 = 𝑤 → ((𝑎𝐶 → (𝐹𝑎) ⊆ 𝐶) → (𝑤𝐶 → (𝐹𝑤) ⊆ 𝐶)))
2418, 23spimfv 2242 . . . . . . . . . . . . . . 15 (∀𝑎(𝑎𝐶 → (𝐹𝑎) ⊆ 𝐶) → (𝑤𝐶 → (𝐹𝑤) ⊆ 𝐶))
2511, 24syl 17 . . . . . . . . . . . . . 14 (𝜑 → (𝑤𝐶 → (𝐹𝑤) ⊆ 𝐶))
2610, 25syl5 34 . . . . . . . . . . . . 13 (𝜑 → (𝑤 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)) → (𝐹𝑤) ⊆ 𝐶))
2726imp 410 . . . . . . . . . . . 12 ((𝜑𝑤 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥))) → (𝐹𝑤) ⊆ 𝐶)
28273adant2 1128 . . . . . . . . . . 11 ((𝜑𝑤𝑥𝑤 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥))) → (𝐹𝑤) ⊆ 𝐶)
29 velpw 4516 . . . . . . . . . . . . . . 15 (𝑤 ∈ 𝒫 𝑥𝑤𝑥)
30 eliman0 6687 . . . . . . . . . . . . . . . 16 ((𝑤 ∈ 𝒫 𝑥 ∧ ¬ (𝐹𝑤) = ∅) → (𝐹𝑤) ∈ (𝐹 “ 𝒫 𝑥))
3130ex 416 . . . . . . . . . . . . . . 15 (𝑤 ∈ 𝒫 𝑥 → (¬ (𝐹𝑤) = ∅ → (𝐹𝑤) ∈ (𝐹 “ 𝒫 𝑥)))
3229, 31sylbir 238 . . . . . . . . . . . . . 14 (𝑤𝑥 → (¬ (𝐹𝑤) = ∅ → (𝐹𝑤) ∈ (𝐹 “ 𝒫 𝑥)))
33 elssuni 4843 . . . . . . . . . . . . . 14 ((𝐹𝑤) ∈ (𝐹 “ 𝒫 𝑥) → (𝐹𝑤) ⊆ (𝐹 “ 𝒫 𝑥))
3432, 33syl6 35 . . . . . . . . . . . . 13 (𝑤𝑥 → (¬ (𝐹𝑤) = ∅ → (𝐹𝑤) ⊆ (𝐹 “ 𝒫 𝑥)))
35 id 22 . . . . . . . . . . . . . 14 ((𝐹𝑤) = ∅ → (𝐹𝑤) = ∅)
36 0ss 4322 . . . . . . . . . . . . . 14 ∅ ⊆ (𝐹 “ 𝒫 𝑥)
3735, 36eqsstrdi 3996 . . . . . . . . . . . . 13 ((𝐹𝑤) = ∅ → (𝐹𝑤) ⊆ (𝐹 “ 𝒫 𝑥))
3834, 37pm2.61d2 184 . . . . . . . . . . . 12 (𝑤𝑥 → (𝐹𝑤) ⊆ (𝐹 “ 𝒫 𝑥))
39383ad2ant2 1131 . . . . . . . . . . 11 ((𝜑𝑤𝑥𝑤 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥))) → (𝐹𝑤) ⊆ (𝐹 “ 𝒫 𝑥))
4028, 39ssind 4183 . . . . . . . . . 10 ((𝜑𝑤𝑥𝑤 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥))) → (𝐹𝑤) ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)))
41403exp 1116 . . . . . . . . 9 (𝜑 → (𝑤𝑥 → (𝑤 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)) → (𝐹𝑤) ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)))))
4241alrimiv 1928 . . . . . . . 8 (𝜑 → ∀𝑤(𝑤𝑥 → (𝑤 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)) → (𝐹𝑤) ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)))))
43 setrec2fun.3 . . . . . . . . . . . 12 Fun 𝐹
445pwex 5258 . . . . . . . . . . . . 13 𝒫 𝑥 ∈ V
4544funimaex 6420 . . . . . . . . . . . 12 (Fun 𝐹 → (𝐹 “ 𝒫 𝑥) ∈ V)
4643, 45ax-mp 5 . . . . . . . . . . 11 (𝐹 “ 𝒫 𝑥) ∈ V
4746uniex 7452 . . . . . . . . . 10 (𝐹 “ 𝒫 𝑥) ∈ V
4847inex2 5198 . . . . . . . . 9 (𝐶 (𝐹 “ 𝒫 𝑥)) ∈ V
49 sseq2 3968 . . . . . . . . . . . . 13 (𝑧 = (𝐶 (𝐹 “ 𝒫 𝑥)) → (𝑤𝑧𝑤 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥))))
50 sseq2 3968 . . . . . . . . . . . . 13 (𝑧 = (𝐶 (𝐹 “ 𝒫 𝑥)) → ((𝐹𝑤) ⊆ 𝑧 ↔ (𝐹𝑤) ⊆ (𝐶 (𝐹 “ 𝒫 𝑥))))
5149, 50imbi12d 348 . . . . . . . . . . . 12 (𝑧 = (𝐶 (𝐹 “ 𝒫 𝑥)) → ((𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧) ↔ (𝑤 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)) → (𝐹𝑤) ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)))))
5251imbi2d 344 . . . . . . . . . . 11 (𝑧 = (𝐶 (𝐹 “ 𝒫 𝑥)) → ((𝑤𝑥 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) ↔ (𝑤𝑥 → (𝑤 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)) → (𝐹𝑤) ⊆ (𝐶 (𝐹 “ 𝒫 𝑥))))))
5352albidv 1921 . . . . . . . . . 10 (𝑧 = (𝐶 (𝐹 “ 𝒫 𝑥)) → (∀𝑤(𝑤𝑥 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) ↔ ∀𝑤(𝑤𝑥 → (𝑤 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)) → (𝐹𝑤) ⊆ (𝐶 (𝐹 “ 𝒫 𝑥))))))
54 sseq2 3968 . . . . . . . . . 10 (𝑧 = (𝐶 (𝐹 “ 𝒫 𝑥)) → (𝑥𝑧𝑥 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥))))
5553, 54imbi12d 348 . . . . . . . . 9 (𝑧 = (𝐶 (𝐹 “ 𝒫 𝑥)) → ((∀𝑤(𝑤𝑥 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑥𝑧) ↔ (∀𝑤(𝑤𝑥 → (𝑤 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)) → (𝐹𝑤) ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)))) → 𝑥 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)))))
5648, 55spcv 3581 . . . . . . . 8 (∀𝑧(∀𝑤(𝑤𝑥 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑥𝑧) → (∀𝑤(𝑤𝑥 → (𝑤 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)) → (𝐹𝑤) ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)))) → 𝑥 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥))))
5742, 56mpan9 510 . . . . . . 7 ((𝜑 ∧ ∀𝑧(∀𝑤(𝑤𝑥 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑥𝑧)) → 𝑥 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)))
5857, 9sstrdi 3954 . . . . . 6 ((𝜑 ∧ ∀𝑧(∀𝑤(𝑤𝑥 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑥𝑧)) → 𝑥𝐶)
5958ex 416 . . . . 5 (𝜑 → (∀𝑧(∀𝑤(𝑤𝑥 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑥𝑧) → 𝑥𝐶))
607, 59sylbid 243 . . . 4 (𝜑 → (𝑥 ∈ {𝑦 ∣ ∀𝑧(∀𝑤(𝑤𝑦 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑦𝑧)} → 𝑥𝐶))
6160ralrimiv 3173 . . 3 (𝜑 → ∀𝑥 ∈ {𝑦 ∣ ∀𝑧(∀𝑤(𝑤𝑦 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑦𝑧)}𝑥𝐶)
62 unissb 4845 . . 3 ( {𝑦 ∣ ∀𝑧(∀𝑤(𝑤𝑦 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑦𝑧)} ⊆ 𝐶 ↔ ∀𝑥 ∈ {𝑦 ∣ ∀𝑧(∀𝑤(𝑤𝑦 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑦𝑧)}𝑥𝐶)
6361, 62sylibr 237 . 2 (𝜑 {𝑦 ∣ ∀𝑧(∀𝑤(𝑤𝑦 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑦𝑧)} ⊆ 𝐶)
643, 63eqsstrid 3990 1 (𝜑𝐵𝐶)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 399  w3a 1084  wal 1536   = wceq 1538  wcel 2114  {cab 2800  wnfc 2960  wral 3130  Vcvv 3469  cin 3907  wss 3908  c0 4265  𝒫 cpw 4511   cuni 4813  cima 5535  Fun wfun 6328  cfv 6334  setrecscsetrecs 45152
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2178  ax-ext 2794  ax-rep 5166  ax-sep 5179  ax-nul 5186  ax-pow 5243  ax-pr 5307  ax-un 7446
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2801  df-cleq 2815  df-clel 2894  df-nfc 2962  df-ne 3012  df-ral 3135  df-rex 3136  df-rab 3139  df-v 3471  df-sbc 3748  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4266  df-if 4440  df-pw 4513  df-sn 4540  df-pr 4542  df-op 4546  df-uni 4814  df-br 5043  df-opab 5105  df-id 5437  df-xp 5538  df-cnv 5540  df-co 5541  df-dm 5542  df-rn 5543  df-res 5544  df-ima 5545  df-iota 6293  df-fun 6336  df-fv 6342  df-setrecs 45153
This theorem is referenced by:  setrec2  45164
  Copyright terms: Public domain W3C validator