Step | Hyp | Ref
| Expression |
1 | | onnbtwn 6458 |
. . 3
โข (๐ด โ On โ ยฌ (๐ด โ ๐ต โง ๐ต โ suc ๐ด)) |
2 | 1 | 3ad2ant1 1133 |
. 2
โข ((๐ด โ On โง ๐ต โ On โง ๐ถ = (2o
ยทo ๐ด))
โ ยฌ (๐ด โ
๐ต โง ๐ต โ suc ๐ด)) |
3 | | suceq 6430 |
. . . . 5
โข (๐ถ = (2o
ยทo ๐ด)
โ suc ๐ถ = suc
(2o ยทo ๐ด)) |
4 | 3 | eqeq1d 2734 |
. . . 4
โข (๐ถ = (2o
ยทo ๐ด)
โ (suc ๐ถ =
(2o ยทo ๐ต) โ suc (2o
ยทo ๐ด) =
(2o ยทo ๐ต))) |
5 | 4 | 3ad2ant3 1135 |
. . 3
โข ((๐ด โ On โง ๐ต โ On โง ๐ถ = (2o
ยทo ๐ด))
โ (suc ๐ถ =
(2o ยทo ๐ต) โ suc (2o
ยทo ๐ด) =
(2o ยทo ๐ต))) |
6 | | ovex 7441 |
. . . . . . . 8
โข
(2o ยทo ๐ด) โ V |
7 | 6 | sucid 6446 |
. . . . . . 7
โข
(2o ยทo ๐ด) โ suc (2o
ยทo ๐ด) |
8 | | eleq2 2822 |
. . . . . . 7
โข (suc
(2o ยทo ๐ด) = (2o ยทo
๐ต) โ ((2o
ยทo ๐ด)
โ suc (2o ยทo ๐ด) โ (2o ยทo
๐ด) โ (2o
ยทo ๐ต))) |
9 | 7, 8 | mpbii 232 |
. . . . . 6
โข (suc
(2o ยทo ๐ด) = (2o ยทo
๐ต) โ (2o
ยทo ๐ด)
โ (2o ยทo ๐ต)) |
10 | | 2on 8479 |
. . . . . . . 8
โข
2o โ On |
11 | | omord 8567 |
. . . . . . . 8
โข ((๐ด โ On โง ๐ต โ On โง 2o
โ On) โ ((๐ด
โ ๐ต โง โ
โ 2o) โ (2o ยทo ๐ด) โ (2o
ยทo ๐ต))) |
12 | 10, 11 | mp3an3 1450 |
. . . . . . 7
โข ((๐ด โ On โง ๐ต โ On) โ ((๐ด โ ๐ต โง โ
โ 2o) โ
(2o ยทo ๐ด) โ (2o ยทo
๐ต))) |
13 | | simpl 483 |
. . . . . . 7
โข ((๐ด โ ๐ต โง โ
โ 2o) โ
๐ด โ ๐ต) |
14 | 12, 13 | syl6bir 253 |
. . . . . 6
โข ((๐ด โ On โง ๐ต โ On) โ
((2o ยทo ๐ด) โ (2o ยทo
๐ต) โ ๐ด โ ๐ต)) |
15 | 9, 14 | syl5 34 |
. . . . 5
โข ((๐ด โ On โง ๐ต โ On) โ (suc
(2o ยทo ๐ด) = (2o ยทo
๐ต) โ ๐ด โ ๐ต)) |
16 | | simpr 485 |
. . . . . . . . 9
โข (((๐ด โ On โง ๐ต โ On) โง suc
(2o ยทo ๐ด) = (2o ยทo
๐ต)) โ suc
(2o ยทo ๐ด) = (2o ยทo
๐ต)) |
17 | | omcl 8535 |
. . . . . . . . . . . . 13
โข
((2o โ On โง ๐ด โ On) โ (2o
ยทo ๐ด)
โ On) |
18 | 10, 17 | mpan 688 |
. . . . . . . . . . . 12
โข (๐ด โ On โ (2o
ยทo ๐ด)
โ On) |
19 | | oa1suc 8530 |
. . . . . . . . . . . 12
โข
((2o ยทo ๐ด) โ On โ ((2o
ยทo ๐ด)
+o 1o) = suc (2o ยทo ๐ด)) |
20 | 18, 19 | syl 17 |
. . . . . . . . . . 11
โข (๐ด โ On โ
((2o ยทo ๐ด) +o 1o) = suc
(2o ยทo ๐ด)) |
21 | | 1oex 8475 |
. . . . . . . . . . . . . . 15
โข
1o โ V |
22 | 21 | sucid 6446 |
. . . . . . . . . . . . . 14
โข
1o โ suc 1o |
23 | | df-2o 8466 |
. . . . . . . . . . . . . 14
โข
2o = suc 1o |
24 | 22, 23 | eleqtrri 2832 |
. . . . . . . . . . . . 13
โข
1o โ 2o |
25 | | 1on 8477 |
. . . . . . . . . . . . . 14
โข
1o โ On |
26 | | oaord 8546 |
. . . . . . . . . . . . . 14
โข
((1o โ On โง 2o โ On โง
(2o ยทo ๐ด) โ On) โ (1o โ
2o โ ((2o ยทo ๐ด) +o 1o) โ
((2o ยทo ๐ด) +o
2o))) |
27 | 25, 10, 18, 26 | mp3an12i 1465 |
. . . . . . . . . . . . 13
โข (๐ด โ On โ (1o
โ 2o โ ((2o ยทo ๐ด) +o 1o)
โ ((2o ยทo ๐ด) +o
2o))) |
28 | 24, 27 | mpbii 232 |
. . . . . . . . . . . 12
โข (๐ด โ On โ
((2o ยทo ๐ด) +o 1o) โ
((2o ยทo ๐ด) +o
2o)) |
29 | | omsuc 8525 |
. . . . . . . . . . . . 13
โข
((2o โ On โง ๐ด โ On) โ (2o
ยทo suc ๐ด)
= ((2o ยทo ๐ด) +o
2o)) |
30 | 10, 29 | mpan 688 |
. . . . . . . . . . . 12
โข (๐ด โ On โ (2o
ยทo suc ๐ด)
= ((2o ยทo ๐ด) +o
2o)) |
31 | 28, 30 | eleqtrrd 2836 |
. . . . . . . . . . 11
โข (๐ด โ On โ
((2o ยทo ๐ด) +o 1o) โ
(2o ยทo suc ๐ด)) |
32 | 20, 31 | eqeltrrd 2834 |
. . . . . . . . . 10
โข (๐ด โ On โ suc
(2o ยทo ๐ด) โ (2o ยทo
suc ๐ด)) |
33 | 32 | ad2antrr 724 |
. . . . . . . . 9
โข (((๐ด โ On โง ๐ต โ On) โง suc
(2o ยทo ๐ด) = (2o ยทo
๐ต)) โ suc
(2o ยทo ๐ด) โ (2o ยทo
suc ๐ด)) |
34 | 16, 33 | eqeltrrd 2834 |
. . . . . . . 8
โข (((๐ด โ On โง ๐ต โ On) โง suc
(2o ยทo ๐ด) = (2o ยทo
๐ต)) โ (2o
ยทo ๐ต)
โ (2o ยทo suc ๐ด)) |
35 | | onsuc 7798 |
. . . . . . . . . . 11
โข (๐ด โ On โ suc ๐ด โ On) |
36 | | omord 8567 |
. . . . . . . . . . . 12
โข ((๐ต โ On โง suc ๐ด โ On โง 2o
โ On) โ ((๐ต
โ suc ๐ด โง โ
โ 2o) โ (2o ยทo ๐ต) โ (2o
ยทo suc ๐ด))) |
37 | 10, 36 | mp3an3 1450 |
. . . . . . . . . . 11
โข ((๐ต โ On โง suc ๐ด โ On) โ ((๐ต โ suc ๐ด โง โ
โ 2o) โ
(2o ยทo ๐ต) โ (2o ยทo
suc ๐ด))) |
38 | 35, 37 | sylan2 593 |
. . . . . . . . . 10
โข ((๐ต โ On โง ๐ด โ On) โ ((๐ต โ suc ๐ด โง โ
โ 2o) โ
(2o ยทo ๐ต) โ (2o ยทo
suc ๐ด))) |
39 | 38 | ancoms 459 |
. . . . . . . . 9
โข ((๐ด โ On โง ๐ต โ On) โ ((๐ต โ suc ๐ด โง โ
โ 2o) โ
(2o ยทo ๐ต) โ (2o ยทo
suc ๐ด))) |
40 | 39 | adantr 481 |
. . . . . . . 8
โข (((๐ด โ On โง ๐ต โ On) โง suc
(2o ยทo ๐ด) = (2o ยทo
๐ต)) โ ((๐ต โ suc ๐ด โง โ
โ 2o) โ
(2o ยทo ๐ต) โ (2o ยทo
suc ๐ด))) |
41 | 34, 40 | mpbird 256 |
. . . . . . 7
โข (((๐ด โ On โง ๐ต โ On) โง suc
(2o ยทo ๐ด) = (2o ยทo
๐ต)) โ (๐ต โ suc ๐ด โง โ
โ
2o)) |
42 | 41 | simpld 495 |
. . . . . 6
โข (((๐ด โ On โง ๐ต โ On) โง suc
(2o ยทo ๐ด) = (2o ยทo
๐ต)) โ ๐ต โ suc ๐ด) |
43 | 42 | ex 413 |
. . . . 5
โข ((๐ด โ On โง ๐ต โ On) โ (suc
(2o ยทo ๐ด) = (2o ยทo
๐ต) โ ๐ต โ suc ๐ด)) |
44 | 15, 43 | jcad 513 |
. . . 4
โข ((๐ด โ On โง ๐ต โ On) โ (suc
(2o ยทo ๐ด) = (2o ยทo
๐ต) โ (๐ด โ ๐ต โง ๐ต โ suc ๐ด))) |
45 | 44 | 3adant3 1132 |
. . 3
โข ((๐ด โ On โง ๐ต โ On โง ๐ถ = (2o
ยทo ๐ด))
โ (suc (2o ยทo ๐ด) = (2o ยทo
๐ต) โ (๐ด โ ๐ต โง ๐ต โ suc ๐ด))) |
46 | 5, 45 | sylbid 239 |
. 2
โข ((๐ด โ On โง ๐ต โ On โง ๐ถ = (2o
ยทo ๐ด))
โ (suc ๐ถ =
(2o ยทo ๐ต) โ (๐ด โ ๐ต โง ๐ต โ suc ๐ด))) |
47 | 2, 46 | mtod 197 |
1
โข ((๐ด โ On โง ๐ต โ On โง ๐ถ = (2o
ยทo ๐ด))
โ ยฌ suc ๐ถ =
(2o ยทo ๐ต)) |