![]() |
Mathbox for Jeff Hoffman |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > findreccl | Structured version Visualization version GIF version |
Description: Please add description here. (Contributed by Jeff Hoffman, 19-Feb-2008.) |
Ref | Expression |
---|---|
findreccl.1 | ⊢ (𝑧 ∈ 𝑃 → (𝐺‘𝑧) ∈ 𝑃) |
Ref | Expression |
---|---|
findreccl | ⊢ (𝐶 ∈ ω → (𝐴 ∈ 𝑃 → (rec(𝐺, 𝐴)‘𝐶) ∈ 𝑃)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rdg0g 7643 | . . 3 ⊢ (𝐴 ∈ 𝑃 → (rec(𝐺, 𝐴)‘∅) = 𝐴) | |
2 | eleq1a 2798 | . . 3 ⊢ (𝐴 ∈ 𝑃 → ((rec(𝐺, 𝐴)‘∅) = 𝐴 → (rec(𝐺, 𝐴)‘∅) ∈ 𝑃)) | |
3 | 1, 2 | mpd 15 | . 2 ⊢ (𝐴 ∈ 𝑃 → (rec(𝐺, 𝐴)‘∅) ∈ 𝑃) |
4 | nnon 7188 | . . . 4 ⊢ (𝑦 ∈ ω → 𝑦 ∈ On) | |
5 | fveq2 6304 | . . . . . . 7 ⊢ (𝑧 = (rec(𝐺, 𝐴)‘𝑦) → (𝐺‘𝑧) = (𝐺‘(rec(𝐺, 𝐴)‘𝑦))) | |
6 | 5 | eleq1d 2788 | . . . . . 6 ⊢ (𝑧 = (rec(𝐺, 𝐴)‘𝑦) → ((𝐺‘𝑧) ∈ 𝑃 ↔ (𝐺‘(rec(𝐺, 𝐴)‘𝑦)) ∈ 𝑃)) |
7 | findreccl.1 | . . . . . 6 ⊢ (𝑧 ∈ 𝑃 → (𝐺‘𝑧) ∈ 𝑃) | |
8 | 6, 7 | vtoclga 3376 | . . . . 5 ⊢ ((rec(𝐺, 𝐴)‘𝑦) ∈ 𝑃 → (𝐺‘(rec(𝐺, 𝐴)‘𝑦)) ∈ 𝑃) |
9 | rdgsuc 7640 | . . . . . 6 ⊢ (𝑦 ∈ On → (rec(𝐺, 𝐴)‘suc 𝑦) = (𝐺‘(rec(𝐺, 𝐴)‘𝑦))) | |
10 | 9 | eleq1d 2788 | . . . . 5 ⊢ (𝑦 ∈ On → ((rec(𝐺, 𝐴)‘suc 𝑦) ∈ 𝑃 ↔ (𝐺‘(rec(𝐺, 𝐴)‘𝑦)) ∈ 𝑃)) |
11 | 8, 10 | syl5ibr 236 | . . . 4 ⊢ (𝑦 ∈ On → ((rec(𝐺, 𝐴)‘𝑦) ∈ 𝑃 → (rec(𝐺, 𝐴)‘suc 𝑦) ∈ 𝑃)) |
12 | 4, 11 | syl 17 | . . 3 ⊢ (𝑦 ∈ ω → ((rec(𝐺, 𝐴)‘𝑦) ∈ 𝑃 → (rec(𝐺, 𝐴)‘suc 𝑦) ∈ 𝑃)) |
13 | 12 | a1d 25 | . 2 ⊢ (𝑦 ∈ ω → (𝐴 ∈ 𝑃 → ((rec(𝐺, 𝐴)‘𝑦) ∈ 𝑃 → (rec(𝐺, 𝐴)‘suc 𝑦) ∈ 𝑃))) |
14 | 3, 13 | findfvcl 32678 | 1 ⊢ (𝐶 ∈ ω → (𝐴 ∈ 𝑃 → (rec(𝐺, 𝐴)‘𝐶) ∈ 𝑃)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1596 ∈ wcel 2103 ∅c0 4023 Oncon0 5836 suc csuc 5838 ‘cfv 6001 ωcom 7182 reccrdg 7625 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1835 ax-4 1850 ax-5 1952 ax-6 2018 ax-7 2054 ax-8 2105 ax-9 2112 ax-10 2132 ax-11 2147 ax-12 2160 ax-13 2355 ax-ext 2704 ax-rep 4879 ax-sep 4889 ax-nul 4897 ax-pow 4948 ax-pr 5011 ax-un 7066 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3or 1073 df-3an 1074 df-tru 1599 df-ex 1818 df-nf 1823 df-sb 2011 df-eu 2575 df-mo 2576 df-clab 2711 df-cleq 2717 df-clel 2720 df-nfc 2855 df-ne 2897 df-ral 3019 df-rex 3020 df-reu 3021 df-rab 3023 df-v 3306 df-sbc 3542 df-csb 3640 df-dif 3683 df-un 3685 df-in 3687 df-ss 3694 df-pss 3696 df-nul 4024 df-if 4195 df-pw 4268 df-sn 4286 df-pr 4288 df-tp 4290 df-op 4292 df-uni 4545 df-iun 4630 df-br 4761 df-opab 4821 df-mpt 4838 df-tr 4861 df-id 5128 df-eprel 5133 df-po 5139 df-so 5140 df-fr 5177 df-we 5179 df-xp 5224 df-rel 5225 df-cnv 5226 df-co 5227 df-dm 5228 df-rn 5229 df-res 5230 df-ima 5231 df-pred 5793 df-ord 5839 df-on 5840 df-lim 5841 df-suc 5842 df-iota 5964 df-fun 6003 df-fn 6004 df-f 6005 df-f1 6006 df-fo 6007 df-f1o 6008 df-fv 6009 df-om 7183 df-wrecs 7527 df-recs 7588 df-rdg 7626 |
This theorem is referenced by: findabrcl 32680 |
Copyright terms: Public domain | W3C validator |