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

Theorem frecabex 5923
Description: The class abstraction from df-frec 5918 exists. This is a lemma for other finite recursion proofs. (Contributed by Jim Kingdon, 13-May-2020.)
Hypotheses
Ref Expression
frecabex.sex (φ𝑆 𝑉)
frecabex.fvex (φy(𝐹y) V)
frecabex.aex (φA 𝑊)
Assertion
Ref Expression
frecabex (φ → {x ∣ (𝑚 𝜔 (dom 𝑆 = suc 𝑚 x (𝐹‘(𝑆𝑚))) (dom 𝑆 = ∅ x A))} V)
Distinct variable groups:   x,A   x,𝐹   x,𝑆,y   φ,𝑚   x,𝑚,y   y,𝐹
Allowed substitution hints:   φ(x,y)   A(y,𝑚)   𝑆(𝑚)   𝐹(𝑚)   𝑉(x,y,𝑚)   𝑊(x,y,𝑚)

Proof of Theorem frecabex
StepHypRef Expression
1 omex 4259 . . . 4 𝜔 V
2 simpr 103 . . . . . . 7 ((dom 𝑆 = suc 𝑚 x (𝐹‘(𝑆𝑚))) → x (𝐹‘(𝑆𝑚)))
32abssi 3009 . . . . . 6 {x ∣ (dom 𝑆 = suc 𝑚 x (𝐹‘(𝑆𝑚)))} ⊆ (𝐹‘(𝑆𝑚))
4 frecabex.sex . . . . . . . 8 (φ𝑆 𝑉)
5 vex 2554 . . . . . . . 8 𝑚 V
6 fvexg 5137 . . . . . . . 8 ((𝑆 𝑉 𝑚 V) → (𝑆𝑚) V)
74, 5, 6sylancl 392 . . . . . . 7 (φ → (𝑆𝑚) V)
8 frecabex.fvex . . . . . . 7 (φy(𝐹y) V)
9 fveq2 5121 . . . . . . . . 9 (y = (𝑆𝑚) → (𝐹y) = (𝐹‘(𝑆𝑚)))
109eleq1d 2103 . . . . . . . 8 (y = (𝑆𝑚) → ((𝐹y) V ↔ (𝐹‘(𝑆𝑚)) V))
1110spcgv 2634 . . . . . . 7 ((𝑆𝑚) V → (y(𝐹y) V → (𝐹‘(𝑆𝑚)) V))
127, 8, 11sylc 56 . . . . . 6 (φ → (𝐹‘(𝑆𝑚)) V)
13 ssexg 3887 . . . . . 6 (({x ∣ (dom 𝑆 = suc 𝑚 x (𝐹‘(𝑆𝑚)))} ⊆ (𝐹‘(𝑆𝑚)) (𝐹‘(𝑆𝑚)) V) → {x ∣ (dom 𝑆 = suc 𝑚 x (𝐹‘(𝑆𝑚)))} V)
143, 12, 13sylancr 393 . . . . 5 (φ → {x ∣ (dom 𝑆 = suc 𝑚 x (𝐹‘(𝑆𝑚)))} V)
1514ralrimivw 2387 . . . 4 (φ𝑚 𝜔 {x ∣ (dom 𝑆 = suc 𝑚 x (𝐹‘(𝑆𝑚)))} V)
16 abrexex2g 5689 . . . 4 ((𝜔 V 𝑚 𝜔 {x ∣ (dom 𝑆 = suc 𝑚 x (𝐹‘(𝑆𝑚)))} V) → {x𝑚 𝜔 (dom 𝑆 = suc 𝑚 x (𝐹‘(𝑆𝑚)))} V)
171, 15, 16sylancr 393 . . 3 (φ → {x𝑚 𝜔 (dom 𝑆 = suc 𝑚 x (𝐹‘(𝑆𝑚)))} V)
18 simpr 103 . . . . 5 ((dom 𝑆 = ∅ x A) → x A)
1918abssi 3009 . . . 4 {x ∣ (dom 𝑆 = ∅ x A)} ⊆ A
20 frecabex.aex . . . 4 (φA 𝑊)
21 ssexg 3887 . . . 4 (({x ∣ (dom 𝑆 = ∅ x A)} ⊆ A A 𝑊) → {x ∣ (dom 𝑆 = ∅ x A)} V)
2219, 20, 21sylancr 393 . . 3 (φ → {x ∣ (dom 𝑆 = ∅ x A)} V)
2317, 22jca 290 . 2 (φ → ({x𝑚 𝜔 (dom 𝑆 = suc 𝑚 x (𝐹‘(𝑆𝑚)))} V {x ∣ (dom 𝑆 = ∅ x A)} V))
24 unexb 4143 . . 3 (({x𝑚 𝜔 (dom 𝑆 = suc 𝑚 x (𝐹‘(𝑆𝑚)))} V {x ∣ (dom 𝑆 = ∅ x A)} V) ↔ ({x𝑚 𝜔 (dom 𝑆 = suc 𝑚 x (𝐹‘(𝑆𝑚)))} ∪ {x ∣ (dom 𝑆 = ∅ x A)}) V)
25 unab 3198 . . . 4 ({x𝑚 𝜔 (dom 𝑆 = suc 𝑚 x (𝐹‘(𝑆𝑚)))} ∪ {x ∣ (dom 𝑆 = ∅ x A)}) = {x ∣ (𝑚 𝜔 (dom 𝑆 = suc 𝑚 x (𝐹‘(𝑆𝑚))) (dom 𝑆 = ∅ x A))}
2625eleq1i 2100 . . 3 (({x𝑚 𝜔 (dom 𝑆 = suc 𝑚 x (𝐹‘(𝑆𝑚)))} ∪ {x ∣ (dom 𝑆 = ∅ x A)}) V ↔ {x ∣ (𝑚 𝜔 (dom 𝑆 = suc 𝑚 x (𝐹‘(𝑆𝑚))) (dom 𝑆 = ∅ x A))} V)
2724, 26bitri 173 . 2 (({x𝑚 𝜔 (dom 𝑆 = suc 𝑚 x (𝐹‘(𝑆𝑚)))} V {x ∣ (dom 𝑆 = ∅ x A)} V) ↔ {x ∣ (𝑚 𝜔 (dom 𝑆 = suc 𝑚 x (𝐹‘(𝑆𝑚))) (dom 𝑆 = ∅ x A))} V)
2823, 27sylib 127 1 (φ → {x ∣ (𝑚 𝜔 (dom 𝑆 = suc 𝑚 x (𝐹‘(𝑆𝑚))) (dom 𝑆 = ∅ x A))} V)
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97   wo 628  wal 1240   = wceq 1242   wcel 1390  {cab 2023  wral 2300  wrex 2301  Vcvv 2551  cun 2909  wss 2911  c0 3218  suc csuc 4068  𝜔com 4256  dom cdm 4288  cfv 4845
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bnd 1396  ax-4 1397  ax-13 1401  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-coll 3863  ax-sep 3866  ax-pow 3918  ax-pr 3935  ax-un 4136  ax-iinf 4254
This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-rex 2306  df-reu 2307  df-rab 2309  df-v 2553  df-sbc 2759  df-csb 2847  df-un 2916  df-in 2918  df-ss 2925  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-uni 3572  df-int 3607  df-iun 3650  df-br 3756  df-opab 3810  df-mpt 3811  df-id 4021  df-iom 4257  df-xp 4294  df-rel 4295  df-cnv 4296  df-co 4297  df-dm 4298  df-rn 4299  df-res 4300  df-ima 4301  df-iota 4810  df-fun 4847  df-fn 4848  df-f 4849  df-f1 4850  df-fo 4851  df-f1o 4852  df-fv 4853
This theorem is referenced by:  frectfr  5924  frecsuclem3  5929
  Copyright terms: Public domain W3C validator