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

Theorem setrec2fun 41729
 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 41728 and setrec2v 41733 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 7000) 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 41721 . . 3 setrecs(𝐹) = {𝑦 ∣ ∀𝑧(∀𝑤(𝑤𝑦 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑦𝑧)}
31, 2eqtri 2643 . 2 𝐵 = {𝑦 ∣ ∀𝑧(∀𝑤(𝑤𝑦 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑦𝑧)}
4 eqid 2621 . . . . . 6 {𝑦 ∣ ∀𝑧(∀𝑤(𝑤𝑦 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑦𝑧)} = {𝑦 ∣ ∀𝑧(∀𝑤(𝑤𝑦 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑦𝑧)}
5 vex 3189 . . . . . . 7 𝑥 ∈ V
65a1i 11 . . . . . 6 (𝜑𝑥 ∈ V)
74, 6setrec1lem1 41724 . . . . 5 (𝜑 → (𝑥 ∈ {𝑦 ∣ ∀𝑧(∀𝑤(𝑤𝑦 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑦𝑧)} ↔ ∀𝑧(∀𝑤(𝑤𝑥 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑥𝑧)))
8 id 22 . . . . . . . . . . . . . . 15 (𝑤 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)) → 𝑤 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)))
9 inss1 3811 . . . . . . . . . . . . . . 15 (𝐶 (𝐹 “ 𝒫 𝑥)) ⊆ 𝐶
108, 9syl6ss 3595 . . . . . . . . . . . . . 14 (𝑤 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)) → 𝑤𝐶)
11 setrec2fun.4 . . . . . . . . . . . . . . 15 (𝜑 → ∀𝑎(𝑎𝐶 → (𝐹𝑎) ⊆ 𝐶))
12 nfv 1840 . . . . . . . . . . . . . . . . 17 𝑎 𝑤𝐶
13 setrec2fun.1 . . . . . . . . . . . . . . . . . . 19 𝑎𝐹
14 nfcv 2761 . . . . . . . . . . . . . . . . . . 19 𝑎𝑤
1513, 14nffv 6155 . . . . . . . . . . . . . . . . . 18 𝑎(𝐹𝑤)
16 nfcv 2761 . . . . . . . . . . . . . . . . . 18 𝑎𝐶
1715, 16nfss 3576 . . . . . . . . . . . . . . . . 17 𝑎(𝐹𝑤) ⊆ 𝐶
1812, 17nfim 1822 . . . . . . . . . . . . . . . 16 𝑎(𝑤𝐶 → (𝐹𝑤) ⊆ 𝐶)
19 sseq1 3605 . . . . . . . . . . . . . . . . . 18 (𝑎 = 𝑤 → (𝑎𝐶𝑤𝐶))
20 fveq2 6148 . . . . . . . . . . . . . . . . . . 19 (𝑎 = 𝑤 → (𝐹𝑎) = (𝐹𝑤))
2120sseq1d 3611 . . . . . . . . . . . . . . . . . 18 (𝑎 = 𝑤 → ((𝐹𝑎) ⊆ 𝐶 ↔ (𝐹𝑤) ⊆ 𝐶))
2219, 21imbi12d 334 . . . . . . . . . . . . . . . . 17 (𝑎 = 𝑤 → ((𝑎𝐶 → (𝐹𝑎) ⊆ 𝐶) ↔ (𝑤𝐶 → (𝐹𝑤) ⊆ 𝐶)))
2322biimpd 219 . . . . . . . . . . . . . . . 16 (𝑎 = 𝑤 → ((𝑎𝐶 → (𝐹𝑎) ⊆ 𝐶) → (𝑤𝐶 → (𝐹𝑤) ⊆ 𝐶)))
2418, 23spim 2253 . . . . . . . . . . . . . . 15 (∀𝑎(𝑎𝐶 → (𝐹𝑎) ⊆ 𝐶) → (𝑤𝐶 → (𝐹𝑤) ⊆ 𝐶))
2511, 24syl 17 . . . . . . . . . . . . . 14 (𝜑 → (𝑤𝐶 → (𝐹𝑤) ⊆ 𝐶))
2610, 25syl5 34 . . . . . . . . . . . . 13 (𝜑 → (𝑤 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)) → (𝐹𝑤) ⊆ 𝐶))
2726imp 445 . . . . . . . . . . . 12 ((𝜑𝑤 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥))) → (𝐹𝑤) ⊆ 𝐶)
28273adant2 1078 . . . . . . . . . . 11 ((𝜑𝑤𝑥𝑤 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥))) → (𝐹𝑤) ⊆ 𝐶)
29 selpw 4137 . . . . . . . . . . . . . . 15 (𝑤 ∈ 𝒫 𝑥𝑤𝑥)
30 eliman0 6180 . . . . . . . . . . . . . . . 16 ((𝑤 ∈ 𝒫 𝑥 ∧ ¬ (𝐹𝑤) = ∅) → (𝐹𝑤) ∈ (𝐹 “ 𝒫 𝑥))
3130ex 450 . . . . . . . . . . . . . . 15 (𝑤 ∈ 𝒫 𝑥 → (¬ (𝐹𝑤) = ∅ → (𝐹𝑤) ∈ (𝐹 “ 𝒫 𝑥)))
3229, 31sylbir 225 . . . . . . . . . . . . . 14 (𝑤𝑥 → (¬ (𝐹𝑤) = ∅ → (𝐹𝑤) ∈ (𝐹 “ 𝒫 𝑥)))
33 elssuni 4433 . . . . . . . . . . . . . 14 ((𝐹𝑤) ∈ (𝐹 “ 𝒫 𝑥) → (𝐹𝑤) ⊆ (𝐹 “ 𝒫 𝑥))
3432, 33syl6 35 . . . . . . . . . . . . 13 (𝑤𝑥 → (¬ (𝐹𝑤) = ∅ → (𝐹𝑤) ⊆ (𝐹 “ 𝒫 𝑥)))
35 id 22 . . . . . . . . . . . . . 14 ((𝐹𝑤) = ∅ → (𝐹𝑤) = ∅)
36 0ss 3944 . . . . . . . . . . . . . 14 ∅ ⊆ (𝐹 “ 𝒫 𝑥)
3735, 36syl6eqss 3634 . . . . . . . . . . . . 13 ((𝐹𝑤) = ∅ → (𝐹𝑤) ⊆ (𝐹 “ 𝒫 𝑥))
3834, 37pm2.61d2 172 . . . . . . . . . . . 12 (𝑤𝑥 → (𝐹𝑤) ⊆ (𝐹 “ 𝒫 𝑥))
39383ad2ant2 1081 . . . . . . . . . . 11 ((𝜑𝑤𝑥𝑤 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥))) → (𝐹𝑤) ⊆ (𝐹 “ 𝒫 𝑥))
4028, 39ssind 3815 . . . . . . . . . 10 ((𝜑𝑤𝑥𝑤 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥))) → (𝐹𝑤) ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)))
41403exp 1261 . . . . . . . . 9 (𝜑 → (𝑤𝑥 → (𝑤 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)) → (𝐹𝑤) ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)))))
4241alrimiv 1852 . . . . . . . 8 (𝜑 → ∀𝑤(𝑤𝑥 → (𝑤 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)) → (𝐹𝑤) ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)))))
43 setrec2fun.3 . . . . . . . . . . . 12 Fun 𝐹
445pwex 4808 . . . . . . . . . . . . 13 𝒫 𝑥 ∈ V
4544funimaex 5934 . . . . . . . . . . . 12 (Fun 𝐹 → (𝐹 “ 𝒫 𝑥) ∈ V)
4643, 45ax-mp 5 . . . . . . . . . . 11 (𝐹 “ 𝒫 𝑥) ∈ V
4746uniex 6906 . . . . . . . . . 10 (𝐹 “ 𝒫 𝑥) ∈ V
4847inex2 4760 . . . . . . . . 9 (𝐶 (𝐹 “ 𝒫 𝑥)) ∈ V
49 sseq2 3606 . . . . . . . . . . . . 13 (𝑧 = (𝐶 (𝐹 “ 𝒫 𝑥)) → (𝑤𝑧𝑤 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥))))
50 sseq2 3606 . . . . . . . . . . . . 13 (𝑧 = (𝐶 (𝐹 “ 𝒫 𝑥)) → ((𝐹𝑤) ⊆ 𝑧 ↔ (𝐹𝑤) ⊆ (𝐶 (𝐹 “ 𝒫 𝑥))))
5149, 50imbi12d 334 . . . . . . . . . . . 12 (𝑧 = (𝐶 (𝐹 “ 𝒫 𝑥)) → ((𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧) ↔ (𝑤 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)) → (𝐹𝑤) ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)))))
5251imbi2d 330 . . . . . . . . . . 11 (𝑧 = (𝐶 (𝐹 “ 𝒫 𝑥)) → ((𝑤𝑥 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) ↔ (𝑤𝑥 → (𝑤 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)) → (𝐹𝑤) ⊆ (𝐶 (𝐹 “ 𝒫 𝑥))))))
5352albidv 1846 . . . . . . . . . 10 (𝑧 = (𝐶 (𝐹 “ 𝒫 𝑥)) → (∀𝑤(𝑤𝑥 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) ↔ ∀𝑤(𝑤𝑥 → (𝑤 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)) → (𝐹𝑤) ⊆ (𝐶 (𝐹 “ 𝒫 𝑥))))))
54 sseq2 3606 . . . . . . . . . 10 (𝑧 = (𝐶 (𝐹 “ 𝒫 𝑥)) → (𝑥𝑧𝑥 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥))))
5553, 54imbi12d 334 . . . . . . . . 9 (𝑧 = (𝐶 (𝐹 “ 𝒫 𝑥)) → ((∀𝑤(𝑤𝑥 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑥𝑧) ↔ (∀𝑤(𝑤𝑥 → (𝑤 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)) → (𝐹𝑤) ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)))) → 𝑥 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)))))
5648, 55spcv 3285 . . . . . . . 8 (∀𝑧(∀𝑤(𝑤𝑥 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑥𝑧) → (∀𝑤(𝑤𝑥 → (𝑤 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)) → (𝐹𝑤) ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)))) → 𝑥 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥))))
5742, 56mpan9 486 . . . . . . 7 ((𝜑 ∧ ∀𝑧(∀𝑤(𝑤𝑥 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑥𝑧)) → 𝑥 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)))
5857, 9syl6ss 3595 . . . . . 6 ((𝜑 ∧ ∀𝑧(∀𝑤(𝑤𝑥 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑥𝑧)) → 𝑥𝐶)
5958ex 450 . . . . 5 (𝜑 → (∀𝑧(∀𝑤(𝑤𝑥 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑥𝑧) → 𝑥𝐶))
607, 59sylbid 230 . . . 4 (𝜑 → (𝑥 ∈ {𝑦 ∣ ∀𝑧(∀𝑤(𝑤𝑦 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑦𝑧)} → 𝑥𝐶))
6160ralrimiv 2959 . . 3 (𝜑 → ∀𝑥 ∈ {𝑦 ∣ ∀𝑧(∀𝑤(𝑤𝑦 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑦𝑧)}𝑥𝐶)
62 unissb 4435 . . 3 ( {𝑦 ∣ ∀𝑧(∀𝑤(𝑤𝑦 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑦𝑧)} ⊆ 𝐶 ↔ ∀𝑥 ∈ {𝑦 ∣ ∀𝑧(∀𝑤(𝑤𝑦 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑦𝑧)}𝑥𝐶)
6361, 62sylibr 224 . 2 (𝜑 {𝑦 ∣ ∀𝑧(∀𝑤(𝑤𝑦 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑦𝑧)} ⊆ 𝐶)
643, 63syl5eqss 3628 1 (𝜑𝐵𝐶)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 384   ∧ w3a 1036  ∀wal 1478   = wceq 1480   ∈ wcel 1987  {cab 2607  Ⅎwnfc 2748  ∀wral 2907  Vcvv 3186   ∩ cin 3554   ⊆ wss 3555  ∅c0 3891  𝒫 cpw 4130  ∪ cuni 4402   “ cima 5077  Fun wfun 5841  ‘cfv 5847  setrecscsetrecs 41720 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4731  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867  ax-un 6902 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3188  df-sbc 3418  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-nul 3892  df-if 4059  df-pw 4132  df-sn 4149  df-pr 4151  df-op 4155  df-uni 4403  df-br 4614  df-opab 4674  df-id 4989  df-xp 5080  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087  df-iota 5810  df-fun 5849  df-fv 5855  df-setrecs 41721 This theorem is referenced by:  setrec2  41732
 Copyright terms: Public domain W3C validator