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 47127
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 47126 and setrec2v 47131 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 7789) 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 47119 . . 3 setrecs(𝐹) = {𝑦 ∣ ∀𝑧(∀𝑤(𝑤𝑦 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑦𝑧)}
31, 2eqtri 2764 . 2 𝐵 = {𝑦 ∣ ∀𝑧(∀𝑤(𝑤𝑦 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑦𝑧)}
4 eqid 2736 . . . . . 6 {𝑦 ∣ ∀𝑧(∀𝑤(𝑤𝑦 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑦𝑧)} = {𝑦 ∣ ∀𝑧(∀𝑤(𝑤𝑦 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑦𝑧)}
5 vex 3449 . . . . . . 7 𝑥 ∈ V
65a1i 11 . . . . . 6 (𝜑𝑥 ∈ V)
74, 6setrec1lem1 47122 . . . . 5 (𝜑 → (𝑥 ∈ {𝑦 ∣ ∀𝑧(∀𝑤(𝑤𝑦 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑦𝑧)} ↔ ∀𝑧(∀𝑤(𝑤𝑥 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑥𝑧)))
8 id 22 . . . . . . . . . . . . . . 15 (𝑤 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)) → 𝑤 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)))
9 inss1 4188 . . . . . . . . . . . . . . 15 (𝐶 (𝐹 “ 𝒫 𝑥)) ⊆ 𝐶
108, 9sstrdi 3956 . . . . . . . . . . . . . 14 (𝑤 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)) → 𝑤𝐶)
11 setrec2fun.4 . . . . . . . . . . . . . . 15 (𝜑 → ∀𝑎(𝑎𝐶 → (𝐹𝑎) ⊆ 𝐶))
12 nfv 1917 . . . . . . . . . . . . . . . . 17 𝑎 𝑤𝐶
13 setrec2fun.1 . . . . . . . . . . . . . . . . . . 19 𝑎𝐹
14 nfcv 2907 . . . . . . . . . . . . . . . . . . 19 𝑎𝑤
1513, 14nffv 6852 . . . . . . . . . . . . . . . . . 18 𝑎(𝐹𝑤)
16 nfcv 2907 . . . . . . . . . . . . . . . . . 18 𝑎𝐶
1715, 16nfss 3936 . . . . . . . . . . . . . . . . 17 𝑎(𝐹𝑤) ⊆ 𝐶
1812, 17nfim 1899 . . . . . . . . . . . . . . . 16 𝑎(𝑤𝐶 → (𝐹𝑤) ⊆ 𝐶)
19 sseq1 3969 . . . . . . . . . . . . . . . . . 18 (𝑎 = 𝑤 → (𝑎𝐶𝑤𝐶))
20 fveq2 6842 . . . . . . . . . . . . . . . . . . 19 (𝑎 = 𝑤 → (𝐹𝑎) = (𝐹𝑤))
2120sseq1d 3975 . . . . . . . . . . . . . . . . . 18 (𝑎 = 𝑤 → ((𝐹𝑎) ⊆ 𝐶 ↔ (𝐹𝑤) ⊆ 𝐶))
2219, 21imbi12d 344 . . . . . . . . . . . . . . . . 17 (𝑎 = 𝑤 → ((𝑎𝐶 → (𝐹𝑎) ⊆ 𝐶) ↔ (𝑤𝐶 → (𝐹𝑤) ⊆ 𝐶)))
2322biimpd 228 . . . . . . . . . . . . . . . 16 (𝑎 = 𝑤 → ((𝑎𝐶 → (𝐹𝑎) ⊆ 𝐶) → (𝑤𝐶 → (𝐹𝑤) ⊆ 𝐶)))
2418, 23spimfv 2232 . . . . . . . . . . . . . . 15 (∀𝑎(𝑎𝐶 → (𝐹𝑎) ⊆ 𝐶) → (𝑤𝐶 → (𝐹𝑤) ⊆ 𝐶))
2511, 24syl 17 . . . . . . . . . . . . . 14 (𝜑 → (𝑤𝐶 → (𝐹𝑤) ⊆ 𝐶))
2610, 25syl5 34 . . . . . . . . . . . . 13 (𝜑 → (𝑤 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)) → (𝐹𝑤) ⊆ 𝐶))
2726imp 407 . . . . . . . . . . . 12 ((𝜑𝑤 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥))) → (𝐹𝑤) ⊆ 𝐶)
28273adant2 1131 . . . . . . . . . . 11 ((𝜑𝑤𝑥𝑤 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥))) → (𝐹𝑤) ⊆ 𝐶)
29 velpw 4565 . . . . . . . . . . . . . . 15 (𝑤 ∈ 𝒫 𝑥𝑤𝑥)
30 eliman0 6882 . . . . . . . . . . . . . . . 16 ((𝑤 ∈ 𝒫 𝑥 ∧ ¬ (𝐹𝑤) = ∅) → (𝐹𝑤) ∈ (𝐹 “ 𝒫 𝑥))
3130ex 413 . . . . . . . . . . . . . . 15 (𝑤 ∈ 𝒫 𝑥 → (¬ (𝐹𝑤) = ∅ → (𝐹𝑤) ∈ (𝐹 “ 𝒫 𝑥)))
3229, 31sylbir 234 . . . . . . . . . . . . . 14 (𝑤𝑥 → (¬ (𝐹𝑤) = ∅ → (𝐹𝑤) ∈ (𝐹 “ 𝒫 𝑥)))
33 elssuni 4898 . . . . . . . . . . . . . 14 ((𝐹𝑤) ∈ (𝐹 “ 𝒫 𝑥) → (𝐹𝑤) ⊆ (𝐹 “ 𝒫 𝑥))
3432, 33syl6 35 . . . . . . . . . . . . 13 (𝑤𝑥 → (¬ (𝐹𝑤) = ∅ → (𝐹𝑤) ⊆ (𝐹 “ 𝒫 𝑥)))
35 id 22 . . . . . . . . . . . . . 14 ((𝐹𝑤) = ∅ → (𝐹𝑤) = ∅)
36 0ss 4356 . . . . . . . . . . . . . 14 ∅ ⊆ (𝐹 “ 𝒫 𝑥)
3735, 36eqsstrdi 3998 . . . . . . . . . . . . 13 ((𝐹𝑤) = ∅ → (𝐹𝑤) ⊆ (𝐹 “ 𝒫 𝑥))
3834, 37pm2.61d2 181 . . . . . . . . . . . 12 (𝑤𝑥 → (𝐹𝑤) ⊆ (𝐹 “ 𝒫 𝑥))
39383ad2ant2 1134 . . . . . . . . . . 11 ((𝜑𝑤𝑥𝑤 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥))) → (𝐹𝑤) ⊆ (𝐹 “ 𝒫 𝑥))
4028, 39ssind 4192 . . . . . . . . . 10 ((𝜑𝑤𝑥𝑤 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥))) → (𝐹𝑤) ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)))
41403exp 1119 . . . . . . . . 9 (𝜑 → (𝑤𝑥 → (𝑤 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)) → (𝐹𝑤) ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)))))
4241alrimiv 1930 . . . . . . . 8 (𝜑 → ∀𝑤(𝑤𝑥 → (𝑤 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)) → (𝐹𝑤) ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)))))
43 setrec2fun.3 . . . . . . . . . . . 12 Fun 𝐹
445pwex 5335 . . . . . . . . . . . . 13 𝒫 𝑥 ∈ V
4544funimaex 6589 . . . . . . . . . . . 12 (Fun 𝐹 → (𝐹 “ 𝒫 𝑥) ∈ V)
4643, 45ax-mp 5 . . . . . . . . . . 11 (𝐹 “ 𝒫 𝑥) ∈ V
4746uniex 7678 . . . . . . . . . 10 (𝐹 “ 𝒫 𝑥) ∈ V
4847inex2 5275 . . . . . . . . 9 (𝐶 (𝐹 “ 𝒫 𝑥)) ∈ V
49 sseq2 3970 . . . . . . . . . . . . 13 (𝑧 = (𝐶 (𝐹 “ 𝒫 𝑥)) → (𝑤𝑧𝑤 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥))))
50 sseq2 3970 . . . . . . . . . . . . 13 (𝑧 = (𝐶 (𝐹 “ 𝒫 𝑥)) → ((𝐹𝑤) ⊆ 𝑧 ↔ (𝐹𝑤) ⊆ (𝐶 (𝐹 “ 𝒫 𝑥))))
5149, 50imbi12d 344 . . . . . . . . . . . 12 (𝑧 = (𝐶 (𝐹 “ 𝒫 𝑥)) → ((𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧) ↔ (𝑤 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)) → (𝐹𝑤) ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)))))
5251imbi2d 340 . . . . . . . . . . 11 (𝑧 = (𝐶 (𝐹 “ 𝒫 𝑥)) → ((𝑤𝑥 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) ↔ (𝑤𝑥 → (𝑤 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)) → (𝐹𝑤) ⊆ (𝐶 (𝐹 “ 𝒫 𝑥))))))
5352albidv 1923 . . . . . . . . . 10 (𝑧 = (𝐶 (𝐹 “ 𝒫 𝑥)) → (∀𝑤(𝑤𝑥 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) ↔ ∀𝑤(𝑤𝑥 → (𝑤 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)) → (𝐹𝑤) ⊆ (𝐶 (𝐹 “ 𝒫 𝑥))))))
54 sseq2 3970 . . . . . . . . . 10 (𝑧 = (𝐶 (𝐹 “ 𝒫 𝑥)) → (𝑥𝑧𝑥 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥))))
5553, 54imbi12d 344 . . . . . . . . 9 (𝑧 = (𝐶 (𝐹 “ 𝒫 𝑥)) → ((∀𝑤(𝑤𝑥 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑥𝑧) ↔ (∀𝑤(𝑤𝑥 → (𝑤 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)) → (𝐹𝑤) ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)))) → 𝑥 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)))))
5648, 55spcv 3564 . . . . . . . 8 (∀𝑧(∀𝑤(𝑤𝑥 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑥𝑧) → (∀𝑤(𝑤𝑥 → (𝑤 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)) → (𝐹𝑤) ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)))) → 𝑥 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥))))
5742, 56mpan9 507 . . . . . . 7 ((𝜑 ∧ ∀𝑧(∀𝑤(𝑤𝑥 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑥𝑧)) → 𝑥 ⊆ (𝐶 (𝐹 “ 𝒫 𝑥)))
5857, 9sstrdi 3956 . . . . . 6 ((𝜑 ∧ ∀𝑧(∀𝑤(𝑤𝑥 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑥𝑧)) → 𝑥𝐶)
5958ex 413 . . . . 5 (𝜑 → (∀𝑧(∀𝑤(𝑤𝑥 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑥𝑧) → 𝑥𝐶))
607, 59sylbid 239 . . . 4 (𝜑 → (𝑥 ∈ {𝑦 ∣ ∀𝑧(∀𝑤(𝑤𝑦 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑦𝑧)} → 𝑥𝐶))
6160ralrimiv 3142 . . 3 (𝜑 → ∀𝑥 ∈ {𝑦 ∣ ∀𝑧(∀𝑤(𝑤𝑦 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑦𝑧)}𝑥𝐶)
62 unissb 4900 . . 3 ( {𝑦 ∣ ∀𝑧(∀𝑤(𝑤𝑦 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑦𝑧)} ⊆ 𝐶 ↔ ∀𝑥 ∈ {𝑦 ∣ ∀𝑧(∀𝑤(𝑤𝑦 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑦𝑧)}𝑥𝐶)
6361, 62sylibr 233 . 2 (𝜑 {𝑦 ∣ ∀𝑧(∀𝑤(𝑤𝑦 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑦𝑧)} ⊆ 𝐶)
643, 63eqsstrid 3992 1 (𝜑𝐵𝐶)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396  w3a 1087  wal 1539   = wceq 1541  wcel 2106  {cab 2713  wnfc 2887  wral 3064  Vcvv 3445  cin 3909  wss 3910  c0 4282  𝒫 cpw 4560   cuni 4865  cima 5636  Fun wfun 6490  cfv 6496  setrecscsetrecs 47118
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-rab 3408  df-v 3447  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-br 5106  df-opab 5168  df-id 5531  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-iota 6448  df-fun 6498  df-fv 6504  df-setrecs 47119
This theorem is referenced by:  setrec2  47130
  Copyright terms: Public domain W3C validator