Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > ontri2orexmidim | Unicode version |
Description: Ordinal trichotomy implies excluded middle. Closed form of ordtri2or2exmid 4548. (Contributed by Jim Kingdon, 26-Aug-2024.) |
Ref | Expression |
---|---|
ontri2orexmidim | DECID |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ordtri2or2exmidlem 4503 | . . . . 5 | |
2 | suc0 4389 | . . . . . 6 | |
3 | 0elon 4370 | . . . . . . 7 | |
4 | 3 | onsuci 4493 | . . . . . 6 |
5 | 2, 4 | eqeltrri 2240 | . . . . 5 |
6 | sseq1 3165 | . . . . . . 7 | |
7 | sseq2 3166 | . . . . . . 7 | |
8 | 6, 7 | orbi12d 783 | . . . . . 6 |
9 | sseq2 3166 | . . . . . . 7 | |
10 | sseq1 3165 | . . . . . . 7 | |
11 | 9, 10 | orbi12d 783 | . . . . . 6 |
12 | 8, 11 | rspc2va 2844 | . . . . 5 |
13 | 1, 5, 12 | mpanl12 433 | . . . 4 |
14 | 5 | onirri 4520 | . . . . . 6 |
15 | simpl 108 | . . . . . . . 8 | |
16 | simpr 109 | . . . . . . . . 9 | |
17 | p0ex 4167 | . . . . . . . . . . 11 | |
18 | 17 | prid2 3683 | . . . . . . . . . 10 |
19 | biidd 171 | . . . . . . . . . . 11 | |
20 | 19 | elrab3 2883 | . . . . . . . . . 10 |
21 | 18, 20 | ax-mp 5 | . . . . . . . . 9 |
22 | 16, 21 | sylibr 133 | . . . . . . . 8 |
23 | 15, 22 | sseldd 3143 | . . . . . . 7 |
24 | 23 | ex 114 | . . . . . 6 |
25 | 14, 24 | mtoi 654 | . . . . 5 |
26 | snssg 3709 | . . . . . . 7 | |
27 | 3, 26 | ax-mp 5 | . . . . . 6 |
28 | 0ex 4109 | . . . . . . . 8 | |
29 | 28 | prid1 3682 | . . . . . . 7 |
30 | biidd 171 | . . . . . . . 8 | |
31 | 30 | elrab3 2883 | . . . . . . 7 |
32 | 29, 31 | ax-mp 5 | . . . . . 6 |
33 | 27, 32 | sylbb1 136 | . . . . 5 |
34 | 25, 33 | orim12i 749 | . . . 4 |
35 | 13, 34 | syl 14 | . . 3 |
36 | 35 | orcomd 719 | . 2 |
37 | df-dc 825 | . 2 DECID | |
38 | 36, 37 | sylibr 133 | 1 DECID |
Colors of variables: wff set class |
Syntax hints: wn 3 wi 4 wa 103 wb 104 wo 698 DECID wdc 824 wceq 1343 wcel 2136 wral 2444 crab 2448 wss 3116 c0 3409 csn 3576 cpr 3577 con0 4341 csuc 4343 |
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 604 ax-in2 605 ax-io 699 ax-5 1435 ax-7 1436 ax-gen 1437 ax-ie1 1481 ax-ie2 1482 ax-8 1492 ax-10 1493 ax-11 1494 ax-i12 1495 ax-bndl 1497 ax-4 1498 ax-17 1514 ax-i9 1518 ax-ial 1522 ax-i5r 1523 ax-13 2138 ax-14 2139 ax-ext 2147 ax-sep 4100 ax-nul 4108 ax-pow 4153 ax-pr 4187 ax-un 4411 ax-setind 4514 |
This theorem depends on definitions: df-bi 116 df-dc 825 df-3an 970 df-tru 1346 df-nf 1449 df-sb 1751 df-clab 2152 df-cleq 2158 df-clel 2161 df-nfc 2297 df-ne 2337 df-ral 2449 df-rex 2450 df-rab 2453 df-v 2728 df-dif 3118 df-un 3120 df-in 3122 df-ss 3129 df-nul 3410 df-pw 3561 df-sn 3582 df-pr 3583 df-uni 3790 df-tr 4081 df-iord 4344 df-on 4346 df-suc 4349 |
This theorem is referenced by: exmidontri2or 7199 |
Copyright terms: Public domain | W3C validator |