![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 1nn | GIF version |
Description: Peano postulate: 1 is a positive integer. (Contributed by NM, 11-Jan-1997.) |
Ref | Expression |
---|---|
1nn | ⊢ 1 ∈ ℕ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfnn2 8108 | . . . 4 ⊢ ℕ = ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} | |
2 | 1 | eleq2i 2146 | . . 3 ⊢ (1 ∈ ℕ ↔ 1 ∈ ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}) |
3 | 1re 7180 | . . . 4 ⊢ 1 ∈ ℝ | |
4 | elintg 3652 | . . . 4 ⊢ (1 ∈ ℝ → (1 ∈ ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} ↔ ∀𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}1 ∈ 𝑧)) | |
5 | 3, 4 | ax-mp 7 | . . 3 ⊢ (1 ∈ ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} ↔ ∀𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}1 ∈ 𝑧) |
6 | 2, 5 | bitri 182 | . 2 ⊢ (1 ∈ ℕ ↔ ∀𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}1 ∈ 𝑧) |
7 | vex 2605 | . . . 4 ⊢ 𝑧 ∈ V | |
8 | eleq2 2143 | . . . . 5 ⊢ (𝑥 = 𝑧 → (1 ∈ 𝑥 ↔ 1 ∈ 𝑧)) | |
9 | eleq2 2143 | . . . . . 6 ⊢ (𝑥 = 𝑧 → ((𝑦 + 1) ∈ 𝑥 ↔ (𝑦 + 1) ∈ 𝑧)) | |
10 | 9 | raleqbi1dv 2558 | . . . . 5 ⊢ (𝑥 = 𝑧 → (∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥 ↔ ∀𝑦 ∈ 𝑧 (𝑦 + 1) ∈ 𝑧)) |
11 | 8, 10 | anbi12d 457 | . . . 4 ⊢ (𝑥 = 𝑧 → ((1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥) ↔ (1 ∈ 𝑧 ∧ ∀𝑦 ∈ 𝑧 (𝑦 + 1) ∈ 𝑧))) |
12 | 7, 11 | elab 2739 | . . 3 ⊢ (𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} ↔ (1 ∈ 𝑧 ∧ ∀𝑦 ∈ 𝑧 (𝑦 + 1) ∈ 𝑧)) |
13 | 12 | simplbi 268 | . 2 ⊢ (𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} → 1 ∈ 𝑧) |
14 | 6, 13 | mprgbir 2422 | 1 ⊢ 1 ∈ ℕ |
Colors of variables: wff set class |
Syntax hints: ∧ wa 102 ↔ wb 103 ∈ wcel 1434 {cab 2068 ∀wral 2349 ∩ cint 3644 (class class class)co 5543 ℝcr 7042 1c1 7044 + caddc 7046 ℕcn 8106 |
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-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-17 1460 ax-i9 1464 ax-ial 1468 ax-i5r 1469 ax-ext 2064 ax-1re 7132 |
This theorem depends on definitions: df-bi 115 df-tru 1288 df-nf 1391 df-sb 1687 df-clab 2069 df-cleq 2075 df-clel 2078 df-nfc 2209 df-ral 2354 df-v 2604 df-int 3645 df-inn 8107 |
This theorem is referenced by: nnind 8122 nn1suc 8125 2nn 8260 1nn0 8371 nn0p1nn 8394 1z 8458 neg1z 8464 elz2 8500 nneoor 8530 9p1e10 8560 indstr 8762 elnn1uz2 8775 zq 8792 qreccl 8808 fz01or 9204 expivallem 9574 exp1 9579 nnexpcl 9586 expnbnd 9693 3dec 9739 fac1 9753 faccl 9759 faclbnd3 9767 resqrexlemf1 10032 resqrexlemcalc3 10040 resqrexlemnmsq 10041 resqrexlemnm 10042 resqrexlemcvg 10043 resqrexlemglsq 10046 resqrexlemga 10047 n2dvds1 10456 ndvdsp1 10476 gcd1 10522 bezoutr1 10566 ncoprmgcdne1b 10615 1nprm 10640 1idssfct 10641 isprm2lem 10642 |
Copyright terms: Public domain | W3C validator |