![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > finds2 | Structured version Visualization version GIF version |
Description: Principle of Finite Induction (inference schema), using implicit substitutions. The first three hypotheses establish the substitutions we need. The last two are the basis and the induction step. Theorem Schema 22 of [Suppes] p. 136. (Contributed by NM, 29-Nov-2002.) |
Ref | Expression |
---|---|
finds2.1 | ⊢ (𝑥 = ∅ → (𝜑 ↔ 𝜓)) |
finds2.2 | ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) |
finds2.3 | ⊢ (𝑥 = suc 𝑦 → (𝜑 ↔ 𝜃)) |
finds2.4 | ⊢ (𝜏 → 𝜓) |
finds2.5 | ⊢ (𝑦 ∈ ω → (𝜏 → (𝜒 → 𝜃))) |
Ref | Expression |
---|---|
finds2 | ⊢ (𝑥 ∈ ω → (𝜏 → 𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | finds2.4 | . . . . 5 ⊢ (𝜏 → 𝜓) | |
2 | 0ex 4942 | . . . . . 6 ⊢ ∅ ∈ V | |
3 | finds2.1 | . . . . . . 7 ⊢ (𝑥 = ∅ → (𝜑 ↔ 𝜓)) | |
4 | 3 | imbi2d 329 | . . . . . 6 ⊢ (𝑥 = ∅ → ((𝜏 → 𝜑) ↔ (𝜏 → 𝜓))) |
5 | 2, 4 | elab 3490 | . . . . 5 ⊢ (∅ ∈ {𝑥 ∣ (𝜏 → 𝜑)} ↔ (𝜏 → 𝜓)) |
6 | 1, 5 | mpbir 221 | . . . 4 ⊢ ∅ ∈ {𝑥 ∣ (𝜏 → 𝜑)} |
7 | finds2.5 | . . . . . . 7 ⊢ (𝑦 ∈ ω → (𝜏 → (𝜒 → 𝜃))) | |
8 | 7 | a2d 29 | . . . . . 6 ⊢ (𝑦 ∈ ω → ((𝜏 → 𝜒) → (𝜏 → 𝜃))) |
9 | vex 3343 | . . . . . . 7 ⊢ 𝑦 ∈ V | |
10 | finds2.2 | . . . . . . . 8 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) | |
11 | 10 | imbi2d 329 | . . . . . . 7 ⊢ (𝑥 = 𝑦 → ((𝜏 → 𝜑) ↔ (𝜏 → 𝜒))) |
12 | 9, 11 | elab 3490 | . . . . . 6 ⊢ (𝑦 ∈ {𝑥 ∣ (𝜏 → 𝜑)} ↔ (𝜏 → 𝜒)) |
13 | 9 | sucex 7177 | . . . . . . 7 ⊢ suc 𝑦 ∈ V |
14 | finds2.3 | . . . . . . . 8 ⊢ (𝑥 = suc 𝑦 → (𝜑 ↔ 𝜃)) | |
15 | 14 | imbi2d 329 | . . . . . . 7 ⊢ (𝑥 = suc 𝑦 → ((𝜏 → 𝜑) ↔ (𝜏 → 𝜃))) |
16 | 13, 15 | elab 3490 | . . . . . 6 ⊢ (suc 𝑦 ∈ {𝑥 ∣ (𝜏 → 𝜑)} ↔ (𝜏 → 𝜃)) |
17 | 8, 12, 16 | 3imtr4g 285 | . . . . 5 ⊢ (𝑦 ∈ ω → (𝑦 ∈ {𝑥 ∣ (𝜏 → 𝜑)} → suc 𝑦 ∈ {𝑥 ∣ (𝜏 → 𝜑)})) |
18 | 17 | rgen 3060 | . . . 4 ⊢ ∀𝑦 ∈ ω (𝑦 ∈ {𝑥 ∣ (𝜏 → 𝜑)} → suc 𝑦 ∈ {𝑥 ∣ (𝜏 → 𝜑)}) |
19 | peano5 7255 | . . . 4 ⊢ ((∅ ∈ {𝑥 ∣ (𝜏 → 𝜑)} ∧ ∀𝑦 ∈ ω (𝑦 ∈ {𝑥 ∣ (𝜏 → 𝜑)} → suc 𝑦 ∈ {𝑥 ∣ (𝜏 → 𝜑)})) → ω ⊆ {𝑥 ∣ (𝜏 → 𝜑)}) | |
20 | 6, 18, 19 | mp2an 710 | . . 3 ⊢ ω ⊆ {𝑥 ∣ (𝜏 → 𝜑)} |
21 | 20 | sseli 3740 | . 2 ⊢ (𝑥 ∈ ω → 𝑥 ∈ {𝑥 ∣ (𝜏 → 𝜑)}) |
22 | abid 2748 | . 2 ⊢ (𝑥 ∈ {𝑥 ∣ (𝜏 → 𝜑)} ↔ (𝜏 → 𝜑)) | |
23 | 21, 22 | sylib 208 | 1 ⊢ (𝑥 ∈ ω → (𝜏 → 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 = wceq 1632 ∈ wcel 2139 {cab 2746 ∀wral 3050 ⊆ wss 3715 ∅c0 4058 suc csuc 5886 ωcom 7231 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1871 ax-4 1886 ax-5 1988 ax-6 2054 ax-7 2090 ax-8 2141 ax-9 2148 ax-10 2168 ax-11 2183 ax-12 2196 ax-13 2391 ax-ext 2740 ax-sep 4933 ax-nul 4941 ax-pr 5055 ax-un 7115 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3or 1073 df-3an 1074 df-tru 1635 df-ex 1854 df-nf 1859 df-sb 2047 df-eu 2611 df-mo 2612 df-clab 2747 df-cleq 2753 df-clel 2756 df-nfc 2891 df-ne 2933 df-ral 3055 df-rex 3056 df-rab 3059 df-v 3342 df-sbc 3577 df-dif 3718 df-un 3720 df-in 3722 df-ss 3729 df-pss 3731 df-nul 4059 df-if 4231 df-pw 4304 df-sn 4322 df-pr 4324 df-tp 4326 df-op 4328 df-uni 4589 df-br 4805 df-opab 4865 df-tr 4905 df-eprel 5179 df-po 5187 df-so 5188 df-fr 5225 df-we 5227 df-ord 5887 df-on 5888 df-lim 5889 df-suc 5890 df-om 7232 |
This theorem is referenced by: finds1 7261 onnseq 7611 nnacl 7862 nnmcl 7863 nnecl 7864 nnacom 7868 nnaass 7873 nndi 7874 nnmass 7875 nnmsucr 7876 nnmcom 7877 nnmordi 7882 omsmolem 7904 isinf 8340 unblem2 8380 fiint 8404 dffi3 8504 card2inf 8627 cantnfle 8743 cantnflt 8744 cantnflem1 8761 cnfcom 8772 trcl 8779 fseqenlem1 9057 infpssrlem3 9339 fin23lem26 9359 axdc3lem2 9485 axdc4lem 9489 axdclem2 9554 wunr1om 9753 wuncval2 9781 tskr1om 9801 grothomex 9863 peano5nni 11235 neibastop2lem 32682 finxpreclem6 33562 |
Copyright terms: Public domain | W3C validator |