Step | Hyp | Ref
| Expression |
1 | | onnbtwn 6415 |
. . 3
โข (๐ด โ On โ ยฌ (๐ด โ ๐ต โง ๐ต โ suc ๐ด)) |
2 | 1 | 3ad2ant1 1134 |
. 2
โข ((๐ด โ On โง ๐ต โ On โง ๐ถ = (2o
ยทo ๐ด))
โ ยฌ (๐ด โ
๐ต โง ๐ต โ suc ๐ด)) |
3 | | suceq 6387 |
. . . . 5
โข (๐ถ = (2o
ยทo ๐ด)
โ suc ๐ถ = suc
(2o ยทo ๐ด)) |
4 | 3 | eqeq1d 2735 |
. . . 4
โข (๐ถ = (2o
ยทo ๐ด)
โ (suc ๐ถ =
(2o ยทo ๐ต) โ suc (2o
ยทo ๐ด) =
(2o ยทo ๐ต))) |
5 | 4 | 3ad2ant3 1136 |
. . 3
โข ((๐ด โ On โง ๐ต โ On โง ๐ถ = (2o
ยทo ๐ด))
โ (suc ๐ถ =
(2o ยทo ๐ต) โ suc (2o
ยทo ๐ด) =
(2o ยทo ๐ต))) |
6 | | ovex 7394 |
. . . . . . . 8
โข
(2o ยทo ๐ด) โ V |
7 | 6 | sucid 6403 |
. . . . . . 7
โข
(2o ยทo ๐ด) โ suc (2o
ยทo ๐ด) |
8 | | eleq2 2823 |
. . . . . . 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 8430 |
. . . . . . . 8
โข
2o โ On |
11 | | omord 8519 |
. . . . . . . 8
โข ((๐ด โ On โง ๐ต โ On โง 2o
โ On) โ ((๐ด
โ ๐ต โง โ
โ 2o) โ (2o ยทo ๐ด) โ (2o
ยทo ๐ต))) |
12 | 10, 11 | mp3an3 1451 |
. . . . . . 7
โข ((๐ด โ On โง ๐ต โ On) โ ((๐ด โ ๐ต โง โ
โ 2o) โ
(2o ยทo ๐ด) โ (2o ยทo
๐ต))) |
13 | | simpl 484 |
. . . . . . 7
โข ((๐ด โ ๐ต โง โ
โ 2o) โ
๐ด โ ๐ต) |
14 | 12, 13 | syl6bir 254 |
. . . . . 6
โข ((๐ด โ On โง ๐ต โ On) โ
((2o ยทo ๐ด) โ (2o ยทo
๐ต) โ ๐ด โ ๐ต)) |
15 | 9, 14 | syl5 34 |
. . . . 5
โข ((๐ด โ On โง ๐ต โ On) โ (suc
(2o ยทo ๐ด) = (2o ยทo
๐ต) โ ๐ด โ ๐ต)) |
16 | | simpr 486 |
. . . . . . . . 9
โข (((๐ด โ On โง ๐ต โ On) โง suc
(2o ยทo ๐ด) = (2o ยทo
๐ต)) โ suc
(2o ยทo ๐ด) = (2o ยทo
๐ต)) |
17 | | omcl 8486 |
. . . . . . . . . . . . 13
โข
((2o โ On โง ๐ด โ On) โ (2o
ยทo ๐ด)
โ On) |
18 | 10, 17 | mpan 689 |
. . . . . . . . . . . 12
โข (๐ด โ On โ (2o
ยทo ๐ด)
โ On) |
19 | | oa1suc 8481 |
. . . . . . . . . . . 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 8426 |
. . . . . . . . . . . . . . 15
โข
1o โ V |
22 | 21 | sucid 6403 |
. . . . . . . . . . . . . 14
โข
1o โ suc 1o |
23 | | df-2o 8417 |
. . . . . . . . . . . . . 14
โข
2o = suc 1o |
24 | 22, 23 | eleqtrri 2833 |
. . . . . . . . . . . . 13
โข
1o โ 2o |
25 | | 1on 8428 |
. . . . . . . . . . . . . 14
โข
1o โ On |
26 | | oaord 8498 |
. . . . . . . . . . . . . 14
โข
((1o โ On โง 2o โ On โง
(2o ยทo ๐ด) โ On) โ (1o โ
2o โ ((2o ยทo ๐ด) +o 1o) โ
((2o ยทo ๐ด) +o
2o))) |
27 | 25, 10, 18, 26 | mp3an12i 1466 |
. . . . . . . . . . . . 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 8476 |
. . . . . . . . . . . . 13
โข
((2o โ On โง ๐ด โ On) โ (2o
ยทo suc ๐ด)
= ((2o ยทo ๐ด) +o
2o)) |
30 | 10, 29 | mpan 689 |
. . . . . . . . . . . 12
โข (๐ด โ On โ (2o
ยทo suc ๐ด)
= ((2o ยทo ๐ด) +o
2o)) |
31 | 28, 30 | eleqtrrd 2837 |
. . . . . . . . . . 11
โข (๐ด โ On โ
((2o ยทo ๐ด) +o 1o) โ
(2o ยทo suc ๐ด)) |
32 | 20, 31 | eqeltrrd 2835 |
. . . . . . . . . 10
โข (๐ด โ On โ suc
(2o ยทo ๐ด) โ (2o ยทo
suc ๐ด)) |
33 | 32 | ad2antrr 725 |
. . . . . . . . 9
โข (((๐ด โ On โง ๐ต โ On) โง suc
(2o ยทo ๐ด) = (2o ยทo
๐ต)) โ suc
(2o ยทo ๐ด) โ (2o ยทo
suc ๐ด)) |
34 | 16, 33 | eqeltrrd 2835 |
. . . . . . . 8
โข (((๐ด โ On โง ๐ต โ On) โง suc
(2o ยทo ๐ด) = (2o ยทo
๐ต)) โ (2o
ยทo ๐ต)
โ (2o ยทo suc ๐ด)) |
35 | | onsuc 7750 |
. . . . . . . . . . 11
โข (๐ด โ On โ suc ๐ด โ On) |
36 | | omord 8519 |
. . . . . . . . . . . 12
โข ((๐ต โ On โง suc ๐ด โ On โง 2o
โ On) โ ((๐ต
โ suc ๐ด โง โ
โ 2o) โ (2o ยทo ๐ต) โ (2o
ยทo suc ๐ด))) |
37 | 10, 36 | mp3an3 1451 |
. . . . . . . . . . 11
โข ((๐ต โ On โง suc ๐ด โ On) โ ((๐ต โ suc ๐ด โง โ
โ 2o) โ
(2o ยทo ๐ต) โ (2o ยทo
suc ๐ด))) |
38 | 35, 37 | sylan2 594 |
. . . . . . . . . 10
โข ((๐ต โ On โง ๐ด โ On) โ ((๐ต โ suc ๐ด โง โ
โ 2o) โ
(2o ยทo ๐ต) โ (2o ยทo
suc ๐ด))) |
39 | 38 | ancoms 460 |
. . . . . . . . 9
โข ((๐ด โ On โง ๐ต โ On) โ ((๐ต โ suc ๐ด โง โ
โ 2o) โ
(2o ยทo ๐ต) โ (2o ยทo
suc ๐ด))) |
40 | 39 | adantr 482 |
. . . . . . . 8
โข (((๐ด โ On โง ๐ต โ On) โง suc
(2o ยทo ๐ด) = (2o ยทo
๐ต)) โ ((๐ต โ suc ๐ด โง โ
โ 2o) โ
(2o ยทo ๐ต) โ (2o ยทo
suc ๐ด))) |
41 | 34, 40 | mpbird 257 |
. . . . . . 7
โข (((๐ด โ On โง ๐ต โ On) โง suc
(2o ยทo ๐ด) = (2o ยทo
๐ต)) โ (๐ต โ suc ๐ด โง โ
โ
2o)) |
42 | 41 | simpld 496 |
. . . . . 6
โข (((๐ด โ On โง ๐ต โ On) โง suc
(2o ยทo ๐ด) = (2o ยทo
๐ต)) โ ๐ต โ suc ๐ด) |
43 | 42 | ex 414 |
. . . . 5
โข ((๐ด โ On โง ๐ต โ On) โ (suc
(2o ยทo ๐ด) = (2o ยทo
๐ต) โ ๐ต โ suc ๐ด)) |
44 | 15, 43 | jcad 514 |
. . . 4
โข ((๐ด โ On โง ๐ต โ On) โ (suc
(2o ยทo ๐ด) = (2o ยทo
๐ต) โ (๐ด โ ๐ต โง ๐ต โ suc ๐ด))) |
45 | 44 | 3adant3 1133 |
. . 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 ๐ต)) |