| 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 5307 | . . . . . 6 ⊢ ∅ ∈ V | |
| 3 | finds2.1 | . . . . . . 7 ⊢ (𝑥 = ∅ → (𝜑 ↔ 𝜓)) | |
| 4 | 3 | imbi2d 340 | . . . . . 6 ⊢ (𝑥 = ∅ → ((𝜏 → 𝜑) ↔ (𝜏 → 𝜓))) |
| 5 | 2, 4 | elab 3679 | . . . . 5 ⊢ (∅ ∈ {𝑥 ∣ (𝜏 → 𝜑)} ↔ (𝜏 → 𝜓)) |
| 6 | 1, 5 | mpbir 231 | . . . 4 ⊢ ∅ ∈ {𝑥 ∣ (𝜏 → 𝜑)} |
| 7 | finds2.5 | . . . . . . 7 ⊢ (𝑦 ∈ ω → (𝜏 → (𝜒 → 𝜃))) | |
| 8 | 7 | a2d 29 | . . . . . 6 ⊢ (𝑦 ∈ ω → ((𝜏 → 𝜒) → (𝜏 → 𝜃))) |
| 9 | vex 3484 | . . . . . . 7 ⊢ 𝑦 ∈ V | |
| 10 | finds2.2 | . . . . . . . 8 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) | |
| 11 | 10 | imbi2d 340 | . . . . . . 7 ⊢ (𝑥 = 𝑦 → ((𝜏 → 𝜑) ↔ (𝜏 → 𝜒))) |
| 12 | 9, 11 | elab 3679 | . . . . . 6 ⊢ (𝑦 ∈ {𝑥 ∣ (𝜏 → 𝜑)} ↔ (𝜏 → 𝜒)) |
| 13 | 9 | sucex 7826 | . . . . . . 7 ⊢ suc 𝑦 ∈ V |
| 14 | finds2.3 | . . . . . . . 8 ⊢ (𝑥 = suc 𝑦 → (𝜑 ↔ 𝜃)) | |
| 15 | 14 | imbi2d 340 | . . . . . . 7 ⊢ (𝑥 = suc 𝑦 → ((𝜏 → 𝜑) ↔ (𝜏 → 𝜃))) |
| 16 | 13, 15 | elab 3679 | . . . . . 6 ⊢ (suc 𝑦 ∈ {𝑥 ∣ (𝜏 → 𝜑)} ↔ (𝜏 → 𝜃)) |
| 17 | 8, 12, 16 | 3imtr4g 296 | . . . . 5 ⊢ (𝑦 ∈ ω → (𝑦 ∈ {𝑥 ∣ (𝜏 → 𝜑)} → suc 𝑦 ∈ {𝑥 ∣ (𝜏 → 𝜑)})) |
| 18 | 17 | rgen 3063 | . . . 4 ⊢ ∀𝑦 ∈ ω (𝑦 ∈ {𝑥 ∣ (𝜏 → 𝜑)} → suc 𝑦 ∈ {𝑥 ∣ (𝜏 → 𝜑)}) |
| 19 | peano5 7915 | . . . 4 ⊢ ((∅ ∈ {𝑥 ∣ (𝜏 → 𝜑)} ∧ ∀𝑦 ∈ ω (𝑦 ∈ {𝑥 ∣ (𝜏 → 𝜑)} → suc 𝑦 ∈ {𝑥 ∣ (𝜏 → 𝜑)})) → ω ⊆ {𝑥 ∣ (𝜏 → 𝜑)}) | |
| 20 | 6, 18, 19 | mp2an 692 | . . 3 ⊢ ω ⊆ {𝑥 ∣ (𝜏 → 𝜑)} |
| 21 | 20 | sseli 3979 | . 2 ⊢ (𝑥 ∈ ω → 𝑥 ∈ {𝑥 ∣ (𝜏 → 𝜑)}) |
| 22 | abid 2718 | . 2 ⊢ (𝑥 ∈ {𝑥 ∣ (𝜏 → 𝜑)} ↔ (𝜏 → 𝜑)) | |
| 23 | 21, 22 | sylib 218 | 1 ⊢ (𝑥 ∈ ω → (𝜏 → 𝜑)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 = wceq 1540 ∈ wcel 2108 {cab 2714 ∀wral 3061 ⊆ wss 3951 ∅c0 4333 suc csuc 6386 ωcom 7887 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-12 2177 ax-ext 2708 ax-sep 5296 ax-nul 5306 ax-pr 5432 ax-un 7755 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-ne 2941 df-ral 3062 df-rex 3071 df-rab 3437 df-v 3482 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-pss 3971 df-nul 4334 df-if 4526 df-pw 4602 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4908 df-br 5144 df-opab 5206 df-tr 5260 df-eprel 5584 df-po 5592 df-so 5593 df-fr 5637 df-we 5639 df-ord 6387 df-on 6388 df-lim 6389 df-suc 6390 df-om 7888 |
| This theorem is referenced by: finds1 7921 onnseq 8384 nnacl 8649 nnmcl 8650 nnecl 8651 nnacom 8655 nnaass 8660 nndi 8661 nnmass 8662 nnmsucr 8663 nnmcom 8664 nnmordi 8669 omsmolem 8695 isinf 9296 isinfOLD 9297 unblem2 9329 fiint 9366 fiintOLD 9367 dffi3 9471 card2inf 9595 cantnfle 9711 cantnflt 9712 cantnflem1 9729 cnfcom 9740 trcl 9768 fseqenlem1 10064 nnadju 10238 infpssrlem3 10345 fin23lem26 10365 axdc3lem2 10491 axdc4lem 10495 axdclem2 10560 wunr1om 10759 wuncval2 10787 tskr1om 10807 grothomex 10869 peano5nni 12269 precsexlem6 28236 precsexlem7 28237 noseqind 28298 om2noseqlt 28305 neibastop2lem 36361 finxpreclem6 37397 domalom 37405 oaabsb 43307 |
| Copyright terms: Public domain | W3C validator |