Step | Hyp | Ref
| Expression |
1 | | omordi 8517 |
. . . . . . . . 9
โข (((๐ถ โ On โง ๐ด โ On) โง โ
โ
๐ด) โ (๐ต โ ๐ถ โ (๐ด ยทo ๐ต) โ (๐ด ยทo ๐ถ))) |
2 | 1 | ex 414 |
. . . . . . . 8
โข ((๐ถ โ On โง ๐ด โ On) โ (โ
โ ๐ด โ (๐ต โ ๐ถ โ (๐ด ยทo ๐ต) โ (๐ด ยทo ๐ถ)))) |
3 | 2 | ancoms 460 |
. . . . . . 7
โข ((๐ด โ On โง ๐ถ โ On) โ (โ
โ ๐ด โ (๐ต โ ๐ถ โ (๐ด ยทo ๐ต) โ (๐ด ยทo ๐ถ)))) |
4 | 3 | 3adant2 1132 |
. . . . . 6
โข ((๐ด โ On โง ๐ต โ On โง ๐ถ โ On) โ (โ
โ ๐ด โ (๐ต โ ๐ถ โ (๐ด ยทo ๐ต) โ (๐ด ยทo ๐ถ)))) |
5 | 4 | imp 408 |
. . . . 5
โข (((๐ด โ On โง ๐ต โ On โง ๐ถ โ On) โง โ
โ
๐ด) โ (๐ต โ ๐ถ โ (๐ด ยทo ๐ต) โ (๐ด ยทo ๐ถ))) |
6 | | omordi 8517 |
. . . . . . . . 9
โข (((๐ต โ On โง ๐ด โ On) โง โ
โ
๐ด) โ (๐ถ โ ๐ต โ (๐ด ยทo ๐ถ) โ (๐ด ยทo ๐ต))) |
7 | 6 | ex 414 |
. . . . . . . 8
โข ((๐ต โ On โง ๐ด โ On) โ (โ
โ ๐ด โ (๐ถ โ ๐ต โ (๐ด ยทo ๐ถ) โ (๐ด ยทo ๐ต)))) |
8 | 7 | ancoms 460 |
. . . . . . 7
โข ((๐ด โ On โง ๐ต โ On) โ (โ
โ ๐ด โ (๐ถ โ ๐ต โ (๐ด ยทo ๐ถ) โ (๐ด ยทo ๐ต)))) |
9 | 8 | 3adant3 1133 |
. . . . . 6
โข ((๐ด โ On โง ๐ต โ On โง ๐ถ โ On) โ (โ
โ ๐ด โ (๐ถ โ ๐ต โ (๐ด ยทo ๐ถ) โ (๐ด ยทo ๐ต)))) |
10 | 9 | imp 408 |
. . . . 5
โข (((๐ด โ On โง ๐ต โ On โง ๐ถ โ On) โง โ
โ
๐ด) โ (๐ถ โ ๐ต โ (๐ด ยทo ๐ถ) โ (๐ด ยทo ๐ต))) |
11 | 5, 10 | orim12d 964 |
. . . 4
โข (((๐ด โ On โง ๐ต โ On โง ๐ถ โ On) โง โ
โ
๐ด) โ ((๐ต โ ๐ถ โจ ๐ถ โ ๐ต) โ ((๐ด ยทo ๐ต) โ (๐ด ยทo ๐ถ) โจ (๐ด ยทo ๐ถ) โ (๐ด ยทo ๐ต)))) |
12 | 11 | con3d 152 |
. . 3
โข (((๐ด โ On โง ๐ต โ On โง ๐ถ โ On) โง โ
โ
๐ด) โ (ยฌ ((๐ด ยทo ๐ต) โ (๐ด ยทo ๐ถ) โจ (๐ด ยทo ๐ถ) โ (๐ด ยทo ๐ต)) โ ยฌ (๐ต โ ๐ถ โจ ๐ถ โ ๐ต))) |
13 | | omcl 8486 |
. . . . . . 7
โข ((๐ด โ On โง ๐ต โ On) โ (๐ด ยทo ๐ต) โ On) |
14 | | eloni 6331 |
. . . . . . 7
โข ((๐ด ยทo ๐ต) โ On โ Ord (๐ด ยทo ๐ต)) |
15 | 13, 14 | syl 17 |
. . . . . 6
โข ((๐ด โ On โง ๐ต โ On) โ Ord (๐ด ยทo ๐ต)) |
16 | | omcl 8486 |
. . . . . . 7
โข ((๐ด โ On โง ๐ถ โ On) โ (๐ด ยทo ๐ถ) โ On) |
17 | | eloni 6331 |
. . . . . . 7
โข ((๐ด ยทo ๐ถ) โ On โ Ord (๐ด ยทo ๐ถ)) |
18 | 16, 17 | syl 17 |
. . . . . 6
โข ((๐ด โ On โง ๐ถ โ On) โ Ord (๐ด ยทo ๐ถ)) |
19 | | ordtri3 6357 |
. . . . . 6
โข ((Ord
(๐ด ยทo
๐ต) โง Ord (๐ด ยทo ๐ถ)) โ ((๐ด ยทo ๐ต) = (๐ด ยทo ๐ถ) โ ยฌ ((๐ด ยทo ๐ต) โ (๐ด ยทo ๐ถ) โจ (๐ด ยทo ๐ถ) โ (๐ด ยทo ๐ต)))) |
20 | 15, 18, 19 | syl2an 597 |
. . . . 5
โข (((๐ด โ On โง ๐ต โ On) โง (๐ด โ On โง ๐ถ โ On)) โ ((๐ด ยทo ๐ต) = (๐ด ยทo ๐ถ) โ ยฌ ((๐ด ยทo ๐ต) โ (๐ด ยทo ๐ถ) โจ (๐ด ยทo ๐ถ) โ (๐ด ยทo ๐ต)))) |
21 | 20 | 3impdi 1351 |
. . . 4
โข ((๐ด โ On โง ๐ต โ On โง ๐ถ โ On) โ ((๐ด ยทo ๐ต) = (๐ด ยทo ๐ถ) โ ยฌ ((๐ด ยทo ๐ต) โ (๐ด ยทo ๐ถ) โจ (๐ด ยทo ๐ถ) โ (๐ด ยทo ๐ต)))) |
22 | 21 | adantr 482 |
. . 3
โข (((๐ด โ On โง ๐ต โ On โง ๐ถ โ On) โง โ
โ
๐ด) โ ((๐ด ยทo ๐ต) = (๐ด ยทo ๐ถ) โ ยฌ ((๐ด ยทo ๐ต) โ (๐ด ยทo ๐ถ) โจ (๐ด ยทo ๐ถ) โ (๐ด ยทo ๐ต)))) |
23 | | eloni 6331 |
. . . . . 6
โข (๐ต โ On โ Ord ๐ต) |
24 | | eloni 6331 |
. . . . . 6
โข (๐ถ โ On โ Ord ๐ถ) |
25 | | ordtri3 6357 |
. . . . . 6
โข ((Ord
๐ต โง Ord ๐ถ) โ (๐ต = ๐ถ โ ยฌ (๐ต โ ๐ถ โจ ๐ถ โ ๐ต))) |
26 | 23, 24, 25 | syl2an 597 |
. . . . 5
โข ((๐ต โ On โง ๐ถ โ On) โ (๐ต = ๐ถ โ ยฌ (๐ต โ ๐ถ โจ ๐ถ โ ๐ต))) |
27 | 26 | 3adant1 1131 |
. . . 4
โข ((๐ด โ On โง ๐ต โ On โง ๐ถ โ On) โ (๐ต = ๐ถ โ ยฌ (๐ต โ ๐ถ โจ ๐ถ โ ๐ต))) |
28 | 27 | adantr 482 |
. . 3
โข (((๐ด โ On โง ๐ต โ On โง ๐ถ โ On) โง โ
โ
๐ด) โ (๐ต = ๐ถ โ ยฌ (๐ต โ ๐ถ โจ ๐ถ โ ๐ต))) |
29 | 12, 22, 28 | 3imtr4d 294 |
. 2
โข (((๐ด โ On โง ๐ต โ On โง ๐ถ โ On) โง โ
โ
๐ด) โ ((๐ด ยทo ๐ต) = (๐ด ยทo ๐ถ) โ ๐ต = ๐ถ)) |
30 | | oveq2 7369 |
. 2
โข (๐ต = ๐ถ โ (๐ด ยทo ๐ต) = (๐ด ยทo ๐ถ)) |
31 | 29, 30 | impbid1 224 |
1
โข (((๐ด โ On โง ๐ต โ On โง ๐ถ โ On) โง โ
โ
๐ด) โ ((๐ด ยทo ๐ต) = (๐ด ยทo ๐ถ) โ ๐ต = ๐ถ)) |