Step | Hyp | Ref
| Expression |
1 | | omord2 8518 |
. . 3
โข (((๐ด โ On โง ๐ต โ On โง ๐ถ โ On) โง โ
โ
๐ถ) โ (๐ด โ ๐ต โ (๐ถ ยทo ๐ด) โ (๐ถ ยทo ๐ต))) |
2 | | 3anrot 1101 |
. . . . 5
โข ((๐ถ โ On โง ๐ด โ On โง ๐ต โ On) โ (๐ด โ On โง ๐ต โ On โง ๐ถ โ On)) |
3 | | omcan 8520 |
. . . . 5
โข (((๐ถ โ On โง ๐ด โ On โง ๐ต โ On) โง โ
โ
๐ถ) โ ((๐ถ ยทo ๐ด) = (๐ถ ยทo ๐ต) โ ๐ด = ๐ต)) |
4 | 2, 3 | sylanbr 583 |
. . . 4
โข (((๐ด โ On โง ๐ต โ On โง ๐ถ โ On) โง โ
โ
๐ถ) โ ((๐ถ ยทo ๐ด) = (๐ถ ยทo ๐ต) โ ๐ด = ๐ต)) |
5 | 4 | bicomd 222 |
. . 3
โข (((๐ด โ On โง ๐ต โ On โง ๐ถ โ On) โง โ
โ
๐ถ) โ (๐ด = ๐ต โ (๐ถ ยทo ๐ด) = (๐ถ ยทo ๐ต))) |
6 | 1, 5 | orbi12d 918 |
. 2
โข (((๐ด โ On โง ๐ต โ On โง ๐ถ โ On) โง โ
โ
๐ถ) โ ((๐ด โ ๐ต โจ ๐ด = ๐ต) โ ((๐ถ ยทo ๐ด) โ (๐ถ ยทo ๐ต) โจ (๐ถ ยทo ๐ด) = (๐ถ ยทo ๐ต)))) |
7 | | onsseleq 6362 |
. . . 4
โข ((๐ด โ On โง ๐ต โ On) โ (๐ด โ ๐ต โ (๐ด โ ๐ต โจ ๐ด = ๐ต))) |
8 | 7 | 3adant3 1133 |
. . 3
โข ((๐ด โ On โง ๐ต โ On โง ๐ถ โ On) โ (๐ด โ ๐ต โ (๐ด โ ๐ต โจ ๐ด = ๐ต))) |
9 | 8 | adantr 482 |
. 2
โข (((๐ด โ On โง ๐ต โ On โง ๐ถ โ On) โง โ
โ
๐ถ) โ (๐ด โ ๐ต โ (๐ด โ ๐ต โจ ๐ด = ๐ต))) |
10 | | omcl 8486 |
. . . . . . 7
โข ((๐ถ โ On โง ๐ด โ On) โ (๐ถ ยทo ๐ด) โ On) |
11 | | omcl 8486 |
. . . . . . 7
โข ((๐ถ โ On โง ๐ต โ On) โ (๐ถ ยทo ๐ต) โ On) |
12 | 10, 11 | anim12dan 620 |
. . . . . 6
โข ((๐ถ โ On โง (๐ด โ On โง ๐ต โ On)) โ ((๐ถ ยทo ๐ด) โ On โง (๐ถ ยทo ๐ต) โ On)) |
13 | 12 | ancoms 460 |
. . . . 5
โข (((๐ด โ On โง ๐ต โ On) โง ๐ถ โ On) โ ((๐ถ ยทo ๐ด) โ On โง (๐ถ ยทo ๐ต) โ On)) |
14 | 13 | 3impa 1111 |
. . . 4
โข ((๐ด โ On โง ๐ต โ On โง ๐ถ โ On) โ ((๐ถ ยทo ๐ด) โ On โง (๐ถ ยทo ๐ต) โ On)) |
15 | | onsseleq 6362 |
. . . 4
โข (((๐ถ ยทo ๐ด) โ On โง (๐ถ ยทo ๐ต) โ On) โ ((๐ถ ยทo ๐ด) โ (๐ถ ยทo ๐ต) โ ((๐ถ ยทo ๐ด) โ (๐ถ ยทo ๐ต) โจ (๐ถ ยทo ๐ด) = (๐ถ ยทo ๐ต)))) |
16 | 14, 15 | syl 17 |
. . 3
โข ((๐ด โ On โง ๐ต โ On โง ๐ถ โ On) โ ((๐ถ ยทo ๐ด) โ (๐ถ ยทo ๐ต) โ ((๐ถ ยทo ๐ด) โ (๐ถ ยทo ๐ต) โจ (๐ถ ยทo ๐ด) = (๐ถ ยทo ๐ต)))) |
17 | 16 | adantr 482 |
. 2
โข (((๐ด โ On โง ๐ต โ On โง ๐ถ โ On) โง โ
โ
๐ถ) โ ((๐ถ ยทo ๐ด) โ (๐ถ ยทo ๐ต) โ ((๐ถ ยทo ๐ด) โ (๐ถ ยทo ๐ต) โจ (๐ถ ยทo ๐ด) = (๐ถ ยทo ๐ต)))) |
18 | 6, 9, 17 | 3bitr4d 311 |
1
โข (((๐ด โ On โง ๐ต โ On โง ๐ถ โ On) โง โ
โ
๐ถ) โ (๐ด โ ๐ต โ (๐ถ ยทo ๐ด) โ (๐ถ ยทo ๐ต))) |