Step | Hyp | Ref
| Expression |
1 | | oveq2 7369 |
. . . . . . . 8
โข (๐ต = โ
โ (โ
โo ๐ต) =
(โ
โo โ
)) |
2 | | oe0m0 8470 |
. . . . . . . . 9
โข (โ
โo โ
) = 1o |
3 | | 1on 8428 |
. . . . . . . . 9
โข
1o โ On |
4 | 2, 3 | eqeltri 2830 |
. . . . . . . 8
โข (โ
โo โ
) โ On |
5 | 1, 4 | eqeltrdi 2842 |
. . . . . . 7
โข (๐ต = โ
โ (โ
โo ๐ต)
โ On) |
6 | 5 | adantl 483 |
. . . . . 6
โข ((๐ต โ On โง ๐ต = โ
) โ (โ
โo ๐ต)
โ On) |
7 | | oe0m1 8471 |
. . . . . . . . 9
โข (๐ต โ On โ (โ
โ ๐ต โ (โ
โo ๐ต) =
โ
)) |
8 | 7 | biimpa 478 |
. . . . . . . 8
โข ((๐ต โ On โง โ
โ
๐ต) โ (โ
โo ๐ต) =
โ
) |
9 | | 0elon 6375 |
. . . . . . . 8
โข โ
โ On |
10 | 8, 9 | eqeltrdi 2842 |
. . . . . . 7
โข ((๐ต โ On โง โ
โ
๐ต) โ (โ
โo ๐ต)
โ On) |
11 | 10 | adantll 713 |
. . . . . 6
โข (((๐ต โ On โง ๐ต โ On) โง โ
โ
๐ต) โ (โ
โo ๐ต)
โ On) |
12 | 6, 11 | oe0lem 8463 |
. . . . 5
โข ((๐ต โ On โง ๐ต โ On) โ (โ
โo ๐ต)
โ On) |
13 | 12 | anidms 568 |
. . . 4
โข (๐ต โ On โ (โ
โo ๐ต)
โ On) |
14 | | oveq1 7368 |
. . . . 5
โข (๐ด = โ
โ (๐ด โo ๐ต) = (โ
โo
๐ต)) |
15 | 14 | eleq1d 2819 |
. . . 4
โข (๐ด = โ
โ ((๐ด โo ๐ต) โ On โ (โ
โo ๐ต)
โ On)) |
16 | 13, 15 | imbitrrid 245 |
. . 3
โข (๐ด = โ
โ (๐ต โ On โ (๐ด โo ๐ต) โ On)) |
17 | 16 | impcom 409 |
. 2
โข ((๐ต โ On โง ๐ด = โ
) โ (๐ด โo ๐ต) โ On) |
18 | | oveq2 7369 |
. . . . . . 7
โข (๐ฅ = โ
โ (๐ด โo ๐ฅ) = (๐ด โo
โ
)) |
19 | 18 | eleq1d 2819 |
. . . . . 6
โข (๐ฅ = โ
โ ((๐ด โo ๐ฅ) โ On โ (๐ด โo โ
)
โ On)) |
20 | | oveq2 7369 |
. . . . . . 7
โข (๐ฅ = ๐ฆ โ (๐ด โo ๐ฅ) = (๐ด โo ๐ฆ)) |
21 | 20 | eleq1d 2819 |
. . . . . 6
โข (๐ฅ = ๐ฆ โ ((๐ด โo ๐ฅ) โ On โ (๐ด โo ๐ฆ) โ On)) |
22 | | oveq2 7369 |
. . . . . . 7
โข (๐ฅ = suc ๐ฆ โ (๐ด โo ๐ฅ) = (๐ด โo suc ๐ฆ)) |
23 | 22 | eleq1d 2819 |
. . . . . 6
โข (๐ฅ = suc ๐ฆ โ ((๐ด โo ๐ฅ) โ On โ (๐ด โo suc ๐ฆ) โ On)) |
24 | | oveq2 7369 |
. . . . . . 7
โข (๐ฅ = ๐ต โ (๐ด โo ๐ฅ) = (๐ด โo ๐ต)) |
25 | 24 | eleq1d 2819 |
. . . . . 6
โข (๐ฅ = ๐ต โ ((๐ด โo ๐ฅ) โ On โ (๐ด โo ๐ต) โ On)) |
26 | | oe0 8472 |
. . . . . . . 8
โข (๐ด โ On โ (๐ด โo โ
) =
1o) |
27 | 26, 3 | eqeltrdi 2842 |
. . . . . . 7
โข (๐ด โ On โ (๐ด โo โ
)
โ On) |
28 | 27 | adantr 482 |
. . . . . 6
โข ((๐ด โ On โง โ
โ
๐ด) โ (๐ด โo โ
)
โ On) |
29 | | omcl 8486 |
. . . . . . . . . . 11
โข (((๐ด โo ๐ฆ) โ On โง ๐ด โ On) โ ((๐ด โo ๐ฆ) ยทo ๐ด) โ On) |
30 | 29 | expcom 415 |
. . . . . . . . . 10
โข (๐ด โ On โ ((๐ด โo ๐ฆ) โ On โ ((๐ด โo ๐ฆ) ยทo ๐ด) โ On)) |
31 | 30 | adantr 482 |
. . . . . . . . 9
โข ((๐ด โ On โง ๐ฆ โ On) โ ((๐ด โo ๐ฆ) โ On โ ((๐ด โo ๐ฆ) ยทo ๐ด) โ On)) |
32 | | oesuc 8477 |
. . . . . . . . . 10
โข ((๐ด โ On โง ๐ฆ โ On) โ (๐ด โo suc ๐ฆ) = ((๐ด โo ๐ฆ) ยทo ๐ด)) |
33 | 32 | eleq1d 2819 |
. . . . . . . . 9
โข ((๐ด โ On โง ๐ฆ โ On) โ ((๐ด โo suc ๐ฆ) โ On โ ((๐ด โo ๐ฆ) ยทo ๐ด) โ On)) |
34 | 31, 33 | sylibrd 259 |
. . . . . . . 8
โข ((๐ด โ On โง ๐ฆ โ On) โ ((๐ด โo ๐ฆ) โ On โ (๐ด โo suc ๐ฆ) โ On)) |
35 | 34 | expcom 415 |
. . . . . . 7
โข (๐ฆ โ On โ (๐ด โ On โ ((๐ด โo ๐ฆ) โ On โ (๐ด โo suc ๐ฆ) โ On))) |
36 | 35 | adantrd 493 |
. . . . . 6
โข (๐ฆ โ On โ ((๐ด โ On โง โ
โ
๐ด) โ ((๐ด โo ๐ฆ) โ On โ (๐ด โo suc ๐ฆ) โ On))) |
37 | | vex 3451 |
. . . . . . . . 9
โข ๐ฅ โ V |
38 | | iunon 8289 |
. . . . . . . . 9
โข ((๐ฅ โ V โง โ๐ฆ โ ๐ฅ (๐ด โo ๐ฆ) โ On) โ โช ๐ฆ โ ๐ฅ (๐ด โo ๐ฆ) โ On) |
39 | 37, 38 | mpan 689 |
. . . . . . . 8
โข
(โ๐ฆ โ
๐ฅ (๐ด โo ๐ฆ) โ On โ โช ๐ฆ โ ๐ฅ (๐ด โo ๐ฆ) โ On) |
40 | | oelim 8484 |
. . . . . . . . . . . 12
โข (((๐ด โ On โง (๐ฅ โ V โง Lim ๐ฅ)) โง โ
โ ๐ด) โ (๐ด โo ๐ฅ) = โช ๐ฆ โ ๐ฅ (๐ด โo ๐ฆ)) |
41 | 37, 40 | mpanlr1 705 |
. . . . . . . . . . 11
โข (((๐ด โ On โง Lim ๐ฅ) โง โ
โ ๐ด) โ (๐ด โo ๐ฅ) = โช ๐ฆ โ ๐ฅ (๐ด โo ๐ฆ)) |
42 | 41 | anasss 468 |
. . . . . . . . . 10
โข ((๐ด โ On โง (Lim ๐ฅ โง โ
โ ๐ด)) โ (๐ด โo ๐ฅ) = โช ๐ฆ โ ๐ฅ (๐ด โo ๐ฆ)) |
43 | 42 | an12s 648 |
. . . . . . . . 9
โข ((Lim
๐ฅ โง (๐ด โ On โง โ
โ ๐ด)) โ (๐ด โo ๐ฅ) = โช ๐ฆ โ ๐ฅ (๐ด โo ๐ฆ)) |
44 | 43 | eleq1d 2819 |
. . . . . . . 8
โข ((Lim
๐ฅ โง (๐ด โ On โง โ
โ ๐ด)) โ ((๐ด โo ๐ฅ) โ On โ โช ๐ฆ โ ๐ฅ (๐ด โo ๐ฆ) โ On)) |
45 | 39, 44 | imbitrrid 245 |
. . . . . . 7
โข ((Lim
๐ฅ โง (๐ด โ On โง โ
โ ๐ด)) โ (โ๐ฆ โ ๐ฅ (๐ด โo ๐ฆ) โ On โ (๐ด โo ๐ฅ) โ On)) |
46 | 45 | ex 414 |
. . . . . 6
โข (Lim
๐ฅ โ ((๐ด โ On โง โ
โ
๐ด) โ (โ๐ฆ โ ๐ฅ (๐ด โo ๐ฆ) โ On โ (๐ด โo ๐ฅ) โ On))) |
47 | 19, 21, 23, 25, 28, 36, 46 | tfinds3 7805 |
. . . . 5
โข (๐ต โ On โ ((๐ด โ On โง โ
โ
๐ด) โ (๐ด โo ๐ต) โ On)) |
48 | 47 | expd 417 |
. . . 4
โข (๐ต โ On โ (๐ด โ On โ (โ
โ ๐ด โ (๐ด โo ๐ต) โ On))) |
49 | 48 | com12 32 |
. . 3
โข (๐ด โ On โ (๐ต โ On โ (โ
โ ๐ด โ (๐ด โo ๐ต) โ On))) |
50 | 49 | imp31 419 |
. 2
โข (((๐ด โ On โง ๐ต โ On) โง โ
โ
๐ด) โ (๐ด โo ๐ต) โ On) |
51 | 17, 50 | oe0lem 8463 |
1
โข ((๐ด โ On โง ๐ต โ On) โ (๐ด โo ๐ต) โ On) |