![]() |
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 4607 |
. 2
![]() ![]() ![]() | |
2 | peano1 4594 |
. 2
![]() ![]() ![]() ![]() | |
3 | vex 2741 |
. . . . . . . . 9
![]() ![]() ![]() ![]() | |
4 | 3 | sucex 4499 |
. . . . . . . 8
![]() ![]() ![]() ![]() ![]() |
5 | 4 | isseti 2746 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | peano2 4595 |
. . . . . . . . 9
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
7 | 3 | sucid 4418 |
. . . . . . . . 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 3813 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
16 | 14, 15 | sylibr 134 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
17 | 16 | ssriv 3160 |
. . 3
![]() ![]() ![]() ![]() ![]() |
18 | orduniss 4426 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
19 | 1, 18 | ax-mp 5 |
. . 3
![]() ![]() ![]() ![]() ![]() |
20 | 17, 19 | eqssi 3172 |
. 2
![]() ![]() ![]() ![]() ![]() |
21 | dflim2 4371 |
. 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 4122 ax-nul 4130 ax-pow 4175 ax-pr 4210 ax-un 4434 ax-iinf 4588 |
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 2740 df-dif 3132 df-un 3134 df-in 3136 df-ss 3143 df-nul 3424 df-pw 3578 df-sn 3599 df-pr 3600 df-uni 3811 df-int 3846 df-tr 4103 df-iord 4367 df-ilim 4370 df-suc 4372 df-iom 4591 |
This theorem is referenced by: freccllem 6403 frecfcllem 6405 frecsuclem 6407 |
Copyright terms: Public domain | W3C validator |