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

Theorem frrlem5e 31489
 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 5294 . . . 4 dom 𝐶 = 𝑧𝐶 dom 𝑧
21eleq2i 2690 . . 3 (𝑋 ∈ dom 𝐶𝑋 𝑧𝐶 dom 𝑧)
3 eliun 4490 . . 3 (𝑋 𝑧𝐶 dom 𝑧 ↔ ∃𝑧𝐶 𝑋 ∈ dom 𝑧)
42, 3bitri 264 . 2 (𝑋 ∈ dom 𝐶 ↔ ∃𝑧𝐶 𝑋 ∈ dom 𝑧)
5 ssel2 3578 . . . . 5 ((𝐶𝐵𝑧𝐶) → 𝑧𝐵)
6 frrlem5.3 . . . . . . . 8 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦)))))}
76frrlem1 31481 . . . . . . 7 𝐵 = {𝑧 ∣ ∃𝑤(𝑧 Fn 𝑤 ∧ (𝑤𝐴 ∧ ∀𝑡𝑤 Pred(𝑅, 𝐴, 𝑡) ⊆ 𝑤 ∧ ∀𝑡𝑤 (𝑧𝑡) = (𝑡𝐺(𝑧 ↾ Pred(𝑅, 𝐴, 𝑡)))))}
87abeq2i 2732 . . . . . 6 (𝑧𝐵 ↔ ∃𝑤(𝑧 Fn 𝑤 ∧ (𝑤𝐴 ∧ ∀𝑡𝑤 Pred(𝑅, 𝐴, 𝑡) ⊆ 𝑤 ∧ ∀𝑡𝑤 (𝑧𝑡) = (𝑡𝐺(𝑧 ↾ Pred(𝑅, 𝐴, 𝑡))))))
9 fndm 5948 . . . . . . . . 9 (𝑧 Fn 𝑤 → dom 𝑧 = 𝑤)
10 predeq3 5643 . . . . . . . . . . . . 13 (𝑡 = 𝑋 → Pred(𝑅, 𝐴, 𝑡) = Pred(𝑅, 𝐴, 𝑋))
1110sseq1d 3611 . . . . . . . . . . . 12 (𝑡 = 𝑋 → (Pred(𝑅, 𝐴, 𝑡) ⊆ 𝑤 ↔ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝑤))
1211rspccv 3292 . . . . . . . . . . 11 (∀𝑡𝑤 Pred(𝑅, 𝐴, 𝑡) ⊆ 𝑤 → (𝑋𝑤 → Pred(𝑅, 𝐴, 𝑋) ⊆ 𝑤))
13123ad2ant2 1081 . . . . . . . . . 10 ((𝑤𝐴 ∧ ∀𝑡𝑤 Pred(𝑅, 𝐴, 𝑡) ⊆ 𝑤 ∧ ∀𝑡𝑤 (𝑧𝑡) = (𝑡𝐺(𝑧 ↾ Pred(𝑅, 𝐴, 𝑡)))) → (𝑋𝑤 → Pred(𝑅, 𝐴, 𝑋) ⊆ 𝑤))
14 eleq2 2687 . . . . . . . . . . 11 (dom 𝑧 = 𝑤 → (𝑋 ∈ dom 𝑧𝑋𝑤))
15 sseq2 3606 . . . . . . . . . . 11 (dom 𝑧 = 𝑤 → (Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑧 ↔ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝑤))
1614, 15imbi12d 334 . . . . . . . . . 10 (dom 𝑧 = 𝑤 → ((𝑋 ∈ dom 𝑧 → Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑧) ↔ (𝑋𝑤 → Pred(𝑅, 𝐴, 𝑋) ⊆ 𝑤)))
1713, 16syl5ibr 236 . . . . . . . . 9 (dom 𝑧 = 𝑤 → ((𝑤𝐴 ∧ ∀𝑡𝑤 Pred(𝑅, 𝐴, 𝑡) ⊆ 𝑤 ∧ ∀𝑡𝑤 (𝑧𝑡) = (𝑡𝐺(𝑧 ↾ Pred(𝑅, 𝐴, 𝑡)))) → (𝑋 ∈ dom 𝑧 → Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑧)))
189, 17syl 17 . . . . . . . 8 (𝑧 Fn 𝑤 → ((𝑤𝐴 ∧ ∀𝑡𝑤 Pred(𝑅, 𝐴, 𝑡) ⊆ 𝑤 ∧ ∀𝑡𝑤 (𝑧𝑡) = (𝑡𝐺(𝑧 ↾ Pred(𝑅, 𝐴, 𝑡)))) → (𝑋 ∈ dom 𝑧 → Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑧)))
1918imp 445 . . . . . . 7 ((𝑧 Fn 𝑤 ∧ (𝑤𝐴 ∧ ∀𝑡𝑤 Pred(𝑅, 𝐴, 𝑡) ⊆ 𝑤 ∧ ∀𝑡𝑤 (𝑧𝑡) = (𝑡𝐺(𝑧 ↾ Pred(𝑅, 𝐴, 𝑡))))) → (𝑋 ∈ dom 𝑧 → Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑧))
2019exlimiv 1855 . . . . . 6 (∃𝑤(𝑧 Fn 𝑤 ∧ (𝑤𝐴 ∧ ∀𝑡𝑤 Pred(𝑅, 𝐴, 𝑡) ⊆ 𝑤 ∧ ∀𝑡𝑤 (𝑧𝑡) = (𝑡𝐺(𝑧 ↾ Pred(𝑅, 𝐴, 𝑡))))) → (𝑋 ∈ dom 𝑧 → Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑧))
218, 20sylbi 207 . . . . 5 (𝑧𝐵 → (𝑋 ∈ dom 𝑧 → Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑧))
225, 21syl 17 . . . 4 ((𝐶𝐵𝑧𝐶) → (𝑋 ∈ dom 𝑧 → Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑧))
23 dmeq 5284 . . . . . . . . . 10 (𝑤 = 𝑧 → dom 𝑤 = dom 𝑧)
2423sseq2d 3612 . . . . . . . . 9 (𝑤 = 𝑧 → (Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑤 ↔ Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑧))
2524rspcev 3295 . . . . . . . 8 ((𝑧𝐶 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑧) → ∃𝑤𝐶 Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑤)
26 ssiun 4528 . . . . . . . 8 (∃𝑤𝐶 Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑤 → Pred(𝑅, 𝐴, 𝑋) ⊆ 𝑤𝐶 dom 𝑤)
2725, 26syl 17 . . . . . . 7 ((𝑧𝐶 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑧) → Pred(𝑅, 𝐴, 𝑋) ⊆ 𝑤𝐶 dom 𝑤)
28 dmuni 5294 . . . . . . 7 dom 𝐶 = 𝑤𝐶 dom 𝑤
2927, 28syl6sseqr 3631 . . . . . 6 ((𝑧𝐶 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑧) → Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝐶)
3029ex 450 . . . . 5 (𝑧𝐶 → (Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑧 → Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝐶))
3130adantl 482 . . . 4 ((𝐶𝐵𝑧𝐶) → (Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑧 → Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝐶))
3222, 31syld 47 . . 3 ((𝐶𝐵𝑧𝐶) → (𝑋 ∈ dom 𝑧 → Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝐶))
3332rexlimdva 3024 . 2 (𝐶𝐵 → (∃𝑧𝐶 𝑋 ∈ dom 𝑧 → Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝐶))
344, 33syl5bi 232 1 (𝐶𝐵 → (𝑋 ∈ dom 𝐶 → Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝐶))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1036   = wceq 1480  ∃wex 1701   ∈ wcel 1987  {cab 2607  ∀wral 2907  ∃wrex 2908   ⊆ wss 3555  ∪ cuni 4402  ∪ ciun 4485   Fr wfr 5030   Se wse 5031  dom cdm 5074   ↾ cres 5076  Predcpred 5638   Fn wfn 5842  ‘cfv 5847  (class class class)co 6604 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-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3188  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-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-ov 6607 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator