Step | Hyp | Ref
| Expression |
1 | | neanior 3034 |
. . . . 5
โข ((๐ด โ โ
โง ๐ต โ โ
) โ ยฌ
(๐ด = โ
โจ ๐ต = โ
)) |
2 | | eloni 6331 |
. . . . . . . . . 10
โข (๐ด โ On โ Ord ๐ด) |
3 | | ordge1n0 8444 |
. . . . . . . . . 10
โข (Ord
๐ด โ (1o
โ ๐ด โ ๐ด โ โ
)) |
4 | 2, 3 | syl 17 |
. . . . . . . . 9
โข (๐ด โ On โ (1o
โ ๐ด โ ๐ด โ โ
)) |
5 | 4 | biimprd 248 |
. . . . . . . 8
โข (๐ด โ On โ (๐ด โ โ
โ
1o โ ๐ด)) |
6 | 5 | adantr 482 |
. . . . . . 7
โข ((๐ด โ On โง ๐ต โ On) โ (๐ด โ โ
โ
1o โ ๐ด)) |
7 | | on0eln0 6377 |
. . . . . . . . 9
โข (๐ต โ On โ (โ
โ ๐ต โ ๐ต โ โ
)) |
8 | 7 | adantl 483 |
. . . . . . . 8
โข ((๐ด โ On โง ๐ต โ On) โ (โ
โ ๐ต โ ๐ต โ โ
)) |
9 | | omword1 8524 |
. . . . . . . . 9
โข (((๐ด โ On โง ๐ต โ On) โง โ
โ
๐ต) โ ๐ด โ (๐ด ยทo ๐ต)) |
10 | 9 | ex 414 |
. . . . . . . 8
โข ((๐ด โ On โง ๐ต โ On) โ (โ
โ ๐ต โ ๐ด โ (๐ด ยทo ๐ต))) |
11 | 8, 10 | sylbird 260 |
. . . . . . 7
โข ((๐ด โ On โง ๐ต โ On) โ (๐ต โ โ
โ ๐ด โ (๐ด ยทo ๐ต))) |
12 | 6, 11 | anim12d 610 |
. . . . . 6
โข ((๐ด โ On โง ๐ต โ On) โ ((๐ด โ โ
โง ๐ต โ โ
) โ
(1o โ ๐ด
โง ๐ด โ (๐ด ยทo ๐ต)))) |
13 | | sstr 3956 |
. . . . . 6
โข
((1o โ ๐ด โง ๐ด โ (๐ด ยทo ๐ต)) โ 1o โ (๐ด ยทo ๐ต)) |
14 | 12, 13 | syl6 35 |
. . . . 5
โข ((๐ด โ On โง ๐ต โ On) โ ((๐ด โ โ
โง ๐ต โ โ
) โ
1o โ (๐ด
ยทo ๐ต))) |
15 | 1, 14 | biimtrrid 242 |
. . . 4
โข ((๐ด โ On โง ๐ต โ On) โ (ยฌ (๐ด = โ
โจ ๐ต = โ
) โ 1o
โ (๐ด
ยทo ๐ต))) |
16 | | omcl 8486 |
. . . . 5
โข ((๐ด โ On โง ๐ต โ On) โ (๐ด ยทo ๐ต) โ On) |
17 | | eloni 6331 |
. . . . 5
โข ((๐ด ยทo ๐ต) โ On โ Ord (๐ด ยทo ๐ต)) |
18 | | ordge1n0 8444 |
. . . . 5
โข (Ord
(๐ด ยทo
๐ต) โ (1o
โ (๐ด
ยทo ๐ต)
โ (๐ด
ยทo ๐ต)
โ โ
)) |
19 | 16, 17, 18 | 3syl 18 |
. . . 4
โข ((๐ด โ On โง ๐ต โ On) โ
(1o โ (๐ด
ยทo ๐ต)
โ (๐ด
ยทo ๐ต)
โ โ
)) |
20 | 15, 19 | sylibd 238 |
. . 3
โข ((๐ด โ On โง ๐ต โ On) โ (ยฌ (๐ด = โ
โจ ๐ต = โ
) โ (๐ด ยทo ๐ต) โ
โ
)) |
21 | 20 | necon4bd 2960 |
. 2
โข ((๐ด โ On โง ๐ต โ On) โ ((๐ด ยทo ๐ต) = โ
โ (๐ด = โ
โจ ๐ต = โ
))) |
22 | | oveq1 7368 |
. . . . . 6
โข (๐ด = โ
โ (๐ด ยทo ๐ต) = (โ
ยทo ๐ต)) |
23 | | om0r 8489 |
. . . . . 6
โข (๐ต โ On โ (โ
ยทo ๐ต) =
โ
) |
24 | 22, 23 | sylan9eqr 2795 |
. . . . 5
โข ((๐ต โ On โง ๐ด = โ
) โ (๐ด ยทo ๐ต) = โ
) |
25 | 24 | ex 414 |
. . . 4
โข (๐ต โ On โ (๐ด = โ
โ (๐ด ยทo ๐ต) = โ
)) |
26 | 25 | adantl 483 |
. . 3
โข ((๐ด โ On โง ๐ต โ On) โ (๐ด = โ
โ (๐ด ยทo ๐ต) = โ
)) |
27 | | oveq2 7369 |
. . . . . 6
โข (๐ต = โ
โ (๐ด ยทo ๐ต) = (๐ด ยทo
โ
)) |
28 | | om0 8467 |
. . . . . 6
โข (๐ด โ On โ (๐ด ยทo โ
) =
โ
) |
29 | 27, 28 | sylan9eqr 2795 |
. . . . 5
โข ((๐ด โ On โง ๐ต = โ
) โ (๐ด ยทo ๐ต) = โ
) |
30 | 29 | ex 414 |
. . . 4
โข (๐ด โ On โ (๐ต = โ
โ (๐ด ยทo ๐ต) = โ
)) |
31 | 30 | adantr 482 |
. . 3
โข ((๐ด โ On โง ๐ต โ On) โ (๐ต = โ
โ (๐ด ยทo ๐ต) = โ
)) |
32 | 26, 31 | jaod 858 |
. 2
โข ((๐ด โ On โง ๐ต โ On) โ ((๐ด = โ
โจ ๐ต = โ
) โ (๐ด ยทo ๐ต) = โ
)) |
33 | 21, 32 | impbid 211 |
1
โข ((๐ด โ On โง ๐ต โ On) โ ((๐ด ยทo ๐ต) = โ
โ (๐ด = โ
โจ ๐ต = โ
))) |