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

Theorem frrlem5e 31913
 Description: Lemma for founded recursion. The domain of the union of a subset of 𝐵 is closed under predecessors. (Contributed by Paul Chapman, 1-May-2012.)
Hypotheses
Ref Expression
frrlem5.1 𝑅 Fr 𝐴
frrlem5.2 𝑅 Se 𝐴
frrlem5.3 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}
Assertion
Ref Expression
frrlem5e (𝐶𝐵 → (𝑋 ∈ dom 𝐶 → Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝐶))
Distinct variable groups:   𝐴,𝑓,𝑥,𝑦   𝑓,𝐺,𝑥,𝑦   𝑅,𝑓,𝑥,𝑦   𝑥,𝐵
Allowed substitution hints:   𝐵(𝑦,𝑓)   𝐶(𝑥,𝑦,𝑓)   𝑋(𝑥,𝑦,𝑓)

Proof of Theorem frrlem5e
Dummy variables 𝑧 𝑡 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dmuni 5366 . . . 4 dom 𝐶 = 𝑧𝐶 dom 𝑧
21eleq2i 2722 . . 3 (𝑋 ∈ dom 𝐶𝑋 𝑧𝐶 dom 𝑧)
3 eliun 4556 . . 3 (𝑋 𝑧𝐶 dom 𝑧 ↔ ∃𝑧𝐶 𝑋 ∈ dom 𝑧)
42, 3bitri 264 . 2 (𝑋 ∈ dom 𝐶 ↔ ∃𝑧𝐶 𝑋 ∈ dom 𝑧)
5 ssel2 3631 . . . . 5 ((𝐶𝐵𝑧𝐶) → 𝑧𝐵)
6 frrlem5.3 . . . . . . . 8 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}
76frrlem1 31905 . . . . . . 7 𝐵 = {𝑧 ∣ ∃𝑤(𝑧 Fn 𝑤 ∧ (𝑤𝐴 ∧ ∀𝑡𝑤 Pred(𝑅, 𝐴, 𝑡) ⊆ 𝑤) ∧ ∀𝑡𝑤 (𝑧𝑡) = (𝑡𝐺(𝑧 ↾ Pred(𝑅, 𝐴, 𝑡))))}
87abeq2i 2764 . . . . . 6 (𝑧𝐵 ↔ ∃𝑤(𝑧 Fn 𝑤 ∧ (𝑤𝐴 ∧ ∀𝑡𝑤 Pred(𝑅, 𝐴, 𝑡) ⊆ 𝑤) ∧ ∀𝑡𝑤 (𝑧𝑡) = (𝑡𝐺(𝑧 ↾ Pred(𝑅, 𝐴, 𝑡)))))
9 predeq3 5722 . . . . . . . . . . . 12 (𝑡 = 𝑋 → Pred(𝑅, 𝐴, 𝑡) = Pred(𝑅, 𝐴, 𝑋))
109sseq1d 3665 . . . . . . . . . . 11 (𝑡 = 𝑋 → (Pred(𝑅, 𝐴, 𝑡) ⊆ 𝑤 ↔ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝑤))
1110rspccv 3337 . . . . . . . . . 10 (∀𝑡𝑤 Pred(𝑅, 𝐴, 𝑡) ⊆ 𝑤 → (𝑋𝑤 → Pred(𝑅, 𝐴, 𝑋) ⊆ 𝑤))
1211ad2antlr 763 . . . . . . . . 9 (((𝑤𝐴 ∧ ∀𝑡𝑤 Pred(𝑅, 𝐴, 𝑡) ⊆ 𝑤) ∧ ∀𝑡𝑤 (𝑧𝑡) = (𝑡𝐺(𝑧 ↾ Pred(𝑅, 𝐴, 𝑡)))) → (𝑋𝑤 → Pred(𝑅, 𝐴, 𝑋) ⊆ 𝑤))
13 fndm 6028 . . . . . . . . . . 11 (𝑧 Fn 𝑤 → dom 𝑧 = 𝑤)
1413eleq2d 2716 . . . . . . . . . 10 (𝑧 Fn 𝑤 → (𝑋 ∈ dom 𝑧𝑋𝑤))
1513sseq2d 3666 . . . . . . . . . 10 (𝑧 Fn 𝑤 → (Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑧 ↔ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝑤))
1614, 15imbi12d 333 . . . . . . . . 9 (𝑧 Fn 𝑤 → ((𝑋 ∈ dom 𝑧 → Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑧) ↔ (𝑋𝑤 → Pred(𝑅, 𝐴, 𝑋) ⊆ 𝑤)))
1712, 16syl5ibr 236 . . . . . . . 8 (𝑧 Fn 𝑤 → (((𝑤𝐴 ∧ ∀𝑡𝑤 Pred(𝑅, 𝐴, 𝑡) ⊆ 𝑤) ∧ ∀𝑡𝑤 (𝑧𝑡) = (𝑡𝐺(𝑧 ↾ Pred(𝑅, 𝐴, 𝑡)))) → (𝑋 ∈ dom 𝑧 → Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑧)))
18173impib 1281 . . . . . . 7 ((𝑧 Fn 𝑤 ∧ (𝑤𝐴 ∧ ∀𝑡𝑤 Pred(𝑅, 𝐴, 𝑡) ⊆ 𝑤) ∧ ∀𝑡𝑤 (𝑧𝑡) = (𝑡𝐺(𝑧 ↾ Pred(𝑅, 𝐴, 𝑡)))) → (𝑋 ∈ dom 𝑧 → Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑧))
1918exlimiv 1898 . . . . . 6 (∃𝑤(𝑧 Fn 𝑤 ∧ (𝑤𝐴 ∧ ∀𝑡𝑤 Pred(𝑅, 𝐴, 𝑡) ⊆ 𝑤) ∧ ∀𝑡𝑤 (𝑧𝑡) = (𝑡𝐺(𝑧 ↾ Pred(𝑅, 𝐴, 𝑡)))) → (𝑋 ∈ dom 𝑧 → Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑧))
208, 19sylbi 207 . . . . 5 (𝑧𝐵 → (𝑋 ∈ dom 𝑧 → Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑧))
215, 20syl 17 . . . 4 ((𝐶𝐵𝑧𝐶) → (𝑋 ∈ dom 𝑧 → Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑧))
22 dmeq 5356 . . . . . . . . . 10 (𝑤 = 𝑧 → dom 𝑤 = dom 𝑧)
2322sseq2d 3666 . . . . . . . . 9 (𝑤 = 𝑧 → (Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑤 ↔ Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑧))
2423rspcev 3340 . . . . . . . 8 ((𝑧𝐶 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑧) → ∃𝑤𝐶 Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑤)
25 ssiun 4594 . . . . . . . 8 (∃𝑤𝐶 Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑤 → Pred(𝑅, 𝐴, 𝑋) ⊆ 𝑤𝐶 dom 𝑤)
2624, 25syl 17 . . . . . . 7 ((𝑧𝐶 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑧) → Pred(𝑅, 𝐴, 𝑋) ⊆ 𝑤𝐶 dom 𝑤)
27 dmuni 5366 . . . . . . 7 dom 𝐶 = 𝑤𝐶 dom 𝑤
2826, 27syl6sseqr 3685 . . . . . 6 ((𝑧𝐶 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑧) → Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝐶)
2928ex 449 . . . . 5 (𝑧𝐶 → (Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑧 → Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝐶))
3029adantl 481 . . . 4 ((𝐶𝐵𝑧𝐶) → (Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑧 → Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝐶))
3121, 30syld 47 . . 3 ((𝐶𝐵𝑧𝐶) → (𝑋 ∈ dom 𝑧 → Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝐶))
3231rexlimdva 3060 . 2 (𝐶𝐵 → (∃𝑧𝐶 𝑋 ∈ dom 𝑧 → Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝐶))
334, 32syl5bi 232 1 (𝐶𝐵 → (𝑋 ∈ dom 𝐶 → Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝐶))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1054   = wceq 1523  ∃wex 1744   ∈ wcel 2030  {cab 2637  ∀wral 2941  ∃wrex 2942   ⊆ wss 3607  ∪ cuni 4468  ∪ ciun 4552   Fr wfr 5099   Se wse 5100  dom cdm 5143   ↾ cres 5145  Predcpred 5717   Fn wfn 5921  ‘cfv 5926  (class class class)co 6690 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-iun 4554  df-br 4686  df-opab 4746  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-iota 5889  df-fun 5928  df-fn 5929  df-fv 5934  df-ov 6693 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator