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

Theorem frrlem8 33137
 Description: Lemma for founded recursion. dom 𝐹 is closed under predecessor classes. (Contributed by Scott Fenton, 6-Dec-2022.)
Hypotheses
Ref Expression
frrlem5.1 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}
frrlem5.2 𝐹 = frecs(𝑅, 𝐴, 𝐺)
Assertion
Ref Expression
frrlem8 (𝑧 ∈ dom 𝐹 → Pred(𝑅, 𝐴, 𝑧) ⊆ dom 𝐹)
Distinct variable groups:   𝐴,𝑓,𝑥,𝑦   𝑓,𝐺,𝑥,𝑦   𝑅,𝑓,𝑥,𝑦   𝑦,𝐹   𝑧,𝐴,𝑓,𝑥,𝑦   𝑧,𝑅   𝑧,𝐺
Allowed substitution hints:   𝐵(𝑥,𝑦,𝑧,𝑓)   𝐹(𝑥,𝑧,𝑓)

Proof of Theorem frrlem8
Dummy variables 𝑔 𝑎 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 vex 3474 . . 3 𝑧 ∈ V
21eldm2 5743 . 2 (𝑧 ∈ dom 𝐹 ↔ ∃𝑤𝑧, 𝑤⟩ ∈ 𝐹)
3 frrlem5.1 . . . . . . . 8 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}
4 frrlem5.2 . . . . . . . 8 𝐹 = frecs(𝑅, 𝐴, 𝐺)
53, 4frrlem5 33134 . . . . . . 7 𝐹 = 𝐵
63frrlem1 33130 . . . . . . . 8 𝐵 = {𝑔 ∣ ∃𝑎(𝑔 Fn 𝑎 ∧ (𝑎𝐴 ∧ ∀𝑧𝑎 Pred(𝑅, 𝐴, 𝑧) ⊆ 𝑎) ∧ ∀𝑧𝑎 (𝑔𝑧) = (𝑧𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑧))))}
76unieqi 4824 . . . . . . 7 𝐵 = {𝑔 ∣ ∃𝑎(𝑔 Fn 𝑎 ∧ (𝑎𝐴 ∧ ∀𝑧𝑎 Pred(𝑅, 𝐴, 𝑧) ⊆ 𝑎) ∧ ∀𝑧𝑎 (𝑔𝑧) = (𝑧𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑧))))}
85, 7eqtri 2844 . . . . . 6 𝐹 = {𝑔 ∣ ∃𝑎(𝑔 Fn 𝑎 ∧ (𝑎𝐴 ∧ ∀𝑧𝑎 Pred(𝑅, 𝐴, 𝑧) ⊆ 𝑎) ∧ ∀𝑧𝑎 (𝑔𝑧) = (𝑧𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑧))))}
98eleq2i 2903 . . . . 5 (⟨𝑧, 𝑤⟩ ∈ 𝐹 ↔ ⟨𝑧, 𝑤⟩ ∈ {𝑔 ∣ ∃𝑎(𝑔 Fn 𝑎 ∧ (𝑎𝐴 ∧ ∀𝑧𝑎 Pred(𝑅, 𝐴, 𝑧) ⊆ 𝑎) ∧ ∀𝑧𝑎 (𝑔𝑧) = (𝑧𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑧))))})
10 eluniab 4826 . . . . 5 (⟨𝑧, 𝑤⟩ ∈ {𝑔 ∣ ∃𝑎(𝑔 Fn 𝑎 ∧ (𝑎𝐴 ∧ ∀𝑧𝑎 Pred(𝑅, 𝐴, 𝑧) ⊆ 𝑎) ∧ ∀𝑧𝑎 (𝑔𝑧) = (𝑧𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑧))))} ↔ ∃𝑔(⟨𝑧, 𝑤⟩ ∈ 𝑔 ∧ ∃𝑎(𝑔 Fn 𝑎 ∧ (𝑎𝐴 ∧ ∀𝑧𝑎 Pred(𝑅, 𝐴, 𝑧) ⊆ 𝑎) ∧ ∀𝑧𝑎 (𝑔𝑧) = (𝑧𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑧))))))
119, 10bitri 278 . . . 4 (⟨𝑧, 𝑤⟩ ∈ 𝐹 ↔ ∃𝑔(⟨𝑧, 𝑤⟩ ∈ 𝑔 ∧ ∃𝑎(𝑔 Fn 𝑎 ∧ (𝑎𝐴 ∧ ∀𝑧𝑎 Pred(𝑅, 𝐴, 𝑧) ⊆ 𝑎) ∧ ∀𝑧𝑎 (𝑔𝑧) = (𝑧𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑧))))))
12 simpr2r 1230 . . . . . . . . . . 11 ((⟨𝑧, 𝑤⟩ ∈ 𝑔 ∧ (𝑔 Fn 𝑎 ∧ (𝑎𝐴 ∧ ∀𝑧𝑎 Pred(𝑅, 𝐴, 𝑧) ⊆ 𝑎) ∧ ∀𝑧𝑎 (𝑔𝑧) = (𝑧𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑧))))) → ∀𝑧𝑎 Pred(𝑅, 𝐴, 𝑧) ⊆ 𝑎)
13 vex 3474 . . . . . . . . . . . . . 14 𝑤 ∈ V
141, 13opeldm 5749 . . . . . . . . . . . . 13 (⟨𝑧, 𝑤⟩ ∈ 𝑔𝑧 ∈ dom 𝑔)
1514adantr 484 . . . . . . . . . . . 12 ((⟨𝑧, 𝑤⟩ ∈ 𝑔 ∧ (𝑔 Fn 𝑎 ∧ (𝑎𝐴 ∧ ∀𝑧𝑎 Pred(𝑅, 𝐴, 𝑧) ⊆ 𝑎) ∧ ∀𝑧𝑎 (𝑔𝑧) = (𝑧𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑧))))) → 𝑧 ∈ dom 𝑔)
16 simpr1 1191 . . . . . . . . . . . . 13 ((⟨𝑧, 𝑤⟩ ∈ 𝑔 ∧ (𝑔 Fn 𝑎 ∧ (𝑎𝐴 ∧ ∀𝑧𝑎 Pred(𝑅, 𝐴, 𝑧) ⊆ 𝑎) ∧ ∀𝑧𝑎 (𝑔𝑧) = (𝑧𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑧))))) → 𝑔 Fn 𝑎)
17 fndm 6428 . . . . . . . . . . . . 13 (𝑔 Fn 𝑎 → dom 𝑔 = 𝑎)
1816, 17syl 17 . . . . . . . . . . . 12 ((⟨𝑧, 𝑤⟩ ∈ 𝑔 ∧ (𝑔 Fn 𝑎 ∧ (𝑎𝐴 ∧ ∀𝑧𝑎 Pred(𝑅, 𝐴, 𝑧) ⊆ 𝑎) ∧ ∀𝑧𝑎 (𝑔𝑧) = (𝑧𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑧))))) → dom 𝑔 = 𝑎)
1915, 18eleqtrd 2914 . . . . . . . . . . 11 ((⟨𝑧, 𝑤⟩ ∈ 𝑔 ∧ (𝑔 Fn 𝑎 ∧ (𝑎𝐴 ∧ ∀𝑧𝑎 Pred(𝑅, 𝐴, 𝑧) ⊆ 𝑎) ∧ ∀𝑧𝑎 (𝑔𝑧) = (𝑧𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑧))))) → 𝑧𝑎)
20 rsp 3193 . . . . . . . . . . 11 (∀𝑧𝑎 Pred(𝑅, 𝐴, 𝑧) ⊆ 𝑎 → (𝑧𝑎 → Pred(𝑅, 𝐴, 𝑧) ⊆ 𝑎))
2112, 19, 20sylc 65 . . . . . . . . . 10 ((⟨𝑧, 𝑤⟩ ∈ 𝑔 ∧ (𝑔 Fn 𝑎 ∧ (𝑎𝐴 ∧ ∀𝑧𝑎 Pred(𝑅, 𝐴, 𝑧) ⊆ 𝑎) ∧ ∀𝑧𝑎 (𝑔𝑧) = (𝑧𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑧))))) → Pred(𝑅, 𝐴, 𝑧) ⊆ 𝑎)
2221, 18sseqtrrd 3984 . . . . . . . . 9 ((⟨𝑧, 𝑤⟩ ∈ 𝑔 ∧ (𝑔 Fn 𝑎 ∧ (𝑎𝐴 ∧ ∀𝑧𝑎 Pred(𝑅, 𝐴, 𝑧) ⊆ 𝑎) ∧ ∀𝑧𝑎 (𝑔𝑧) = (𝑧𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑧))))) → Pred(𝑅, 𝐴, 𝑧) ⊆ dom 𝑔)
23 19.8a 2181 . . . . . . . . . . . . . 14 ((𝑔 Fn 𝑎 ∧ (𝑎𝐴 ∧ ∀𝑧𝑎 Pred(𝑅, 𝐴, 𝑧) ⊆ 𝑎) ∧ ∀𝑧𝑎 (𝑔𝑧) = (𝑧𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑧)))) → ∃𝑎(𝑔 Fn 𝑎 ∧ (𝑎𝐴 ∧ ∀𝑧𝑎 Pred(𝑅, 𝐴, 𝑧) ⊆ 𝑎) ∧ ∀𝑧𝑎 (𝑔𝑧) = (𝑧𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑧)))))
246abeq2i 2947 . . . . . . . . . . . . . 14 (𝑔𝐵 ↔ ∃𝑎(𝑔 Fn 𝑎 ∧ (𝑎𝐴 ∧ ∀𝑧𝑎 Pred(𝑅, 𝐴, 𝑧) ⊆ 𝑎) ∧ ∀𝑧𝑎 (𝑔𝑧) = (𝑧𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑧)))))
2523, 24sylibr 237 . . . . . . . . . . . . 13 ((𝑔 Fn 𝑎 ∧ (𝑎𝐴 ∧ ∀𝑧𝑎 Pred(𝑅, 𝐴, 𝑧) ⊆ 𝑎) ∧ ∀𝑧𝑎 (𝑔𝑧) = (𝑧𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑧)))) → 𝑔𝐵)
2625adantl 485 . . . . . . . . . . . 12 ((⟨𝑧, 𝑤⟩ ∈ 𝑔 ∧ (𝑔 Fn 𝑎 ∧ (𝑎𝐴 ∧ ∀𝑧𝑎 Pred(𝑅, 𝐴, 𝑧) ⊆ 𝑎) ∧ ∀𝑧𝑎 (𝑔𝑧) = (𝑧𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑧))))) → 𝑔𝐵)
27 elssuni 4841 . . . . . . . . . . . 12 (𝑔𝐵𝑔 𝐵)
2826, 27syl 17 . . . . . . . . . . 11 ((⟨𝑧, 𝑤⟩ ∈ 𝑔 ∧ (𝑔 Fn 𝑎 ∧ (𝑎𝐴 ∧ ∀𝑧𝑎 Pred(𝑅, 𝐴, 𝑧) ⊆ 𝑎) ∧ ∀𝑧𝑎 (𝑔𝑧) = (𝑧𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑧))))) → 𝑔 𝐵)
2928, 5sseqtrrdi 3994 . . . . . . . . . 10 ((⟨𝑧, 𝑤⟩ ∈ 𝑔 ∧ (𝑔 Fn 𝑎 ∧ (𝑎𝐴 ∧ ∀𝑧𝑎 Pred(𝑅, 𝐴, 𝑧) ⊆ 𝑎) ∧ ∀𝑧𝑎 (𝑔𝑧) = (𝑧𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑧))))) → 𝑔𝐹)
30 dmss 5744 . . . . . . . . . 10 (𝑔𝐹 → dom 𝑔 ⊆ dom 𝐹)
3129, 30syl 17 . . . . . . . . 9 ((⟨𝑧, 𝑤⟩ ∈ 𝑔 ∧ (𝑔 Fn 𝑎 ∧ (𝑎𝐴 ∧ ∀𝑧𝑎 Pred(𝑅, 𝐴, 𝑧) ⊆ 𝑎) ∧ ∀𝑧𝑎 (𝑔𝑧) = (𝑧𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑧))))) → dom 𝑔 ⊆ dom 𝐹)
3222, 31sstrd 3953 . . . . . . . 8 ((⟨𝑧, 𝑤⟩ ∈ 𝑔 ∧ (𝑔 Fn 𝑎 ∧ (𝑎𝐴 ∧ ∀𝑧𝑎 Pred(𝑅, 𝐴, 𝑧) ⊆ 𝑎) ∧ ∀𝑧𝑎 (𝑔𝑧) = (𝑧𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑧))))) → Pred(𝑅, 𝐴, 𝑧) ⊆ dom 𝐹)
3332expcom 417 . . . . . . 7 ((𝑔 Fn 𝑎 ∧ (𝑎𝐴 ∧ ∀𝑧𝑎 Pred(𝑅, 𝐴, 𝑧) ⊆ 𝑎) ∧ ∀𝑧𝑎 (𝑔𝑧) = (𝑧𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑧)))) → (⟨𝑧, 𝑤⟩ ∈ 𝑔 → Pred(𝑅, 𝐴, 𝑧) ⊆ dom 𝐹))
3433exlimiv 1932 . . . . . 6 (∃𝑎(𝑔 Fn 𝑎 ∧ (𝑎𝐴 ∧ ∀𝑧𝑎 Pred(𝑅, 𝐴, 𝑧) ⊆ 𝑎) ∧ ∀𝑧𝑎 (𝑔𝑧) = (𝑧𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑧)))) → (⟨𝑧, 𝑤⟩ ∈ 𝑔 → Pred(𝑅, 𝐴, 𝑧) ⊆ dom 𝐹))
3534impcom 411 . . . . 5 ((⟨𝑧, 𝑤⟩ ∈ 𝑔 ∧ ∃𝑎(𝑔 Fn 𝑎 ∧ (𝑎𝐴 ∧ ∀𝑧𝑎 Pred(𝑅, 𝐴, 𝑧) ⊆ 𝑎) ∧ ∀𝑧𝑎 (𝑔𝑧) = (𝑧𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑧))))) → Pred(𝑅, 𝐴, 𝑧) ⊆ dom 𝐹)
3635exlimiv 1932 . . . 4 (∃𝑔(⟨𝑧, 𝑤⟩ ∈ 𝑔 ∧ ∃𝑎(𝑔 Fn 𝑎 ∧ (𝑎𝐴 ∧ ∀𝑧𝑎 Pred(𝑅, 𝐴, 𝑧) ⊆ 𝑎) ∧ ∀𝑧𝑎 (𝑔𝑧) = (𝑧𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑧))))) → Pred(𝑅, 𝐴, 𝑧) ⊆ dom 𝐹)
3711, 36sylbi 220 . . 3 (⟨𝑧, 𝑤⟩ ∈ 𝐹 → Pred(𝑅, 𝐴, 𝑧) ⊆ dom 𝐹)
3837exlimiv 1932 . 2 (∃𝑤𝑧, 𝑤⟩ ∈ 𝐹 → Pred(𝑅, 𝐴, 𝑧) ⊆ dom 𝐹)
392, 38sylbi 220 1 (𝑧 ∈ dom 𝐹 → Pred(𝑅, 𝐴, 𝑧) ⊆ dom 𝐹)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084   = wceq 1538  ∃wex 1781   ∈ wcel 2115  {cab 2799  ∀wral 3126   ⊆ wss 3910  ⟨cop 4546  ∪ cuni 4811  dom cdm 5528   ↾ cres 5530  Predcpred 6120   Fn wfn 6323  ‘cfv 6328  (class class class)co 7130  frecscfrecs 33124 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2178  ax-ext 2793 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-clab 2800  df-cleq 2814  df-clel 2892  df-nfc 2960  df-ral 3131  df-rab 3135  df-v 3473  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4267  df-if 4441  df-sn 4541  df-pr 4543  df-op 4547  df-uni 4812  df-br 5040  df-opab 5102  df-xp 5534  df-rel 5535  df-cnv 5536  df-co 5537  df-dm 5538  df-rn 5539  df-res 5540  df-ima 5541  df-pred 6121  df-iota 6287  df-fun 6330  df-fn 6331  df-fv 6336  df-ov 7133  df-frecs 33125 This theorem is referenced by:  frrlem12  33141  frrlem13  33142
 Copyright terms: Public domain W3C validator