Users' Mathboxes Mathbox for BJ < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >   Mathboxes  >  peano5set GIF version

Theorem peano5set 10986
Description: Version of peano5 4368 when ω ∩ 𝐴 is assumed to be a set, allowing a proof from the core axioms of CZF. (Contributed by BJ, 19-Nov-2019.) (Proof modification is discouraged.)
Assertion
Ref Expression
peano5set ((ω ∩ 𝐴) ∈ 𝑉 → ((∅ ∈ 𝐴 ∧ ∀𝑥 ∈ ω (𝑥𝐴 → suc 𝑥𝐴)) → ω ⊆ 𝐴))
Distinct variable group:   𝑥,𝐴
Allowed substitution hint:   𝑉(𝑥)

Proof of Theorem peano5set
StepHypRef Expression
1 bj-omind 10980 . . . . 5 Ind ω
2 bj-indind 10978 . . . . 5 ((Ind ω ∧ (∅ ∈ 𝐴 ∧ ∀𝑥 ∈ ω (𝑥𝐴 → suc 𝑥𝐴))) → Ind (ω ∩ 𝐴))
31, 2mpan 415 . . . 4 ((∅ ∈ 𝐴 ∧ ∀𝑥 ∈ ω (𝑥𝐴 → suc 𝑥𝐴)) → Ind (ω ∩ 𝐴))
4 bj-omssind 10981 . . . . 5 ((ω ∩ 𝐴) ∈ 𝑉 → (Ind (ω ∩ 𝐴) → ω ⊆ (ω ∩ 𝐴)))
54imp 122 . . . 4 (((ω ∩ 𝐴) ∈ 𝑉 ∧ Ind (ω ∩ 𝐴)) → ω ⊆ (ω ∩ 𝐴))
63, 5sylan2 280 . . 3 (((ω ∩ 𝐴) ∈ 𝑉 ∧ (∅ ∈ 𝐴 ∧ ∀𝑥 ∈ ω (𝑥𝐴 → suc 𝑥𝐴))) → ω ⊆ (ω ∩ 𝐴))
7 inss2 3204 . . 3 (ω ∩ 𝐴) ⊆ 𝐴
86, 7syl6ss 3021 . 2 (((ω ∩ 𝐴) ∈ 𝑉 ∧ (∅ ∈ 𝐴 ∧ ∀𝑥 ∈ ω (𝑥𝐴 → suc 𝑥𝐴))) → ω ⊆ 𝐴)
98ex 113 1 ((ω ∩ 𝐴) ∈ 𝑉 → ((∅ ∈ 𝐴 ∧ ∀𝑥 ∈ ω (𝑥𝐴 → suc 𝑥𝐴)) → ω ⊆ 𝐴))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wcel 1434  wral 2353  cin 2982  wss 2983  c0 3268  suc csuc 4149  ωcom 4360  Ind wind 10972
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-13 1445  ax-14 1446  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065  ax-nul 3925  ax-pr 3993  ax-un 4217  ax-bd0 10855  ax-bdor 10858  ax-bdex 10861  ax-bdeq 10862  ax-bdel 10863  ax-bdsb 10864  ax-bdsep 10926
This theorem depends on definitions:  df-bi 115  df-tru 1288  df-nf 1391  df-sb 1688  df-clab 2070  df-cleq 2076  df-clel 2079  df-nfc 2212  df-ral 2358  df-rex 2359  df-rab 2362  df-v 2612  df-dif 2985  df-un 2987  df-in 2989  df-ss 2996  df-nul 3269  df-sn 3423  df-pr 3424  df-uni 3623  df-int 3658  df-suc 4155  df-iom 4361  df-bdc 10883  df-bj-ind 10973
This theorem is referenced by:  bdpeano5  10989  speano5  10990
  Copyright terms: Public domain W3C validator