Step | Hyp | Ref
| Expression |
1 | | oveq2 7369 |
. . . . 5
โข (๐ฅ = โ
โ (๐ด โo ๐ฅ) = (๐ด โo
โ
)) |
2 | | oveq2 7369 |
. . . . 5
โข (๐ฅ = โ
โ (๐ต โo ๐ฅ) = (๐ต โo
โ
)) |
3 | 1, 2 | sseq12d 3981 |
. . . 4
โข (๐ฅ = โ
โ ((๐ด โo ๐ฅ) โ (๐ต โo ๐ฅ) โ (๐ด โo โ
) โ (๐ต โo
โ
))) |
4 | | oveq2 7369 |
. . . . 5
โข (๐ฅ = ๐ฆ โ (๐ด โo ๐ฅ) = (๐ด โo ๐ฆ)) |
5 | | oveq2 7369 |
. . . . 5
โข (๐ฅ = ๐ฆ โ (๐ต โo ๐ฅ) = (๐ต โo ๐ฆ)) |
6 | 4, 5 | sseq12d 3981 |
. . . 4
โข (๐ฅ = ๐ฆ โ ((๐ด โo ๐ฅ) โ (๐ต โo ๐ฅ) โ (๐ด โo ๐ฆ) โ (๐ต โo ๐ฆ))) |
7 | | oveq2 7369 |
. . . . 5
โข (๐ฅ = suc ๐ฆ โ (๐ด โo ๐ฅ) = (๐ด โo suc ๐ฆ)) |
8 | | oveq2 7369 |
. . . . 5
โข (๐ฅ = suc ๐ฆ โ (๐ต โo ๐ฅ) = (๐ต โo suc ๐ฆ)) |
9 | 7, 8 | sseq12d 3981 |
. . . 4
โข (๐ฅ = suc ๐ฆ โ ((๐ด โo ๐ฅ) โ (๐ต โo ๐ฅ) โ (๐ด โo suc ๐ฆ) โ (๐ต โo suc ๐ฆ))) |
10 | | oveq2 7369 |
. . . . 5
โข (๐ฅ = ๐ถ โ (๐ด โo ๐ฅ) = (๐ด โo ๐ถ)) |
11 | | oveq2 7369 |
. . . . 5
โข (๐ฅ = ๐ถ โ (๐ต โo ๐ฅ) = (๐ต โo ๐ถ)) |
12 | 10, 11 | sseq12d 3981 |
. . . 4
โข (๐ฅ = ๐ถ โ ((๐ด โo ๐ฅ) โ (๐ต โo ๐ฅ) โ (๐ด โo ๐ถ) โ (๐ต โo ๐ถ))) |
13 | | onelon 6346 |
. . . . . . 7
โข ((๐ต โ On โง ๐ด โ ๐ต) โ ๐ด โ On) |
14 | | oe0 8472 |
. . . . . . 7
โข (๐ด โ On โ (๐ด โo โ
) =
1o) |
15 | 13, 14 | syl 17 |
. . . . . 6
โข ((๐ต โ On โง ๐ด โ ๐ต) โ (๐ด โo โ
) =
1o) |
16 | | oe0 8472 |
. . . . . . 7
โข (๐ต โ On โ (๐ต โo โ
) =
1o) |
17 | 16 | adantr 482 |
. . . . . 6
โข ((๐ต โ On โง ๐ด โ ๐ต) โ (๐ต โo โ
) =
1o) |
18 | 15, 17 | eqtr4d 2776 |
. . . . 5
โข ((๐ต โ On โง ๐ด โ ๐ต) โ (๐ด โo โ
) = (๐ต โo
โ
)) |
19 | | eqimss 4004 |
. . . . 5
โข ((๐ด โo โ
) =
(๐ต โo
โ
) โ (๐ด
โo โ
) โ (๐ต โo
โ
)) |
20 | 18, 19 | syl 17 |
. . . 4
โข ((๐ต โ On โง ๐ด โ ๐ต) โ (๐ด โo โ
) โ (๐ต โo
โ
)) |
21 | | simpl 484 |
. . . . . 6
โข ((๐ต โ On โง ๐ด โ ๐ต) โ ๐ต โ On) |
22 | | onelss 6363 |
. . . . . . 7
โข (๐ต โ On โ (๐ด โ ๐ต โ ๐ด โ ๐ต)) |
23 | 22 | imp 408 |
. . . . . 6
โข ((๐ต โ On โง ๐ด โ ๐ต) โ ๐ด โ ๐ต) |
24 | 13, 21, 23 | jca31 516 |
. . . . 5
โข ((๐ต โ On โง ๐ด โ ๐ต) โ ((๐ด โ On โง ๐ต โ On) โง ๐ด โ ๐ต)) |
25 | | oecl 8487 |
. . . . . . . . . . . . . 14
โข ((๐ด โ On โง ๐ฆ โ On) โ (๐ด โo ๐ฆ) โ On) |
26 | 25 | 3adant2 1132 |
. . . . . . . . . . . . 13
โข ((๐ด โ On โง ๐ต โ On โง ๐ฆ โ On) โ (๐ด โo ๐ฆ) โ On) |
27 | | oecl 8487 |
. . . . . . . . . . . . . 14
โข ((๐ต โ On โง ๐ฆ โ On) โ (๐ต โo ๐ฆ) โ On) |
28 | 27 | 3adant1 1131 |
. . . . . . . . . . . . 13
โข ((๐ด โ On โง ๐ต โ On โง ๐ฆ โ On) โ (๐ต โo ๐ฆ) โ On) |
29 | | simp1 1137 |
. . . . . . . . . . . . 13
โข ((๐ด โ On โง ๐ต โ On โง ๐ฆ โ On) โ ๐ด โ On) |
30 | | omwordri 8523 |
. . . . . . . . . . . . 13
โข (((๐ด โo ๐ฆ) โ On โง (๐ต โo ๐ฆ) โ On โง ๐ด โ On) โ ((๐ด โo ๐ฆ) โ (๐ต โo ๐ฆ) โ ((๐ด โo ๐ฆ) ยทo ๐ด) โ ((๐ต โo ๐ฆ) ยทo ๐ด))) |
31 | 26, 28, 29, 30 | syl3anc 1372 |
. . . . . . . . . . . 12
โข ((๐ด โ On โง ๐ต โ On โง ๐ฆ โ On) โ ((๐ด โo ๐ฆ) โ (๐ต โo ๐ฆ) โ ((๐ด โo ๐ฆ) ยทo ๐ด) โ ((๐ต โo ๐ฆ) ยทo ๐ด))) |
32 | 31 | imp 408 |
. . . . . . . . . . 11
โข (((๐ด โ On โง ๐ต โ On โง ๐ฆ โ On) โง (๐ด โo ๐ฆ) โ (๐ต โo ๐ฆ)) โ ((๐ด โo ๐ฆ) ยทo ๐ด) โ ((๐ต โo ๐ฆ) ยทo ๐ด)) |
33 | 32 | adantrl 715 |
. . . . . . . . . 10
โข (((๐ด โ On โง ๐ต โ On โง ๐ฆ โ On) โง (๐ด โ ๐ต โง (๐ด โo ๐ฆ) โ (๐ต โo ๐ฆ))) โ ((๐ด โo ๐ฆ) ยทo ๐ด) โ ((๐ต โo ๐ฆ) ยทo ๐ด)) |
34 | | omwordi 8522 |
. . . . . . . . . . . . 13
โข ((๐ด โ On โง ๐ต โ On โง (๐ต โo ๐ฆ) โ On) โ (๐ด โ ๐ต โ ((๐ต โo ๐ฆ) ยทo ๐ด) โ ((๐ต โo ๐ฆ) ยทo ๐ต))) |
35 | 28, 34 | syld3an3 1410 |
. . . . . . . . . . . 12
โข ((๐ด โ On โง ๐ต โ On โง ๐ฆ โ On) โ (๐ด โ ๐ต โ ((๐ต โo ๐ฆ) ยทo ๐ด) โ ((๐ต โo ๐ฆ) ยทo ๐ต))) |
36 | 35 | imp 408 |
. . . . . . . . . . 11
โข (((๐ด โ On โง ๐ต โ On โง ๐ฆ โ On) โง ๐ด โ ๐ต) โ ((๐ต โo ๐ฆ) ยทo ๐ด) โ ((๐ต โo ๐ฆ) ยทo ๐ต)) |
37 | 36 | adantrr 716 |
. . . . . . . . . 10
โข (((๐ด โ On โง ๐ต โ On โง ๐ฆ โ On) โง (๐ด โ ๐ต โง (๐ด โo ๐ฆ) โ (๐ต โo ๐ฆ))) โ ((๐ต โo ๐ฆ) ยทo ๐ด) โ ((๐ต โo ๐ฆ) ยทo ๐ต)) |
38 | 33, 37 | sstrd 3958 |
. . . . . . . . 9
โข (((๐ด โ On โง ๐ต โ On โง ๐ฆ โ On) โง (๐ด โ ๐ต โง (๐ด โo ๐ฆ) โ (๐ต โo ๐ฆ))) โ ((๐ด โo ๐ฆ) ยทo ๐ด) โ ((๐ต โo ๐ฆ) ยทo ๐ต)) |
39 | | oesuc 8477 |
. . . . . . . . . . 11
โข ((๐ด โ On โง ๐ฆ โ On) โ (๐ด โo suc ๐ฆ) = ((๐ด โo ๐ฆ) ยทo ๐ด)) |
40 | 39 | 3adant2 1132 |
. . . . . . . . . 10
โข ((๐ด โ On โง ๐ต โ On โง ๐ฆ โ On) โ (๐ด โo suc ๐ฆ) = ((๐ด โo ๐ฆ) ยทo ๐ด)) |
41 | 40 | adantr 482 |
. . . . . . . . 9
โข (((๐ด โ On โง ๐ต โ On โง ๐ฆ โ On) โง (๐ด โ ๐ต โง (๐ด โo ๐ฆ) โ (๐ต โo ๐ฆ))) โ (๐ด โo suc ๐ฆ) = ((๐ด โo ๐ฆ) ยทo ๐ด)) |
42 | | oesuc 8477 |
. . . . . . . . . . 11
โข ((๐ต โ On โง ๐ฆ โ On) โ (๐ต โo suc ๐ฆ) = ((๐ต โo ๐ฆ) ยทo ๐ต)) |
43 | 42 | 3adant1 1131 |
. . . . . . . . . 10
โข ((๐ด โ On โง ๐ต โ On โง ๐ฆ โ On) โ (๐ต โo suc ๐ฆ) = ((๐ต โo ๐ฆ) ยทo ๐ต)) |
44 | 43 | adantr 482 |
. . . . . . . . 9
โข (((๐ด โ On โง ๐ต โ On โง ๐ฆ โ On) โง (๐ด โ ๐ต โง (๐ด โo ๐ฆ) โ (๐ต โo ๐ฆ))) โ (๐ต โo suc ๐ฆ) = ((๐ต โo ๐ฆ) ยทo ๐ต)) |
45 | 38, 41, 44 | 3sstr4d 3995 |
. . . . . . . 8
โข (((๐ด โ On โง ๐ต โ On โง ๐ฆ โ On) โง (๐ด โ ๐ต โง (๐ด โo ๐ฆ) โ (๐ต โo ๐ฆ))) โ (๐ด โo suc ๐ฆ) โ (๐ต โo suc ๐ฆ)) |
46 | 45 | exp520 1358 |
. . . . . . 7
โข (๐ด โ On โ (๐ต โ On โ (๐ฆ โ On โ (๐ด โ ๐ต โ ((๐ด โo ๐ฆ) โ (๐ต โo ๐ฆ) โ (๐ด โo suc ๐ฆ) โ (๐ต โo suc ๐ฆ)))))) |
47 | 46 | com3r 87 |
. . . . . 6
โข (๐ฆ โ On โ (๐ด โ On โ (๐ต โ On โ (๐ด โ ๐ต โ ((๐ด โo ๐ฆ) โ (๐ต โo ๐ฆ) โ (๐ด โo suc ๐ฆ) โ (๐ต โo suc ๐ฆ)))))) |
48 | 47 | imp4c 425 |
. . . . 5
โข (๐ฆ โ On โ (((๐ด โ On โง ๐ต โ On) โง ๐ด โ ๐ต) โ ((๐ด โo ๐ฆ) โ (๐ต โo ๐ฆ) โ (๐ด โo suc ๐ฆ) โ (๐ต โo suc ๐ฆ)))) |
49 | 24, 48 | syl5 34 |
. . . 4
โข (๐ฆ โ On โ ((๐ต โ On โง ๐ด โ ๐ต) โ ((๐ด โo ๐ฆ) โ (๐ต โo ๐ฆ) โ (๐ด โo suc ๐ฆ) โ (๐ต โo suc ๐ฆ)))) |
50 | | vex 3451 |
. . . . . . . . . . . 12
โข ๐ฅ โ V |
51 | | limelon 6385 |
. . . . . . . . . . . 12
โข ((๐ฅ โ V โง Lim ๐ฅ) โ ๐ฅ โ On) |
52 | 50, 51 | mpan 689 |
. . . . . . . . . . 11
โข (Lim
๐ฅ โ ๐ฅ โ On) |
53 | | 0ellim 6384 |
. . . . . . . . . . 11
โข (Lim
๐ฅ โ โ
โ
๐ฅ) |
54 | | oe0m1 8471 |
. . . . . . . . . . . 12
โข (๐ฅ โ On โ (โ
โ ๐ฅ โ (โ
โo ๐ฅ) =
โ
)) |
55 | 54 | biimpa 478 |
. . . . . . . . . . 11
โข ((๐ฅ โ On โง โ
โ
๐ฅ) โ (โ
โo ๐ฅ) =
โ
) |
56 | 52, 53, 55 | syl2anc 585 |
. . . . . . . . . 10
โข (Lim
๐ฅ โ (โ
โo ๐ฅ) =
โ
) |
57 | | 0ss 4360 |
. . . . . . . . . 10
โข โ
โ (๐ต
โo ๐ฅ) |
58 | 56, 57 | eqsstrdi 4002 |
. . . . . . . . 9
โข (Lim
๐ฅ โ (โ
โo ๐ฅ)
โ (๐ต
โo ๐ฅ)) |
59 | | oveq1 7368 |
. . . . . . . . . 10
โข (๐ด = โ
โ (๐ด โo ๐ฅ) = (โ
โo
๐ฅ)) |
60 | 59 | sseq1d 3979 |
. . . . . . . . 9
โข (๐ด = โ
โ ((๐ด โo ๐ฅ) โ (๐ต โo ๐ฅ) โ (โ
โo ๐ฅ) โ (๐ต โo ๐ฅ))) |
61 | 58, 60 | imbitrrid 245 |
. . . . . . . 8
โข (๐ด = โ
โ (Lim ๐ฅ โ (๐ด โo ๐ฅ) โ (๐ต โo ๐ฅ))) |
62 | 61 | adantl 483 |
. . . . . . 7
โข (((๐ต โ On โง ๐ด โ ๐ต) โง ๐ด = โ
) โ (Lim ๐ฅ โ (๐ด โo ๐ฅ) โ (๐ต โo ๐ฅ))) |
63 | 62 | a1dd 50 |
. . . . . 6
โข (((๐ต โ On โง ๐ด โ ๐ต) โง ๐ด = โ
) โ (Lim ๐ฅ โ (โ๐ฆ โ ๐ฅ (๐ด โo ๐ฆ) โ (๐ต โo ๐ฆ) โ (๐ด โo ๐ฅ) โ (๐ต โo ๐ฅ)))) |
64 | | ss2iun 4976 |
. . . . . . . 8
โข
(โ๐ฆ โ
๐ฅ (๐ด โo ๐ฆ) โ (๐ต โo ๐ฆ) โ โช
๐ฆ โ ๐ฅ (๐ด โo ๐ฆ) โ โช
๐ฆ โ ๐ฅ (๐ต โo ๐ฆ)) |
65 | | oelim 8484 |
. . . . . . . . . . . 12
โข (((๐ด โ On โง (๐ฅ โ V โง Lim ๐ฅ)) โง โ
โ ๐ด) โ (๐ด โo ๐ฅ) = โช ๐ฆ โ ๐ฅ (๐ด โo ๐ฆ)) |
66 | 50, 65 | mpanlr1 705 |
. . . . . . . . . . 11
โข (((๐ด โ On โง Lim ๐ฅ) โง โ
โ ๐ด) โ (๐ด โo ๐ฅ) = โช ๐ฆ โ ๐ฅ (๐ด โo ๐ฆ)) |
67 | 66 | an32s 651 |
. . . . . . . . . 10
โข (((๐ด โ On โง โ
โ
๐ด) โง Lim ๐ฅ) โ (๐ด โo ๐ฅ) = โช ๐ฆ โ ๐ฅ (๐ด โo ๐ฆ)) |
68 | 67 | adantllr 718 |
. . . . . . . . 9
โข ((((๐ด โ On โง (๐ต โ On โง ๐ด โ ๐ต)) โง โ
โ ๐ด) โง Lim ๐ฅ) โ (๐ด โo ๐ฅ) = โช ๐ฆ โ ๐ฅ (๐ด โo ๐ฆ)) |
69 | 21 | anim1i 616 |
. . . . . . . . . . 11
โข (((๐ต โ On โง ๐ด โ ๐ต) โง Lim ๐ฅ) โ (๐ต โ On โง Lim ๐ฅ)) |
70 | | ne0i 4298 |
. . . . . . . . . . . . . 14
โข (๐ด โ ๐ต โ ๐ต โ โ
) |
71 | | on0eln0 6377 |
. . . . . . . . . . . . . 14
โข (๐ต โ On โ (โ
โ ๐ต โ ๐ต โ โ
)) |
72 | 70, 71 | imbitrrid 245 |
. . . . . . . . . . . . 13
โข (๐ต โ On โ (๐ด โ ๐ต โ โ
โ ๐ต)) |
73 | 72 | imp 408 |
. . . . . . . . . . . 12
โข ((๐ต โ On โง ๐ด โ ๐ต) โ โ
โ ๐ต) |
74 | 73 | adantr 482 |
. . . . . . . . . . 11
โข (((๐ต โ On โง ๐ด โ ๐ต) โง Lim ๐ฅ) โ โ
โ ๐ต) |
75 | | oelim 8484 |
. . . . . . . . . . . 12
โข (((๐ต โ On โง (๐ฅ โ V โง Lim ๐ฅ)) โง โ
โ ๐ต) โ (๐ต โo ๐ฅ) = โช ๐ฆ โ ๐ฅ (๐ต โo ๐ฆ)) |
76 | 50, 75 | mpanlr1 705 |
. . . . . . . . . . 11
โข (((๐ต โ On โง Lim ๐ฅ) โง โ
โ ๐ต) โ (๐ต โo ๐ฅ) = โช ๐ฆ โ ๐ฅ (๐ต โo ๐ฆ)) |
77 | 69, 74, 76 | syl2anc 585 |
. . . . . . . . . 10
โข (((๐ต โ On โง ๐ด โ ๐ต) โง Lim ๐ฅ) โ (๐ต โo ๐ฅ) = โช ๐ฆ โ ๐ฅ (๐ต โo ๐ฆ)) |
78 | 77 | ad4ant24 753 |
. . . . . . . . 9
โข ((((๐ด โ On โง (๐ต โ On โง ๐ด โ ๐ต)) โง โ
โ ๐ด) โง Lim ๐ฅ) โ (๐ต โo ๐ฅ) = โช ๐ฆ โ ๐ฅ (๐ต โo ๐ฆ)) |
79 | 68, 78 | sseq12d 3981 |
. . . . . . . 8
โข ((((๐ด โ On โง (๐ต โ On โง ๐ด โ ๐ต)) โง โ
โ ๐ด) โง Lim ๐ฅ) โ ((๐ด โo ๐ฅ) โ (๐ต โo ๐ฅ) โ โช
๐ฆ โ ๐ฅ (๐ด โo ๐ฆ) โ โช
๐ฆ โ ๐ฅ (๐ต โo ๐ฆ))) |
80 | 64, 79 | imbitrrid 245 |
. . . . . . 7
โข ((((๐ด โ On โง (๐ต โ On โง ๐ด โ ๐ต)) โง โ
โ ๐ด) โง Lim ๐ฅ) โ (โ๐ฆ โ ๐ฅ (๐ด โo ๐ฆ) โ (๐ต โo ๐ฆ) โ (๐ด โo ๐ฅ) โ (๐ต โo ๐ฅ))) |
81 | 80 | ex 414 |
. . . . . 6
โข (((๐ด โ On โง (๐ต โ On โง ๐ด โ ๐ต)) โง โ
โ ๐ด) โ (Lim ๐ฅ โ (โ๐ฆ โ ๐ฅ (๐ด โo ๐ฆ) โ (๐ต โo ๐ฆ) โ (๐ด โo ๐ฅ) โ (๐ต โo ๐ฅ)))) |
82 | 63, 81 | oe0lem 8463 |
. . . . 5
โข ((๐ด โ On โง (๐ต โ On โง ๐ด โ ๐ต)) โ (Lim ๐ฅ โ (โ๐ฆ โ ๐ฅ (๐ด โo ๐ฆ) โ (๐ต โo ๐ฆ) โ (๐ด โo ๐ฅ) โ (๐ต โo ๐ฅ)))) |
83 | 13 | ancri 551 |
. . . . 5
โข ((๐ต โ On โง ๐ด โ ๐ต) โ (๐ด โ On โง (๐ต โ On โง ๐ด โ ๐ต))) |
84 | 82, 83 | syl11 33 |
. . . 4
โข (Lim
๐ฅ โ ((๐ต โ On โง ๐ด โ ๐ต) โ (โ๐ฆ โ ๐ฅ (๐ด โo ๐ฆ) โ (๐ต โo ๐ฆ) โ (๐ด โo ๐ฅ) โ (๐ต โo ๐ฅ)))) |
85 | 3, 6, 9, 12, 20, 49, 84 | tfinds3 7805 |
. . 3
โข (๐ถ โ On โ ((๐ต โ On โง ๐ด โ ๐ต) โ (๐ด โo ๐ถ) โ (๐ต โo ๐ถ))) |
86 | 85 | expd 417 |
. 2
โข (๐ถ โ On โ (๐ต โ On โ (๐ด โ ๐ต โ (๐ด โo ๐ถ) โ (๐ต โo ๐ถ)))) |
87 | 86 | impcom 409 |
1
โข ((๐ต โ On โง ๐ถ โ On) โ (๐ด โ ๐ต โ (๐ด โo ๐ถ) โ (๐ต โo ๐ถ))) |