![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > finds | Structured version Visualization version GIF version |
Description: Principle of Finite Induction (inference schema), using implicit substitutions. The first four hypotheses establish the substitutions we need. The last two are the basis and the induction step. Theorem Schema 22 of [Suppes] p. 136. This is Metamath 100 proof #74. (Contributed by NM, 14-Apr-1995.) |
Ref | Expression |
---|---|
finds.1 | ⊢ (𝑥 = ∅ → (𝜑 ↔ 𝜓)) |
finds.2 | ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) |
finds.3 | ⊢ (𝑥 = suc 𝑦 → (𝜑 ↔ 𝜃)) |
finds.4 | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏)) |
finds.5 | ⊢ 𝜓 |
finds.6 | ⊢ (𝑦 ∈ ω → (𝜒 → 𝜃)) |
Ref | Expression |
---|---|
finds | ⊢ (𝐴 ∈ ω → 𝜏) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | finds.5 | . . . . 5 ⊢ 𝜓 | |
2 | 0ex 5309 | . . . . . 6 ⊢ ∅ ∈ V | |
3 | finds.1 | . . . . . 6 ⊢ (𝑥 = ∅ → (𝜑 ↔ 𝜓)) | |
4 | 2, 3 | elab 3667 | . . . . 5 ⊢ (∅ ∈ {𝑥 ∣ 𝜑} ↔ 𝜓) |
5 | 1, 4 | mpbir 230 | . . . 4 ⊢ ∅ ∈ {𝑥 ∣ 𝜑} |
6 | finds.6 | . . . . . 6 ⊢ (𝑦 ∈ ω → (𝜒 → 𝜃)) | |
7 | vex 3475 | . . . . . . 7 ⊢ 𝑦 ∈ V | |
8 | finds.2 | . . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) | |
9 | 7, 8 | elab 3667 | . . . . . 6 ⊢ (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ 𝜒) |
10 | 7 | sucex 7813 | . . . . . . 7 ⊢ suc 𝑦 ∈ V |
11 | finds.3 | . . . . . . 7 ⊢ (𝑥 = suc 𝑦 → (𝜑 ↔ 𝜃)) | |
12 | 10, 11 | elab 3667 | . . . . . 6 ⊢ (suc 𝑦 ∈ {𝑥 ∣ 𝜑} ↔ 𝜃) |
13 | 6, 9, 12 | 3imtr4g 295 | . . . . 5 ⊢ (𝑦 ∈ ω → (𝑦 ∈ {𝑥 ∣ 𝜑} → suc 𝑦 ∈ {𝑥 ∣ 𝜑})) |
14 | 13 | rgen 3059 | . . . 4 ⊢ ∀𝑦 ∈ ω (𝑦 ∈ {𝑥 ∣ 𝜑} → suc 𝑦 ∈ {𝑥 ∣ 𝜑}) |
15 | peano5 7903 | . . . 4 ⊢ ((∅ ∈ {𝑥 ∣ 𝜑} ∧ ∀𝑦 ∈ ω (𝑦 ∈ {𝑥 ∣ 𝜑} → suc 𝑦 ∈ {𝑥 ∣ 𝜑})) → ω ⊆ {𝑥 ∣ 𝜑}) | |
16 | 5, 14, 15 | mp2an 690 | . . 3 ⊢ ω ⊆ {𝑥 ∣ 𝜑} |
17 | 16 | sseli 3976 | . 2 ⊢ (𝐴 ∈ ω → 𝐴 ∈ {𝑥 ∣ 𝜑}) |
18 | finds.4 | . . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏)) | |
19 | 18 | elabg 3665 | . 2 ⊢ (𝐴 ∈ ω → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜏)) |
20 | 17, 19 | mpbid 231 | 1 ⊢ (𝐴 ∈ ω → 𝜏) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 = wceq 1533 ∈ wcel 2098 {cab 2704 ∀wral 3057 ⊆ wss 3947 ∅c0 4324 suc csuc 6374 ωcom 7874 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2698 ax-sep 5301 ax-nul 5308 ax-pr 5431 ax-un 7744 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3or 1085 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-sb 2060 df-clab 2705 df-cleq 2719 df-clel 2805 df-ne 2937 df-ral 3058 df-rex 3067 df-rab 3429 df-v 3473 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-pss 3966 df-nul 4325 df-if 4531 df-pw 4606 df-sn 4631 df-pr 4633 df-op 4637 df-uni 4911 df-br 5151 df-opab 5213 df-tr 5268 df-eprel 5584 df-po 5592 df-so 5593 df-fr 5635 df-we 5637 df-ord 6375 df-on 6376 df-lim 6377 df-suc 6378 df-om 7875 |
This theorem is referenced by: findsg 7909 findes 7912 seqomlem1 8475 nna0r 8634 nnm0r 8635 nnawordi 8646 nneob 8681 enrefnn 9076 pssnn 9197 nneneq 9238 nneneqOLD 9250 pssnnOLD 9294 inf3lem1 9657 inf3lem2 9658 cantnfval2 9698 cantnfp1lem3 9709 ttrclss 9749 ttrclselem2 9755 r1fin 9802 ackbij1lem14 10262 ackbij1lem16 10264 ackbij1 10267 ackbij2lem2 10269 ackbij2lem3 10270 infpssrlem4 10335 fin23lem14 10362 fin23lem34 10375 itunitc1 10449 ituniiun 10451 om2uzuzi 13952 om2uzlti 13953 om2uzrdg 13959 uzrdgxfr 13970 hashgadd 14374 mreexexd 17633 precsexlem8 28130 precsexlem9 28131 om2noseqrdg 28195 satfrel 34982 satfdm 34984 satfrnmapom 34985 satf0op 34992 satf0n0 34993 sat1el2xp 34994 fmlafvel 35000 fmlaomn0 35005 gonar 35010 goalr 35012 satffun 35024 findfvcl 35941 finxp00 36886 onmcl 42763 naddonnn 42828 |
Copyright terms: Public domain | W3C validator |