![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > ordirr | GIF 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 4288. If in the definition of ordinals df-iord 4129, we also required that membership be well-founded on any ordinal (see df-frind 4095), then we could prove ordirr 4293 without ax-setind 4288. (Contributed by NM, 2-Jan-1994.) |
Ref | Expression |
---|---|
ordirr | ⊢ (Ord 𝐴 → ¬ 𝐴 ∈ 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elirr 4292 | . 2 ⊢ ¬ 𝐴 ∈ 𝐴 | |
2 | 1 | a1i 9 | 1 ⊢ (Ord 𝐴 → ¬ 𝐴 ∈ 𝐴) |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 → wi 4 ∈ wcel 1434 Ord word 4125 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-in1 577 ax-in2 578 ax-io 663 ax-5 1377 ax-7 1378 ax-gen 1379 ax-ie1 1423 ax-ie2 1424 ax-8 1436 ax-10 1437 ax-11 1438 ax-i12 1439 ax-bndl 1440 ax-4 1441 ax-17 1460 ax-i9 1464 ax-ial 1468 ax-i5r 1469 ax-ext 2064 ax-setind 4288 |
This theorem depends on definitions: df-bi 115 df-3an 922 df-tru 1288 df-nf 1391 df-sb 1687 df-clab 2069 df-cleq 2075 df-clel 2078 df-nfc 2209 df-ne 2247 df-ral 2354 df-v 2604 df-dif 2976 df-sn 3412 |
This theorem is referenced by: onirri 4294 nordeq 4295 ordn2lp 4296 orddisj 4297 onprc 4303 nlimsucg 4317 tfr1onlemsucfn 5989 tfr1onlemsucaccv 5990 tfrcllemsucfn 6002 tfrcllemsucaccv 6003 unsnfi 6439 addnidpig 6588 frecfzennn 9508 sizeinf 9802 sizeennn 9804 sizep1i 9834 |
Copyright terms: Public domain | W3C validator |