Step | Hyp | Ref
| Expression |
1 | | omordi 8517 |
. . 3
โข (((๐ต โ On โง ๐ถ โ On) โง โ
โ
๐ถ) โ (๐ด โ ๐ต โ (๐ถ ยทo ๐ด) โ (๐ถ ยทo ๐ต))) |
2 | 1 | 3adantl1 1167 |
. 2
โข (((๐ด โ On โง ๐ต โ On โง ๐ถ โ On) โง โ
โ
๐ถ) โ (๐ด โ ๐ต โ (๐ถ ยทo ๐ด) โ (๐ถ ยทo ๐ต))) |
3 | | oveq2 7369 |
. . . . . 6
โข (๐ด = ๐ต โ (๐ถ ยทo ๐ด) = (๐ถ ยทo ๐ต)) |
4 | 3 | a1i 11 |
. . . . 5
โข (((๐ด โ On โง ๐ต โ On โง ๐ถ โ On) โง โ
โ
๐ถ) โ (๐ด = ๐ต โ (๐ถ ยทo ๐ด) = (๐ถ ยทo ๐ต))) |
5 | | omordi 8517 |
. . . . . 6
โข (((๐ด โ On โง ๐ถ โ On) โง โ
โ
๐ถ) โ (๐ต โ ๐ด โ (๐ถ ยทo ๐ต) โ (๐ถ ยทo ๐ด))) |
6 | 5 | 3adantl2 1168 |
. . . . 5
โข (((๐ด โ On โง ๐ต โ On โง ๐ถ โ On) โง โ
โ
๐ถ) โ (๐ต โ ๐ด โ (๐ถ ยทo ๐ต) โ (๐ถ ยทo ๐ด))) |
7 | 4, 6 | orim12d 964 |
. . . 4
โข (((๐ด โ On โง ๐ต โ On โง ๐ถ โ On) โง โ
โ
๐ถ) โ ((๐ด = ๐ต โจ ๐ต โ ๐ด) โ ((๐ถ ยทo ๐ด) = (๐ถ ยทo ๐ต) โจ (๐ถ ยทo ๐ต) โ (๐ถ ยทo ๐ด)))) |
8 | 7 | con3d 152 |
. . 3
โข (((๐ด โ On โง ๐ต โ On โง ๐ถ โ On) โง โ
โ
๐ถ) โ (ยฌ ((๐ถ ยทo ๐ด) = (๐ถ ยทo ๐ต) โจ (๐ถ ยทo ๐ต) โ (๐ถ ยทo ๐ด)) โ ยฌ (๐ด = ๐ต โจ ๐ต โ ๐ด))) |
9 | | omcl 8486 |
. . . . . . . 8
โข ((๐ถ โ On โง ๐ด โ On) โ (๐ถ ยทo ๐ด) โ On) |
10 | | omcl 8486 |
. . . . . . . 8
โข ((๐ถ โ On โง ๐ต โ On) โ (๐ถ ยทo ๐ต) โ On) |
11 | | eloni 6331 |
. . . . . . . . 9
โข ((๐ถ ยทo ๐ด) โ On โ Ord (๐ถ ยทo ๐ด)) |
12 | | eloni 6331 |
. . . . . . . . 9
โข ((๐ถ ยทo ๐ต) โ On โ Ord (๐ถ ยทo ๐ต)) |
13 | | ordtri2 6356 |
. . . . . . . . 9
โข ((Ord
(๐ถ ยทo
๐ด) โง Ord (๐ถ ยทo ๐ต)) โ ((๐ถ ยทo ๐ด) โ (๐ถ ยทo ๐ต) โ ยฌ ((๐ถ ยทo ๐ด) = (๐ถ ยทo ๐ต) โจ (๐ถ ยทo ๐ต) โ (๐ถ ยทo ๐ด)))) |
14 | 11, 12, 13 | syl2an 597 |
. . . . . . . 8
โข (((๐ถ ยทo ๐ด) โ On โง (๐ถ ยทo ๐ต) โ On) โ ((๐ถ ยทo ๐ด) โ (๐ถ ยทo ๐ต) โ ยฌ ((๐ถ ยทo ๐ด) = (๐ถ ยทo ๐ต) โจ (๐ถ ยทo ๐ต) โ (๐ถ ยทo ๐ด)))) |
15 | 9, 10, 14 | syl2an 597 |
. . . . . . 7
โข (((๐ถ โ On โง ๐ด โ On) โง (๐ถ โ On โง ๐ต โ On)) โ ((๐ถ ยทo ๐ด) โ (๐ถ ยทo ๐ต) โ ยฌ ((๐ถ ยทo ๐ด) = (๐ถ ยทo ๐ต) โจ (๐ถ ยทo ๐ต) โ (๐ถ ยทo ๐ด)))) |
16 | 15 | anandis 677 |
. . . . . 6
โข ((๐ถ โ On โง (๐ด โ On โง ๐ต โ On)) โ ((๐ถ ยทo ๐ด) โ (๐ถ ยทo ๐ต) โ ยฌ ((๐ถ ยทo ๐ด) = (๐ถ ยทo ๐ต) โจ (๐ถ ยทo ๐ต) โ (๐ถ ยทo ๐ด)))) |
17 | 16 | ancoms 460 |
. . . . 5
โข (((๐ด โ On โง ๐ต โ On) โง ๐ถ โ On) โ ((๐ถ ยทo ๐ด) โ (๐ถ ยทo ๐ต) โ ยฌ ((๐ถ ยทo ๐ด) = (๐ถ ยทo ๐ต) โจ (๐ถ ยทo ๐ต) โ (๐ถ ยทo ๐ด)))) |
18 | 17 | 3impa 1111 |
. . . 4
โข ((๐ด โ On โง ๐ต โ On โง ๐ถ โ On) โ ((๐ถ ยทo ๐ด) โ (๐ถ ยทo ๐ต) โ ยฌ ((๐ถ ยทo ๐ด) = (๐ถ ยทo ๐ต) โจ (๐ถ ยทo ๐ต) โ (๐ถ ยทo ๐ด)))) |
19 | 18 | adantr 482 |
. . 3
โข (((๐ด โ On โง ๐ต โ On โง ๐ถ โ On) โง โ
โ
๐ถ) โ ((๐ถ ยทo ๐ด) โ (๐ถ ยทo ๐ต) โ ยฌ ((๐ถ ยทo ๐ด) = (๐ถ ยทo ๐ต) โจ (๐ถ ยทo ๐ต) โ (๐ถ ยทo ๐ด)))) |
20 | | eloni 6331 |
. . . . . 6
โข (๐ด โ On โ Ord ๐ด) |
21 | | eloni 6331 |
. . . . . 6
โข (๐ต โ On โ Ord ๐ต) |
22 | | ordtri2 6356 |
. . . . . 6
โข ((Ord
๐ด โง Ord ๐ต) โ (๐ด โ ๐ต โ ยฌ (๐ด = ๐ต โจ ๐ต โ ๐ด))) |
23 | 20, 21, 22 | syl2an 597 |
. . . . 5
โข ((๐ด โ On โง ๐ต โ On) โ (๐ด โ ๐ต โ ยฌ (๐ด = ๐ต โจ ๐ต โ ๐ด))) |
24 | 23 | 3adant3 1133 |
. . . 4
โข ((๐ด โ On โง ๐ต โ On โง ๐ถ โ On) โ (๐ด โ ๐ต โ ยฌ (๐ด = ๐ต โจ ๐ต โ ๐ด))) |
25 | 24 | adantr 482 |
. . 3
โข (((๐ด โ On โง ๐ต โ On โง ๐ถ โ On) โง โ
โ
๐ถ) โ (๐ด โ ๐ต โ ยฌ (๐ด = ๐ต โจ ๐ต โ ๐ด))) |
26 | 8, 19, 25 | 3imtr4d 294 |
. 2
โข (((๐ด โ On โง ๐ต โ On โง ๐ถ โ On) โง โ
โ
๐ถ) โ ((๐ถ ยทo ๐ด) โ (๐ถ ยทo ๐ต) โ ๐ด โ ๐ต)) |
27 | 2, 26 | impbid 211 |
1
โข (((๐ด โ On โง ๐ต โ On โง ๐ถ โ On) โง โ
โ
๐ถ) โ (๐ด โ ๐ต โ (๐ถ ยทo ๐ด) โ (๐ถ ยทo ๐ต))) |