![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 0lt1o | Structured version Visualization version GIF version |
Description: Ordinal zero is less than ordinal one. (Contributed by NM, 5-Jan-2005.) |
Ref | Expression |
---|---|
0lt1o | ⊢ ∅ ∈ 1o |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2826 | . 2 ⊢ ∅ = ∅ | |
2 | el1o 7847 | . 2 ⊢ (∅ ∈ 1o ↔ ∅ = ∅) | |
3 | 1, 2 | mpbir 223 | 1 ⊢ ∅ ∈ 1o |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1658 ∈ wcel 2166 ∅c0 4145 1oc1o 7820 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-4 1910 ax-5 2011 ax-6 2077 ax-7 2114 ax-9 2175 ax-10 2194 ax-11 2209 ax-12 2222 ax-13 2391 ax-ext 2804 ax-nul 5014 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 881 df-tru 1662 df-ex 1881 df-nf 1885 df-sb 2070 df-clab 2813 df-cleq 2819 df-clel 2822 df-nfc 2959 df-v 3417 df-dif 3802 df-un 3804 df-nul 4146 df-sn 4399 df-suc 5970 df-1o 7827 |
This theorem is referenced by: dif20el 7853 oe1m 7893 oen0 7934 oeoa 7945 oeoe 7947 isfin4-3 9453 fin1a2lem4 9541 1lt2pi 10043 indpi 10045 sadcp1 15551 vr1cl2 19924 fvcoe1 19938 vr1cl 19948 subrgvr1cl 19993 coe1mul2lem1 19998 coe1tm 20004 ply1coe 20027 evl1var 20061 evls1var 20063 xkofvcn 21859 pw2f1ocnv 38448 wepwsolem 38456 |
Copyright terms: Public domain | W3C validator |