Step | Hyp | Ref
| Expression |
1 | | eldifi 4091 |
. . . . . . . . . . . . . . . . . 18
โข (๐ด โ (On โ
2o) โ ๐ด
โ On) |
2 | 1 | adantr 482 |
. . . . . . . . . . . . . . . . 17
โข ((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โ ๐ด โ On) |
3 | 2 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ โ On โง ๐ท โ (๐ด โ 1o))) โ ๐ด โ On) |
4 | | simprl 770 |
. . . . . . . . . . . . . . . 16
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ โ On โง ๐ท โ (๐ด โ 1o))) โ ๐ถ โ On) |
5 | | oecl 8488 |
. . . . . . . . . . . . . . . 16
โข ((๐ด โ On โง ๐ถ โ On) โ (๐ด โo ๐ถ) โ On) |
6 | 3, 4, 5 | syl2anc 585 |
. . . . . . . . . . . . . . 15
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ โ On โง ๐ท โ (๐ด โ 1o))) โ (๐ด โo ๐ถ) โ On) |
7 | | om1 8494 |
. . . . . . . . . . . . . . 15
โข ((๐ด โo ๐ถ) โ On โ ((๐ด โo ๐ถ) ยทo
1o) = (๐ด
โo ๐ถ)) |
8 | 6, 7 | syl 17 |
. . . . . . . . . . . . . 14
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ โ On โง ๐ท โ (๐ด โ 1o))) โ ((๐ด โo ๐ถ) ยทo
1o) = (๐ด
โo ๐ถ)) |
9 | | df1o2 8424 |
. . . . . . . . . . . . . . . 16
โข
1o = {โ
} |
10 | | dif1o 8451 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ท โ (๐ด โ 1o) โ (๐ท โ ๐ด โง ๐ท โ โ
)) |
11 | 10 | simprbi 498 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ท โ (๐ด โ 1o) โ ๐ท โ โ
) |
12 | 11 | ad2antll 728 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ โ On โง ๐ท โ (๐ด โ 1o))) โ ๐ท โ โ
) |
13 | | eldifi 4091 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ท โ (๐ด โ 1o) โ ๐ท โ ๐ด) |
14 | 13 | ad2antll 728 |
. . . . . . . . . . . . . . . . . . . 20
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ โ On โง ๐ท โ (๐ด โ 1o))) โ ๐ท โ ๐ด) |
15 | | onelon 6347 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ด โ On โง ๐ท โ ๐ด) โ ๐ท โ On) |
16 | 3, 14, 15 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . 19
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ โ On โง ๐ท โ (๐ด โ 1o))) โ ๐ท โ On) |
17 | | on0eln0 6378 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ท โ On โ (โ
โ ๐ท โ ๐ท โ โ
)) |
18 | 16, 17 | syl 17 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ โ On โง ๐ท โ (๐ด โ 1o))) โ (โ
โ ๐ท โ ๐ท โ โ
)) |
19 | 12, 18 | mpbird 257 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ โ On โง ๐ท โ (๐ด โ 1o))) โ โ
โ ๐ท) |
20 | 19 | snssd 4774 |
. . . . . . . . . . . . . . . 16
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ โ On โง ๐ท โ (๐ด โ 1o))) โ {โ
}
โ ๐ท) |
21 | 9, 20 | eqsstrid 3997 |
. . . . . . . . . . . . . . 15
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ โ On โง ๐ท โ (๐ด โ 1o))) โ
1o โ ๐ท) |
22 | | 1on 8429 |
. . . . . . . . . . . . . . . . 17
โข
1o โ On |
23 | 22 | a1i 11 |
. . . . . . . . . . . . . . . 16
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ โ On โง ๐ท โ (๐ด โ 1o))) โ
1o โ On) |
24 | | omwordi 8523 |
. . . . . . . . . . . . . . . 16
โข
((1o โ On โง ๐ท โ On โง (๐ด โo ๐ถ) โ On) โ (1o โ
๐ท โ ((๐ด โo ๐ถ) ยทo
1o) โ ((๐ด
โo ๐ถ)
ยทo ๐ท))) |
25 | 23, 16, 6, 24 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ โ On โง ๐ท โ (๐ด โ 1o))) โ
(1o โ ๐ท
โ ((๐ด
โo ๐ถ)
ยทo 1o) โ ((๐ด โo ๐ถ) ยทo ๐ท))) |
26 | 21, 25 | mpd 15 |
. . . . . . . . . . . . . 14
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ โ On โง ๐ท โ (๐ด โ 1o))) โ ((๐ด โo ๐ถ) ยทo
1o) โ ((๐ด
โo ๐ถ)
ยทo ๐ท)) |
27 | 8, 26 | eqsstrrd 3988 |
. . . . . . . . . . . . 13
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ โ On โง ๐ท โ (๐ด โ 1o))) โ (๐ด โo ๐ถ) โ ((๐ด โo ๐ถ) ยทo ๐ท)) |
28 | | omcl 8487 |
. . . . . . . . . . . . . . . 16
โข (((๐ด โo ๐ถ) โ On โง ๐ท โ On) โ ((๐ด โo ๐ถ) ยทo ๐ท) โ On) |
29 | 6, 16, 28 | syl2anc 585 |
. . . . . . . . . . . . . . 15
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ โ On โง ๐ท โ (๐ด โ 1o))) โ ((๐ด โo ๐ถ) ยทo ๐ท) โ On) |
30 | | simplrl 776 |
. . . . . . . . . . . . . . . 16
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ โ On โง ๐ท โ (๐ด โ 1o))) โ ๐ธ โ (๐ด โo ๐ถ)) |
31 | | onelon 6347 |
. . . . . . . . . . . . . . . 16
โข (((๐ด โo ๐ถ) โ On โง ๐ธ โ (๐ด โo ๐ถ)) โ ๐ธ โ On) |
32 | 6, 30, 31 | syl2anc 585 |
. . . . . . . . . . . . . . 15
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ โ On โง ๐ท โ (๐ด โ 1o))) โ ๐ธ โ On) |
33 | | oaword1 8504 |
. . . . . . . . . . . . . . 15
โข ((((๐ด โo ๐ถ) ยทo ๐ท) โ On โง ๐ธ โ On) โ ((๐ด โo ๐ถ) ยทo ๐ท) โ (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ)) |
34 | 29, 32, 33 | syl2anc 585 |
. . . . . . . . . . . . . 14
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ โ On โง ๐ท โ (๐ด โ 1o))) โ ((๐ด โo ๐ถ) ยทo ๐ท) โ (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ)) |
35 | | simplrr 777 |
. . . . . . . . . . . . . 14
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ โ On โง ๐ท โ (๐ด โ 1o))) โ (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต) |
36 | 34, 35 | sseqtrd 3989 |
. . . . . . . . . . . . 13
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ โ On โง ๐ท โ (๐ด โ 1o))) โ ((๐ด โo ๐ถ) ยทo ๐ท) โ ๐ต) |
37 | 27, 36 | sstrd 3959 |
. . . . . . . . . . . 12
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ โ On โง ๐ท โ (๐ด โ 1o))) โ (๐ด โo ๐ถ) โ ๐ต) |
38 | | oeeu.1 |
. . . . . . . . . . . . . . 15
โข ๐ = โช
โฉ {๐ฅ โ On โฃ ๐ต โ (๐ด โo ๐ฅ)} |
39 | 38 | oeeulem 8553 |
. . . . . . . . . . . . . 14
โข ((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โ (๐ โ On โง (๐ด โo ๐) โ ๐ต โง ๐ต โ (๐ด โo suc ๐))) |
40 | 39 | simp3d 1145 |
. . . . . . . . . . . . 13
โข ((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โ ๐ต โ (๐ด โo suc ๐)) |
41 | 40 | ad2antrr 725 |
. . . . . . . . . . . 12
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ โ On โง ๐ท โ (๐ด โ 1o))) โ ๐ต โ (๐ด โo suc ๐)) |
42 | 39 | simp1d 1143 |
. . . . . . . . . . . . . . . 16
โข ((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โ ๐ โ On) |
43 | 42 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ โ On โง ๐ท โ (๐ด โ 1o))) โ ๐ โ On) |
44 | | onsuc 7751 |
. . . . . . . . . . . . . . 15
โข (๐ โ On โ suc ๐ โ On) |
45 | 43, 44 | syl 17 |
. . . . . . . . . . . . . 14
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ โ On โง ๐ท โ (๐ด โ 1o))) โ suc ๐ โ On) |
46 | | oecl 8488 |
. . . . . . . . . . . . . 14
โข ((๐ด โ On โง suc ๐ โ On) โ (๐ด โo suc ๐) โ On) |
47 | 3, 45, 46 | syl2anc 585 |
. . . . . . . . . . . . 13
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ โ On โง ๐ท โ (๐ด โ 1o))) โ (๐ด โo suc ๐) โ On) |
48 | | ontr2 6369 |
. . . . . . . . . . . . 13
โข (((๐ด โo ๐ถ) โ On โง (๐ด โo suc ๐) โ On) โ (((๐ด โo ๐ถ) โ ๐ต โง ๐ต โ (๐ด โo suc ๐)) โ (๐ด โo ๐ถ) โ (๐ด โo suc ๐))) |
49 | 6, 47, 48 | syl2anc 585 |
. . . . . . . . . . . 12
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ โ On โง ๐ท โ (๐ด โ 1o))) โ (((๐ด โo ๐ถ) โ ๐ต โง ๐ต โ (๐ด โo suc ๐)) โ (๐ด โo ๐ถ) โ (๐ด โo suc ๐))) |
50 | 37, 41, 49 | mp2and 698 |
. . . . . . . . . . 11
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ โ On โง ๐ท โ (๐ด โ 1o))) โ (๐ด โo ๐ถ) โ (๐ด โo suc ๐)) |
51 | | simplll 774 |
. . . . . . . . . . . 12
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ โ On โง ๐ท โ (๐ด โ 1o))) โ ๐ด โ (On โ
2o)) |
52 | | oeord 8540 |
. . . . . . . . . . . 12
โข ((๐ถ โ On โง suc ๐ โ On โง ๐ด โ (On โ
2o)) โ (๐ถ
โ suc ๐ โ (๐ด โo ๐ถ) โ (๐ด โo suc ๐))) |
53 | 4, 45, 51, 52 | syl3anc 1372 |
. . . . . . . . . . 11
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ โ On โง ๐ท โ (๐ด โ 1o))) โ (๐ถ โ suc ๐ โ (๐ด โo ๐ถ) โ (๐ด โo suc ๐))) |
54 | 50, 53 | mpbird 257 |
. . . . . . . . . 10
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ โ On โง ๐ท โ (๐ด โ 1o))) โ ๐ถ โ suc ๐) |
55 | | onsssuc 6412 |
. . . . . . . . . . 11
โข ((๐ถ โ On โง ๐ โ On) โ (๐ถ โ ๐ โ ๐ถ โ suc ๐)) |
56 | 4, 43, 55 | syl2anc 585 |
. . . . . . . . . 10
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ โ On โง ๐ท โ (๐ด โ 1o))) โ (๐ถ โ ๐ โ ๐ถ โ suc ๐)) |
57 | 54, 56 | mpbird 257 |
. . . . . . . . 9
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ โ On โง ๐ท โ (๐ด โ 1o))) โ ๐ถ โ ๐) |
58 | 39 | simp2d 1144 |
. . . . . . . . . . . . 13
โข ((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โ (๐ด โo ๐) โ ๐ต) |
59 | 58 | ad2antrr 725 |
. . . . . . . . . . . 12
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ โ On โง ๐ท โ (๐ด โ 1o))) โ (๐ด โo ๐) โ ๐ต) |
60 | | eloni 6332 |
. . . . . . . . . . . . . . . . 17
โข (๐ด โ On โ Ord ๐ด) |
61 | 3, 60 | syl 17 |
. . . . . . . . . . . . . . . 16
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ โ On โง ๐ท โ (๐ด โ 1o))) โ Ord ๐ด) |
62 | | ordsucss 7758 |
. . . . . . . . . . . . . . . 16
โข (Ord
๐ด โ (๐ท โ ๐ด โ suc ๐ท โ ๐ด)) |
63 | 61, 14, 62 | sylc 65 |
. . . . . . . . . . . . . . 15
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ โ On โง ๐ท โ (๐ด โ 1o))) โ suc ๐ท โ ๐ด) |
64 | | onsuc 7751 |
. . . . . . . . . . . . . . . . 17
โข (๐ท โ On โ suc ๐ท โ On) |
65 | 16, 64 | syl 17 |
. . . . . . . . . . . . . . . 16
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ โ On โง ๐ท โ (๐ด โ 1o))) โ suc ๐ท โ On) |
66 | | dif20el 8456 |
. . . . . . . . . . . . . . . . . 18
โข (๐ด โ (On โ
2o) โ โ
โ ๐ด) |
67 | 51, 66 | syl 17 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ โ On โง ๐ท โ (๐ด โ 1o))) โ โ
โ ๐ด) |
68 | | oen0 8538 |
. . . . . . . . . . . . . . . . 17
โข (((๐ด โ On โง ๐ถ โ On) โง โ
โ
๐ด) โ โ
โ
(๐ด โo ๐ถ)) |
69 | 3, 4, 67, 68 | syl21anc 837 |
. . . . . . . . . . . . . . . 16
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ โ On โง ๐ท โ (๐ด โ 1o))) โ โ
โ (๐ด
โo ๐ถ)) |
70 | | omword 8522 |
. . . . . . . . . . . . . . . 16
โข (((suc
๐ท โ On โง ๐ด โ On โง (๐ด โo ๐ถ) โ On) โง โ
โ (๐ด
โo ๐ถ))
โ (suc ๐ท โ ๐ด โ ((๐ด โo ๐ถ) ยทo suc ๐ท) โ ((๐ด โo ๐ถ) ยทo ๐ด))) |
71 | 65, 3, 6, 69, 70 | syl31anc 1374 |
. . . . . . . . . . . . . . 15
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ โ On โง ๐ท โ (๐ด โ 1o))) โ (suc ๐ท โ ๐ด โ ((๐ด โo ๐ถ) ยทo suc ๐ท) โ ((๐ด โo ๐ถ) ยทo ๐ด))) |
72 | 63, 71 | mpbid 231 |
. . . . . . . . . . . . . 14
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ โ On โง ๐ท โ (๐ด โ 1o))) โ ((๐ด โo ๐ถ) ยทo suc ๐ท) โ ((๐ด โo ๐ถ) ยทo ๐ด)) |
73 | | oaord 8499 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ธ โ On โง (๐ด โo ๐ถ) โ On โง ((๐ด โo ๐ถ) ยทo ๐ท) โ On) โ (๐ธ โ (๐ด โo ๐ถ) โ (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) โ (((๐ด โo ๐ถ) ยทo ๐ท) +o (๐ด โo ๐ถ)))) |
74 | 32, 6, 29, 73 | syl3anc 1372 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ โ On โง ๐ท โ (๐ด โ 1o))) โ (๐ธ โ (๐ด โo ๐ถ) โ (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) โ (((๐ด โo ๐ถ) ยทo ๐ท) +o (๐ด โo ๐ถ)))) |
75 | 30, 74 | mpbid 231 |
. . . . . . . . . . . . . . . 16
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ โ On โง ๐ท โ (๐ด โ 1o))) โ (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) โ (((๐ด โo ๐ถ) ยทo ๐ท) +o (๐ด โo ๐ถ))) |
76 | 35, 75 | eqeltrrd 2839 |
. . . . . . . . . . . . . . 15
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ โ On โง ๐ท โ (๐ด โ 1o))) โ ๐ต โ (((๐ด โo ๐ถ) ยทo ๐ท) +o (๐ด โo ๐ถ))) |
77 | | odi 8531 |
. . . . . . . . . . . . . . . . 17
โข (((๐ด โo ๐ถ) โ On โง ๐ท โ On โง 1o
โ On) โ ((๐ด
โo ๐ถ)
ยทo (๐ท
+o 1o)) = (((๐ด โo ๐ถ) ยทo ๐ท) +o ((๐ด โo ๐ถ) ยทo
1o))) |
78 | 6, 16, 23, 77 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ โ On โง ๐ท โ (๐ด โ 1o))) โ ((๐ด โo ๐ถ) ยทo (๐ท +o 1o)) =
(((๐ด โo
๐ถ) ยทo
๐ท) +o ((๐ด โo ๐ถ) ยทo
1o))) |
79 | | oa1suc 8482 |
. . . . . . . . . . . . . . . . . 18
โข (๐ท โ On โ (๐ท +o 1o) =
suc ๐ท) |
80 | 16, 79 | syl 17 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ โ On โง ๐ท โ (๐ด โ 1o))) โ (๐ท +o 1o) =
suc ๐ท) |
81 | 80 | oveq2d 7378 |
. . . . . . . . . . . . . . . 16
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ โ On โง ๐ท โ (๐ด โ 1o))) โ ((๐ด โo ๐ถ) ยทo (๐ท +o 1o)) =
((๐ด โo
๐ถ) ยทo suc
๐ท)) |
82 | 8 | oveq2d 7378 |
. . . . . . . . . . . . . . . 16
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ โ On โง ๐ท โ (๐ด โ 1o))) โ (((๐ด โo ๐ถ) ยทo ๐ท) +o ((๐ด โo ๐ถ) ยทo
1o)) = (((๐ด
โo ๐ถ)
ยทo ๐ท)
+o (๐ด
โo ๐ถ))) |
83 | 78, 81, 82 | 3eqtr3d 2785 |
. . . . . . . . . . . . . . 15
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ โ On โง ๐ท โ (๐ด โ 1o))) โ ((๐ด โo ๐ถ) ยทo suc ๐ท) = (((๐ด โo ๐ถ) ยทo ๐ท) +o (๐ด โo ๐ถ))) |
84 | 76, 83 | eleqtrrd 2841 |
. . . . . . . . . . . . . 14
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ โ On โง ๐ท โ (๐ด โ 1o))) โ ๐ต โ ((๐ด โo ๐ถ) ยทo suc ๐ท)) |
85 | 72, 84 | sseldd 3950 |
. . . . . . . . . . . . 13
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ โ On โง ๐ท โ (๐ด โ 1o))) โ ๐ต โ ((๐ด โo ๐ถ) ยทo ๐ด)) |
86 | | oesuc 8478 |
. . . . . . . . . . . . . 14
โข ((๐ด โ On โง ๐ถ โ On) โ (๐ด โo suc ๐ถ) = ((๐ด โo ๐ถ) ยทo ๐ด)) |
87 | 3, 4, 86 | syl2anc 585 |
. . . . . . . . . . . . 13
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ โ On โง ๐ท โ (๐ด โ 1o))) โ (๐ด โo suc ๐ถ) = ((๐ด โo ๐ถ) ยทo ๐ด)) |
88 | 85, 87 | eleqtrrd 2841 |
. . . . . . . . . . . 12
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ โ On โง ๐ท โ (๐ด โ 1o))) โ ๐ต โ (๐ด โo suc ๐ถ)) |
89 | | oecl 8488 |
. . . . . . . . . . . . . 14
โข ((๐ด โ On โง ๐ โ On) โ (๐ด โo ๐) โ On) |
90 | 3, 43, 89 | syl2anc 585 |
. . . . . . . . . . . . 13
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ โ On โง ๐ท โ (๐ด โ 1o))) โ (๐ด โo ๐) โ On) |
91 | | onsuc 7751 |
. . . . . . . . . . . . . . 15
โข (๐ถ โ On โ suc ๐ถ โ On) |
92 | 91 | ad2antrl 727 |
. . . . . . . . . . . . . 14
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ โ On โง ๐ท โ (๐ด โ 1o))) โ suc ๐ถ โ On) |
93 | | oecl 8488 |
. . . . . . . . . . . . . 14
โข ((๐ด โ On โง suc ๐ถ โ On) โ (๐ด โo suc ๐ถ) โ On) |
94 | 3, 92, 93 | syl2anc 585 |
. . . . . . . . . . . . 13
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ โ On โง ๐ท โ (๐ด โ 1o))) โ (๐ด โo suc ๐ถ) โ On) |
95 | | ontr2 6369 |
. . . . . . . . . . . . 13
โข (((๐ด โo ๐) โ On โง (๐ด โo suc ๐ถ) โ On) โ (((๐ด โo ๐) โ ๐ต โง ๐ต โ (๐ด โo suc ๐ถ)) โ (๐ด โo ๐) โ (๐ด โo suc ๐ถ))) |
96 | 90, 94, 95 | syl2anc 585 |
. . . . . . . . . . . 12
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ โ On โง ๐ท โ (๐ด โ 1o))) โ (((๐ด โo ๐) โ ๐ต โง ๐ต โ (๐ด โo suc ๐ถ)) โ (๐ด โo ๐) โ (๐ด โo suc ๐ถ))) |
97 | 59, 88, 96 | mp2and 698 |
. . . . . . . . . . 11
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ โ On โง ๐ท โ (๐ด โ 1o))) โ (๐ด โo ๐) โ (๐ด โo suc ๐ถ)) |
98 | | oeord 8540 |
. . . . . . . . . . . 12
โข ((๐ โ On โง suc ๐ถ โ On โง ๐ด โ (On โ
2o)) โ (๐
โ suc ๐ถ โ (๐ด โo ๐) โ (๐ด โo suc ๐ถ))) |
99 | 43, 92, 51, 98 | syl3anc 1372 |
. . . . . . . . . . 11
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ โ On โง ๐ท โ (๐ด โ 1o))) โ (๐ โ suc ๐ถ โ (๐ด โo ๐) โ (๐ด โo suc ๐ถ))) |
100 | 97, 99 | mpbird 257 |
. . . . . . . . . 10
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ โ On โง ๐ท โ (๐ด โ 1o))) โ ๐ โ suc ๐ถ) |
101 | | onsssuc 6412 |
. . . . . . . . . . 11
โข ((๐ โ On โง ๐ถ โ On) โ (๐ โ ๐ถ โ ๐ โ suc ๐ถ)) |
102 | 43, 4, 101 | syl2anc 585 |
. . . . . . . . . 10
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ โ On โง ๐ท โ (๐ด โ 1o))) โ (๐ โ ๐ถ โ ๐ โ suc ๐ถ)) |
103 | 100, 102 | mpbird 257 |
. . . . . . . . 9
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ โ On โง ๐ท โ (๐ด โ 1o))) โ ๐ โ ๐ถ) |
104 | 57, 103 | eqssd 3966 |
. . . . . . . 8
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ โ On โง ๐ท โ (๐ด โ 1o))) โ ๐ถ = ๐) |
105 | 104, 16 | jca 513 |
. . . . . . 7
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ โ On โง ๐ท โ (๐ด โ 1o))) โ (๐ถ = ๐ โง ๐ท โ On)) |
106 | | simprl 770 |
. . . . . . . . 9
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ = ๐ โง ๐ท โ On)) โ ๐ถ = ๐) |
107 | 42 | ad2antrr 725 |
. . . . . . . . 9
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ = ๐ โง ๐ท โ On)) โ ๐ โ On) |
108 | 106, 107 | eqeltrd 2838 |
. . . . . . . 8
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ = ๐ โง ๐ท โ On)) โ ๐ถ โ On) |
109 | 2 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ = ๐ โง ๐ท โ On)) โ ๐ด โ On) |
110 | 109, 108,
5 | syl2anc 585 |
. . . . . . . . . . . . . 14
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ = ๐ โง ๐ท โ On)) โ (๐ด โo ๐ถ) โ On) |
111 | | simprr 772 |
. . . . . . . . . . . . . 14
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ = ๐ โง ๐ท โ On)) โ ๐ท โ On) |
112 | 110, 111,
28 | syl2anc 585 |
. . . . . . . . . . . . 13
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ = ๐ โง ๐ท โ On)) โ ((๐ด โo ๐ถ) ยทo ๐ท) โ On) |
113 | | simplrl 776 |
. . . . . . . . . . . . . 14
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ = ๐ โง ๐ท โ On)) โ ๐ธ โ (๐ด โo ๐ถ)) |
114 | 110, 113,
31 | syl2anc 585 |
. . . . . . . . . . . . 13
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ = ๐ โง ๐ท โ On)) โ ๐ธ โ On) |
115 | 112, 114,
33 | syl2anc 585 |
. . . . . . . . . . . 12
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ = ๐ โง ๐ท โ On)) โ ((๐ด โo ๐ถ) ยทo ๐ท) โ (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ)) |
116 | | simplrr 777 |
. . . . . . . . . . . 12
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ = ๐ โง ๐ท โ On)) โ (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต) |
117 | 115, 116 | sseqtrd 3989 |
. . . . . . . . . . 11
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ = ๐ โง ๐ท โ On)) โ ((๐ด โo ๐ถ) ยทo ๐ท) โ ๐ต) |
118 | 40 | ad2antrr 725 |
. . . . . . . . . . . 12
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ = ๐ โง ๐ท โ On)) โ ๐ต โ (๐ด โo suc ๐)) |
119 | | suceq 6388 |
. . . . . . . . . . . . . . 15
โข (๐ถ = ๐ โ suc ๐ถ = suc ๐) |
120 | 119 | ad2antrl 727 |
. . . . . . . . . . . . . 14
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ = ๐ โง ๐ท โ On)) โ suc ๐ถ = suc ๐) |
121 | 120 | oveq2d 7378 |
. . . . . . . . . . . . 13
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ = ๐ โง ๐ท โ On)) โ (๐ด โo suc ๐ถ) = (๐ด โo suc ๐)) |
122 | 109, 108,
86 | syl2anc 585 |
. . . . . . . . . . . . 13
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ = ๐ โง ๐ท โ On)) โ (๐ด โo suc ๐ถ) = ((๐ด โo ๐ถ) ยทo ๐ด)) |
123 | 121, 122 | eqtr3d 2779 |
. . . . . . . . . . . 12
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ = ๐ โง ๐ท โ On)) โ (๐ด โo suc ๐) = ((๐ด โo ๐ถ) ยทo ๐ด)) |
124 | 118, 123 | eleqtrd 2840 |
. . . . . . . . . . 11
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ = ๐ โง ๐ท โ On)) โ ๐ต โ ((๐ด โo ๐ถ) ยทo ๐ด)) |
125 | | omcl 8487 |
. . . . . . . . . . . . 13
โข (((๐ด โo ๐ถ) โ On โง ๐ด โ On) โ ((๐ด โo ๐ถ) ยทo ๐ด) โ On) |
126 | 110, 109,
125 | syl2anc 585 |
. . . . . . . . . . . 12
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ = ๐ โง ๐ท โ On)) โ ((๐ด โo ๐ถ) ยทo ๐ด) โ On) |
127 | | ontr2 6369 |
. . . . . . . . . . . 12
โข ((((๐ด โo ๐ถ) ยทo ๐ท) โ On โง ((๐ด โo ๐ถ) ยทo ๐ด) โ On) โ ((((๐ด โo ๐ถ) ยทo ๐ท) โ ๐ต โง ๐ต โ ((๐ด โo ๐ถ) ยทo ๐ด)) โ ((๐ด โo ๐ถ) ยทo ๐ท) โ ((๐ด โo ๐ถ) ยทo ๐ด))) |
128 | 112, 126,
127 | syl2anc 585 |
. . . . . . . . . . 11
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ = ๐ โง ๐ท โ On)) โ ((((๐ด โo ๐ถ) ยทo ๐ท) โ ๐ต โง ๐ต โ ((๐ด โo ๐ถ) ยทo ๐ด)) โ ((๐ด โo ๐ถ) ยทo ๐ท) โ ((๐ด โo ๐ถ) ยทo ๐ด))) |
129 | 117, 124,
128 | mp2and 698 |
. . . . . . . . . 10
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ = ๐ โง ๐ท โ On)) โ ((๐ด โo ๐ถ) ยทo ๐ท) โ ((๐ด โo ๐ถ) ยทo ๐ด)) |
130 | 66 | adantr 482 |
. . . . . . . . . . . . 13
โข ((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โ โ
โ ๐ด) |
131 | 130 | ad2antrr 725 |
. . . . . . . . . . . 12
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ = ๐ โง ๐ท โ On)) โ โ
โ ๐ด) |
132 | 109, 108,
131, 68 | syl21anc 837 |
. . . . . . . . . . 11
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ = ๐ โง ๐ท โ On)) โ โ
โ (๐ด โo ๐ถ)) |
133 | | omord2 8519 |
. . . . . . . . . . 11
โข (((๐ท โ On โง ๐ด โ On โง (๐ด โo ๐ถ) โ On) โง โ
โ (๐ด
โo ๐ถ))
โ (๐ท โ ๐ด โ ((๐ด โo ๐ถ) ยทo ๐ท) โ ((๐ด โo ๐ถ) ยทo ๐ด))) |
134 | 111, 109,
110, 132, 133 | syl31anc 1374 |
. . . . . . . . . 10
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ = ๐ โง ๐ท โ On)) โ (๐ท โ ๐ด โ ((๐ด โo ๐ถ) ยทo ๐ท) โ ((๐ด โo ๐ถ) ยทo ๐ด))) |
135 | 129, 134 | mpbird 257 |
. . . . . . . . 9
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ = ๐ โง ๐ท โ On)) โ ๐ท โ ๐ด) |
136 | 106 | oveq2d 7378 |
. . . . . . . . . . . 12
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ = ๐ โง ๐ท โ On)) โ (๐ด โo ๐ถ) = (๐ด โo ๐)) |
137 | 58 | ad2antrr 725 |
. . . . . . . . . . . 12
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ = ๐ โง ๐ท โ On)) โ (๐ด โo ๐) โ ๐ต) |
138 | 136, 137 | eqsstrd 3987 |
. . . . . . . . . . 11
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ = ๐ โง ๐ท โ On)) โ (๐ด โo ๐ถ) โ ๐ต) |
139 | | eldifi 4091 |
. . . . . . . . . . . . . 14
โข (๐ต โ (On โ
1o) โ ๐ต
โ On) |
140 | 139 | adantl 483 |
. . . . . . . . . . . . 13
โข ((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โ ๐ต โ On) |
141 | 140 | ad2antrr 725 |
. . . . . . . . . . . 12
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ = ๐ โง ๐ท โ On)) โ ๐ต โ On) |
142 | | ontri1 6356 |
. . . . . . . . . . . 12
โข (((๐ด โo ๐ถ) โ On โง ๐ต โ On) โ ((๐ด โo ๐ถ) โ ๐ต โ ยฌ ๐ต โ (๐ด โo ๐ถ))) |
143 | 110, 141,
142 | syl2anc 585 |
. . . . . . . . . . 11
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ = ๐ โง ๐ท โ On)) โ ((๐ด โo ๐ถ) โ ๐ต โ ยฌ ๐ต โ (๐ด โo ๐ถ))) |
144 | 138, 143 | mpbid 231 |
. . . . . . . . . 10
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ = ๐ โง ๐ท โ On)) โ ยฌ ๐ต โ (๐ด โo ๐ถ)) |
145 | | om0 8468 |
. . . . . . . . . . . . . . . . 17
โข ((๐ด โo ๐ถ) โ On โ ((๐ด โo ๐ถ) ยทo โ
)
= โ
) |
146 | 110, 145 | syl 17 |
. . . . . . . . . . . . . . . 16
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ = ๐ โง ๐ท โ On)) โ ((๐ด โo ๐ถ) ยทo โ
) =
โ
) |
147 | 146 | oveq1d 7377 |
. . . . . . . . . . . . . . 15
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ = ๐ โง ๐ท โ On)) โ (((๐ด โo ๐ถ) ยทo โ
)
+o ๐ธ) = (โ
+o ๐ธ)) |
148 | | oa0r 8489 |
. . . . . . . . . . . . . . . 16
โข (๐ธ โ On โ (โ
+o ๐ธ) = ๐ธ) |
149 | 114, 148 | syl 17 |
. . . . . . . . . . . . . . 15
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ = ๐ โง ๐ท โ On)) โ (โ
+o
๐ธ) = ๐ธ) |
150 | 147, 149 | eqtrd 2777 |
. . . . . . . . . . . . . 14
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ = ๐ โง ๐ท โ On)) โ (((๐ด โo ๐ถ) ยทo โ
)
+o ๐ธ) = ๐ธ) |
151 | 150, 113 | eqeltrd 2838 |
. . . . . . . . . . . . 13
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ = ๐ โง ๐ท โ On)) โ (((๐ด โo ๐ถ) ยทo โ
)
+o ๐ธ) โ
(๐ด โo ๐ถ)) |
152 | | oveq2 7370 |
. . . . . . . . . . . . . . 15
โข (๐ท = โ
โ ((๐ด โo ๐ถ) ยทo ๐ท) = ((๐ด โo ๐ถ) ยทo
โ
)) |
153 | 152 | oveq1d 7377 |
. . . . . . . . . . . . . 14
โข (๐ท = โ
โ (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = (((๐ด โo ๐ถ) ยทo โ
)
+o ๐ธ)) |
154 | 153 | eleq1d 2823 |
. . . . . . . . . . . . 13
โข (๐ท = โ
โ ((((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) โ (๐ด โo ๐ถ) โ (((๐ด โo ๐ถ) ยทo โ
)
+o ๐ธ) โ
(๐ด โo ๐ถ))) |
155 | 151, 154 | syl5ibrcom 247 |
. . . . . . . . . . . 12
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ = ๐ โง ๐ท โ On)) โ (๐ท = โ
โ (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) โ (๐ด โo ๐ถ))) |
156 | 116 | eleq1d 2823 |
. . . . . . . . . . . 12
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ = ๐ โง ๐ท โ On)) โ ((((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) โ (๐ด โo ๐ถ) โ ๐ต โ (๐ด โo ๐ถ))) |
157 | 155, 156 | sylibd 238 |
. . . . . . . . . . 11
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ = ๐ โง ๐ท โ On)) โ (๐ท = โ
โ ๐ต โ (๐ด โo ๐ถ))) |
158 | 157 | necon3bd 2958 |
. . . . . . . . . 10
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ = ๐ โง ๐ท โ On)) โ (ยฌ ๐ต โ (๐ด โo ๐ถ) โ ๐ท โ โ
)) |
159 | 144, 158 | mpd 15 |
. . . . . . . . 9
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ = ๐ โง ๐ท โ On)) โ ๐ท โ โ
) |
160 | 135, 159,
10 | sylanbrc 584 |
. . . . . . . 8
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ = ๐ โง ๐ท โ On)) โ ๐ท โ (๐ด โ 1o)) |
161 | 108, 160 | jca 513 |
. . . . . . 7
โข ((((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โง (๐ถ = ๐ โง ๐ท โ On)) โ (๐ถ โ On โง ๐ท โ (๐ด โ 1o))) |
162 | 105, 161 | impbida 800 |
. . . . . 6
โข (((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โ ((๐ถ โ On โง ๐ท โ (๐ด โ 1o)) โ (๐ถ = ๐ โง ๐ท โ On))) |
163 | 162 | ex 414 |
. . . . 5
โข ((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โ ((๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต) โ ((๐ถ โ On โง ๐ท โ (๐ด โ 1o)) โ (๐ถ = ๐ โง ๐ท โ On)))) |
164 | 163 | pm5.32rd 579 |
. . . 4
โข ((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โ (((๐ถ โ On โง ๐ท โ (๐ด โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โ ((๐ถ = ๐ โง ๐ท โ On) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)))) |
165 | | anass 470 |
. . . 4
โข (((๐ถ = ๐ โง ๐ท โ On) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โ (๐ถ = ๐ โง (๐ท โ On โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)))) |
166 | 164, 165 | bitrdi 287 |
. . 3
โข ((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โ (((๐ถ โ On โง ๐ท โ (๐ด โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โ (๐ถ = ๐ โง (๐ท โ On โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต))))) |
167 | | 3anass 1096 |
. . . . . 6
โข ((๐ท โ On โง ๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต) โ (๐ท โ On โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต))) |
168 | | oveq2 7370 |
. . . . . . . 8
โข (๐ถ = ๐ โ (๐ด โo ๐ถ) = (๐ด โo ๐)) |
169 | 168 | eleq2d 2824 |
. . . . . . 7
โข (๐ถ = ๐ โ (๐ธ โ (๐ด โo ๐ถ) โ ๐ธ โ (๐ด โo ๐))) |
170 | 168 | oveq1d 7377 |
. . . . . . . . 9
โข (๐ถ = ๐ โ ((๐ด โo ๐ถ) ยทo ๐ท) = ((๐ด โo ๐) ยทo ๐ท)) |
171 | 170 | oveq1d 7377 |
. . . . . . . 8
โข (๐ถ = ๐ โ (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = (((๐ด โo ๐) ยทo ๐ท) +o ๐ธ)) |
172 | 171 | eqeq1d 2739 |
. . . . . . 7
โข (๐ถ = ๐ โ ((((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต โ (((๐ด โo ๐) ยทo ๐ท) +o ๐ธ) = ๐ต)) |
173 | 169, 172 | 3anbi23d 1440 |
. . . . . 6
โข (๐ถ = ๐ โ ((๐ท โ On โง ๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต) โ (๐ท โ On โง ๐ธ โ (๐ด โo ๐) โง (((๐ด โo ๐) ยทo ๐ท) +o ๐ธ) = ๐ต))) |
174 | 167, 173 | bitr3id 285 |
. . . . 5
โข (๐ถ = ๐ โ ((๐ท โ On โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โ (๐ท โ On โง ๐ธ โ (๐ด โo ๐) โง (((๐ด โo ๐) ยทo ๐ท) +o ๐ธ) = ๐ต))) |
175 | 2, 42, 89 | syl2anc 585 |
. . . . . 6
โข ((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โ (๐ด โo ๐) โ On) |
176 | | oen0 8538 |
. . . . . . . 8
โข (((๐ด โ On โง ๐ โ On) โง โ
โ
๐ด) โ โ
โ
(๐ด โo ๐)) |
177 | 2, 42, 130, 176 | syl21anc 837 |
. . . . . . 7
โข ((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โ โ
โ (๐ด โo ๐)) |
178 | 177 | ne0d 4300 |
. . . . . 6
โข ((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โ (๐ด โo ๐) โ โ
) |
179 | | omeu 8537 |
. . . . . . 7
โข (((๐ด โo ๐) โ On โง ๐ต โ On โง (๐ด โo ๐) โ โ
) โ
โ!๐โ๐ โ On โ๐ โ (๐ด โo ๐)(๐ = โจ๐, ๐โฉ โง (((๐ด โo ๐) ยทo ๐) +o ๐) = ๐ต)) |
180 | | oeeu.2 |
. . . . . . . . 9
โข ๐ = (โฉ๐คโ๐ฆ โ On โ๐ง โ (๐ด โo ๐)(๐ค = โจ๐ฆ, ๐งโฉ โง (((๐ด โo ๐) ยทo ๐ฆ) +o ๐ง) = ๐ต)) |
181 | | opeq1 4835 |
. . . . . . . . . . . . . 14
โข (๐ฆ = ๐ โ โจ๐ฆ, ๐งโฉ = โจ๐, ๐งโฉ) |
182 | 181 | eqeq2d 2748 |
. . . . . . . . . . . . 13
โข (๐ฆ = ๐ โ (๐ค = โจ๐ฆ, ๐งโฉ โ ๐ค = โจ๐, ๐งโฉ)) |
183 | | oveq2 7370 |
. . . . . . . . . . . . . . 15
โข (๐ฆ = ๐ โ ((๐ด โo ๐) ยทo ๐ฆ) = ((๐ด โo ๐) ยทo ๐)) |
184 | 183 | oveq1d 7377 |
. . . . . . . . . . . . . 14
โข (๐ฆ = ๐ โ (((๐ด โo ๐) ยทo ๐ฆ) +o ๐ง) = (((๐ด โo ๐) ยทo ๐) +o ๐ง)) |
185 | 184 | eqeq1d 2739 |
. . . . . . . . . . . . 13
โข (๐ฆ = ๐ โ ((((๐ด โo ๐) ยทo ๐ฆ) +o ๐ง) = ๐ต โ (((๐ด โo ๐) ยทo ๐) +o ๐ง) = ๐ต)) |
186 | 182, 185 | anbi12d 632 |
. . . . . . . . . . . 12
โข (๐ฆ = ๐ โ ((๐ค = โจ๐ฆ, ๐งโฉ โง (((๐ด โo ๐) ยทo ๐ฆ) +o ๐ง) = ๐ต) โ (๐ค = โจ๐, ๐งโฉ โง (((๐ด โo ๐) ยทo ๐) +o ๐ง) = ๐ต))) |
187 | | opeq2 4836 |
. . . . . . . . . . . . . 14
โข (๐ง = ๐ โ โจ๐, ๐งโฉ = โจ๐, ๐โฉ) |
188 | 187 | eqeq2d 2748 |
. . . . . . . . . . . . 13
โข (๐ง = ๐ โ (๐ค = โจ๐, ๐งโฉ โ ๐ค = โจ๐, ๐โฉ)) |
189 | | oveq2 7370 |
. . . . . . . . . . . . . 14
โข (๐ง = ๐ โ (((๐ด โo ๐) ยทo ๐) +o ๐ง) = (((๐ด โo ๐) ยทo ๐) +o ๐)) |
190 | 189 | eqeq1d 2739 |
. . . . . . . . . . . . 13
โข (๐ง = ๐ โ ((((๐ด โo ๐) ยทo ๐) +o ๐ง) = ๐ต โ (((๐ด โo ๐) ยทo ๐) +o ๐) = ๐ต)) |
191 | 188, 190 | anbi12d 632 |
. . . . . . . . . . . 12
โข (๐ง = ๐ โ ((๐ค = โจ๐, ๐งโฉ โง (((๐ด โo ๐) ยทo ๐) +o ๐ง) = ๐ต) โ (๐ค = โจ๐, ๐โฉ โง (((๐ด โo ๐) ยทo ๐) +o ๐) = ๐ต))) |
192 | 186, 191 | cbvrex2vw 3231 |
. . . . . . . . . . 11
โข
(โ๐ฆ โ On
โ๐ง โ (๐ด โo ๐)(๐ค = โจ๐ฆ, ๐งโฉ โง (((๐ด โo ๐) ยทo ๐ฆ) +o ๐ง) = ๐ต) โ โ๐ โ On โ๐ โ (๐ด โo ๐)(๐ค = โจ๐, ๐โฉ โง (((๐ด โo ๐) ยทo ๐) +o ๐) = ๐ต)) |
193 | | eqeq1 2741 |
. . . . . . . . . . . . 13
โข (๐ค = ๐ โ (๐ค = โจ๐, ๐โฉ โ ๐ = โจ๐, ๐โฉ)) |
194 | 193 | anbi1d 631 |
. . . . . . . . . . . 12
โข (๐ค = ๐ โ ((๐ค = โจ๐, ๐โฉ โง (((๐ด โo ๐) ยทo ๐) +o ๐) = ๐ต) โ (๐ = โจ๐, ๐โฉ โง (((๐ด โo ๐) ยทo ๐) +o ๐) = ๐ต))) |
195 | 194 | 2rexbidv 3214 |
. . . . . . . . . . 11
โข (๐ค = ๐ โ (โ๐ โ On โ๐ โ (๐ด โo ๐)(๐ค = โจ๐, ๐โฉ โง (((๐ด โo ๐) ยทo ๐) +o ๐) = ๐ต) โ โ๐ โ On โ๐ โ (๐ด โo ๐)(๐ = โจ๐, ๐โฉ โง (((๐ด โo ๐) ยทo ๐) +o ๐) = ๐ต))) |
196 | 192, 195 | bitrid 283 |
. . . . . . . . . 10
โข (๐ค = ๐ โ (โ๐ฆ โ On โ๐ง โ (๐ด โo ๐)(๐ค = โจ๐ฆ, ๐งโฉ โง (((๐ด โo ๐) ยทo ๐ฆ) +o ๐ง) = ๐ต) โ โ๐ โ On โ๐ โ (๐ด โo ๐)(๐ = โจ๐, ๐โฉ โง (((๐ด โo ๐) ยทo ๐) +o ๐) = ๐ต))) |
197 | 196 | cbviotavw 6461 |
. . . . . . . . 9
โข
(โฉ๐คโ๐ฆ โ On โ๐ง โ (๐ด โo ๐)(๐ค = โจ๐ฆ, ๐งโฉ โง (((๐ด โo ๐) ยทo ๐ฆ) +o ๐ง) = ๐ต)) = (โฉ๐โ๐ โ On โ๐ โ (๐ด โo ๐)(๐ = โจ๐, ๐โฉ โง (((๐ด โo ๐) ยทo ๐) +o ๐) = ๐ต)) |
198 | 180, 197 | eqtri 2765 |
. . . . . . . 8
โข ๐ = (โฉ๐โ๐ โ On โ๐ โ (๐ด โo ๐)(๐ = โจ๐, ๐โฉ โง (((๐ด โo ๐) ยทo ๐) +o ๐) = ๐ต)) |
199 | | oeeu.3 |
. . . . . . . 8
โข ๐ = (1st โ๐) |
200 | | oeeu.4 |
. . . . . . . 8
โข ๐ = (2nd โ๐) |
201 | | oveq2 7370 |
. . . . . . . . . 10
โข (๐ = ๐ท โ ((๐ด โo ๐) ยทo ๐) = ((๐ด โo ๐) ยทo ๐ท)) |
202 | 201 | oveq1d 7377 |
. . . . . . . . 9
โข (๐ = ๐ท โ (((๐ด โo ๐) ยทo ๐) +o ๐) = (((๐ด โo ๐) ยทo ๐ท) +o ๐)) |
203 | 202 | eqeq1d 2739 |
. . . . . . . 8
โข (๐ = ๐ท โ ((((๐ด โo ๐) ยทo ๐) +o ๐) = ๐ต โ (((๐ด โo ๐) ยทo ๐ท) +o ๐) = ๐ต)) |
204 | | oveq2 7370 |
. . . . . . . . 9
โข (๐ = ๐ธ โ (((๐ด โo ๐) ยทo ๐ท) +o ๐) = (((๐ด โo ๐) ยทo ๐ท) +o ๐ธ)) |
205 | 204 | eqeq1d 2739 |
. . . . . . . 8
โข (๐ = ๐ธ โ ((((๐ด โo ๐) ยทo ๐ท) +o ๐) = ๐ต โ (((๐ด โo ๐) ยทo ๐ท) +o ๐ธ) = ๐ต)) |
206 | 198, 199,
200, 203, 205 | opiota 7996 |
. . . . . . 7
โข
(โ!๐โ๐ โ On โ๐ โ (๐ด โo ๐)(๐ = โจ๐, ๐โฉ โง (((๐ด โo ๐) ยทo ๐) +o ๐) = ๐ต) โ ((๐ท โ On โง ๐ธ โ (๐ด โo ๐) โง (((๐ด โo ๐) ยทo ๐ท) +o ๐ธ) = ๐ต) โ (๐ท = ๐ โง ๐ธ = ๐))) |
207 | 179, 206 | syl 17 |
. . . . . 6
โข (((๐ด โo ๐) โ On โง ๐ต โ On โง (๐ด โo ๐) โ โ
) โ ((๐ท โ On โง ๐ธ โ (๐ด โo ๐) โง (((๐ด โo ๐) ยทo ๐ท) +o ๐ธ) = ๐ต) โ (๐ท = ๐ โง ๐ธ = ๐))) |
208 | 175, 140,
178, 207 | syl3anc 1372 |
. . . . 5
โข ((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โ ((๐ท โ On โง ๐ธ โ (๐ด โo ๐) โง (((๐ด โo ๐) ยทo ๐ท) +o ๐ธ) = ๐ต) โ (๐ท = ๐ โง ๐ธ = ๐))) |
209 | 174, 208 | sylan9bbr 512 |
. . . 4
โข (((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โง ๐ถ = ๐) โ ((๐ท โ On โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โ (๐ท = ๐ โง ๐ธ = ๐))) |
210 | 209 | pm5.32da 580 |
. . 3
โข ((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โ ((๐ถ = ๐ โง (๐ท โ On โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต))) โ (๐ถ = ๐ โง (๐ท = ๐ โง ๐ธ = ๐)))) |
211 | 166, 210 | bitrd 279 |
. 2
โข ((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โ (((๐ถ โ On โง ๐ท โ (๐ด โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต)) โ (๐ถ = ๐ โง (๐ท = ๐ โง ๐ธ = ๐)))) |
212 | | 3an4anass 1106 |
. 2
โข (((๐ถ โ On โง ๐ท โ (๐ด โ 1o) โง ๐ธ โ (๐ด โo ๐ถ)) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต) โ ((๐ถ โ On โง ๐ท โ (๐ด โ 1o)) โง (๐ธ โ (๐ด โo ๐ถ) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต))) |
213 | | 3anass 1096 |
. 2
โข ((๐ถ = ๐ โง ๐ท = ๐ โง ๐ธ = ๐) โ (๐ถ = ๐ โง (๐ท = ๐ โง ๐ธ = ๐))) |
214 | 211, 212,
213 | 3bitr4g 314 |
1
โข ((๐ด โ (On โ
2o) โง ๐ต
โ (On โ 1o)) โ (((๐ถ โ On โง ๐ท โ (๐ด โ 1o) โง ๐ธ โ (๐ด โo ๐ถ)) โง (((๐ด โo ๐ถ) ยทo ๐ท) +o ๐ธ) = ๐ต) โ (๐ถ = ๐ โง ๐ท = ๐ โง ๐ธ = ๐))) |