Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > ordirr | Unicode version |
Description: Epsilon irreflexivity of ordinals: no ordinal class is a member of itself. Theorem 2.2(i) of [BellMachover] p. 469, generalized to classes. The present proof requires ax-setind 4452. If in the definition of ordinals df-iord 4288, we also required that membership be well-founded on any ordinal (see df-frind 4254), then we could prove ordirr 4457 without ax-setind 4452. (Contributed by NM, 2-Jan-1994.) |
Ref | Expression |
---|---|
ordirr |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elirr 4456 | . 2 | |
2 | 1 | a1i 9 | 1 |
Colors of variables: wff set class |
Syntax hints: wn 3 wi 4 wcel 1480 word 4284 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 603 ax-in2 604 ax-io 698 ax-5 1423 ax-7 1424 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-8 1482 ax-10 1483 ax-11 1484 ax-i12 1485 ax-bndl 1486 ax-4 1487 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2121 ax-setind 4452 |
This theorem depends on definitions: df-bi 116 df-3an 964 df-tru 1334 df-nf 1437 df-sb 1736 df-clab 2126 df-cleq 2132 df-clel 2135 df-nfc 2270 df-ne 2309 df-ral 2421 df-v 2688 df-dif 3073 df-sn 3533 |
This theorem is referenced by: onirri 4458 nordeq 4459 ordn2lp 4460 orddisj 4461 onprc 4467 nlimsucg 4481 tfr1onlemsucfn 6237 tfr1onlemsucaccv 6238 tfrcllemsucfn 6250 tfrcllemsucaccv 6251 nntr2 6399 unsnfi 6807 addnidpig 7144 frecfzennn 10199 hashinfom 10524 hashennn 10526 hashp1i 10556 ennnfonelemg 11916 ctinfom 11941 nninfalllemn 13202 |
Copyright terms: Public domain | W3C validator |