![]() |
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 8580 | . . . 4 ⊢ ℕ = ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} | |
2 | 1 | eleq2i 2166 | . . 3 ⊢ (1 ∈ ℕ ↔ 1 ∈ ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}) |
3 | 1re 7637 | . . . 4 ⊢ 1 ∈ ℝ | |
4 | elintg 3726 | . . . 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 183 | . 2 ⊢ (1 ∈ ℕ ↔ ∀𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}1 ∈ 𝑧) |
7 | vex 2644 | . . . 4 ⊢ 𝑧 ∈ V | |
8 | eleq2 2163 | . . . . 5 ⊢ (𝑥 = 𝑧 → (1 ∈ 𝑥 ↔ 1 ∈ 𝑧)) | |
9 | eleq2 2163 | . . . . . 6 ⊢ (𝑥 = 𝑧 → ((𝑦 + 1) ∈ 𝑥 ↔ (𝑦 + 1) ∈ 𝑧)) | |
10 | 9 | raleqbi1dv 2592 | . . . . 5 ⊢ (𝑥 = 𝑧 → (∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥 ↔ ∀𝑦 ∈ 𝑧 (𝑦 + 1) ∈ 𝑧)) |
11 | 8, 10 | anbi12d 460 | . . . 4 ⊢ (𝑥 = 𝑧 → ((1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥) ↔ (1 ∈ 𝑧 ∧ ∀𝑦 ∈ 𝑧 (𝑦 + 1) ∈ 𝑧))) |
12 | 7, 11 | elab 2782 | . . 3 ⊢ (𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} ↔ (1 ∈ 𝑧 ∧ ∀𝑦 ∈ 𝑧 (𝑦 + 1) ∈ 𝑧)) |
13 | 12 | simplbi 270 | . 2 ⊢ (𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} → 1 ∈ 𝑧) |
14 | 6, 13 | mprgbir 2449 | 1 ⊢ 1 ∈ ℕ |
Colors of variables: wff set class |
Syntax hints: ∧ wa 103 ↔ wb 104 ∈ wcel 1448 {cab 2086 ∀wral 2375 ∩ cint 3718 (class class class)co 5706 ℝcr 7499 1c1 7501 + caddc 7503 ℕcn 8578 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 671 ax-5 1391 ax-7 1392 ax-gen 1393 ax-ie1 1437 ax-ie2 1438 ax-8 1450 ax-10 1451 ax-11 1452 ax-i12 1453 ax-bndl 1454 ax-4 1455 ax-17 1474 ax-i9 1478 ax-ial 1482 ax-i5r 1483 ax-ext 2082 ax-1re 7589 |
This theorem depends on definitions: df-bi 116 df-tru 1302 df-nf 1405 df-sb 1704 df-clab 2087 df-cleq 2093 df-clel 2096 df-nfc 2229 df-ral 2380 df-v 2643 df-int 3719 df-inn 8579 |
This theorem is referenced by: nnind 8594 nn1suc 8597 2nn 8733 1nn0 8845 nn0p1nn 8868 1z 8932 neg1z 8938 elz2 8974 nneoor 9005 9p1e10 9036 indstr 9238 elnn1uz2 9251 zq 9268 qreccl 9284 fz01or 9732 exp3vallem 10135 exp1 10140 nnexpcl 10147 expnbnd 10256 3dec 10302 fac1 10316 faccl 10322 faclbnd3 10330 resqrexlemf1 10620 resqrexlemcalc3 10628 resqrexlemnmsq 10629 resqrexlemnm 10630 resqrexlemcvg 10631 resqrexlemglsq 10634 resqrexlemga 10635 sumsnf 11017 cvgratnnlemnexp 11132 cvgratnnlemfm 11137 cvgratnnlemrate 11138 cvgratnn 11139 eftlub 11194 eirraplem 11278 n2dvds1 11404 ndvdsp1 11424 gcd1 11470 bezoutr1 11514 ncoprmgcdne1b 11563 1nprm 11588 1idssfct 11589 isprm2lem 11590 qden1elz 11675 phicl2 11682 phi1 11687 phiprm 11691 exmidunben 11731 base0 11790 baseval 11793 baseid 11794 basendx 11795 basendxnn 11796 1strstrg 11839 2strstrg 11841 basendxnplusgndx 11847 basendxnmulrndx 11855 rngstrg 11856 lmodstrd 11874 topgrpstrd 11892 setsmsdsg 12408 trilpolemgt1 12816 |
Copyright terms: Public domain | W3C validator |