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

Theorem setrec1lem4 45611
 Description: Lemma for setrec1 45612. If 𝑋 is recursively generated by 𝐹, then so is 𝑋 ∪ (𝐹‘𝐴). In the proof of setrec1 45612, the following is substituted for this theorem's 𝜑: (𝜑 ∧ (𝐴 ⊆ 𝑥 ∧ 𝑥 ∈ {𝑦 ∣ ∀𝑧(∀𝑤 (𝑤 ⊆ 𝑦 → (𝑤 ⊆ 𝑧 → (𝐹‘𝑤) ⊆ 𝑧)) → 𝑦 ⊆ 𝑧)})) Therefore, we cannot declare 𝑧 to be a distinct variable from 𝜑, since we need it to appear as a bound variable in 𝜑. This theorem can be proven without the hypothesis Ⅎ𝑧𝜑, but the proof would be harder to read because theorems in deduction form would be interrupted by theorems like eximi 1836, making the antecedent of each line something more complicated than 𝜑. The proof of setrec1lem2 45609 could similarly be made easier to read by adding the hypothesis Ⅎ𝑧𝜑, but I had already finished the proof and decided to leave it as is. (Contributed by Emmett Weisz, 26-Nov-2020.) (New usage is discouraged.)
Hypotheses
Ref Expression
setrec1lem4.1 𝑧𝜑
setrec1lem4.2 𝑌 = {𝑦 ∣ ∀𝑧(∀𝑤(𝑤𝑦 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑦𝑧)}
setrec1lem4.3 (𝜑𝐴 ∈ V)
setrec1lem4.4 (𝜑𝐴𝑋)
setrec1lem4.5 (𝜑𝑋𝑌)
Assertion
Ref Expression
setrec1lem4 (𝜑 → (𝑋 ∪ (𝐹𝐴)) ∈ 𝑌)
Distinct variable groups:   𝑦,𝑤,𝑧,𝐴   𝑤,𝐹,𝑦,𝑧   𝑤,𝑋,𝑦,𝑧
Allowed substitution hints:   𝜑(𝑦,𝑧,𝑤)   𝑌(𝑦,𝑧,𝑤)

Proof of Theorem setrec1lem4
StepHypRef Expression
1 setrec1lem4.1 . . 3 𝑧𝜑
2 id 22 . . . . . . . 8 (𝑤𝑋𝑤𝑋)
3 ssun1 4077 . . . . . . . 8 𝑋 ⊆ (𝑋 ∪ (𝐹𝐴))
42, 3sstrdi 3904 . . . . . . 7 (𝑤𝑋𝑤 ⊆ (𝑋 ∪ (𝐹𝐴)))
54imim1i 63 . . . . . 6 ((𝑤 ⊆ (𝑋 ∪ (𝐹𝐴)) → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → (𝑤𝑋 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)))
65alimi 1813 . . . . 5 (∀𝑤(𝑤 ⊆ (𝑋 ∪ (𝐹𝐴)) → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → ∀𝑤(𝑤𝑋 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)))
7 setrec1lem4.5 . . . . . . . 8 (𝜑𝑋𝑌)
8 setrec1lem4.2 . . . . . . . . 9 𝑌 = {𝑦 ∣ ∀𝑧(∀𝑤(𝑤𝑦 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑦𝑧)}
98, 7setrec1lem1 45608 . . . . . . . 8 (𝜑 → (𝑋𝑌 ↔ ∀𝑧(∀𝑤(𝑤𝑋 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑋𝑧)))
107, 9mpbid 235 . . . . . . 7 (𝜑 → ∀𝑧(∀𝑤(𝑤𝑋 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑋𝑧))
11 sp 2180 . . . . . . 7 (∀𝑧(∀𝑤(𝑤𝑋 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑋𝑧) → (∀𝑤(𝑤𝑋 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑋𝑧))
1210, 11syl 17 . . . . . 6 (𝜑 → (∀𝑤(𝑤𝑋 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑋𝑧))
13 setrec1lem4.4 . . . . . . . . 9 (𝜑𝐴𝑋)
14 sstr2 3899 . . . . . . . . 9 (𝐴𝑋 → (𝑋𝑧𝐴𝑧))
1513, 14syl 17 . . . . . . . 8 (𝜑 → (𝑋𝑧𝐴𝑧))
1612, 15syld 47 . . . . . . 7 (𝜑 → (∀𝑤(𝑤𝑋 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝐴𝑧))
17 setrec1lem4.3 . . . . . . . . 9 (𝜑𝐴 ∈ V)
18 sseq1 3917 . . . . . . . . . 10 (𝑤 = 𝐴 → (𝑤𝑋𝐴𝑋))
19 sseq1 3917 . . . . . . . . . . 11 (𝑤 = 𝐴 → (𝑤𝑧𝐴𝑧))
20 fveq2 6658 . . . . . . . . . . . 12 (𝑤 = 𝐴 → (𝐹𝑤) = (𝐹𝐴))
2120sseq1d 3923 . . . . . . . . . . 11 (𝑤 = 𝐴 → ((𝐹𝑤) ⊆ 𝑧 ↔ (𝐹𝐴) ⊆ 𝑧))
2219, 21imbi12d 348 . . . . . . . . . 10 (𝑤 = 𝐴 → ((𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧) ↔ (𝐴𝑧 → (𝐹𝐴) ⊆ 𝑧)))
2318, 22imbi12d 348 . . . . . . . . 9 (𝑤 = 𝐴 → ((𝑤𝑋 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) ↔ (𝐴𝑋 → (𝐴𝑧 → (𝐹𝐴) ⊆ 𝑧))))
2417, 23spcdvw 45600 . . . . . . . 8 (𝜑 → (∀𝑤(𝑤𝑋 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → (𝐴𝑋 → (𝐴𝑧 → (𝐹𝐴) ⊆ 𝑧))))
2513, 24mpid 44 . . . . . . 7 (𝜑 → (∀𝑤(𝑤𝑋 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → (𝐴𝑧 → (𝐹𝐴) ⊆ 𝑧)))
2616, 25mpdd 43 . . . . . 6 (𝜑 → (∀𝑤(𝑤𝑋 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → (𝐹𝐴) ⊆ 𝑧))
2712, 26jcad 516 . . . . 5 (𝜑 → (∀𝑤(𝑤𝑋 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → (𝑋𝑧 ∧ (𝐹𝐴) ⊆ 𝑧)))
286, 27syl5 34 . . . 4 (𝜑 → (∀𝑤(𝑤 ⊆ (𝑋 ∪ (𝐹𝐴)) → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → (𝑋𝑧 ∧ (𝐹𝐴) ⊆ 𝑧)))
29 unss 4089 . . . 4 ((𝑋𝑧 ∧ (𝐹𝐴) ⊆ 𝑧) ↔ (𝑋 ∪ (𝐹𝐴)) ⊆ 𝑧)
3028, 29syl6ib 254 . . 3 (𝜑 → (∀𝑤(𝑤 ⊆ (𝑋 ∪ (𝐹𝐴)) → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → (𝑋 ∪ (𝐹𝐴)) ⊆ 𝑧))
311, 30alrimi 2211 . 2 (𝜑 → ∀𝑧(∀𝑤(𝑤 ⊆ (𝑋 ∪ (𝐹𝐴)) → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → (𝑋 ∪ (𝐹𝐴)) ⊆ 𝑧))
32 fvex 6671 . . . 4 (𝐹𝐴) ∈ V
33 unexg 7470 . . . 4 ((𝑋𝑌 ∧ (𝐹𝐴) ∈ V) → (𝑋 ∪ (𝐹𝐴)) ∈ V)
347, 32, 33sylancl 589 . . 3 (𝜑 → (𝑋 ∪ (𝐹𝐴)) ∈ V)
358, 34setrec1lem1 45608 . 2 (𝜑 → ((𝑋 ∪ (𝐹𝐴)) ∈ 𝑌 ↔ ∀𝑧(∀𝑤(𝑤 ⊆ (𝑋 ∪ (𝐹𝐴)) → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → (𝑋 ∪ (𝐹𝐴)) ⊆ 𝑧)))
3631, 35mpbird 260 1 (𝜑 → (𝑋 ∪ (𝐹𝐴)) ∈ 𝑌)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399  ∀wal 1536   = wceq 1538  Ⅎwnf 1785   ∈ wcel 2111  {cab 2735  Vcvv 3409   ∪ cun 3856   ⊆ wss 3858  ‘cfv 6335 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 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-sep 5169  ax-nul 5176  ax-pr 5298  ax-un 7459 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ral 3075  df-rex 3076  df-rab 3079  df-v 3411  df-sbc 3697  df-dif 3861  df-un 3863  df-in 3865  df-ss 3875  df-nul 4226  df-sn 4523  df-pr 4525  df-op 4529  df-uni 4799  df-br 5033  df-iota 6294  df-fv 6343 This theorem is referenced by:  setrec1  45612
 Copyright terms: Public domain W3C validator