Theorem 0lt2o 6517

Description: Ordinal zero is less than ordinal two. (Contributed by Jim Kingdon, 31-Jul-2022.)

Assertion

Ref	Expression
0lt2o	⊢ ∅ ∈ 2o

Proof of Theorem 0lt2o

Step	Hyp	Ref	Expression
1		0ex 4170	. . 3 ⊢ ∅ ∈ V
2	1	prid1 3738	. 2 ⊢ ∅ ∈ {∅, 1o}
3		df2o3 6506	. 2 ⊢ 2o = {∅, 1o}
4	2, 3	eleqtrri 2280	1 ⊢ ∅ ∈ 2o

Syntax hints:   ∈ wcel 2175  ∅c0 3459  {cpr 3633  1_oc1o 6485  2_oc2o 6486

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-in1 615  ax-in2 616  ax-io 710  ax-5 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186  ax-nul 4169

This theorem depends on definitions:  df-bi 117  df-tru 1375  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-v 2773  df-dif 3167  df-un 3169  df-nul 3460  df-sn 3638  df-pr 3639  df-suc 4416  df-1o 6492  df-2o 6493

This theorem is referenced by:  nnnninf  7210  nnnninfeq  7212  fodjuf  7229  mkvprop  7242  nninfwlporlemd  7256  nninfwlporlem  7257  nninfwlpoimlemg  7259  nninfwlpoimlemginf  7260  2oneel  7350  2omotaplemst  7352  nninfinf  10569  nninfctlemfo  12280  unct  12732  xpsfeq  13095  xpsfval  13098  xpsval  13102  bj-charfun  15607  bj-charfundc  15608  012of  15794  2omap  15796  pwle2  15799  subctctexmid  15801  0nninf  15805  nninfsellemcl  15812  nninffeq  15821