![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > limom | Unicode version |
Description: Omega is a limit ordinal. Theorem 2.8 of [BellMachover] p. 473. (Contributed by NM, 26-Mar-1995.) (Proof rewritten by Jim Kingdon, 5-Jan-2019.) |
Ref | Expression |
---|---|
limom |
![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ordom 4606 |
. 2
![]() ![]() ![]() | |
2 | peano1 4593 |
. 2
![]() ![]() ![]() ![]() | |
3 | vex 2740 |
. . . . . . . . 9
![]() ![]() ![]() ![]() | |
4 | 3 | sucex 4498 |
. . . . . . . 8
![]() ![]() ![]() ![]() ![]() |
5 | 4 | isseti 2745 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | peano2 4594 |
. . . . . . . . 9
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
7 | 3 | sucid 4417 |
. . . . . . . . 9
![]() ![]() ![]() ![]() ![]() |
8 | 6, 7 | jctil 312 |
. . . . . . . 8
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
9 | eleq2 2241 |
. . . . . . . . 9
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
10 | eleq1 2240 |
. . . . . . . . 9
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
11 | 9, 10 | anbi12d 473 |
. . . . . . . 8
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
12 | 8, 11 | imbitrrid 156 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
13 | 5, 12 | eximii 1602 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
14 | 13 | 19.37aiv 1675 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
15 | eluni 3812 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
16 | 14, 15 | sylibr 134 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
17 | 16 | ssriv 3159 |
. . 3
![]() ![]() ![]() ![]() ![]() |
18 | orduniss 4425 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
19 | 1, 18 | ax-mp 5 |
. . 3
![]() ![]() ![]() ![]() ![]() |
20 | 17, 19 | eqssi 3171 |
. 2
![]() ![]() ![]() ![]() ![]() |
21 | dflim2 4370 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
22 | 1, 2, 20, 21 | mpbir3an 1179 |
1
![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 614 ax-in2 615 ax-io 709 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-10 1505 ax-11 1506 ax-i12 1507 ax-bndl 1509 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-13 2150 ax-14 2151 ax-ext 2159 ax-sep 4121 ax-nul 4129 ax-pow 4174 ax-pr 4209 ax-un 4433 ax-iinf 4587 |
This theorem depends on definitions: df-bi 117 df-3an 980 df-tru 1356 df-nf 1461 df-sb 1763 df-clab 2164 df-cleq 2170 df-clel 2173 df-nfc 2308 df-ral 2460 df-rex 2461 df-v 2739 df-dif 3131 df-un 3133 df-in 3135 df-ss 3142 df-nul 3423 df-pw 3577 df-sn 3598 df-pr 3599 df-uni 3810 df-int 3845 df-tr 4102 df-iord 4366 df-ilim 4369 df-suc 4371 df-iom 4590 |
This theorem is referenced by: freccllem 6402 frecfcllem 6404 frecsuclem 6406 |
Copyright terms: Public domain | W3C validator |