Step | Hyp | Ref
| Expression |
1 | | eleq2 2823 |
. . . . . 6
โข (๐ต = โ
โ (๐ด โ ๐ต โ ๐ด โ โ
)) |
2 | | noel 4291 |
. . . . . . 7
โข ยฌ
๐ด โ
โ
|
3 | 2 | pm2.21i 119 |
. . . . . 6
โข (๐ด โ โ
โ (โ
โ ๐ด โ (๐ด ยทo ๐ต) = ๐ต)) |
4 | 1, 3 | syl6bi 253 |
. . . . 5
โข (๐ต = โ
โ (๐ด โ ๐ต โ (โ
โ ๐ด โ (๐ด ยทo ๐ต) = ๐ต))) |
5 | 4 | impd 412 |
. . . 4
โข (๐ต = โ
โ ((๐ด โ ๐ต โง โ
โ ๐ด) โ (๐ด ยทo ๐ต) = ๐ต)) |
6 | 5 | com12 32 |
. . 3
โข ((๐ด โ ๐ต โง โ
โ ๐ด) โ (๐ต = โ
โ (๐ด ยทo ๐ต) = ๐ต)) |
7 | | elpri 4609 |
. . . . . . . . 9
โข (๐ด โ {โ
, 1o}
โ (๐ด = โ
โจ
๐ด =
1o)) |
8 | | eleq2 2823 |
. . . . . . . . . . 11
โข (๐ด = โ
โ (โ
โ ๐ด โ โ
โ โ
)) |
9 | | noel 4291 |
. . . . . . . . . . . 12
โข ยฌ
โ
โ โ
|
10 | 9 | pm2.21i 119 |
. . . . . . . . . . 11
โข (โ
โ โ
โ (๐ด
ยทo 2o) = 2o) |
11 | 8, 10 | syl6bi 253 |
. . . . . . . . . 10
โข (๐ด = โ
โ (โ
โ ๐ด โ (๐ด ยทo
2o) = 2o)) |
12 | | oveq1 7365 |
. . . . . . . . . . . 12
โข (๐ด = 1o โ (๐ด ยทo
2o) = (1o ยทo
2o)) |
13 | | 2on 8427 |
. . . . . . . . . . . . 13
โข
2o โ On |
14 | | om1r 8491 |
. . . . . . . . . . . . 13
โข
(2o โ On โ (1o ยทo
2o) = 2o) |
15 | 13, 14 | ax-mp 5 |
. . . . . . . . . . . 12
โข
(1o ยทo 2o) =
2o |
16 | 12, 15 | eqtrdi 2789 |
. . . . . . . . . . 11
โข (๐ด = 1o โ (๐ด ยทo
2o) = 2o) |
17 | 16 | a1d 25 |
. . . . . . . . . 10
โข (๐ด = 1o โ (โ
โ ๐ด โ (๐ด ยทo
2o) = 2o)) |
18 | 11, 17 | jaoi 856 |
. . . . . . . . 9
โข ((๐ด = โ
โจ ๐ด = 1o) โ
(โ
โ ๐ด โ
(๐ด ยทo
2o) = 2o)) |
19 | 7, 18 | syl 17 |
. . . . . . . 8
โข (๐ด โ {โ
, 1o}
โ (โ
โ ๐ด
โ (๐ด
ยทo 2o) = 2o)) |
20 | | df2o3 8421 |
. . . . . . . 8
โข
2o = {โ
, 1o} |
21 | 19, 20 | eleq2s 2852 |
. . . . . . 7
โข (๐ด โ 2o โ
(โ
โ ๐ด โ
(๐ด ยทo
2o) = 2o)) |
22 | 21 | imp 408 |
. . . . . 6
โข ((๐ด โ 2o โง
โ
โ ๐ด) โ
(๐ด ยทo
2o) = 2o) |
23 | 22 | a1i 11 |
. . . . 5
โข (๐ต = 2o โ ((๐ด โ 2o โง
โ
โ ๐ด) โ
(๐ด ยทo
2o) = 2o)) |
24 | | eleq2 2823 |
. . . . . 6
โข (๐ต = 2o โ (๐ด โ ๐ต โ ๐ด โ 2o)) |
25 | 24 | anbi1d 631 |
. . . . 5
โข (๐ต = 2o โ ((๐ด โ ๐ต โง โ
โ ๐ด) โ (๐ด โ 2o โง โ
โ
๐ด))) |
26 | | oveq2 7366 |
. . . . . 6
โข (๐ต = 2o โ (๐ด ยทo ๐ต) = (๐ด ยทo
2o)) |
27 | | id 22 |
. . . . . 6
โข (๐ต = 2o โ ๐ต =
2o) |
28 | 26, 27 | eqeq12d 2749 |
. . . . 5
โข (๐ต = 2o โ ((๐ด ยทo ๐ต) = ๐ต โ (๐ด ยทo 2o) =
2o)) |
29 | 23, 25, 28 | 3imtr4d 294 |
. . . 4
โข (๐ต = 2o โ ((๐ด โ ๐ต โง โ
โ ๐ด) โ (๐ด ยทo ๐ต) = ๐ต)) |
30 | 29 | com12 32 |
. . 3
โข ((๐ด โ ๐ต โง โ
โ ๐ด) โ (๐ต = 2o โ (๐ด ยทo ๐ต) = ๐ต)) |
31 | | simpr 486 |
. . . . . . 7
โข ((((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
๐ด โ ฯ) โ
๐ด โ
ฯ) |
32 | | simpllr 775 |
. . . . . . 7
โข ((((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
๐ด โ ฯ) โ
โ
โ ๐ด) |
33 | | omelon 9587 |
. . . . . . . . . 10
โข ฯ
โ On |
34 | | oecl 8484 |
. . . . . . . . . 10
โข ((ฯ
โ On โง ๐ถ โ
On) โ (ฯ โo ๐ถ) โ On) |
35 | 33, 34 | mpan 689 |
. . . . . . . . 9
โข (๐ถ โ On โ (ฯ
โo ๐ถ)
โ On) |
36 | 35 | adantl 483 |
. . . . . . . 8
โข ((๐ต = (ฯ โo
(ฯ โo ๐ถ)) โง ๐ถ โ On) โ (ฯ
โo ๐ถ)
โ On) |
37 | 36 | ad2antlr 726 |
. . . . . . 7
โข ((((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
๐ด โ ฯ) โ
(ฯ โo ๐ถ) โ On) |
38 | 33 | jctl 525 |
. . . . . . . . . 10
โข (๐ถ โ On โ (ฯ
โ On โง ๐ถ โ
On)) |
39 | | peano1 7826 |
. . . . . . . . . 10
โข โ
โ ฯ |
40 | | oen0 8534 |
. . . . . . . . . 10
โข
(((ฯ โ On โง ๐ถ โ On) โง โ
โ ฯ)
โ โ
โ (ฯ โo ๐ถ)) |
41 | 38, 39, 40 | sylancl 587 |
. . . . . . . . 9
โข (๐ถ โ On โ โ
โ
(ฯ โo ๐ถ)) |
42 | 41 | adantl 483 |
. . . . . . . 8
โข ((๐ต = (ฯ โo
(ฯ โo ๐ถ)) โง ๐ถ โ On) โ โ
โ (ฯ
โo ๐ถ)) |
43 | 42 | ad2antlr 726 |
. . . . . . 7
โข ((((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
๐ด โ ฯ) โ
โ
โ (ฯ โo ๐ถ)) |
44 | | omabs 8598 |
. . . . . . 7
โข (((๐ด โ ฯ โง โ
โ ๐ด) โง ((ฯ
โo ๐ถ)
โ On โง โ
โ (ฯ โo ๐ถ))) โ (๐ด ยทo (ฯ
โo (ฯ โo ๐ถ))) = (ฯ โo (ฯ
โo ๐ถ))) |
45 | 31, 32, 37, 43, 44 | syl22anc 838 |
. . . . . 6
โข ((((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
๐ด โ ฯ) โ
(๐ด ยทo
(ฯ โo (ฯ โo ๐ถ))) = (ฯ โo (ฯ
โo ๐ถ))) |
46 | | oveq2 7366 |
. . . . . . . . 9
โข (๐ต = (ฯ โo
(ฯ โo ๐ถ)) โ (๐ด ยทo ๐ต) = (๐ด ยทo (ฯ
โo (ฯ โo ๐ถ)))) |
47 | | id 22 |
. . . . . . . . 9
โข (๐ต = (ฯ โo
(ฯ โo ๐ถ)) โ ๐ต = (ฯ โo (ฯ
โo ๐ถ))) |
48 | 46, 47 | eqeq12d 2749 |
. . . . . . . 8
โข (๐ต = (ฯ โo
(ฯ โo ๐ถ)) โ ((๐ด ยทo ๐ต) = ๐ต โ (๐ด ยทo (ฯ
โo (ฯ โo ๐ถ))) = (ฯ โo (ฯ
โo ๐ถ)))) |
49 | 48 | adantr 482 |
. . . . . . 7
โข ((๐ต = (ฯ โo
(ฯ โo ๐ถ)) โง ๐ถ โ On) โ ((๐ด ยทo ๐ต) = ๐ต โ (๐ด ยทo (ฯ
โo (ฯ โo ๐ถ))) = (ฯ โo (ฯ
โo ๐ถ)))) |
50 | 49 | ad2antlr 726 |
. . . . . 6
โข ((((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
๐ด โ ฯ) โ
((๐ด ยทo
๐ต) = ๐ต โ (๐ด ยทo (ฯ
โo (ฯ โo ๐ถ))) = (ฯ โo (ฯ
โo ๐ถ)))) |
51 | 45, 50 | mpbird 257 |
. . . . 5
โข ((((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
๐ด โ ฯ) โ
(๐ด ยทo
๐ต) = ๐ต) |
52 | | simpl 484 |
. . . . . . . . . . . 12
โข ((๐ต = (ฯ โo
(ฯ โo ๐ถ)) โง ๐ถ โ On) โ ๐ต = (ฯ โo (ฯ
โo ๐ถ))) |
53 | | oecl 8484 |
. . . . . . . . . . . . . 14
โข ((ฯ
โ On โง (ฯ โo ๐ถ) โ On) โ (ฯ
โo (ฯ โo ๐ถ)) โ On) |
54 | 33, 35, 53 | sylancr 588 |
. . . . . . . . . . . . 13
โข (๐ถ โ On โ (ฯ
โo (ฯ โo ๐ถ)) โ On) |
55 | 54 | adantl 483 |
. . . . . . . . . . . 12
โข ((๐ต = (ฯ โo
(ฯ โo ๐ถ)) โง ๐ถ โ On) โ (ฯ
โo (ฯ โo ๐ถ)) โ On) |
56 | 52, 55 | eqeltrd 2834 |
. . . . . . . . . . 11
โข ((๐ต = (ฯ โo
(ฯ โo ๐ถ)) โง ๐ถ โ On) โ ๐ต โ On) |
57 | | simpl 484 |
. . . . . . . . . . 11
โข ((๐ด โ ๐ต โง โ
โ ๐ด) โ ๐ด โ ๐ต) |
58 | | onelon 6343 |
. . . . . . . . . . 11
โข ((๐ต โ On โง ๐ด โ ๐ต) โ ๐ด โ On) |
59 | 56, 57, 58 | syl2anr 598 |
. . . . . . . . . 10
โข (((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โ
๐ด โ
On) |
60 | | simplr 768 |
. . . . . . . . . 10
โข (((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โ
โ
โ ๐ด) |
61 | | ondif1 8448 |
. . . . . . . . . 10
โข (๐ด โ (On โ
1o) โ (๐ด
โ On โง โ
โ ๐ด)) |
62 | 59, 60, 61 | sylanbrc 584 |
. . . . . . . . 9
โข (((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โ
๐ด โ (On โ
1o)) |
63 | | 1onn 8587 |
. . . . . . . . . 10
โข
1o โ ฯ |
64 | | ondif2 8449 |
. . . . . . . . . 10
โข (ฯ
โ (On โ 2o) โ (ฯ โ On โง 1o
โ ฯ)) |
65 | 33, 63, 64 | mpbir2an 710 |
. . . . . . . . 9
โข ฯ
โ (On โ 2o) |
66 | 62, 65 | jctil 521 |
. . . . . . . 8
โข (((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โ
(ฯ โ (On โ 2o) โง ๐ด โ (On โ
1o))) |
67 | 66 | adantr 482 |
. . . . . . 7
โข ((((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โ
(ฯ โ (On โ 2o) โง ๐ด โ (On โ
1o))) |
68 | | oeeu 8551 |
. . . . . . 7
โข ((ฯ
โ (On โ 2o) โง ๐ด โ (On โ 1o)) โ
โ!๐คโ๐ฅ โ On โ๐ฆ โ (ฯ โ
1o)โ๐ง
โ (ฯ โo ๐ฅ)(๐ค = โจ๐ฅ, ๐ฆ, ๐งโฉ โง (((ฯ โo
๐ฅ) ยทo
๐ฆ) +o ๐ง) = ๐ด)) |
69 | 67, 68 | syl 17 |
. . . . . 6
โข ((((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โ
โ!๐คโ๐ฅ โ On โ๐ฆ โ (ฯ โ
1o)โ๐ง
โ (ฯ โo ๐ฅ)(๐ค = โจ๐ฅ, ๐ฆ, ๐งโฉ โง (((ฯ โo
๐ฅ) ยทo
๐ฆ) +o ๐ง) = ๐ด)) |
70 | | euex 2572 |
. . . . . . 7
โข
(โ!๐คโ๐ฅ โ On โ๐ฆ โ (ฯ โ
1o)โ๐ง
โ (ฯ โo ๐ฅ)(๐ค = โจ๐ฅ, ๐ฆ, ๐งโฉ โง (((ฯ โo
๐ฅ) ยทo
๐ฆ) +o ๐ง) = ๐ด) โ โ๐คโ๐ฅ โ On โ๐ฆ โ (ฯ โ
1o)โ๐ง
โ (ฯ โo ๐ฅ)(๐ค = โจ๐ฅ, ๐ฆ, ๐งโฉ โง (((ฯ โo
๐ฅ) ยทo
๐ฆ) +o ๐ง) = ๐ด)) |
71 | | simpr 486 |
. . . . . . . . . . . 12
โข ((๐ค = โจ๐ฅ, ๐ฆ, ๐งโฉ โง (((ฯ โo
๐ฅ) ยทo
๐ฆ) +o ๐ง) = ๐ด) โ (((ฯ โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ด) |
72 | | 0ss 4357 |
. . . . . . . . . . . . . . . . . . 19
โข โ
โ ๐ง |
73 | | 0elon 6372 |
. . . . . . . . . . . . . . . . . . . 20
โข โ
โ On |
74 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข
(((((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โง
๐ฅ โ On) โ ๐ฅ โ On) |
75 | | oecl 8484 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((ฯ
โ On โง ๐ฅ โ
On) โ (ฯ โo ๐ฅ) โ On) |
76 | 33, 74, 75 | sylancr 588 |
. . . . . . . . . . . . . . . . . . . . . 22
โข
(((((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โง
๐ฅ โ On) โ
(ฯ โo ๐ฅ) โ On) |
77 | 76 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . 21
โข
(((((((๐ด โ
๐ต โง โ
โ
๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โง
๐ฅ โ On) โง ๐ฆ โ (ฯ โ
1o)) โง ๐ง
โ (ฯ โo ๐ฅ)) โ (ฯ โo ๐ฅ) โ On) |
78 | | onelon 6343 |
. . . . . . . . . . . . . . . . . . . . 21
โข
(((ฯ โo ๐ฅ) โ On โง ๐ง โ (ฯ โo ๐ฅ)) โ ๐ง โ On) |
79 | 77, 78 | sylancom 589 |
. . . . . . . . . . . . . . . . . . . 20
โข
(((((((๐ด โ
๐ต โง โ
โ
๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โง
๐ฅ โ On) โง ๐ฆ โ (ฯ โ
1o)) โง ๐ง
โ (ฯ โo ๐ฅ)) โ ๐ง โ On) |
80 | | 1on 8425 |
. . . . . . . . . . . . . . . . . . . . . 22
โข
1o โ On |
81 | | omcl 8483 |
. . . . . . . . . . . . . . . . . . . . . 22
โข
(((ฯ โo ๐ฅ) โ On โง 1o โ On)
โ ((ฯ โo ๐ฅ) ยทo 1o) โ
On) |
82 | 76, 80, 81 | sylancl 587 |
. . . . . . . . . . . . . . . . . . . . 21
โข
(((((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โง
๐ฅ โ On) โ
((ฯ โo ๐ฅ) ยทo 1o) โ
On) |
83 | 82 | ad5ant12 755 |
. . . . . . . . . . . . . . . . . . . 20
โข
((((((((๐ด โ
๐ต โง โ
โ
๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โง
๐ฅ โ On) โง ๐ฆ โ (ฯ โ
1o)) โง ๐ง
โ (ฯ โo ๐ฅ)) โง (((ฯ โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ด) โ ((ฯ โo ๐ฅ) ยทo
1o) โ On) |
84 | | oaword 8497 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((โ
โ On โง ๐ง โ On
โง ((ฯ โo ๐ฅ) ยทo 1o) โ
On) โ (โ
โ ๐ง โ (((ฯ โo ๐ฅ) ยทo
1o) +o โ
) โ (((ฯ โo
๐ฅ) ยทo
1o) +o ๐ง))) |
85 | 84 | biimpd 228 |
. . . . . . . . . . . . . . . . . . . 20
โข ((โ
โ On โง ๐ง โ On
โง ((ฯ โo ๐ฅ) ยทo 1o) โ
On) โ (โ
โ ๐ง โ (((ฯ โo ๐ฅ) ยทo
1o) +o โ
) โ (((ฯ โo
๐ฅ) ยทo
1o) +o ๐ง))) |
86 | 73, 79, 83, 85 | mp3an2ani 1469 |
. . . . . . . . . . . . . . . . . . 19
โข
((((((((๐ด โ
๐ต โง โ
โ
๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โง
๐ฅ โ On) โง ๐ฆ โ (ฯ โ
1o)) โง ๐ง
โ (ฯ โo ๐ฅ)) โง (((ฯ โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ด) โ (โ
โ ๐ง โ (((ฯ โo ๐ฅ) ยทo
1o) +o โ
) โ (((ฯ โo
๐ฅ) ยทo
1o) +o ๐ง))) |
87 | 72, 86 | mpi 20 |
. . . . . . . . . . . . . . . . . 18
โข
((((((((๐ด โ
๐ต โง โ
โ
๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โง
๐ฅ โ On) โง ๐ฆ โ (ฯ โ
1o)) โง ๐ง
โ (ฯ โo ๐ฅ)) โง (((ฯ โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ด) โ (((ฯ โo ๐ฅ) ยทo
1o) +o โ
) โ (((ฯ โo
๐ฅ) ยทo
1o) +o ๐ง)) |
88 | | simpllr 775 |
. . . . . . . . . . . . . . . . . . . . 21
โข
((((((((๐ด โ
๐ต โง โ
โ
๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โง
๐ฅ โ On) โง ๐ฆ โ (ฯ โ
1o)) โง ๐ง
โ (ฯ โo ๐ฅ)) โง (((ฯ โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ด) โ ๐ฆ โ (ฯ โ
1o)) |
89 | | omsson 7807 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ฯ
โ On |
90 | | ssdif 4100 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (ฯ
โ On โ (ฯ โ 1o) โ (On โ
1o)) |
91 | 89, 90 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (ฯ
โ 1o) โ (On โ 1o) |
92 | 91 | sseli 3941 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ฆ โ (ฯ โ
1o) โ ๐ฆ
โ (On โ 1o)) |
93 | | ondif1 8448 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ฆ โ (On โ
1o) โ (๐ฆ
โ On โง โ
โ ๐ฆ)) |
94 | | df-1o 8413 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข
1o = suc โ
|
95 | | eloni 6328 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (๐ฆ โ On โ Ord ๐ฆ) |
96 | | ordsucss 7754 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (Ord
๐ฆ โ (โ
โ
๐ฆ โ suc โ
โ ๐ฆ)) |
97 | 95, 96 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ฆ โ On โ (โ
โ ๐ฆ โ suc โ
โ ๐ฆ)) |
98 | 97 | imp 408 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ฆ โ On โง โ
โ
๐ฆ) โ suc โ
โ ๐ฆ) |
99 | 94, 98 | eqsstrid 3993 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ฆ โ On โง โ
โ
๐ฆ) โ 1o
โ ๐ฆ) |
100 | 93, 99 | sylbi 216 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ฆ โ (On โ
1o) โ 1o โ ๐ฆ) |
101 | 88, 92, 100 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . 20
โข
((((((((๐ด โ
๐ต โง โ
โ
๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โง
๐ฅ โ On) โง ๐ฆ โ (ฯ โ
1o)) โง ๐ง
โ (ฯ โo ๐ฅ)) โง (((ฯ โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ด) โ 1o โ ๐ฆ) |
102 | | eldifi 4087 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ฆ โ (ฯ โ
1o) โ ๐ฆ
โ ฯ) |
103 | | nnon 7809 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ฆ โ ฯ โ ๐ฆ โ On) |
104 | 102, 103 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ฆ โ (ฯ โ
1o) โ ๐ฆ
โ On) |
105 | 104 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . . . 21
โข
(((((((๐ด โ
๐ต โง โ
โ
๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โง
๐ฅ โ On) โง ๐ฆ โ (ฯ โ
1o)) โง ๐ง
โ (ฯ โo ๐ฅ)) โ ๐ฆ โ On) |
106 | | simp-4r 783 |
. . . . . . . . . . . . . . . . . . . . . 22
โข
((((((((๐ด โ
๐ต โง โ
โ
๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โง
๐ฅ โ On) โง ๐ฆ โ (ฯ โ
1o)) โง ๐ง
โ (ฯ โo ๐ฅ)) โง (((ฯ โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ด) โ ๐ฅ โ On) |
107 | 33, 106, 75 | sylancr 588 |
. . . . . . . . . . . . . . . . . . . . 21
โข
((((((((๐ด โ
๐ต โง โ
โ
๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โง
๐ฅ โ On) โง ๐ฆ โ (ฯ โ
1o)) โง ๐ง
โ (ฯ โo ๐ฅ)) โง (((ฯ โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ด) โ (ฯ โo ๐ฅ) โ On) |
108 | | omwordi 8519 |
. . . . . . . . . . . . . . . . . . . . 21
โข
((1o โ On โง ๐ฆ โ On โง (ฯ โo
๐ฅ) โ On) โ
(1o โ ๐ฆ
โ ((ฯ โo ๐ฅ) ยทo 1o) โ
((ฯ โo ๐ฅ) ยทo ๐ฆ))) |
109 | 80, 105, 107, 108 | mp3an2ani 1469 |
. . . . . . . . . . . . . . . . . . . 20
โข
((((((((๐ด โ
๐ต โง โ
โ
๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โง
๐ฅ โ On) โง ๐ฆ โ (ฯ โ
1o)) โง ๐ง
โ (ฯ โo ๐ฅ)) โง (((ฯ โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ด) โ (1o โ ๐ฆ โ ((ฯ
โo ๐ฅ)
ยทo 1o) โ ((ฯ โo ๐ฅ) ยทo ๐ฆ))) |
110 | 101, 109 | mpd 15 |
. . . . . . . . . . . . . . . . . . 19
โข
((((((((๐ด โ
๐ต โง โ
โ
๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โง
๐ฅ โ On) โง ๐ฆ โ (ฯ โ
1o)) โง ๐ง
โ (ฯ โo ๐ฅ)) โง (((ฯ โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ด) โ ((ฯ โo ๐ฅ) ยทo
1o) โ ((ฯ โo ๐ฅ) ยทo ๐ฆ)) |
111 | 105 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
โข
((((((((๐ด โ
๐ต โง โ
โ
๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โง
๐ฅ โ On) โง ๐ฆ โ (ฯ โ
1o)) โง ๐ง
โ (ฯ โo ๐ฅ)) โง (((ฯ โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ด) โ ๐ฆ โ On) |
112 | | omcl 8483 |
. . . . . . . . . . . . . . . . . . . . 21
โข
(((ฯ โo ๐ฅ) โ On โง ๐ฆ โ On) โ ((ฯ
โo ๐ฅ)
ยทo ๐ฆ)
โ On) |
113 | 107, 111,
112 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . 20
โข
((((((((๐ด โ
๐ต โง โ
โ
๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โง
๐ฅ โ On) โง ๐ฆ โ (ฯ โ
1o)) โง ๐ง
โ (ฯ โo ๐ฅ)) โง (((ฯ โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ด) โ ((ฯ โo ๐ฅ) ยทo ๐ฆ) โ On) |
114 | 79 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
โข
((((((((๐ด โ
๐ต โง โ
โ
๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โง
๐ฅ โ On) โง ๐ฆ โ (ฯ โ
1o)) โง ๐ง
โ (ฯ โo ๐ฅ)) โง (((ฯ โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ด) โ ๐ง โ On) |
115 | | oawordri 8498 |
. . . . . . . . . . . . . . . . . . . 20
โข
((((ฯ โo ๐ฅ) ยทo 1o) โ
On โง ((ฯ โo ๐ฅ) ยทo ๐ฆ) โ On โง ๐ง โ On) โ (((ฯ
โo ๐ฅ)
ยทo 1o) โ ((ฯ โo ๐ฅ) ยทo ๐ฆ) โ (((ฯ
โo ๐ฅ)
ยทo 1o) +o ๐ง) โ (((ฯ โo ๐ฅ) ยทo ๐ฆ) +o ๐ง))) |
116 | 83, 113, 114, 115 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . 19
โข
((((((((๐ด โ
๐ต โง โ
โ
๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โง
๐ฅ โ On) โง ๐ฆ โ (ฯ โ
1o)) โง ๐ง
โ (ฯ โo ๐ฅ)) โง (((ฯ โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ด) โ (((ฯ โo ๐ฅ) ยทo
1o) โ ((ฯ โo ๐ฅ) ยทo ๐ฆ) โ (((ฯ โo ๐ฅ) ยทo
1o) +o ๐ง) โ (((ฯ โo ๐ฅ) ยทo ๐ฆ) +o ๐ง))) |
117 | 110, 116 | mpd 15 |
. . . . . . . . . . . . . . . . . 18
โข
((((((((๐ด โ
๐ต โง โ
โ
๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โง
๐ฅ โ On) โง ๐ฆ โ (ฯ โ
1o)) โง ๐ง
โ (ฯ โo ๐ฅ)) โง (((ฯ โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ด) โ (((ฯ โo ๐ฅ) ยทo
1o) +o ๐ง) โ (((ฯ โo ๐ฅ) ยทo ๐ฆ) +o ๐ง)) |
118 | 87, 117 | sstrd 3955 |
. . . . . . . . . . . . . . . . 17
โข
((((((((๐ด โ
๐ต โง โ
โ
๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โง
๐ฅ โ On) โง ๐ฆ โ (ฯ โ
1o)) โง ๐ง
โ (ฯ โo ๐ฅ)) โง (((ฯ โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ด) โ (((ฯ โo ๐ฅ) ยทo
1o) +o โ
) โ (((ฯ โo
๐ฅ) ยทo
๐ฆ) +o ๐ง)) |
119 | 33, 75 | mpan 689 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ฅ โ On โ (ฯ
โo ๐ฅ)
โ On) |
120 | 119, 80, 81 | sylancl 587 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ฅ โ On โ ((ฯ
โo ๐ฅ)
ยทo 1o) โ On) |
121 | | oa0 8463 |
. . . . . . . . . . . . . . . . . . . 20
โข
(((ฯ โo ๐ฅ) ยทo 1o) โ
On โ (((ฯ โo ๐ฅ) ยทo 1o)
+o โ
) = ((ฯ โo ๐ฅ) ยทo
1o)) |
122 | 120, 121 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ฅ โ On โ (((ฯ
โo ๐ฅ)
ยทo 1o) +o โ
) = ((ฯ
โo ๐ฅ)
ยทo 1o)) |
123 | | om1 8490 |
. . . . . . . . . . . . . . . . . . . 20
โข ((ฯ
โo ๐ฅ)
โ On โ ((ฯ โo ๐ฅ) ยทo 1o) =
(ฯ โo ๐ฅ)) |
124 | 119, 123 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ฅ โ On โ ((ฯ
โo ๐ฅ)
ยทo 1o) = (ฯ โo ๐ฅ)) |
125 | 122, 124 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . 18
โข (๐ฅ โ On โ (((ฯ
โo ๐ฅ)
ยทo 1o) +o โ
) = (ฯ
โo ๐ฅ)) |
126 | 106, 125 | syl 17 |
. . . . . . . . . . . . . . . . 17
โข
((((((((๐ด โ
๐ต โง โ
โ
๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โง
๐ฅ โ On) โง ๐ฆ โ (ฯ โ
1o)) โง ๐ง
โ (ฯ โo ๐ฅ)) โง (((ฯ โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ด) โ (((ฯ โo ๐ฅ) ยทo
1o) +o โ
) = (ฯ โo ๐ฅ)) |
127 | | simpr 486 |
. . . . . . . . . . . . . . . . 17
โข
((((((((๐ด โ
๐ต โง โ
โ
๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โง
๐ฅ โ On) โง ๐ฆ โ (ฯ โ
1o)) โง ๐ง
โ (ฯ โo ๐ฅ)) โง (((ฯ โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ด) โ (((ฯ โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ด) |
128 | 118, 126,
127 | 3sstr3d 3991 |
. . . . . . . . . . . . . . . 16
โข
((((((((๐ด โ
๐ต โง โ
โ
๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โง
๐ฅ โ On) โง ๐ฆ โ (ฯ โ
1o)) โง ๐ง
โ (ฯ โo ๐ฅ)) โง (((ฯ โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ด) โ (ฯ โo ๐ฅ) โ ๐ด) |
129 | | simp-7l 788 |
. . . . . . . . . . . . . . . . 17
โข
((((((((๐ด โ
๐ต โง โ
โ
๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โง
๐ฅ โ On) โง ๐ฆ โ (ฯ โ
1o)) โง ๐ง
โ (ฯ โo ๐ฅ)) โง (((ฯ โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ด) โ ๐ด โ ๐ต) |
130 | | simplrl 776 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โ
๐ต = (ฯ
โo (ฯ โo ๐ถ))) |
131 | 130 | ad4antr 731 |
. . . . . . . . . . . . . . . . 17
โข
((((((((๐ด โ
๐ต โง โ
โ
๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โง
๐ฅ โ On) โง ๐ฆ โ (ฯ โ
1o)) โง ๐ง
โ (ฯ โo ๐ฅ)) โง (((ฯ โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ด) โ ๐ต = (ฯ โo (ฯ
โo ๐ถ))) |
132 | 129, 131 | eleqtrd 2836 |
. . . . . . . . . . . . . . . 16
โข
((((((((๐ด โ
๐ต โง โ
โ
๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โง
๐ฅ โ On) โง ๐ฆ โ (ฯ โ
1o)) โง ๐ง
โ (ฯ โo ๐ฅ)) โง (((ฯ โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ด) โ ๐ด โ (ฯ โo (ฯ
โo ๐ถ))) |
133 | 55 | ad6antlr 736 |
. . . . . . . . . . . . . . . . 17
โข
((((((((๐ด โ
๐ต โง โ
โ
๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โง
๐ฅ โ On) โง ๐ฆ โ (ฯ โ
1o)) โง ๐ง
โ (ฯ โo ๐ฅ)) โง (((ฯ โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ด) โ (ฯ โo
(ฯ โo ๐ถ)) โ On) |
134 | | ontr2 6365 |
. . . . . . . . . . . . . . . . 17
โข
(((ฯ โo ๐ฅ) โ On โง (ฯ โo
(ฯ โo ๐ถ)) โ On) โ (((ฯ
โo ๐ฅ)
โ ๐ด โง ๐ด โ (ฯ
โo (ฯ โo ๐ถ))) โ (ฯ โo ๐ฅ) โ (ฯ
โo (ฯ โo ๐ถ)))) |
135 | 107, 133,
134 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
โข
((((((((๐ด โ
๐ต โง โ
โ
๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โง
๐ฅ โ On) โง ๐ฆ โ (ฯ โ
1o)) โง ๐ง
โ (ฯ โo ๐ฅ)) โง (((ฯ โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ด) โ (((ฯ โo ๐ฅ) โ ๐ด โง ๐ด โ (ฯ โo (ฯ
โo ๐ถ)))
โ (ฯ โo ๐ฅ) โ (ฯ โo (ฯ
โo ๐ถ)))) |
136 | 128, 132,
135 | mp2and 698 |
. . . . . . . . . . . . . . 15
โข
((((((((๐ด โ
๐ต โง โ
โ
๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โง
๐ฅ โ On) โง ๐ฆ โ (ฯ โ
1o)) โง ๐ง
โ (ฯ โo ๐ฅ)) โง (((ฯ โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ด) โ (ฯ โo ๐ฅ) โ (ฯ
โo (ฯ โo ๐ถ))) |
137 | 36 | ad6antlr 736 |
. . . . . . . . . . . . . . . 16
โข
((((((((๐ด โ
๐ต โง โ
โ
๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โง
๐ฅ โ On) โง ๐ฆ โ (ฯ โ
1o)) โง ๐ง
โ (ฯ โo ๐ฅ)) โง (((ฯ โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ด) โ (ฯ โo ๐ถ) โ On) |
138 | 65 | a1i 11 |
. . . . . . . . . . . . . . . 16
โข
((((((((๐ด โ
๐ต โง โ
โ
๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โง
๐ฅ โ On) โง ๐ฆ โ (ฯ โ
1o)) โง ๐ง
โ (ฯ โo ๐ฅ)) โง (((ฯ โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ด) โ ฯ โ (On โ
2o)) |
139 | | oeord 8536 |
. . . . . . . . . . . . . . . 16
โข ((๐ฅ โ On โง (ฯ
โo ๐ถ)
โ On โง ฯ โ (On โ 2o)) โ (๐ฅ โ (ฯ
โo ๐ถ)
โ (ฯ โo ๐ฅ) โ (ฯ โo (ฯ
โo ๐ถ)))) |
140 | 106, 137,
138, 139 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
โข
((((((((๐ด โ
๐ต โง โ
โ
๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โง
๐ฅ โ On) โง ๐ฆ โ (ฯ โ
1o)) โง ๐ง
โ (ฯ โo ๐ฅ)) โง (((ฯ โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ด) โ (๐ฅ โ (ฯ โo ๐ถ) โ (ฯ
โo ๐ฅ)
โ (ฯ โo (ฯ โo ๐ถ)))) |
141 | 136, 140 | mpbird 257 |
. . . . . . . . . . . . . 14
โข
((((((((๐ด โ
๐ต โง โ
โ
๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โง
๐ฅ โ On) โง ๐ฆ โ (ฯ โ
1o)) โง ๐ง
โ (ฯ โo ๐ฅ)) โง (((ฯ โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ด) โ ๐ฅ โ (ฯ โo ๐ถ)) |
142 | | simp-5r 785 |
. . . . . . . . . . . . . . 15
โข
((((((((๐ด โ
๐ต โง โ
โ
๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โง
๐ฅ โ On) โง ๐ฆ โ (ฯ โ
1o)) โง ๐ง
โ (ฯ โo ๐ฅ)) โง (((ฯ โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ด) โ ฯ โ ๐ด) |
143 | 142, 128 | unssd 4147 |
. . . . . . . . . . . . . 14
โข
((((((((๐ด โ
๐ต โง โ
โ
๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โง
๐ฅ โ On) โง ๐ฆ โ (ฯ โ
1o)) โง ๐ง
โ (ฯ โo ๐ฅ)) โง (((ฯ โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ด) โ (ฯ โช (ฯ
โo ๐ฅ))
โ ๐ด) |
144 | | simplr 768 |
. . . . . . . . . . . . . . . . . . . 20
โข
((((((((๐ด โ
๐ต โง โ
โ
๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โง
๐ฅ โ On) โง ๐ฆ โ (ฯ โ
1o)) โง ๐ง
โ (ฯ โo ๐ฅ)) โง (((ฯ โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ด) โ ๐ง โ (ฯ โo ๐ฅ)) |
145 | | onelpss 6358 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ง โ On โง (ฯ
โo ๐ฅ)
โ On) โ (๐ง โ
(ฯ โo ๐ฅ) โ (๐ง โ (ฯ โo ๐ฅ) โง ๐ง โ (ฯ โo ๐ฅ)))) |
146 | 145 | biimpd 228 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ง โ On โง (ฯ
โo ๐ฅ)
โ On) โ (๐ง โ
(ฯ โo ๐ฅ) โ (๐ง โ (ฯ โo ๐ฅ) โง ๐ง โ (ฯ โo ๐ฅ)))) |
147 | 79, 107, 146 | syl2an2r 684 |
. . . . . . . . . . . . . . . . . . . 20
โข
((((((((๐ด โ
๐ต โง โ
โ
๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โง
๐ฅ โ On) โง ๐ฆ โ (ฯ โ
1o)) โง ๐ง
โ (ฯ โo ๐ฅ)) โง (((ฯ โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ด) โ (๐ง โ (ฯ โo ๐ฅ) โ (๐ง โ (ฯ โo ๐ฅ) โง ๐ง โ (ฯ โo ๐ฅ)))) |
148 | 144, 147 | mpd 15 |
. . . . . . . . . . . . . . . . . . 19
โข
((((((((๐ด โ
๐ต โง โ
โ
๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โง
๐ฅ โ On) โง ๐ฆ โ (ฯ โ
1o)) โง ๐ง
โ (ฯ โo ๐ฅ)) โง (((ฯ โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ด) โ (๐ง โ (ฯ โo ๐ฅ) โง ๐ง โ (ฯ โo ๐ฅ))) |
149 | | simpl 484 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ง โ (ฯ
โo ๐ฅ) โง
๐ง โ (ฯ
โo ๐ฅ))
โ ๐ง โ (ฯ
โo ๐ฅ)) |
150 | 148, 149 | syl 17 |
. . . . . . . . . . . . . . . . . 18
โข
((((((((๐ด โ
๐ต โง โ
โ
๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โง
๐ฅ โ On) โง ๐ฆ โ (ฯ โ
1o)) โง ๐ง
โ (ฯ โo ๐ฅ)) โง (((ฯ โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ด) โ ๐ง โ (ฯ โo ๐ฅ)) |
151 | | oaword 8497 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ง โ On โง (ฯ
โo ๐ฅ)
โ On โง ((ฯ โo ๐ฅ) ยทo ๐ฆ) โ On) โ (๐ง โ (ฯ โo ๐ฅ) โ (((ฯ
โo ๐ฅ)
ยทo ๐ฆ)
+o ๐ง) โ
(((ฯ โo ๐ฅ) ยทo ๐ฆ) +o (ฯ โo
๐ฅ)))) |
152 | 151 | biimpd 228 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ง โ On โง (ฯ
โo ๐ฅ)
โ On โง ((ฯ โo ๐ฅ) ยทo ๐ฆ) โ On) โ (๐ง โ (ฯ โo ๐ฅ) โ (((ฯ
โo ๐ฅ)
ยทo ๐ฆ)
+o ๐ง) โ
(((ฯ โo ๐ฅ) ยทo ๐ฆ) +o (ฯ โo
๐ฅ)))) |
153 | 114, 107,
113, 152 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . 18
โข
((((((((๐ด โ
๐ต โง โ
โ
๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โง
๐ฅ โ On) โง ๐ฆ โ (ฯ โ
1o)) โง ๐ง
โ (ฯ โo ๐ฅ)) โง (((ฯ โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ด) โ (๐ง โ (ฯ โo ๐ฅ) โ (((ฯ
โo ๐ฅ)
ยทo ๐ฆ)
+o ๐ง) โ
(((ฯ โo ๐ฅ) ยทo ๐ฆ) +o (ฯ โo
๐ฅ)))) |
154 | 150, 153 | mpd 15 |
. . . . . . . . . . . . . . . . 17
โข
((((((((๐ด โ
๐ต โง โ
โ
๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โง
๐ฅ โ On) โง ๐ฆ โ (ฯ โ
1o)) โง ๐ง
โ (ฯ โo ๐ฅ)) โง (((ฯ โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ด) โ (((ฯ โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) โ (((ฯ
โo ๐ฅ)
ยทo ๐ฆ)
+o (ฯ โo ๐ฅ))) |
155 | | omsuc 8473 |
. . . . . . . . . . . . . . . . . 18
โข
(((ฯ โo ๐ฅ) โ On โง ๐ฆ โ On) โ ((ฯ
โo ๐ฅ)
ยทo suc ๐ฆ)
= (((ฯ โo ๐ฅ) ยทo ๐ฆ) +o (ฯ โo
๐ฅ))) |
156 | 107, 111,
155 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
โข
((((((((๐ด โ
๐ต โง โ
โ
๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โง
๐ฅ โ On) โง ๐ฆ โ (ฯ โ
1o)) โง ๐ง
โ (ฯ โo ๐ฅ)) โง (((ฯ โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ด) โ ((ฯ โo ๐ฅ) ยทo suc ๐ฆ) = (((ฯ
โo ๐ฅ)
ยทo ๐ฆ)
+o (ฯ โo ๐ฅ))) |
157 | 154, 156 | sseqtrrd 3986 |
. . . . . . . . . . . . . . . 16
โข
((((((((๐ด โ
๐ต โง โ
โ
๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โง
๐ฅ โ On) โง ๐ฆ โ (ฯ โ
1o)) โง ๐ง
โ (ฯ โo ๐ฅ)) โง (((ฯ โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ด) โ (((ฯ โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) โ ((ฯ
โo ๐ฅ)
ยทo suc ๐ฆ)) |
158 | | ordom 7813 |
. . . . . . . . . . . . . . . . . . 19
โข Ord
ฯ |
159 | 88, 102 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
โข
((((((((๐ด โ
๐ต โง โ
โ
๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โง
๐ฅ โ On) โง ๐ฆ โ (ฯ โ
1o)) โง ๐ง
โ (ฯ โo ๐ฅ)) โง (((ฯ โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ด) โ ๐ฆ โ ฯ) |
160 | | ordsucss 7754 |
. . . . . . . . . . . . . . . . . . 19
โข (Ord
ฯ โ (๐ฆ โ
ฯ โ suc ๐ฆ
โ ฯ)) |
161 | 158, 159,
160 | mpsyl 68 |
. . . . . . . . . . . . . . . . . 18
โข
((((((((๐ด โ
๐ต โง โ
โ
๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โง
๐ฅ โ On) โง ๐ฆ โ (ฯ โ
1o)) โง ๐ง
โ (ฯ โo ๐ฅ)) โง (((ฯ โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ด) โ suc ๐ฆ โ ฯ) |
162 | | oe1 8492 |
. . . . . . . . . . . . . . . . . . . 20
โข (ฯ
โ On โ (ฯ โo 1o) =
ฯ) |
163 | 33, 162 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
โข (ฯ
โo 1o) = ฯ |
164 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
โข
(((((((((๐ด โ
๐ต โง โ
โ
๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โง
๐ฅ โ On) โง ๐ฆ โ (ฯ โ
1o)) โง ๐ง
โ (ฯ โo ๐ฅ)) โง (((ฯ โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ด) โง ๐ฅ = โ
) โ ๐ฅ = โ
) |
165 | 164 | oveq2d 7374 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
โข
(((((((((๐ด โ
๐ต โง โ
โ
๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โง
๐ฅ โ On) โง ๐ฆ โ (ฯ โ
1o)) โง ๐ง
โ (ฯ โo ๐ฅ)) โง (((ฯ โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ด) โง ๐ฅ = โ
) โ (ฯ
โo ๐ฅ) =
(ฯ โo โ
)) |
166 | | oe0 8469 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
โข (ฯ
โ On โ (ฯ โo โ
) =
1o) |
167 | 33, 166 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
โข (ฯ
โo โ
) = 1o |
168 | 165, 167 | eqtrdi 2789 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข
(((((((((๐ด โ
๐ต โง โ
โ
๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โง
๐ฅ โ On) โง ๐ฆ โ (ฯ โ
1o)) โง ๐ง
โ (ฯ โo ๐ฅ)) โง (((ฯ โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ด) โง ๐ฅ = โ
) โ (ฯ
โo ๐ฅ) =
1o) |
169 | 168 | oveq1d 7373 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข
(((((((((๐ด โ
๐ต โง โ
โ
๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โง
๐ฅ โ On) โง ๐ฆ โ (ฯ โ
1o)) โง ๐ง
โ (ฯ โo ๐ฅ)) โง (((ฯ โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ด) โง ๐ฅ = โ
) โ ((ฯ
โo ๐ฅ)
ยทo ๐ฆ) =
(1o ยทo ๐ฆ)) |
170 | 104 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
โข
((((((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โง
๐ฅ โ On) โง ๐ฆ โ (ฯ โ
1o)) โ ๐ฆ
โ On) |
171 | 170 | ad5ant12 755 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข
(((((((((๐ด โ
๐ต โง โ
โ
๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โง
๐ฅ โ On) โง ๐ฆ โ (ฯ โ
1o)) โง ๐ง
โ (ฯ โo ๐ฅ)) โง (((ฯ โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ด) โง ๐ฅ = โ
) โ ๐ฆ โ On) |
172 | | om1r 8491 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข (๐ฆ โ On โ (1o
ยทo ๐ฆ) =
๐ฆ) |
173 | 171, 172 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข
(((((((((๐ด โ
๐ต โง โ
โ
๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โง
๐ฅ โ On) โง ๐ฆ โ (ฯ โ
1o)) โง ๐ง
โ (ฯ โo ๐ฅ)) โง (((ฯ โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ด) โง ๐ฅ = โ
) โ (1o
ยทo ๐ฆ) =
๐ฆ) |
174 | 169, 173 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข
(((((((((๐ด โ
๐ต โง โ
โ
๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โง
๐ฅ โ On) โง ๐ฆ โ (ฯ โ
1o)) โง ๐ง
โ (ฯ โo ๐ฅ)) โง (((ฯ โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ด) โง ๐ฅ = โ
) โ ((ฯ
โo ๐ฅ)
ยทo ๐ฆ) =
๐ฆ) |
175 | | simpllr 775 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข
(((((((((๐ด โ
๐ต โง โ
โ
๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โง
๐ฅ โ On) โง ๐ฆ โ (ฯ โ
1o)) โง ๐ง
โ (ฯ โo ๐ฅ)) โง (((ฯ โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ด) โง ๐ฅ = โ
) โ ๐ง โ (ฯ โo ๐ฅ)) |
176 | 175, 168 | eleqtrd 2836 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข
(((((((((๐ด โ
๐ต โง โ
โ
๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โง
๐ฅ โ On) โง ๐ฆ โ (ฯ โ
1o)) โง ๐ง
โ (ฯ โo ๐ฅ)) โง (((ฯ โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ด) โง ๐ฅ = โ
) โ ๐ง โ 1o) |
177 | | el1o 8442 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข (๐ง โ 1o โ
๐ง =
โ
) |
178 | 176, 177 | sylib 217 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข
(((((((((๐ด โ
๐ต โง โ
โ
๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โง
๐ฅ โ On) โง ๐ฆ โ (ฯ โ
1o)) โง ๐ง
โ (ฯ โo ๐ฅ)) โง (((ฯ โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ด) โง ๐ฅ = โ
) โ ๐ง = โ
) |
179 | 174, 178 | oveq12d 7376 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข
(((((((((๐ด โ
๐ต โง โ
โ
๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โง
๐ฅ โ On) โง ๐ฆ โ (ฯ โ
1o)) โง ๐ง
โ (ฯ โo ๐ฅ)) โง (((ฯ โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ด) โง ๐ฅ = โ
) โ (((ฯ
โo ๐ฅ)
ยทo ๐ฆ)
+o ๐ง) = (๐ฆ +o
โ
)) |
180 | | simplr 768 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข
(((((((((๐ด โ
๐ต โง โ
โ
๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โง
๐ฅ โ On) โง ๐ฆ โ (ฯ โ
1o)) โง ๐ง
โ (ฯ โo ๐ฅ)) โง (((ฯ โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ด) โง ๐ฅ = โ
) โ (((ฯ
โo ๐ฅ)
ยทo ๐ฆ)
+o ๐ง) = ๐ด) |
181 | | oa0 8463 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (๐ฆ โ On โ (๐ฆ +o โ
) = ๐ฆ) |
182 | 171, 181 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข
(((((((((๐ด โ
๐ต โง โ
โ
๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โง
๐ฅ โ On) โง ๐ฆ โ (ฯ โ
1o)) โง ๐ง
โ (ฯ โo ๐ฅ)) โง (((ฯ โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ด) โง ๐ฅ = โ
) โ (๐ฆ +o โ
) = ๐ฆ) |
183 | 179, 180,
182 | 3eqtr3d 2781 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข
(((((((((๐ด โ
๐ต โง โ
โ
๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โง
๐ฅ โ On) โง ๐ฆ โ (ฯ โ
1o)) โง ๐ง
โ (ฯ โo ๐ฅ)) โง (((ฯ โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ด) โง ๐ฅ = โ
) โ ๐ด = ๐ฆ) |
184 | 159 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข
(((((((((๐ด โ
๐ต โง โ
โ
๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โง
๐ฅ โ On) โง ๐ฆ โ (ฯ โ
1o)) โง ๐ง
โ (ฯ โo ๐ฅ)) โง (((ฯ โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ด) โง ๐ฅ = โ
) โ ๐ฆ โ ฯ) |
185 | 183, 184 | eqeltrd 2834 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข
(((((((((๐ด โ
๐ต โง โ
โ
๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โง
๐ฅ โ On) โง ๐ฆ โ (ฯ โ
1o)) โง ๐ง
โ (ฯ โo ๐ฅ)) โง (((ฯ โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ด) โง ๐ฅ = โ
) โ ๐ด โ ฯ) |
186 | 185 | ex 414 |
. . . . . . . . . . . . . . . . . . . . . 22
โข
((((((((๐ด โ
๐ต โง โ
โ
๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โง
๐ฅ โ On) โง ๐ฆ โ (ฯ โ
1o)) โง ๐ง
โ (ฯ โo ๐ฅ)) โง (((ฯ โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ด) โ (๐ฅ = โ
โ ๐ด โ ฯ)) |
187 | 33, 33 | pm3.2i 472 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (ฯ
โ On โง ฯ โ On) |
188 | | ontr2 6365 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((ฯ
โ On โง ฯ โ On) โ ((ฯ โ ๐ด โง ๐ด โ ฯ) โ ฯ โ
ฯ)) |
189 | 188 | expd 417 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((ฯ
โ On โง ฯ โ On) โ (ฯ โ ๐ด โ (๐ด โ ฯ โ ฯ โ
ฯ))) |
190 | 187, 142,
189 | mpsyl 68 |
. . . . . . . . . . . . . . . . . . . . . 22
โข
((((((((๐ด โ
๐ต โง โ
โ
๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โง
๐ฅ โ On) โง ๐ฆ โ (ฯ โ
1o)) โง ๐ง
โ (ฯ โo ๐ฅ)) โง (((ฯ โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ด) โ (๐ด โ ฯ โ ฯ โ
ฯ)) |
191 | | elirr 9538 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ยฌ
ฯ โ ฯ |
192 | 191 | pm2.21i 119 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (ฯ
โ ฯ โ 1o โ ๐ฅ) |
193 | 192 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
โข
((((((((๐ด โ
๐ต โง โ
โ
๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โง
๐ฅ โ On) โง ๐ฆ โ (ฯ โ
1o)) โง ๐ง
โ (ฯ โo ๐ฅ)) โง (((ฯ โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ด) โ (ฯ โ ฯ โ
1o โ ๐ฅ)) |
194 | 186, 190,
193 | 3syld 60 |
. . . . . . . . . . . . . . . . . . . . 21
โข
((((((((๐ด โ
๐ต โง โ
โ
๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โง
๐ฅ โ On) โง ๐ฆ โ (ฯ โ
1o)) โง ๐ง
โ (ฯ โo ๐ฅ)) โง (((ฯ โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ด) โ (๐ฅ = โ
โ 1o โ ๐ฅ)) |
195 | | eloni 6328 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ฅ โ On โ Ord ๐ฅ) |
196 | | ordsucss 7754 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (Ord
๐ฅ โ (โ
โ
๐ฅ โ suc โ
โ ๐ฅ)) |
197 | 196 | imp 408 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((Ord
๐ฅ โง โ
โ
๐ฅ) โ suc โ
โ ๐ฅ) |
198 | 94, 197 | eqsstrid 3993 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((Ord
๐ฅ โง โ
โ
๐ฅ) โ 1o
โ ๐ฅ) |
199 | 198 | ex 414 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (Ord
๐ฅ โ (โ
โ
๐ฅ โ 1o
โ ๐ฅ)) |
200 | 106, 195,
199 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . 21
โข
((((((((๐ด โ
๐ต โง โ
โ
๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โง
๐ฅ โ On) โง ๐ฆ โ (ฯ โ
1o)) โง ๐ง
โ (ฯ โo ๐ฅ)) โง (((ฯ โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ด) โ (โ
โ ๐ฅ โ 1o โ ๐ฅ)) |
201 | | on0eqel 6442 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ฅ โ On โ (๐ฅ = โ
โจ โ
โ
๐ฅ)) |
202 | 106, 201 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
โข
((((((((๐ด โ
๐ต โง โ
โ
๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โง
๐ฅ โ On) โง ๐ฆ โ (ฯ โ
1o)) โง ๐ง
โ (ฯ โo ๐ฅ)) โง (((ฯ โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ด) โ (๐ฅ = โ
โจ โ
โ ๐ฅ)) |
203 | 194, 200,
202 | mpjaod 859 |
. . . . . . . . . . . . . . . . . . . 20
โข
((((((((๐ด โ
๐ต โง โ
โ
๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โง
๐ฅ โ On) โง ๐ฆ โ (ฯ โ
1o)) โง ๐ง
โ (ฯ โo ๐ฅ)) โง (((ฯ โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ด) โ 1o โ ๐ฅ) |
204 | 80 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
โข
((((((((๐ด โ
๐ต โง โ
โ
๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โง
๐ฅ โ On) โง ๐ฆ โ (ฯ โ
1o)) โง ๐ง
โ (ฯ โo ๐ฅ)) โง (((ฯ โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ด) โ 1o โ
On) |
205 | 33 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
โข
((((((((๐ด โ
๐ต โง โ
โ
๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โง
๐ฅ โ On) โง ๐ฆ โ (ฯ โ
1o)) โง ๐ง
โ (ฯ โo ๐ฅ)) โง (((ฯ โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ด) โ ฯ โ On) |
206 | 204, 106,
205 | 3jca 1129 |
. . . . . . . . . . . . . . . . . . . . 21
โข
((((((((๐ด โ
๐ต โง โ
โ
๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โง
๐ฅ โ On) โง ๐ฆ โ (ฯ โ
1o)) โง ๐ง
โ (ฯ โo ๐ฅ)) โง (((ฯ โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ด) โ (1o โ On โง
๐ฅ โ On โง ฯ
โ On)) |
207 | | oewordi 8539 |
. . . . . . . . . . . . . . . . . . . . 21
โข
(((1o โ On โง ๐ฅ โ On โง ฯ โ On) โง
โ
โ ฯ) โ (1o โ ๐ฅ โ (ฯ โo
1o) โ (ฯ โo ๐ฅ))) |
208 | 206, 39, 207 | sylancl 587 |
. . . . . . . . . . . . . . . . . . . 20
โข
((((((((๐ด โ
๐ต โง โ
โ
๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โง
๐ฅ โ On) โง ๐ฆ โ (ฯ โ
1o)) โง ๐ง
โ (ฯ โo ๐ฅ)) โง (((ฯ โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ด) โ (1o โ ๐ฅ โ (ฯ
โo 1o) โ (ฯ โo ๐ฅ))) |
209 | 203, 208 | mpd 15 |
. . . . . . . . . . . . . . . . . . 19
โข
((((((((๐ด โ
๐ต โง โ
โ
๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โง
๐ฅ โ On) โง ๐ฆ โ (ฯ โ
1o)) โง ๐ง
โ (ฯ โo ๐ฅ)) โง (((ฯ โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ด) โ (ฯ โo
1o) โ (ฯ โo ๐ฅ)) |
210 | 163, 209 | eqsstrrid 3994 |
. . . . . . . . . . . . . . . . . 18
โข
((((((((๐ด โ
๐ต โง โ
โ
๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โง
๐ฅ โ On) โง ๐ฆ โ (ฯ โ
1o)) โง ๐ง
โ (ฯ โo ๐ฅ)) โง (((ฯ โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ด) โ ฯ โ (ฯ
โo ๐ฅ)) |
211 | 161, 210 | sstrd 3955 |
. . . . . . . . . . . . . . . . 17
โข
((((((((๐ด โ
๐ต โง โ
โ
๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โง
๐ฅ โ On) โง ๐ฆ โ (ฯ โ
1o)) โง ๐ง
โ (ฯ โo ๐ฅ)) โง (((ฯ โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ด) โ suc ๐ฆ โ (ฯ โo ๐ฅ)) |
212 | | onsuc 7747 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ฆ โ On โ suc ๐ฆ โ On) |
213 | 111, 212 | syl 17 |
. . . . . . . . . . . . . . . . . 18
โข
((((((((๐ด โ
๐ต โง โ
โ
๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โง
๐ฅ โ On) โง ๐ฆ โ (ฯ โ
1o)) โง ๐ง
โ (ฯ โo ๐ฅ)) โง (((ฯ โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ด) โ suc ๐ฆ โ On) |
214 | | omwordi 8519 |
. . . . . . . . . . . . . . . . . 18
โข ((suc
๐ฆ โ On โง (ฯ
โo ๐ฅ)
โ On โง (ฯ โo ๐ฅ) โ On) โ (suc ๐ฆ โ (ฯ โo ๐ฅ) โ ((ฯ
โo ๐ฅ)
ยทo suc ๐ฆ)
โ ((ฯ โo ๐ฅ) ยทo (ฯ
โo ๐ฅ)))) |
215 | 213, 107,
107, 214 | syl3anc 1372 |
. . . . . . . . . . . . . . . . 17
โข
((((((((๐ด โ
๐ต โง โ
โ
๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โง
๐ฅ โ On) โง ๐ฆ โ (ฯ โ
1o)) โง ๐ง
โ (ฯ โo ๐ฅ)) โง (((ฯ โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ด) โ (suc ๐ฆ โ (ฯ โo ๐ฅ) โ ((ฯ
โo ๐ฅ)
ยทo suc ๐ฆ)
โ ((ฯ โo ๐ฅ) ยทo (ฯ
โo ๐ฅ)))) |
216 | 211, 215 | mpd 15 |
. . . . . . . . . . . . . . . 16
โข
((((((((๐ด โ
๐ต โง โ
โ
๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โง
๐ฅ โ On) โง ๐ฆ โ (ฯ โ
1o)) โง ๐ง
โ (ฯ โo ๐ฅ)) โง (((ฯ โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ด) โ ((ฯ โo ๐ฅ) ยทo suc ๐ฆ) โ ((ฯ
โo ๐ฅ)
ยทo (ฯ โo ๐ฅ))) |
217 | 157, 216 | sstrd 3955 |
. . . . . . . . . . . . . . 15
โข
((((((((๐ด โ
๐ต โง โ
โ
๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โง
๐ฅ โ On) โง ๐ฆ โ (ฯ โ
1o)) โง ๐ง
โ (ฯ โo ๐ฅ)) โง (((ฯ โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ด) โ (((ฯ โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) โ ((ฯ
โo ๐ฅ)
ยทo (ฯ โo ๐ฅ))) |
218 | 127 | eqcomd 2739 |
. . . . . . . . . . . . . . 15
โข
((((((((๐ด โ
๐ต โง โ
โ
๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โง
๐ฅ โ On) โง ๐ฆ โ (ฯ โ
1o)) โง ๐ง
โ (ฯ โo ๐ฅ)) โง (((ฯ โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ด) โ ๐ด = (((ฯ โo ๐ฅ) ยทo ๐ฆ) +o ๐ง)) |
219 | | oeoa 8545 |
. . . . . . . . . . . . . . . 16
โข ((ฯ
โ On โง ๐ฅ โ On
โง ๐ฅ โ On) โ
(ฯ โo (๐ฅ +o ๐ฅ)) = ((ฯ โo ๐ฅ) ยทo (ฯ
โo ๐ฅ))) |
220 | 33, 106, 106, 219 | mp3an2i 1467 |
. . . . . . . . . . . . . . 15
โข
((((((((๐ด โ
๐ต โง โ
โ
๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โง
๐ฅ โ On) โง ๐ฆ โ (ฯ โ
1o)) โง ๐ง
โ (ฯ โo ๐ฅ)) โง (((ฯ โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ด) โ (ฯ โo (๐ฅ +o ๐ฅ)) = ((ฯ
โo ๐ฅ)
ยทo (ฯ โo ๐ฅ))) |
221 | 217, 218,
220 | 3sstr4d 3992 |
. . . . . . . . . . . . . 14
โข
((((((((๐ด โ
๐ต โง โ
โ
๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โง
๐ฅ โ On) โง ๐ฆ โ (ฯ โ
1o)) โง ๐ง
โ (ฯ โo ๐ฅ)) โง (((ฯ โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ด) โ ๐ด โ (ฯ โo (๐ฅ +o ๐ฅ))) |
222 | | simpr3 1197 |
. . . . . . . . . . . . . . . . . . . 20
โข ((((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
(๐ฅ โ (ฯ
โo ๐ถ) โง
(ฯ โช (ฯ โo ๐ฅ)) โ ๐ด โง ๐ด โ (ฯ โo (๐ฅ +o ๐ฅ)))) โ ๐ด โ (ฯ โo (๐ฅ +o ๐ฅ))) |
223 | 59 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
(๐ฅ โ (ฯ
โo ๐ถ) โง
(ฯ โช (ฯ โo ๐ฅ)) โ ๐ด โง ๐ด โ (ฯ โo (๐ฅ +o ๐ฅ)))) โ ๐ด โ On) |
224 | | simprr 772 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โ
๐ถ โ
On) |
225 | | simp1 1137 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ฅ โ (ฯ
โo ๐ถ) โง
(ฯ โช (ฯ โo ๐ฅ)) โ ๐ด โง ๐ด โ (ฯ โo (๐ฅ +o ๐ฅ))) โ ๐ฅ โ (ฯ โo ๐ถ)) |
226 | 224, 225 | anim12i 614 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
(๐ฅ โ (ฯ
โo ๐ถ) โง
(ฯ โช (ฯ โo ๐ฅ)) โ ๐ด โง ๐ด โ (ฯ โo (๐ฅ +o ๐ฅ)))) โ (๐ถ โ On โง ๐ฅ โ (ฯ โo ๐ถ))) |
227 | | onelon 6343 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข
(((ฯ โo ๐ถ) โ On โง ๐ฅ โ (ฯ โo ๐ถ)) โ ๐ฅ โ On) |
228 | 35, 227 | sylan 581 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข ((๐ถ โ On โง ๐ฅ โ (ฯ
โo ๐ถ))
โ ๐ฅ โ
On) |
229 | | pm4.24 565 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (๐ฅ โ On โ (๐ฅ โ On โง ๐ฅ โ On)) |
230 | 228, 229 | sylib 217 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((๐ถ โ On โง ๐ฅ โ (ฯ
โo ๐ถ))
โ (๐ฅ โ On โง
๐ฅ โ
On)) |
231 | | oacl 8482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((๐ฅ โ On โง ๐ฅ โ On) โ (๐ฅ +o ๐ฅ) โ On) |
232 | 230, 231 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ถ โ On โง ๐ฅ โ (ฯ
โo ๐ถ))
โ (๐ฅ +o
๐ฅ) โ
On) |
233 | | oecl 8484 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((ฯ
โ On โง (๐ฅ
+o ๐ฅ) โ On)
โ (ฯ โo (๐ฅ +o ๐ฅ)) โ On) |
234 | 33, 232, 233 | sylancr 588 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ถ โ On โง ๐ฅ โ (ฯ
โo ๐ถ))
โ (ฯ โo (๐ฅ +o ๐ฅ)) โ On) |
235 | 226, 234 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
(๐ฅ โ (ฯ
โo ๐ถ) โง
(ฯ โช (ฯ โo ๐ฅ)) โ ๐ด โง ๐ด โ (ฯ โo (๐ฅ +o ๐ฅ)))) โ (ฯ
โo (๐ฅ
+o ๐ฅ)) โ
On) |
236 | 55 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
(๐ฅ โ (ฯ
โo ๐ถ) โง
(ฯ โช (ฯ โo ๐ฅ)) โ ๐ด โง ๐ด โ (ฯ โo (๐ฅ +o ๐ฅ)))) โ (ฯ
โo (ฯ โo ๐ถ)) โ On) |
237 | | omwordri 8520 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ด โ On โง (ฯ
โo (๐ฅ
+o ๐ฅ)) โ On
โง (ฯ โo (ฯ โo ๐ถ)) โ On) โ (๐ด โ (ฯ โo (๐ฅ +o ๐ฅ)) โ (๐ด ยทo (ฯ
โo (ฯ โo ๐ถ))) โ ((ฯ โo
(๐ฅ +o ๐ฅ)) ยทo (ฯ
โo (ฯ โo ๐ถ))))) |
238 | 223, 235,
236, 237 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . 20
โข ((((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
(๐ฅ โ (ฯ
โo ๐ถ) โง
(ฯ โช (ฯ โo ๐ฅ)) โ ๐ด โง ๐ด โ (ฯ โo (๐ฅ +o ๐ฅ)))) โ (๐ด โ (ฯ โo (๐ฅ +o ๐ฅ)) โ (๐ด ยทo (ฯ
โo (ฯ โo ๐ถ))) โ ((ฯ โo
(๐ฅ +o ๐ฅ)) ยทo (ฯ
โo (ฯ โo ๐ถ))))) |
239 | 222, 238 | mpd 15 |
. . . . . . . . . . . . . . . . . . 19
โข ((((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
(๐ฅ โ (ฯ
โo ๐ถ) โง
(ฯ โช (ฯ โo ๐ฅ)) โ ๐ด โง ๐ด โ (ฯ โo (๐ฅ +o ๐ฅ)))) โ (๐ด ยทo (ฯ
โo (ฯ โo ๐ถ))) โ ((ฯ โo
(๐ฅ +o ๐ฅ)) ยทo (ฯ
โo (ฯ โo ๐ถ)))) |
240 | 226, 230,
231 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
(๐ฅ โ (ฯ
โo ๐ถ) โง
(ฯ โช (ฯ โo ๐ฅ)) โ ๐ด โง ๐ด โ (ฯ โo (๐ฅ +o ๐ฅ)))) โ (๐ฅ +o ๐ฅ) โ On) |
241 | 36 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
(๐ฅ โ (ฯ
โo ๐ถ) โง
(ฯ โช (ฯ โo ๐ฅ)) โ ๐ด โง ๐ด โ (ฯ โo (๐ฅ +o ๐ฅ)))) โ (ฯ
โo ๐ถ)
โ On) |
242 | | oeoa 8545 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((ฯ
โ On โง (๐ฅ
+o ๐ฅ) โ On
โง (ฯ โo ๐ถ) โ On) โ (ฯ
โo ((๐ฅ
+o ๐ฅ)
+o (ฯ โo ๐ถ))) = ((ฯ โo (๐ฅ +o ๐ฅ)) ยทo (ฯ
โo (ฯ โo ๐ถ)))) |
243 | 33, 240, 241, 242 | mp3an2i 1467 |
. . . . . . . . . . . . . . . . . . . 20
โข ((((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
(๐ฅ โ (ฯ
โo ๐ถ) โง
(ฯ โช (ฯ โo ๐ฅ)) โ ๐ด โง ๐ด โ (ฯ โo (๐ฅ +o ๐ฅ)))) โ (ฯ
โo ((๐ฅ
+o ๐ฅ)
+o (ฯ โo ๐ถ))) = ((ฯ โo (๐ฅ +o ๐ฅ)) ยทo (ฯ
โo (ฯ โo ๐ถ)))) |
244 | 226, 228 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
(๐ฅ โ (ฯ
โo ๐ถ) โง
(ฯ โช (ฯ โo ๐ฅ)) โ ๐ด โง ๐ด โ (ฯ โo (๐ฅ +o ๐ฅ)))) โ ๐ฅ โ On) |
245 | | oaass 8509 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ฅ โ On โง ๐ฅ โ On โง (ฯ
โo ๐ถ)
โ On) โ ((๐ฅ
+o ๐ฅ)
+o (ฯ โo ๐ถ)) = (๐ฅ +o (๐ฅ +o (ฯ โo
๐ถ)))) |
246 | 244, 244,
241, 245 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
(๐ฅ โ (ฯ
โo ๐ถ) โง
(ฯ โช (ฯ โo ๐ฅ)) โ ๐ด โง ๐ด โ (ฯ โo (๐ฅ +o ๐ฅ)))) โ ((๐ฅ +o ๐ฅ) +o (ฯ โo
๐ถ)) = (๐ฅ +o (๐ฅ +o (ฯ โo
๐ถ)))) |
247 | | simpr1 1195 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
(๐ฅ โ (ฯ
โo ๐ถ) โง
(ฯ โช (ฯ โo ๐ฅ)) โ ๐ด โง ๐ด โ (ฯ โo (๐ฅ +o ๐ฅ)))) โ ๐ฅ โ (ฯ โo ๐ถ)) |
248 | | ssidd 3968 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
(๐ฅ โ (ฯ
โo ๐ถ) โง
(ฯ โช (ฯ โo ๐ฅ)) โ ๐ด โง ๐ด โ (ฯ โo (๐ฅ +o ๐ฅ)))) โ (ฯ
โo ๐ถ)
โ (ฯ โo ๐ถ)) |
249 | | oaabs2 8596 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (((๐ฅ โ (ฯ
โo ๐ถ) โง
(ฯ โo ๐ถ) โ On) โง (ฯ
โo ๐ถ)
โ (ฯ โo ๐ถ)) โ (๐ฅ +o (ฯ โo
๐ถ)) = (ฯ
โo ๐ถ)) |
250 | 247, 241,
248, 249 | syl21anc 837 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
(๐ฅ โ (ฯ
โo ๐ถ) โง
(ฯ โช (ฯ โo ๐ฅ)) โ ๐ด โง ๐ด โ (ฯ โo (๐ฅ +o ๐ฅ)))) โ (๐ฅ +o (ฯ โo
๐ถ)) = (ฯ
โo ๐ถ)) |
251 | 250 | oveq2d 7374 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
(๐ฅ โ (ฯ
โo ๐ถ) โง
(ฯ โช (ฯ โo ๐ฅ)) โ ๐ด โง ๐ด โ (ฯ โo (๐ฅ +o ๐ฅ)))) โ (๐ฅ +o (๐ฅ +o (ฯ โo
๐ถ))) = (๐ฅ +o (ฯ โo
๐ถ))) |
252 | 246, 251,
250 | 3eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
(๐ฅ โ (ฯ
โo ๐ถ) โง
(ฯ โช (ฯ โo ๐ฅ)) โ ๐ด โง ๐ด โ (ฯ โo (๐ฅ +o ๐ฅ)))) โ ((๐ฅ +o ๐ฅ) +o (ฯ โo
๐ถ)) = (ฯ
โo ๐ถ)) |
253 | 252 | oveq2d 7374 |
. . . . . . . . . . . . . . . . . . . 20
โข ((((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
(๐ฅ โ (ฯ
โo ๐ถ) โง
(ฯ โช (ฯ โo ๐ฅ)) โ ๐ด โง ๐ด โ (ฯ โo (๐ฅ +o ๐ฅ)))) โ (ฯ
โo ((๐ฅ
+o ๐ฅ)
+o (ฯ โo ๐ถ))) = (ฯ โo (ฯ
โo ๐ถ))) |
254 | 243, 253 | eqtr3d 2775 |
. . . . . . . . . . . . . . . . . . 19
โข ((((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
(๐ฅ โ (ฯ
โo ๐ถ) โง
(ฯ โช (ฯ โo ๐ฅ)) โ ๐ด โง ๐ด โ (ฯ โo (๐ฅ +o ๐ฅ)))) โ ((ฯ
โo (๐ฅ
+o ๐ฅ))
ยทo (ฯ โo (ฯ โo
๐ถ))) = (ฯ
โo (ฯ โo ๐ถ))) |
255 | 239, 254 | sseqtrd 3985 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
(๐ฅ โ (ฯ
โo ๐ถ) โง
(ฯ โช (ฯ โo ๐ฅ)) โ ๐ด โง ๐ด โ (ฯ โo (๐ฅ +o ๐ฅ)))) โ (๐ด ยทo (ฯ
โo (ฯ โo ๐ถ))) โ (ฯ โo
(ฯ โo ๐ถ))) |
256 | | oveq2 7366 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (๐ฅ = โ
โ (ฯ
โo ๐ฅ) =
(ฯ โo โ
)) |
257 | 256, 167 | eqtrdi 2789 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (๐ฅ = โ
โ (ฯ
โo ๐ฅ) =
1o) |
258 | 257 | uneq2d 4124 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ฅ = โ
โ (ฯ โช
(ฯ โo ๐ฅ)) = (ฯ โช
1o)) |
259 | 33 | oneluni 6437 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข
(1o โ ฯ โ (ฯ โช 1o) =
ฯ) |
260 | 63, 259 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (ฯ
โช 1o) = ฯ |
261 | 260, 163 | eqtr4i 2764 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (ฯ
โช 1o) = (ฯ โo
1o) |
262 | 258, 261 | eqtrdi 2789 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ฅ = โ
โ (ฯ โช
(ฯ โo ๐ฅ)) = (ฯ โo
1o)) |
263 | 262 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . 22
โข
(((((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
(๐ฅ โ (ฯ
โo ๐ถ) โง
(ฯ โช (ฯ โo ๐ฅ)) โ ๐ด โง ๐ด โ (ฯ โo (๐ฅ +o ๐ฅ)))) โง ๐ฅ = โ
) โ (ฯ โช (ฯ
โo ๐ฅ)) =
(ฯ โo 1o)) |
264 | 263 | oveq1d 7373 |
. . . . . . . . . . . . . . . . . . . . 21
โข
(((((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
(๐ฅ โ (ฯ
โo ๐ถ) โง
(ฯ โช (ฯ โo ๐ฅ)) โ ๐ด โง ๐ด โ (ฯ โo (๐ฅ +o ๐ฅ)))) โง ๐ฅ = โ
) โ ((ฯ โช (ฯ
โo ๐ฅ))
ยทo (ฯ โo (ฯ โo
๐ถ))) = ((ฯ
โo 1o) ยทo (ฯ
โo (ฯ โo ๐ถ)))) |
265 | 224 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข
(((((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
(๐ฅ โ (ฯ
โo ๐ถ) โง
(ฯ โช (ฯ โo ๐ฅ)) โ ๐ด โง ๐ด โ (ฯ โo (๐ฅ +o ๐ฅ)))) โง ๐ฅ = โ
) โ ๐ถ โ On) |
266 | | oecl 8484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
โข ((ฯ
โ On โง โ
โ On) โ (ฯ โo โ
)
โ On) |
267 | 33, 73, 266 | mp2an 691 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
โข (ฯ
โo โ
) โ On |
268 | | oecl 8484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
โข ((ฯ
โ On โง (ฯ โo โ
) โ On) โ (ฯ
โo (ฯ โo โ
)) โ
On) |
269 | 33, 267, 268 | mp2an 691 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข (ฯ
โo (ฯ โo โ
)) โ
On |
270 | 269 | 2a1i 12 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข
(((((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
(๐ฅ โ (ฯ
โo ๐ถ) โง
(ฯ โช (ฯ โo ๐ฅ)) โ ๐ด โง ๐ด โ (ฯ โo (๐ฅ +o ๐ฅ)))) โง ๐ฅ = โ
) โ (๐ถ โ On โ (ฯ
โo (ฯ โo โ
)) โ
On)) |
271 | 270, 54 | jca2 515 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข
(((((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
(๐ฅ โ (ฯ
โo ๐ถ) โง
(ฯ โช (ฯ โo ๐ฅ)) โ ๐ด โง ๐ด โ (ฯ โo (๐ฅ +o ๐ฅ)))) โง ๐ฅ = โ
) โ (๐ถ โ On โ ((ฯ
โo (ฯ โo โ
)) โ On โง
(ฯ โo (ฯ โo ๐ถ)) โ On))) |
272 | 167 | oveq2i 7369 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
โข (ฯ
โo (ฯ โo โ
)) = (ฯ
โo 1o) |
273 | 272, 163 | eqtri 2761 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
โข (ฯ
โo (ฯ โo โ
)) =
ฯ |
274 | | ssun1 4133 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
โข ฯ
โ (ฯ โช (ฯ โo ๐ฅ)) |
275 | 273, 274 | eqsstri 3979 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
โข (ฯ
โo (ฯ โo โ
)) โ (ฯ โช
(ฯ โo ๐ฅ)) |
276 | | simp2 1138 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
โข ((๐ฅ โ (ฯ
โo ๐ถ) โง
(ฯ โช (ฯ โo ๐ฅ)) โ ๐ด โง ๐ด โ (ฯ โo (๐ฅ +o ๐ฅ))) โ (ฯ โช
(ฯ โo ๐ฅ)) โ ๐ด) |
277 | 275, 276 | sstrid 3956 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
โข ((๐ฅ โ (ฯ
โo ๐ถ) โง
(ฯ โช (ฯ โo ๐ฅ)) โ ๐ด โง ๐ด โ (ฯ โo (๐ฅ +o ๐ฅ))) โ (ฯ
โo (ฯ โo โ
)) โ ๐ด) |
278 | 277 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข ((((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
(๐ฅ โ (ฯ
โo ๐ถ) โง
(ฯ โช (ฯ โo ๐ฅ)) โ ๐ด โง ๐ด โ (ฯ โo (๐ฅ +o ๐ฅ)))) โ (ฯ
โo (ฯ โo โ
)) โ ๐ด) |
279 | 57 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
โข ((((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
(๐ฅ โ (ฯ
โo ๐ถ) โง
(ฯ โช (ฯ โo ๐ฅ)) โ ๐ด โง ๐ด โ (ฯ โo (๐ฅ +o ๐ฅ)))) โ ๐ด โ ๐ต) |
280 | | simplrl 776 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
โข ((((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
(๐ฅ โ (ฯ
โo ๐ถ) โง
(ฯ โช (ฯ โo ๐ฅ)) โ ๐ด โง ๐ด โ (ฯ โo (๐ฅ +o ๐ฅ)))) โ ๐ต = (ฯ โo (ฯ
โo ๐ถ))) |
281 | 279, 280 | eleqtrd 2836 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข ((((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
(๐ฅ โ (ฯ
โo ๐ถ) โง
(ฯ โช (ฯ โo ๐ฅ)) โ ๐ด โง ๐ด โ (ฯ โo (๐ฅ +o ๐ฅ)))) โ ๐ด โ (ฯ โo (ฯ
โo ๐ถ))) |
282 | 278, 281 | jca 513 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข ((((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
(๐ฅ โ (ฯ
โo ๐ถ) โง
(ฯ โช (ฯ โo ๐ฅ)) โ ๐ด โง ๐ด โ (ฯ โo (๐ฅ +o ๐ฅ)))) โ ((ฯ
โo (ฯ โo โ
)) โ ๐ด โง ๐ด โ (ฯ โo (ฯ
โo ๐ถ)))) |
283 | 282 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข
(((((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
(๐ฅ โ (ฯ
โo ๐ถ) โง
(ฯ โช (ฯ โo ๐ฅ)) โ ๐ด โง ๐ด โ (ฯ โo (๐ฅ +o ๐ฅ)))) โง ๐ฅ = โ
) โ ((ฯ
โo (ฯ โo โ
)) โ ๐ด โง ๐ด โ (ฯ โo (ฯ
โo ๐ถ)))) |
284 | | ontr2 6365 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข
(((ฯ โo (ฯ โo โ
))
โ On โง (ฯ โo (ฯ โo ๐ถ)) โ On) โ (((ฯ
โo (ฯ โo โ
)) โ ๐ด โง ๐ด โ (ฯ โo (ฯ
โo ๐ถ)))
โ (ฯ โo (ฯ โo โ
)) โ
(ฯ โo (ฯ โo ๐ถ)))) |
285 | 271, 283,
284 | syl6ci 71 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข
(((((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
(๐ฅ โ (ฯ
โo ๐ถ) โง
(ฯ โช (ฯ โo ๐ฅ)) โ ๐ด โง ๐ด โ (ฯ โo (๐ฅ +o ๐ฅ)))) โง ๐ฅ = โ
) โ (๐ถ โ On โ (ฯ
โo (ฯ โo โ
)) โ (ฯ
โo (ฯ โo ๐ถ)))) |
286 | | oeord 8536 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข ((โ
โ On โง ๐ถ โ On
โง ฯ โ (On โ 2o)) โ (โ
โ ๐ถ โ (ฯ
โo โ
) โ (ฯ โo ๐ถ))) |
287 | 73, 65, 286 | mp3an13 1453 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข (๐ถ โ On โ (โ
โ ๐ถ โ (ฯ
โo โ
) โ (ฯ โo ๐ถ))) |
288 | 65 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข (๐ถ โ On โ ฯ โ
(On โ 2o)) |
289 | | oeord 8536 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข
(((ฯ โo โ
) โ On โง (ฯ
โo ๐ถ)
โ On โง ฯ โ (On โ 2o)) โ ((ฯ
โo โ
) โ (ฯ โo ๐ถ) โ (ฯ
โo (ฯ โo โ
)) โ (ฯ
โo (ฯ โo ๐ถ)))) |
290 | 267, 35, 288, 289 | mp3an2i 1467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข (๐ถ โ On โ ((ฯ
โo โ
) โ (ฯ โo ๐ถ) โ (ฯ
โo (ฯ โo โ
)) โ (ฯ
โo (ฯ โo ๐ถ)))) |
291 | 287, 290 | bitrd 279 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (๐ถ โ On โ (โ
โ ๐ถ โ (ฯ
โo (ฯ โo โ
)) โ (ฯ
โo (ฯ โo ๐ถ)))) |
292 | 291 | biimprd 248 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (๐ถ โ On โ ((ฯ
โo (ฯ โo โ
)) โ (ฯ
โo (ฯ โo ๐ถ)) โ โ
โ ๐ถ)) |
293 | 285, 292 | sylcom 30 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข
(((((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
(๐ฅ โ (ฯ
โo ๐ถ) โง
(ฯ โช (ฯ โo ๐ฅ)) โ ๐ด โง ๐ด โ (ฯ โo (๐ฅ +o ๐ฅ)))) โง ๐ฅ = โ
) โ (๐ถ โ On โ โ
โ ๐ถ)) |
294 | | eloni 6328 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (๐ถ โ On โ Ord ๐ถ) |
295 | | ordsucss 7754 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (Ord
๐ถ โ (โ
โ
๐ถ โ suc โ
โ ๐ถ)) |
296 | 94 | sseq1i 3973 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข
(1o โ ๐ถ โ suc โ
โ ๐ถ) |
297 | 295, 296 | syl6ibr 252 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (Ord
๐ถ โ (โ
โ
๐ถ โ 1o
โ ๐ถ)) |
298 | 294, 297 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ถ โ On โ (โ
โ ๐ถ โ
1o โ ๐ถ)) |
299 | 293, 298 | sylcom 30 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข
(((((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
(๐ฅ โ (ฯ
โo ๐ถ) โง
(ฯ โช (ฯ โo ๐ฅ)) โ ๐ด โง ๐ด โ (ฯ โo (๐ฅ +o ๐ฅ)))) โง ๐ฅ = โ
) โ (๐ถ โ On โ 1o โ
๐ถ)) |
300 | 265, 299 | jcai 518 |
. . . . . . . . . . . . . . . . . . . . . 22
โข
(((((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
(๐ฅ โ (ฯ
โo ๐ถ) โง
(ฯ โช (ฯ โo ๐ฅ)) โ ๐ด โง ๐ด โ (ฯ โo (๐ฅ +o ๐ฅ)))) โง ๐ฅ = โ
) โ (๐ถ โ On โง 1o โ ๐ถ)) |
301 | 33 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (๐ถ โ On โ ฯ โ
On) |
302 | 80 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (๐ถ โ On โ 1o
โ On) |
303 | 301, 302,
35 | 3jca 1129 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (๐ถ โ On โ (ฯ
โ On โง 1o โ On โง (ฯ โo ๐ถ) โ On)) |
304 | 303 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((๐ถ โ On โง 1o
โ ๐ถ) โ (ฯ
โ On โง 1o โ On โง (ฯ โo ๐ถ) โ On)) |
305 | | oeoa 8545 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((ฯ
โ On โง 1o โ On โง (ฯ โo ๐ถ) โ On) โ (ฯ
โo (1o +o (ฯ โo
๐ถ))) = ((ฯ
โo 1o) ยทo (ฯ
โo (ฯ โo ๐ถ)))) |
306 | 304, 305 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ถ โ On โง 1o
โ ๐ถ) โ (ฯ
โo (1o +o (ฯ โo
๐ถ))) = ((ฯ
โo 1o) ยทo (ฯ
โo (ฯ โo ๐ถ)))) |
307 | 63 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข ((๐ถ โ On โง 1o
โ ๐ถ) โ
1o โ ฯ) |
308 | 35 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข ((๐ถ โ On โง 1o
โ ๐ถ) โ (ฯ
โo ๐ถ)
โ On) |
309 | | oeword 8538 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข
((1o โ On โง ๐ถ โ On โง ฯ โ (On โ
2o)) โ (1o โ ๐ถ โ (ฯ โo
1o) โ (ฯ โo ๐ถ))) |
310 | 80, 65, 309 | mp3an13 1453 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข (๐ถ โ On โ (1o
โ ๐ถ โ (ฯ
โo 1o) โ (ฯ โo ๐ถ))) |
311 | 310 | biimpa 478 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข ((๐ถ โ On โง 1o
โ ๐ถ) โ (ฯ
โo 1o) โ (ฯ โo ๐ถ)) |
312 | 163, 311 | eqsstrrid 3994 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข ((๐ถ โ On โง 1o
โ ๐ถ) โ ฯ
โ (ฯ โo ๐ถ)) |
313 | | oaabs 8595 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข
(((1o โ ฯ โง (ฯ โo ๐ถ) โ On) โง ฯ
โ (ฯ โo ๐ถ)) โ (1o +o
(ฯ โo ๐ถ)) = (ฯ โo ๐ถ)) |
314 | 307, 308,
312, 313 | syl21anc 837 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((๐ถ โ On โง 1o
โ ๐ถ) โ
(1o +o (ฯ โo ๐ถ)) = (ฯ โo ๐ถ)) |
315 | 314 | oveq2d 7374 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ถ โ On โง 1o
โ ๐ถ) โ (ฯ
โo (1o +o (ฯ โo
๐ถ))) = (ฯ
โo (ฯ โo ๐ถ))) |
316 | 306, 315 | eqtr3d 2775 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ถ โ On โง 1o
โ ๐ถ) โ ((ฯ
โo 1o) ยทo (ฯ
โo (ฯ โo ๐ถ))) = (ฯ โo (ฯ
โo ๐ถ))) |
317 | 300, 316 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
โข
(((((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
(๐ฅ โ (ฯ
โo ๐ถ) โง
(ฯ โช (ฯ โo ๐ฅ)) โ ๐ด โง ๐ด โ (ฯ โo (๐ฅ +o ๐ฅ)))) โง ๐ฅ = โ
) โ ((ฯ
โo 1o) ยทo (ฯ
โo (ฯ โo ๐ถ))) = (ฯ โo (ฯ
โo ๐ถ))) |
318 | 264, 317 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . 20
โข
(((((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
(๐ฅ โ (ฯ
โo ๐ถ) โง
(ฯ โช (ฯ โo ๐ฅ)) โ ๐ด โง ๐ด โ (ฯ โo (๐ฅ +o ๐ฅ)))) โง ๐ฅ = โ
) โ ((ฯ โช (ฯ
โo ๐ฅ))
ยทo (ฯ โo (ฯ โo
๐ถ))) = (ฯ
โo (ฯ โo ๐ถ))) |
319 | 244, 195,
196 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข ((((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
(๐ฅ โ (ฯ
โo ๐ถ) โง
(ฯ โช (ฯ โo ๐ฅ)) โ ๐ด โง ๐ด โ (ฯ โo (๐ฅ +o ๐ฅ)))) โ (โ
โ
๐ฅ โ suc โ
โ ๐ฅ)) |
320 | 319 | imp 408 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข
(((((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
(๐ฅ โ (ฯ
โo ๐ถ) โง
(ฯ โช (ฯ โo ๐ฅ)) โ ๐ด โง ๐ด โ (ฯ โo (๐ฅ +o ๐ฅ)))) โง โ
โ ๐ฅ) โ suc โ
โ
๐ฅ) |
321 | 94, 320 | eqsstrid 3993 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข
(((((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
(๐ฅ โ (ฯ
โo ๐ถ) โง
(ฯ โช (ฯ โo ๐ฅ)) โ ๐ด โง ๐ด โ (ฯ โo (๐ฅ +o ๐ฅ)))) โง โ
โ ๐ฅ) โ 1o โ
๐ฅ) |
322 | 247 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข
(((((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
(๐ฅ โ (ฯ
โo ๐ถ) โง
(ฯ โช (ฯ โo ๐ฅ)) โ ๐ด โง ๐ด โ (ฯ โo (๐ฅ +o ๐ฅ)))) โง โ
โ ๐ฅ) โ ๐ฅ โ (ฯ โo ๐ถ)) |
323 | 241, 322,
227 | syl2an2r 684 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข
(((((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
(๐ฅ โ (ฯ
โo ๐ถ) โง
(ฯ โช (ฯ โo ๐ฅ)) โ ๐ด โง ๐ด โ (ฯ โo (๐ฅ +o ๐ฅ)))) โง โ
โ ๐ฅ) โ ๐ฅ โ On) |
324 | 65 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข
(((((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
(๐ฅ โ (ฯ
โo ๐ถ) โง
(ฯ โช (ฯ โo ๐ฅ)) โ ๐ด โง ๐ด โ (ฯ โo (๐ฅ +o ๐ฅ)))) โง โ
โ ๐ฅ) โ ฯ โ (On
โ 2o)) |
325 | | oeword 8538 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข
((1o โ On โง ๐ฅ โ On โง ฯ โ (On โ
2o)) โ (1o โ ๐ฅ โ (ฯ โo
1o) โ (ฯ โo ๐ฅ))) |
326 | 80, 323, 324, 325 | mp3an2i 1467 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข
(((((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
(๐ฅ โ (ฯ
โo ๐ถ) โง
(ฯ โช (ฯ โo ๐ฅ)) โ ๐ด โง ๐ด โ (ฯ โo (๐ฅ +o ๐ฅ)))) โง โ
โ ๐ฅ) โ (1o โ
๐ฅ โ (ฯ
โo 1o) โ (ฯ โo ๐ฅ))) |
327 | 321, 326 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข
(((((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
(๐ฅ โ (ฯ
โo ๐ถ) โง
(ฯ โช (ฯ โo ๐ฅ)) โ ๐ด โง ๐ด โ (ฯ โo (๐ฅ +o ๐ฅ)))) โง โ
โ ๐ฅ) โ (ฯ
โo 1o) โ (ฯ โo ๐ฅ)) |
328 | 163, 327 | eqsstrrid 3994 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข
(((((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
(๐ฅ โ (ฯ
โo ๐ถ) โง
(ฯ โช (ฯ โo ๐ฅ)) โ ๐ด โง ๐ด โ (ฯ โo (๐ฅ +o ๐ฅ)))) โง โ
โ ๐ฅ) โ ฯ โ
(ฯ โo ๐ฅ)) |
329 | | ssequn1 4141 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (ฯ
โ (ฯ โo ๐ฅ) โ (ฯ โช (ฯ
โo ๐ฅ)) =
(ฯ โo ๐ฅ)) |
330 | 328, 329 | sylib 217 |
. . . . . . . . . . . . . . . . . . . . . 22
โข
(((((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
(๐ฅ โ (ฯ
โo ๐ถ) โง
(ฯ โช (ฯ โo ๐ฅ)) โ ๐ด โง ๐ด โ (ฯ โo (๐ฅ +o ๐ฅ)))) โง โ
โ ๐ฅ) โ (ฯ โช (ฯ
โo ๐ฅ)) =
(ฯ โo ๐ฅ)) |
331 | 330 | oveq1d 7373 |
. . . . . . . . . . . . . . . . . . . . 21
โข
(((((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
(๐ฅ โ (ฯ
โo ๐ถ) โง
(ฯ โช (ฯ โo ๐ฅ)) โ ๐ด โง ๐ด โ (ฯ โo (๐ฅ +o ๐ฅ)))) โง โ
โ ๐ฅ) โ ((ฯ โช
(ฯ โo ๐ฅ)) ยทo (ฯ
โo (ฯ โo ๐ถ))) = ((ฯ โo ๐ฅ) ยทo (ฯ
โo (ฯ โo ๐ถ)))) |
332 | 241 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . 22
โข
(((((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
(๐ฅ โ (ฯ
โo ๐ถ) โง
(ฯ โช (ฯ โo ๐ฅ)) โ ๐ด โง ๐ด โ (ฯ โo (๐ฅ +o ๐ฅ)))) โง โ
โ ๐ฅ) โ (ฯ
โo ๐ถ)
โ On) |
333 | | oeoa 8545 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((ฯ
โ On โง ๐ฅ โ On
โง (ฯ โo ๐ถ) โ On) โ (ฯ
โo (๐ฅ
+o (ฯ โo ๐ถ))) = ((ฯ โo ๐ฅ) ยทo (ฯ
โo (ฯ โo ๐ถ)))) |
334 | 33, 323, 332, 333 | mp3an2i 1467 |
. . . . . . . . . . . . . . . . . . . . 21
โข
(((((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
(๐ฅ โ (ฯ
โo ๐ถ) โง
(ฯ โช (ฯ โo ๐ฅ)) โ ๐ด โง ๐ด โ (ฯ โo (๐ฅ +o ๐ฅ)))) โง โ
โ ๐ฅ) โ (ฯ
โo (๐ฅ
+o (ฯ โo ๐ถ))) = ((ฯ โo ๐ฅ) ยทo (ฯ
โo (ฯ โo ๐ถ)))) |
335 | | ssidd 3968 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข
(((((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
(๐ฅ โ (ฯ
โo ๐ถ) โง
(ฯ โช (ฯ โo ๐ฅ)) โ ๐ด โง ๐ด โ (ฯ โo (๐ฅ +o ๐ฅ)))) โง โ
โ ๐ฅ) โ (ฯ
โo ๐ถ)
โ (ฯ โo ๐ถ)) |
336 | 322, 332,
335, 249 | syl21anc 837 |
. . . . . . . . . . . . . . . . . . . . . 22
โข
(((((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
(๐ฅ โ (ฯ
โo ๐ถ) โง
(ฯ โช (ฯ โo ๐ฅ)) โ ๐ด โง ๐ด โ (ฯ โo (๐ฅ +o ๐ฅ)))) โง โ
โ ๐ฅ) โ (๐ฅ +o (ฯ โo
๐ถ)) = (ฯ
โo ๐ถ)) |
337 | 336 | oveq2d 7374 |
. . . . . . . . . . . . . . . . . . . . 21
โข
(((((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
(๐ฅ โ (ฯ
โo ๐ถ) โง
(ฯ โช (ฯ โo ๐ฅ)) โ ๐ด โง ๐ด โ (ฯ โo (๐ฅ +o ๐ฅ)))) โง โ
โ ๐ฅ) โ (ฯ
โo (๐ฅ
+o (ฯ โo ๐ถ))) = (ฯ โo (ฯ
โo ๐ถ))) |
338 | 331, 334,
337 | 3eqtr2d 2779 |
. . . . . . . . . . . . . . . . . . . 20
โข
(((((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
(๐ฅ โ (ฯ
โo ๐ถ) โง
(ฯ โช (ฯ โo ๐ฅ)) โ ๐ด โง ๐ด โ (ฯ โo (๐ฅ +o ๐ฅ)))) โง โ
โ ๐ฅ) โ ((ฯ โช
(ฯ โo ๐ฅ)) ยทo (ฯ
โo (ฯ โo ๐ถ))) = (ฯ โo (ฯ
โo ๐ถ))) |
339 | 226, 228,
201 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . 20
โข ((((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
(๐ฅ โ (ฯ
โo ๐ถ) โง
(ฯ โช (ฯ โo ๐ฅ)) โ ๐ด โง ๐ด โ (ฯ โo (๐ฅ +o ๐ฅ)))) โ (๐ฅ = โ
โจ โ
โ ๐ฅ)) |
340 | 318, 338,
339 | mpjaodan 958 |
. . . . . . . . . . . . . . . . . . 19
โข ((((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
(๐ฅ โ (ฯ
โo ๐ถ) โง
(ฯ โช (ฯ โo ๐ฅ)) โ ๐ด โง ๐ด โ (ฯ โo (๐ฅ +o ๐ฅ)))) โ ((ฯ โช
(ฯ โo ๐ฅ)) ยทo (ฯ
โo (ฯ โo ๐ถ))) = (ฯ โo (ฯ
โo ๐ถ))) |
341 | 276 | adantl 483 |
. . . . . . . . . . . . . . . . . . . 20
โข ((((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
(๐ฅ โ (ฯ
โo ๐ถ) โง
(ฯ โช (ฯ โo ๐ฅ)) โ ๐ด โง ๐ด โ (ฯ โo (๐ฅ +o ๐ฅ)))) โ (ฯ โช
(ฯ โo ๐ฅ)) โ ๐ด) |
342 | 33, 228, 75 | sylancr 588 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ถ โ On โง ๐ฅ โ (ฯ
โo ๐ถ))
โ (ฯ โo ๐ฅ) โ On) |
343 | 342, 33 | jctil 521 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ถ โ On โง ๐ฅ โ (ฯ
โo ๐ถ))
โ (ฯ โ On โง (ฯ โo ๐ฅ) โ On)) |
344 | | onun2 6426 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((ฯ
โ On โง (ฯ โo ๐ฅ) โ On) โ (ฯ โช (ฯ
โo ๐ฅ))
โ On) |
345 | 226, 343,
344 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
(๐ฅ โ (ฯ
โo ๐ถ) โง
(ฯ โช (ฯ โo ๐ฅ)) โ ๐ด โง ๐ด โ (ฯ โo (๐ฅ +o ๐ฅ)))) โ (ฯ โช
(ฯ โo ๐ฅ)) โ On) |
346 | | omwordri 8520 |
. . . . . . . . . . . . . . . . . . . . 21
โข
(((ฯ โช (ฯ โo ๐ฅ)) โ On โง ๐ด โ On โง (ฯ โo
(ฯ โo ๐ถ)) โ On) โ ((ฯ โช
(ฯ โo ๐ฅ)) โ ๐ด โ ((ฯ โช (ฯ
โo ๐ฅ))
ยทo (ฯ โo (ฯ โo
๐ถ))) โ (๐ด ยทo (ฯ
โo (ฯ โo ๐ถ))))) |
347 | 345, 223,
236, 346 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . 20
โข ((((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
(๐ฅ โ (ฯ
โo ๐ถ) โง
(ฯ โช (ฯ โo ๐ฅ)) โ ๐ด โง ๐ด โ (ฯ โo (๐ฅ +o ๐ฅ)))) โ ((ฯ โช
(ฯ โo ๐ฅ)) โ ๐ด โ ((ฯ โช (ฯ
โo ๐ฅ))
ยทo (ฯ โo (ฯ โo
๐ถ))) โ (๐ด ยทo (ฯ
โo (ฯ โo ๐ถ))))) |
348 | 341, 347 | mpd 15 |
. . . . . . . . . . . . . . . . . . 19
โข ((((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
(๐ฅ โ (ฯ
โo ๐ถ) โง
(ฯ โช (ฯ โo ๐ฅ)) โ ๐ด โง ๐ด โ (ฯ โo (๐ฅ +o ๐ฅ)))) โ ((ฯ โช
(ฯ โo ๐ฅ)) ยทo (ฯ
โo (ฯ โo ๐ถ))) โ (๐ด ยทo (ฯ
โo (ฯ โo ๐ถ)))) |
349 | 340, 348 | eqsstrrd 3984 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
(๐ฅ โ (ฯ
โo ๐ถ) โง
(ฯ โช (ฯ โo ๐ฅ)) โ ๐ด โง ๐ด โ (ฯ โo (๐ฅ +o ๐ฅ)))) โ (ฯ
โo (ฯ โo ๐ถ)) โ (๐ด ยทo (ฯ
โo (ฯ โo ๐ถ)))) |
350 | 255, 349 | eqssd 3962 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
(๐ฅ โ (ฯ
โo ๐ถ) โง
(ฯ โช (ฯ โo ๐ฅ)) โ ๐ด โง ๐ด โ (ฯ โo (๐ฅ +o ๐ฅ)))) โ (๐ด ยทo (ฯ
โo (ฯ โo ๐ถ))) = (ฯ โo (ฯ
โo ๐ถ))) |
351 | 49 | ad2antlr 726 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
(๐ฅ โ (ฯ
โo ๐ถ) โง
(ฯ โช (ฯ โo ๐ฅ)) โ ๐ด โง ๐ด โ (ฯ โo (๐ฅ +o ๐ฅ)))) โ ((๐ด ยทo ๐ต) = ๐ต โ (๐ด ยทo (ฯ
โo (ฯ โo ๐ถ))) = (ฯ โo (ฯ
โo ๐ถ)))) |
352 | 350, 351 | mpbird 257 |
. . . . . . . . . . . . . . . 16
โข ((((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
(๐ฅ โ (ฯ
โo ๐ถ) โง
(ฯ โช (ฯ โo ๐ฅ)) โ ๐ด โง ๐ด โ (ฯ โo (๐ฅ +o ๐ฅ)))) โ (๐ด ยทo ๐ต) = ๐ต) |
353 | 352 | ex 414 |
. . . . . . . . . . . . . . 15
โข (((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โ
((๐ฅ โ (ฯ
โo ๐ถ) โง
(ฯ โช (ฯ โo ๐ฅ)) โ ๐ด โง ๐ด โ (ฯ โo (๐ฅ +o ๐ฅ))) โ (๐ด ยทo ๐ต) = ๐ต)) |
354 | 353 | ad5antr 733 |
. . . . . . . . . . . . . 14
โข
((((((((๐ด โ
๐ต โง โ
โ
๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โง
๐ฅ โ On) โง ๐ฆ โ (ฯ โ
1o)) โง ๐ง
โ (ฯ โo ๐ฅ)) โง (((ฯ โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ด) โ ((๐ฅ โ (ฯ โo ๐ถ) โง (ฯ โช (ฯ
โo ๐ฅ))
โ ๐ด โง ๐ด โ (ฯ
โo (๐ฅ
+o ๐ฅ))) โ
(๐ด ยทo
๐ต) = ๐ต)) |
355 | 141, 143,
221, 354 | mp3and 1465 |
. . . . . . . . . . . . 13
โข
((((((((๐ด โ
๐ต โง โ
โ
๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โง
๐ฅ โ On) โง ๐ฆ โ (ฯ โ
1o)) โง ๐ง
โ (ฯ โo ๐ฅ)) โง (((ฯ โo ๐ฅ) ยทo ๐ฆ) +o ๐ง) = ๐ด) โ (๐ด ยทo ๐ต) = ๐ต) |
356 | 355 | ex 414 |
. . . . . . . . . . . 12
โข
(((((((๐ด โ
๐ต โง โ
โ
๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โง
๐ฅ โ On) โง ๐ฆ โ (ฯ โ
1o)) โง ๐ง
โ (ฯ โo ๐ฅ)) โ ((((ฯ โo
๐ฅ) ยทo
๐ฆ) +o ๐ง) = ๐ด โ (๐ด ยทo ๐ต) = ๐ต)) |
357 | 71, 356 | syl5 34 |
. . . . . . . . . . 11
โข
(((((((๐ด โ
๐ต โง โ
โ
๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โง
๐ฅ โ On) โง ๐ฆ โ (ฯ โ
1o)) โง ๐ง
โ (ฯ โo ๐ฅ)) โ ((๐ค = โจ๐ฅ, ๐ฆ, ๐งโฉ โง (((ฯ โo
๐ฅ) ยทo
๐ฆ) +o ๐ง) = ๐ด) โ (๐ด ยทo ๐ต) = ๐ต)) |
358 | 357 | rexlimdva 3149 |
. . . . . . . . . 10
โข
((((((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โง
๐ฅ โ On) โง ๐ฆ โ (ฯ โ
1o)) โ (โ๐ง โ (ฯ โo ๐ฅ)(๐ค = โจ๐ฅ, ๐ฆ, ๐งโฉ โง (((ฯ โo
๐ฅ) ยทo
๐ฆ) +o ๐ง) = ๐ด) โ (๐ด ยทo ๐ต) = ๐ต)) |
359 | 358 | rexlimdva 3149 |
. . . . . . . . 9
โข
(((((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โง
๐ฅ โ On) โ
(โ๐ฆ โ (ฯ
โ 1o)โ๐ง โ (ฯ โo ๐ฅ)(๐ค = โจ๐ฅ, ๐ฆ, ๐งโฉ โง (((ฯ โo
๐ฅ) ยทo
๐ฆ) +o ๐ง) = ๐ด) โ (๐ด ยทo ๐ต) = ๐ต)) |
360 | 359 | rexlimdva 3149 |
. . . . . . . 8
โข ((((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โ
(โ๐ฅ โ On
โ๐ฆ โ (ฯ
โ 1o)โ๐ง โ (ฯ โo ๐ฅ)(๐ค = โจ๐ฅ, ๐ฆ, ๐งโฉ โง (((ฯ โo
๐ฅ) ยทo
๐ฆ) +o ๐ง) = ๐ด) โ (๐ด ยทo ๐ต) = ๐ต)) |
361 | 360 | exlimdv 1937 |
. . . . . . 7
โข ((((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โ
(โ๐คโ๐ฅ โ On โ๐ฆ โ (ฯ โ
1o)โ๐ง
โ (ฯ โo ๐ฅ)(๐ค = โจ๐ฅ, ๐ฆ, ๐งโฉ โง (((ฯ โo
๐ฅ) ยทo
๐ฆ) +o ๐ง) = ๐ด) โ (๐ด ยทo ๐ต) = ๐ต)) |
362 | 70, 361 | syl5 34 |
. . . . . 6
โข ((((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โ
(โ!๐คโ๐ฅ โ On โ๐ฆ โ (ฯ โ
1o)โ๐ง
โ (ฯ โo ๐ฅ)(๐ค = โจ๐ฅ, ๐ฆ, ๐งโฉ โง (((ฯ โo
๐ฅ) ยทo
๐ฆ) +o ๐ง) = ๐ด) โ (๐ด ยทo ๐ต) = ๐ต)) |
363 | 69, 362 | mpd 15 |
. . . . 5
โข ((((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โง
ฯ โ ๐ด) โ
(๐ด ยทo
๐ต) = ๐ต) |
364 | | eloni 6328 |
. . . . . . 7
โข (๐ด โ On โ Ord ๐ด) |
365 | 59, 364 | syl 17 |
. . . . . 6
โข (((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โ
Ord ๐ด) |
366 | | ordtri2or 6416 |
. . . . . 6
โข ((Ord
๐ด โง Ord ฯ) โ
(๐ด โ ฯ โจ
ฯ โ ๐ด)) |
367 | 365, 158,
366 | sylancl 587 |
. . . . 5
โข (((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โ
(๐ด โ ฯ โจ
ฯ โ ๐ด)) |
368 | 51, 363, 367 | mpjaodan 958 |
. . . 4
โข (((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โ
(๐ด ยทo
๐ต) = ๐ต) |
369 | 368 | ex 414 |
. . 3
โข ((๐ด โ ๐ต โง โ
โ ๐ด) โ ((๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On) โ
(๐ด ยทo
๐ต) = ๐ต)) |
370 | 6, 30, 369 | 3jaod 1429 |
. 2
โข ((๐ด โ ๐ต โง โ
โ ๐ด) โ ((๐ต = โ
โจ ๐ต = 2o โจ (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On)) โ
(๐ด ยทo
๐ต) = ๐ต)) |
371 | 370 | imp 408 |
1
โข (((๐ด โ ๐ต โง โ
โ ๐ด) โง (๐ต = โ
โจ ๐ต = 2o โจ (๐ต = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On))) โ
(๐ด ยทo
๐ต) = ๐ต) |