![]() |
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 4412. If in the definition of ordinals df-iord 4248, we also required that membership be well-founded on any ordinal (see df-frind 4214), then we could prove ordirr 4417 without ax-setind 4412. (Contributed by NM, 2-Jan-1994.) |
Ref | Expression |
---|---|
ordirr |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elirr 4416 |
. 2
![]() ![]() ![]() ![]() ![]() | |
2 | 1 | a1i 9 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 586 ax-in2 587 ax-io 681 ax-5 1406 ax-7 1407 ax-gen 1408 ax-ie1 1452 ax-ie2 1453 ax-8 1465 ax-10 1466 ax-11 1467 ax-i12 1468 ax-bndl 1469 ax-4 1470 ax-17 1489 ax-i9 1493 ax-ial 1497 ax-i5r 1498 ax-ext 2097 ax-setind 4412 |
This theorem depends on definitions: df-bi 116 df-3an 947 df-tru 1317 df-nf 1420 df-sb 1719 df-clab 2102 df-cleq 2108 df-clel 2111 df-nfc 2244 df-ne 2283 df-ral 2395 df-v 2659 df-dif 3039 df-sn 3499 |
This theorem is referenced by: onirri 4418 nordeq 4419 ordn2lp 4420 orddisj 4421 onprc 4427 nlimsucg 4441 tfr1onlemsucfn 6191 tfr1onlemsucaccv 6192 tfrcllemsucfn 6204 tfrcllemsucaccv 6205 nntr2 6353 unsnfi 6760 addnidpig 7092 frecfzennn 10092 hashinfom 10417 hashennn 10419 hashp1i 10449 ennnfonelemg 11761 ctinfom 11786 nninfalllemn 12892 |
Copyright terms: Public domain | W3C validator |