Theorem ordirr 3023

Description: Epsilon irreflexivity of ordinals: no ordinal class is a member of itself. Theorem 2.2(i) of [BellMachover] p. 469, generalized to classes. We prove this without invoking the Axiom of Regularity.

Assertion

Ref	Expression
ordirr	|- (Ord A -> -. A e. A)

Proof of Theorem ordirr

Step	Hyp	Ref	Expression
1		ordfr 3020	. 2 |- (Ord A -> E Fr A)
2		efrirr 2985	. 2 |- (E Fr A -> -. A e. A)
3	1, 2	syl 10	1 |- (Ord A -> -. A e. A)

Syntax hints:  -. wn 2   -> wi 3   e. wcel 999  Ecep 2886   Fr wfr 2972  Ord word 3004

This theorem is referenced by:  nordeq 3024  ordn2lp 3025  ordtri3or 3036  ordtri1 3037  ordtri3 3040  orddisj 3042  onprc 3046  ordunidif 3062  ordnbtwn 3120  onsucuni2 3148  onirri 3154  onssneli 3158  nlimsucg 3169  nnlim 3201  limom 3203  tfrlem13 3981  limensuci 4571  infensuc 4700  ondomcard 4922  addnidpi 5093

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1003  ax-gen 1004  ax-8 1005  ax-10 1007  ax-11 1008  ax-12 1009  ax-13 1010  ax-14 1011  ax-17 1012  ax-4 1014  ax-5o 1016  ax-6o 1019  ax-9o 1164  ax-10o 1182  ax-16 1252  ax-11o 1260  ax-ext 1504  ax-sep 2758  ax-pow 2798  ax-pr 2835

This theorem depends on definitions:  df-bi 154  df-or 231  df-an 232  df-3an 789  df-ex 1022  df-sb 1214  df-eu 1424  df-mo 1425  df-clab 1510  df-cleq 1515  df-clel 1518  df-ne 1634  df-ral 1696  df-rex 1697  df-v 1859  df-dif 2100  df-un 2101  df-in 2102  df-ss 2104  df-nul 2332  df-pw 2454  df-sn 2464  df-pr 2465  df-op 2468  df-br 2675  df-opab 2722  df-eprel 2888  df-fr 2974  df-we 2991  df-ord 3008

Copyright terms: Public domain