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 | com12 32 |
. . . 4
โข (๐ด โ ๐ถ โ (๐ถ = โ
โ (๐ด ยทo ๐ต) โ ๐ถ)) |
6 | 5 | adantr 482 |
. . 3
โข ((๐ด โ ๐ถ โง ๐ต โ ๐ถ) โ (๐ถ = โ
โ (๐ด ยทo ๐ต) โ ๐ถ)) |
7 | | simpl 484 |
. . . . . . . 8
โข ((๐ถ = (ฯ โo
(ฯ โo ๐ท)) โง ๐ท โ On) โ ๐ถ = (ฯ โo (ฯ
โo ๐ท))) |
8 | | omelon 9587 |
. . . . . . . . . . . 12
โข ฯ
โ On |
9 | | oecl 8484 |
. . . . . . . . . . . 12
โข ((ฯ
โ On โง ๐ท โ
On) โ (ฯ โo ๐ท) โ On) |
10 | 8, 9 | mpan 689 |
. . . . . . . . . . 11
โข (๐ท โ On โ (ฯ
โo ๐ท)
โ On) |
11 | 10, 8 | jctil 521 |
. . . . . . . . . 10
โข (๐ท โ On โ (ฯ
โ On โง (ฯ โo ๐ท) โ On)) |
12 | | oecl 8484 |
. . . . . . . . . 10
โข ((ฯ
โ On โง (ฯ โo ๐ท) โ On) โ (ฯ
โo (ฯ โo ๐ท)) โ On) |
13 | 11, 12 | syl 17 |
. . . . . . . . 9
โข (๐ท โ On โ (ฯ
โo (ฯ โo ๐ท)) โ On) |
14 | 13 | adantl 483 |
. . . . . . . 8
โข ((๐ถ = (ฯ โo
(ฯ โo ๐ท)) โง ๐ท โ On) โ (ฯ
โo (ฯ โo ๐ท)) โ On) |
15 | 7, 14 | eqeltrd 2834 |
. . . . . . 7
โข ((๐ถ = (ฯ โo
(ฯ โo ๐ท)) โง ๐ท โ On) โ ๐ถ โ On) |
16 | | simpll 766 |
. . . . . . 7
โข (((๐ด โ ๐ถ โง ๐ต โ ๐ถ) โง (๐ถ = (ฯ โo (ฯ
โo ๐ท))
โง ๐ท โ On)) โ
๐ด โ ๐ถ) |
17 | | onelon 6343 |
. . . . . . 7
โข ((๐ถ โ On โง ๐ด โ ๐ถ) โ ๐ด โ On) |
18 | 15, 16, 17 | syl2an2 685 |
. . . . . 6
โข (((๐ด โ ๐ถ โง ๐ต โ ๐ถ) โง (๐ถ = (ฯ โo (ฯ
โo ๐ท))
โง ๐ท โ On)) โ
๐ด โ
On) |
19 | | on0eqel 6442 |
. . . . . 6
โข (๐ด โ On โ (๐ด = โ
โจ โ
โ
๐ด)) |
20 | 18, 19 | syl 17 |
. . . . 5
โข (((๐ด โ ๐ถ โง ๐ต โ ๐ถ) โง (๐ถ = (ฯ โo (ฯ
โo ๐ท))
โง ๐ท โ On)) โ
(๐ด = โ
โจ โ
โ ๐ด)) |
21 | | oveq1 7365 |
. . . . . . . . 9
โข (๐ด = โ
โ (๐ด ยทo ๐ต) = (โ
ยทo ๐ต)) |
22 | | simpr 486 |
. . . . . . . . . . . 12
โข ((๐ด โ ๐ถ โง ๐ต โ ๐ถ) โ ๐ต โ ๐ถ) |
23 | 22 | adantr 482 |
. . . . . . . . . . 11
โข (((๐ด โ ๐ถ โง ๐ต โ ๐ถ) โง (๐ถ = (ฯ โo (ฯ
โo ๐ท))
โง ๐ท โ On)) โ
๐ต โ ๐ถ) |
24 | | onelon 6343 |
. . . . . . . . . . 11
โข ((๐ถ โ On โง ๐ต โ ๐ถ) โ ๐ต โ On) |
25 | 15, 23, 24 | syl2an2 685 |
. . . . . . . . . 10
โข (((๐ด โ ๐ถ โง ๐ต โ ๐ถ) โง (๐ถ = (ฯ โo (ฯ
โo ๐ท))
โง ๐ท โ On)) โ
๐ต โ
On) |
26 | | om0r 8486 |
. . . . . . . . . 10
โข (๐ต โ On โ (โ
ยทo ๐ต) =
โ
) |
27 | 25, 26 | syl 17 |
. . . . . . . . 9
โข (((๐ด โ ๐ถ โง ๐ต โ ๐ถ) โง (๐ถ = (ฯ โo (ฯ
โo ๐ท))
โง ๐ท โ On)) โ
(โ
ยทo ๐ต) = โ
) |
28 | 21, 27 | sylan9eqr 2795 |
. . . . . . . 8
โข ((((๐ด โ ๐ถ โง ๐ต โ ๐ถ) โง (๐ถ = (ฯ โo (ฯ
โo ๐ท))
โง ๐ท โ On)) โง
๐ด = โ
) โ (๐ด ยทo ๐ต) = โ
) |
29 | | peano1 7826 |
. . . . . . . . . . . . 13
โข โ
โ ฯ |
30 | | oen0 8534 |
. . . . . . . . . . . . 13
โข
(((ฯ โ On โง (ฯ โo ๐ท) โ On) โง โ
โ ฯ)
โ โ
โ (ฯ โo (ฯ โo
๐ท))) |
31 | 11, 29, 30 | sylancl 587 |
. . . . . . . . . . . 12
โข (๐ท โ On โ โ
โ
(ฯ โo (ฯ โo ๐ท))) |
32 | 31 | adantl 483 |
. . . . . . . . . . 11
โข ((๐ถ = (ฯ โo
(ฯ โo ๐ท)) โง ๐ท โ On) โ โ
โ (ฯ
โo (ฯ โo ๐ท))) |
33 | 32, 7 | eleqtrrd 2837 |
. . . . . . . . . 10
โข ((๐ถ = (ฯ โo
(ฯ โo ๐ท)) โง ๐ท โ On) โ โ
โ ๐ถ) |
34 | 33 | adantl 483 |
. . . . . . . . 9
โข (((๐ด โ ๐ถ โง ๐ต โ ๐ถ) โง (๐ถ = (ฯ โo (ฯ
โo ๐ท))
โง ๐ท โ On)) โ
โ
โ ๐ถ) |
35 | 34 | adantr 482 |
. . . . . . . 8
โข ((((๐ด โ ๐ถ โง ๐ต โ ๐ถ) โง (๐ถ = (ฯ โo (ฯ
โo ๐ท))
โง ๐ท โ On)) โง
๐ด = โ
) โ โ
โ ๐ถ) |
36 | 28, 35 | eqeltrd 2834 |
. . . . . . 7
โข ((((๐ด โ ๐ถ โง ๐ต โ ๐ถ) โง (๐ถ = (ฯ โo (ฯ
โo ๐ท))
โง ๐ท โ On)) โง
๐ด = โ
) โ (๐ด ยทo ๐ต) โ ๐ถ) |
37 | 36 | ex 414 |
. . . . . 6
โข (((๐ด โ ๐ถ โง ๐ต โ ๐ถ) โง (๐ถ = (ฯ โo (ฯ
โo ๐ท))
โง ๐ท โ On)) โ
(๐ด = โ
โ (๐ด ยทo ๐ต) โ ๐ถ)) |
38 | | simp1 1137 |
. . . . . . . . . . . 12
โข ((๐ด โ ๐ถ โง ๐ต โ ๐ถ โง โ
โ ๐ด) โ ๐ด โ ๐ถ) |
39 | 15 | adantl 483 |
. . . . . . . . . . . . . 14
โข (((๐ด โ ๐ถ โง ๐ต โ ๐ถ โง โ
โ ๐ด) โง (๐ถ = (ฯ โo (ฯ
โo ๐ท))
โง ๐ท โ On)) โ
๐ถ โ
On) |
40 | | simpr 486 |
. . . . . . . . . . . . . . . 16
โข ((((๐ด โ ๐ถ โง ๐ต โ ๐ถ โง โ
โ ๐ด) โง (๐ถ = (ฯ โo (ฯ
โo ๐ท))
โง ๐ท โ On)) โง
๐ถ โ On) โ ๐ถ โ On) |
41 | 38 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
โข ((((๐ด โ ๐ถ โง ๐ต โ ๐ถ โง โ
โ ๐ด) โง (๐ถ = (ฯ โo (ฯ
โo ๐ท))
โง ๐ท โ On)) โง
๐ถ โ On) โ ๐ด โ ๐ถ) |
42 | 40, 41, 17 | syl2anc 585 |
. . . . . . . . . . . . . . 15
โข ((((๐ด โ ๐ถ โง ๐ต โ ๐ถ โง โ
โ ๐ด) โง (๐ถ = (ฯ โo (ฯ
โo ๐ท))
โง ๐ท โ On)) โง
๐ถ โ On) โ ๐ด โ On) |
43 | 42 | ex 414 |
. . . . . . . . . . . . . 14
โข (((๐ด โ ๐ถ โง ๐ต โ ๐ถ โง โ
โ ๐ด) โง (๐ถ = (ฯ โo (ฯ
โo ๐ท))
โง ๐ท โ On)) โ
(๐ถ โ On โ ๐ด โ On)) |
44 | 39, 43 | jcai 518 |
. . . . . . . . . . . . 13
โข (((๐ด โ ๐ถ โง ๐ต โ ๐ถ โง โ
โ ๐ด) โง (๐ถ = (ฯ โo (ฯ
โo ๐ท))
โง ๐ท โ On)) โ
(๐ถ โ On โง ๐ด โ On)) |
45 | | simpl3 1194 |
. . . . . . . . . . . . 13
โข (((๐ด โ ๐ถ โง ๐ต โ ๐ถ โง โ
โ ๐ด) โง (๐ถ = (ฯ โo (ฯ
โo ๐ท))
โง ๐ท โ On)) โ
โ
โ ๐ด) |
46 | | simpl2 1193 |
. . . . . . . . . . . . 13
โข (((๐ด โ ๐ถ โง ๐ต โ ๐ถ โง โ
โ ๐ด) โง (๐ถ = (ฯ โo (ฯ
โo ๐ท))
โง ๐ท โ On)) โ
๐ต โ ๐ถ) |
47 | | omordi 8514 |
. . . . . . . . . . . . . 14
โข (((๐ถ โ On โง ๐ด โ On) โง โ
โ
๐ด) โ (๐ต โ ๐ถ โ (๐ด ยทo ๐ต) โ (๐ด ยทo ๐ถ))) |
48 | 47 | imp 408 |
. . . . . . . . . . . . 13
โข ((((๐ถ โ On โง ๐ด โ On) โง โ
โ
๐ด) โง ๐ต โ ๐ถ) โ (๐ด ยทo ๐ต) โ (๐ด ยทo ๐ถ)) |
49 | 44, 45, 46, 48 | syl21anc 837 |
. . . . . . . . . . . 12
โข (((๐ด โ ๐ถ โง ๐ต โ ๐ถ โง โ
โ ๐ด) โง (๐ถ = (ฯ โo (ฯ
โo ๐ท))
โง ๐ท โ On)) โ
(๐ด ยทo
๐ต) โ (๐ด ยทo ๐ถ)) |
50 | | oveq1 7365 |
. . . . . . . . . . . . 13
โข (๐ฅ = ๐ด โ (๐ฅ ยทo ๐ถ) = (๐ด ยทo ๐ถ)) |
51 | 50 | eliuni 4961 |
. . . . . . . . . . . 12
โข ((๐ด โ ๐ถ โง (๐ด ยทo ๐ต) โ (๐ด ยทo ๐ถ)) โ (๐ด ยทo ๐ต) โ โช
๐ฅ โ ๐ถ (๐ฅ ยทo ๐ถ)) |
52 | 38, 49, 51 | syl2an2r 684 |
. . . . . . . . . . 11
โข (((๐ด โ ๐ถ โง ๐ต โ ๐ถ โง โ
โ ๐ด) โง (๐ถ = (ฯ โo (ฯ
โo ๐ท))
โง ๐ท โ On)) โ
(๐ด ยทo
๐ต) โ โช ๐ฅ โ ๐ถ (๐ฅ ยทo ๐ถ)) |
53 | | simpr 486 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ถ = (ฯ โo
(ฯ โo ๐ท)) โง ๐ท โ On) โง ๐ฅ โ ๐ถ) โง ๐ฅ = โ
) โ ๐ฅ = โ
) |
54 | 53 | oveq1d 7373 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ถ = (ฯ โo
(ฯ โo ๐ท)) โง ๐ท โ On) โง ๐ฅ โ ๐ถ) โง ๐ฅ = โ
) โ (๐ฅ ยทo ๐ถ) = (โ
ยทo ๐ถ)) |
55 | | om0r 8486 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ถ โ On โ (โ
ยทo ๐ถ) =
โ
) |
56 | 15, 55 | syl 17 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ถ = (ฯ โo
(ฯ โo ๐ท)) โง ๐ท โ On) โ (โ
ยทo ๐ถ) =
โ
) |
57 | 56 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ถ = (ฯ โo
(ฯ โo ๐ท)) โง ๐ท โ On) โง ๐ฅ โ ๐ถ) โง ๐ฅ = โ
) โ (โ
ยทo ๐ถ) =
โ
) |
58 | 54, 57 | eqtrd 2773 |
. . . . . . . . . . . . . . . 16
โข ((((๐ถ = (ฯ โo
(ฯ โo ๐ท)) โง ๐ท โ On) โง ๐ฅ โ ๐ถ) โง ๐ฅ = โ
) โ (๐ฅ ยทo ๐ถ) = โ
) |
59 | | 0ss 4357 |
. . . . . . . . . . . . . . . . 17
โข โ
โ ๐ถ |
60 | 59 | a1i 11 |
. . . . . . . . . . . . . . . 16
โข ((((๐ถ = (ฯ โo
(ฯ โo ๐ท)) โง ๐ท โ On) โง ๐ฅ โ ๐ถ) โง ๐ฅ = โ
) โ โ
โ ๐ถ) |
61 | 58, 60 | eqsstrd 3983 |
. . . . . . . . . . . . . . 15
โข ((((๐ถ = (ฯ โo
(ฯ โo ๐ท)) โง ๐ท โ On) โง ๐ฅ โ ๐ถ) โง ๐ฅ = โ
) โ (๐ฅ ยทo ๐ถ) โ ๐ถ) |
62 | | id 22 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ฅ โ ๐ถ โง โ
โ ๐ฅ) โ (๐ฅ โ ๐ถ โง โ
โ ๐ฅ)) |
63 | 62 | adantll 713 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ถ = (ฯ โo
(ฯ โo ๐ท)) โง ๐ท โ On) โง ๐ฅ โ ๐ถ) โง โ
โ ๐ฅ) โ (๐ฅ โ ๐ถ โง โ
โ ๐ฅ)) |
64 | | simpll 766 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ถ = (ฯ โo
(ฯ โo ๐ท)) โง ๐ท โ On) โง ๐ฅ โ ๐ถ) โง โ
โ ๐ฅ) โ (๐ถ = (ฯ โo (ฯ
โo ๐ท))
โง ๐ท โ
On)) |
65 | 64 | 3mix3d 1339 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ถ = (ฯ โo
(ฯ โo ๐ท)) โง ๐ท โ On) โง ๐ฅ โ ๐ถ) โง โ
โ ๐ฅ) โ (๐ถ = โ
โจ ๐ถ = 2o โจ (๐ถ = (ฯ โo (ฯ
โo ๐ท))
โง ๐ท โ
On))) |
66 | | omabs2 41710 |
. . . . . . . . . . . . . . . . 17
โข (((๐ฅ โ ๐ถ โง โ
โ ๐ฅ) โง (๐ถ = โ
โจ ๐ถ = 2o โจ (๐ถ = (ฯ โo (ฯ
โo ๐ท))
โง ๐ท โ On))) โ
(๐ฅ ยทo
๐ถ) = ๐ถ) |
67 | 63, 65, 66 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
โข ((((๐ถ = (ฯ โo
(ฯ โo ๐ท)) โง ๐ท โ On) โง ๐ฅ โ ๐ถ) โง โ
โ ๐ฅ) โ (๐ฅ ยทo ๐ถ) = ๐ถ) |
68 | | ssidd 3968 |
. . . . . . . . . . . . . . . 16
โข ((((๐ถ = (ฯ โo
(ฯ โo ๐ท)) โง ๐ท โ On) โง ๐ฅ โ ๐ถ) โง โ
โ ๐ฅ) โ ๐ถ โ ๐ถ) |
69 | 67, 68 | eqsstrd 3983 |
. . . . . . . . . . . . . . 15
โข ((((๐ถ = (ฯ โo
(ฯ โo ๐ท)) โง ๐ท โ On) โง ๐ฅ โ ๐ถ) โง โ
โ ๐ฅ) โ (๐ฅ ยทo ๐ถ) โ ๐ถ) |
70 | | onelon 6343 |
. . . . . . . . . . . . . . . . 17
โข ((๐ถ โ On โง ๐ฅ โ ๐ถ) โ ๐ฅ โ On) |
71 | 15, 70 | sylan 581 |
. . . . . . . . . . . . . . . 16
โข (((๐ถ = (ฯ โo
(ฯ โo ๐ท)) โง ๐ท โ On) โง ๐ฅ โ ๐ถ) โ ๐ฅ โ On) |
72 | | on0eqel 6442 |
. . . . . . . . . . . . . . . 16
โข (๐ฅ โ On โ (๐ฅ = โ
โจ โ
โ
๐ฅ)) |
73 | 71, 72 | syl 17 |
. . . . . . . . . . . . . . 15
โข (((๐ถ = (ฯ โo
(ฯ โo ๐ท)) โง ๐ท โ On) โง ๐ฅ โ ๐ถ) โ (๐ฅ = โ
โจ โ
โ ๐ฅ)) |
74 | 61, 69, 73 | mpjaodan 958 |
. . . . . . . . . . . . . 14
โข (((๐ถ = (ฯ โo
(ฯ โo ๐ท)) โง ๐ท โ On) โง ๐ฅ โ ๐ถ) โ (๐ฅ ยทo ๐ถ) โ ๐ถ) |
75 | 74 | iunssd 5011 |
. . . . . . . . . . . . 13
โข ((๐ถ = (ฯ โo
(ฯ โo ๐ท)) โง ๐ท โ On) โ โช ๐ฅ โ ๐ถ (๐ฅ ยทo ๐ถ) โ ๐ถ) |
76 | | simpr 486 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ถ = (ฯ โo
(ฯ โo ๐ท)) โง ๐ท โ On) โ ๐ท โ On) |
77 | 76, 8 | jctil 521 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ถ = (ฯ โo
(ฯ โo ๐ท)) โง ๐ท โ On) โ (ฯ โ On โง
๐ท โ
On)) |
78 | | oen0 8534 |
. . . . . . . . . . . . . . . . . 18
โข
(((ฯ โ On โง ๐ท โ On) โง โ
โ ฯ)
โ โ
โ (ฯ โo ๐ท)) |
79 | 77, 29, 78 | sylancl 587 |
. . . . . . . . . . . . . . . . 17
โข ((๐ถ = (ฯ โo
(ฯ โo ๐ท)) โง ๐ท โ On) โ โ
โ (ฯ
โo ๐ท)) |
80 | 77, 9 | syl 17 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ถ = (ฯ โo
(ฯ โo ๐ท)) โง ๐ท โ On) โ (ฯ
โo ๐ท)
โ On) |
81 | | 1onn 8587 |
. . . . . . . . . . . . . . . . . . 19
โข
1o โ ฯ |
82 | | ondif2 8449 |
. . . . . . . . . . . . . . . . . . 19
โข (ฯ
โ (On โ 2o) โ (ฯ โ On โง 1o
โ ฯ)) |
83 | 8, 81, 82 | mpbir2an 710 |
. . . . . . . . . . . . . . . . . 18
โข ฯ
โ (On โ 2o) |
84 | | oeordi 8535 |
. . . . . . . . . . . . . . . . . 18
โข
(((ฯ โo ๐ท) โ On โง ฯ โ (On โ
2o)) โ (โ
โ (ฯ โo ๐ท) โ (ฯ
โo โ
) โ (ฯ โo (ฯ
โo ๐ท)))) |
85 | 80, 83, 84 | sylancl 587 |
. . . . . . . . . . . . . . . . 17
โข ((๐ถ = (ฯ โo
(ฯ โo ๐ท)) โง ๐ท โ On) โ (โ
โ (ฯ
โo ๐ท)
โ (ฯ โo โ
) โ (ฯ โo
(ฯ โo ๐ท)))) |
86 | 79, 85 | mpd 15 |
. . . . . . . . . . . . . . . 16
โข ((๐ถ = (ฯ โo
(ฯ โo ๐ท)) โง ๐ท โ On) โ (ฯ
โo โ
) โ (ฯ โo (ฯ
โo ๐ท))) |
87 | | oe0 8469 |
. . . . . . . . . . . . . . . . . . 19
โข (ฯ
โ On โ (ฯ โo โ
) =
1o) |
88 | 8, 87 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
โข (ฯ
โo โ
) = 1o |
89 | 88 | eqcomi 2742 |
. . . . . . . . . . . . . . . . 17
โข
1o = (ฯ โo โ
) |
90 | 89 | a1i 11 |
. . . . . . . . . . . . . . . 16
โข ((๐ถ = (ฯ โo
(ฯ โo ๐ท)) โง ๐ท โ On) โ 1o = (ฯ
โo โ
)) |
91 | 86, 90, 7 | 3eltr4d 2849 |
. . . . . . . . . . . . . . 15
โข ((๐ถ = (ฯ โo
(ฯ โo ๐ท)) โง ๐ท โ On) โ 1o โ
๐ถ) |
92 | | oveq1 7365 |
. . . . . . . . . . . . . . . . 17
โข (๐ฅ = 1o โ (๐ฅ ยทo ๐ถ) = (1o
ยทo ๐ถ)) |
93 | | om1r 8491 |
. . . . . . . . . . . . . . . . . 18
โข (๐ถ โ On โ (1o
ยทo ๐ถ) =
๐ถ) |
94 | 15, 93 | syl 17 |
. . . . . . . . . . . . . . . . 17
โข ((๐ถ = (ฯ โo
(ฯ โo ๐ท)) โง ๐ท โ On) โ (1o
ยทo ๐ถ) =
๐ถ) |
95 | 92, 94 | sylan9eqr 2795 |
. . . . . . . . . . . . . . . 16
โข (((๐ถ = (ฯ โo
(ฯ โo ๐ท)) โง ๐ท โ On) โง ๐ฅ = 1o) โ (๐ฅ ยทo ๐ถ) = ๐ถ) |
96 | 95 | sseq2d 3977 |
. . . . . . . . . . . . . . 15
โข (((๐ถ = (ฯ โo
(ฯ โo ๐ท)) โง ๐ท โ On) โง ๐ฅ = 1o) โ (๐ถ โ (๐ฅ ยทo ๐ถ) โ ๐ถ โ ๐ถ)) |
97 | | ssidd 3968 |
. . . . . . . . . . . . . . 15
โข ((๐ถ = (ฯ โo
(ฯ โo ๐ท)) โง ๐ท โ On) โ ๐ถ โ ๐ถ) |
98 | 91, 96, 97 | rspcedvd 3582 |
. . . . . . . . . . . . . 14
โข ((๐ถ = (ฯ โo
(ฯ โo ๐ท)) โง ๐ท โ On) โ โ๐ฅ โ ๐ถ ๐ถ โ (๐ฅ ยทo ๐ถ)) |
99 | | ssiun 5007 |
. . . . . . . . . . . . . 14
โข
(โ๐ฅ โ
๐ถ ๐ถ โ (๐ฅ ยทo ๐ถ) โ ๐ถ โ โช
๐ฅ โ ๐ถ (๐ฅ ยทo ๐ถ)) |
100 | 98, 99 | syl 17 |
. . . . . . . . . . . . 13
โข ((๐ถ = (ฯ โo
(ฯ โo ๐ท)) โง ๐ท โ On) โ ๐ถ โ โช
๐ฅ โ ๐ถ (๐ฅ ยทo ๐ถ)) |
101 | 75, 100 | eqssd 3962 |
. . . . . . . . . . . 12
โข ((๐ถ = (ฯ โo
(ฯ โo ๐ท)) โง ๐ท โ On) โ โช ๐ฅ โ ๐ถ (๐ฅ ยทo ๐ถ) = ๐ถ) |
102 | 101 | adantl 483 |
. . . . . . . . . . 11
โข (((๐ด โ ๐ถ โง ๐ต โ ๐ถ โง โ
โ ๐ด) โง (๐ถ = (ฯ โo (ฯ
โo ๐ท))
โง ๐ท โ On)) โ
โช ๐ฅ โ ๐ถ (๐ฅ ยทo ๐ถ) = ๐ถ) |
103 | 52, 102 | eleqtrd 2836 |
. . . . . . . . . 10
โข (((๐ด โ ๐ถ โง ๐ต โ ๐ถ โง โ
โ ๐ด) โง (๐ถ = (ฯ โo (ฯ
โo ๐ท))
โง ๐ท โ On)) โ
(๐ด ยทo
๐ต) โ ๐ถ) |
104 | 103 | ex 414 |
. . . . . . . . 9
โข ((๐ด โ ๐ถ โง ๐ต โ ๐ถ โง โ
โ ๐ด) โ ((๐ถ = (ฯ โo (ฯ
โo ๐ท))
โง ๐ท โ On) โ
(๐ด ยทo
๐ต) โ ๐ถ)) |
105 | 104 | 3expia 1122 |
. . . . . . . 8
โข ((๐ด โ ๐ถ โง ๐ต โ ๐ถ) โ (โ
โ ๐ด โ ((๐ถ = (ฯ โo (ฯ
โo ๐ท))
โง ๐ท โ On) โ
(๐ด ยทo
๐ต) โ ๐ถ))) |
106 | 105 | com23 86 |
. . . . . . 7
โข ((๐ด โ ๐ถ โง ๐ต โ ๐ถ) โ ((๐ถ = (ฯ โo (ฯ
โo ๐ท))
โง ๐ท โ On) โ
(โ
โ ๐ด โ
(๐ด ยทo
๐ต) โ ๐ถ))) |
107 | 106 | imp 408 |
. . . . . 6
โข (((๐ด โ ๐ถ โง ๐ต โ ๐ถ) โง (๐ถ = (ฯ โo (ฯ
โo ๐ท))
โง ๐ท โ On)) โ
(โ
โ ๐ด โ
(๐ด ยทo
๐ต) โ ๐ถ)) |
108 | 37, 107 | jaod 858 |
. . . . 5
โข (((๐ด โ ๐ถ โง ๐ต โ ๐ถ) โง (๐ถ = (ฯ โo (ฯ
โo ๐ท))
โง ๐ท โ On)) โ
((๐ด = โ
โจ โ
โ ๐ด) โ (๐ด ยทo ๐ต) โ ๐ถ)) |
109 | 20, 108 | mpd 15 |
. . . 4
โข (((๐ด โ ๐ถ โง ๐ต โ ๐ถ) โง (๐ถ = (ฯ โo (ฯ
โo ๐ท))
โง ๐ท โ On)) โ
(๐ด ยทo
๐ต) โ ๐ถ) |
110 | 109 | ex 414 |
. . 3
โข ((๐ด โ ๐ถ โง ๐ต โ ๐ถ) โ ((๐ถ = (ฯ โo (ฯ
โo ๐ท))
โง ๐ท โ On) โ
(๐ด ยทo
๐ต) โ ๐ถ)) |
111 | 6, 110 | jaod 858 |
. 2
โข ((๐ด โ ๐ถ โง ๐ต โ ๐ถ) โ ((๐ถ = โ
โจ (๐ถ = (ฯ โo (ฯ
โo ๐ท))
โง ๐ท โ On)) โ
(๐ด ยทo
๐ต) โ ๐ถ)) |
112 | 111 | imp 408 |
1
โข (((๐ด โ ๐ถ โง ๐ต โ ๐ถ) โง (๐ถ = โ
โจ (๐ถ = (ฯ โo (ฯ
โo ๐ท))
โง ๐ท โ On))) โ
(๐ด ยทo
๐ต) โ ๐ถ) |