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

Theorem dfrecs3 8374
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-ordered recursion. (Contributed by Scott Fenton, 3-Aug-2020.) (Proof revised by Scott Fenton, 18-Nov-2024.)
Assertion
Ref Expression
dfrecs3 recs(𝐹) = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))}
Distinct variable group:   𝑓,𝐹,𝑥,𝑦

Proof of Theorem dfrecs3
StepHypRef Expression
1 df-recs 8373 . 2 recs(𝐹) = wrecs( E , On, 𝐹)
2 df-wrecs 8299 . 2 wrecs( E , On, 𝐹) = frecs( E , On, (𝐹 ∘ 2nd ))
3 df-frecs 8268 . . 3 frecs( E , On, (𝐹 ∘ 2nd )) = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ On ∧ ∀𝑦𝑥 Pred( E , On, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝑦(𝐹 ∘ 2nd )(𝑓 ↾ Pred( E , On, 𝑦))))}
4 3anass 1093 . . . . . . . 8 ((𝑓 Fn 𝑥 ∧ (𝑥 ⊆ On ∧ ∀𝑦𝑥 Pred( E , On, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝑦(𝐹 ∘ 2nd )(𝑓 ↾ Pred( E , On, 𝑦)))) ↔ (𝑓 Fn 𝑥 ∧ ((𝑥 ⊆ On ∧ ∀𝑦𝑥 Pred( E , On, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝑦(𝐹 ∘ 2nd )(𝑓 ↾ Pred( E , On, 𝑦))))))
5 vex 3476 . . . . . . . . . . . . 13 𝑥 ∈ V
65elon 6372 . . . . . . . . . . . 12 (𝑥 ∈ On ↔ Ord 𝑥)
7 ordsson 7772 . . . . . . . . . . . . . 14 (Ord 𝑥𝑥 ⊆ On)
8 ordtr 6377 . . . . . . . . . . . . . 14 (Ord 𝑥 → Tr 𝑥)
97, 8jca 510 . . . . . . . . . . . . 13 (Ord 𝑥 → (𝑥 ⊆ On ∧ Tr 𝑥))
10 epweon 7764 . . . . . . . . . . . . . . . 16 E We On
11 wess 5662 . . . . . . . . . . . . . . . 16 (𝑥 ⊆ On → ( E We On → E We 𝑥))
1210, 11mpi 20 . . . . . . . . . . . . . . 15 (𝑥 ⊆ On → E We 𝑥)
1312anim1ci 614 . . . . . . . . . . . . . 14 ((𝑥 ⊆ On ∧ Tr 𝑥) → (Tr 𝑥 ∧ E We 𝑥))
14 df-ord 6366 . . . . . . . . . . . . . 14 (Ord 𝑥 ↔ (Tr 𝑥 ∧ E We 𝑥))
1513, 14sylibr 233 . . . . . . . . . . . . 13 ((𝑥 ⊆ On ∧ Tr 𝑥) → Ord 𝑥)
169, 15impbii 208 . . . . . . . . . . . 12 (Ord 𝑥 ↔ (𝑥 ⊆ On ∧ Tr 𝑥))
17 dftr3 5270 . . . . . . . . . . . . . 14 (Tr 𝑥 ↔ ∀𝑦𝑥 𝑦𝑥)
18 ssel2 3976 . . . . . . . . . . . . . . . 16 ((𝑥 ⊆ On ∧ 𝑦𝑥) → 𝑦 ∈ On)
19 predon 7775 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ On → Pred( E , On, 𝑦) = 𝑦)
2019sseq1d 4012 . . . . . . . . . . . . . . . 16 (𝑦 ∈ On → (Pred( E , On, 𝑦) ⊆ 𝑥𝑦𝑥))
2118, 20syl 17 . . . . . . . . . . . . . . 15 ((𝑥 ⊆ On ∧ 𝑦𝑥) → (Pred( E , On, 𝑦) ⊆ 𝑥𝑦𝑥))
2221ralbidva 3173 . . . . . . . . . . . . . 14 (𝑥 ⊆ On → (∀𝑦𝑥 Pred( E , On, 𝑦) ⊆ 𝑥 ↔ ∀𝑦𝑥 𝑦𝑥))
2317, 22bitr4id 289 . . . . . . . . . . . . 13 (𝑥 ⊆ On → (Tr 𝑥 ↔ ∀𝑦𝑥 Pred( E , On, 𝑦) ⊆ 𝑥))
2423pm5.32i 573 . . . . . . . . . . . 12 ((𝑥 ⊆ On ∧ Tr 𝑥) ↔ (𝑥 ⊆ On ∧ ∀𝑦𝑥 Pred( E , On, 𝑦) ⊆ 𝑥))
256, 16, 243bitri 296 . . . . . . . . . . 11 (𝑥 ∈ On ↔ (𝑥 ⊆ On ∧ ∀𝑦𝑥 Pred( E , On, 𝑦) ⊆ 𝑥))
2625anbi1i 622 . . . . . . . . . 10 ((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝑦(𝐹 ∘ 2nd )(𝑓 ↾ Pred( E , On, 𝑦)))) ↔ ((𝑥 ⊆ On ∧ ∀𝑦𝑥 Pred( E , On, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝑦(𝐹 ∘ 2nd )(𝑓 ↾ Pred( E , On, 𝑦)))))
27 onelon 6388 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ On ∧ 𝑦𝑥) → 𝑦 ∈ On)
2827, 19syl 17 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ On ∧ 𝑦𝑥) → Pred( E , On, 𝑦) = 𝑦)
2928reseq2d 5980 . . . . . . . . . . . . . . 15 ((𝑥 ∈ On ∧ 𝑦𝑥) → (𝑓 ↾ Pred( E , On, 𝑦)) = (𝑓𝑦))
3029oveq2d 7427 . . . . . . . . . . . . . 14 ((𝑥 ∈ On ∧ 𝑦𝑥) → (𝑦(𝐹 ∘ 2nd )(𝑓 ↾ Pred( E , On, 𝑦))) = (𝑦(𝐹 ∘ 2nd )(𝑓𝑦)))
31 id 22 . . . . . . . . . . . . . . . 16 (𝑦𝑥𝑦𝑥)
32 vex 3476 . . . . . . . . . . . . . . . . . 18 𝑓 ∈ V
3332resex 6028 . . . . . . . . . . . . . . . . 17 (𝑓𝑦) ∈ V
3433a1i 11 . . . . . . . . . . . . . . . 16 (𝑦𝑥 → (𝑓𝑦) ∈ V)
3531, 34opco2 8112 . . . . . . . . . . . . . . 15 (𝑦𝑥 → (𝑦(𝐹 ∘ 2nd )(𝑓𝑦)) = (𝐹‘(𝑓𝑦)))
3635adantl 480 . . . . . . . . . . . . . 14 ((𝑥 ∈ On ∧ 𝑦𝑥) → (𝑦(𝐹 ∘ 2nd )(𝑓𝑦)) = (𝐹‘(𝑓𝑦)))
3730, 36eqtrd 2770 . . . . . . . . . . . . 13 ((𝑥 ∈ On ∧ 𝑦𝑥) → (𝑦(𝐹 ∘ 2nd )(𝑓 ↾ Pred( E , On, 𝑦))) = (𝐹‘(𝑓𝑦)))
3837eqeq2d 2741 . . . . . . . . . . . 12 ((𝑥 ∈ On ∧ 𝑦𝑥) → ((𝑓𝑦) = (𝑦(𝐹 ∘ 2nd )(𝑓 ↾ Pred( E , On, 𝑦))) ↔ (𝑓𝑦) = (𝐹‘(𝑓𝑦))))
3938ralbidva 3173 . . . . . . . . . . 11 (𝑥 ∈ On → (∀𝑦𝑥 (𝑓𝑦) = (𝑦(𝐹 ∘ 2nd )(𝑓 ↾ Pred( E , On, 𝑦))) ↔ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦))))
4039pm5.32i 573 . . . . . . . . . 10 ((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝑦(𝐹 ∘ 2nd )(𝑓 ↾ Pred( E , On, 𝑦)))) ↔ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦))))
4126, 40bitr3i 276 . . . . . . . . 9 (((𝑥 ⊆ On ∧ ∀𝑦𝑥 Pred( E , On, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝑦(𝐹 ∘ 2nd )(𝑓 ↾ Pred( E , On, 𝑦)))) ↔ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦))))
4241anbi2i 621 . . . . . . . 8 ((𝑓 Fn 𝑥 ∧ ((𝑥 ⊆ On ∧ ∀𝑦𝑥 Pred( E , On, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝑦(𝐹 ∘ 2nd )(𝑓 ↾ Pred( E , On, 𝑦))))) ↔ (𝑓 Fn 𝑥 ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))))
43 an12 641 . . . . . . . 8 ((𝑓 Fn 𝑥 ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))) ↔ (𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))))
444, 42, 433bitri 296 . . . . . . 7 ((𝑓 Fn 𝑥 ∧ (𝑥 ⊆ On ∧ ∀𝑦𝑥 Pred( E , On, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝑦(𝐹 ∘ 2nd )(𝑓 ↾ Pred( E , On, 𝑦)))) ↔ (𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))))
4544exbii 1848 . . . . . 6 (∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ On ∧ ∀𝑦𝑥 Pred( E , On, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝑦(𝐹 ∘ 2nd )(𝑓 ↾ Pred( E , On, 𝑦)))) ↔ ∃𝑥(𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))))
46 df-rex 3069 . . . . . 6 (∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦))) ↔ ∃𝑥(𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))))
4745, 46bitr4i 277 . . . . 5 (∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ On ∧ ∀𝑦𝑥 Pred( E , On, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝑦(𝐹 ∘ 2nd )(𝑓 ↾ Pred( E , On, 𝑦)))) ↔ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦))))
4847abbii 2800 . . . 4 {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ On ∧ ∀𝑦𝑥 Pred( E , On, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝑦(𝐹 ∘ 2nd )(𝑓 ↾ Pred( E , On, 𝑦))))} = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))}
4948unieqi 4920 . . 3 {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ On ∧ ∀𝑦𝑥 Pred( E , On, 𝑦) ⊆ 𝑥) ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝑦(𝐹 ∘ 2nd )(𝑓 ↾ Pred( E , On, 𝑦))))} = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))}
503, 49eqtri 2758 . 2 frecs( E , On, (𝐹 ∘ 2nd )) = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))}
511, 2, 503eqtri 2762 1 recs(𝐹) = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))}
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 394  w3a 1085   = wceq 1539  wex 1779  wcel 2104  {cab 2707  wral 3059  wrex 3068  Vcvv 3472  wss 3947   cuni 4907  Tr wtr 5264   E cep 5578   We wwe 5629  cres 5677  ccom 5679  Predcpred 6298  Ord word 6362  Oncon0 6363   Fn wfn 6537  cfv 6542  (class class class)co 7411  2nd c2nd 7976  frecscfrecs 8267  wrecscwrecs 8298  recscrecs 8372
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pr 5426  ax-un 7727
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6299  df-ord 6366  df-on 6367  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-fo 6548  df-fv 6550  df-ov 7414  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373
This theorem is referenced by:  recsfval  8383  tfrlem9  8387  dfrdg2  35071  dfrecs2  35226
  Copyright terms: Public domain W3C validator