Step | Hyp | Ref
| Expression |
1 | | eltpi 4649 |
. . . . 5
โข (๐ถ โ {โ
, 1o,
2o} โ (๐ถ =
โ
โจ ๐ถ =
1o โจ ๐ถ =
2o)) |
2 | | df-3o 8415 |
. . . . . 6
โข
3o = suc 2o |
3 | | df2o3 8421 |
. . . . . . . 8
โข
2o = {โ
, 1o} |
4 | 3 | uneq1i 4120 |
. . . . . . 7
โข
(2o โช {2o}) = ({โ
, 1o} โช
{2o}) |
5 | | df-suc 6324 |
. . . . . . 7
โข suc
2o = (2o โช {2o}) |
6 | | df-tp 4592 |
. . . . . . 7
โข {โ
,
1o, 2o} = ({โ
, 1o} โช
{2o}) |
7 | 4, 5, 6 | 3eqtr4i 2771 |
. . . . . 6
โข suc
2o = {โ
, 1o, 2o} |
8 | 2, 7 | eqtri 2761 |
. . . . 5
โข
3o = {โ
, 1o, 2o} |
9 | 1, 8 | eleq2s 2852 |
. . . 4
โข (๐ถ โ 3o โ
(๐ถ = โ
โจ ๐ถ = 1o โจ ๐ถ =
2o)) |
10 | | orc 866 |
. . . . . . 7
โข (๐ถ = โ
โ (๐ถ = โ
โจ (๐ถ = (ฯ โo
(ฯ โo ๐ถ)) โง ๐ถ โ On))) |
11 | | omcl2 41711 |
. . . . . . 7
โข (((๐ด โ ๐ถ โง ๐ต โ ๐ถ) โง (๐ถ = โ
โจ (๐ถ = (ฯ โo (ฯ
โo ๐ถ))
โง ๐ถ โ On))) โ
(๐ด ยทo
๐ต) โ ๐ถ) |
12 | 10, 11 | sylan2 594 |
. . . . . 6
โข (((๐ด โ ๐ถ โง ๐ต โ ๐ถ) โง ๐ถ = โ
) โ (๐ด ยทo ๐ต) โ ๐ถ) |
13 | 12 | ex 414 |
. . . . 5
โข ((๐ด โ ๐ถ โง ๐ต โ ๐ถ) โ (๐ถ = โ
โ (๐ด ยทo ๐ต) โ ๐ถ)) |
14 | | el1o 8442 |
. . . . . . . . 9
โข (๐ด โ 1o โ
๐ด =
โ
) |
15 | | el1o 8442 |
. . . . . . . . 9
โข (๐ต โ 1o โ
๐ต =
โ
) |
16 | | oveq12 7367 |
. . . . . . . . . 10
โข ((๐ด = โ
โง ๐ต = โ
) โ (๐ด ยทo ๐ต) = (โ
ยทo โ
)) |
17 | | 0elon 6372 |
. . . . . . . . . . . 12
โข โ
โ On |
18 | | om0 8464 |
. . . . . . . . . . . 12
โข (โ
โ On โ (โ
ยทo โ
) =
โ
) |
19 | 17, 18 | ax-mp 5 |
. . . . . . . . . . 11
โข (โ
ยทo โ
) = โ
|
20 | | 0lt1o 8451 |
. . . . . . . . . . 11
โข โ
โ 1o |
21 | 19, 20 | eqeltri 2830 |
. . . . . . . . . 10
โข (โ
ยทo โ
) โ 1o |
22 | 16, 21 | eqeltrdi 2842 |
. . . . . . . . 9
โข ((๐ด = โ
โง ๐ต = โ
) โ (๐ด ยทo ๐ต) โ
1o) |
23 | 14, 15, 22 | syl2anb 599 |
. . . . . . . 8
โข ((๐ด โ 1o โง
๐ต โ 1o)
โ (๐ด
ยทo ๐ต)
โ 1o) |
24 | 23 | a1i 11 |
. . . . . . 7
โข (๐ถ = 1o โ ((๐ด โ 1o โง
๐ต โ 1o)
โ (๐ด
ยทo ๐ต)
โ 1o)) |
25 | | eleq2 2823 |
. . . . . . . 8
โข (๐ถ = 1o โ (๐ด โ ๐ถ โ ๐ด โ 1o)) |
26 | | eleq2 2823 |
. . . . . . . 8
โข (๐ถ = 1o โ (๐ต โ ๐ถ โ ๐ต โ 1o)) |
27 | 25, 26 | anbi12d 632 |
. . . . . . 7
โข (๐ถ = 1o โ ((๐ด โ ๐ถ โง ๐ต โ ๐ถ) โ (๐ด โ 1o โง ๐ต โ
1o))) |
28 | | eleq2 2823 |
. . . . . . 7
โข (๐ถ = 1o โ ((๐ด ยทo ๐ต) โ ๐ถ โ (๐ด ยทo ๐ต) โ 1o)) |
29 | 24, 27, 28 | 3imtr4d 294 |
. . . . . 6
โข (๐ถ = 1o โ ((๐ด โ ๐ถ โง ๐ต โ ๐ถ) โ (๐ด ยทo ๐ต) โ ๐ถ)) |
30 | 29 | com12 32 |
. . . . 5
โข ((๐ด โ ๐ถ โง ๐ต โ ๐ถ) โ (๐ถ = 1o โ (๐ด ยทo ๐ต) โ ๐ถ)) |
31 | | elpri 4609 |
. . . . . . . . . 10
โข (๐ด โ {โ
, 1o}
โ (๐ด = โ
โจ
๐ด =
1o)) |
32 | 31, 3 | eleq2s 2852 |
. . . . . . . . 9
โข (๐ด โ 2o โ
(๐ด = โ
โจ ๐ด =
1o)) |
33 | | elpri 4609 |
. . . . . . . . . 10
โข (๐ต โ {โ
, 1o}
โ (๐ต = โ
โจ
๐ต =
1o)) |
34 | 33, 3 | eleq2s 2852 |
. . . . . . . . 9
โข (๐ต โ 2o โ
(๐ต = โ
โจ ๐ต =
1o)) |
35 | | 0ex 5265 |
. . . . . . . . . . . . 13
โข โ
โ V |
36 | 35 | prid1 4724 |
. . . . . . . . . . . 12
โข โ
โ {โ
, 1o} |
37 | 36, 19, 3 | 3eltr4i 2847 |
. . . . . . . . . . 11
โข (โ
ยทo โ
) โ 2o |
38 | 16, 37 | eqeltrdi 2842 |
. . . . . . . . . 10
โข ((๐ด = โ
โง ๐ต = โ
) โ (๐ด ยทo ๐ต) โ
2o) |
39 | | oveq12 7367 |
. . . . . . . . . . 11
โข ((๐ด = 1o โง ๐ต = โ
) โ (๐ด ยทo ๐ต) = (1o
ยทo โ
)) |
40 | | 1on 8425 |
. . . . . . . . . . . . 13
โข
1o โ On |
41 | | om0 8464 |
. . . . . . . . . . . . 13
โข
(1o โ On โ (1o ยทo
โ
) = โ
) |
42 | 40, 41 | ax-mp 5 |
. . . . . . . . . . . 12
โข
(1o ยทo โ
) = โ
|
43 | 36, 42, 3 | 3eltr4i 2847 |
. . . . . . . . . . 11
โข
(1o ยทo โ
) โ
2o |
44 | 39, 43 | eqeltrdi 2842 |
. . . . . . . . . 10
โข ((๐ด = 1o โง ๐ต = โ
) โ (๐ด ยทo ๐ต) โ
2o) |
45 | | oveq12 7367 |
. . . . . . . . . . 11
โข ((๐ด = โ
โง ๐ต = 1o) โ (๐ด ยทo ๐ต) = (โ
ยทo 1o)) |
46 | | om0r 8486 |
. . . . . . . . . . . . 13
โข
(1o โ On โ (โ
ยทo
1o) = โ
) |
47 | 40, 46 | ax-mp 5 |
. . . . . . . . . . . 12
โข (โ
ยทo 1o) = โ
|
48 | 36, 47, 3 | 3eltr4i 2847 |
. . . . . . . . . . 11
โข (โ
ยทo 1o) โ 2o |
49 | 45, 48 | eqeltrdi 2842 |
. . . . . . . . . 10
โข ((๐ด = โ
โง ๐ต = 1o) โ (๐ด ยทo ๐ต) โ
2o) |
50 | | oveq12 7367 |
. . . . . . . . . . 11
โข ((๐ด = 1o โง ๐ต = 1o) โ (๐ด ยทo ๐ต) = (1o
ยทo 1o)) |
51 | | 1oex 8423 |
. . . . . . . . . . . . 13
โข
1o โ V |
52 | 51 | prid2 4725 |
. . . . . . . . . . . 12
โข
1o โ {โ
, 1o} |
53 | | om1 8490 |
. . . . . . . . . . . . 13
โข
(1o โ On โ (1o ยทo
1o) = 1o) |
54 | 40, 53 | ax-mp 5 |
. . . . . . . . . . . 12
โข
(1o ยทo 1o) =
1o |
55 | 52, 54, 3 | 3eltr4i 2847 |
. . . . . . . . . . 11
โข
(1o ยทo 1o) โ
2o |
56 | 50, 55 | eqeltrdi 2842 |
. . . . . . . . . 10
โข ((๐ด = 1o โง ๐ต = 1o) โ (๐ด ยทo ๐ต) โ
2o) |
57 | 38, 44, 49, 56 | ccase 1037 |
. . . . . . . . 9
โข (((๐ด = โ
โจ ๐ด = 1o) โง (๐ต = โ
โจ ๐ต = 1o)) โ (๐ด ยทo ๐ต) โ
2o) |
58 | 32, 34, 57 | syl2an 597 |
. . . . . . . 8
โข ((๐ด โ 2o โง
๐ต โ 2o)
โ (๐ด
ยทo ๐ต)
โ 2o) |
59 | 58 | a1i 11 |
. . . . . . 7
โข (๐ถ = 2o โ ((๐ด โ 2o โง
๐ต โ 2o)
โ (๐ด
ยทo ๐ต)
โ 2o)) |
60 | | eleq2 2823 |
. . . . . . . 8
โข (๐ถ = 2o โ (๐ด โ ๐ถ โ ๐ด โ 2o)) |
61 | | eleq2 2823 |
. . . . . . . 8
โข (๐ถ = 2o โ (๐ต โ ๐ถ โ ๐ต โ 2o)) |
62 | 60, 61 | anbi12d 632 |
. . . . . . 7
โข (๐ถ = 2o โ ((๐ด โ ๐ถ โง ๐ต โ ๐ถ) โ (๐ด โ 2o โง ๐ต โ
2o))) |
63 | | eleq2 2823 |
. . . . . . 7
โข (๐ถ = 2o โ ((๐ด ยทo ๐ต) โ ๐ถ โ (๐ด ยทo ๐ต) โ 2o)) |
64 | 59, 62, 63 | 3imtr4d 294 |
. . . . . 6
โข (๐ถ = 2o โ ((๐ด โ ๐ถ โง ๐ต โ ๐ถ) โ (๐ด ยทo ๐ต) โ ๐ถ)) |
65 | 64 | com12 32 |
. . . . 5
โข ((๐ด โ ๐ถ โง ๐ต โ ๐ถ) โ (๐ถ = 2o โ (๐ด ยทo ๐ต) โ ๐ถ)) |
66 | 13, 30, 65 | 3jaod 1429 |
. . . 4
โข ((๐ด โ ๐ถ โง ๐ต โ ๐ถ) โ ((๐ถ = โ
โจ ๐ถ = 1o โจ ๐ถ = 2o) โ (๐ด ยทo ๐ต) โ ๐ถ)) |
67 | 9, 66 | syl5 34 |
. . 3
โข ((๐ด โ ๐ถ โง ๐ต โ ๐ถ) โ (๐ถ โ 3o โ (๐ด ยทo ๐ต) โ ๐ถ)) |
68 | | olc 867 |
. . . . 5
โข ((๐ถ = (ฯ โo
(ฯ โo ๐ท)) โง ๐ท โ On) โ (๐ถ = โ
โจ (๐ถ = (ฯ โo (ฯ
โo ๐ท))
โง ๐ท โ
On))) |
69 | | omcl2 41711 |
. . . . 5
โข (((๐ด โ ๐ถ โง ๐ต โ ๐ถ) โง (๐ถ = โ
โจ (๐ถ = (ฯ โo (ฯ
โo ๐ท))
โง ๐ท โ On))) โ
(๐ด ยทo
๐ต) โ ๐ถ) |
70 | 68, 69 | sylan2 594 |
. . . 4
โข (((๐ด โ ๐ถ โง ๐ต โ ๐ถ) โง (๐ถ = (ฯ โo (ฯ
โo ๐ท))
โง ๐ท โ On)) โ
(๐ด ยทo
๐ต) โ ๐ถ) |
71 | 70 | ex 414 |
. . 3
โข ((๐ด โ ๐ถ โง ๐ต โ ๐ถ) โ ((๐ถ = (ฯ โo (ฯ
โo ๐ท))
โง ๐ท โ On) โ
(๐ด ยทo
๐ต) โ ๐ถ)) |
72 | 67, 71 | jaod 858 |
. 2
โข ((๐ด โ ๐ถ โง ๐ต โ ๐ถ) โ ((๐ถ โ 3o โจ (๐ถ = (ฯ โo
(ฯ โo ๐ท)) โง ๐ท โ On)) โ (๐ด ยทo ๐ต) โ ๐ถ)) |
73 | 72 | imp 408 |
1
โข (((๐ด โ ๐ถ โง ๐ต โ ๐ถ) โง (๐ถ โ 3o โจ (๐ถ = (ฯ โo
(ฯ โo ๐ท)) โง ๐ท โ On))) โ (๐ด ยทo ๐ต) โ ๐ถ) |