Step | Hyp | Ref
| Expression |
1 | | scutcl 27649 |
. . . . . . . 8
âĒ (ðī <<s ðĩ â (ðī |s ðĩ) â No
) |
2 | 1 | ad3antrrr 727 |
. . . . . . 7
âĒ ((((ðī <<s ðĩ â§ ðķ <<s ð·) â§ (ðī |s ðĩ) âĪs (ðķ |s ð·)) â§ ð â ð·) â (ðī |s ðĩ) â No
) |
3 | | scutcl 27649 |
. . . . . . . 8
âĒ (ðķ <<s ð· â (ðķ |s ð·) â No
) |
4 | 3 | ad3antlr 728 |
. . . . . . 7
âĒ ((((ðī <<s ðĩ â§ ðķ <<s ð·) â§ (ðī |s ðĩ) âĪs (ðķ |s ð·)) â§ ð â ð·) â (ðķ |s ð·) â No
) |
5 | | ssltss2 27636 |
. . . . . . . . 9
âĒ (ðķ <<s ð· â ð· â No
) |
6 | 5 | ad2antlr 724 |
. . . . . . . 8
âĒ (((ðī <<s ðĩ â§ ðķ <<s ð·) â§ (ðī |s ðĩ) âĪs (ðķ |s ð·)) â ð· â No
) |
7 | 6 | sselda 3982 |
. . . . . . 7
âĒ ((((ðī <<s ðĩ â§ ðķ <<s ð·) â§ (ðī |s ðĩ) âĪs (ðķ |s ð·)) â§ ð â ð·) â ð â No
) |
8 | | simplr 766 |
. . . . . . 7
âĒ ((((ðī <<s ðĩ â§ ðķ <<s ð·) â§ (ðī |s ðĩ) âĪs (ðķ |s ð·)) â§ ð â ð·) â (ðī |s ðĩ) âĪs (ðķ |s ð·)) |
9 | | scutcut 27648 |
. . . . . . . . . . . 12
âĒ (ðķ <<s ð· â ((ðķ |s ð·) â No
â§ ðķ <<s {(ðķ |s ð·)} â§ {(ðķ |s ð·)} <<s ð·)) |
10 | 9 | simp3d 1143 |
. . . . . . . . . . 11
âĒ (ðķ <<s ð· â {(ðķ |s ð·)} <<s ð·) |
11 | 10 | ad2antlr 724 |
. . . . . . . . . 10
âĒ (((ðī <<s ðĩ â§ ðķ <<s ð·) â§ (ðī |s ðĩ) âĪs (ðķ |s ð·)) â {(ðķ |s ð·)} <<s ð·) |
12 | | ssltsep 27637 |
. . . . . . . . . 10
âĒ ({(ðķ |s ð·)} <<s ð· â âð â {(ðķ |s ð·)}âð â ð· ð <s ð) |
13 | 11, 12 | syl 17 |
. . . . . . . . 9
âĒ (((ðī <<s ðĩ â§ ðķ <<s ð·) â§ (ðī |s ðĩ) âĪs (ðķ |s ð·)) â âð â {(ðķ |s ð·)}âð â ð· ð <s ð) |
14 | | ovex 7445 |
. . . . . . . . . 10
âĒ (ðķ |s ð·) â V |
15 | | breq1 5151 |
. . . . . . . . . . 11
âĒ (ð = (ðķ |s ð·) â (ð <s ð â (ðķ |s ð·) <s ð)) |
16 | 15 | ralbidv 3176 |
. . . . . . . . . 10
âĒ (ð = (ðķ |s ð·) â (âð â ð· ð <s ð â âð â ð· (ðķ |s ð·) <s ð)) |
17 | 14, 16 | ralsn 4685 |
. . . . . . . . 9
âĒ
(âð â
{(ðķ |s ð·)}âð â ð· ð <s ð â âð â ð· (ðķ |s ð·) <s ð) |
18 | 13, 17 | sylib 217 |
. . . . . . . 8
âĒ (((ðī <<s ðĩ â§ ðķ <<s ð·) â§ (ðī |s ðĩ) âĪs (ðķ |s ð·)) â âð â ð· (ðķ |s ð·) <s ð) |
19 | 18 | r19.21bi 3247 |
. . . . . . 7
âĒ ((((ðī <<s ðĩ â§ ðķ <<s ð·) â§ (ðī |s ðĩ) âĪs (ðķ |s ð·)) â§ ð â ð·) â (ðķ |s ð·) <s ð) |
20 | 2, 4, 7, 8, 19 | slelttrd 27608 |
. . . . . 6
âĒ ((((ðī <<s ðĩ â§ ðķ <<s ð·) â§ (ðī |s ðĩ) âĪs (ðķ |s ð·)) â§ ð â ð·) â (ðī |s ðĩ) <s ð) |
21 | 20 | ralrimiva 3145 |
. . . . 5
âĒ (((ðī <<s ðĩ â§ ðķ <<s ð·) â§ (ðī |s ðĩ) âĪs (ðķ |s ð·)) â âð â ð· (ðī |s ðĩ) <s ð) |
22 | | ssltss1 27635 |
. . . . . . . . . 10
âĒ (ðī <<s ðĩ â ðī â No
) |
23 | 22 | adantr 480 |
. . . . . . . . 9
âĒ ((ðī <<s ðĩ â§ ðķ <<s ð·) â ðī â No
) |
24 | 23 | adantr 480 |
. . . . . . . 8
âĒ (((ðī <<s ðĩ â§ ðķ <<s ð·) â§ (ðī |s ðĩ) âĪs (ðķ |s ð·)) â ðī â No
) |
25 | 24 | sselda 3982 |
. . . . . . 7
âĒ ((((ðī <<s ðĩ â§ ðķ <<s ð·) â§ (ðī |s ðĩ) âĪs (ðķ |s ð·)) â§ ð â ðī) â ð â No
) |
26 | 1 | ad3antrrr 727 |
. . . . . . 7
âĒ ((((ðī <<s ðĩ â§ ðķ <<s ð·) â§ (ðī |s ðĩ) âĪs (ðķ |s ð·)) â§ ð â ðī) â (ðī |s ðĩ) â No
) |
27 | 3 | ad3antlr 728 |
. . . . . . 7
âĒ ((((ðī <<s ðĩ â§ ðķ <<s ð·) â§ (ðī |s ðĩ) âĪs (ðķ |s ð·)) â§ ð â ðī) â (ðķ |s ð·) â No
) |
28 | | scutcut 27648 |
. . . . . . . . . . . . 13
âĒ (ðī <<s ðĩ â ((ðī |s ðĩ) â No
â§ ðī <<s {(ðī |s ðĩ)} â§ {(ðī |s ðĩ)} <<s ðĩ)) |
29 | 28 | simp2d 1142 |
. . . . . . . . . . . 12
âĒ (ðī <<s ðĩ â ðī <<s {(ðī |s ðĩ)}) |
30 | 29 | adantr 480 |
. . . . . . . . . . 11
âĒ ((ðī <<s ðĩ â§ ðķ <<s ð·) â ðī <<s {(ðī |s ðĩ)}) |
31 | 30 | adantr 480 |
. . . . . . . . . 10
âĒ (((ðī <<s ðĩ â§ ðķ <<s ð·) â§ (ðī |s ðĩ) âĪs (ðķ |s ð·)) â ðī <<s {(ðī |s ðĩ)}) |
32 | | ssltsep 27637 |
. . . . . . . . . 10
âĒ (ðī <<s {(ðī |s ðĩ)} â âð â ðī âð â {(ðī |s ðĩ)}ð <s ð) |
33 | 31, 32 | syl 17 |
. . . . . . . . 9
âĒ (((ðī <<s ðĩ â§ ðķ <<s ð·) â§ (ðī |s ðĩ) âĪs (ðķ |s ð·)) â âð â ðī âð â {(ðī |s ðĩ)}ð <s ð) |
34 | 33 | r19.21bi 3247 |
. . . . . . . 8
âĒ ((((ðī <<s ðĩ â§ ðķ <<s ð·) â§ (ðī |s ðĩ) âĪs (ðķ |s ð·)) â§ ð â ðī) â âð â {(ðī |s ðĩ)}ð <s ð) |
35 | | ovex 7445 |
. . . . . . . . 9
âĒ (ðī |s ðĩ) â V |
36 | | breq2 5152 |
. . . . . . . . 9
âĒ (ð = (ðī |s ðĩ) â (ð <s ð â ð <s (ðī |s ðĩ))) |
37 | 35, 36 | ralsn 4685 |
. . . . . . . 8
âĒ
(âð â
{(ðī |s ðĩ)}ð <s ð â ð <s (ðī |s ðĩ)) |
38 | 34, 37 | sylib 217 |
. . . . . . 7
âĒ ((((ðī <<s ðĩ â§ ðķ <<s ð·) â§ (ðī |s ðĩ) âĪs (ðķ |s ð·)) â§ ð â ðī) â ð <s (ðī |s ðĩ)) |
39 | | simplr 766 |
. . . . . . 7
âĒ ((((ðī <<s ðĩ â§ ðķ <<s ð·) â§ (ðī |s ðĩ) âĪs (ðķ |s ð·)) â§ ð â ðī) â (ðī |s ðĩ) âĪs (ðķ |s ð·)) |
40 | 25, 26, 27, 38, 39 | sltletrd 27607 |
. . . . . 6
âĒ ((((ðī <<s ðĩ â§ ðķ <<s ð·) â§ (ðī |s ðĩ) âĪs (ðķ |s ð·)) â§ ð â ðī) â ð <s (ðķ |s ð·)) |
41 | 40 | ralrimiva 3145 |
. . . . 5
âĒ (((ðī <<s ðĩ â§ ðķ <<s ð·) â§ (ðī |s ðĩ) âĪs (ðķ |s ð·)) â âð â ðī ð <s (ðķ |s ð·)) |
42 | 21, 41 | jca 511 |
. . . 4
âĒ (((ðī <<s ðĩ â§ ðķ <<s ð·) â§ (ðī |s ðĩ) âĪs (ðķ |s ð·)) â (âð â ð· (ðī |s ðĩ) <s ð â§ âð â ðī ð <s (ðķ |s ð·))) |
43 | | bdayelon 27623 |
. . . . . . 7
âĒ ( bday â(ðī |s ðĩ)) â On |
44 | 43 | onordi 6475 |
. . . . . 6
âĒ Ord
( bday â(ðī |s ðĩ)) |
45 | | ordn2lp 6384 |
. . . . . 6
âĒ (Ord
( bday â(ðī |s ðĩ)) â ÂŽ ((
bday â(ðī |s
ðĩ)) â ( bday â(ðķ |s ð·)) â§ ( bday
â(ðķ |s ð·)) â ( bday â(ðī |s ðĩ)))) |
46 | 44, 45 | ax-mp 5 |
. . . . 5
âĒ ÂŽ
(( bday â(ðī |s ðĩ)) â ( bday
â(ðķ |s ð·)) â§ (
bday â(ðķ |s
ð·)) â ( bday â(ðī |s ðĩ))) |
47 | 3 | ad2antlr 724 |
. . . . . . 7
âĒ (((ðī <<s ðĩ â§ ðķ <<s ð·) â§ (âð â ð· (ðī |s ðĩ) <s ð â§ âð â ðī ð <s (ðķ |s ð·))) â (ðķ |s ð·) â No
) |
48 | 1 | adantr 480 |
. . . . . . . 8
âĒ ((ðī <<s ðĩ â§ ðķ <<s ð·) â (ðī |s ðĩ) â No
) |
49 | 48 | adantr 480 |
. . . . . . 7
âĒ (((ðī <<s ðĩ â§ ðķ <<s ð·) â§ (âð â ð· (ðī |s ðĩ) <s ð â§ âð â ðī ð <s (ðķ |s ð·))) â (ðī |s ðĩ) â No
) |
50 | | sltnle 27600 |
. . . . . . 7
âĒ (((ðķ |s ð·) â No
â§ (ðī |s ðĩ) â
No ) â ((ðķ |s
ð·) <s (ðī |s ðĩ) â ÂŽ (ðī |s ðĩ) âĪs (ðķ |s ð·))) |
51 | 47, 49, 50 | syl2anc 583 |
. . . . . 6
âĒ (((ðī <<s ðĩ â§ ðķ <<s ð·) â§ (âð â ð· (ðī |s ðĩ) <s ð â§ âð â ðī ð <s (ðķ |s ð·))) â ((ðķ |s ð·) <s (ðī |s ðĩ) â ÂŽ (ðī |s ðĩ) âĪs (ðķ |s ð·))) |
52 | 3 | ad3antlr 728 |
. . . . . . . . 9
âĒ ((((ðī <<s ðĩ â§ ðķ <<s ð·) â§ (âð â ð· (ðī |s ðĩ) <s ð â§ âð â ðī ð <s (ðķ |s ð·))) â§ (ðķ |s ð·) <s (ðī |s ðĩ)) â (ðķ |s ð·) â No
) |
53 | | ssltex1 27633 |
. . . . . . . . . . . 12
âĒ (ðī <<s ðĩ â ðī â V) |
54 | 53 | ad3antrrr 727 |
. . . . . . . . . . 11
âĒ ((((ðī <<s ðĩ â§ ðķ <<s ð·) â§ (âð â ð· (ðī |s ðĩ) <s ð â§ âð â ðī ð <s (ðķ |s ð·))) â§ (ðķ |s ð·) <s (ðī |s ðĩ)) â ðī â V) |
55 | | snex 5431 |
. . . . . . . . . . 11
âĒ {(ðķ |s ð·)} â V |
56 | 54, 55 | jctir 520 |
. . . . . . . . . 10
âĒ ((((ðī <<s ðĩ â§ ðķ <<s ð·) â§ (âð â ð· (ðī |s ðĩ) <s ð â§ âð â ðī ð <s (ðķ |s ð·))) â§ (ðķ |s ð·) <s (ðī |s ðĩ)) â (ðī â V â§ {(ðķ |s ð·)} â V)) |
57 | 22 | ad3antrrr 727 |
. . . . . . . . . . 11
âĒ ((((ðī <<s ðĩ â§ ðķ <<s ð·) â§ (âð â ð· (ðī |s ðĩ) <s ð â§ âð â ðī ð <s (ðķ |s ð·))) â§ (ðķ |s ð·) <s (ðī |s ðĩ)) â ðī â No
) |
58 | 52 | snssd 4812 |
. . . . . . . . . . 11
âĒ ((((ðī <<s ðĩ â§ ðķ <<s ð·) â§ (âð â ð· (ðī |s ðĩ) <s ð â§ âð â ðī ð <s (ðķ |s ð·))) â§ (ðķ |s ð·) <s (ðī |s ðĩ)) â {(ðķ |s ð·)} â No
) |
59 | | simplrr 775 |
. . . . . . . . . . . 12
âĒ ((((ðī <<s ðĩ â§ ðķ <<s ð·) â§ (âð â ð· (ðī |s ðĩ) <s ð â§ âð â ðī ð <s (ðķ |s ð·))) â§ (ðķ |s ð·) <s (ðī |s ðĩ)) â âð â ðī ð <s (ðķ |s ð·)) |
60 | | breq2 5152 |
. . . . . . . . . . . . . 14
âĒ (ð = (ðķ |s ð·) â (ð <s ð â ð <s (ðķ |s ð·))) |
61 | 14, 60 | ralsn 4685 |
. . . . . . . . . . . . 13
âĒ
(âð â
{(ðķ |s ð·)}ð <s ð â ð <s (ðķ |s ð·)) |
62 | 61 | ralbii 3092 |
. . . . . . . . . . . 12
âĒ
(âð â
ðī âð â {(ðķ |s ð·)}ð <s ð â âð â ðī ð <s (ðķ |s ð·)) |
63 | 59, 62 | sylibr 233 |
. . . . . . . . . . 11
âĒ ((((ðī <<s ðĩ â§ ðķ <<s ð·) â§ (âð â ð· (ðī |s ðĩ) <s ð â§ âð â ðī ð <s (ðķ |s ð·))) â§ (ðķ |s ð·) <s (ðī |s ðĩ)) â âð â ðī âð â {(ðķ |s ð·)}ð <s ð) |
64 | 57, 58, 63 | 3jca 1127 |
. . . . . . . . . 10
âĒ ((((ðī <<s ðĩ â§ ðķ <<s ð·) â§ (âð â ð· (ðī |s ðĩ) <s ð â§ âð â ðī ð <s (ðķ |s ð·))) â§ (ðķ |s ð·) <s (ðī |s ðĩ)) â (ðī â No
â§ {(ðķ |s ð·)} â No â§ âð â ðī âð â {(ðķ |s ð·)}ð <s ð)) |
65 | | brsslt 27632 |
. . . . . . . . . 10
âĒ (ðī <<s {(ðķ |s ð·)} â ((ðī â V â§ {(ðķ |s ð·)} â V) â§ (ðī â No
â§ {(ðķ |s ð·)} â No â§ âð â ðī âð â {(ðķ |s ð·)}ð <s ð))) |
66 | 56, 64, 65 | sylanbrc 582 |
. . . . . . . . 9
âĒ ((((ðī <<s ðĩ â§ ðķ <<s ð·) â§ (âð â ð· (ðī |s ðĩ) <s ð â§ âð â ðī ð <s (ðķ |s ð·))) â§ (ðķ |s ð·) <s (ðī |s ðĩ)) â ðī <<s {(ðķ |s ð·)}) |
67 | | ssltex2 27634 |
. . . . . . . . . . . 12
âĒ (ðī <<s ðĩ â ðĩ â V) |
68 | 67 | ad3antrrr 727 |
. . . . . . . . . . 11
âĒ ((((ðī <<s ðĩ â§ ðķ <<s ð·) â§ (âð â ð· (ðī |s ðĩ) <s ð â§ âð â ðī ð <s (ðķ |s ð·))) â§ (ðķ |s ð·) <s (ðī |s ðĩ)) â ðĩ â V) |
69 | 68, 55 | jctil 519 |
. . . . . . . . . 10
âĒ ((((ðī <<s ðĩ â§ ðķ <<s ð·) â§ (âð â ð· (ðī |s ðĩ) <s ð â§ âð â ðī ð <s (ðķ |s ð·))) â§ (ðķ |s ð·) <s (ðī |s ðĩ)) â ({(ðķ |s ð·)} â V â§ ðĩ â V)) |
70 | | ssltss2 27636 |
. . . . . . . . . . . 12
âĒ (ðī <<s ðĩ â ðĩ â No
) |
71 | 70 | ad3antrrr 727 |
. . . . . . . . . . 11
âĒ ((((ðī <<s ðĩ â§ ðķ <<s ð·) â§ (âð â ð· (ðī |s ðĩ) <s ð â§ âð â ðī ð <s (ðķ |s ð·))) â§ (ðķ |s ð·) <s (ðī |s ðĩ)) â ðĩ â No
) |
72 | 52 | adantr 480 |
. . . . . . . . . . . . . 14
âĒ
(((((ðī <<s
ðĩ â§ ðķ <<s ð·) â§ (âð â ð· (ðī |s ðĩ) <s ð â§ âð â ðī ð <s (ðķ |s ð·))) â§ (ðķ |s ð·) <s (ðī |s ðĩ)) â§ ð â ðĩ) â (ðķ |s ð·) â No
) |
73 | 48 | ad3antrrr 727 |
. . . . . . . . . . . . . 14
âĒ
(((((ðī <<s
ðĩ â§ ðķ <<s ð·) â§ (âð â ð· (ðī |s ðĩ) <s ð â§ âð â ðī ð <s (ðķ |s ð·))) â§ (ðķ |s ð·) <s (ðī |s ðĩ)) â§ ð â ðĩ) â (ðī |s ðĩ) â No
) |
74 | 71 | sselda 3982 |
. . . . . . . . . . . . . 14
âĒ
(((((ðī <<s
ðĩ â§ ðķ <<s ð·) â§ (âð â ð· (ðī |s ðĩ) <s ð â§ âð â ðī ð <s (ðķ |s ð·))) â§ (ðķ |s ð·) <s (ðī |s ðĩ)) â§ ð â ðĩ) â ð â No
) |
75 | | simplr 766 |
. . . . . . . . . . . . . 14
âĒ
(((((ðī <<s
ðĩ â§ ðķ <<s ð·) â§ (âð â ð· (ðī |s ðĩ) <s ð â§ âð â ðī ð <s (ðķ |s ð·))) â§ (ðķ |s ð·) <s (ðī |s ðĩ)) â§ ð â ðĩ) â (ðķ |s ð·) <s (ðī |s ðĩ)) |
76 | 28 | simp3d 1143 |
. . . . . . . . . . . . . . . . . 18
âĒ (ðī <<s ðĩ â {(ðī |s ðĩ)} <<s ðĩ) |
77 | 76 | ad3antrrr 727 |
. . . . . . . . . . . . . . . . 17
âĒ ((((ðī <<s ðĩ â§ ðķ <<s ð·) â§ (âð â ð· (ðī |s ðĩ) <s ð â§ âð â ðī ð <s (ðķ |s ð·))) â§ (ðķ |s ð·) <s (ðī |s ðĩ)) â {(ðī |s ðĩ)} <<s ðĩ) |
78 | | ssltsep 27637 |
. . . . . . . . . . . . . . . . 17
âĒ ({(ðī |s ðĩ)} <<s ðĩ â âð â {(ðī |s ðĩ)}âð â ðĩ ð <s ð) |
79 | 77, 78 | syl 17 |
. . . . . . . . . . . . . . . 16
âĒ ((((ðī <<s ðĩ â§ ðķ <<s ð·) â§ (âð â ð· (ðī |s ðĩ) <s ð â§ âð â ðī ð <s (ðķ |s ð·))) â§ (ðķ |s ð·) <s (ðī |s ðĩ)) â âð â {(ðī |s ðĩ)}âð â ðĩ ð <s ð) |
80 | | breq1 5151 |
. . . . . . . . . . . . . . . . . 18
âĒ (ð = (ðī |s ðĩ) â (ð <s ð â (ðī |s ðĩ) <s ð)) |
81 | 80 | ralbidv 3176 |
. . . . . . . . . . . . . . . . 17
âĒ (ð = (ðī |s ðĩ) â (âð â ðĩ ð <s ð â âð â ðĩ (ðī |s ðĩ) <s ð)) |
82 | 35, 81 | ralsn 4685 |
. . . . . . . . . . . . . . . 16
âĒ
(âð â
{(ðī |s ðĩ)}âð â ðĩ ð <s ð â âð â ðĩ (ðī |s ðĩ) <s ð) |
83 | 79, 82 | sylib 217 |
. . . . . . . . . . . . . . 15
âĒ ((((ðī <<s ðĩ â§ ðķ <<s ð·) â§ (âð â ð· (ðī |s ðĩ) <s ð â§ âð â ðī ð <s (ðķ |s ð·))) â§ (ðķ |s ð·) <s (ðī |s ðĩ)) â âð â ðĩ (ðī |s ðĩ) <s ð) |
84 | 83 | r19.21bi 3247 |
. . . . . . . . . . . . . 14
âĒ
(((((ðī <<s
ðĩ â§ ðķ <<s ð·) â§ (âð â ð· (ðī |s ðĩ) <s ð â§ âð â ðī ð <s (ðķ |s ð·))) â§ (ðķ |s ð·) <s (ðī |s ðĩ)) â§ ð â ðĩ) â (ðī |s ðĩ) <s ð) |
85 | 72, 73, 74, 75, 84 | slttrd 27606 |
. . . . . . . . . . . . 13
âĒ
(((((ðī <<s
ðĩ â§ ðķ <<s ð·) â§ (âð â ð· (ðī |s ðĩ) <s ð â§ âð â ðī ð <s (ðķ |s ð·))) â§ (ðķ |s ð·) <s (ðī |s ðĩ)) â§ ð â ðĩ) â (ðķ |s ð·) <s ð) |
86 | 85 | ralrimiva 3145 |
. . . . . . . . . . . 12
âĒ ((((ðī <<s ðĩ â§ ðķ <<s ð·) â§ (âð â ð· (ðī |s ðĩ) <s ð â§ âð â ðī ð <s (ðķ |s ð·))) â§ (ðķ |s ð·) <s (ðī |s ðĩ)) â âð â ðĩ (ðķ |s ð·) <s ð) |
87 | | breq1 5151 |
. . . . . . . . . . . . . 14
âĒ (ð = (ðķ |s ð·) â (ð <s ð â (ðķ |s ð·) <s ð)) |
88 | 87 | ralbidv 3176 |
. . . . . . . . . . . . 13
âĒ (ð = (ðķ |s ð·) â (âð â ðĩ ð <s ð â âð â ðĩ (ðķ |s ð·) <s ð)) |
89 | 14, 88 | ralsn 4685 |
. . . . . . . . . . . 12
âĒ
(âð â
{(ðķ |s ð·)}âð â ðĩ ð <s ð â âð â ðĩ (ðķ |s ð·) <s ð) |
90 | 86, 89 | sylibr 233 |
. . . . . . . . . . 11
âĒ ((((ðī <<s ðĩ â§ ðķ <<s ð·) â§ (âð â ð· (ðī |s ðĩ) <s ð â§ âð â ðī ð <s (ðķ |s ð·))) â§ (ðķ |s ð·) <s (ðī |s ðĩ)) â âð â {(ðķ |s ð·)}âð â ðĩ ð <s ð) |
91 | 58, 71, 90 | 3jca 1127 |
. . . . . . . . . 10
âĒ ((((ðī <<s ðĩ â§ ðķ <<s ð·) â§ (âð â ð· (ðī |s ðĩ) <s ð â§ âð â ðī ð <s (ðķ |s ð·))) â§ (ðķ |s ð·) <s (ðī |s ðĩ)) â ({(ðķ |s ð·)} â No
â§ ðĩ â No â§ âð â {(ðķ |s ð·)}âð â ðĩ ð <s ð)) |
92 | | brsslt 27632 |
. . . . . . . . . 10
âĒ ({(ðķ |s ð·)} <<s ðĩ â (({(ðķ |s ð·)} â V â§ ðĩ â V) â§ ({(ðķ |s ð·)} â No
â§ ðĩ â No â§ âð â {(ðķ |s ð·)}âð â ðĩ ð <s ð))) |
93 | 69, 91, 92 | sylanbrc 582 |
. . . . . . . . 9
âĒ ((((ðī <<s ðĩ â§ ðķ <<s ð·) â§ (âð â ð· (ðī |s ðĩ) <s ð â§ âð â ðī ð <s (ðķ |s ð·))) â§ (ðķ |s ð·) <s (ðī |s ðĩ)) â {(ðķ |s ð·)} <<s ðĩ) |
94 | | sltirr 27593 |
. . . . . . . . . . . . . 14
âĒ ((ðī |s ðĩ) â No
â ÂŽ (ðī |s ðĩ) <s (ðī |s ðĩ)) |
95 | 49, 94 | syl 17 |
. . . . . . . . . . . . 13
âĒ (((ðī <<s ðĩ â§ ðķ <<s ð·) â§ (âð â ð· (ðī |s ðĩ) <s ð â§ âð â ðī ð <s (ðķ |s ð·))) â ÂŽ (ðī |s ðĩ) <s (ðī |s ðĩ)) |
96 | | breq1 5151 |
. . . . . . . . . . . . . 14
âĒ ((ðī |s ðĩ) = (ðķ |s ð·) â ((ðī |s ðĩ) <s (ðī |s ðĩ) â (ðķ |s ð·) <s (ðī |s ðĩ))) |
97 | 96 | notbid 318 |
. . . . . . . . . . . . 13
âĒ ((ðī |s ðĩ) = (ðķ |s ð·) â (ÂŽ (ðī |s ðĩ) <s (ðī |s ðĩ) â ÂŽ (ðķ |s ð·) <s (ðī |s ðĩ))) |
98 | 95, 97 | syl5ibcom 244 |
. . . . . . . . . . . 12
âĒ (((ðī <<s ðĩ â§ ðķ <<s ð·) â§ (âð â ð· (ðī |s ðĩ) <s ð â§ âð â ðī ð <s (ðķ |s ð·))) â ((ðī |s ðĩ) = (ðķ |s ð·) â ÂŽ (ðķ |s ð·) <s (ðī |s ðĩ))) |
99 | 98 | necon2ad 2954 |
. . . . . . . . . . 11
âĒ (((ðī <<s ðĩ â§ ðķ <<s ð·) â§ (âð â ð· (ðī |s ðĩ) <s ð â§ âð â ðī ð <s (ðķ |s ð·))) â ((ðķ |s ð·) <s (ðī |s ðĩ) â (ðī |s ðĩ) â (ðķ |s ð·))) |
100 | 99 | imp 406 |
. . . . . . . . . 10
âĒ ((((ðī <<s ðĩ â§ ðķ <<s ð·) â§ (âð â ð· (ðī |s ðĩ) <s ð â§ âð â ðī ð <s (ðķ |s ð·))) â§ (ðķ |s ð·) <s (ðī |s ðĩ)) â (ðī |s ðĩ) â (ðķ |s ð·)) |
101 | 100 | necomd 2995 |
. . . . . . . . 9
âĒ ((((ðī <<s ðĩ â§ ðķ <<s ð·) â§ (âð â ð· (ðī |s ðĩ) <s ð â§ âð â ðī ð <s (ðķ |s ð·))) â§ (ðķ |s ð·) <s (ðī |s ðĩ)) â (ðķ |s ð·) â (ðī |s ðĩ)) |
102 | | scutbdaylt 27665 |
. . . . . . . . 9
âĒ (((ðķ |s ð·) â No
â§ (ðī <<s {(ðķ |s ð·)} â§ {(ðķ |s ð·)} <<s ðĩ) â§ (ðķ |s ð·) â (ðī |s ðĩ)) â ( bday
â(ðī |s ðĩ)) â ( bday â(ðķ |s ð·))) |
103 | 52, 66, 93, 101, 102 | syl121anc 1374 |
. . . . . . . 8
âĒ ((((ðī <<s ðĩ â§ ðķ <<s ð·) â§ (âð â ð· (ðī |s ðĩ) <s ð â§ âð â ðī ð <s (ðķ |s ð·))) â§ (ðķ |s ð·) <s (ðī |s ðĩ)) â ( bday
â(ðī |s ðĩ)) â ( bday â(ðķ |s ð·))) |
104 | 1 | ad3antrrr 727 |
. . . . . . . . 9
âĒ ((((ðī <<s ðĩ â§ ðķ <<s ð·) â§ (âð â ð· (ðī |s ðĩ) <s ð â§ âð â ðī ð <s (ðķ |s ð·))) â§ (ðķ |s ð·) <s (ðī |s ðĩ)) â (ðī |s ðĩ) â No
) |
105 | | ssltex1 27633 |
. . . . . . . . . . . 12
âĒ (ðķ <<s ð· â ðķ â V) |
106 | 105 | ad3antlr 728 |
. . . . . . . . . . 11
âĒ ((((ðī <<s ðĩ â§ ðķ <<s ð·) â§ (âð â ð· (ðī |s ðĩ) <s ð â§ âð â ðī ð <s (ðķ |s ð·))) â§ (ðķ |s ð·) <s (ðī |s ðĩ)) â ðķ â V) |
107 | | snex 5431 |
. . . . . . . . . . 11
âĒ {(ðī |s ðĩ)} â V |
108 | 106, 107 | jctir 520 |
. . . . . . . . . 10
âĒ ((((ðī <<s ðĩ â§ ðķ <<s ð·) â§ (âð â ð· (ðī |s ðĩ) <s ð â§ âð â ðī ð <s (ðķ |s ð·))) â§ (ðķ |s ð·) <s (ðī |s ðĩ)) â (ðķ â V â§ {(ðī |s ðĩ)} â V)) |
109 | | ssltss1 27635 |
. . . . . . . . . . . 12
âĒ (ðķ <<s ð· â ðķ â No
) |
110 | 109 | ad3antlr 728 |
. . . . . . . . . . 11
âĒ ((((ðī <<s ðĩ â§ ðķ <<s ð·) â§ (âð â ð· (ðī |s ðĩ) <s ð â§ âð â ðī ð <s (ðķ |s ð·))) â§ (ðķ |s ð·) <s (ðī |s ðĩ)) â ðķ â No
) |
111 | 104 | snssd 4812 |
. . . . . . . . . . 11
âĒ ((((ðī <<s ðĩ â§ ðķ <<s ð·) â§ (âð â ð· (ðī |s ðĩ) <s ð â§ âð â ðī ð <s (ðķ |s ð·))) â§ (ðķ |s ð·) <s (ðī |s ðĩ)) â {(ðī |s ðĩ)} â No
) |
112 | 110 | sselda 3982 |
. . . . . . . . . . . . . 14
âĒ
(((((ðī <<s
ðĩ â§ ðķ <<s ð·) â§ (âð â ð· (ðī |s ðĩ) <s ð â§ âð â ðī ð <s (ðķ |s ð·))) â§ (ðķ |s ð·) <s (ðī |s ðĩ)) â§ ð â ðķ) â ð â No
) |
113 | 52 | adantr 480 |
. . . . . . . . . . . . . 14
âĒ
(((((ðī <<s
ðĩ â§ ðķ <<s ð·) â§ (âð â ð· (ðī |s ðĩ) <s ð â§ âð â ðī ð <s (ðķ |s ð·))) â§ (ðķ |s ð·) <s (ðī |s ðĩ)) â§ ð â ðķ) â (ðķ |s ð·) â No
) |
114 | 48 | ad3antrrr 727 |
. . . . . . . . . . . . . 14
âĒ
(((((ðī <<s
ðĩ â§ ðķ <<s ð·) â§ (âð â ð· (ðī |s ðĩ) <s ð â§ âð â ðī ð <s (ðķ |s ð·))) â§ (ðķ |s ð·) <s (ðī |s ðĩ)) â§ ð â ðķ) â (ðī |s ðĩ) â No
) |
115 | 9 | simp2d 1142 |
. . . . . . . . . . . . . . . . . 18
âĒ (ðķ <<s ð· â ðķ <<s {(ðķ |s ð·)}) |
116 | 115 | ad3antlr 728 |
. . . . . . . . . . . . . . . . 17
âĒ ((((ðī <<s ðĩ â§ ðķ <<s ð·) â§ (âð â ð· (ðī |s ðĩ) <s ð â§ âð â ðī ð <s (ðķ |s ð·))) â§ (ðķ |s ð·) <s (ðī |s ðĩ)) â ðķ <<s {(ðķ |s ð·)}) |
117 | | ssltsep 27637 |
. . . . . . . . . . . . . . . . 17
âĒ (ðķ <<s {(ðķ |s ð·)} â âð â ðķ âð â {(ðķ |s ð·)}ð <s ð) |
118 | 116, 117 | syl 17 |
. . . . . . . . . . . . . . . 16
âĒ ((((ðī <<s ðĩ â§ ðķ <<s ð·) â§ (âð â ð· (ðī |s ðĩ) <s ð â§ âð â ðī ð <s (ðķ |s ð·))) â§ (ðķ |s ð·) <s (ðī |s ðĩ)) â âð â ðķ âð â {(ðķ |s ð·)}ð <s ð) |
119 | 118 | r19.21bi 3247 |
. . . . . . . . . . . . . . 15
âĒ
(((((ðī <<s
ðĩ â§ ðķ <<s ð·) â§ (âð â ð· (ðī |s ðĩ) <s ð â§ âð â ðī ð <s (ðķ |s ð·))) â§ (ðķ |s ð·) <s (ðī |s ðĩ)) â§ ð â ðķ) â âð â {(ðķ |s ð·)}ð <s ð) |
120 | | breq2 5152 |
. . . . . . . . . . . . . . . 16
âĒ (ð = (ðķ |s ð·) â (ð <s ð â ð <s (ðķ |s ð·))) |
121 | 14, 120 | ralsn 4685 |
. . . . . . . . . . . . . . 15
âĒ
(âð â
{(ðķ |s ð·)}ð <s ð â ð <s (ðķ |s ð·)) |
122 | 119, 121 | sylib 217 |
. . . . . . . . . . . . . 14
âĒ
(((((ðī <<s
ðĩ â§ ðķ <<s ð·) â§ (âð â ð· (ðī |s ðĩ) <s ð â§ âð â ðī ð <s (ðķ |s ð·))) â§ (ðķ |s ð·) <s (ðī |s ðĩ)) â§ ð â ðķ) â ð <s (ðķ |s ð·)) |
123 | | simplr 766 |
. . . . . . . . . . . . . 14
âĒ
(((((ðī <<s
ðĩ â§ ðķ <<s ð·) â§ (âð â ð· (ðī |s ðĩ) <s ð â§ âð â ðī ð <s (ðķ |s ð·))) â§ (ðķ |s ð·) <s (ðī |s ðĩ)) â§ ð â ðķ) â (ðķ |s ð·) <s (ðī |s ðĩ)) |
124 | 112, 113,
114, 122, 123 | slttrd 27606 |
. . . . . . . . . . . . 13
âĒ
(((((ðī <<s
ðĩ â§ ðķ <<s ð·) â§ (âð â ð· (ðī |s ðĩ) <s ð â§ âð â ðī ð <s (ðķ |s ð·))) â§ (ðķ |s ð·) <s (ðī |s ðĩ)) â§ ð â ðķ) â ð <s (ðī |s ðĩ)) |
125 | | breq2 5152 |
. . . . . . . . . . . . . 14
âĒ (ð = (ðī |s ðĩ) â (ð <s ð â ð <s (ðī |s ðĩ))) |
126 | 35, 125 | ralsn 4685 |
. . . . . . . . . . . . 13
âĒ
(âð â
{(ðī |s ðĩ)}ð <s ð â ð <s (ðī |s ðĩ)) |
127 | 124, 126 | sylibr 233 |
. . . . . . . . . . . 12
âĒ
(((((ðī <<s
ðĩ â§ ðķ <<s ð·) â§ (âð â ð· (ðī |s ðĩ) <s ð â§ âð â ðī ð <s (ðķ |s ð·))) â§ (ðķ |s ð·) <s (ðī |s ðĩ)) â§ ð â ðķ) â âð â {(ðī |s ðĩ)}ð <s ð) |
128 | 127 | ralrimiva 3145 |
. . . . . . . . . . 11
âĒ ((((ðī <<s ðĩ â§ ðķ <<s ð·) â§ (âð â ð· (ðī |s ðĩ) <s ð â§ âð â ðī ð <s (ðķ |s ð·))) â§ (ðķ |s ð·) <s (ðī |s ðĩ)) â âð â ðķ âð â {(ðī |s ðĩ)}ð <s ð) |
129 | 110, 111,
128 | 3jca 1127 |
. . . . . . . . . 10
âĒ ((((ðī <<s ðĩ â§ ðķ <<s ð·) â§ (âð â ð· (ðī |s ðĩ) <s ð â§ âð â ðī ð <s (ðķ |s ð·))) â§ (ðķ |s ð·) <s (ðī |s ðĩ)) â (ðķ â No
â§ {(ðī |s ðĩ)} â No â§ âð â ðķ âð â {(ðī |s ðĩ)}ð <s ð)) |
130 | | brsslt 27632 |
. . . . . . . . . 10
âĒ (ðķ <<s {(ðī |s ðĩ)} â ((ðķ â V â§ {(ðī |s ðĩ)} â V) â§ (ðķ â No
â§ {(ðī |s ðĩ)} â No â§ âð â ðķ âð â {(ðī |s ðĩ)}ð <s ð))) |
131 | 108, 129,
130 | sylanbrc 582 |
. . . . . . . . 9
âĒ ((((ðī <<s ðĩ â§ ðķ <<s ð·) â§ (âð â ð· (ðī |s ðĩ) <s ð â§ âð â ðī ð <s (ðķ |s ð·))) â§ (ðķ |s ð·) <s (ðī |s ðĩ)) â ðķ <<s {(ðī |s ðĩ)}) |
132 | | ssltex2 27634 |
. . . . . . . . . . . 12
âĒ (ðķ <<s ð· â ð· â V) |
133 | 132 | ad3antlr 728 |
. . . . . . . . . . 11
âĒ ((((ðī <<s ðĩ â§ ðķ <<s ð·) â§ (âð â ð· (ðī |s ðĩ) <s ð â§ âð â ðī ð <s (ðķ |s ð·))) â§ (ðķ |s ð·) <s (ðī |s ðĩ)) â ð· â V) |
134 | 133, 107 | jctil 519 |
. . . . . . . . . 10
âĒ ((((ðī <<s ðĩ â§ ðķ <<s ð·) â§ (âð â ð· (ðī |s ðĩ) <s ð â§ âð â ðī ð <s (ðķ |s ð·))) â§ (ðķ |s ð·) <s (ðī |s ðĩ)) â ({(ðī |s ðĩ)} â V â§ ð· â V)) |
135 | 5 | ad3antlr 728 |
. . . . . . . . . . 11
âĒ ((((ðī <<s ðĩ â§ ðķ <<s ð·) â§ (âð â ð· (ðī |s ðĩ) <s ð â§ âð â ðī ð <s (ðķ |s ð·))) â§ (ðķ |s ð·) <s (ðī |s ðĩ)) â ð· â No
) |
136 | | simplrl 774 |
. . . . . . . . . . . 12
âĒ ((((ðī <<s ðĩ â§ ðķ <<s ð·) â§ (âð â ð· (ðī |s ðĩ) <s ð â§ âð â ðī ð <s (ðķ |s ð·))) â§ (ðķ |s ð·) <s (ðī |s ðĩ)) â âð â ð· (ðī |s ðĩ) <s ð) |
137 | | breq1 5151 |
. . . . . . . . . . . . . 14
âĒ (ð = (ðī |s ðĩ) â (ð <s ð â (ðī |s ðĩ) <s ð)) |
138 | 137 | ralbidv 3176 |
. . . . . . . . . . . . 13
âĒ (ð = (ðī |s ðĩ) â (âð â ð· ð <s ð â âð â ð· (ðī |s ðĩ) <s ð)) |
139 | 35, 138 | ralsn 4685 |
. . . . . . . . . . . 12
âĒ
(âð â
{(ðī |s ðĩ)}âð â ð· ð <s ð â âð â ð· (ðī |s ðĩ) <s ð) |
140 | 136, 139 | sylibr 233 |
. . . . . . . . . . 11
âĒ ((((ðī <<s ðĩ â§ ðķ <<s ð·) â§ (âð â ð· (ðī |s ðĩ) <s ð â§ âð â ðī ð <s (ðķ |s ð·))) â§ (ðķ |s ð·) <s (ðī |s ðĩ)) â âð â {(ðī |s ðĩ)}âð â ð· ð <s ð) |
141 | 111, 135,
140 | 3jca 1127 |
. . . . . . . . . 10
âĒ ((((ðī <<s ðĩ â§ ðķ <<s ð·) â§ (âð â ð· (ðī |s ðĩ) <s ð â§ âð â ðī ð <s (ðķ |s ð·))) â§ (ðķ |s ð·) <s (ðī |s ðĩ)) â ({(ðī |s ðĩ)} â No
â§ ð· â No â§ âð â {(ðī |s ðĩ)}âð â ð· ð <s ð)) |
142 | | brsslt 27632 |
. . . . . . . . . 10
âĒ ({(ðī |s ðĩ)} <<s ð· â (({(ðī |s ðĩ)} â V â§ ð· â V) â§ ({(ðī |s ðĩ)} â No
â§ ð· â No â§ âð â {(ðī |s ðĩ)}âð â ð· ð <s ð))) |
143 | 134, 141,
142 | sylanbrc 582 |
. . . . . . . . 9
âĒ ((((ðī <<s ðĩ â§ ðķ <<s ð·) â§ (âð â ð· (ðī |s ðĩ) <s ð â§ âð â ðī ð <s (ðķ |s ð·))) â§ (ðķ |s ð·) <s (ðī |s ðĩ)) â {(ðī |s ðĩ)} <<s ð·) |
144 | | scutbdaylt 27665 |
. . . . . . . . 9
âĒ (((ðī |s ðĩ) â No
â§ (ðķ <<s {(ðī |s ðĩ)} â§ {(ðī |s ðĩ)} <<s ð·) â§ (ðī |s ðĩ) â (ðķ |s ð·)) â ( bday
â(ðķ |s ð·)) â ( bday â(ðī |s ðĩ))) |
145 | 104, 131,
143, 100, 144 | syl121anc 1374 |
. . . . . . . 8
âĒ ((((ðī <<s ðĩ â§ ðķ <<s ð·) â§ (âð â ð· (ðī |s ðĩ) <s ð â§ âð â ðī ð <s (ðķ |s ð·))) â§ (ðķ |s ð·) <s (ðī |s ðĩ)) â ( bday
â(ðķ |s ð·)) â ( bday â(ðī |s ðĩ))) |
146 | 103, 145 | jca 511 |
. . . . . . 7
âĒ ((((ðī <<s ðĩ â§ ðķ <<s ð·) â§ (âð â ð· (ðī |s ðĩ) <s ð â§ âð â ðī ð <s (ðķ |s ð·))) â§ (ðķ |s ð·) <s (ðī |s ðĩ)) â (( bday
â(ðī |s ðĩ)) â ( bday â(ðķ |s ð·)) â§ ( bday
â(ðķ |s ð·)) â ( bday â(ðī |s ðĩ)))) |
147 | 146 | ex 412 |
. . . . . 6
âĒ (((ðī <<s ðĩ â§ ðķ <<s ð·) â§ (âð â ð· (ðī |s ðĩ) <s ð â§ âð â ðī ð <s (ðķ |s ð·))) â ((ðķ |s ð·) <s (ðī |s ðĩ) â (( bday
â(ðī |s ðĩ)) â ( bday â(ðķ |s ð·)) â§ ( bday
â(ðķ |s ð·)) â ( bday â(ðī |s ðĩ))))) |
148 | 51, 147 | sylbird 260 |
. . . . 5
âĒ (((ðī <<s ðĩ â§ ðķ <<s ð·) â§ (âð â ð· (ðī |s ðĩ) <s ð â§ âð â ðī ð <s (ðķ |s ð·))) â (ÂŽ (ðī |s ðĩ) âĪs (ðķ |s ð·) â (( bday
â(ðī |s ðĩ)) â ( bday â(ðķ |s ð·)) â§ ( bday
â(ðķ |s ð·)) â ( bday â(ðī |s ðĩ))))) |
149 | 46, 148 | mt3i 149 |
. . . 4
âĒ (((ðī <<s ðĩ â§ ðķ <<s ð·) â§ (âð â ð· (ðī |s ðĩ) <s ð â§ âð â ðī ð <s (ðķ |s ð·))) â (ðī |s ðĩ) âĪs (ðķ |s ð·)) |
150 | 42, 149 | impbida 798 |
. . 3
âĒ ((ðī <<s ðĩ â§ ðķ <<s ð·) â ((ðī |s ðĩ) âĪs (ðķ |s ð·) â (âð â ð· (ðī |s ðĩ) <s ð â§ âð â ðī ð <s (ðķ |s ð·)))) |
151 | | breq12 5153 |
. . . 4
âĒ ((ð = (ðī |s ðĩ) â§ ð = (ðķ |s ð·)) â (ð âĪs ð â (ðī |s ðĩ) âĪs (ðķ |s ð·))) |
152 | | breq1 5151 |
. . . . . 6
âĒ (ð = (ðī |s ðĩ) â (ð <s ð â (ðī |s ðĩ) <s ð)) |
153 | 152 | ralbidv 3176 |
. . . . 5
âĒ (ð = (ðī |s ðĩ) â (âð â ð· ð <s ð â âð â ð· (ðī |s ðĩ) <s ð)) |
154 | | breq2 5152 |
. . . . . 6
âĒ (ð = (ðķ |s ð·) â (ð <s ð â ð <s (ðķ |s ð·))) |
155 | 154 | ralbidv 3176 |
. . . . 5
âĒ (ð = (ðķ |s ð·) â (âð â ðī ð <s ð â âð â ðī ð <s (ðķ |s ð·))) |
156 | 153, 155 | bi2anan9 636 |
. . . 4
âĒ ((ð = (ðī |s ðĩ) â§ ð = (ðķ |s ð·)) â ((âð â ð· ð <s ð â§ âð â ðī ð <s ð) â (âð â ð· (ðī |s ðĩ) <s ð â§ âð â ðī ð <s (ðķ |s ð·)))) |
157 | 151, 156 | bibi12d 345 |
. . 3
âĒ ((ð = (ðī |s ðĩ) â§ ð = (ðķ |s ð·)) â ((ð âĪs ð â (âð â ð· ð <s ð â§ âð â ðī ð <s ð)) â ((ðī |s ðĩ) âĪs (ðķ |s ð·) â (âð â ð· (ðī |s ðĩ) <s ð â§ âð â ðī ð <s (ðķ |s ð·))))) |
158 | 150, 157 | imbitrrid 245 |
. 2
âĒ ((ð = (ðī |s ðĩ) â§ ð = (ðķ |s ð·)) â ((ðī <<s ðĩ â§ ðķ <<s ð·) â (ð âĪs ð â (âð â ð· ð <s ð â§ âð â ðī ð <s ð)))) |
159 | 158 | impcom 407 |
1
âĒ (((ðī <<s ðĩ â§ ðķ <<s ð·) â§ (ð = (ðī |s ðĩ) â§ ð = (ðķ |s ð·))) â (ð âĪs ð â (âð â ð· ð <s ð â§ âð â ðī ð <s ð))) |