MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  wfrdmcl Structured version   Visualization version   GIF version

Theorem wfrdmcl 7669
Description: Given 𝐹 = wrecs(𝑅, 𝐴, 𝑋) ∧ 𝑋 ∈ dom 𝐹, then its predecessor class is a subset of dom 𝐹. (Contributed by Scott Fenton, 21-Apr-2011.)
Hypothesis
Ref Expression
wfrlem6.1 𝐹 = wrecs(𝑅, 𝐴, 𝐺)
Assertion
Ref Expression
wfrdmcl (𝑋 ∈ dom 𝐹 → Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝐹)

Proof of Theorem wfrdmcl
Dummy variables 𝑓 𝑔 𝑤 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 wfrlem6.1 . . . . . . . 8 𝐹 = wrecs(𝑅, 𝐴, 𝐺)
2 df-wrecs 7652 . . . . . . . 8 wrecs(𝑅, 𝐴, 𝐺) = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}
31, 2eqtri 2839 . . . . . . 7 𝐹 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}
43dmeqi 5540 . . . . . 6 dom 𝐹 = dom {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}
5 dmuni 5549 . . . . . 6 dom {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} = 𝑔 ∈ {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}dom 𝑔
64, 5eqtri 2839 . . . . 5 dom 𝐹 = 𝑔 ∈ {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}dom 𝑔
76eleq2i 2888 . . . 4 (𝑋 ∈ dom 𝐹𝑋 𝑔 ∈ {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}dom 𝑔)
8 eliun 4727 . . . 4 (𝑋 𝑔 ∈ {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}dom 𝑔 ↔ ∃𝑔 ∈ {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}𝑋 ∈ dom 𝑔)
97, 8bitri 266 . . 3 (𝑋 ∈ dom 𝐹 ↔ ∃𝑔 ∈ {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}𝑋 ∈ dom 𝑔)
10 eqid 2817 . . . . . . . 8 {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}
1110wfrlem1 7659 . . . . . . 7 {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} = {𝑔 ∣ ∃𝑧(𝑔 Fn 𝑧 ∧ (𝑧𝐴 ∧ ∀𝑤𝑧 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑧) ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑤))))}
1211abeq2i 2930 . . . . . 6 (𝑔 ∈ {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} ↔ ∃𝑧(𝑔 Fn 𝑧 ∧ (𝑧𝐴 ∧ ∀𝑤𝑧 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑧) ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑤)))))
13 predeq3 5911 . . . . . . . . . . . . 13 (𝑤 = 𝑋 → Pred(𝑅, 𝐴, 𝑤) = Pred(𝑅, 𝐴, 𝑋))
1413sseq1d 3840 . . . . . . . . . . . 12 (𝑤 = 𝑋 → (Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑧 ↔ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝑧))
1514rspccv 3510 . . . . . . . . . . 11 (∀𝑤𝑧 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑧 → (𝑋𝑧 → Pred(𝑅, 𝐴, 𝑋) ⊆ 𝑧))
1615adantl 469 . . . . . . . . . 10 ((𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑧) → (𝑋𝑧 → Pred(𝑅, 𝐴, 𝑋) ⊆ 𝑧))
17 fndm 6211 . . . . . . . . . . . . 13 (𝑔 Fn 𝑧 → dom 𝑔 = 𝑧)
1817eleq2d 2882 . . . . . . . . . . . 12 (𝑔 Fn 𝑧 → (𝑋 ∈ dom 𝑔𝑋𝑧))
1917sseq2d 3841 . . . . . . . . . . . 12 (𝑔 Fn 𝑧 → (Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑔 ↔ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝑧))
2018, 19imbi12d 335 . . . . . . . . . . 11 (𝑔 Fn 𝑧 → ((𝑋 ∈ dom 𝑔 → Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑔) ↔ (𝑋𝑧 → Pred(𝑅, 𝐴, 𝑋) ⊆ 𝑧)))
2120adantr 468 . . . . . . . . . 10 ((𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑧) → ((𝑋 ∈ dom 𝑔 → Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑔) ↔ (𝑋𝑧 → Pred(𝑅, 𝐴, 𝑋) ⊆ 𝑧)))
2216, 21mpbird 248 . . . . . . . . 9 ((𝑔 Fn 𝑧 ∧ ∀𝑤𝑧 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑧) → (𝑋 ∈ dom 𝑔 → Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑔))
2322adantrl 698 . . . . . . . 8 ((𝑔 Fn 𝑧 ∧ (𝑧𝐴 ∧ ∀𝑤𝑧 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑧)) → (𝑋 ∈ dom 𝑔 → Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑔))
24233adant3 1155 . . . . . . 7 ((𝑔 Fn 𝑧 ∧ (𝑧𝐴 ∧ ∀𝑤𝑧 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑧) ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑤)))) → (𝑋 ∈ dom 𝑔 → Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑔))
2524exlimiv 2021 . . . . . 6 (∃𝑧(𝑔 Fn 𝑧 ∧ (𝑧𝐴 ∧ ∀𝑤𝑧 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑧) ∧ ∀𝑤𝑧 (𝑔𝑤) = (𝐺‘(𝑔 ↾ Pred(𝑅, 𝐴, 𝑤)))) → (𝑋 ∈ dom 𝑔 → Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑔))
2612, 25sylbi 208 . . . . 5 (𝑔 ∈ {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} → (𝑋 ∈ dom 𝑔 → Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑔))
2726reximia 3207 . . . 4 (∃𝑔 ∈ {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}𝑋 ∈ dom 𝑔 → ∃𝑔 ∈ {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑔)
28 ssiun 4765 . . . 4 (∃𝑔 ∈ {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝑔 → Pred(𝑅, 𝐴, 𝑋) ⊆ 𝑔 ∈ {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}dom 𝑔)
2927, 28syl 17 . . 3 (∃𝑔 ∈ {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}𝑋 ∈ dom 𝑔 → Pred(𝑅, 𝐴, 𝑋) ⊆ 𝑔 ∈ {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}dom 𝑔)
309, 29sylbi 208 . 2 (𝑋 ∈ dom 𝐹 → Pred(𝑅, 𝐴, 𝑋) ⊆ 𝑔 ∈ {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥𝐴 ∧ ∀𝑦𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐺‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))}dom 𝑔)
3130, 6syl6sseqr 3860 1 (𝑋 ∈ dom 𝐹 → Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384  w3a 1100   = wceq 1637  wex 1859  wcel 2157  {cab 2803  wral 3107  wrex 3108  wss 3780   cuni 4641   ciun 4723  dom cdm 5324  cres 5326  Predcpred 5906   Fn wfn 6106  cfv 6111  wrecscwrecs 7651
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 2795
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 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-ral 3112  df-rex 3113  df-rab 3116  df-v 3404  df-dif 3783  df-un 3785  df-in 3787  df-ss 3794  df-nul 4128  df-if 4291  df-sn 4382  df-pr 4384  df-op 4388  df-uni 4642  df-iun 4725  df-br 4856  df-opab 4918  df-xp 5330  df-rel 5331  df-cnv 5332  df-co 5333  df-dm 5334  df-rn 5335  df-res 5336  df-ima 5337  df-pred 5907  df-iota 6074  df-fun 6113  df-fn 6114  df-fv 6119  df-wrecs 7652
This theorem is referenced by:  wfrlem10  7670  wfrlem14  7674  wfrlem15  7675
  Copyright terms: Public domain W3C validator