Step | Hyp | Ref
| Expression |
1 | | onelon 6388 |
. . . 4
โข ((๐ต โ On โง ๐ด โ ๐ต) โ ๐ด โ On) |
2 | 1 | ex 411 |
. . 3
โข (๐ต โ On โ (๐ด โ ๐ต โ ๐ด โ On)) |
3 | 2 | adantr 479 |
. 2
โข ((๐ต โ On โง ๐ถ โ On) โ (๐ด โ ๐ต โ ๐ด โ On)) |
4 | | oewordri 8594 |
. . . . . . . . . . 11
โข ((๐ต โ On โง ๐ถ โ On) โ (๐ด โ ๐ต โ (๐ด โo ๐ถ) โ (๐ต โo ๐ถ))) |
5 | 4 | 3adant1 1128 |
. . . . . . . . . 10
โข ((๐ด โ On โง ๐ต โ On โง ๐ถ โ On) โ (๐ด โ ๐ต โ (๐ด โo ๐ถ) โ (๐ต โo ๐ถ))) |
6 | | oecl 8539 |
. . . . . . . . . . . 12
โข ((๐ด โ On โง ๐ถ โ On) โ (๐ด โo ๐ถ) โ On) |
7 | 6 | 3adant2 1129 |
. . . . . . . . . . 11
โข ((๐ด โ On โง ๐ต โ On โง ๐ถ โ On) โ (๐ด โo ๐ถ) โ On) |
8 | | oecl 8539 |
. . . . . . . . . . . 12
โข ((๐ต โ On โง ๐ถ โ On) โ (๐ต โo ๐ถ) โ On) |
9 | 8 | 3adant1 1128 |
. . . . . . . . . . 11
โข ((๐ด โ On โง ๐ต โ On โง ๐ถ โ On) โ (๐ต โo ๐ถ) โ On) |
10 | | simp1 1134 |
. . . . . . . . . . 11
โข ((๐ด โ On โง ๐ต โ On โง ๐ถ โ On) โ ๐ด โ On) |
11 | | omwordri 8574 |
. . . . . . . . . . 11
โข (((๐ด โo ๐ถ) โ On โง (๐ต โo ๐ถ) โ On โง ๐ด โ On) โ ((๐ด โo ๐ถ) โ (๐ต โo ๐ถ) โ ((๐ด โo ๐ถ) ยทo ๐ด) โ ((๐ต โo ๐ถ) ยทo ๐ด))) |
12 | 7, 9, 10, 11 | syl3anc 1369 |
. . . . . . . . . 10
โข ((๐ด โ On โง ๐ต โ On โง ๐ถ โ On) โ ((๐ด โo ๐ถ) โ (๐ต โo ๐ถ) โ ((๐ด โo ๐ถ) ยทo ๐ด) โ ((๐ต โo ๐ถ) ยทo ๐ด))) |
13 | 5, 12 | syld 47 |
. . . . . . . . 9
โข ((๐ด โ On โง ๐ต โ On โง ๐ถ โ On) โ (๐ด โ ๐ต โ ((๐ด โo ๐ถ) ยทo ๐ด) โ ((๐ต โo ๐ถ) ยทo ๐ด))) |
14 | | oesuc 8529 |
. . . . . . . . . . 11
โข ((๐ด โ On โง ๐ถ โ On) โ (๐ด โo suc ๐ถ) = ((๐ด โo ๐ถ) ยทo ๐ด)) |
15 | 14 | 3adant2 1129 |
. . . . . . . . . 10
โข ((๐ด โ On โง ๐ต โ On โง ๐ถ โ On) โ (๐ด โo suc ๐ถ) = ((๐ด โo ๐ถ) ยทo ๐ด)) |
16 | 15 | sseq1d 4012 |
. . . . . . . . 9
โข ((๐ด โ On โง ๐ต โ On โง ๐ถ โ On) โ ((๐ด โo suc ๐ถ) โ ((๐ต โo ๐ถ) ยทo ๐ด) โ ((๐ด โo ๐ถ) ยทo ๐ด) โ ((๐ต โo ๐ถ) ยทo ๐ด))) |
17 | 13, 16 | sylibrd 258 |
. . . . . . . 8
โข ((๐ด โ On โง ๐ต โ On โง ๐ถ โ On) โ (๐ด โ ๐ต โ (๐ด โo suc ๐ถ) โ ((๐ต โo ๐ถ) ยทo ๐ด))) |
18 | | ne0i 4333 |
. . . . . . . . . . . . . 14
โข (๐ด โ ๐ต โ ๐ต โ โ
) |
19 | | on0eln0 6419 |
. . . . . . . . . . . . . 14
โข (๐ต โ On โ (โ
โ ๐ต โ ๐ต โ โ
)) |
20 | 18, 19 | imbitrrid 245 |
. . . . . . . . . . . . 13
โข (๐ต โ On โ (๐ด โ ๐ต โ โ
โ ๐ต)) |
21 | 20 | adantr 479 |
. . . . . . . . . . . 12
โข ((๐ต โ On โง ๐ถ โ On) โ (๐ด โ ๐ต โ โ
โ ๐ต)) |
22 | | oen0 8588 |
. . . . . . . . . . . . 13
โข (((๐ต โ On โง ๐ถ โ On) โง โ
โ
๐ต) โ โ
โ
(๐ต โo ๐ถ)) |
23 | 22 | ex 411 |
. . . . . . . . . . . 12
โข ((๐ต โ On โง ๐ถ โ On) โ (โ
โ ๐ต โ โ
โ (๐ต
โo ๐ถ))) |
24 | 21, 23 | syld 47 |
. . . . . . . . . . 11
โข ((๐ต โ On โง ๐ถ โ On) โ (๐ด โ ๐ต โ โ
โ (๐ต โo ๐ถ))) |
25 | | omordi 8568 |
. . . . . . . . . . . . . 14
โข (((๐ต โ On โง (๐ต โo ๐ถ) โ On) โง โ
โ (๐ต
โo ๐ถ))
โ (๐ด โ ๐ต โ ((๐ต โo ๐ถ) ยทo ๐ด) โ ((๐ต โo ๐ถ) ยทo ๐ต))) |
26 | 8, 25 | syldanl 600 |
. . . . . . . . . . . . 13
โข (((๐ต โ On โง ๐ถ โ On) โง โ
โ
(๐ต โo ๐ถ)) โ (๐ด โ ๐ต โ ((๐ต โo ๐ถ) ยทo ๐ด) โ ((๐ต โo ๐ถ) ยทo ๐ต))) |
27 | 26 | ex 411 |
. . . . . . . . . . . 12
โข ((๐ต โ On โง ๐ถ โ On) โ (โ
โ (๐ต
โo ๐ถ)
โ (๐ด โ ๐ต โ ((๐ต โo ๐ถ) ยทo ๐ด) โ ((๐ต โo ๐ถ) ยทo ๐ต)))) |
28 | 27 | com23 86 |
. . . . . . . . . . 11
โข ((๐ต โ On โง ๐ถ โ On) โ (๐ด โ ๐ต โ (โ
โ (๐ต โo ๐ถ) โ ((๐ต โo ๐ถ) ยทo ๐ด) โ ((๐ต โo ๐ถ) ยทo ๐ต)))) |
29 | 24, 28 | mpdd 43 |
. . . . . . . . . 10
โข ((๐ต โ On โง ๐ถ โ On) โ (๐ด โ ๐ต โ ((๐ต โo ๐ถ) ยทo ๐ด) โ ((๐ต โo ๐ถ) ยทo ๐ต))) |
30 | 29 | 3adant1 1128 |
. . . . . . . . 9
โข ((๐ด โ On โง ๐ต โ On โง ๐ถ โ On) โ (๐ด โ ๐ต โ ((๐ต โo ๐ถ) ยทo ๐ด) โ ((๐ต โo ๐ถ) ยทo ๐ต))) |
31 | | oesuc 8529 |
. . . . . . . . . . 11
โข ((๐ต โ On โง ๐ถ โ On) โ (๐ต โo suc ๐ถ) = ((๐ต โo ๐ถ) ยทo ๐ต)) |
32 | 31 | 3adant1 1128 |
. . . . . . . . . 10
โข ((๐ด โ On โง ๐ต โ On โง ๐ถ โ On) โ (๐ต โo suc ๐ถ) = ((๐ต โo ๐ถ) ยทo ๐ต)) |
33 | 32 | eleq2d 2817 |
. . . . . . . . 9
โข ((๐ด โ On โง ๐ต โ On โง ๐ถ โ On) โ (((๐ต โo ๐ถ) ยทo ๐ด) โ (๐ต โo suc ๐ถ) โ ((๐ต โo ๐ถ) ยทo ๐ด) โ ((๐ต โo ๐ถ) ยทo ๐ต))) |
34 | 30, 33 | sylibrd 258 |
. . . . . . . 8
โข ((๐ด โ On โง ๐ต โ On โง ๐ถ โ On) โ (๐ด โ ๐ต โ ((๐ต โo ๐ถ) ยทo ๐ด) โ (๐ต โo suc ๐ถ))) |
35 | 17, 34 | jcad 511 |
. . . . . . 7
โข ((๐ด โ On โง ๐ต โ On โง ๐ถ โ On) โ (๐ด โ ๐ต โ ((๐ด โo suc ๐ถ) โ ((๐ต โo ๐ถ) ยทo ๐ด) โง ((๐ต โo ๐ถ) ยทo ๐ด) โ (๐ต โo suc ๐ถ)))) |
36 | 35 | 3expa 1116 |
. . . . . 6
โข (((๐ด โ On โง ๐ต โ On) โง ๐ถ โ On) โ (๐ด โ ๐ต โ ((๐ด โo suc ๐ถ) โ ((๐ต โo ๐ถ) ยทo ๐ด) โง ((๐ต โo ๐ถ) ยทo ๐ด) โ (๐ต โo suc ๐ถ)))) |
37 | | onsucb 7807 |
. . . . . . 7
โข (๐ถ โ On โ suc ๐ถ โ On) |
38 | | oecl 8539 |
. . . . . . . . 9
โข ((๐ด โ On โง suc ๐ถ โ On) โ (๐ด โo suc ๐ถ) โ On) |
39 | | oecl 8539 |
. . . . . . . . 9
โข ((๐ต โ On โง suc ๐ถ โ On) โ (๐ต โo suc ๐ถ) โ On) |
40 | | ontr2 6410 |
. . . . . . . . 9
โข (((๐ด โo suc ๐ถ) โ On โง (๐ต โo suc ๐ถ) โ On) โ (((๐ด โo suc ๐ถ) โ ((๐ต โo ๐ถ) ยทo ๐ด) โง ((๐ต โo ๐ถ) ยทo ๐ด) โ (๐ต โo suc ๐ถ)) โ (๐ด โo suc ๐ถ) โ (๐ต โo suc ๐ถ))) |
41 | 38, 39, 40 | syl2an 594 |
. . . . . . . 8
โข (((๐ด โ On โง suc ๐ถ โ On) โง (๐ต โ On โง suc ๐ถ โ On)) โ (((๐ด โo suc ๐ถ) โ ((๐ต โo ๐ถ) ยทo ๐ด) โง ((๐ต โo ๐ถ) ยทo ๐ด) โ (๐ต โo suc ๐ถ)) โ (๐ด โo suc ๐ถ) โ (๐ต โo suc ๐ถ))) |
42 | 41 | anandirs 675 |
. . . . . . 7
โข (((๐ด โ On โง ๐ต โ On) โง suc ๐ถ โ On) โ (((๐ด โo suc ๐ถ) โ ((๐ต โo ๐ถ) ยทo ๐ด) โง ((๐ต โo ๐ถ) ยทo ๐ด) โ (๐ต โo suc ๐ถ)) โ (๐ด โo suc ๐ถ) โ (๐ต โo suc ๐ถ))) |
43 | 37, 42 | sylan2b 592 |
. . . . . 6
โข (((๐ด โ On โง ๐ต โ On) โง ๐ถ โ On) โ (((๐ด โo suc ๐ถ) โ ((๐ต โo ๐ถ) ยทo ๐ด) โง ((๐ต โo ๐ถ) ยทo ๐ด) โ (๐ต โo suc ๐ถ)) โ (๐ด โo suc ๐ถ) โ (๐ต โo suc ๐ถ))) |
44 | 36, 43 | syld 47 |
. . . . 5
โข (((๐ด โ On โง ๐ต โ On) โง ๐ถ โ On) โ (๐ด โ ๐ต โ (๐ด โo suc ๐ถ) โ (๐ต โo suc ๐ถ))) |
45 | 44 | exp31 418 |
. . . 4
โข (๐ด โ On โ (๐ต โ On โ (๐ถ โ On โ (๐ด โ ๐ต โ (๐ด โo suc ๐ถ) โ (๐ต โo suc ๐ถ))))) |
46 | 45 | com4l 92 |
. . 3
โข (๐ต โ On โ (๐ถ โ On โ (๐ด โ ๐ต โ (๐ด โ On โ (๐ด โo suc ๐ถ) โ (๐ต โo suc ๐ถ))))) |
47 | 46 | imp 405 |
. 2
โข ((๐ต โ On โง ๐ถ โ On) โ (๐ด โ ๐ต โ (๐ด โ On โ (๐ด โo suc ๐ถ) โ (๐ต โo suc ๐ถ)))) |
48 | 3, 47 | mpdd 43 |
1
โข ((๐ต โ On โง ๐ถ โ On) โ (๐ด โ ๐ต โ (๐ด โo suc ๐ถ) โ (๐ต โo suc ๐ถ))) |