Step | Hyp | Ref
| Expression |
1 | | ssun1 4133 |
. . . . . . . 8
âĒ ðī â (ðī ⊠ðĩ) |
2 | | sstr 3953 |
. . . . . . . 8
âĒ ((ðī â (ðī ⊠ðĩ) ⧠(ðī ⊠ðĩ) â ( O â(
bday âð)))
â ðī â ( O
â( bday âð))) |
3 | 1, 2 | mpan 689 |
. . . . . . 7
âĒ ((ðī ⊠ðĩ) â ( O â(
bday âð))
â ðī â ( O
â( bday âð))) |
4 | 3 | 3ad2ant1 1134 |
. . . . . 6
âĒ (((ðī ⊠ðĩ) â ( O â(
bday âð))
⧠ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) â ðī â ( O â(
bday âð))) |
5 | 4 | sselda 3945 |
. . . . 5
âĒ ((((ðī ⊠ðĩ) â ( O â(
bday âð))
⧠ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ðĨ â ðī) â ðĨ â ( O â(
bday âð))) |
6 | | simpl2 1193 |
. . . . . . . . 9
âĒ ((((ðī ⊠ðĩ) â ( O â(
bday âð))
⧠ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ðĨ â ðī) â ðī <<s ðĩ) |
7 | | scutcut 27143 |
. . . . . . . . 9
âĒ (ðī <<s ðĩ â ((ðī |s ðĩ) â No
⧠ðī <<s {(ðī |s ðĩ)} ⧠{(ðī |s ðĩ)} <<s ðĩ)) |
8 | 6, 7 | syl 17 |
. . . . . . . 8
âĒ ((((ðī ⊠ðĩ) â ( O â(
bday âð))
⧠ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ðĨ â ðī) â ((ðī |s ðĩ) â No
⧠ðī <<s {(ðī |s ðĩ)} ⧠{(ðī |s ðĩ)} <<s ðĩ)) |
9 | 8 | simp2d 1144 |
. . . . . . 7
âĒ ((((ðī ⊠ðĩ) â ( O â(
bday âð))
⧠ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ðĨ â ðī) â ðī <<s {(ðī |s ðĩ)}) |
10 | | simpr 486 |
. . . . . . 7
âĒ ((((ðī ⊠ðĩ) â ( O â(
bday âð))
⧠ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ðĨ â ðī) â ðĨ â ðī) |
11 | | ovex 7391 |
. . . . . . . . 9
âĒ (ðī |s ðĩ) â V |
12 | 11 | snid 4623 |
. . . . . . . 8
âĒ (ðī |s ðĩ) â {(ðī |s ðĩ)} |
13 | 12 | a1i 11 |
. . . . . . 7
âĒ ((((ðī ⊠ðĩ) â ( O â(
bday âð))
⧠ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ðĨ â ðī) â (ðī |s ðĩ) â {(ðī |s ðĩ)}) |
14 | 9, 10, 13 | ssltsepcd 27136 |
. . . . . 6
âĒ ((((ðī ⊠ðĩ) â ( O â(
bday âð))
⧠ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ðĨ â ðī) â ðĨ <s (ðī |s ðĩ)) |
15 | | simpl3 1194 |
. . . . . 6
âĒ ((((ðī ⊠ðĩ) â ( O â(
bday âð))
⧠ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ðĨ â ðī) â ð = (ðī |s ðĩ)) |
16 | 14, 15 | breqtrrd 5134 |
. . . . 5
âĒ ((((ðī ⊠ðĩ) â ( O â(
bday âð))
⧠ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ðĨ â ðī) â ðĨ <s ð) |
17 | | leftval 27196 |
. . . . . . . 8
âĒ ( L
âð) = {ðĨ â ( O â( bday âð)) âĢ ðĨ <s ð} |
18 | 17 | a1i 11 |
. . . . . . 7
âĒ ((((ðī ⊠ðĩ) â ( O â(
bday âð))
⧠ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ðĨ â ðī) â ( L âð) = {ðĨ â ( O â(
bday âð))
âĢ ðĨ <s ð}) |
19 | 18 | eleq2d 2824 |
. . . . . 6
âĒ ((((ðī ⊠ðĩ) â ( O â(
bday âð))
⧠ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ðĨ â ðī) â (ðĨ â ( L âð) â ðĨ â {ðĨ â ( O â(
bday âð))
âĢ ðĨ <s ð})) |
20 | | rabid 3428 |
. . . . . 6
âĒ (ðĨ â {ðĨ â ( O â(
bday âð))
âĢ ðĨ <s ð} â (ðĨ â ( O â(
bday âð))
⧠ðĨ <s ð)) |
21 | 19, 20 | bitrdi 287 |
. . . . 5
âĒ ((((ðī ⊠ðĩ) â ( O â(
bday âð))
⧠ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ðĨ â ðī) â (ðĨ â ( L âð) â (ðĨ â ( O â(
bday âð))
⧠ðĨ <s ð))) |
22 | 5, 16, 21 | mpbir2and 712 |
. . . 4
âĒ ((((ðī ⊠ðĩ) â ( O â(
bday âð))
⧠ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ðĨ â ðī) â ðĨ â ( L âð)) |
23 | | leftssno 27213 |
. . . . . 6
âĒ ( L
âð) â No |
24 | 23, 22 | sselid 3943 |
. . . . 5
âĒ ((((ðī ⊠ðĩ) â ( O â(
bday âð))
⧠ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ðĨ â ðī) â ðĨ â No
) |
25 | | slerflex 27114 |
. . . . 5
âĒ (ðĨ â
No â ðĨ âĪs
ðĨ) |
26 | 24, 25 | syl 17 |
. . . 4
âĒ ((((ðī ⊠ðĩ) â ( O â(
bday âð))
⧠ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ðĨ â ðī) â ðĨ âĪs ðĨ) |
27 | | breq2 5110 |
. . . . 5
âĒ (ðĶ = ðĨ â (ðĨ âĪs ðĶ â ðĨ âĪs ðĨ)) |
28 | 27 | rspcev 3582 |
. . . 4
âĒ ((ðĨ â ( L âð) ⧠ðĨ âĪs ðĨ) â âðĶ â ( L âð)ðĨ âĪs ðĶ) |
29 | 22, 26, 28 | syl2anc 585 |
. . 3
âĒ ((((ðī ⊠ðĩ) â ( O â(
bday âð))
⧠ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ðĨ â ðī) â âðĶ â ( L âð)ðĨ âĪs ðĶ) |
30 | 29 | ralrimiva 3144 |
. 2
âĒ (((ðī ⊠ðĩ) â ( O â(
bday âð))
⧠ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) â âðĨ â ðī âðĶ â ( L âð)ðĨ âĪs ðĶ) |
31 | | ssun2 4134 |
. . . . . . . 8
âĒ ðĩ â (ðī ⊠ðĩ) |
32 | | sstr 3953 |
. . . . . . . 8
âĒ ((ðĩ â (ðī ⊠ðĩ) ⧠(ðī ⊠ðĩ) â ( O â(
bday âð)))
â ðĩ â ( O
â( bday âð))) |
33 | 31, 32 | mpan 689 |
. . . . . . 7
âĒ ((ðī ⊠ðĩ) â ( O â(
bday âð))
â ðĩ â ( O
â( bday âð))) |
34 | 33 | 3ad2ant1 1134 |
. . . . . 6
âĒ (((ðī ⊠ðĩ) â ( O â(
bday âð))
⧠ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) â ðĩ â ( O â(
bday âð))) |
35 | 34 | sselda 3945 |
. . . . 5
âĒ ((((ðī ⊠ðĩ) â ( O â(
bday âð))
⧠ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ð§ â ðĩ) â ð§ â ( O â(
bday âð))) |
36 | | simpl3 1194 |
. . . . . 6
âĒ ((((ðī ⊠ðĩ) â ( O â(
bday âð))
⧠ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ð§ â ðĩ) â ð = (ðī |s ðĩ)) |
37 | | simpl2 1193 |
. . . . . . . . 9
âĒ ((((ðī ⊠ðĩ) â ( O â(
bday âð))
⧠ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ð§ â ðĩ) â ðī <<s ðĩ) |
38 | 37, 7 | syl 17 |
. . . . . . . 8
âĒ ((((ðī ⊠ðĩ) â ( O â(
bday âð))
⧠ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ð§ â ðĩ) â ((ðī |s ðĩ) â No
⧠ðī <<s {(ðī |s ðĩ)} ⧠{(ðī |s ðĩ)} <<s ðĩ)) |
39 | 38 | simp3d 1145 |
. . . . . . 7
âĒ ((((ðī ⊠ðĩ) â ( O â(
bday âð))
⧠ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ð§ â ðĩ) â {(ðī |s ðĩ)} <<s ðĩ) |
40 | 12 | a1i 11 |
. . . . . . 7
âĒ ((((ðī ⊠ðĩ) â ( O â(
bday âð))
⧠ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ð§ â ðĩ) â (ðī |s ðĩ) â {(ðī |s ðĩ)}) |
41 | | simpr 486 |
. . . . . . 7
âĒ ((((ðī ⊠ðĩ) â ( O â(
bday âð))
⧠ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ð§ â ðĩ) â ð§ â ðĩ) |
42 | 39, 40, 41 | ssltsepcd 27136 |
. . . . . 6
âĒ ((((ðī ⊠ðĩ) â ( O â(
bday âð))
⧠ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ð§ â ðĩ) â (ðī |s ðĩ) <s ð§) |
43 | 36, 42 | eqbrtrd 5128 |
. . . . 5
âĒ ((((ðī ⊠ðĩ) â ( O â(
bday âð))
⧠ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ð§ â ðĩ) â ð <s ð§) |
44 | | rightval 27197 |
. . . . . . . 8
âĒ ( R
âð) = {ð§ â ( O â( bday âð)) âĢ ð <s ð§} |
45 | 44 | a1i 11 |
. . . . . . 7
âĒ ((((ðī ⊠ðĩ) â ( O â(
bday âð))
⧠ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ð§ â ðĩ) â ( R âð) = {ð§ â ( O â(
bday âð))
âĢ ð <s ð§}) |
46 | 45 | eleq2d 2824 |
. . . . . 6
âĒ ((((ðī ⊠ðĩ) â ( O â(
bday âð))
⧠ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ð§ â ðĩ) â (ð§ â ( R âð) â ð§ â {ð§ â ( O â(
bday âð))
âĢ ð <s ð§})) |
47 | | rabid 3428 |
. . . . . 6
âĒ (ð§ â {ð§ â ( O â(
bday âð))
âĢ ð <s ð§} â (ð§ â ( O â(
bday âð))
⧠ð <s ð§)) |
48 | 46, 47 | bitrdi 287 |
. . . . 5
âĒ ((((ðī ⊠ðĩ) â ( O â(
bday âð))
⧠ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ð§ â ðĩ) â (ð§ â ( R âð) â (ð§ â ( O â(
bday âð))
⧠ð <s ð§))) |
49 | 35, 43, 48 | mpbir2and 712 |
. . . 4
âĒ ((((ðī ⊠ðĩ) â ( O â(
bday âð))
⧠ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ð§ â ðĩ) â ð§ â ( R âð)) |
50 | | rightssno 27214 |
. . . . . 6
âĒ ( R
âð) â No |
51 | 50, 49 | sselid 3943 |
. . . . 5
âĒ ((((ðī ⊠ðĩ) â ( O â(
bday âð))
⧠ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ð§ â ðĩ) â ð§ â No
) |
52 | | slerflex 27114 |
. . . . 5
âĒ (ð§ â
No â ð§ âĪs
ð§) |
53 | 51, 52 | syl 17 |
. . . 4
âĒ ((((ðī ⊠ðĩ) â ( O â(
bday âð))
⧠ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ð§ â ðĩ) â ð§ âĪs ð§) |
54 | | breq1 5109 |
. . . . 5
âĒ (ðĪ = ð§ â (ðĪ âĪs ð§ â ð§ âĪs ð§)) |
55 | 54 | rspcev 3582 |
. . . 4
âĒ ((ð§ â ( R âð) ⧠ð§ âĪs ð§) â âðĪ â ( R âð)ðĪ âĪs ð§) |
56 | 49, 53, 55 | syl2anc 585 |
. . 3
âĒ ((((ðī ⊠ðĩ) â ( O â(
bday âð))
⧠ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) ⧠ð§ â ðĩ) â âðĪ â ( R âð)ðĪ âĪs ð§) |
57 | 56 | ralrimiva 3144 |
. 2
âĒ (((ðī ⊠ðĩ) â ( O â(
bday âð))
⧠ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) â âð§ â ðĩ âðĪ â ( R âð)ðĪ âĪs ð§) |
58 | 30, 57 | jca 513 |
1
âĒ (((ðī ⊠ðĩ) â ( O â(
bday âð))
⧠ðī <<s ðĩ ⧠ð = (ðī |s ðĩ)) â (âðĨ â ðī âðĶ â ( L âð)ðĨ âĪs ðĶ ⧠âð§ â ðĩ âðĪ â ( R âð)ðĪ âĪs ð§)) |