Step | Hyp | Ref
| Expression |
1 | | oveq2 7369 |
. . . . . 6
โข (๐ฅ = โ
โ (๐ด ยทo ๐ฅ) = (๐ด ยทo
โ
)) |
2 | | oveq2 7369 |
. . . . . 6
โข (๐ฅ = โ
โ (๐ต ยทo ๐ฅ) = (๐ต ยทo
โ
)) |
3 | 1, 2 | sseq12d 3981 |
. . . . 5
โข (๐ฅ = โ
โ ((๐ด ยทo ๐ฅ) โ (๐ต ยทo ๐ฅ) โ (๐ด ยทo โ
) โ
(๐ต ยทo
โ
))) |
4 | | oveq2 7369 |
. . . . . 6
โข (๐ฅ = ๐ฆ โ (๐ด ยทo ๐ฅ) = (๐ด ยทo ๐ฆ)) |
5 | | oveq2 7369 |
. . . . . 6
โข (๐ฅ = ๐ฆ โ (๐ต ยทo ๐ฅ) = (๐ต ยทo ๐ฆ)) |
6 | 4, 5 | sseq12d 3981 |
. . . . 5
โข (๐ฅ = ๐ฆ โ ((๐ด ยทo ๐ฅ) โ (๐ต ยทo ๐ฅ) โ (๐ด ยทo ๐ฆ) โ (๐ต ยทo ๐ฆ))) |
7 | | oveq2 7369 |
. . . . . 6
โข (๐ฅ = suc ๐ฆ โ (๐ด ยทo ๐ฅ) = (๐ด ยทo suc ๐ฆ)) |
8 | | oveq2 7369 |
. . . . . 6
โข (๐ฅ = suc ๐ฆ โ (๐ต ยทo ๐ฅ) = (๐ต ยทo suc ๐ฆ)) |
9 | 7, 8 | sseq12d 3981 |
. . . . 5
โข (๐ฅ = suc ๐ฆ โ ((๐ด ยทo ๐ฅ) โ (๐ต ยทo ๐ฅ) โ (๐ด ยทo suc ๐ฆ) โ (๐ต ยทo suc ๐ฆ))) |
10 | | oveq2 7369 |
. . . . . 6
โข (๐ฅ = ๐ถ โ (๐ด ยทo ๐ฅ) = (๐ด ยทo ๐ถ)) |
11 | | oveq2 7369 |
. . . . . 6
โข (๐ฅ = ๐ถ โ (๐ต ยทo ๐ฅ) = (๐ต ยทo ๐ถ)) |
12 | 10, 11 | sseq12d 3981 |
. . . . 5
โข (๐ฅ = ๐ถ โ ((๐ด ยทo ๐ฅ) โ (๐ต ยทo ๐ฅ) โ (๐ด ยทo ๐ถ) โ (๐ต ยทo ๐ถ))) |
13 | | om0 8467 |
. . . . . . 7
โข (๐ด โ On โ (๐ด ยทo โ
) =
โ
) |
14 | | 0ss 4360 |
. . . . . . 7
โข โ
โ (๐ต
ยทo โ
) |
15 | 13, 14 | eqsstrdi 4002 |
. . . . . 6
โข (๐ด โ On โ (๐ด ยทo โ
)
โ (๐ต
ยทo โ
)) |
16 | 15 | ad2antrr 725 |
. . . . 5
โข (((๐ด โ On โง ๐ต โ On) โง ๐ด โ ๐ต) โ (๐ด ยทo โ
) โ
(๐ต ยทo
โ
)) |
17 | | omcl 8486 |
. . . . . . . . . . . . . 14
โข ((๐ด โ On โง ๐ฆ โ On) โ (๐ด ยทo ๐ฆ) โ On) |
18 | 17 | 3adant2 1132 |
. . . . . . . . . . . . 13
โข ((๐ด โ On โง ๐ต โ On โง ๐ฆ โ On) โ (๐ด ยทo ๐ฆ) โ On) |
19 | | omcl 8486 |
. . . . . . . . . . . . . 14
โข ((๐ต โ On โง ๐ฆ โ On) โ (๐ต ยทo ๐ฆ) โ On) |
20 | 19 | 3adant1 1131 |
. . . . . . . . . . . . 13
โข ((๐ด โ On โง ๐ต โ On โง ๐ฆ โ On) โ (๐ต ยทo ๐ฆ) โ On) |
21 | | simp1 1137 |
. . . . . . . . . . . . 13
โข ((๐ด โ On โง ๐ต โ On โง ๐ฆ โ On) โ ๐ด โ On) |
22 | | oawordri 8501 |
. . . . . . . . . . . . 13
โข (((๐ด ยทo ๐ฆ) โ On โง (๐ต ยทo ๐ฆ) โ On โง ๐ด โ On) โ ((๐ด ยทo ๐ฆ) โ (๐ต ยทo ๐ฆ) โ ((๐ด ยทo ๐ฆ) +o ๐ด) โ ((๐ต ยทo ๐ฆ) +o ๐ด))) |
23 | 18, 20, 21, 22 | syl3anc 1372 |
. . . . . . . . . . . 12
โข ((๐ด โ On โง ๐ต โ On โง ๐ฆ โ On) โ ((๐ด ยทo ๐ฆ) โ (๐ต ยทo ๐ฆ) โ ((๐ด ยทo ๐ฆ) +o ๐ด) โ ((๐ต ยทo ๐ฆ) +o ๐ด))) |
24 | 23 | imp 408 |
. . . . . . . . . . 11
โข (((๐ด โ On โง ๐ต โ On โง ๐ฆ โ On) โง (๐ด ยทo ๐ฆ) โ (๐ต ยทo ๐ฆ)) โ ((๐ด ยทo ๐ฆ) +o ๐ด) โ ((๐ต ยทo ๐ฆ) +o ๐ด)) |
25 | 24 | adantrl 715 |
. . . . . . . . . 10
โข (((๐ด โ On โง ๐ต โ On โง ๐ฆ โ On) โง (๐ด โ ๐ต โง (๐ด ยทo ๐ฆ) โ (๐ต ยทo ๐ฆ))) โ ((๐ด ยทo ๐ฆ) +o ๐ด) โ ((๐ต ยทo ๐ฆ) +o ๐ด)) |
26 | | oaword 8500 |
. . . . . . . . . . . . 13
โข ((๐ด โ On โง ๐ต โ On โง (๐ต ยทo ๐ฆ) โ On) โ (๐ด โ ๐ต โ ((๐ต ยทo ๐ฆ) +o ๐ด) โ ((๐ต ยทo ๐ฆ) +o ๐ต))) |
27 | 20, 26 | syld3an3 1410 |
. . . . . . . . . . . 12
โข ((๐ด โ On โง ๐ต โ On โง ๐ฆ โ On) โ (๐ด โ ๐ต โ ((๐ต ยทo ๐ฆ) +o ๐ด) โ ((๐ต ยทo ๐ฆ) +o ๐ต))) |
28 | 27 | biimpa 478 |
. . . . . . . . . . 11
โข (((๐ด โ On โง ๐ต โ On โง ๐ฆ โ On) โง ๐ด โ ๐ต) โ ((๐ต ยทo ๐ฆ) +o ๐ด) โ ((๐ต ยทo ๐ฆ) +o ๐ต)) |
29 | 28 | adantrr 716 |
. . . . . . . . . 10
โข (((๐ด โ On โง ๐ต โ On โง ๐ฆ โ On) โง (๐ด โ ๐ต โง (๐ด ยทo ๐ฆ) โ (๐ต ยทo ๐ฆ))) โ ((๐ต ยทo ๐ฆ) +o ๐ด) โ ((๐ต ยทo ๐ฆ) +o ๐ต)) |
30 | 25, 29 | sstrd 3958 |
. . . . . . . . 9
โข (((๐ด โ On โง ๐ต โ On โง ๐ฆ โ On) โง (๐ด โ ๐ต โง (๐ด ยทo ๐ฆ) โ (๐ต ยทo ๐ฆ))) โ ((๐ด ยทo ๐ฆ) +o ๐ด) โ ((๐ต ยทo ๐ฆ) +o ๐ต)) |
31 | | omsuc 8476 |
. . . . . . . . . . 11
โข ((๐ด โ On โง ๐ฆ โ On) โ (๐ด ยทo suc ๐ฆ) = ((๐ด ยทo ๐ฆ) +o ๐ด)) |
32 | 31 | 3adant2 1132 |
. . . . . . . . . 10
โข ((๐ด โ On โง ๐ต โ On โง ๐ฆ โ On) โ (๐ด ยทo suc ๐ฆ) = ((๐ด ยทo ๐ฆ) +o ๐ด)) |
33 | 32 | adantr 482 |
. . . . . . . . 9
โข (((๐ด โ On โง ๐ต โ On โง ๐ฆ โ On) โง (๐ด โ ๐ต โง (๐ด ยทo ๐ฆ) โ (๐ต ยทo ๐ฆ))) โ (๐ด ยทo suc ๐ฆ) = ((๐ด ยทo ๐ฆ) +o ๐ด)) |
34 | | omsuc 8476 |
. . . . . . . . . . 11
โข ((๐ต โ On โง ๐ฆ โ On) โ (๐ต ยทo suc ๐ฆ) = ((๐ต ยทo ๐ฆ) +o ๐ต)) |
35 | 34 | 3adant1 1131 |
. . . . . . . . . 10
โข ((๐ด โ On โง ๐ต โ On โง ๐ฆ โ On) โ (๐ต ยทo suc ๐ฆ) = ((๐ต ยทo ๐ฆ) +o ๐ต)) |
36 | 35 | adantr 482 |
. . . . . . . . 9
โข (((๐ด โ On โง ๐ต โ On โง ๐ฆ โ On) โง (๐ด โ ๐ต โง (๐ด ยทo ๐ฆ) โ (๐ต ยทo ๐ฆ))) โ (๐ต ยทo suc ๐ฆ) = ((๐ต ยทo ๐ฆ) +o ๐ต)) |
37 | 30, 33, 36 | 3sstr4d 3995 |
. . . . . . . 8
โข (((๐ด โ On โง ๐ต โ On โง ๐ฆ โ On) โง (๐ด โ ๐ต โง (๐ด ยทo ๐ฆ) โ (๐ต ยทo ๐ฆ))) โ (๐ด ยทo suc ๐ฆ) โ (๐ต ยทo suc ๐ฆ)) |
38 | 37 | exp520 1358 |
. . . . . . 7
โข (๐ด โ On โ (๐ต โ On โ (๐ฆ โ On โ (๐ด โ ๐ต โ ((๐ด ยทo ๐ฆ) โ (๐ต ยทo ๐ฆ) โ (๐ด ยทo suc ๐ฆ) โ (๐ต ยทo suc ๐ฆ)))))) |
39 | 38 | com3r 87 |
. . . . . 6
โข (๐ฆ โ On โ (๐ด โ On โ (๐ต โ On โ (๐ด โ ๐ต โ ((๐ด ยทo ๐ฆ) โ (๐ต ยทo ๐ฆ) โ (๐ด ยทo suc ๐ฆ) โ (๐ต ยทo suc ๐ฆ)))))) |
40 | 39 | imp4c 425 |
. . . . 5
โข (๐ฆ โ On โ (((๐ด โ On โง ๐ต โ On) โง ๐ด โ ๐ต) โ ((๐ด ยทo ๐ฆ) โ (๐ต ยทo ๐ฆ) โ (๐ด ยทo suc ๐ฆ) โ (๐ต ยทo suc ๐ฆ)))) |
41 | | vex 3451 |
. . . . . . . 8
โข ๐ฅ โ V |
42 | | ss2iun 4976 |
. . . . . . . . . 10
โข
(โ๐ฆ โ
๐ฅ (๐ด ยทo ๐ฆ) โ (๐ต ยทo ๐ฆ) โ โช
๐ฆ โ ๐ฅ (๐ด ยทo ๐ฆ) โ โช
๐ฆ โ ๐ฅ (๐ต ยทo ๐ฆ)) |
43 | | omlim 8483 |
. . . . . . . . . . . 12
โข ((๐ด โ On โง (๐ฅ โ V โง Lim ๐ฅ)) โ (๐ด ยทo ๐ฅ) = โช ๐ฆ โ ๐ฅ (๐ด ยทo ๐ฆ)) |
44 | 43 | ad2ant2rl 748 |
. . . . . . . . . . 11
โข (((๐ด โ On โง (๐ฅ โ V โง Lim ๐ฅ)) โง (๐ต โ On โง (๐ฅ โ V โง Lim ๐ฅ))) โ (๐ด ยทo ๐ฅ) = โช ๐ฆ โ ๐ฅ (๐ด ยทo ๐ฆ)) |
45 | | omlim 8483 |
. . . . . . . . . . . 12
โข ((๐ต โ On โง (๐ฅ โ V โง Lim ๐ฅ)) โ (๐ต ยทo ๐ฅ) = โช ๐ฆ โ ๐ฅ (๐ต ยทo ๐ฆ)) |
46 | 45 | adantl 483 |
. . . . . . . . . . 11
โข (((๐ด โ On โง (๐ฅ โ V โง Lim ๐ฅ)) โง (๐ต โ On โง (๐ฅ โ V โง Lim ๐ฅ))) โ (๐ต ยทo ๐ฅ) = โช ๐ฆ โ ๐ฅ (๐ต ยทo ๐ฆ)) |
47 | 44, 46 | sseq12d 3981 |
. . . . . . . . . 10
โข (((๐ด โ On โง (๐ฅ โ V โง Lim ๐ฅ)) โง (๐ต โ On โง (๐ฅ โ V โง Lim ๐ฅ))) โ ((๐ด ยทo ๐ฅ) โ (๐ต ยทo ๐ฅ) โ โช
๐ฆ โ ๐ฅ (๐ด ยทo ๐ฆ) โ โช
๐ฆ โ ๐ฅ (๐ต ยทo ๐ฆ))) |
48 | 42, 47 | imbitrrid 245 |
. . . . . . . . 9
โข (((๐ด โ On โง (๐ฅ โ V โง Lim ๐ฅ)) โง (๐ต โ On โง (๐ฅ โ V โง Lim ๐ฅ))) โ (โ๐ฆ โ ๐ฅ (๐ด ยทo ๐ฆ) โ (๐ต ยทo ๐ฆ) โ (๐ด ยทo ๐ฅ) โ (๐ต ยทo ๐ฅ))) |
49 | 48 | anandirs 678 |
. . . . . . . 8
โข (((๐ด โ On โง ๐ต โ On) โง (๐ฅ โ V โง Lim ๐ฅ)) โ (โ๐ฆ โ ๐ฅ (๐ด ยทo ๐ฆ) โ (๐ต ยทo ๐ฆ) โ (๐ด ยทo ๐ฅ) โ (๐ต ยทo ๐ฅ))) |
50 | 41, 49 | mpanr1 702 |
. . . . . . 7
โข (((๐ด โ On โง ๐ต โ On) โง Lim ๐ฅ) โ (โ๐ฆ โ ๐ฅ (๐ด ยทo ๐ฆ) โ (๐ต ยทo ๐ฆ) โ (๐ด ยทo ๐ฅ) โ (๐ต ยทo ๐ฅ))) |
51 | 50 | expcom 415 |
. . . . . 6
โข (Lim
๐ฅ โ ((๐ด โ On โง ๐ต โ On) โ
(โ๐ฆ โ ๐ฅ (๐ด ยทo ๐ฆ) โ (๐ต ยทo ๐ฆ) โ (๐ด ยทo ๐ฅ) โ (๐ต ยทo ๐ฅ)))) |
52 | 51 | adantrd 493 |
. . . . 5
โข (Lim
๐ฅ โ (((๐ด โ On โง ๐ต โ On) โง ๐ด โ ๐ต) โ (โ๐ฆ โ ๐ฅ (๐ด ยทo ๐ฆ) โ (๐ต ยทo ๐ฆ) โ (๐ด ยทo ๐ฅ) โ (๐ต ยทo ๐ฅ)))) |
53 | 3, 6, 9, 12, 16, 40, 52 | tfinds3 7805 |
. . . 4
โข (๐ถ โ On โ (((๐ด โ On โง ๐ต โ On) โง ๐ด โ ๐ต) โ (๐ด ยทo ๐ถ) โ (๐ต ยทo ๐ถ))) |
54 | 53 | expd 417 |
. . 3
โข (๐ถ โ On โ ((๐ด โ On โง ๐ต โ On) โ (๐ด โ ๐ต โ (๐ด ยทo ๐ถ) โ (๐ต ยทo ๐ถ)))) |
55 | 54 | 3impib 1117 |
. 2
โข ((๐ถ โ On โง ๐ด โ On โง ๐ต โ On) โ (๐ด โ ๐ต โ (๐ด ยทo ๐ถ) โ (๐ต ยทo ๐ถ))) |
56 | 55 | 3coml 1128 |
1
โข ((๐ด โ On โง ๐ต โ On โง ๐ถ โ On) โ (๐ด โ ๐ต โ (๐ด ยทo ๐ถ) โ (๐ต ยทo ๐ถ))) |