ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  indpi Structured version   GIF version

Theorem indpi 6326
Description: Principle of Finite Induction on positive integers. (Contributed by NM, 23-Mar-1996.)
Hypotheses
Ref Expression
indpi.1 (x = 1𝑜 → (φψ))
indpi.2 (x = y → (φχ))
indpi.3 (x = (y +N 1𝑜) → (φθ))
indpi.4 (x = A → (φτ))
indpi.5 ψ
indpi.6 (y N → (χθ))
Assertion
Ref Expression
indpi (A Nτ)
Distinct variable groups:   x,y   x,A   ψ,x   χ,x   θ,x   τ,x   φ,y
Allowed substitution hints:   φ(x)   ψ(y)   χ(y)   θ(y)   τ(y)   A(y)

Proof of Theorem indpi
StepHypRef Expression
1 indpi.4 . 2 (x = A → (φτ))
2 elni 6292 . . 3 (x N ↔ (x 𝜔 x ≠ ∅))
3 eqid 2037 . . . . . . . . . 10 ∅ = ∅
43orci 649 . . . . . . . . 9 (∅ = ∅ [∅ / x]φ)
5 nfv 1418 . . . . . . . . . . 11 x∅ = ∅
6 nfsbc1v 2776 . . . . . . . . . . 11 x[∅ / x]φ
75, 6nfor 1463 . . . . . . . . . 10 x(∅ = ∅ [∅ / x]φ)
8 0ex 3875 . . . . . . . . . 10 V
9 eqeq1 2043 . . . . . . . . . . 11 (x = ∅ → (x = ∅ ↔ ∅ = ∅))
10 sbceq1a 2767 . . . . . . . . . . 11 (x = ∅ → (φ[∅ / x]φ))
119, 10orbi12d 706 . . . . . . . . . 10 (x = ∅ → ((x = ∅ φ) ↔ (∅ = ∅ [∅ / x]φ)))
127, 8, 11elabf 2680 . . . . . . . . 9 (∅ {x ∣ (x = ∅ φ)} ↔ (∅ = ∅ [∅ / x]φ))
134, 12mpbir 134 . . . . . . . 8 {x ∣ (x = ∅ φ)}
14 suceq 4105 . . . . . . . . . . . . . 14 (y = ∅ → suc y = suc ∅)
15 df-1o 5940 . . . . . . . . . . . . . 14 1𝑜 = suc ∅
1614, 15syl6eqr 2087 . . . . . . . . . . . . 13 (y = ∅ → suc y = 1𝑜)
17 indpi.5 . . . . . . . . . . . . . . 15 ψ
1817olci 650 . . . . . . . . . . . . . 14 (1𝑜 = ∅ ψ)
19 1onn 6029 . . . . . . . . . . . . . . . 16 1𝑜 𝜔
2019elexi 2561 . . . . . . . . . . . . . . 15 1𝑜 V
21 eqeq1 2043 . . . . . . . . . . . . . . . 16 (x = 1𝑜 → (x = ∅ ↔ 1𝑜 = ∅))
22 indpi.1 . . . . . . . . . . . . . . . 16 (x = 1𝑜 → (φψ))
2321, 22orbi12d 706 . . . . . . . . . . . . . . 15 (x = 1𝑜 → ((x = ∅ φ) ↔ (1𝑜 = ∅ ψ)))
2420, 23elab 2681 . . . . . . . . . . . . . 14 (1𝑜 {x ∣ (x = ∅ φ)} ↔ (1𝑜 = ∅ ψ))
2518, 24mpbir 134 . . . . . . . . . . . . 13 1𝑜 {x ∣ (x = ∅ φ)}
2616, 25syl6eqel 2125 . . . . . . . . . . . 12 (y = ∅ → suc y {x ∣ (x = ∅ φ)})
2726a1d 22 . . . . . . . . . . 11 (y = ∅ → (y {x ∣ (x = ∅ φ)} → suc y {x ∣ (x = ∅ φ)}))
2827a1i 9 . . . . . . . . . 10 (y 𝜔 → (y = ∅ → (y {x ∣ (x = ∅ φ)} → suc y {x ∣ (x = ∅ φ)})))
29 indpi.6 . . . . . . . . . . . 12 (y N → (χθ))
30 elni 6292 . . . . . . . . . . . . . . . 16 (y N ↔ (y 𝜔 y ≠ ∅))
3130simprbi 260 . . . . . . . . . . . . . . 15 (y Ny ≠ ∅)
3231neneqd 2221 . . . . . . . . . . . . . 14 (y N → ¬ y = ∅)
33 biorf 662 . . . . . . . . . . . . . 14 y = ∅ → (χ ↔ (y = ∅ χ)))
3432, 33syl 14 . . . . . . . . . . . . 13 (y N → (χ ↔ (y = ∅ χ)))
35 vex 2554 . . . . . . . . . . . . . 14 y V
36 eqeq1 2043 . . . . . . . . . . . . . . 15 (x = y → (x = ∅ ↔ y = ∅))
37 indpi.2 . . . . . . . . . . . . . . 15 (x = y → (φχ))
3836, 37orbi12d 706 . . . . . . . . . . . . . 14 (x = y → ((x = ∅ φ) ↔ (y = ∅ χ)))
3935, 38elab 2681 . . . . . . . . . . . . 13 (y {x ∣ (x = ∅ φ)} ↔ (y = ∅ χ))
4034, 39syl6bbr 187 . . . . . . . . . . . 12 (y N → (χy {x ∣ (x = ∅ φ)}))
41 1pi 6299 . . . . . . . . . . . . . . . . . 18 1𝑜 N
42 addclpi 6311 . . . . . . . . . . . . . . . . . 18 ((y N 1𝑜 N) → (y +N 1𝑜) N)
4341, 42mpan2 401 . . . . . . . . . . . . . . . . 17 (y N → (y +N 1𝑜) N)
44 elni 6292 . . . . . . . . . . . . . . . . 17 ((y +N 1𝑜) N ↔ ((y +N 1𝑜) 𝜔 (y +N 1𝑜) ≠ ∅))
4543, 44sylib 127 . . . . . . . . . . . . . . . 16 (y N → ((y +N 1𝑜) 𝜔 (y +N 1𝑜) ≠ ∅))
4645simprd 107 . . . . . . . . . . . . . . 15 (y N → (y +N 1𝑜) ≠ ∅)
4746neneqd 2221 . . . . . . . . . . . . . 14 (y N → ¬ (y +N 1𝑜) = ∅)
48 biorf 662 . . . . . . . . . . . . . 14 (¬ (y +N 1𝑜) = ∅ → (θ ↔ ((y +N 1𝑜) = ∅ θ)))
4947, 48syl 14 . . . . . . . . . . . . 13 (y N → (θ ↔ ((y +N 1𝑜) = ∅ θ)))
50 eqeq1 2043 . . . . . . . . . . . . . . . 16 (x = (y +N 1𝑜) → (x = ∅ ↔ (y +N 1𝑜) = ∅))
51 indpi.3 . . . . . . . . . . . . . . . 16 (x = (y +N 1𝑜) → (φθ))
5250, 51orbi12d 706 . . . . . . . . . . . . . . 15 (x = (y +N 1𝑜) → ((x = ∅ φ) ↔ ((y +N 1𝑜) = ∅ θ)))
5352elabg 2682 . . . . . . . . . . . . . 14 ((y +N 1𝑜) N → ((y +N 1𝑜) {x ∣ (x = ∅ φ)} ↔ ((y +N 1𝑜) = ∅ θ)))
5443, 53syl 14 . . . . . . . . . . . . 13 (y N → ((y +N 1𝑜) {x ∣ (x = ∅ φ)} ↔ ((y +N 1𝑜) = ∅ θ)))
55 addpiord 6300 . . . . . . . . . . . . . . . 16 ((y N 1𝑜 N) → (y +N 1𝑜) = (y +𝑜 1𝑜))
5641, 55mpan2 401 . . . . . . . . . . . . . . 15 (y N → (y +N 1𝑜) = (y +𝑜 1𝑜))
57 pion 6294 . . . . . . . . . . . . . . . 16 (y Ny On)
58 oa1suc 5986 . . . . . . . . . . . . . . . 16 (y On → (y +𝑜 1𝑜) = suc y)
5957, 58syl 14 . . . . . . . . . . . . . . 15 (y N → (y +𝑜 1𝑜) = suc y)
6056, 59eqtrd 2069 . . . . . . . . . . . . . 14 (y N → (y +N 1𝑜) = suc y)
6160eleq1d 2103 . . . . . . . . . . . . 13 (y N → ((y +N 1𝑜) {x ∣ (x = ∅ φ)} ↔ suc y {x ∣ (x = ∅ φ)}))
6249, 54, 613bitr2d 205 . . . . . . . . . . . 12 (y N → (θ ↔ suc y {x ∣ (x = ∅ φ)}))
6329, 40, 623imtr3d 191 . . . . . . . . . . 11 (y N → (y {x ∣ (x = ∅ φ)} → suc y {x ∣ (x = ∅ φ)}))
6463a1i 9 . . . . . . . . . 10 (y 𝜔 → (y N → (y {x ∣ (x = ∅ φ)} → suc y {x ∣ (x = ∅ φ)})))
65 nndceq0 4282 . . . . . . . . . . . 12 (y 𝜔 → DECID y = ∅)
66 df-dc 742 . . . . . . . . . . . 12 (DECID y = ∅ ↔ (y = ∅ ¬ y = ∅))
6765, 66sylib 127 . . . . . . . . . . 11 (y 𝜔 → (y = ∅ ¬ y = ∅))
68 idd 21 . . . . . . . . . . . . . . 15 (y 𝜔 → (y = ∅ → y = ∅))
6968necon3bd 2242 . . . . . . . . . . . . . 14 (y 𝜔 → (¬ y = ∅ → y ≠ ∅))
7069anc2li 312 . . . . . . . . . . . . 13 (y 𝜔 → (¬ y = ∅ → (y 𝜔 y ≠ ∅)))
7170, 30syl6ibr 151 . . . . . . . . . . . 12 (y 𝜔 → (¬ y = ∅ → y N))
7271orim2d 701 . . . . . . . . . . 11 (y 𝜔 → ((y = ∅ ¬ y = ∅) → (y = ∅ y N)))
7367, 72mpd 13 . . . . . . . . . 10 (y 𝜔 → (y = ∅ y N))
7428, 64, 73mpjaod 637 . . . . . . . . 9 (y 𝜔 → (y {x ∣ (x = ∅ φ)} → suc y {x ∣ (x = ∅ φ)}))
7574rgen 2368 . . . . . . . 8 y 𝜔 (y {x ∣ (x = ∅ φ)} → suc y {x ∣ (x = ∅ φ)})
76 peano5 4264 . . . . . . . 8 ((∅ {x ∣ (x = ∅ φ)} y 𝜔 (y {x ∣ (x = ∅ φ)} → suc y {x ∣ (x = ∅ φ)})) → 𝜔 ⊆ {x ∣ (x = ∅ φ)})
7713, 75, 76mp2an 402 . . . . . . 7 𝜔 ⊆ {x ∣ (x = ∅ φ)}
7877sseli 2935 . . . . . 6 (x 𝜔 → x {x ∣ (x = ∅ φ)})
79 abid 2025 . . . . . 6 (x {x ∣ (x = ∅ φ)} ↔ (x = ∅ φ))
8078, 79sylib 127 . . . . 5 (x 𝜔 → (x = ∅ φ))
8180adantr 261 . . . 4 ((x 𝜔 x ≠ ∅) → (x = ∅ φ))
82 df-ne 2203 . . . . . 6 (x ≠ ∅ ↔ ¬ x = ∅)
83 biorf 662 . . . . . 6 x = ∅ → (φ ↔ (x = ∅ φ)))
8482, 83sylbi 114 . . . . 5 (x ≠ ∅ → (φ ↔ (x = ∅ φ)))
8584adantl 262 . . . 4 ((x 𝜔 x ≠ ∅) → (φ ↔ (x = ∅ φ)))
8681, 85mpbird 156 . . 3 ((x 𝜔 x ≠ ∅) → φ)
872, 86sylbi 114 . 2 (x Nφ)
881, 87vtoclga 2613 1 (A Nτ)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4   wa 97  wb 98   wo 628  DECID wdc 741   = wceq 1242   wcel 1390  {cab 2023  wne 2201  wral 2300  [wsbc 2758  wss 2911  c0 3218  Oncon0 4066  suc csuc 4068  𝜔com 4256  (class class class)co 5455  1𝑜c1o 5933   +𝑜 coa 5937  Ncnpi 6256   +N cpli 6257
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 544  ax-in2 545  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bnd 1396  ax-4 1397  ax-13 1401  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-coll 3863  ax-sep 3866  ax-nul 3874  ax-pow 3918  ax-pr 3935  ax-un 4136  ax-setind 4220  ax-iinf 4254
This theorem depends on definitions:  df-bi 110  df-dc 742  df-3an 886  df-tru 1245  df-fal 1248  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ne 2203  df-ral 2305  df-rex 2306  df-reu 2307  df-rab 2309  df-v 2553  df-sbc 2759  df-csb 2847  df-dif 2914  df-un 2916  df-in 2918  df-ss 2925  df-nul 3219  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-uni 3572  df-int 3607  df-iun 3650  df-br 3756  df-opab 3810  df-mpt 3811  df-tr 3846  df-id 4021  df-iord 4069  df-on 4071  df-suc 4074  df-iom 4257  df-xp 4294  df-rel 4295  df-cnv 4296  df-co 4297  df-dm 4298  df-rn 4299  df-res 4300  df-ima 4301  df-iota 4810  df-fun 4847  df-fn 4848  df-f 4849  df-f1 4850  df-fo 4851  df-f1o 4852  df-fv 4853  df-ov 5458  df-oprab 5459  df-mpt2 5460  df-1st 5709  df-2nd 5710  df-recs 5861  df-irdg 5897  df-1o 5940  df-oadd 5944  df-ni 6288  df-pli 6289
This theorem is referenced by:  pitonn  6744
  Copyright terms: Public domain W3C validator