![]() |
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 8952 | . . . 4 ⊢ ℕ = ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} | |
2 | 1 | eleq2i 2256 | . . 3 ⊢ (1 ∈ ℕ ↔ 1 ∈ ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}) |
3 | 1re 7987 | . . . 4 ⊢ 1 ∈ ℝ | |
4 | elintg 3867 | . . . 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 184 | . 2 ⊢ (1 ∈ ℕ ↔ ∀𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}1 ∈ 𝑧) |
7 | vex 2755 | . . . 4 ⊢ 𝑧 ∈ V | |
8 | eleq2 2253 | . . . . 5 ⊢ (𝑥 = 𝑧 → (1 ∈ 𝑥 ↔ 1 ∈ 𝑧)) | |
9 | eleq2 2253 | . . . . . 6 ⊢ (𝑥 = 𝑧 → ((𝑦 + 1) ∈ 𝑥 ↔ (𝑦 + 1) ∈ 𝑧)) | |
10 | 9 | raleqbi1dv 2694 | . . . . 5 ⊢ (𝑥 = 𝑧 → (∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥 ↔ ∀𝑦 ∈ 𝑧 (𝑦 + 1) ∈ 𝑧)) |
11 | 8, 10 | anbi12d 473 | . . . 4 ⊢ (𝑥 = 𝑧 → ((1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥) ↔ (1 ∈ 𝑧 ∧ ∀𝑦 ∈ 𝑧 (𝑦 + 1) ∈ 𝑧))) |
12 | 7, 11 | elab 2896 | . . 3 ⊢ (𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} ↔ (1 ∈ 𝑧 ∧ ∀𝑦 ∈ 𝑧 (𝑦 + 1) ∈ 𝑧)) |
13 | 12 | simplbi 274 | . 2 ⊢ (𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} → 1 ∈ 𝑧) |
14 | 6, 13 | mprgbir 2548 | 1 ⊢ 1 ∈ ℕ |
Colors of variables: wff set class |
Syntax hints: ∧ wa 104 ↔ wb 105 ∈ wcel 2160 {cab 2175 ∀wral 2468 ∩ cint 3859 (class class class)co 5897 ℝcr 7841 1c1 7843 + caddc 7845 ℕcn 8950 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 710 ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-ext 2171 ax-1re 7936 |
This theorem depends on definitions: df-bi 117 df-tru 1367 df-nf 1472 df-sb 1774 df-clab 2176 df-cleq 2182 df-clel 2185 df-nfc 2321 df-ral 2473 df-v 2754 df-int 3860 df-inn 8951 |
This theorem is referenced by: nnind 8966 nn1suc 8969 2nn 9111 1nn0 9223 nn0p1nn 9246 1z 9310 neg1z 9316 elz2 9355 nneoor 9386 9p1e10 9417 indstr 9625 elnn1uz2 9639 zq 9658 qreccl 9674 fz01or 10143 exp3vallem 10555 exp1 10560 nnexpcl 10567 expnbnd 10678 3dec 10729 fac1 10744 faccl 10750 faclbnd3 10758 fiubnn 10845 resqrexlemf1 11052 resqrexlemcalc3 11060 resqrexlemnmsq 11061 resqrexlemnm 11062 resqrexlemcvg 11063 resqrexlemglsq 11066 resqrexlemga 11067 sumsnf 11452 cvgratnnlemnexp 11567 cvgratnnlemfm 11572 cvgratnnlemrate 11573 cvgratnn 11574 prodsnf 11635 fprodnncl 11653 eftlub 11733 eirraplem 11819 n2dvds1 11952 ndvdsp1 11972 gcd1 12023 bezoutr1 12069 ncoprmgcdne1b 12124 1nprm 12149 1idssfct 12150 isprm2lem 12151 qden1elz 12240 phicl2 12249 phi1 12254 phiprm 12258 eulerthlema 12265 pcpre1 12327 pczpre 12332 pcmptcl 12377 pcmpt 12378 infpnlem2 12395 mul4sq 12429 exmidunben 12480 nninfdc 12507 base0 12565 baseval 12568 baseid 12569 basendx 12570 basendxnn 12571 1strstrg 12631 2strstrg 12633 basendxnplusgndx 12639 basendxnmulrndx 12648 rngstrg 12649 lmodstrd 12678 topgrpstrd 12710 basendxltdsndx 12729 dsndxnplusgndx 12731 dsndxnmulrndx 12732 slotsdnscsi 12733 dsndxntsetndx 12734 slotsdifdsndx 12735 basendxltunifndx 12739 unifndxntsetndx 12741 slotsdifunifndx 12742 mulg1 13086 mulg2 13088 mulgnndir 13108 cnfldstr 13883 setsmsdsg 14457 lgsdir2lem1 14907 lgsdir2lem4 14910 lgsdir2lem5 14911 lgsdir 14914 lgsne0 14917 lgs1 14923 trilpolemgt1 15266 |
Copyright terms: Public domain | W3C validator |