MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  frsucmptn Structured version   Visualization version   GIF version

Theorem frsucmptn 8477
Description: The value of the finite recursive definition generator at a successor (special case where the characteristic function is a mapping abstraction and where the mapping class 𝐷 is a proper class). This is a technical lemma that can be used together with frsucmpt 8476 to help eliminate redundant sethood antecedents. (Contributed by Scott Fenton, 19-Feb-2011.) (Revised by Mario Carneiro, 11-Sep-2015.)
Hypotheses
Ref Expression
frsucmpt.1 𝑥𝐴
frsucmpt.2 𝑥𝐵
frsucmpt.3 𝑥𝐷
frsucmpt.4 𝐹 = (rec((𝑥 ∈ V ↦ 𝐶), 𝐴) ↾ ω)
frsucmpt.5 (𝑥 = (𝐹𝐵) → 𝐶 = 𝐷)
Assertion
Ref Expression
frsucmptn 𝐷 ∈ V → (𝐹‘suc 𝐵) = ∅)

Proof of Theorem frsucmptn
StepHypRef Expression
1 frsucmpt.4 . . 3 𝐹 = (rec((𝑥 ∈ V ↦ 𝐶), 𝐴) ↾ ω)
21fveq1i 6906 . 2 (𝐹‘suc 𝐵) = ((rec((𝑥 ∈ V ↦ 𝐶), 𝐴) ↾ ω)‘suc 𝐵)
3 frfnom 8473 . . . . . 6 (rec((𝑥 ∈ V ↦ 𝐶), 𝐴) ↾ ω) Fn ω
4 fndm 6667 . . . . . 6 ((rec((𝑥 ∈ V ↦ 𝐶), 𝐴) ↾ ω) Fn ω → dom (rec((𝑥 ∈ V ↦ 𝐶), 𝐴) ↾ ω) = ω)
53, 4ax-mp 5 . . . . 5 dom (rec((𝑥 ∈ V ↦ 𝐶), 𝐴) ↾ ω) = ω
65eleq2i 2821 . . . 4 (suc 𝐵 ∈ dom (rec((𝑥 ∈ V ↦ 𝐶), 𝐴) ↾ ω) ↔ suc 𝐵 ∈ ω)
7 peano2b 7901 . . . . 5 (𝐵 ∈ ω ↔ suc 𝐵 ∈ ω)
8 frsuc 8475 . . . . . . . 8 (𝐵 ∈ ω → ((rec((𝑥 ∈ V ↦ 𝐶), 𝐴) ↾ ω)‘suc 𝐵) = ((𝑥 ∈ V ↦ 𝐶)‘((rec((𝑥 ∈ V ↦ 𝐶), 𝐴) ↾ ω)‘𝐵)))
91fveq1i 6906 . . . . . . . . 9 (𝐹𝐵) = ((rec((𝑥 ∈ V ↦ 𝐶), 𝐴) ↾ ω)‘𝐵)
109fveq2i 6908 . . . . . . . 8 ((𝑥 ∈ V ↦ 𝐶)‘(𝐹𝐵)) = ((𝑥 ∈ V ↦ 𝐶)‘((rec((𝑥 ∈ V ↦ 𝐶), 𝐴) ↾ ω)‘𝐵))
118, 10eqtr4di 2787 . . . . . . 7 (𝐵 ∈ ω → ((rec((𝑥 ∈ V ↦ 𝐶), 𝐴) ↾ ω)‘suc 𝐵) = ((𝑥 ∈ V ↦ 𝐶)‘(𝐹𝐵)))
12 nfmpt1 5264 . . . . . . . . . . . 12 𝑥(𝑥 ∈ V ↦ 𝐶)
13 frsucmpt.1 . . . . . . . . . . . 12 𝑥𝐴
1412, 13nfrdg 8452 . . . . . . . . . . 11 𝑥rec((𝑥 ∈ V ↦ 𝐶), 𝐴)
15 nfcv 2895 . . . . . . . . . . 11 𝑥ω
1614, 15nfres 5996 . . . . . . . . . 10 𝑥(rec((𝑥 ∈ V ↦ 𝐶), 𝐴) ↾ ω)
171, 16nfcxfr 2893 . . . . . . . . 9 𝑥𝐹
18 frsucmpt.2 . . . . . . . . 9 𝑥𝐵
1917, 18nffv 6915 . . . . . . . 8 𝑥(𝐹𝐵)
20 frsucmpt.3 . . . . . . . 8 𝑥𝐷
21 frsucmpt.5 . . . . . . . 8 (𝑥 = (𝐹𝐵) → 𝐶 = 𝐷)
22 eqid 2729 . . . . . . . 8 (𝑥 ∈ V ↦ 𝐶) = (𝑥 ∈ V ↦ 𝐶)
2319, 20, 21, 22fvmptnf 7036 . . . . . . 7 𝐷 ∈ V → ((𝑥 ∈ V ↦ 𝐶)‘(𝐹𝐵)) = ∅)
2411, 23sylan9eqr 2791 . . . . . 6 ((¬ 𝐷 ∈ V ∧ 𝐵 ∈ ω) → ((rec((𝑥 ∈ V ↦ 𝐶), 𝐴) ↾ ω)‘suc 𝐵) = ∅)
2524ex 411 . . . . 5 𝐷 ∈ V → (𝐵 ∈ ω → ((rec((𝑥 ∈ V ↦ 𝐶), 𝐴) ↾ ω)‘suc 𝐵) = ∅))
267, 25biimtrrid 242 . . . 4 𝐷 ∈ V → (suc 𝐵 ∈ ω → ((rec((𝑥 ∈ V ↦ 𝐶), 𝐴) ↾ ω)‘suc 𝐵) = ∅))
276, 26biimtrid 241 . . 3 𝐷 ∈ V → (suc 𝐵 ∈ dom (rec((𝑥 ∈ V ↦ 𝐶), 𝐴) ↾ ω) → ((rec((𝑥 ∈ V ↦ 𝐶), 𝐴) ↾ ω)‘suc 𝐵) = ∅))
28 ndmfv 6940 . . 3 (¬ suc 𝐵 ∈ dom (rec((𝑥 ∈ V ↦ 𝐶), 𝐴) ↾ ω) → ((rec((𝑥 ∈ V ↦ 𝐶), 𝐴) ↾ ω)‘suc 𝐵) = ∅)
2927, 28pm2.61d1 180 . 2 𝐷 ∈ V → ((rec((𝑥 ∈ V ↦ 𝐶), 𝐴) ↾ ω)‘suc 𝐵) = ∅)
302, 29eqtrid 2781 1 𝐷 ∈ V → (𝐹‘suc 𝐵) = ∅)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1534  wcel 2100  wnfc 2879  Vcvv 3472  c0 4335  cmpt 5239  dom cdm 5686  cres 5688  suc csuc 6382   Fn wfn 6553  cfv 6558  ωcom 7884  reccrdg 8447
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2102  ax-9 2110  ax-10 2133  ax-11 2150  ax-12 2170  ax-ext 2700  ax-sep 5307  ax-nul 5314  ax-pr 5437  ax-un 7751
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2062  df-mo 2532  df-eu 2561  df-clab 2707  df-cleq 2721  df-clel 2806  df-nfc 2881  df-ne 2934  df-ral 3055  df-rex 3064  df-reu 3374  df-rab 3429  df-v 3474  df-sbc 3789  df-csb 3905  df-dif 3962  df-un 3964  df-in 3966  df-ss 3976  df-pss 3979  df-nul 4336  df-if 4537  df-pw 4612  df-sn 4637  df-pr 4639  df-op 4643  df-uni 4919  df-iun 5008  df-br 5157  df-opab 5219  df-mpt 5240  df-tr 5274  df-id 5584  df-eprel 5590  df-po 5598  df-so 5599  df-fr 5641  df-we 5643  df-xp 5692  df-rel 5693  df-cnv 5694  df-co 5695  df-dm 5696  df-rn 5697  df-res 5698  df-ima 5699  df-pred 6317  df-ord 6383  df-on 6384  df-lim 6385  df-suc 6386  df-iota 6510  df-fun 6560  df-fn 6561  df-f 6562  df-f1 6563  df-fo 6564  df-f1o 6565  df-fv 6566  df-ov 7433  df-om 7885  df-2nd 8012  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator