Theorem 1lt2o 6612

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

Assertion

Ref	Expression
1lt2o	⊢ 1o ∈ 2o

Proof of Theorem 1lt2o

Step	Hyp	Ref	Expression
1		1oex 6592	. . 3 ⊢ 1o ∈ V
2	1	prid2 3777	. 2 ⊢ 1o ∈ {∅, 1o}
3		df2o3 6599	. 2 ⊢ 2o = {∅, 1o}
4	2, 3	eleqtrri 2306	1 ⊢ 1o ∈ 2o

Syntax hints:   ∈ wcel 2201  ∅c0 3493  {cpr 3669  1_oc1o 6577  2_oc2o 6578

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 619  ax-in2 620  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-13 2203  ax-14 2204  ax-ext 2212  ax-sep 4206  ax-nul 4214  ax-pow 4263  ax-pr 4298  ax-un 4529

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1810  df-clab 2217  df-cleq 2223  df-clel 2226  df-nfc 2362  df-ral 2514  df-rex 2515  df-v 2803  df-dif 3201  df-un 3203  df-in 3205  df-ss 3212  df-nul 3494  df-pw 3653  df-sn 3674  df-pr 3675  df-uni 3893  df-tr 4187  df-iord 4462  df-on 4464  df-suc 4467  df-1o 6584  df-2o 6585

This theorem is referenced by:  en2  7000  1ndom2  7053  infnninf  7325  infnninfOLD  7326  nnnninf  7327  nnnninfeq  7329  nninfisollemne  7332  fodjuf  7346  mkvprop  7359  nninfwlporlemd  7373  nninfwlporlem  7374  nninfwlpoimlemg  7376  nninfwlpoimlemginf  7377  exmidonfinlem  7406  pw1ne3  7450  3nelsucpw1  7454  3nsssucpw1  7456  2oneel  7477  2omotaplemst  7479  nninfinf  10708  nninfctlemfo  12631  unct  13083  xpsfeq  13448  xpsfval  13451  xpsval  13455  bj-charfun  16460  bj-charfundc  16461  3dom  16645  012of  16650  2omap  16652  pwle2  16657  subctctexmid  16659  nnsf  16665  peano4nninf  16666  nninfsellemcl  16671  nninffeq  16680