Step | Hyp | Ref
| Expression |
1 | | oveq2 7369 |
. . . . 5
โข (๐ฅ = suc ๐ด โ (๐ถ โo ๐ฅ) = (๐ถ โo suc ๐ด)) |
2 | 1 | eleq2d 2820 |
. . . 4
โข (๐ฅ = suc ๐ด โ ((๐ถ โo ๐ด) โ (๐ถ โo ๐ฅ) โ (๐ถ โo ๐ด) โ (๐ถ โo suc ๐ด))) |
3 | 2 | imbi2d 341 |
. . 3
โข (๐ฅ = suc ๐ด โ ((๐ถ โ (On โ 2o) โ
(๐ถ โo ๐ด) โ (๐ถ โo ๐ฅ)) โ (๐ถ โ (On โ 2o) โ
(๐ถ โo ๐ด) โ (๐ถ โo suc ๐ด)))) |
4 | | oveq2 7369 |
. . . . 5
โข (๐ฅ = ๐ฆ โ (๐ถ โo ๐ฅ) = (๐ถ โo ๐ฆ)) |
5 | 4 | eleq2d 2820 |
. . . 4
โข (๐ฅ = ๐ฆ โ ((๐ถ โo ๐ด) โ (๐ถ โo ๐ฅ) โ (๐ถ โo ๐ด) โ (๐ถ โo ๐ฆ))) |
6 | 5 | imbi2d 341 |
. . 3
โข (๐ฅ = ๐ฆ โ ((๐ถ โ (On โ 2o) โ
(๐ถ โo ๐ด) โ (๐ถ โo ๐ฅ)) โ (๐ถ โ (On โ 2o) โ
(๐ถ โo ๐ด) โ (๐ถ โo ๐ฆ)))) |
7 | | oveq2 7369 |
. . . . 5
โข (๐ฅ = suc ๐ฆ โ (๐ถ โo ๐ฅ) = (๐ถ โo suc ๐ฆ)) |
8 | 7 | eleq2d 2820 |
. . . 4
โข (๐ฅ = suc ๐ฆ โ ((๐ถ โo ๐ด) โ (๐ถ โo ๐ฅ) โ (๐ถ โo ๐ด) โ (๐ถ โo suc ๐ฆ))) |
9 | 8 | imbi2d 341 |
. . 3
โข (๐ฅ = suc ๐ฆ โ ((๐ถ โ (On โ 2o) โ
(๐ถ โo ๐ด) โ (๐ถ โo ๐ฅ)) โ (๐ถ โ (On โ 2o) โ
(๐ถ โo ๐ด) โ (๐ถ โo suc ๐ฆ)))) |
10 | | oveq2 7369 |
. . . . 5
โข (๐ฅ = ๐ต โ (๐ถ โo ๐ฅ) = (๐ถ โo ๐ต)) |
11 | 10 | eleq2d 2820 |
. . . 4
โข (๐ฅ = ๐ต โ ((๐ถ โo ๐ด) โ (๐ถ โo ๐ฅ) โ (๐ถ โo ๐ด) โ (๐ถ โo ๐ต))) |
12 | 11 | imbi2d 341 |
. . 3
โข (๐ฅ = ๐ต โ ((๐ถ โ (On โ 2o) โ
(๐ถ โo ๐ด) โ (๐ถ โo ๐ฅ)) โ (๐ถ โ (On โ 2o) โ
(๐ถ โo ๐ด) โ (๐ถ โo ๐ต)))) |
13 | | eldifi 4090 |
. . . . . . . 8
โข (๐ถ โ (On โ
2o) โ ๐ถ
โ On) |
14 | | oecl 8487 |
. . . . . . . 8
โข ((๐ถ โ On โง ๐ด โ On) โ (๐ถ โo ๐ด) โ On) |
15 | 13, 14 | sylan 581 |
. . . . . . 7
โข ((๐ถ โ (On โ
2o) โง ๐ด
โ On) โ (๐ถ
โo ๐ด)
โ On) |
16 | | om1 8493 |
. . . . . . 7
โข ((๐ถ โo ๐ด) โ On โ ((๐ถ โo ๐ด) ยทo
1o) = (๐ถ
โo ๐ด)) |
17 | 15, 16 | syl 17 |
. . . . . 6
โข ((๐ถ โ (On โ
2o) โง ๐ด
โ On) โ ((๐ถ
โo ๐ด)
ยทo 1o) = (๐ถ โo ๐ด)) |
18 | | ondif2 8452 |
. . . . . . . . 9
โข (๐ถ โ (On โ
2o) โ (๐ถ
โ On โง 1o โ ๐ถ)) |
19 | 18 | simprbi 498 |
. . . . . . . 8
โข (๐ถ โ (On โ
2o) โ 1o โ ๐ถ) |
20 | 19 | adantr 482 |
. . . . . . 7
โข ((๐ถ โ (On โ
2o) โง ๐ด
โ On) โ 1o โ ๐ถ) |
21 | 13 | adantr 482 |
. . . . . . . 8
โข ((๐ถ โ (On โ
2o) โง ๐ด
โ On) โ ๐ถ โ
On) |
22 | | simpr 486 |
. . . . . . . . 9
โข ((๐ถ โ (On โ
2o) โง ๐ด
โ On) โ ๐ด โ
On) |
23 | | dif20el 8455 |
. . . . . . . . . 10
โข (๐ถ โ (On โ
2o) โ โ
โ ๐ถ) |
24 | 23 | adantr 482 |
. . . . . . . . 9
โข ((๐ถ โ (On โ
2o) โง ๐ด
โ On) โ โ
โ ๐ถ) |
25 | | oen0 8537 |
. . . . . . . . 9
โข (((๐ถ โ On โง ๐ด โ On) โง โ
โ
๐ถ) โ โ
โ
(๐ถ โo ๐ด)) |
26 | 21, 22, 24, 25 | syl21anc 837 |
. . . . . . . 8
โข ((๐ถ โ (On โ
2o) โง ๐ด
โ On) โ โ
โ (๐ถ โo ๐ด)) |
27 | | omordi 8517 |
. . . . . . . 8
โข (((๐ถ โ On โง (๐ถ โo ๐ด) โ On) โง โ
โ (๐ถ
โo ๐ด))
โ (1o โ ๐ถ โ ((๐ถ โo ๐ด) ยทo 1o) โ
((๐ถ โo
๐ด) ยทo
๐ถ))) |
28 | 21, 15, 26, 27 | syl21anc 837 |
. . . . . . 7
โข ((๐ถ โ (On โ
2o) โง ๐ด
โ On) โ (1o โ ๐ถ โ ((๐ถ โo ๐ด) ยทo 1o) โ
((๐ถ โo
๐ด) ยทo
๐ถ))) |
29 | 20, 28 | mpd 15 |
. . . . . 6
โข ((๐ถ โ (On โ
2o) โง ๐ด
โ On) โ ((๐ถ
โo ๐ด)
ยทo 1o) โ ((๐ถ โo ๐ด) ยทo ๐ถ)) |
30 | 17, 29 | eqeltrrd 2835 |
. . . . 5
โข ((๐ถ โ (On โ
2o) โง ๐ด
โ On) โ (๐ถ
โo ๐ด)
โ ((๐ถ
โo ๐ด)
ยทo ๐ถ)) |
31 | | oesuc 8477 |
. . . . . 6
โข ((๐ถ โ On โง ๐ด โ On) โ (๐ถ โo suc ๐ด) = ((๐ถ โo ๐ด) ยทo ๐ถ)) |
32 | 13, 31 | sylan 581 |
. . . . 5
โข ((๐ถ โ (On โ
2o) โง ๐ด
โ On) โ (๐ถ
โo suc ๐ด) =
((๐ถ โo
๐ด) ยทo
๐ถ)) |
33 | 30, 32 | eleqtrrd 2837 |
. . . 4
โข ((๐ถ โ (On โ
2o) โง ๐ด
โ On) โ (๐ถ
โo ๐ด)
โ (๐ถ
โo suc ๐ด)) |
34 | 33 | expcom 415 |
. . 3
โข (๐ด โ On โ (๐ถ โ (On โ
2o) โ (๐ถ
โo ๐ด)
โ (๐ถ
โo suc ๐ด))) |
35 | | oecl 8487 |
. . . . . . . . . . 11
โข ((๐ถ โ On โง ๐ฆ โ On) โ (๐ถ โo ๐ฆ) โ On) |
36 | 13, 35 | sylan 581 |
. . . . . . . . . 10
โข ((๐ถ โ (On โ
2o) โง ๐ฆ
โ On) โ (๐ถ
โo ๐ฆ)
โ On) |
37 | | om1 8493 |
. . . . . . . . . 10
โข ((๐ถ โo ๐ฆ) โ On โ ((๐ถ โo ๐ฆ) ยทo
1o) = (๐ถ
โo ๐ฆ)) |
38 | 36, 37 | syl 17 |
. . . . . . . . 9
โข ((๐ถ โ (On โ
2o) โง ๐ฆ
โ On) โ ((๐ถ
โo ๐ฆ)
ยทo 1o) = (๐ถ โo ๐ฆ)) |
39 | 19 | adantr 482 |
. . . . . . . . . 10
โข ((๐ถ โ (On โ
2o) โง ๐ฆ
โ On) โ 1o โ ๐ถ) |
40 | 13 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ถ โ (On โ
2o) โง ๐ฆ
โ On) โ ๐ถ โ
On) |
41 | | simpr 486 |
. . . . . . . . . . . 12
โข ((๐ถ โ (On โ
2o) โง ๐ฆ
โ On) โ ๐ฆ โ
On) |
42 | 23 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ถ โ (On โ
2o) โง ๐ฆ
โ On) โ โ
โ ๐ถ) |
43 | | oen0 8537 |
. . . . . . . . . . . 12
โข (((๐ถ โ On โง ๐ฆ โ On) โง โ
โ
๐ถ) โ โ
โ
(๐ถ โo ๐ฆ)) |
44 | 40, 41, 42, 43 | syl21anc 837 |
. . . . . . . . . . 11
โข ((๐ถ โ (On โ
2o) โง ๐ฆ
โ On) โ โ
โ (๐ถ โo ๐ฆ)) |
45 | | omordi 8517 |
. . . . . . . . . . 11
โข (((๐ถ โ On โง (๐ถ โo ๐ฆ) โ On) โง โ
โ (๐ถ
โo ๐ฆ))
โ (1o โ ๐ถ โ ((๐ถ โo ๐ฆ) ยทo 1o) โ
((๐ถ โo
๐ฆ) ยทo
๐ถ))) |
46 | 40, 36, 44, 45 | syl21anc 837 |
. . . . . . . . . 10
โข ((๐ถ โ (On โ
2o) โง ๐ฆ
โ On) โ (1o โ ๐ถ โ ((๐ถ โo ๐ฆ) ยทo 1o) โ
((๐ถ โo
๐ฆ) ยทo
๐ถ))) |
47 | 39, 46 | mpd 15 |
. . . . . . . . 9
โข ((๐ถ โ (On โ
2o) โง ๐ฆ
โ On) โ ((๐ถ
โo ๐ฆ)
ยทo 1o) โ ((๐ถ โo ๐ฆ) ยทo ๐ถ)) |
48 | 38, 47 | eqeltrrd 2835 |
. . . . . . . 8
โข ((๐ถ โ (On โ
2o) โง ๐ฆ
โ On) โ (๐ถ
โo ๐ฆ)
โ ((๐ถ
โo ๐ฆ)
ยทo ๐ถ)) |
49 | | oesuc 8477 |
. . . . . . . . 9
โข ((๐ถ โ On โง ๐ฆ โ On) โ (๐ถ โo suc ๐ฆ) = ((๐ถ โo ๐ฆ) ยทo ๐ถ)) |
50 | 13, 49 | sylan 581 |
. . . . . . . 8
โข ((๐ถ โ (On โ
2o) โง ๐ฆ
โ On) โ (๐ถ
โo suc ๐ฆ) =
((๐ถ โo
๐ฆ) ยทo
๐ถ)) |
51 | 48, 50 | eleqtrrd 2837 |
. . . . . . 7
โข ((๐ถ โ (On โ
2o) โง ๐ฆ
โ On) โ (๐ถ
โo ๐ฆ)
โ (๐ถ
โo suc ๐ฆ)) |
52 | | onsuc 7750 |
. . . . . . . . 9
โข (๐ฆ โ On โ suc ๐ฆ โ On) |
53 | | oecl 8487 |
. . . . . . . . 9
โข ((๐ถ โ On โง suc ๐ฆ โ On) โ (๐ถ โo suc ๐ฆ) โ On) |
54 | 13, 52, 53 | syl2an 597 |
. . . . . . . 8
โข ((๐ถ โ (On โ
2o) โง ๐ฆ
โ On) โ (๐ถ
โo suc ๐ฆ)
โ On) |
55 | | ontr1 6367 |
. . . . . . . 8
โข ((๐ถ โo suc ๐ฆ) โ On โ (((๐ถ โo ๐ด) โ (๐ถ โo ๐ฆ) โง (๐ถ โo ๐ฆ) โ (๐ถ โo suc ๐ฆ)) โ (๐ถ โo ๐ด) โ (๐ถ โo suc ๐ฆ))) |
56 | 54, 55 | syl 17 |
. . . . . . 7
โข ((๐ถ โ (On โ
2o) โง ๐ฆ
โ On) โ (((๐ถ
โo ๐ด)
โ (๐ถ
โo ๐ฆ) โง
(๐ถ โo ๐ฆ) โ (๐ถ โo suc ๐ฆ)) โ (๐ถ โo ๐ด) โ (๐ถ โo suc ๐ฆ))) |
57 | 51, 56 | mpan2d 693 |
. . . . . 6
โข ((๐ถ โ (On โ
2o) โง ๐ฆ
โ On) โ ((๐ถ
โo ๐ด)
โ (๐ถ
โo ๐ฆ)
โ (๐ถ
โo ๐ด)
โ (๐ถ
โo suc ๐ฆ))) |
58 | 57 | expcom 415 |
. . . . 5
โข (๐ฆ โ On โ (๐ถ โ (On โ
2o) โ ((๐ถ
โo ๐ด)
โ (๐ถ
โo ๐ฆ)
โ (๐ถ
โo ๐ด)
โ (๐ถ
โo suc ๐ฆ)))) |
59 | 58 | adantr 482 |
. . . 4
โข ((๐ฆ โ On โง ๐ด โ ๐ฆ) โ (๐ถ โ (On โ 2o) โ
((๐ถ โo
๐ด) โ (๐ถ โo ๐ฆ) โ (๐ถ โo ๐ด) โ (๐ถ โo suc ๐ฆ)))) |
60 | 59 | a2d 29 |
. . 3
โข ((๐ฆ โ On โง ๐ด โ ๐ฆ) โ ((๐ถ โ (On โ 2o) โ
(๐ถ โo ๐ด) โ (๐ถ โo ๐ฆ)) โ (๐ถ โ (On โ 2o) โ
(๐ถ โo ๐ด) โ (๐ถ โo suc ๐ฆ)))) |
61 | | bi2.04 389 |
. . . . . 6
โข ((๐ด โ ๐ฆ โ (๐ถ โ (On โ 2o) โ
(๐ถ โo ๐ด) โ (๐ถ โo ๐ฆ))) โ (๐ถ โ (On โ 2o) โ
(๐ด โ ๐ฆ โ (๐ถ โo ๐ด) โ (๐ถ โo ๐ฆ)))) |
62 | 61 | ralbii 3093 |
. . . . 5
โข
(โ๐ฆ โ
๐ฅ (๐ด โ ๐ฆ โ (๐ถ โ (On โ 2o) โ
(๐ถ โo ๐ด) โ (๐ถ โo ๐ฆ))) โ โ๐ฆ โ ๐ฅ (๐ถ โ (On โ 2o) โ
(๐ด โ ๐ฆ โ (๐ถ โo ๐ด) โ (๐ถ โo ๐ฆ)))) |
63 | | r19.21v 3173 |
. . . . 5
โข
(โ๐ฆ โ
๐ฅ (๐ถ โ (On โ 2o) โ
(๐ด โ ๐ฆ โ (๐ถ โo ๐ด) โ (๐ถ โo ๐ฆ))) โ (๐ถ โ (On โ 2o) โ
โ๐ฆ โ ๐ฅ (๐ด โ ๐ฆ โ (๐ถ โo ๐ด) โ (๐ถ โo ๐ฆ)))) |
64 | 62, 63 | bitri 275 |
. . . 4
โข
(โ๐ฆ โ
๐ฅ (๐ด โ ๐ฆ โ (๐ถ โ (On โ 2o) โ
(๐ถ โo ๐ด) โ (๐ถ โo ๐ฆ))) โ (๐ถ โ (On โ 2o) โ
โ๐ฆ โ ๐ฅ (๐ด โ ๐ฆ โ (๐ถ โo ๐ด) โ (๐ถ โo ๐ฆ)))) |
65 | | limsuc 7789 |
. . . . . . . . . 10
โข (Lim
๐ฅ โ (๐ด โ ๐ฅ โ suc ๐ด โ ๐ฅ)) |
66 | 65 | biimpa 478 |
. . . . . . . . 9
โข ((Lim
๐ฅ โง ๐ด โ ๐ฅ) โ suc ๐ด โ ๐ฅ) |
67 | | elex 3465 |
. . . . . . . . . . . . 13
โข (suc
๐ด โ ๐ฅ โ suc ๐ด โ V) |
68 | | sucexb 7743 |
. . . . . . . . . . . . . 14
โข (๐ด โ V โ suc ๐ด โ V) |
69 | | sucidg 6402 |
. . . . . . . . . . . . . 14
โข (๐ด โ V โ ๐ด โ suc ๐ด) |
70 | 68, 69 | sylbir 234 |
. . . . . . . . . . . . 13
โข (suc
๐ด โ V โ ๐ด โ suc ๐ด) |
71 | 67, 70 | syl 17 |
. . . . . . . . . . . 12
โข (suc
๐ด โ ๐ฅ โ ๐ด โ suc ๐ด) |
72 | | eleq2 2823 |
. . . . . . . . . . . . . 14
โข (๐ฆ = suc ๐ด โ (๐ด โ ๐ฆ โ ๐ด โ suc ๐ด)) |
73 | | oveq2 7369 |
. . . . . . . . . . . . . . 15
โข (๐ฆ = suc ๐ด โ (๐ถ โo ๐ฆ) = (๐ถ โo suc ๐ด)) |
74 | 73 | eleq2d 2820 |
. . . . . . . . . . . . . 14
โข (๐ฆ = suc ๐ด โ ((๐ถ โo ๐ด) โ (๐ถ โo ๐ฆ) โ (๐ถ โo ๐ด) โ (๐ถ โo suc ๐ด))) |
75 | 72, 74 | imbi12d 345 |
. . . . . . . . . . . . 13
โข (๐ฆ = suc ๐ด โ ((๐ด โ ๐ฆ โ (๐ถ โo ๐ด) โ (๐ถ โo ๐ฆ)) โ (๐ด โ suc ๐ด โ (๐ถ โo ๐ด) โ (๐ถ โo suc ๐ด)))) |
76 | 75 | rspcv 3579 |
. . . . . . . . . . . 12
โข (suc
๐ด โ ๐ฅ โ (โ๐ฆ โ ๐ฅ (๐ด โ ๐ฆ โ (๐ถ โo ๐ด) โ (๐ถ โo ๐ฆ)) โ (๐ด โ suc ๐ด โ (๐ถ โo ๐ด) โ (๐ถ โo suc ๐ด)))) |
77 | 71, 76 | mpid 44 |
. . . . . . . . . . 11
โข (suc
๐ด โ ๐ฅ โ (โ๐ฆ โ ๐ฅ (๐ด โ ๐ฆ โ (๐ถ โo ๐ด) โ (๐ถ โo ๐ฆ)) โ (๐ถ โo ๐ด) โ (๐ถ โo suc ๐ด))) |
78 | 77 | anc2li 557 |
. . . . . . . . . 10
โข (suc
๐ด โ ๐ฅ โ (โ๐ฆ โ ๐ฅ (๐ด โ ๐ฆ โ (๐ถ โo ๐ด) โ (๐ถ โo ๐ฆ)) โ (suc ๐ด โ ๐ฅ โง (๐ถ โo ๐ด) โ (๐ถ โo suc ๐ด)))) |
79 | 73 | eliuni 4964 |
. . . . . . . . . 10
โข ((suc
๐ด โ ๐ฅ โง (๐ถ โo ๐ด) โ (๐ถ โo suc ๐ด)) โ (๐ถ โo ๐ด) โ โช
๐ฆ โ ๐ฅ (๐ถ โo ๐ฆ)) |
80 | 78, 79 | syl6 35 |
. . . . . . . . 9
โข (suc
๐ด โ ๐ฅ โ (โ๐ฆ โ ๐ฅ (๐ด โ ๐ฆ โ (๐ถ โo ๐ด) โ (๐ถ โo ๐ฆ)) โ (๐ถ โo ๐ด) โ โช
๐ฆ โ ๐ฅ (๐ถ โo ๐ฆ))) |
81 | 66, 80 | syl 17 |
. . . . . . . 8
โข ((Lim
๐ฅ โง ๐ด โ ๐ฅ) โ (โ๐ฆ โ ๐ฅ (๐ด โ ๐ฆ โ (๐ถ โo ๐ด) โ (๐ถ โo ๐ฆ)) โ (๐ถ โo ๐ด) โ โช
๐ฆ โ ๐ฅ (๐ถ โo ๐ฆ))) |
82 | 81 | adantr 482 |
. . . . . . 7
โข (((Lim
๐ฅ โง ๐ด โ ๐ฅ) โง ๐ถ โ (On โ 2o)) โ
(โ๐ฆ โ ๐ฅ (๐ด โ ๐ฆ โ (๐ถ โo ๐ด) โ (๐ถ โo ๐ฆ)) โ (๐ถ โo ๐ด) โ โช
๐ฆ โ ๐ฅ (๐ถ โo ๐ฆ))) |
83 | 13 | adantl 483 |
. . . . . . . . . 10
โข ((Lim
๐ฅ โง ๐ถ โ (On โ 2o)) โ
๐ถ โ
On) |
84 | | simpl 484 |
. . . . . . . . . 10
โข ((Lim
๐ฅ โง ๐ถ โ (On โ 2o)) โ
Lim ๐ฅ) |
85 | 23 | adantl 483 |
. . . . . . . . . 10
โข ((Lim
๐ฅ โง ๐ถ โ (On โ 2o)) โ
โ
โ ๐ถ) |
86 | | vex 3451 |
. . . . . . . . . . 11
โข ๐ฅ โ V |
87 | | oelim 8484 |
. . . . . . . . . . 11
โข (((๐ถ โ On โง (๐ฅ โ V โง Lim ๐ฅ)) โง โ
โ ๐ถ) โ (๐ถ โo ๐ฅ) = โช ๐ฆ โ ๐ฅ (๐ถ โo ๐ฆ)) |
88 | 86, 87 | mpanlr1 705 |
. . . . . . . . . 10
โข (((๐ถ โ On โง Lim ๐ฅ) โง โ
โ ๐ถ) โ (๐ถ โo ๐ฅ) = โช ๐ฆ โ ๐ฅ (๐ถ โo ๐ฆ)) |
89 | 83, 84, 85, 88 | syl21anc 837 |
. . . . . . . . 9
โข ((Lim
๐ฅ โง ๐ถ โ (On โ 2o)) โ
(๐ถ โo ๐ฅ) = โช ๐ฆ โ ๐ฅ (๐ถ โo ๐ฆ)) |
90 | 89 | adantlr 714 |
. . . . . . . 8
โข (((Lim
๐ฅ โง ๐ด โ ๐ฅ) โง ๐ถ โ (On โ 2o)) โ
(๐ถ โo ๐ฅ) = โช ๐ฆ โ ๐ฅ (๐ถ โo ๐ฆ)) |
91 | 90 | eleq2d 2820 |
. . . . . . 7
โข (((Lim
๐ฅ โง ๐ด โ ๐ฅ) โง ๐ถ โ (On โ 2o)) โ
((๐ถ โo
๐ด) โ (๐ถ โo ๐ฅ) โ (๐ถ โo ๐ด) โ โช
๐ฆ โ ๐ฅ (๐ถ โo ๐ฆ))) |
92 | 82, 91 | sylibrd 259 |
. . . . . 6
โข (((Lim
๐ฅ โง ๐ด โ ๐ฅ) โง ๐ถ โ (On โ 2o)) โ
(โ๐ฆ โ ๐ฅ (๐ด โ ๐ฆ โ (๐ถ โo ๐ด) โ (๐ถ โo ๐ฆ)) โ (๐ถ โo ๐ด) โ (๐ถ โo ๐ฅ))) |
93 | 92 | ex 414 |
. . . . 5
โข ((Lim
๐ฅ โง ๐ด โ ๐ฅ) โ (๐ถ โ (On โ 2o) โ
(โ๐ฆ โ ๐ฅ (๐ด โ ๐ฆ โ (๐ถ โo ๐ด) โ (๐ถ โo ๐ฆ)) โ (๐ถ โo ๐ด) โ (๐ถ โo ๐ฅ)))) |
94 | 93 | a2d 29 |
. . . 4
โข ((Lim
๐ฅ โง ๐ด โ ๐ฅ) โ ((๐ถ โ (On โ 2o) โ
โ๐ฆ โ ๐ฅ (๐ด โ ๐ฆ โ (๐ถ โo ๐ด) โ (๐ถ โo ๐ฆ))) โ (๐ถ โ (On โ 2o) โ
(๐ถ โo ๐ด) โ (๐ถ โo ๐ฅ)))) |
95 | 64, 94 | biimtrid 241 |
. . 3
โข ((Lim
๐ฅ โง ๐ด โ ๐ฅ) โ (โ๐ฆ โ ๐ฅ (๐ด โ ๐ฆ โ (๐ถ โ (On โ 2o) โ
(๐ถ โo ๐ด) โ (๐ถ โo ๐ฆ))) โ (๐ถ โ (On โ 2o) โ
(๐ถ โo ๐ด) โ (๐ถ โo ๐ฅ)))) |
96 | 3, 6, 9, 12, 34, 60, 95 | tfindsg2 7802 |
. 2
โข ((๐ต โ On โง ๐ด โ ๐ต) โ (๐ถ โ (On โ 2o) โ
(๐ถ โo ๐ด) โ (๐ถ โo ๐ต))) |
97 | 96 | impancom 453 |
1
โข ((๐ต โ On โง ๐ถ โ (On โ
2o)) โ (๐ด
โ ๐ต โ (๐ถ โo ๐ด) โ (๐ถ โo ๐ต))) |