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

Theorem tfrlem10 7443
 Description: Lemma for transfinite recursion. We define class 𝐶 by extending recs with one ordered pair. We will assume, falsely, that domain of recs is a member of, and thus not equal to, On. Using this assumption we will prove facts about 𝐶 that will lead to a contradiction in tfrlem14 7447, thus showing the domain of recs does in fact equal On. Here we show (under the false assumption) that 𝐶 is a function extending the domain of recs(𝐹) by one. (Contributed by NM, 14-Aug-1994.) (Revised by Mario Carneiro, 9-May-2015.)
Hypotheses
Ref Expression
tfrlem.1 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))}
tfrlem.3 𝐶 = (recs(𝐹) ∪ {⟨dom recs(𝐹), (𝐹‘recs(𝐹))⟩})
Assertion
Ref Expression
tfrlem10 (dom recs(𝐹) ∈ On → 𝐶 Fn suc dom recs(𝐹))
Distinct variable groups:   𝑥,𝑓,𝑦,𝐶   𝑓,𝐹,𝑥,𝑦
Allowed substitution hints:   𝐴(𝑥,𝑦,𝑓)

Proof of Theorem tfrlem10
StepHypRef Expression
1 fvex 6168 . . . . . 6 (𝐹‘recs(𝐹)) ∈ V
2 funsng 5905 . . . . . 6 ((dom recs(𝐹) ∈ On ∧ (𝐹‘recs(𝐹)) ∈ V) → Fun {⟨dom recs(𝐹), (𝐹‘recs(𝐹))⟩})
31, 2mpan2 706 . . . . 5 (dom recs(𝐹) ∈ On → Fun {⟨dom recs(𝐹), (𝐹‘recs(𝐹))⟩})
4 tfrlem.1 . . . . . 6 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))}
54tfrlem7 7439 . . . . 5 Fun recs(𝐹)
63, 5jctil 559 . . . 4 (dom recs(𝐹) ∈ On → (Fun recs(𝐹) ∧ Fun {⟨dom recs(𝐹), (𝐹‘recs(𝐹))⟩}))
71dmsnop 5578 . . . . . 6 dom {⟨dom recs(𝐹), (𝐹‘recs(𝐹))⟩} = {dom recs(𝐹)}
87ineq2i 3795 . . . . 5 (dom recs(𝐹) ∩ dom {⟨dom recs(𝐹), (𝐹‘recs(𝐹))⟩}) = (dom recs(𝐹) ∩ {dom recs(𝐹)})
94tfrlem8 7440 . . . . . 6 Ord dom recs(𝐹)
10 orddisj 5731 . . . . . 6 (Ord dom recs(𝐹) → (dom recs(𝐹) ∩ {dom recs(𝐹)}) = ∅)
119, 10ax-mp 5 . . . . 5 (dom recs(𝐹) ∩ {dom recs(𝐹)}) = ∅
128, 11eqtri 2643 . . . 4 (dom recs(𝐹) ∩ dom {⟨dom recs(𝐹), (𝐹‘recs(𝐹))⟩}) = ∅
13 funun 5900 . . . 4 (((Fun recs(𝐹) ∧ Fun {⟨dom recs(𝐹), (𝐹‘recs(𝐹))⟩}) ∧ (dom recs(𝐹) ∩ dom {⟨dom recs(𝐹), (𝐹‘recs(𝐹))⟩}) = ∅) → Fun (recs(𝐹) ∪ {⟨dom recs(𝐹), (𝐹‘recs(𝐹))⟩}))
146, 12, 13sylancl 693 . . 3 (dom recs(𝐹) ∈ On → Fun (recs(𝐹) ∪ {⟨dom recs(𝐹), (𝐹‘recs(𝐹))⟩}))
157uneq2i 3748 . . . 4 (dom recs(𝐹) ∪ dom {⟨dom recs(𝐹), (𝐹‘recs(𝐹))⟩}) = (dom recs(𝐹) ∪ {dom recs(𝐹)})
16 dmun 5301 . . . 4 dom (recs(𝐹) ∪ {⟨dom recs(𝐹), (𝐹‘recs(𝐹))⟩}) = (dom recs(𝐹) ∪ dom {⟨dom recs(𝐹), (𝐹‘recs(𝐹))⟩})
17 df-suc 5698 . . . 4 suc dom recs(𝐹) = (dom recs(𝐹) ∪ {dom recs(𝐹)})
1815, 16, 173eqtr4i 2653 . . 3 dom (recs(𝐹) ∪ {⟨dom recs(𝐹), (𝐹‘recs(𝐹))⟩}) = suc dom recs(𝐹)
19 df-fn 5860 . . 3 ((recs(𝐹) ∪ {⟨dom recs(𝐹), (𝐹‘recs(𝐹))⟩}) Fn suc dom recs(𝐹) ↔ (Fun (recs(𝐹) ∪ {⟨dom recs(𝐹), (𝐹‘recs(𝐹))⟩}) ∧ dom (recs(𝐹) ∪ {⟨dom recs(𝐹), (𝐹‘recs(𝐹))⟩}) = suc dom recs(𝐹)))
2014, 18, 19sylanblrc 696 . 2 (dom recs(𝐹) ∈ On → (recs(𝐹) ∪ {⟨dom recs(𝐹), (𝐹‘recs(𝐹))⟩}) Fn suc dom recs(𝐹))
21 tfrlem.3 . . 3 𝐶 = (recs(𝐹) ∪ {⟨dom recs(𝐹), (𝐹‘recs(𝐹))⟩})
2221fneq1i 5953 . 2 (𝐶 Fn suc dom recs(𝐹) ↔ (recs(𝐹) ∪ {⟨dom recs(𝐹), (𝐹‘recs(𝐹))⟩}) Fn suc dom recs(𝐹))
2320, 22sylibr 224 1 (dom recs(𝐹) ∈ On → 𝐶 Fn suc dom recs(𝐹))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 384   = wceq 1480   ∈ wcel 1987  {cab 2607  ∀wral 2908  ∃wrex 2909  Vcvv 3190   ∪ cun 3558   ∩ cin 3559  ∅c0 3897  {csn 4155  ⟨cop 4161  dom cdm 5084   ↾ cres 5086  Ord word 5691  Oncon0 5692  suc csuc 5694  Fun wfun 5851   Fn wfn 5852  ‘cfv 5857  recscrecs 7427 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4751  ax-nul 4759  ax-pow 4813  ax-pr 4877  ax-un 6914 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2913  df-rex 2914  df-rab 2917  df-v 3192  df-sbc 3423  df-csb 3520  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-pss 3576  df-nul 3898  df-if 4065  df-sn 4156  df-pr 4158  df-tp 4160  df-op 4162  df-uni 4410  df-iun 4494  df-br 4624  df-opab 4684  df-mpt 4685  df-tr 4723  df-eprel 4995  df-id 4999  df-po 5005  df-so 5006  df-fr 5043  df-we 5045  df-xp 5090  df-rel 5091  df-cnv 5092  df-co 5093  df-dm 5094  df-rn 5095  df-res 5096  df-ima 5097  df-pred 5649  df-ord 5695  df-on 5696  df-suc 5698  df-iota 5820  df-fun 5859  df-fn 5860  df-fv 5865  df-wrecs 7367  df-recs 7428 This theorem is referenced by:  tfrlem11  7444  tfrlem12  7445  tfrlem13  7446
 Copyright terms: Public domain W3C validator