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

Theorem setrec1lem3 45385
 Description: Lemma for setrec1 45387. If each element 𝑎 of 𝐴 is covered by a set 𝑥 recursively generated by 𝐹, then there is a single such set covering all of 𝐴. The set is constructed explicitly using setrec1lem2 45384. It turns out that 𝑥 = 𝐴 also works, i.e., given the hypotheses it is possible to prove that 𝐴 ∈ 𝑌. I don't know if proving this fact directly using setrec1lem1 45383 would be any easier than the current proof using setrec1lem2 45384, and it would only slightly simplify the proof of setrec1 45387. Other than the use of bnd2d 45377, this is a purely technical theorem for rearranging notation from that of setrec1lem2 45384 to that of setrec1 45387. (Contributed by Emmett Weisz, 20-Jan-2021.) (New usage is discouraged.)
Hypotheses
Ref Expression
setrec1lem3.1 𝑌 = {𝑦 ∣ ∀𝑧(∀𝑤(𝑤𝑦 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑦𝑧)}
setrec1lem3.2 (𝜑𝐴 ∈ V)
setrec1lem3.3 (𝜑 → ∀𝑎𝐴𝑥(𝑎𝑥𝑥𝑌))
Assertion
Ref Expression
setrec1lem3 (𝜑 → ∃𝑥(𝐴𝑥𝑥𝑌))
Distinct variable groups:   𝑦,𝑤,𝑧   𝑥,𝑎,𝐴   𝑌,𝑎,𝑥   𝑥,𝑦,𝐹
Allowed substitution hints:   𝜑(𝑥,𝑦,𝑧,𝑤,𝑎)   𝐴(𝑦,𝑧,𝑤)   𝐹(𝑧,𝑤,𝑎)   𝑌(𝑦,𝑧,𝑤)

Proof of Theorem setrec1lem3
Dummy variable 𝑣 is distinct from all other variables.
StepHypRef Expression
1 setrec1lem3.2 . . . 4 (𝜑𝐴 ∈ V)
2 setrec1lem3.3 . . . . . 6 (𝜑 → ∀𝑎𝐴𝑥(𝑎𝑥𝑥𝑌))
3 exancom 1862 . . . . . . 7 (∃𝑥(𝑎𝑥𝑥𝑌) ↔ ∃𝑥(𝑥𝑌𝑎𝑥))
43ralbii 3133 . . . . . 6 (∀𝑎𝐴𝑥(𝑎𝑥𝑥𝑌) ↔ ∀𝑎𝐴𝑥(𝑥𝑌𝑎𝑥))
52, 4sylib 221 . . . . 5 (𝜑 → ∀𝑎𝐴𝑥(𝑥𝑌𝑎𝑥))
6 df-rex 3112 . . . . . 6 (∃𝑥𝑌 𝑎𝑥 ↔ ∃𝑥(𝑥𝑌𝑎𝑥))
76ralbii 3133 . . . . 5 (∀𝑎𝐴𝑥𝑌 𝑎𝑥 ↔ ∀𝑎𝐴𝑥(𝑥𝑌𝑎𝑥))
85, 7sylibr 237 . . . 4 (𝜑 → ∀𝑎𝐴𝑥𝑌 𝑎𝑥)
91, 8bnd2d 45377 . . 3 (𝜑 → ∃𝑣(𝑣𝑌 ∧ ∀𝑎𝐴𝑥𝑣 𝑎𝑥))
10 exancom 1862 . . . . . . . 8 (∃𝑥(𝑥𝑣𝑎𝑥) ↔ ∃𝑥(𝑎𝑥𝑥𝑣))
11 df-rex 3112 . . . . . . . 8 (∃𝑥𝑣 𝑎𝑥 ↔ ∃𝑥(𝑥𝑣𝑎𝑥))
12 eluni 4807 . . . . . . . 8 (𝑎 𝑣 ↔ ∃𝑥(𝑎𝑥𝑥𝑣))
1310, 11, 123bitr4i 306 . . . . . . 7 (∃𝑥𝑣 𝑎𝑥𝑎 𝑣)
1413ralbii 3133 . . . . . 6 (∀𝑎𝐴𝑥𝑣 𝑎𝑥 ↔ ∀𝑎𝐴 𝑎 𝑣)
15 dfss3 3905 . . . . . 6 (𝐴 𝑣 ↔ ∀𝑎𝐴 𝑎 𝑣)
1614, 15bitr4i 281 . . . . 5 (∀𝑎𝐴𝑥𝑣 𝑎𝑥𝐴 𝑣)
1716anbi2i 625 . . . 4 ((𝑣𝑌 ∧ ∀𝑎𝐴𝑥𝑣 𝑎𝑥) ↔ (𝑣𝑌𝐴 𝑣))
1817exbii 1849 . . 3 (∃𝑣(𝑣𝑌 ∧ ∀𝑎𝐴𝑥𝑣 𝑎𝑥) ↔ ∃𝑣(𝑣𝑌𝐴 𝑣))
199, 18sylib 221 . 2 (𝜑 → ∃𝑣(𝑣𝑌𝐴 𝑣))
20 setrec1lem3.1 . . . . . . 7 𝑌 = {𝑦 ∣ ∀𝑧(∀𝑤(𝑤𝑦 → (𝑤𝑧 → (𝐹𝑤) ⊆ 𝑧)) → 𝑦𝑧)}
21 vex 3445 . . . . . . . 8 𝑣 ∈ V
2221a1i 11 . . . . . . 7 (𝑣𝑌𝑣 ∈ V)
23 id 22 . . . . . . 7 (𝑣𝑌𝑣𝑌)
2420, 22, 23setrec1lem2 45384 . . . . . 6 (𝑣𝑌 𝑣𝑌)
2524anim1i 617 . . . . 5 ((𝑣𝑌𝐴 𝑣) → ( 𝑣𝑌𝐴 𝑣))
2625ancomd 465 . . . 4 ((𝑣𝑌𝐴 𝑣) → (𝐴 𝑣 𝑣𝑌))
2721uniex 7460 . . . . 5 𝑣 ∈ V
28 sseq2 3943 . . . . . 6 (𝑥 = 𝑣 → (𝐴𝑥𝐴 𝑣))
29 eleq1 2877 . . . . . 6 (𝑥 = 𝑣 → (𝑥𝑌 𝑣𝑌))
3028, 29anbi12d 633 . . . . 5 (𝑥 = 𝑣 → ((𝐴𝑥𝑥𝑌) ↔ (𝐴 𝑣 𝑣𝑌)))
3127, 30spcev 3556 . . . 4 ((𝐴 𝑣 𝑣𝑌) → ∃𝑥(𝐴𝑥𝑥𝑌))
3226, 31syl 17 . . 3 ((𝑣𝑌𝐴 𝑣) → ∃𝑥(𝐴𝑥𝑥𝑌))
3332exlimiv 1931 . 2 (∃𝑣(𝑣𝑌𝐴 𝑣) → ∃𝑥(𝐴𝑥𝑥𝑌))
3419, 33syl 17 1 (𝜑 → ∃𝑥(𝐴𝑥𝑥𝑌))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399  ∀wal 1536   = wceq 1538  ∃wex 1781   ∈ wcel 2111  {cab 2776  ∀wral 3106  ∃wrex 3107  Vcvv 3442   ⊆ wss 3883  ∪ cuni 4804  ‘cfv 6332 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 2770  ax-rep 5158  ax-sep 5171  ax-nul 5178  ax-pow 5235  ax-pr 5299  ax-un 7454  ax-reg 9058  ax-inf2 9106 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-reu 3113  df-rab 3115  df-v 3444  df-sbc 3723  df-csb 3831  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-tp 4533  df-op 4535  df-uni 4805  df-int 4843  df-iun 4887  df-iin 4888  df-br 5035  df-opab 5097  df-mpt 5115  df-tr 5141  df-id 5429  df-eprel 5434  df-po 5442  df-so 5443  df-fr 5482  df-we 5484  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-pred 6123  df-ord 6169  df-on 6170  df-lim 6171  df-suc 6172  df-iota 6291  df-fun 6334  df-fn 6335  df-f 6336  df-f1 6337  df-fo 6338  df-f1o 6339  df-fv 6340  df-om 7574  df-wrecs 7948  df-recs 8009  df-rdg 8047  df-r1 9195  df-rank 9196 This theorem is referenced by:  setrec1  45387
 Copyright terms: Public domain W3C validator