Step | Hyp | Ref
| Expression |
1 | | simp3l 1202 |
. . . . . 6
โข (((๐ด โ On โง ๐ด โ โ
) โง (๐ต โ On โง ๐ถ โ ๐ด) โง (๐ท โ On โง ๐ธ โ ๐ด)) โ ๐ท โ On) |
2 | | eloni 6331 |
. . . . . 6
โข (๐ท โ On โ Ord ๐ท) |
3 | | ordsucss 7757 |
. . . . . 6
โข (Ord
๐ท โ (๐ต โ ๐ท โ suc ๐ต โ ๐ท)) |
4 | 1, 2, 3 | 3syl 18 |
. . . . 5
โข (((๐ด โ On โง ๐ด โ โ
) โง (๐ต โ On โง ๐ถ โ ๐ด) โง (๐ท โ On โง ๐ธ โ ๐ด)) โ (๐ต โ ๐ท โ suc ๐ต โ ๐ท)) |
5 | | simp2l 1200 |
. . . . . . 7
โข (((๐ด โ On โง ๐ด โ โ
) โง (๐ต โ On โง ๐ถ โ ๐ด) โง (๐ท โ On โง ๐ธ โ ๐ด)) โ ๐ต โ On) |
6 | | onsuc 7750 |
. . . . . . 7
โข (๐ต โ On โ suc ๐ต โ On) |
7 | 5, 6 | syl 17 |
. . . . . 6
โข (((๐ด โ On โง ๐ด โ โ
) โง (๐ต โ On โง ๐ถ โ ๐ด) โง (๐ท โ On โง ๐ธ โ ๐ด)) โ suc ๐ต โ On) |
8 | | simp1l 1198 |
. . . . . 6
โข (((๐ด โ On โง ๐ด โ โ
) โง (๐ต โ On โง ๐ถ โ ๐ด) โง (๐ท โ On โง ๐ธ โ ๐ด)) โ ๐ด โ On) |
9 | | simp1r 1199 |
. . . . . . 7
โข (((๐ด โ On โง ๐ด โ โ
) โง (๐ต โ On โง ๐ถ โ ๐ด) โง (๐ท โ On โง ๐ธ โ ๐ด)) โ ๐ด โ โ
) |
10 | | on0eln0 6377 |
. . . . . . . 8
โข (๐ด โ On โ (โ
โ ๐ด โ ๐ด โ โ
)) |
11 | 8, 10 | syl 17 |
. . . . . . 7
โข (((๐ด โ On โง ๐ด โ โ
) โง (๐ต โ On โง ๐ถ โ ๐ด) โง (๐ท โ On โง ๐ธ โ ๐ด)) โ (โ
โ ๐ด โ ๐ด โ โ
)) |
12 | 9, 11 | mpbird 257 |
. . . . . 6
โข (((๐ด โ On โง ๐ด โ โ
) โง (๐ต โ On โง ๐ถ โ ๐ด) โง (๐ท โ On โง ๐ธ โ ๐ด)) โ โ
โ ๐ด) |
13 | | omword 8521 |
. . . . . 6
โข (((suc
๐ต โ On โง ๐ท โ On โง ๐ด โ On) โง โ
โ
๐ด) โ (suc ๐ต โ ๐ท โ (๐ด ยทo suc ๐ต) โ (๐ด ยทo ๐ท))) |
14 | 7, 1, 8, 12, 13 | syl31anc 1374 |
. . . . 5
โข (((๐ด โ On โง ๐ด โ โ
) โง (๐ต โ On โง ๐ถ โ ๐ด) โง (๐ท โ On โง ๐ธ โ ๐ด)) โ (suc ๐ต โ ๐ท โ (๐ด ยทo suc ๐ต) โ (๐ด ยทo ๐ท))) |
15 | 4, 14 | sylibd 238 |
. . . 4
โข (((๐ด โ On โง ๐ด โ โ
) โง (๐ต โ On โง ๐ถ โ ๐ด) โง (๐ท โ On โง ๐ธ โ ๐ด)) โ (๐ต โ ๐ท โ (๐ด ยทo suc ๐ต) โ (๐ด ยทo ๐ท))) |
16 | | omcl 8486 |
. . . . . 6
โข ((๐ด โ On โง ๐ท โ On) โ (๐ด ยทo ๐ท) โ On) |
17 | 8, 1, 16 | syl2anc 585 |
. . . . 5
โข (((๐ด โ On โง ๐ด โ โ
) โง (๐ต โ On โง ๐ถ โ ๐ด) โง (๐ท โ On โง ๐ธ โ ๐ด)) โ (๐ด ยทo ๐ท) โ On) |
18 | | simp3r 1203 |
. . . . . 6
โข (((๐ด โ On โง ๐ด โ โ
) โง (๐ต โ On โง ๐ถ โ ๐ด) โง (๐ท โ On โง ๐ธ โ ๐ด)) โ ๐ธ โ ๐ด) |
19 | | onelon 6346 |
. . . . . 6
โข ((๐ด โ On โง ๐ธ โ ๐ด) โ ๐ธ โ On) |
20 | 8, 18, 19 | syl2anc 585 |
. . . . 5
โข (((๐ด โ On โง ๐ด โ โ
) โง (๐ต โ On โง ๐ถ โ ๐ด) โง (๐ท โ On โง ๐ธ โ ๐ด)) โ ๐ธ โ On) |
21 | | oaword1 8503 |
. . . . . 6
โข (((๐ด ยทo ๐ท) โ On โง ๐ธ โ On) โ (๐ด ยทo ๐ท) โ ((๐ด ยทo ๐ท) +o ๐ธ)) |
22 | | sstr 3956 |
. . . . . . 7
โข (((๐ด ยทo suc ๐ต) โ (๐ด ยทo ๐ท) โง (๐ด ยทo ๐ท) โ ((๐ด ยทo ๐ท) +o ๐ธ)) โ (๐ด ยทo suc ๐ต) โ ((๐ด ยทo ๐ท) +o ๐ธ)) |
23 | 22 | expcom 415 |
. . . . . 6
โข ((๐ด ยทo ๐ท) โ ((๐ด ยทo ๐ท) +o ๐ธ) โ ((๐ด ยทo suc ๐ต) โ (๐ด ยทo ๐ท) โ (๐ด ยทo suc ๐ต) โ ((๐ด ยทo ๐ท) +o ๐ธ))) |
24 | 21, 23 | syl 17 |
. . . . 5
โข (((๐ด ยทo ๐ท) โ On โง ๐ธ โ On) โ ((๐ด ยทo suc ๐ต) โ (๐ด ยทo ๐ท) โ (๐ด ยทo suc ๐ต) โ ((๐ด ยทo ๐ท) +o ๐ธ))) |
25 | 17, 20, 24 | syl2anc 585 |
. . . 4
โข (((๐ด โ On โง ๐ด โ โ
) โง (๐ต โ On โง ๐ถ โ ๐ด) โง (๐ท โ On โง ๐ธ โ ๐ด)) โ ((๐ด ยทo suc ๐ต) โ (๐ด ยทo ๐ท) โ (๐ด ยทo suc ๐ต) โ ((๐ด ยทo ๐ท) +o ๐ธ))) |
26 | 15, 25 | syld 47 |
. . 3
โข (((๐ด โ On โง ๐ด โ โ
) โง (๐ต โ On โง ๐ถ โ ๐ด) โง (๐ท โ On โง ๐ธ โ ๐ด)) โ (๐ต โ ๐ท โ (๐ด ยทo suc ๐ต) โ ((๐ด ยทo ๐ท) +o ๐ธ))) |
27 | | simp2r 1201 |
. . . . . 6
โข (((๐ด โ On โง ๐ด โ โ
) โง (๐ต โ On โง ๐ถ โ ๐ด) โง (๐ท โ On โง ๐ธ โ ๐ด)) โ ๐ถ โ ๐ด) |
28 | | onelon 6346 |
. . . . . 6
โข ((๐ด โ On โง ๐ถ โ ๐ด) โ ๐ถ โ On) |
29 | 8, 27, 28 | syl2anc 585 |
. . . . 5
โข (((๐ด โ On โง ๐ด โ โ
) โง (๐ต โ On โง ๐ถ โ ๐ด) โง (๐ท โ On โง ๐ธ โ ๐ด)) โ ๐ถ โ On) |
30 | | omcl 8486 |
. . . . . 6
โข ((๐ด โ On โง ๐ต โ On) โ (๐ด ยทo ๐ต) โ On) |
31 | 8, 5, 30 | syl2anc 585 |
. . . . 5
โข (((๐ด โ On โง ๐ด โ โ
) โง (๐ต โ On โง ๐ถ โ ๐ด) โง (๐ท โ On โง ๐ธ โ ๐ด)) โ (๐ด ยทo ๐ต) โ On) |
32 | | oaord 8498 |
. . . . . 6
โข ((๐ถ โ On โง ๐ด โ On โง (๐ด ยทo ๐ต) โ On) โ (๐ถ โ ๐ด โ ((๐ด ยทo ๐ต) +o ๐ถ) โ ((๐ด ยทo ๐ต) +o ๐ด))) |
33 | 32 | biimpa 478 |
. . . . 5
โข (((๐ถ โ On โง ๐ด โ On โง (๐ด ยทo ๐ต) โ On) โง ๐ถ โ ๐ด) โ ((๐ด ยทo ๐ต) +o ๐ถ) โ ((๐ด ยทo ๐ต) +o ๐ด)) |
34 | 29, 8, 31, 27, 33 | syl31anc 1374 |
. . . 4
โข (((๐ด โ On โง ๐ด โ โ
) โง (๐ต โ On โง ๐ถ โ ๐ด) โง (๐ท โ On โง ๐ธ โ ๐ด)) โ ((๐ด ยทo ๐ต) +o ๐ถ) โ ((๐ด ยทo ๐ต) +o ๐ด)) |
35 | | omsuc 8476 |
. . . . 5
โข ((๐ด โ On โง ๐ต โ On) โ (๐ด ยทo suc ๐ต) = ((๐ด ยทo ๐ต) +o ๐ด)) |
36 | 8, 5, 35 | syl2anc 585 |
. . . 4
โข (((๐ด โ On โง ๐ด โ โ
) โง (๐ต โ On โง ๐ถ โ ๐ด) โง (๐ท โ On โง ๐ธ โ ๐ด)) โ (๐ด ยทo suc ๐ต) = ((๐ด ยทo ๐ต) +o ๐ด)) |
37 | 34, 36 | eleqtrrd 2837 |
. . 3
โข (((๐ด โ On โง ๐ด โ โ
) โง (๐ต โ On โง ๐ถ โ ๐ด) โง (๐ท โ On โง ๐ธ โ ๐ด)) โ ((๐ด ยทo ๐ต) +o ๐ถ) โ (๐ด ยทo suc ๐ต)) |
38 | | ssel 3941 |
. . 3
โข ((๐ด ยทo suc ๐ต) โ ((๐ด ยทo ๐ท) +o ๐ธ) โ (((๐ด ยทo ๐ต) +o ๐ถ) โ (๐ด ยทo suc ๐ต) โ ((๐ด ยทo ๐ต) +o ๐ถ) โ ((๐ด ยทo ๐ท) +o ๐ธ))) |
39 | 26, 37, 38 | syl6ci 71 |
. 2
โข (((๐ด โ On โง ๐ด โ โ
) โง (๐ต โ On โง ๐ถ โ ๐ด) โง (๐ท โ On โง ๐ธ โ ๐ด)) โ (๐ต โ ๐ท โ ((๐ด ยทo ๐ต) +o ๐ถ) โ ((๐ด ยทo ๐ท) +o ๐ธ))) |
40 | | simpr 486 |
. . . . 5
โข ((๐ต = ๐ท โง ๐ถ โ ๐ธ) โ ๐ถ โ ๐ธ) |
41 | | oaord 8498 |
. . . . 5
โข ((๐ถ โ On โง ๐ธ โ On โง (๐ด ยทo ๐ต) โ On) โ (๐ถ โ ๐ธ โ ((๐ด ยทo ๐ต) +o ๐ถ) โ ((๐ด ยทo ๐ต) +o ๐ธ))) |
42 | 40, 41 | imbitrid 243 |
. . . 4
โข ((๐ถ โ On โง ๐ธ โ On โง (๐ด ยทo ๐ต) โ On) โ ((๐ต = ๐ท โง ๐ถ โ ๐ธ) โ ((๐ด ยทo ๐ต) +o ๐ถ) โ ((๐ด ยทo ๐ต) +o ๐ธ))) |
43 | | oveq2 7369 |
. . . . . . 7
โข (๐ต = ๐ท โ (๐ด ยทo ๐ต) = (๐ด ยทo ๐ท)) |
44 | 43 | oveq1d 7376 |
. . . . . 6
โข (๐ต = ๐ท โ ((๐ด ยทo ๐ต) +o ๐ธ) = ((๐ด ยทo ๐ท) +o ๐ธ)) |
45 | 44 | adantr 482 |
. . . . 5
โข ((๐ต = ๐ท โง ๐ถ โ ๐ธ) โ ((๐ด ยทo ๐ต) +o ๐ธ) = ((๐ด ยทo ๐ท) +o ๐ธ)) |
46 | 45 | eleq2d 2820 |
. . . 4
โข ((๐ต = ๐ท โง ๐ถ โ ๐ธ) โ (((๐ด ยทo ๐ต) +o ๐ถ) โ ((๐ด ยทo ๐ต) +o ๐ธ) โ ((๐ด ยทo ๐ต) +o ๐ถ) โ ((๐ด ยทo ๐ท) +o ๐ธ))) |
47 | 42, 46 | mpbidi 240 |
. . 3
โข ((๐ถ โ On โง ๐ธ โ On โง (๐ด ยทo ๐ต) โ On) โ ((๐ต = ๐ท โง ๐ถ โ ๐ธ) โ ((๐ด ยทo ๐ต) +o ๐ถ) โ ((๐ด ยทo ๐ท) +o ๐ธ))) |
48 | 29, 20, 31, 47 | syl3anc 1372 |
. 2
โข (((๐ด โ On โง ๐ด โ โ
) โง (๐ต โ On โง ๐ถ โ ๐ด) โง (๐ท โ On โง ๐ธ โ ๐ด)) โ ((๐ต = ๐ท โง ๐ถ โ ๐ธ) โ ((๐ด ยทo ๐ต) +o ๐ถ) โ ((๐ด ยทo ๐ท) +o ๐ธ))) |
49 | 39, 48 | jaod 858 |
1
โข (((๐ด โ On โง ๐ด โ โ
) โง (๐ต โ On โง ๐ถ โ ๐ด) โง (๐ท โ On โง ๐ธ โ ๐ด)) โ ((๐ต โ ๐ท โจ (๐ต = ๐ท โง ๐ถ โ ๐ธ)) โ ((๐ด ยทo ๐ต) +o ๐ถ) โ ((๐ด ยทo ๐ท) +o ๐ธ))) |