![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > tfr1 | Structured version Visualization version GIF version |
Description: Principle of Transfinite Recursion, part 1 of 3. Theorem 7.41(1) of [TakeutiZaring] p. 47. We start with an arbitrary class 𝐺, normally a function, and define a class 𝐴 of all "acceptable" functions. The final function we're interested in is the union 𝐹 = recs(𝐺) of them. 𝐹 is then said to be defined by transfinite recursion. The purpose of the 3 parts of this theorem is to demonstrate properties of 𝐹. In this first part we show that 𝐹 is a function whose domain is all ordinal numbers. (Contributed by NM, 17-Aug-1994.) (Revised by Mario Carneiro, 18-Jan-2015.) |
Ref | Expression |
---|---|
tfr.1 | ⊢ 𝐹 = recs(𝐺) |
Ref | Expression |
---|---|
tfr1 | ⊢ 𝐹 Fn On |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2748 | . . . 4 ⊢ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)))} = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)))} | |
2 | 1 | tfrlem7 7636 | . . 3 ⊢ Fun recs(𝐺) |
3 | 1 | tfrlem14 7644 | . . 3 ⊢ dom recs(𝐺) = On |
4 | df-fn 6040 | . . 3 ⊢ (recs(𝐺) Fn On ↔ (Fun recs(𝐺) ∧ dom recs(𝐺) = On)) | |
5 | 2, 3, 4 | mpbir2an 993 | . 2 ⊢ recs(𝐺) Fn On |
6 | tfr.1 | . . 3 ⊢ 𝐹 = recs(𝐺) | |
7 | 6 | fneq1i 6134 | . 2 ⊢ (𝐹 Fn On ↔ recs(𝐺) Fn On) |
8 | 5, 7 | mpbir 221 | 1 ⊢ 𝐹 Fn On |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 383 = wceq 1620 {cab 2734 ∀wral 3038 ∃wrex 3039 dom cdm 5254 ↾ cres 5256 Oncon0 5872 Fun wfun 6031 Fn wfn 6032 ‘cfv 6037 recscrecs 7624 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1859 ax-4 1874 ax-5 1976 ax-6 2042 ax-7 2078 ax-8 2129 ax-9 2136 ax-10 2156 ax-11 2171 ax-12 2184 ax-13 2379 ax-ext 2728 ax-rep 4911 ax-sep 4921 ax-nul 4929 ax-pow 4980 ax-pr 5043 ax-un 7102 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3or 1073 df-3an 1074 df-tru 1623 df-ex 1842 df-nf 1847 df-sb 2035 df-eu 2599 df-mo 2600 df-clab 2735 df-cleq 2741 df-clel 2744 df-nfc 2879 df-ne 2921 df-ral 3043 df-rex 3044 df-reu 3045 df-rab 3047 df-v 3330 df-sbc 3565 df-csb 3663 df-dif 3706 df-un 3708 df-in 3710 df-ss 3717 df-pss 3719 df-nul 4047 df-if 4219 df-sn 4310 df-pr 4312 df-tp 4314 df-op 4316 df-uni 4577 df-iun 4662 df-br 4793 df-opab 4853 df-mpt 4870 df-tr 4893 df-id 5162 df-eprel 5167 df-po 5175 df-so 5176 df-fr 5213 df-we 5215 df-xp 5260 df-rel 5261 df-cnv 5262 df-co 5263 df-dm 5264 df-rn 5265 df-res 5266 df-ima 5267 df-pred 5829 df-ord 5875 df-on 5876 df-suc 5878 df-iota 6000 df-fun 6039 df-fn 6040 df-f 6041 df-f1 6042 df-fo 6043 df-f1o 6044 df-fv 6045 df-wrecs 7564 df-recs 7625 |
This theorem is referenced by: tfr2 7651 tfr3 7652 recsfnon 7656 rdgfnon 7671 dfac8alem 9013 dfac12lem1 9128 dfac12lem2 9129 zorn2lem1 9481 zorn2lem2 9482 zorn2lem4 9484 zorn2lem5 9485 zorn2lem6 9486 zorn2lem7 9487 ttukeylem3 9496 ttukeylem5 9498 ttukeylem6 9499 madeval 32212 dnnumch1 38085 dnnumch3lem 38087 dnnumch3 38088 aomclem6 38100 |
Copyright terms: Public domain | W3C validator |