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 8690 | . . . 4 ⊢ ℕ = ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} | |
2 | 1 | eleq2i 2184 | . . 3 ⊢ (1 ∈ ℕ ↔ 1 ∈ ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}) |
3 | 1re 7733 | . . . 4 ⊢ 1 ∈ ℝ | |
4 | elintg 3749 | . . . 4 ⊢ (1 ∈ ℝ → (1 ∈ ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} ↔ ∀𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}1 ∈ 𝑧)) | |
5 | 3, 4 | ax-mp 5 | . . 3 ⊢ (1 ∈ ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} ↔ ∀𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}1 ∈ 𝑧) |
6 | 2, 5 | bitri 183 | . 2 ⊢ (1 ∈ ℕ ↔ ∀𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}1 ∈ 𝑧) |
7 | vex 2663 | . . . 4 ⊢ 𝑧 ∈ V | |
8 | eleq2 2181 | . . . . 5 ⊢ (𝑥 = 𝑧 → (1 ∈ 𝑥 ↔ 1 ∈ 𝑧)) | |
9 | eleq2 2181 | . . . . . 6 ⊢ (𝑥 = 𝑧 → ((𝑦 + 1) ∈ 𝑥 ↔ (𝑦 + 1) ∈ 𝑧)) | |
10 | 9 | raleqbi1dv 2611 | . . . . 5 ⊢ (𝑥 = 𝑧 → (∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥 ↔ ∀𝑦 ∈ 𝑧 (𝑦 + 1) ∈ 𝑧)) |
11 | 8, 10 | anbi12d 464 | . . . 4 ⊢ (𝑥 = 𝑧 → ((1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥) ↔ (1 ∈ 𝑧 ∧ ∀𝑦 ∈ 𝑧 (𝑦 + 1) ∈ 𝑧))) |
12 | 7, 11 | elab 2802 | . . 3 ⊢ (𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} ↔ (1 ∈ 𝑧 ∧ ∀𝑦 ∈ 𝑧 (𝑦 + 1) ∈ 𝑧)) |
13 | 12 | simplbi 272 | . 2 ⊢ (𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} → 1 ∈ 𝑧) |
14 | 6, 13 | mprgbir 2467 | 1 ⊢ 1 ∈ ℕ |
Colors of variables: wff set class |
Syntax hints: ∧ wa 103 ↔ wb 104 ∈ wcel 1465 {cab 2103 ∀wral 2393 ∩ cint 3741 (class class class)co 5742 ℝcr 7587 1c1 7589 + caddc 7591 ℕcn 8688 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 683 ax-5 1408 ax-7 1409 ax-gen 1410 ax-ie1 1454 ax-ie2 1455 ax-8 1467 ax-10 1468 ax-11 1469 ax-i12 1470 ax-bndl 1471 ax-4 1472 ax-17 1491 ax-i9 1495 ax-ial 1499 ax-i5r 1500 ax-ext 2099 ax-1re 7682 |
This theorem depends on definitions: df-bi 116 df-tru 1319 df-nf 1422 df-sb 1721 df-clab 2104 df-cleq 2110 df-clel 2113 df-nfc 2247 df-ral 2398 df-v 2662 df-int 3742 df-inn 8689 |
This theorem is referenced by: nnind 8704 nn1suc 8707 2nn 8849 1nn0 8961 nn0p1nn 8984 1z 9048 neg1z 9054 elz2 9090 nneoor 9121 9p1e10 9152 indstr 9356 elnn1uz2 9369 zq 9386 qreccl 9402 fz01or 9859 exp3vallem 10262 exp1 10267 nnexpcl 10274 expnbnd 10383 3dec 10429 fac1 10443 faccl 10449 faclbnd3 10457 resqrexlemf1 10748 resqrexlemcalc3 10756 resqrexlemnmsq 10757 resqrexlemnm 10758 resqrexlemcvg 10759 resqrexlemglsq 10762 resqrexlemga 10763 sumsnf 11146 cvgratnnlemnexp 11261 cvgratnnlemfm 11266 cvgratnnlemrate 11267 cvgratnn 11268 eftlub 11323 eirraplem 11410 n2dvds1 11536 ndvdsp1 11556 gcd1 11602 bezoutr1 11648 ncoprmgcdne1b 11697 1nprm 11722 1idssfct 11723 isprm2lem 11724 qden1elz 11810 phicl2 11817 phi1 11822 phiprm 11826 exmidunben 11866 base0 11935 baseval 11938 baseid 11939 basendx 11940 basendxnn 11941 1strstrg 11984 2strstrg 11986 basendxnplusgndx 11992 basendxnmulrndx 12000 rngstrg 12001 lmodstrd 12019 topgrpstrd 12037 setsmsdsg 12576 trilpolemgt1 13159 |
Copyright terms: Public domain | W3C validator |