ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  frecabex GIF version

Theorem frecabex 6014
Description: The class abstraction from df-frec 6008 exists. This is a lemma for other finite recursion proofs. (Contributed by Jim Kingdon, 13-May-2020.)
Hypotheses
Ref Expression
frecabex.sex (𝜑𝑆𝑉)
frecabex.fvex (𝜑 → ∀𝑦(𝐹𝑦) ∈ V)
frecabex.aex (𝜑𝐴𝑊)
Assertion
Ref Expression
frecabex (𝜑 → {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑆 = suc 𝑚𝑥 ∈ (𝐹‘(𝑆𝑚))) ∨ (dom 𝑆 = ∅ ∧ 𝑥𝐴))} ∈ V)
Distinct variable groups:   𝑥,𝐴   𝑥,𝐹   𝑥,𝑆,𝑦   𝜑,𝑚   𝑥,𝑚,𝑦   𝑦,𝐹
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝐴(𝑦,𝑚)   𝑆(𝑚)   𝐹(𝑚)   𝑉(𝑥,𝑦,𝑚)   𝑊(𝑥,𝑦,𝑚)

Proof of Theorem frecabex
StepHypRef Expression
1 omex 4343 . . . 4 ω ∈ V
2 simpr 107 . . . . . . 7 ((dom 𝑆 = suc 𝑚𝑥 ∈ (𝐹‘(𝑆𝑚))) → 𝑥 ∈ (𝐹‘(𝑆𝑚)))
32abssi 3042 . . . . . 6 {𝑥 ∣ (dom 𝑆 = suc 𝑚𝑥 ∈ (𝐹‘(𝑆𝑚)))} ⊆ (𝐹‘(𝑆𝑚))
4 frecabex.sex . . . . . . . 8 (𝜑𝑆𝑉)
5 vex 2577 . . . . . . . 8 𝑚 ∈ V
6 fvexg 5221 . . . . . . . 8 ((𝑆𝑉𝑚 ∈ V) → (𝑆𝑚) ∈ V)
74, 5, 6sylancl 398 . . . . . . 7 (𝜑 → (𝑆𝑚) ∈ V)
8 frecabex.fvex . . . . . . 7 (𝜑 → ∀𝑦(𝐹𝑦) ∈ V)
9 fveq2 5205 . . . . . . . . 9 (𝑦 = (𝑆𝑚) → (𝐹𝑦) = (𝐹‘(𝑆𝑚)))
109eleq1d 2122 . . . . . . . 8 (𝑦 = (𝑆𝑚) → ((𝐹𝑦) ∈ V ↔ (𝐹‘(𝑆𝑚)) ∈ V))
1110spcgv 2657 . . . . . . 7 ((𝑆𝑚) ∈ V → (∀𝑦(𝐹𝑦) ∈ V → (𝐹‘(𝑆𝑚)) ∈ V))
127, 8, 11sylc 60 . . . . . 6 (𝜑 → (𝐹‘(𝑆𝑚)) ∈ V)
13 ssexg 3923 . . . . . 6 (({𝑥 ∣ (dom 𝑆 = suc 𝑚𝑥 ∈ (𝐹‘(𝑆𝑚)))} ⊆ (𝐹‘(𝑆𝑚)) ∧ (𝐹‘(𝑆𝑚)) ∈ V) → {𝑥 ∣ (dom 𝑆 = suc 𝑚𝑥 ∈ (𝐹‘(𝑆𝑚)))} ∈ V)
143, 12, 13sylancr 399 . . . . 5 (𝜑 → {𝑥 ∣ (dom 𝑆 = suc 𝑚𝑥 ∈ (𝐹‘(𝑆𝑚)))} ∈ V)
1514ralrimivw 2410 . . . 4 (𝜑 → ∀𝑚 ∈ ω {𝑥 ∣ (dom 𝑆 = suc 𝑚𝑥 ∈ (𝐹‘(𝑆𝑚)))} ∈ V)
16 abrexex2g 5774 . . . 4 ((ω ∈ V ∧ ∀𝑚 ∈ ω {𝑥 ∣ (dom 𝑆 = suc 𝑚𝑥 ∈ (𝐹‘(𝑆𝑚)))} ∈ V) → {𝑥 ∣ ∃𝑚 ∈ ω (dom 𝑆 = suc 𝑚𝑥 ∈ (𝐹‘(𝑆𝑚)))} ∈ V)
171, 15, 16sylancr 399 . . 3 (𝜑 → {𝑥 ∣ ∃𝑚 ∈ ω (dom 𝑆 = suc 𝑚𝑥 ∈ (𝐹‘(𝑆𝑚)))} ∈ V)
18 simpr 107 . . . . 5 ((dom 𝑆 = ∅ ∧ 𝑥𝐴) → 𝑥𝐴)
1918abssi 3042 . . . 4 {𝑥 ∣ (dom 𝑆 = ∅ ∧ 𝑥𝐴)} ⊆ 𝐴
20 frecabex.aex . . . 4 (𝜑𝐴𝑊)
21 ssexg 3923 . . . 4 (({𝑥 ∣ (dom 𝑆 = ∅ ∧ 𝑥𝐴)} ⊆ 𝐴𝐴𝑊) → {𝑥 ∣ (dom 𝑆 = ∅ ∧ 𝑥𝐴)} ∈ V)
2219, 20, 21sylancr 399 . . 3 (𝜑 → {𝑥 ∣ (dom 𝑆 = ∅ ∧ 𝑥𝐴)} ∈ V)
2317, 22jca 294 . 2 (𝜑 → ({𝑥 ∣ ∃𝑚 ∈ ω (dom 𝑆 = suc 𝑚𝑥 ∈ (𝐹‘(𝑆𝑚)))} ∈ V ∧ {𝑥 ∣ (dom 𝑆 = ∅ ∧ 𝑥𝐴)} ∈ V))
24 unexb 4204 . . 3 (({𝑥 ∣ ∃𝑚 ∈ ω (dom 𝑆 = suc 𝑚𝑥 ∈ (𝐹‘(𝑆𝑚)))} ∈ V ∧ {𝑥 ∣ (dom 𝑆 = ∅ ∧ 𝑥𝐴)} ∈ V) ↔ ({𝑥 ∣ ∃𝑚 ∈ ω (dom 𝑆 = suc 𝑚𝑥 ∈ (𝐹‘(𝑆𝑚)))} ∪ {𝑥 ∣ (dom 𝑆 = ∅ ∧ 𝑥𝐴)}) ∈ V)
25 unab 3231 . . . 4 ({𝑥 ∣ ∃𝑚 ∈ ω (dom 𝑆 = suc 𝑚𝑥 ∈ (𝐹‘(𝑆𝑚)))} ∪ {𝑥 ∣ (dom 𝑆 = ∅ ∧ 𝑥𝐴)}) = {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑆 = suc 𝑚𝑥 ∈ (𝐹‘(𝑆𝑚))) ∨ (dom 𝑆 = ∅ ∧ 𝑥𝐴))}
2625eleq1i 2119 . . 3 (({𝑥 ∣ ∃𝑚 ∈ ω (dom 𝑆 = suc 𝑚𝑥 ∈ (𝐹‘(𝑆𝑚)))} ∪ {𝑥 ∣ (dom 𝑆 = ∅ ∧ 𝑥𝐴)}) ∈ V ↔ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑆 = suc 𝑚𝑥 ∈ (𝐹‘(𝑆𝑚))) ∨ (dom 𝑆 = ∅ ∧ 𝑥𝐴))} ∈ V)
2724, 26bitri 177 . 2 (({𝑥 ∣ ∃𝑚 ∈ ω (dom 𝑆 = suc 𝑚𝑥 ∈ (𝐹‘(𝑆𝑚)))} ∈ V ∧ {𝑥 ∣ (dom 𝑆 = ∅ ∧ 𝑥𝐴)} ∈ V) ↔ {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑆 = suc 𝑚𝑥 ∈ (𝐹‘(𝑆𝑚))) ∨ (dom 𝑆 = ∅ ∧ 𝑥𝐴))} ∈ V)
2823, 27sylib 131 1 (𝜑 → {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝑆 = suc 𝑚𝑥 ∈ (𝐹‘(𝑆𝑚))) ∨ (dom 𝑆 = ∅ ∧ 𝑥𝐴))} ∈ V)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 101  wo 639  wal 1257   = wceq 1259  wcel 1409  {cab 2042  wral 2323  wrex 2324  Vcvv 2574  cun 2942  wss 2944  c0 3251  suc csuc 4129  ωcom 4340  dom cdm 4372  cfv 4929
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-io 640  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-10 1412  ax-11 1413  ax-i12 1414  ax-bndl 1415  ax-4 1416  ax-13 1420  ax-14 1421  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038  ax-coll 3899  ax-sep 3902  ax-pow 3954  ax-pr 3971  ax-un 4197  ax-iinf 4338
This theorem depends on definitions:  df-bi 114  df-3an 898  df-tru 1262  df-nf 1366  df-sb 1662  df-eu 1919  df-mo 1920  df-clab 2043  df-cleq 2049  df-clel 2052  df-nfc 2183  df-ral 2328  df-rex 2329  df-reu 2330  df-rab 2332  df-v 2576  df-sbc 2787  df-csb 2880  df-un 2949  df-in 2951  df-ss 2958  df-pw 3388  df-sn 3408  df-pr 3409  df-op 3411  df-uni 3608  df-int 3643  df-iun 3686  df-br 3792  df-opab 3846  df-mpt 3847  df-id 4057  df-iom 4341  df-xp 4378  df-rel 4379  df-cnv 4380  df-co 4381  df-dm 4382  df-rn 4383  df-res 4384  df-ima 4385  df-iota 4894  df-fun 4931  df-fn 4932  df-f 4933  df-f1 4934  df-fo 4935  df-f1o 4936  df-fv 4937
This theorem is referenced by:  frectfr  6015  frecsuclem3  6020
  Copyright terms: Public domain W3C validator