Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  frrlem1 Structured version   Visualization version   GIF version

Theorem frrlem1 32641
Description: Lemma for founded recursion. The final item we are interested in is the union of acceptable functions 𝐵. This lemma just changes bound variables for later use. (Contributed by Paul Chapman, 21-Apr-2012.)
Hypothesis
Ref Expression
frrlem1.1 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}
Assertion
Ref Expression
frrlem1 𝐵 = {𝑔 ∣ ∃𝑧(𝑔 Fn 𝑧 ∧ (𝑧𝐴 ∧ ∀𝑤𝑧 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑧) ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝑤𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑤))))}
Distinct variable groups:   𝐴,𝑓,𝑔,𝑤,𝑥,𝑦,𝑧   𝑓,𝐺,𝑔,𝑤,𝑥,𝑦,𝑧   𝑅,𝑓,𝑔,𝑤,𝑥,𝑦,𝑧
Allowed substitution hints:   𝐵(𝑥,𝑦,𝑧,𝑤,𝑓,𝑔)

Proof of Theorem frrlem1
StepHypRef Expression
1 frrlem1.1 . 2 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}
2 fneq1 6277 . . . . . 6 (𝑓 = 𝑔 → (𝑓 Fn 𝑥𝑔 Fn 𝑥))
3 fveq1 6498 . . . . . . . 8 (𝑓 = 𝑔 → (𝑓𝑦) = (𝑔𝑦))
4 reseq1 5689 . . . . . . . . 9 (𝑓 = 𝑔 → (𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)) = (𝑔 ↾ Pred(𝑅, 𝐴, 𝑦)))
54oveq2d 6992 . . . . . . . 8 (𝑓 = 𝑔 → (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))) = (𝑦𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑦))))
63, 5eqeq12d 2794 . . . . . . 7 (𝑓 = 𝑔 → ((𝑓𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))) ↔ (𝑔𝑦) = (𝑦𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑦)))))
76ralbidv 3148 . . . . . 6 (𝑓 = 𝑔 → (∀𝑦𝑥 (𝑓𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))) ↔ ∀𝑦𝑥 (𝑔𝑦) = (𝑦𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑦)))))
82, 73anbi13d 1417 . . . . 5 (𝑓 = 𝑔 → ((𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))) ↔ (𝑔 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑔𝑦) = (𝑦𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑦))))))
98exbidv 1880 . . . 4 (𝑓 = 𝑔 → (∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))) ↔ ∃𝑥(𝑔 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑔𝑦) = (𝑦𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑦))))))
10 fneq2 6278 . . . . . 6 (𝑥 = 𝑧 → (𝑔 Fn 𝑥𝑔 Fn 𝑧))
11 sseq1 3883 . . . . . . 7 (𝑥 = 𝑧 → (𝑥𝐴𝑧𝐴))
12 sseq2 3884 . . . . . . . . 9 (𝑥 = 𝑧 → (Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥 ↔ Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑧))
1312raleqbi1dv 3344 . . . . . . . 8 (𝑥 = 𝑧 → (∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥 ↔ ∀𝑦𝑧 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑧))
14 predeq3 5990 . . . . . . . . . 10 (𝑦 = 𝑤 → Pred(𝑅, 𝐴, 𝑦) = Pred(𝑅, 𝐴, 𝑤))
1514sseq1d 3889 . . . . . . . . 9 (𝑦 = 𝑤 → (Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑧 ↔ Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑧))
1615cbvralv 3384 . . . . . . . 8 (∀𝑦𝑧 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑧 ↔ ∀𝑤𝑧 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑧)
1713, 16syl6bb 279 . . . . . . 7 (𝑥 = 𝑧 → (∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥 ↔ ∀𝑤𝑧 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑧))
1811, 17anbi12d 621 . . . . . 6 (𝑥 = 𝑧 → ((𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ↔ (𝑧𝐴 ∧ ∀𝑤𝑧 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑧)))
19 raleq 3346 . . . . . . 7 (𝑥 = 𝑧 → (∀𝑦𝑥 (𝑔𝑦) = (𝑦𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑦))) ↔ ∀𝑦𝑧 (𝑔𝑦) = (𝑦𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑦)))))
20 fveq2 6499 . . . . . . . . 9 (𝑦 = 𝑤 → (𝑔𝑦) = (𝑔𝑤))
21 id 22 . . . . . . . . . 10 (𝑦 = 𝑤𝑦 = 𝑤)
2214reseq2d 5695 . . . . . . . . . 10 (𝑦 = 𝑤 → (𝑔 ↾ Pred(𝑅, 𝐴, 𝑦)) = (𝑔 ↾ Pred(𝑅, 𝐴, 𝑤)))
2321, 22oveq12d 6994 . . . . . . . . 9 (𝑦 = 𝑤 → (𝑦𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑦))) = (𝑤𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑤))))
2420, 23eqeq12d 2794 . . . . . . . 8 (𝑦 = 𝑤 → ((𝑔𝑦) = (𝑦𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑦))) ↔ (𝑔𝑤) = (𝑤𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑤)))))
2524cbvralv 3384 . . . . . . 7 (∀𝑦𝑧 (𝑔𝑦) = (𝑦𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑦))) ↔ ∀𝑤𝑧 (𝑔𝑤) = (𝑤𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑤))))
2619, 25syl6bb 279 . . . . . 6 (𝑥 = 𝑧 → (∀𝑦𝑥 (𝑔𝑦) = (𝑦𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑦))) ↔ ∀𝑤𝑧 (𝑔𝑤) = (𝑤𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑤)))))
2710, 18, 263anbi123d 1415 . . . . 5 (𝑥 = 𝑧 → ((𝑔 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑔𝑦) = (𝑦𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑦)))) ↔ (𝑔 Fn 𝑧 ∧ (𝑧𝐴 ∧ ∀𝑤𝑧 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑧) ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝑤𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑤))))))
2827cbvexvw 1994 . . . 4 (∃𝑥(𝑔 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑔𝑦) = (𝑦𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑦)))) ↔ ∃𝑧(𝑔 Fn 𝑧 ∧ (𝑧𝐴 ∧ ∀𝑤𝑧 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑧) ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝑤𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑤)))))
299, 28syl6bb 279 . . 3 (𝑓 = 𝑔 → (∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))) ↔ ∃𝑧(𝑔 Fn 𝑧 ∧ (𝑧𝐴 ∧ ∀𝑤𝑧 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑧) ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝑤𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑤))))))
3029cbvabv 2911 . 2 {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} = {𝑔 ∣ ∃𝑧(𝑔 Fn 𝑧 ∧ (𝑧𝐴 ∧ ∀𝑤𝑧 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑧) ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝑤𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑤))))}
311, 30eqtri 2803 1 𝐵 = {𝑔 ∣ ∃𝑧(𝑔 Fn 𝑧 ∧ (𝑧𝐴 ∧ ∀𝑤𝑧 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑧) ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝑤𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑤))))}
Colors of variables: wff setvar class
Syntax hints:  wa 387  w3a 1068   = wceq 1507  wex 1742  {cab 2759  wral 3089  wss 3830  cres 5409  Predcpred 5985   Fn wfn 6183  cfv 6188  (class class class)co 6976
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2751
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-clab 2760  df-cleq 2772  df-clel 2847  df-nfc 2919  df-ral 3094  df-rex 3095  df-rab 3098  df-v 3418  df-dif 3833  df-un 3835  df-in 3837  df-ss 3844  df-nul 4180  df-if 4351  df-sn 4442  df-pr 4444  df-op 4448  df-uni 4713  df-br 4930  df-opab 4992  df-xp 5413  df-rel 5414  df-cnv 5415  df-co 5416  df-dm 5417  df-rn 5418  df-res 5419  df-ima 5420  df-pred 5986  df-iota 6152  df-fun 6190  df-fn 6191  df-fv 6196  df-ov 6979
This theorem is referenced by:  frrlem2  32642  frrlem3  32643  frrlem4  32644  frrlem8  32648  frrlem12  32652  frrlem13  32653  fpr1  32657  fpr2  32658  frr1  32662  frr2  32663
  Copyright terms: Public domain W3C validator