Step | Hyp | Ref
| Expression |
1 | | omord2 8518 |
. . . 4
โข (((๐ด โ On โง ๐ต โ On โง ๐ถ โ On) โง โ
โ
๐ถ) โ (๐ด โ ๐ต โ (๐ถ ยทo ๐ด) โ (๐ถ ยทo ๐ต))) |
2 | 1 | ex 414 |
. . 3
โข ((๐ด โ On โง ๐ต โ On โง ๐ถ โ On) โ (โ
โ ๐ถ โ (๐ด โ ๐ต โ (๐ถ ยทo ๐ด) โ (๐ถ ยทo ๐ต)))) |
3 | 2 | pm5.32rd 579 |
. 2
โข ((๐ด โ On โง ๐ต โ On โง ๐ถ โ On) โ ((๐ด โ ๐ต โง โ
โ ๐ถ) โ ((๐ถ ยทo ๐ด) โ (๐ถ ยทo ๐ต) โง โ
โ ๐ถ))) |
4 | | simpl 484 |
. . 3
โข (((๐ถ ยทo ๐ด) โ (๐ถ ยทo ๐ต) โง โ
โ ๐ถ) โ (๐ถ ยทo ๐ด) โ (๐ถ ยทo ๐ต)) |
5 | | ne0i 4298 |
. . . . . . . 8
โข ((๐ถ ยทo ๐ด) โ (๐ถ ยทo ๐ต) โ (๐ถ ยทo ๐ต) โ โ
) |
6 | | om0r 8489 |
. . . . . . . . . 10
โข (๐ต โ On โ (โ
ยทo ๐ต) =
โ
) |
7 | | oveq1 7368 |
. . . . . . . . . . 11
โข (๐ถ = โ
โ (๐ถ ยทo ๐ต) = (โ
ยทo ๐ต)) |
8 | 7 | eqeq1d 2735 |
. . . . . . . . . 10
โข (๐ถ = โ
โ ((๐ถ ยทo ๐ต) = โ
โ (โ
ยทo ๐ต) =
โ
)) |
9 | 6, 8 | syl5ibrcom 247 |
. . . . . . . . 9
โข (๐ต โ On โ (๐ถ = โ
โ (๐ถ ยทo ๐ต) = โ
)) |
10 | 9 | necon3d 2961 |
. . . . . . . 8
โข (๐ต โ On โ ((๐ถ ยทo ๐ต) โ โ
โ ๐ถ โ โ
)) |
11 | 5, 10 | syl5 34 |
. . . . . . 7
โข (๐ต โ On โ ((๐ถ ยทo ๐ด) โ (๐ถ ยทo ๐ต) โ ๐ถ โ โ
)) |
12 | 11 | adantr 482 |
. . . . . 6
โข ((๐ต โ On โง ๐ถ โ On) โ ((๐ถ ยทo ๐ด) โ (๐ถ ยทo ๐ต) โ ๐ถ โ โ
)) |
13 | | on0eln0 6377 |
. . . . . . 7
โข (๐ถ โ On โ (โ
โ ๐ถ โ ๐ถ โ โ
)) |
14 | 13 | adantl 483 |
. . . . . 6
โข ((๐ต โ On โง ๐ถ โ On) โ (โ
โ ๐ถ โ ๐ถ โ โ
)) |
15 | 12, 14 | sylibrd 259 |
. . . . 5
โข ((๐ต โ On โง ๐ถ โ On) โ ((๐ถ ยทo ๐ด) โ (๐ถ ยทo ๐ต) โ โ
โ ๐ถ)) |
16 | 15 | 3adant1 1131 |
. . . 4
โข ((๐ด โ On โง ๐ต โ On โง ๐ถ โ On) โ ((๐ถ ยทo ๐ด) โ (๐ถ ยทo ๐ต) โ โ
โ ๐ถ)) |
17 | 16 | ancld 552 |
. . 3
โข ((๐ด โ On โง ๐ต โ On โง ๐ถ โ On) โ ((๐ถ ยทo ๐ด) โ (๐ถ ยทo ๐ต) โ ((๐ถ ยทo ๐ด) โ (๐ถ ยทo ๐ต) โง โ
โ ๐ถ))) |
18 | 4, 17 | impbid2 225 |
. 2
โข ((๐ด โ On โง ๐ต โ On โง ๐ถ โ On) โ (((๐ถ ยทo ๐ด) โ (๐ถ ยทo ๐ต) โง โ
โ ๐ถ) โ (๐ถ ยทo ๐ด) โ (๐ถ ยทo ๐ต))) |
19 | 3, 18 | bitrd 279 |
1
โข ((๐ด โ On โง ๐ต โ On โง ๐ถ โ On) โ ((๐ด โ ๐ต โง โ
โ ๐ถ) โ (๐ถ ยทo ๐ด) โ (๐ถ ยทo ๐ต))) |