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

Theorem dfrecs3 7999
Description: The old definition of transfinite recursion. This version is preferred for development, as it demonstrates the properties of transfinite recursion without relying on well-founded recursion. (Contributed by Scott Fenton, 3-Aug-2020.)
Assertion
Ref Expression
dfrecs3 recs(𝐹) = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))}
Distinct variable group:   𝑓,𝐹,𝑥,𝑦

Proof of Theorem dfrecs3
StepHypRef Expression
1 df-recs 7998 . 2 recs(𝐹) = wrecs( E , On, 𝐹)
2 df-wrecs 7937 . 2 wrecs( E , On, 𝐹) = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ On ∧ ∀𝑦𝑥 Pred( E , On, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓 ↾ Pred( E , On, 𝑦))))}
3 3anass 1092 . . . . . . 7 ((𝑓 Fn 𝑥 ∧ (𝑥 ⊆ On ∧ ∀𝑦𝑥 Pred( E , On, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓 ↾ Pred( E , On, 𝑦)))) ↔ (𝑓 Fn 𝑥 ∧ ((𝑥 ⊆ On ∧ ∀𝑦𝑥 Pred( E , On, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓 ↾ Pred( E , On, 𝑦))))))
4 vex 3483 . . . . . . . . . . . 12 𝑥 ∈ V
54elon 6187 . . . . . . . . . . 11 (𝑥 ∈ On ↔ Ord 𝑥)
6 ordsson 7494 . . . . . . . . . . . . 13 (Ord 𝑥𝑥 ⊆ On)
7 ordtr 6192 . . . . . . . . . . . . 13 (Ord 𝑥 → Tr 𝑥)
86, 7jca 515 . . . . . . . . . . . 12 (Ord 𝑥 → (𝑥 ⊆ On ∧ Tr 𝑥))
9 epweon 7487 . . . . . . . . . . . . . . 15 E We On
10 wess 5529 . . . . . . . . . . . . . . 15 (𝑥 ⊆ On → ( E We On → E We 𝑥))
119, 10mpi 20 . . . . . . . . . . . . . 14 (𝑥 ⊆ On → E We 𝑥)
1211anim1ci 618 . . . . . . . . . . . . 13 ((𝑥 ⊆ On ∧ Tr 𝑥) → (Tr 𝑥 ∧ E We 𝑥))
13 df-ord 6181 . . . . . . . . . . . . 13 (Ord 𝑥 ↔ (Tr 𝑥 ∧ E We 𝑥))
1412, 13sylibr 237 . . . . . . . . . . . 12 ((𝑥 ⊆ On ∧ Tr 𝑥) → Ord 𝑥)
158, 14impbii 212 . . . . . . . . . . 11 (Ord 𝑥 ↔ (𝑥 ⊆ On ∧ Tr 𝑥))
16 ssel2 3947 . . . . . . . . . . . . . . 15 ((𝑥 ⊆ On ∧ 𝑦𝑥) → 𝑦 ∈ On)
17 predon 7496 . . . . . . . . . . . . . . . 16 (𝑦 ∈ On → Pred( E , On, 𝑦) = 𝑦)
1817sseq1d 3983 . . . . . . . . . . . . . . 15 (𝑦 ∈ On → (Pred( E , On, 𝑦) ⊆ 𝑥𝑦𝑥))
1916, 18syl 17 . . . . . . . . . . . . . 14 ((𝑥 ⊆ On ∧ 𝑦𝑥) → (Pred( E , On, 𝑦) ⊆ 𝑥𝑦𝑥))
2019ralbidva 3191 . . . . . . . . . . . . 13 (𝑥 ⊆ On → (∀𝑦𝑥 Pred( E , On, 𝑦) ⊆ 𝑥 ↔ ∀𝑦𝑥 𝑦𝑥))
21 dftr3 5162 . . . . . . . . . . . . 13 (Tr 𝑥 ↔ ∀𝑦𝑥 𝑦𝑥)
2220, 21syl6rbbr 293 . . . . . . . . . . . 12 (𝑥 ⊆ On → (Tr 𝑥 ↔ ∀𝑦𝑥 Pred( E , On, 𝑦) ⊆ 𝑥))
2322pm5.32i 578 . . . . . . . . . . 11 ((𝑥 ⊆ On ∧ Tr 𝑥) ↔ (𝑥 ⊆ On ∧ ∀𝑦𝑥 Pred( E , On, 𝑦) ⊆ 𝑥))
245, 15, 233bitri 300 . . . . . . . . . 10 (𝑥 ∈ On ↔ (𝑥 ⊆ On ∧ ∀𝑦𝑥 Pred( E , On, 𝑦) ⊆ 𝑥))
2524anbi1i 626 . . . . . . . . 9 ((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓 ↾ Pred( E , On, 𝑦)))) ↔ ((𝑥 ⊆ On ∧ ∀𝑦𝑥 Pred( E , On, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓 ↾ Pred( E , On, 𝑦)))))
26 onelon 6203 . . . . . . . . . . . 12 ((𝑥 ∈ On ∧ 𝑦𝑥) → 𝑦 ∈ On)
2717reseq2d 5840 . . . . . . . . . . . . . 14 (𝑦 ∈ On → (𝑓 ↾ Pred( E , On, 𝑦)) = (𝑓𝑦))
2827fveq2d 6662 . . . . . . . . . . . . 13 (𝑦 ∈ On → (𝐹‘(𝑓 ↾ Pred( E , On, 𝑦))) = (𝐹‘(𝑓𝑦)))
2928eqeq2d 2835 . . . . . . . . . . . 12 (𝑦 ∈ On → ((𝑓𝑦) = (𝐹‘(𝑓 ↾ Pred( E , On, 𝑦))) ↔ (𝑓𝑦) = (𝐹‘(𝑓𝑦))))
3026, 29syl 17 . . . . . . . . . . 11 ((𝑥 ∈ On ∧ 𝑦𝑥) → ((𝑓𝑦) = (𝐹‘(𝑓 ↾ Pred( E , On, 𝑦))) ↔ (𝑓𝑦) = (𝐹‘(𝑓𝑦))))
3130ralbidva 3191 . . . . . . . . . 10 (𝑥 ∈ On → (∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓 ↾ Pred( E , On, 𝑦))) ↔ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦))))
3231pm5.32i 578 . . . . . . . . 9 ((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓 ↾ Pred( E , On, 𝑦)))) ↔ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦))))
3325, 32bitr3i 280 . . . . . . . 8 (((𝑥 ⊆ On ∧ ∀𝑦𝑥 Pred( E , On, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓 ↾ Pred( E , On, 𝑦)))) ↔ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦))))
3433anbi2i 625 . . . . . . 7 ((𝑓 Fn 𝑥 ∧ ((𝑥 ⊆ On ∧ ∀𝑦𝑥 Pred( E , On, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓 ↾ Pred( E , On, 𝑦))))) ↔ (𝑓 Fn 𝑥 ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))))
35 an12 644 . . . . . . 7 ((𝑓 Fn 𝑥 ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))) ↔ (𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))))
363, 34, 353bitri 300 . . . . . 6 ((𝑓 Fn 𝑥 ∧ (𝑥 ⊆ On ∧ ∀𝑦𝑥 Pred( E , On, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓 ↾ Pred( E , On, 𝑦)))) ↔ (𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))))
3736exbii 1849 . . . . 5 (∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ On ∧ ∀𝑦𝑥 Pred( E , On, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓 ↾ Pred( E , On, 𝑦)))) ↔ ∃𝑥(𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))))
38 df-rex 3139 . . . . 5 (∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦))) ↔ ∃𝑥(𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))))
3937, 38bitr4i 281 . . . 4 (∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ On ∧ ∀𝑦𝑥 Pred( E , On, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓 ↾ Pred( E , On, 𝑦)))) ↔ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦))))
4039abbii 2889 . . 3 {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ On ∧ ∀𝑦𝑥 Pred( E , On, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓 ↾ Pred( E , On, 𝑦))))} = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))}
4140unieqi 4837 . 2 {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ On ∧ ∀𝑦𝑥 Pred( E , On, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓 ↾ Pred( E , On, 𝑦))))} = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))}
421, 2, 413eqtri 2851 1 recs(𝐹) = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))}
Colors of variables: wff setvar class
Syntax hints:  wb 209  wa 399  w3a 1084   = wceq 1538  wex 1781  wcel 2115  {cab 2802  wral 3133  wrex 3134  wss 3919   cuni 4824  Tr wtr 5158   E cep 5451   We wwe 5500  cres 5544  Predcpred 6134  Ord word 6177  Oncon0 6178   Fn wfn 6338  cfv 6343  wrecscwrecs 7936  recscrecs 7997
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 2179  ax-ext 2796  ax-sep 5189  ax-nul 5196  ax-pr 5317  ax-un 7451
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3015  df-ral 3138  df-rex 3139  df-rab 3142  df-v 3482  df-sbc 3759  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-pss 3938  df-nul 4276  df-if 4450  df-sn 4550  df-pr 4552  df-tp 4554  df-op 4556  df-uni 4825  df-br 5053  df-opab 5115  df-tr 5159  df-eprel 5452  df-po 5461  df-so 5462  df-fr 5501  df-we 5503  df-xp 5548  df-rel 5549  df-cnv 5550  df-dm 5552  df-rn 5553  df-res 5554  df-ima 5555  df-pred 6135  df-ord 6181  df-on 6182  df-iota 6302  df-fv 6351  df-wrecs 7937  df-recs 7998
This theorem is referenced by:  recsfval  8007  tfrlem9  8011  dfrdg2  33065  dfrecs2  33436
  Copyright terms: Public domain W3C validator