Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > elnn | Structured version Visualization version GIF version |
Description: A member of a natural number is a natural number. (Contributed by NM, 21-Jun-1998.) |
Ref | Expression |
---|---|
elnn | ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ ω) → 𝐴 ∈ ω) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ordom 7620 | . 2 ⊢ Ord ω | |
2 | ordtr 6196 | . 2 ⊢ (Ord ω → Tr ω) | |
3 | trel 5153 | . 2 ⊢ (Tr ω → ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ ω) → 𝐴 ∈ ω)) | |
4 | 1, 2, 3 | mp2b 10 | 1 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ ω) → 𝐴 ∈ ω) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 ∈ wcel 2114 Tr wtr 5146 Ord word 6181 ωcom 7611 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 ax-8 2116 ax-9 2124 ax-11 2162 ax-ext 2711 ax-sep 5177 ax-nul 5184 ax-pr 5306 ax-un 7491 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1787 df-sb 2075 df-clab 2718 df-cleq 2731 df-clel 2812 df-ne 2936 df-ral 3059 df-rex 3060 df-rab 3063 df-v 3402 df-dif 3856 df-un 3858 df-in 3860 df-ss 3870 df-pss 3872 df-nul 4222 df-if 4425 df-sn 4527 df-pr 4529 df-tp 4531 df-op 4533 df-uni 4807 df-br 5041 df-opab 5103 df-tr 5147 df-eprel 5444 df-po 5452 df-so 5453 df-fr 5493 df-we 5495 df-ord 6185 df-on 6186 df-lim 6187 df-om 7612 |
This theorem is referenced by: nnaordi 8287 nnmordi 8300 pssnn 8779 ssnnfi 8780 ssnnfiOLD 8781 pssnnOLD 8827 unfilem1 8868 unfilem2 8869 inf3lem5 9180 cantnflt 9220 cantnfp1lem3 9228 cantnflem1d 9236 cantnflem1 9237 cnfcomlem 9247 cnfcom 9248 infpssrlem4 9818 axdc3lem2 9963 pwfseqlem3 10172 bnj1098 32346 bnj517 32448 bnj594 32475 bnj1001 32522 bnj1118 32547 bnj1128 32553 bnj1145 32556 elhf2 34132 hfelhf 34138 |
Copyright terms: Public domain | W3C validator |