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

Theorem wfrlem13 7372
 Description: Lemma for well-founded recursion. From here through wfrlem16 7375, we aim to prove that dom 𝐹 = 𝐴. We do this by supposing that there is an element 𝑧 of 𝐴 that is not in dom 𝐹. We then define 𝐶 by extending dom 𝐹 with the appropriate value at 𝑧. We then show that 𝑧 cannot be an 𝑅 minimal element of (𝐴 ∖ dom 𝐹), meaning that (𝐴 ∖ dom 𝐹) must be empty, so dom 𝐹 = 𝐴. Here, we show that 𝐶 is a function extending the domain of 𝐹 by one. (Contributed by Scott Fenton, 21-Apr-2011.) (Revised by Mario Carneiro, 26-Jun-2015.)
Hypotheses
Ref Expression
wfrlem13.1 𝑅 We 𝐴
wfrlem13.2 𝑅 Se 𝐴
wfrlem13.3 𝐹 = wrecs(𝑅, 𝐴, 𝐺)
wfrlem13.4 𝐶 = (𝐹 ∪ {⟨𝑧, (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩})
Assertion
Ref Expression
wfrlem13 (𝑧 ∈ (𝐴 ∖ dom 𝐹) → 𝐶 Fn (dom 𝐹 ∪ {𝑧}))
Distinct variable groups:   𝑧,𝐴   𝑧,𝐹   𝑧,𝑅
Allowed substitution hints:   𝐶(𝑧)   𝐺(𝑧)

Proof of Theorem wfrlem13
StepHypRef Expression
1 wfrlem13.1 . . . . . 6 𝑅 We 𝐴
2 wfrlem13.2 . . . . . 6 𝑅 Se 𝐴
3 wfrlem13.3 . . . . . 6 𝐹 = wrecs(𝑅, 𝐴, 𝐺)
41, 2, 3wfrfun 7370 . . . . 5 Fun 𝐹
5 vex 3189 . . . . . 6 𝑧 ∈ V
6 fvex 6158 . . . . . 6 (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧))) ∈ V
75, 6funsn 5897 . . . . 5 Fun {⟨𝑧, (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩}
84, 7pm3.2i 471 . . . 4 (Fun 𝐹 ∧ Fun {⟨𝑧, (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩})
96dmsnop 5568 . . . . . 6 dom {⟨𝑧, (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩} = {𝑧}
109ineq2i 3789 . . . . 5 (dom 𝐹 ∩ dom {⟨𝑧, (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩}) = (dom 𝐹 ∩ {𝑧})
11 eldifn 3711 . . . . . 6 (𝑧 ∈ (𝐴 ∖ dom 𝐹) → ¬ 𝑧 ∈ dom 𝐹)
12 disjsn 4216 . . . . . 6 ((dom 𝐹 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ dom 𝐹)
1311, 12sylibr 224 . . . . 5 (𝑧 ∈ (𝐴 ∖ dom 𝐹) → (dom 𝐹 ∩ {𝑧}) = ∅)
1410, 13syl5eq 2667 . . . 4 (𝑧 ∈ (𝐴 ∖ dom 𝐹) → (dom 𝐹 ∩ dom {⟨𝑧, (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩}) = ∅)
15 funun 5890 . . . 4 (((Fun 𝐹 ∧ Fun {⟨𝑧, (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩}) ∧ (dom 𝐹 ∩ dom {⟨𝑧, (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩}) = ∅) → Fun (𝐹 ∪ {⟨𝑧, (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩}))
168, 14, 15sylancr 694 . . 3 (𝑧 ∈ (𝐴 ∖ dom 𝐹) → Fun (𝐹 ∪ {⟨𝑧, (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩}))
17 dmun 5291 . . . 4 dom (𝐹 ∪ {⟨𝑧, (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩}) = (dom 𝐹 ∪ dom {⟨𝑧, (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩})
189uneq2i 3742 . . . 4 (dom 𝐹 ∪ dom {⟨𝑧, (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩}) = (dom 𝐹 ∪ {𝑧})
1917, 18eqtri 2643 . . 3 dom (𝐹 ∪ {⟨𝑧, (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩}) = (dom 𝐹 ∪ {𝑧})
2016, 19jctir 560 . 2 (𝑧 ∈ (𝐴 ∖ dom 𝐹) → (Fun (𝐹 ∪ {⟨𝑧, (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩}) ∧ dom (𝐹 ∪ {⟨𝑧, (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩}) = (dom 𝐹 ∪ {𝑧})))
21 wfrlem13.4 . . . 4 𝐶 = (𝐹 ∪ {⟨𝑧, (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩})
2221fneq1i 5943 . . 3 (𝐶 Fn (dom 𝐹 ∪ {𝑧}) ↔ (𝐹 ∪ {⟨𝑧, (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩}) Fn (dom 𝐹 ∪ {𝑧}))
23 df-fn 5850 . . 3 ((𝐹 ∪ {⟨𝑧, (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩}) Fn (dom 𝐹 ∪ {𝑧}) ↔ (Fun (𝐹 ∪ {⟨𝑧, (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩}) ∧ dom (𝐹 ∪ {⟨𝑧, (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩}) = (dom 𝐹 ∪ {𝑧})))
2422, 23bitri 264 . 2 (𝐶 Fn (dom 𝐹 ∪ {𝑧}) ↔ (Fun (𝐹 ∪ {⟨𝑧, (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩}) ∧ dom (𝐹 ∪ {⟨𝑧, (𝐺‘(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩}) = (dom 𝐹 ∪ {𝑧})))
2520, 24sylibr 224 1 (𝑧 ∈ (𝐴 ∖ dom 𝐹) → 𝐶 Fn (dom 𝐹 ∪ {𝑧}))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 384   = wceq 1480   ∈ wcel 1987   ∖ cdif 3552   ∪ cun 3553   ∩ cin 3554  ∅c0 3891  {csn 4148  ⟨cop 4154   Se wse 5031   We wwe 5032  dom cdm 5074   ↾ cres 5076  Predcpred 5638  Fun wfun 5841   Fn wfn 5842  ‘cfv 5847  wrecscwrecs 7351 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 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867 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 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3188  df-sbc 3418  df-csb 3515  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-nul 3892  df-if 4059  df-sn 4149  df-pr 4151  df-op 4155  df-uni 4403  df-iun 4487  df-br 4614  df-opab 4674  df-mpt 4675  df-id 4989  df-po 4995  df-so 4996  df-fr 5033  df-se 5034  df-we 5035  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087  df-pred 5639  df-iota 5810  df-fun 5849  df-fn 5850  df-fv 5855  df-wrecs 7352 This theorem is referenced by:  wfrlem14  7373  wfrlem15  7374
 Copyright terms: Public domain W3C validator