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

Theorem frrlem5e 32114
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 5542 . . . 4 dom 𝐶 = 𝑧𝐶 dom 𝑧
21eleq2i 2884 . . 3 (𝑋 ∈ dom 𝐶𝑋 𝑧𝐶 dom 𝑧)
3 eliun 4723 . . 3 (𝑋 𝑧𝐶 dom 𝑧 ↔ ∃𝑧𝐶 𝑋 ∈ dom 𝑧)
42, 3bitri 266 . 2 (𝑋 ∈ dom 𝐶 ↔ ∃𝑧𝐶 𝑋 ∈ dom 𝑧)
5 ssel2 3800 . . . . 5 ((𝐶𝐵𝑧𝐶) → 𝑧𝐵)
6 frrlem5.3 . . . . . . . 8 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}
76frrlem1 32106 . . . . . . 7 𝐵 = {𝑧 ∣ ∃𝑤(𝑧 Fn 𝑤 ∧ (𝑤𝐴 ∧ ∀𝑡𝑤 Pred(𝑅, 𝐴, 𝑡) ⊆ 𝑤) ∧ ∀𝑡𝑤 (𝑧𝑡) = (𝑡𝐺(𝑧 ↾ Pred(𝑅, 𝐴, 𝑡))))}
87abeq2i 2926 . . . . . 6 (𝑧𝐵 ↔ ∃𝑤(𝑧 Fn 𝑤 ∧ (𝑤𝐴 ∧ ∀𝑡𝑤 Pred(𝑅, 𝐴, 𝑡) ⊆ 𝑤) ∧ ∀𝑡𝑤 (𝑧𝑡) = (𝑡𝐺(𝑧 ↾ Pred(𝑅, 𝐴, 𝑡)))))
9 predeq3 5904 . . . . . . . . . . . 12 (𝑡 = 𝑋 → Pred(𝑅, 𝐴, 𝑡) = Pred(𝑅, 𝐴, 𝑋))
109sseq1d 3836 . . . . . . . . . . 11 (𝑡 = 𝑋 → (Pred(𝑅, 𝐴, 𝑡) ⊆ 𝑤 ↔ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝑤))
1110rspccv 3506 . . . . . . . . . 10 (∀𝑡𝑤 Pred(𝑅, 𝐴, 𝑡) ⊆ 𝑤 → (𝑋𝑤 → Pred(𝑅, 𝐴, 𝑋) ⊆ 𝑤))
1211ad2antlr 709 . . . . . . . . 9 (((𝑤𝐴 ∧ ∀𝑡𝑤 Pred(𝑅, 𝐴, 𝑡) ⊆ 𝑤) ∧ ∀𝑡𝑤 (𝑧𝑡) = (𝑡𝐺(𝑧 ↾ Pred(𝑅, 𝐴, 𝑡)))) → (𝑋𝑤 → Pred(𝑅, 𝐴, 𝑋) ⊆ 𝑤))
13 fndm 6204 . . . . . . . . . . 11 (𝑧 Fn 𝑤 → dom 𝑧 = 𝑤)
1413eleq2d 2878 . . . . . . . . . 10 (𝑧 Fn 𝑤 → (𝑋 ∈ dom 𝑧𝑋𝑤))
1513sseq2d 3837 . . . . . . . . . 10 (𝑧 Fn 𝑤 → (Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑧 ↔ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝑤))
1614, 15imbi12d 335 . . . . . . . . 9 (𝑧 Fn 𝑤 → ((𝑋 ∈ dom 𝑧 → Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑧) ↔ (𝑋𝑤 → Pred(𝑅, 𝐴, 𝑋) ⊆ 𝑤)))
1712, 16syl5ibr 237 . . . . . . . 8 (𝑧 Fn 𝑤 → (((𝑤𝐴 ∧ ∀𝑡𝑤 Pred(𝑅, 𝐴, 𝑡) ⊆ 𝑤) ∧ ∀𝑡𝑤 (𝑧𝑡) = (𝑡𝐺(𝑧 ↾ Pred(𝑅, 𝐴, 𝑡)))) → (𝑋 ∈ dom 𝑧 → Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑧)))
18173impib 1137 . . . . . . 7 ((𝑧 Fn 𝑤 ∧ (𝑤𝐴 ∧ ∀𝑡𝑤 Pred(𝑅, 𝐴, 𝑡) ⊆ 𝑤) ∧ ∀𝑡𝑤 (𝑧𝑡) = (𝑡𝐺(𝑧 ↾ Pred(𝑅, 𝐴, 𝑡)))) → (𝑋 ∈ dom 𝑧 → Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑧))
1918exlimiv 2021 . . . . . 6 (∃𝑤(𝑧 Fn 𝑤 ∧ (𝑤𝐴 ∧ ∀𝑡𝑤 Pred(𝑅, 𝐴, 𝑡) ⊆ 𝑤) ∧ ∀𝑡𝑤 (𝑧𝑡) = (𝑡𝐺(𝑧 ↾ Pred(𝑅, 𝐴, 𝑡)))) → (𝑋 ∈ dom 𝑧 → Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑧))
208, 19sylbi 208 . . . . 5 (𝑧𝐵 → (𝑋 ∈ dom 𝑧 → Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑧))
215, 20syl 17 . . . 4 ((𝐶𝐵𝑧𝐶) → (𝑋 ∈ dom 𝑧 → Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑧))
22 dmeq 5532 . . . . . . . . . 10 (𝑤 = 𝑧 → dom 𝑤 = dom 𝑧)
2322sseq2d 3837 . . . . . . . . 9 (𝑤 = 𝑧 → (Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑤 ↔ Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑧))
2423rspcev 3509 . . . . . . . 8 ((𝑧𝐶 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑧) → ∃𝑤𝐶 Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑤)
25 ssiun 4761 . . . . . . . 8 (∃𝑤𝐶 Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑤 → Pred(𝑅, 𝐴, 𝑋) ⊆ 𝑤𝐶 dom 𝑤)
2624, 25syl 17 . . . . . . 7 ((𝑧𝐶 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑧) → Pred(𝑅, 𝐴, 𝑋) ⊆ 𝑤𝐶 dom 𝑤)
27 dmuni 5542 . . . . . . 7 dom 𝐶 = 𝑤𝐶 dom 𝑤
2826, 27syl6sseqr 3856 . . . . . 6 ((𝑧𝐶 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑧) → Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝐶)
2928ex 399 . . . . 5 (𝑧𝐶 → (Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑧 → Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝐶))
3029adantl 469 . . . 4 ((𝐶𝐵𝑧𝐶) → (Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑧 → Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝐶))
3121, 30syld 47 . . 3 ((𝐶𝐵𝑧𝐶) → (𝑋 ∈ dom 𝑧 → Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝐶))
3231rexlimdva 3226 . 2 (𝐶𝐵 → (∃𝑧𝐶 𝑋 ∈ dom 𝑧 → Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝐶))
334, 32syl5bi 233 1 (𝐶𝐵 → (𝑋 ∈ dom 𝐶 → Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1100   = wceq 1637  wex 1859  wcel 2157  {cab 2799  wral 3103  wrex 3104  wss 3776   cuni 4637   ciun 4719   Fr wfr 5274   Se wse 5275  dom cdm 5318  cres 5320  Predcpred 5899   Fn wfn 6099  cfv 6104  (class class class)co 6877
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2791
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2800  df-cleq 2806  df-clel 2809  df-nfc 2944  df-ral 3108  df-rex 3109  df-rab 3112  df-v 3400  df-dif 3779  df-un 3781  df-in 3783  df-ss 3790  df-nul 4124  df-if 4287  df-sn 4378  df-pr 4380  df-op 4384  df-uni 4638  df-iun 4721  df-br 4852  df-opab 4914  df-xp 5324  df-rel 5325  df-cnv 5326  df-co 5327  df-dm 5328  df-rn 5329  df-res 5330  df-ima 5331  df-pred 5900  df-iota 6067  df-fun 6106  df-fn 6107  df-fv 6112  df-ov 6880
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator