Step | Hyp | Ref
| Expression |
1 | | omelon 9661 |
. . . . . 6
โข ฯ
โ On |
2 | 1 | a1i 11 |
. . . . 5
โข (๐ โ ฯ โ
On) |
3 | | naddwordnex.d |
. . . . . . 7
โข (๐ โ ๐ท โ On) |
4 | | naddwordnex.c |
. . . . . . 7
โข (๐ โ ๐ถ โ ๐ท) |
5 | | onelon 6388 |
. . . . . . 7
โข ((๐ท โ On โง ๐ถ โ ๐ท) โ ๐ถ โ On) |
6 | 3, 4, 5 | syl2anc 583 |
. . . . . 6
โข (๐ โ ๐ถ โ On) |
7 | | omcl 8550 |
. . . . . 6
โข ((ฯ
โ On โง ๐ถ โ
On) โ (ฯ ยทo ๐ถ) โ On) |
8 | 2, 6, 7 | syl2anc 583 |
. . . . 5
โข (๐ โ (ฯ
ยทo ๐ถ)
โ On) |
9 | 2, 8 | jca 511 |
. . . 4
โข (๐ โ (ฯ โ On โง
(ฯ ยทo ๐ถ) โ On)) |
10 | | naddwordnex.m |
. . . 4
โข (๐ โ ๐ โ ฯ) |
11 | | oaordi 8560 |
. . . 4
โข ((ฯ
โ On โง (ฯ ยทo ๐ถ) โ On) โ (๐ โ ฯ โ ((ฯ
ยทo ๐ถ)
+o ๐) โ
((ฯ ยทo ๐ถ) +o ฯ))) |
12 | 9, 10, 11 | sylc 65 |
. . 3
โข (๐ โ ((ฯ
ยทo ๐ถ)
+o ๐) โ
((ฯ ยทo ๐ถ) +o ฯ)) |
13 | | naddwordnex.a |
. . 3
โข (๐ โ ๐ด = ((ฯ ยทo ๐ถ) +o ๐)) |
14 | | omsuc 8540 |
. . . 4
โข ((ฯ
โ On โง ๐ถ โ
On) โ (ฯ ยทo suc ๐ถ) = ((ฯ ยทo ๐ถ) +o
ฯ)) |
15 | 2, 6, 14 | syl2anc 583 |
. . 3
โข (๐ โ (ฯ
ยทo suc ๐ถ)
= ((ฯ ยทo ๐ถ) +o ฯ)) |
16 | 12, 13, 15 | 3eltr4d 2843 |
. 2
โข (๐ โ ๐ด โ (ฯ ยทo suc
๐ถ)) |
17 | | onsuc 7808 |
. . . . . . 7
โข (๐ถ โ On โ suc ๐ถ โ On) |
18 | 6, 17 | syl 17 |
. . . . . 6
โข (๐ โ suc ๐ถ โ On) |
19 | 18, 3, 2 | 3jca 1126 |
. . . . 5
โข (๐ โ (suc ๐ถ โ On โง ๐ท โ On โง ฯ โ
On)) |
20 | | onsucss 42618 |
. . . . . 6
โข (๐ท โ On โ (๐ถ โ ๐ท โ suc ๐ถ โ ๐ท)) |
21 | 3, 4, 20 | sylc 65 |
. . . . 5
โข (๐ โ suc ๐ถ โ ๐ท) |
22 | | omwordi 8585 |
. . . . 5
โข ((suc
๐ถ โ On โง ๐ท โ On โง ฯ โ
On) โ (suc ๐ถ โ
๐ท โ (ฯ
ยทo suc ๐ถ)
โ (ฯ ยทo ๐ท))) |
23 | 19, 21, 22 | sylc 65 |
. . . 4
โข (๐ โ (ฯ
ยทo suc ๐ถ)
โ (ฯ ยทo ๐ท)) |
24 | | omcl 8550 |
. . . . . 6
โข ((ฯ
โ On โง ๐ท โ
On) โ (ฯ ยทo ๐ท) โ On) |
25 | 2, 3, 24 | syl2anc 583 |
. . . . 5
โข (๐ โ (ฯ
ยทo ๐ท)
โ On) |
26 | | naddwordnex.n |
. . . . . . . 8
โข (๐ โ ๐ โ ๐) |
27 | 26, 10 | jca 511 |
. . . . . . 7
โข (๐ โ (๐ โ ๐ โง ๐ โ ฯ)) |
28 | | ontr1 6409 |
. . . . . . 7
โข (ฯ
โ On โ ((๐ โ
๐ โง ๐ โ ฯ) โ ๐ โ ฯ)) |
29 | 2, 27, 28 | sylc 65 |
. . . . . 6
โข (๐ โ ๐ โ ฯ) |
30 | | nnon 7870 |
. . . . . 6
โข (๐ โ ฯ โ ๐ โ On) |
31 | 29, 30 | syl 17 |
. . . . 5
โข (๐ โ ๐ โ On) |
32 | | oaword1 8566 |
. . . . 5
โข
(((ฯ ยทo ๐ท) โ On โง ๐ โ On) โ (ฯ
ยทo ๐ท)
โ ((ฯ ยทo ๐ท) +o ๐)) |
33 | 25, 31, 32 | syl2anc 583 |
. . . 4
โข (๐ โ (ฯ
ยทo ๐ท)
โ ((ฯ ยทo ๐ท) +o ๐)) |
34 | 23, 33 | sstrd 3988 |
. . 3
โข (๐ โ (ฯ
ยทo suc ๐ถ)
โ ((ฯ ยทo ๐ท) +o ๐)) |
35 | | naddwordnex.b |
. . 3
โข (๐ โ ๐ต = ((ฯ ยทo ๐ท) +o ๐)) |
36 | 34, 35 | sseqtrrd 4019 |
. 2
โข (๐ โ (ฯ
ยทo suc ๐ถ)
โ ๐ต) |
37 | 16, 36 | jca 511 |
1
โข (๐ โ (๐ด โ (ฯ ยทo suc
๐ถ) โง (ฯ
ยทo suc ๐ถ)
โ ๐ต)) |