Step | Hyp | Ref
| Expression |
1 | | omword 8521 |
. . . 4
โข (((๐ด โ On โง ๐ต โ On โง ๐ถ โ On) โง โ
โ
๐ถ) โ (๐ด โ ๐ต โ (๐ถ ยทo ๐ด) โ (๐ถ ยทo ๐ต))) |
2 | 1 | biimpd 228 |
. . 3
โข (((๐ด โ On โง ๐ต โ On โง ๐ถ โ On) โง โ
โ
๐ถ) โ (๐ด โ ๐ต โ (๐ถ ยทo ๐ด) โ (๐ถ ยทo ๐ต))) |
3 | 2 | ex 414 |
. 2
โข ((๐ด โ On โง ๐ต โ On โง ๐ถ โ On) โ (โ
โ ๐ถ โ (๐ด โ ๐ต โ (๐ถ ยทo ๐ด) โ (๐ถ ยทo ๐ต)))) |
4 | | eloni 6331 |
. . . . . 6
โข (๐ถ โ On โ Ord ๐ถ) |
5 | | ord0eln0 6376 |
. . . . . . 7
โข (Ord
๐ถ โ (โ
โ
๐ถ โ ๐ถ โ โ
)) |
6 | 5 | necon2bbid 2984 |
. . . . . 6
โข (Ord
๐ถ โ (๐ถ = โ
โ ยฌ โ
โ ๐ถ)) |
7 | 4, 6 | syl 17 |
. . . . 5
โข (๐ถ โ On โ (๐ถ = โ
โ ยฌ โ
โ ๐ถ)) |
8 | 7 | 3ad2ant3 1136 |
. . . 4
โข ((๐ด โ On โง ๐ต โ On โง ๐ถ โ On) โ (๐ถ = โ
โ ยฌ โ
โ ๐ถ)) |
9 | | ssid 3970 |
. . . . . . 7
โข โ
โ โ
|
10 | | om0r 8489 |
. . . . . . . . 9
โข (๐ด โ On โ (โ
ยทo ๐ด) =
โ
) |
11 | 10 | adantr 482 |
. . . . . . . 8
โข ((๐ด โ On โง ๐ต โ On) โ (โ
ยทo ๐ด) =
โ
) |
12 | | om0r 8489 |
. . . . . . . . 9
โข (๐ต โ On โ (โ
ยทo ๐ต) =
โ
) |
13 | 12 | adantl 483 |
. . . . . . . 8
โข ((๐ด โ On โง ๐ต โ On) โ (โ
ยทo ๐ต) =
โ
) |
14 | 11, 13 | sseq12d 3981 |
. . . . . . 7
โข ((๐ด โ On โง ๐ต โ On) โ ((โ
ยทo ๐ด)
โ (โ
ยทo ๐ต) โ โ
โ
โ
)) |
15 | 9, 14 | mpbiri 258 |
. . . . . 6
โข ((๐ด โ On โง ๐ต โ On) โ (โ
ยทo ๐ด)
โ (โ
ยทo ๐ต)) |
16 | | oveq1 7368 |
. . . . . . 7
โข (๐ถ = โ
โ (๐ถ ยทo ๐ด) = (โ
ยทo ๐ด)) |
17 | | oveq1 7368 |
. . . . . . 7
โข (๐ถ = โ
โ (๐ถ ยทo ๐ต) = (โ
ยทo ๐ต)) |
18 | 16, 17 | sseq12d 3981 |
. . . . . 6
โข (๐ถ = โ
โ ((๐ถ ยทo ๐ด) โ (๐ถ ยทo ๐ต) โ (โ
ยทo ๐ด) โ (โ
ยทo ๐ต))) |
19 | 15, 18 | syl5ibrcom 247 |
. . . . 5
โข ((๐ด โ On โง ๐ต โ On) โ (๐ถ = โ
โ (๐ถ ยทo ๐ด) โ (๐ถ ยทo ๐ต))) |
20 | 19 | 3adant3 1133 |
. . . 4
โข ((๐ด โ On โง ๐ต โ On โง ๐ถ โ On) โ (๐ถ = โ
โ (๐ถ ยทo ๐ด) โ (๐ถ ยทo ๐ต))) |
21 | 8, 20 | sylbird 260 |
. . 3
โข ((๐ด โ On โง ๐ต โ On โง ๐ถ โ On) โ (ยฌ
โ
โ ๐ถ โ
(๐ถ ยทo
๐ด) โ (๐ถ ยทo ๐ต))) |
22 | 21 | a1dd 50 |
. 2
โข ((๐ด โ On โง ๐ต โ On โง ๐ถ โ On) โ (ยฌ
โ
โ ๐ถ โ
(๐ด โ ๐ต โ (๐ถ ยทo ๐ด) โ (๐ถ ยทo ๐ต)))) |
23 | 3, 22 | pm2.61d 179 |
1
โข ((๐ด โ On โง ๐ต โ On โง ๐ถ โ On) โ (๐ด โ ๐ต โ (๐ถ ยทo ๐ด) โ (๐ถ ยทo ๐ต))) |