Step | Hyp | Ref
| Expression |
1 | | simpl2l 1227 |
. . . . . . 7
โข ((((๐ด โ On โง ๐ด โ โ
) โง (๐ต โ On โง ๐ถ โ ๐ด) โง (๐ท โ On โง ๐ธ โ ๐ด)) โง ((๐ด ยทo ๐ต) +o ๐ถ) = ((๐ด ยทo ๐ท) +o ๐ธ)) โ ๐ต โ On) |
2 | | eloni 6331 |
. . . . . . 7
โข (๐ต โ On โ Ord ๐ต) |
3 | 1, 2 | syl 17 |
. . . . . 6
โข ((((๐ด โ On โง ๐ด โ โ
) โง (๐ต โ On โง ๐ถ โ ๐ด) โง (๐ท โ On โง ๐ธ โ ๐ด)) โง ((๐ด ยทo ๐ต) +o ๐ถ) = ((๐ด ยทo ๐ท) +o ๐ธ)) โ Ord ๐ต) |
4 | | simpl3l 1229 |
. . . . . . 7
โข ((((๐ด โ On โง ๐ด โ โ
) โง (๐ต โ On โง ๐ถ โ ๐ด) โง (๐ท โ On โง ๐ธ โ ๐ด)) โง ((๐ด ยทo ๐ต) +o ๐ถ) = ((๐ด ยทo ๐ท) +o ๐ธ)) โ ๐ท โ On) |
5 | | eloni 6331 |
. . . . . . 7
โข (๐ท โ On โ Ord ๐ท) |
6 | 4, 5 | syl 17 |
. . . . . 6
โข ((((๐ด โ On โง ๐ด โ โ
) โง (๐ต โ On โง ๐ถ โ ๐ด) โง (๐ท โ On โง ๐ธ โ ๐ด)) โง ((๐ด ยทo ๐ต) +o ๐ถ) = ((๐ด ยทo ๐ท) +o ๐ธ)) โ Ord ๐ท) |
7 | | ordtri3or 6353 |
. . . . . 6
โข ((Ord
๐ต โง Ord ๐ท) โ (๐ต โ ๐ท โจ ๐ต = ๐ท โจ ๐ท โ ๐ต)) |
8 | 3, 6, 7 | syl2anc 585 |
. . . . 5
โข ((((๐ด โ On โง ๐ด โ โ
) โง (๐ต โ On โง ๐ถ โ ๐ด) โง (๐ท โ On โง ๐ธ โ ๐ด)) โง ((๐ด ยทo ๐ต) +o ๐ถ) = ((๐ด ยทo ๐ท) +o ๐ธ)) โ (๐ต โ ๐ท โจ ๐ต = ๐ท โจ ๐ท โ ๐ต)) |
9 | | simpr 486 |
. . . . . . . . 9
โข ((((๐ด โ On โง ๐ด โ โ
) โง (๐ต โ On โง ๐ถ โ ๐ด) โง (๐ท โ On โง ๐ธ โ ๐ด)) โง ((๐ด ยทo ๐ต) +o ๐ถ) = ((๐ด ยทo ๐ท) +o ๐ธ)) โ ((๐ด ยทo ๐ต) +o ๐ถ) = ((๐ด ยทo ๐ท) +o ๐ธ)) |
10 | | simpl1l 1225 |
. . . . . . . . . . . 12
โข ((((๐ด โ On โง ๐ด โ โ
) โง (๐ต โ On โง ๐ถ โ ๐ด) โง (๐ท โ On โง ๐ธ โ ๐ด)) โง ((๐ด ยทo ๐ต) +o ๐ถ) = ((๐ด ยทo ๐ท) +o ๐ธ)) โ ๐ด โ On) |
11 | | omcl 8486 |
. . . . . . . . . . . 12
โข ((๐ด โ On โง ๐ท โ On) โ (๐ด ยทo ๐ท) โ On) |
12 | 10, 4, 11 | syl2anc 585 |
. . . . . . . . . . 11
โข ((((๐ด โ On โง ๐ด โ โ
) โง (๐ต โ On โง ๐ถ โ ๐ด) โง (๐ท โ On โง ๐ธ โ ๐ด)) โง ((๐ด ยทo ๐ต) +o ๐ถ) = ((๐ด ยทo ๐ท) +o ๐ธ)) โ (๐ด ยทo ๐ท) โ On) |
13 | | simpl3r 1230 |
. . . . . . . . . . . 12
โข ((((๐ด โ On โง ๐ด โ โ
) โง (๐ต โ On โง ๐ถ โ ๐ด) โง (๐ท โ On โง ๐ธ โ ๐ด)) โง ((๐ด ยทo ๐ต) +o ๐ถ) = ((๐ด ยทo ๐ท) +o ๐ธ)) โ ๐ธ โ ๐ด) |
14 | | onelon 6346 |
. . . . . . . . . . . 12
โข ((๐ด โ On โง ๐ธ โ ๐ด) โ ๐ธ โ On) |
15 | 10, 13, 14 | syl2anc 585 |
. . . . . . . . . . 11
โข ((((๐ด โ On โง ๐ด โ โ
) โง (๐ต โ On โง ๐ถ โ ๐ด) โง (๐ท โ On โง ๐ธ โ ๐ด)) โง ((๐ด ยทo ๐ต) +o ๐ถ) = ((๐ด ยทo ๐ท) +o ๐ธ)) โ ๐ธ โ On) |
16 | | oacl 8485 |
. . . . . . . . . . 11
โข (((๐ด ยทo ๐ท) โ On โง ๐ธ โ On) โ ((๐ด ยทo ๐ท) +o ๐ธ) โ On) |
17 | 12, 15, 16 | syl2anc 585 |
. . . . . . . . . 10
โข ((((๐ด โ On โง ๐ด โ โ
) โง (๐ต โ On โง ๐ถ โ ๐ด) โง (๐ท โ On โง ๐ธ โ ๐ด)) โง ((๐ด ยทo ๐ต) +o ๐ถ) = ((๐ด ยทo ๐ท) +o ๐ธ)) โ ((๐ด ยทo ๐ท) +o ๐ธ) โ On) |
18 | | eloni 6331 |
. . . . . . . . . 10
โข (((๐ด ยทo ๐ท) +o ๐ธ) โ On โ Ord ((๐ด ยทo ๐ท) +o ๐ธ)) |
19 | | ordirr 6339 |
. . . . . . . . . 10
โข (Ord
((๐ด ยทo
๐ท) +o ๐ธ) โ ยฌ ((๐ด ยทo ๐ท) +o ๐ธ) โ ((๐ด ยทo ๐ท) +o ๐ธ)) |
20 | 17, 18, 19 | 3syl 18 |
. . . . . . . . 9
โข ((((๐ด โ On โง ๐ด โ โ
) โง (๐ต โ On โง ๐ถ โ ๐ด) โง (๐ท โ On โง ๐ธ โ ๐ด)) โง ((๐ด ยทo ๐ต) +o ๐ถ) = ((๐ด ยทo ๐ท) +o ๐ธ)) โ ยฌ ((๐ด ยทo ๐ท) +o ๐ธ) โ ((๐ด ยทo ๐ท) +o ๐ธ)) |
21 | 9, 20 | eqneltrd 2854 |
. . . . . . . 8
โข ((((๐ด โ On โง ๐ด โ โ
) โง (๐ต โ On โง ๐ถ โ ๐ด) โง (๐ท โ On โง ๐ธ โ ๐ด)) โง ((๐ด ยทo ๐ต) +o ๐ถ) = ((๐ด ยทo ๐ท) +o ๐ธ)) โ ยฌ ((๐ด ยทo ๐ต) +o ๐ถ) โ ((๐ด ยทo ๐ท) +o ๐ธ)) |
22 | | orc 866 |
. . . . . . . . 9
โข (๐ต โ ๐ท โ (๐ต โ ๐ท โจ (๐ต = ๐ท โง ๐ถ โ ๐ธ))) |
23 | | omeulem2 8534 |
. . . . . . . . . 10
โข (((๐ด โ On โง ๐ด โ โ
) โง (๐ต โ On โง ๐ถ โ ๐ด) โง (๐ท โ On โง ๐ธ โ ๐ด)) โ ((๐ต โ ๐ท โจ (๐ต = ๐ท โง ๐ถ โ ๐ธ)) โ ((๐ด ยทo ๐ต) +o ๐ถ) โ ((๐ด ยทo ๐ท) +o ๐ธ))) |
24 | 23 | adantr 482 |
. . . . . . . . 9
โข ((((๐ด โ On โง ๐ด โ โ
) โง (๐ต โ On โง ๐ถ โ ๐ด) โง (๐ท โ On โง ๐ธ โ ๐ด)) โง ((๐ด ยทo ๐ต) +o ๐ถ) = ((๐ด ยทo ๐ท) +o ๐ธ)) โ ((๐ต โ ๐ท โจ (๐ต = ๐ท โง ๐ถ โ ๐ธ)) โ ((๐ด ยทo ๐ต) +o ๐ถ) โ ((๐ด ยทo ๐ท) +o ๐ธ))) |
25 | 22, 24 | syl5 34 |
. . . . . . . 8
โข ((((๐ด โ On โง ๐ด โ โ
) โง (๐ต โ On โง ๐ถ โ ๐ด) โง (๐ท โ On โง ๐ธ โ ๐ด)) โง ((๐ด ยทo ๐ต) +o ๐ถ) = ((๐ด ยทo ๐ท) +o ๐ธ)) โ (๐ต โ ๐ท โ ((๐ด ยทo ๐ต) +o ๐ถ) โ ((๐ด ยทo ๐ท) +o ๐ธ))) |
26 | 21, 25 | mtod 197 |
. . . . . . 7
โข ((((๐ด โ On โง ๐ด โ โ
) โง (๐ต โ On โง ๐ถ โ ๐ด) โง (๐ท โ On โง ๐ธ โ ๐ด)) โง ((๐ด ยทo ๐ต) +o ๐ถ) = ((๐ด ยทo ๐ท) +o ๐ธ)) โ ยฌ ๐ต โ ๐ท) |
27 | 26 | pm2.21d 121 |
. . . . . 6
โข ((((๐ด โ On โง ๐ด โ โ
) โง (๐ต โ On โง ๐ถ โ ๐ด) โง (๐ท โ On โง ๐ธ โ ๐ด)) โง ((๐ด ยทo ๐ต) +o ๐ถ) = ((๐ด ยทo ๐ท) +o ๐ธ)) โ (๐ต โ ๐ท โ ๐ต = ๐ท)) |
28 | | idd 24 |
. . . . . 6
โข ((((๐ด โ On โง ๐ด โ โ
) โง (๐ต โ On โง ๐ถ โ ๐ด) โง (๐ท โ On โง ๐ธ โ ๐ด)) โง ((๐ด ยทo ๐ต) +o ๐ถ) = ((๐ด ยทo ๐ท) +o ๐ธ)) โ (๐ต = ๐ท โ ๐ต = ๐ท)) |
29 | 20, 9 | neleqtrrd 2857 |
. . . . . . . 8
โข ((((๐ด โ On โง ๐ด โ โ
) โง (๐ต โ On โง ๐ถ โ ๐ด) โง (๐ท โ On โง ๐ธ โ ๐ด)) โง ((๐ด ยทo ๐ต) +o ๐ถ) = ((๐ด ยทo ๐ท) +o ๐ธ)) โ ยฌ ((๐ด ยทo ๐ท) +o ๐ธ) โ ((๐ด ยทo ๐ต) +o ๐ถ)) |
30 | | orc 866 |
. . . . . . . . 9
โข (๐ท โ ๐ต โ (๐ท โ ๐ต โจ (๐ท = ๐ต โง ๐ธ โ ๐ถ))) |
31 | | simpl1r 1226 |
. . . . . . . . . 10
โข ((((๐ด โ On โง ๐ด โ โ
) โง (๐ต โ On โง ๐ถ โ ๐ด) โง (๐ท โ On โง ๐ธ โ ๐ด)) โง ((๐ด ยทo ๐ต) +o ๐ถ) = ((๐ด ยทo ๐ท) +o ๐ธ)) โ ๐ด โ โ
) |
32 | | simpl2r 1228 |
. . . . . . . . . 10
โข ((((๐ด โ On โง ๐ด โ โ
) โง (๐ต โ On โง ๐ถ โ ๐ด) โง (๐ท โ On โง ๐ธ โ ๐ด)) โง ((๐ด ยทo ๐ต) +o ๐ถ) = ((๐ด ยทo ๐ท) +o ๐ธ)) โ ๐ถ โ ๐ด) |
33 | | omeulem2 8534 |
. . . . . . . . . 10
โข (((๐ด โ On โง ๐ด โ โ
) โง (๐ท โ On โง ๐ธ โ ๐ด) โง (๐ต โ On โง ๐ถ โ ๐ด)) โ ((๐ท โ ๐ต โจ (๐ท = ๐ต โง ๐ธ โ ๐ถ)) โ ((๐ด ยทo ๐ท) +o ๐ธ) โ ((๐ด ยทo ๐ต) +o ๐ถ))) |
34 | 10, 31, 4, 13, 1, 32, 33 | syl222anc 1387 |
. . . . . . . . 9
โข ((((๐ด โ On โง ๐ด โ โ
) โง (๐ต โ On โง ๐ถ โ ๐ด) โง (๐ท โ On โง ๐ธ โ ๐ด)) โง ((๐ด ยทo ๐ต) +o ๐ถ) = ((๐ด ยทo ๐ท) +o ๐ธ)) โ ((๐ท โ ๐ต โจ (๐ท = ๐ต โง ๐ธ โ ๐ถ)) โ ((๐ด ยทo ๐ท) +o ๐ธ) โ ((๐ด ยทo ๐ต) +o ๐ถ))) |
35 | 30, 34 | syl5 34 |
. . . . . . . 8
โข ((((๐ด โ On โง ๐ด โ โ
) โง (๐ต โ On โง ๐ถ โ ๐ด) โง (๐ท โ On โง ๐ธ โ ๐ด)) โง ((๐ด ยทo ๐ต) +o ๐ถ) = ((๐ด ยทo ๐ท) +o ๐ธ)) โ (๐ท โ ๐ต โ ((๐ด ยทo ๐ท) +o ๐ธ) โ ((๐ด ยทo ๐ต) +o ๐ถ))) |
36 | 29, 35 | mtod 197 |
. . . . . . 7
โข ((((๐ด โ On โง ๐ด โ โ
) โง (๐ต โ On โง ๐ถ โ ๐ด) โง (๐ท โ On โง ๐ธ โ ๐ด)) โง ((๐ด ยทo ๐ต) +o ๐ถ) = ((๐ด ยทo ๐ท) +o ๐ธ)) โ ยฌ ๐ท โ ๐ต) |
37 | 36 | pm2.21d 121 |
. . . . . 6
โข ((((๐ด โ On โง ๐ด โ โ
) โง (๐ต โ On โง ๐ถ โ ๐ด) โง (๐ท โ On โง ๐ธ โ ๐ด)) โง ((๐ด ยทo ๐ต) +o ๐ถ) = ((๐ด ยทo ๐ท) +o ๐ธ)) โ (๐ท โ ๐ต โ ๐ต = ๐ท)) |
38 | 27, 28, 37 | 3jaod 1429 |
. . . . 5
โข ((((๐ด โ On โง ๐ด โ โ
) โง (๐ต โ On โง ๐ถ โ ๐ด) โง (๐ท โ On โง ๐ธ โ ๐ด)) โง ((๐ด ยทo ๐ต) +o ๐ถ) = ((๐ด ยทo ๐ท) +o ๐ธ)) โ ((๐ต โ ๐ท โจ ๐ต = ๐ท โจ ๐ท โ ๐ต) โ ๐ต = ๐ท)) |
39 | 8, 38 | mpd 15 |
. . . 4
โข ((((๐ด โ On โง ๐ด โ โ
) โง (๐ต โ On โง ๐ถ โ ๐ด) โง (๐ท โ On โง ๐ธ โ ๐ด)) โง ((๐ด ยทo ๐ต) +o ๐ถ) = ((๐ด ยทo ๐ท) +o ๐ธ)) โ ๐ต = ๐ท) |
40 | | onelon 6346 |
. . . . . . . 8
โข ((๐ด โ On โง ๐ถ โ ๐ด) โ ๐ถ โ On) |
41 | | eloni 6331 |
. . . . . . . 8
โข (๐ถ โ On โ Ord ๐ถ) |
42 | 40, 41 | syl 17 |
. . . . . . 7
โข ((๐ด โ On โง ๐ถ โ ๐ด) โ Ord ๐ถ) |
43 | 10, 32, 42 | syl2anc 585 |
. . . . . 6
โข ((((๐ด โ On โง ๐ด โ โ
) โง (๐ต โ On โง ๐ถ โ ๐ด) โง (๐ท โ On โง ๐ธ โ ๐ด)) โง ((๐ด ยทo ๐ต) +o ๐ถ) = ((๐ด ยทo ๐ท) +o ๐ธ)) โ Ord ๐ถ) |
44 | | eloni 6331 |
. . . . . . . 8
โข (๐ธ โ On โ Ord ๐ธ) |
45 | 14, 44 | syl 17 |
. . . . . . 7
โข ((๐ด โ On โง ๐ธ โ ๐ด) โ Ord ๐ธ) |
46 | 10, 13, 45 | syl2anc 585 |
. . . . . 6
โข ((((๐ด โ On โง ๐ด โ โ
) โง (๐ต โ On โง ๐ถ โ ๐ด) โง (๐ท โ On โง ๐ธ โ ๐ด)) โง ((๐ด ยทo ๐ต) +o ๐ถ) = ((๐ด ยทo ๐ท) +o ๐ธ)) โ Ord ๐ธ) |
47 | | ordtri3or 6353 |
. . . . . 6
โข ((Ord
๐ถ โง Ord ๐ธ) โ (๐ถ โ ๐ธ โจ ๐ถ = ๐ธ โจ ๐ธ โ ๐ถ)) |
48 | 43, 46, 47 | syl2anc 585 |
. . . . 5
โข ((((๐ด โ On โง ๐ด โ โ
) โง (๐ต โ On โง ๐ถ โ ๐ด) โง (๐ท โ On โง ๐ธ โ ๐ด)) โง ((๐ด ยทo ๐ต) +o ๐ถ) = ((๐ด ยทo ๐ท) +o ๐ธ)) โ (๐ถ โ ๐ธ โจ ๐ถ = ๐ธ โจ ๐ธ โ ๐ถ)) |
49 | | olc 867 |
. . . . . . . . . 10
โข ((๐ต = ๐ท โง ๐ถ โ ๐ธ) โ (๐ต โ ๐ท โจ (๐ต = ๐ท โง ๐ถ โ ๐ธ))) |
50 | 49, 24 | syl5 34 |
. . . . . . . . 9
โข ((((๐ด โ On โง ๐ด โ โ
) โง (๐ต โ On โง ๐ถ โ ๐ด) โง (๐ท โ On โง ๐ธ โ ๐ด)) โง ((๐ด ยทo ๐ต) +o ๐ถ) = ((๐ด ยทo ๐ท) +o ๐ธ)) โ ((๐ต = ๐ท โง ๐ถ โ ๐ธ) โ ((๐ด ยทo ๐ต) +o ๐ถ) โ ((๐ด ยทo ๐ท) +o ๐ธ))) |
51 | 39, 50 | mpand 694 |
. . . . . . . 8
โข ((((๐ด โ On โง ๐ด โ โ
) โง (๐ต โ On โง ๐ถ โ ๐ด) โง (๐ท โ On โง ๐ธ โ ๐ด)) โง ((๐ด ยทo ๐ต) +o ๐ถ) = ((๐ด ยทo ๐ท) +o ๐ธ)) โ (๐ถ โ ๐ธ โ ((๐ด ยทo ๐ต) +o ๐ถ) โ ((๐ด ยทo ๐ท) +o ๐ธ))) |
52 | 21, 51 | mtod 197 |
. . . . . . 7
โข ((((๐ด โ On โง ๐ด โ โ
) โง (๐ต โ On โง ๐ถ โ ๐ด) โง (๐ท โ On โง ๐ธ โ ๐ด)) โง ((๐ด ยทo ๐ต) +o ๐ถ) = ((๐ด ยทo ๐ท) +o ๐ธ)) โ ยฌ ๐ถ โ ๐ธ) |
53 | 52 | pm2.21d 121 |
. . . . . 6
โข ((((๐ด โ On โง ๐ด โ โ
) โง (๐ต โ On โง ๐ถ โ ๐ด) โง (๐ท โ On โง ๐ธ โ ๐ด)) โง ((๐ด ยทo ๐ต) +o ๐ถ) = ((๐ด ยทo ๐ท) +o ๐ธ)) โ (๐ถ โ ๐ธ โ ๐ถ = ๐ธ)) |
54 | | idd 24 |
. . . . . 6
โข ((((๐ด โ On โง ๐ด โ โ
) โง (๐ต โ On โง ๐ถ โ ๐ด) โง (๐ท โ On โง ๐ธ โ ๐ด)) โง ((๐ด ยทo ๐ต) +o ๐ถ) = ((๐ด ยทo ๐ท) +o ๐ธ)) โ (๐ถ = ๐ธ โ ๐ถ = ๐ธ)) |
55 | 39 | eqcomd 2739 |
. . . . . . . . 9
โข ((((๐ด โ On โง ๐ด โ โ
) โง (๐ต โ On โง ๐ถ โ ๐ด) โง (๐ท โ On โง ๐ธ โ ๐ด)) โง ((๐ด ยทo ๐ต) +o ๐ถ) = ((๐ด ยทo ๐ท) +o ๐ธ)) โ ๐ท = ๐ต) |
56 | | olc 867 |
. . . . . . . . . 10
โข ((๐ท = ๐ต โง ๐ธ โ ๐ถ) โ (๐ท โ ๐ต โจ (๐ท = ๐ต โง ๐ธ โ ๐ถ))) |
57 | 56, 34 | syl5 34 |
. . . . . . . . 9
โข ((((๐ด โ On โง ๐ด โ โ
) โง (๐ต โ On โง ๐ถ โ ๐ด) โง (๐ท โ On โง ๐ธ โ ๐ด)) โง ((๐ด ยทo ๐ต) +o ๐ถ) = ((๐ด ยทo ๐ท) +o ๐ธ)) โ ((๐ท = ๐ต โง ๐ธ โ ๐ถ) โ ((๐ด ยทo ๐ท) +o ๐ธ) โ ((๐ด ยทo ๐ต) +o ๐ถ))) |
58 | 55, 57 | mpand 694 |
. . . . . . . 8
โข ((((๐ด โ On โง ๐ด โ โ
) โง (๐ต โ On โง ๐ถ โ ๐ด) โง (๐ท โ On โง ๐ธ โ ๐ด)) โง ((๐ด ยทo ๐ต) +o ๐ถ) = ((๐ด ยทo ๐ท) +o ๐ธ)) โ (๐ธ โ ๐ถ โ ((๐ด ยทo ๐ท) +o ๐ธ) โ ((๐ด ยทo ๐ต) +o ๐ถ))) |
59 | 29, 58 | mtod 197 |
. . . . . . 7
โข ((((๐ด โ On โง ๐ด โ โ
) โง (๐ต โ On โง ๐ถ โ ๐ด) โง (๐ท โ On โง ๐ธ โ ๐ด)) โง ((๐ด ยทo ๐ต) +o ๐ถ) = ((๐ด ยทo ๐ท) +o ๐ธ)) โ ยฌ ๐ธ โ ๐ถ) |
60 | 59 | pm2.21d 121 |
. . . . . 6
โข ((((๐ด โ On โง ๐ด โ โ
) โง (๐ต โ On โง ๐ถ โ ๐ด) โง (๐ท โ On โง ๐ธ โ ๐ด)) โง ((๐ด ยทo ๐ต) +o ๐ถ) = ((๐ด ยทo ๐ท) +o ๐ธ)) โ (๐ธ โ ๐ถ โ ๐ถ = ๐ธ)) |
61 | 53, 54, 60 | 3jaod 1429 |
. . . . 5
โข ((((๐ด โ On โง ๐ด โ โ
) โง (๐ต โ On โง ๐ถ โ ๐ด) โง (๐ท โ On โง ๐ธ โ ๐ด)) โง ((๐ด ยทo ๐ต) +o ๐ถ) = ((๐ด ยทo ๐ท) +o ๐ธ)) โ ((๐ถ โ ๐ธ โจ ๐ถ = ๐ธ โจ ๐ธ โ ๐ถ) โ ๐ถ = ๐ธ)) |
62 | 48, 61 | mpd 15 |
. . . 4
โข ((((๐ด โ On โง ๐ด โ โ
) โง (๐ต โ On โง ๐ถ โ ๐ด) โง (๐ท โ On โง ๐ธ โ ๐ด)) โง ((๐ด ยทo ๐ต) +o ๐ถ) = ((๐ด ยทo ๐ท) +o ๐ธ)) โ ๐ถ = ๐ธ) |
63 | 39, 62 | jca 513 |
. . 3
โข ((((๐ด โ On โง ๐ด โ โ
) โง (๐ต โ On โง ๐ถ โ ๐ด) โง (๐ท โ On โง ๐ธ โ ๐ด)) โง ((๐ด ยทo ๐ต) +o ๐ถ) = ((๐ด ยทo ๐ท) +o ๐ธ)) โ (๐ต = ๐ท โง ๐ถ = ๐ธ)) |
64 | 63 | ex 414 |
. 2
โข (((๐ด โ On โง ๐ด โ โ
) โง (๐ต โ On โง ๐ถ โ ๐ด) โง (๐ท โ On โง ๐ธ โ ๐ด)) โ (((๐ด ยทo ๐ต) +o ๐ถ) = ((๐ด ยทo ๐ท) +o ๐ธ) โ (๐ต = ๐ท โง ๐ถ = ๐ธ))) |
65 | | oveq2 7369 |
. . 3
โข (๐ต = ๐ท โ (๐ด ยทo ๐ต) = (๐ด ยทo ๐ท)) |
66 | | id 22 |
. . 3
โข (๐ถ = ๐ธ โ ๐ถ = ๐ธ) |
67 | 65, 66 | oveqan12d 7380 |
. 2
โข ((๐ต = ๐ท โง ๐ถ = ๐ธ) โ ((๐ด ยทo ๐ต) +o ๐ถ) = ((๐ด ยทo ๐ท) +o ๐ธ)) |
68 | 64, 67 | impbid1 224 |
1
โข (((๐ด โ On โง ๐ด โ โ
) โง (๐ต โ On โง ๐ถ โ ๐ด) โง (๐ท โ On โง ๐ธ โ ๐ด)) โ (((๐ด ยทo ๐ต) +o ๐ถ) = ((๐ด ยทo ๐ท) +o ๐ธ) โ (๐ต = ๐ท โง ๐ถ = ๐ธ))) |