Step | Hyp | Ref
| Expression |
1 | | eleq2 2827 |
. . . . 5
โข (๐ต = โ
โ (๐ด โ ๐ต โ ๐ด โ โ
)) |
2 | | noel 4295 |
. . . . . 6
โข ยฌ
๐ด โ
โ
|
3 | 2 | pm2.21i 119 |
. . . . 5
โข (๐ด โ โ
โ suc ๐ด โ ๐ต) |
4 | 1, 3 | syl6bi 253 |
. . . 4
โข (๐ต = โ
โ (๐ด โ ๐ต โ suc ๐ด โ ๐ต)) |
5 | 4 | com12 32 |
. . 3
โข (๐ด โ ๐ต โ (๐ต = โ
โ suc ๐ด โ ๐ต)) |
6 | | simpl 484 |
. . . . 5
โข ((๐ด โ ๐ต โง (๐ต = (ฯ ยทo ๐ถ) โง ๐ถ โ (On โ 1o))) โ
๐ด โ ๐ต) |
7 | | eldifi 4091 |
. . . . . . . . 9
โข (๐ถ โ (On โ
1o) โ ๐ถ
โ On) |
8 | 7 | ad2antll 728 |
. . . . . . . 8
โข ((๐ด โ ๐ต โง (๐ต = (ฯ ยทo ๐ถ) โง ๐ถ โ (On โ 1o))) โ
๐ถ โ
On) |
9 | | omex 9586 |
. . . . . . . . . 10
โข ฯ
โ V |
10 | | limom 7823 |
. . . . . . . . . 10
โข Lim
ฯ |
11 | 9, 10 | pm3.2i 472 |
. . . . . . . . 9
โข (ฯ
โ V โง Lim ฯ) |
12 | 11 | a1i 11 |
. . . . . . . 8
โข ((๐ด โ ๐ต โง (๐ต = (ฯ ยทo ๐ถ) โง ๐ถ โ (On โ 1o))) โ
(ฯ โ V โง Lim ฯ)) |
13 | | ondif1 8452 |
. . . . . . . . . 10
โข (๐ถ โ (On โ
1o) โ (๐ถ
โ On โง โ
โ ๐ถ)) |
14 | 13 | simprbi 498 |
. . . . . . . . 9
โข (๐ถ โ (On โ
1o) โ โ
โ ๐ถ) |
15 | 14 | ad2antll 728 |
. . . . . . . 8
โข ((๐ด โ ๐ต โง (๐ต = (ฯ ยทo ๐ถ) โง ๐ถ โ (On โ 1o))) โ
โ
โ ๐ถ) |
16 | | omlimcl2 41605 |
. . . . . . . 8
โข (((๐ถ โ On โง (ฯ โ
V โง Lim ฯ)) โง โ
โ ๐ถ) โ Lim (ฯ ยทo
๐ถ)) |
17 | 8, 12, 15, 16 | syl21anc 837 |
. . . . . . 7
โข ((๐ด โ ๐ต โง (๐ต = (ฯ ยทo ๐ถ) โง ๐ถ โ (On โ 1o))) โ
Lim (ฯ ยทo ๐ถ)) |
18 | | limeq 6334 |
. . . . . . . 8
โข (๐ต = (ฯ ยทo
๐ถ) โ (Lim ๐ต โ Lim (ฯ
ยทo ๐ถ))) |
19 | 18 | ad2antrl 727 |
. . . . . . 7
โข ((๐ด โ ๐ต โง (๐ต = (ฯ ยทo ๐ถ) โง ๐ถ โ (On โ 1o))) โ
(Lim ๐ต โ Lim (ฯ
ยทo ๐ถ))) |
20 | 17, 19 | mpbird 257 |
. . . . . 6
โข ((๐ด โ ๐ต โง (๐ต = (ฯ ยทo ๐ถ) โง ๐ถ โ (On โ 1o))) โ
Lim ๐ต) |
21 | | limsuc 7790 |
. . . . . 6
โข (Lim
๐ต โ (๐ด โ ๐ต โ suc ๐ด โ ๐ต)) |
22 | 20, 21 | syl 17 |
. . . . 5
โข ((๐ด โ ๐ต โง (๐ต = (ฯ ยทo ๐ถ) โง ๐ถ โ (On โ 1o))) โ
(๐ด โ ๐ต โ suc ๐ด โ ๐ต)) |
23 | 6, 22 | mpbid 231 |
. . . 4
โข ((๐ด โ ๐ต โง (๐ต = (ฯ ยทo ๐ถ) โง ๐ถ โ (On โ 1o))) โ
suc ๐ด โ ๐ต) |
24 | 23 | ex 414 |
. . 3
โข (๐ด โ ๐ต โ ((๐ต = (ฯ ยทo ๐ถ) โง ๐ถ โ (On โ 1o)) โ
suc ๐ด โ ๐ต)) |
25 | 5, 24 | jaod 858 |
. 2
โข (๐ด โ ๐ต โ ((๐ต = โ
โจ (๐ต = (ฯ ยทo ๐ถ) โง ๐ถ โ (On โ 1o))) โ
suc ๐ด โ ๐ต)) |
26 | 25 | imp 408 |
1
โข ((๐ด โ ๐ต โง (๐ต = โ
โจ (๐ต = (ฯ ยทo ๐ถ) โง ๐ถ โ (On โ 1o)))) โ
suc ๐ด โ ๐ต) |