![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > ILE Home > Th. List > rdgifnon | Structured version GIF version |
Description: The recursive definition generator is a function on ordinal numbers. The 𝐹 Fn V condition states that the characteristic function is defined for all sets (being defined for all ordinals might be enough, but being defined for all sets will generally hold for the characteristic functions we need to use this with). (Contributed by Jim Kingdon, 13-Jul-2019.) |
Ref | Expression |
---|---|
rdgifnon | ⊢ ((𝐹 Fn V ∧ A ∈ 𝑉) → rec(𝐹, A) Fn On) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-irdg 5873 | . 2 ⊢ rec(𝐹, A) = recs((g ∈ V ↦ (A ∪ ∪ x ∈ dom g(𝐹‘(g‘x))))) | |
2 | rdgruledefgg 5877 | . . 3 ⊢ ((𝐹 Fn V ∧ A ∈ 𝑉) → (Fun (g ∈ V ↦ (A ∪ ∪ x ∈ dom g(𝐹‘(g‘x)))) ∧ ((g ∈ V ↦ (A ∪ ∪ x ∈ dom g(𝐹‘(g‘x))))‘f) ∈ V)) | |
3 | 2 | alrimiv 1737 | . 2 ⊢ ((𝐹 Fn V ∧ A ∈ 𝑉) → ∀f(Fun (g ∈ V ↦ (A ∪ ∪ x ∈ dom g(𝐹‘(g‘x)))) ∧ ((g ∈ V ↦ (A ∪ ∪ x ∈ dom g(𝐹‘(g‘x))))‘f) ∈ V)) |
4 | 1, 3 | tfri1d 5866 | 1 ⊢ ((𝐹 Fn V ∧ A ∈ 𝑉) → rec(𝐹, A) Fn On) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 97 ∈ wcel 1375 Vcvv 2534 ∪ cun 2891 ∪ ciun 3630 ↦ cmpt 3791 Oncon0 4047 dom cdm 4270 Fun wfun 4821 Fn wfn 4822 ‘cfv 4827 reccrdg 5872 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-in1 532 ax-in2 533 ax-io 617 ax-5 1316 ax-7 1317 ax-gen 1318 ax-ie1 1364 ax-ie2 1365 ax-8 1377 ax-10 1378 ax-11 1379 ax-i12 1380 ax-bnd 1381 ax-4 1382 ax-13 1386 ax-14 1387 ax-17 1401 ax-i9 1405 ax-ial 1410 ax-i5r 1411 ax-ext 2005 ax-coll 3845 ax-sep 3848 ax-pow 3900 ax-pr 3917 ax-un 4118 ax-setind 4202 |
This theorem depends on definitions: df-bi 110 df-3an 875 df-tru 1231 df-fal 1234 df-nf 1330 df-sb 1629 df-eu 1886 df-mo 1887 df-clab 2010 df-cleq 2016 df-clel 2019 df-nfc 2150 df-ne 2189 df-ral 2288 df-rex 2289 df-reu 2290 df-rab 2292 df-v 2536 df-sbc 2741 df-csb 2829 df-dif 2896 df-un 2898 df-in 2900 df-ss 2907 df-nul 3201 df-pw 3335 df-sn 3355 df-pr 3356 df-op 3358 df-uni 3554 df-iun 3632 df-br 3738 df-opab 3792 df-mpt 3793 df-tr 3828 df-id 4003 df-iord 4050 df-on 4052 df-suc 4055 df-xp 4276 df-rel 4277 df-cnv 4278 df-co 4279 df-dm 4280 df-rn 4281 df-res 4282 df-ima 4283 df-iota 4792 df-fun 4829 df-fn 4830 df-f 4831 df-f1 4832 df-fo 4833 df-f1o 4834 df-fv 4835 df-recs 5837 df-irdg 5873 |
This theorem is referenced by: rdgivallem 5883 frecrdg 5903 |
Copyright terms: Public domain | W3C validator |