Step | Hyp | Ref
| Expression |
1 | | eqid 2731 |
. . . . 5
โข (๐ โ ๐ฟ, ๐ โ ๐ โฆ (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))) = (๐ โ ๐ฟ, ๐ โ ๐ โฆ (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))) |
2 | 1 | rnmpo 7525 |
. . . 4
โข ran
(๐ โ ๐ฟ, ๐ โ ๐ โฆ (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))) = {๐ โฃ โ๐ โ ๐ฟ โ๐ โ ๐ ๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} |
3 | | ssltmul1.1 |
. . . . . . 7
โข (๐ โ ๐ฟ <<s ๐
) |
4 | | ssltex1 27214 |
. . . . . . 7
โข (๐ฟ <<s ๐
โ ๐ฟ โ V) |
5 | 3, 4 | syl 17 |
. . . . . 6
โข (๐ โ ๐ฟ โ V) |
6 | | ssltmul1.2 |
. . . . . . 7
โข (๐ โ ๐ <<s ๐) |
7 | | ssltex1 27214 |
. . . . . . 7
โข (๐ <<s ๐ โ ๐ โ V) |
8 | 6, 7 | syl 17 |
. . . . . 6
โข (๐ โ ๐ โ V) |
9 | 1 | mpoexg 8045 |
. . . . . 6
โข ((๐ฟ โ V โง ๐ โ V) โ (๐ โ ๐ฟ, ๐ โ ๐ โฆ (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))) โ V) |
10 | 5, 8, 9 | syl2anc 584 |
. . . . 5
โข (๐ โ (๐ โ ๐ฟ, ๐ โ ๐ โฆ (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))) โ V) |
11 | | rnexg 7877 |
. . . . 5
โข ((๐ โ ๐ฟ, ๐ โ ๐ โฆ (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))) โ V โ ran (๐ โ ๐ฟ, ๐ โ ๐ โฆ (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))) โ V) |
12 | 10, 11 | syl 17 |
. . . 4
โข (๐ โ ran (๐ โ ๐ฟ, ๐ โ ๐ โฆ (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))) โ V) |
13 | 2, 12 | eqeltrrid 2837 |
. . 3
โข (๐ โ {๐ โฃ โ๐ โ ๐ฟ โ๐ โ ๐ ๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โ V) |
14 | | eqid 2731 |
. . . . 5
โข (๐ โ ๐
, ๐ โ ๐ โฆ (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ ))) = (๐ โ ๐
, ๐ โ ๐ โฆ (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ ))) |
15 | 14 | rnmpo 7525 |
. . . 4
โข ran
(๐ โ ๐
, ๐ โ ๐ โฆ (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ ))) = {๐ โฃ โ๐ โ ๐
โ๐ โ ๐ ๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ ))} |
16 | | ssltex2 27215 |
. . . . . . 7
โข (๐ฟ <<s ๐
โ ๐
โ V) |
17 | 3, 16 | syl 17 |
. . . . . 6
โข (๐ โ ๐
โ V) |
18 | | ssltex2 27215 |
. . . . . . 7
โข (๐ <<s ๐ โ ๐ โ V) |
19 | 6, 18 | syl 17 |
. . . . . 6
โข (๐ โ ๐ โ V) |
20 | 14 | mpoexg 8045 |
. . . . . 6
โข ((๐
โ V โง ๐ โ V) โ (๐ โ ๐
, ๐ โ ๐ โฆ (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ ))) โ V) |
21 | 17, 19, 20 | syl2anc 584 |
. . . . 5
โข (๐ โ (๐ โ ๐
, ๐ โ ๐ โฆ (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ ))) โ V) |
22 | | rnexg 7877 |
. . . . 5
โข ((๐ โ ๐
, ๐ โ ๐ โฆ (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ ))) โ V โ ran (๐ โ ๐
, ๐ โ ๐ โฆ (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ ))) โ V) |
23 | 21, 22 | syl 17 |
. . . 4
โข (๐ โ ran (๐ โ ๐
, ๐ โ ๐ โฆ (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ ))) โ V) |
24 | 15, 23 | eqeltrrid 2837 |
. . 3
โข (๐ โ {๐ โฃ โ๐ โ ๐
โ๐ โ ๐ ๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ ))} โ V) |
25 | 13, 24 | unexd 7724 |
. 2
โข (๐ โ ({๐ โฃ โ๐ โ ๐ฟ โ๐ โ ๐ ๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โช {๐ โฃ โ๐ โ ๐
โ๐ โ ๐ ๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ ))}) โ V) |
26 | | snex 5424 |
. . 3
โข {(๐ด ยทs ๐ต)} โ V |
27 | 26 | a1i 11 |
. 2
โข (๐ โ {(๐ด ยทs ๐ต)} โ V) |
28 | | ssltss1 27216 |
. . . . . . . . . . . 12
โข (๐ฟ <<s ๐
โ ๐ฟ โ No
) |
29 | 3, 28 | syl 17 |
. . . . . . . . . . 11
โข (๐ โ ๐ฟ โ No
) |
30 | 29 | adantr 481 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ ๐ฟ โง ๐ โ ๐)) โ ๐ฟ โ No
) |
31 | | simprl 769 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ ๐ฟ โง ๐ โ ๐)) โ ๐ โ ๐ฟ) |
32 | 30, 31 | sseldd 3979 |
. . . . . . . . 9
โข ((๐ โง (๐ โ ๐ฟ โง ๐ โ ๐)) โ ๐ โ No
) |
33 | | ssltmul1.4 |
. . . . . . . . . . 11
โข (๐ โ ๐ต = (๐ |s ๐)) |
34 | 6 | scutcld 27230 |
. . . . . . . . . . 11
โข (๐ โ (๐ |s ๐) โ No
) |
35 | 33, 34 | eqeltrd 2832 |
. . . . . . . . . 10
โข (๐ โ ๐ต โ No
) |
36 | 35 | adantr 481 |
. . . . . . . . 9
โข ((๐ โง (๐ โ ๐ฟ โง ๐ โ ๐)) โ ๐ต โ No
) |
37 | 32, 36 | mulscld 27504 |
. . . . . . . 8
โข ((๐ โง (๐ โ ๐ฟ โง ๐ โ ๐)) โ (๐ ยทs ๐ต) โ No
) |
38 | | ssltmul1.3 |
. . . . . . . . . . 11
โข (๐ โ ๐ด = (๐ฟ |s ๐
)) |
39 | 3 | scutcld 27230 |
. . . . . . . . . . 11
โข (๐ โ (๐ฟ |s ๐
) โ No
) |
40 | 38, 39 | eqeltrd 2832 |
. . . . . . . . . 10
โข (๐ โ ๐ด โ No
) |
41 | 40 | adantr 481 |
. . . . . . . . 9
โข ((๐ โง (๐ โ ๐ฟ โง ๐ โ ๐)) โ ๐ด โ No
) |
42 | | ssltss1 27216 |
. . . . . . . . . . . 12
โข (๐ <<s ๐ โ ๐ โ No
) |
43 | 6, 42 | syl 17 |
. . . . . . . . . . 11
โข (๐ โ ๐ โ No
) |
44 | 43 | adantr 481 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ ๐ฟ โง ๐ โ ๐)) โ ๐ โ No
) |
45 | | simprr 771 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ ๐ฟ โง ๐ โ ๐)) โ ๐ โ ๐) |
46 | 44, 45 | sseldd 3979 |
. . . . . . . . 9
โข ((๐ โง (๐ โ ๐ฟ โง ๐ โ ๐)) โ ๐ โ No
) |
47 | 41, 46 | mulscld 27504 |
. . . . . . . 8
โข ((๐ โง (๐ โ ๐ฟ โง ๐ โ ๐)) โ (๐ด ยทs ๐) โ No
) |
48 | 37, 47 | addscld 27380 |
. . . . . . 7
โข ((๐ โง (๐ โ ๐ฟ โง ๐ โ ๐)) โ ((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) โ No
) |
49 | 32, 46 | mulscld 27504 |
. . . . . . 7
โข ((๐ โง (๐ โ ๐ฟ โง ๐ โ ๐)) โ (๐ ยทs ๐) โ No
) |
50 | 48, 49 | subscld 27449 |
. . . . . 6
โข ((๐ โง (๐ โ ๐ฟ โง ๐ โ ๐)) โ (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) โ No
) |
51 | | eleq1 2820 |
. . . . . 6
โข (๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) โ (๐ โ No
โ (((๐
ยทs ๐ต)
+s (๐ด
ยทs ๐))
-s (๐
ยทs ๐))
โ No )) |
52 | 50, 51 | syl5ibrcom 246 |
. . . . 5
โข ((๐ โง (๐ โ ๐ฟ โง ๐ โ ๐)) โ (๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) โ ๐ โ No
)) |
53 | 52 | rexlimdvva 3210 |
. . . 4
โข (๐ โ (โ๐ โ ๐ฟ โ๐ โ ๐ ๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) โ ๐ โ No
)) |
54 | 53 | abssdv 4061 |
. . 3
โข (๐ โ {๐ โฃ โ๐ โ ๐ฟ โ๐ โ ๐ ๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โ No
) |
55 | | ssltss2 27217 |
. . . . . . . . . . . 12
โข (๐ฟ <<s ๐
โ ๐
โ No
) |
56 | 3, 55 | syl 17 |
. . . . . . . . . . 11
โข (๐ โ ๐
โ No
) |
57 | 56 | adantr 481 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ ๐
โง ๐ โ ๐)) โ ๐
โ No
) |
58 | | simprl 769 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ ๐
โง ๐ โ ๐)) โ ๐ โ ๐
) |
59 | 57, 58 | sseldd 3979 |
. . . . . . . . 9
โข ((๐ โง (๐ โ ๐
โง ๐ โ ๐)) โ ๐ โ No
) |
60 | 35 | adantr 481 |
. . . . . . . . 9
โข ((๐ โง (๐ โ ๐
โง ๐ โ ๐)) โ ๐ต โ No
) |
61 | 59, 60 | mulscld 27504 |
. . . . . . . 8
โข ((๐ โง (๐ โ ๐
โง ๐ โ ๐)) โ (๐ ยทs ๐ต) โ No
) |
62 | 40 | adantr 481 |
. . . . . . . . 9
โข ((๐ โง (๐ โ ๐
โง ๐ โ ๐)) โ ๐ด โ No
) |
63 | | ssltss2 27217 |
. . . . . . . . . . . 12
โข (๐ <<s ๐ โ ๐ โ No
) |
64 | 6, 63 | syl 17 |
. . . . . . . . . . 11
โข (๐ โ ๐ โ No
) |
65 | 64 | adantr 481 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ ๐
โง ๐ โ ๐)) โ ๐ โ No
) |
66 | | simprr 771 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ ๐
โง ๐ โ ๐)) โ ๐ โ ๐) |
67 | 65, 66 | sseldd 3979 |
. . . . . . . . 9
โข ((๐ โง (๐ โ ๐
โง ๐ โ ๐)) โ ๐ โ No
) |
68 | 62, 67 | mulscld 27504 |
. . . . . . . 8
โข ((๐ โง (๐ โ ๐
โง ๐ โ ๐)) โ (๐ด ยทs ๐ ) โ No
) |
69 | 61, 68 | addscld 27380 |
. . . . . . 7
โข ((๐ โง (๐ โ ๐
โง ๐ โ ๐)) โ ((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) โ No
) |
70 | 59, 67 | mulscld 27504 |
. . . . . . 7
โข ((๐ โง (๐ โ ๐
โง ๐ โ ๐)) โ (๐ ยทs ๐ ) โ No
) |
71 | 69, 70 | subscld 27449 |
. . . . . 6
โข ((๐ โง (๐ โ ๐
โง ๐ โ ๐)) โ (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ )) โ No
) |
72 | | eleq1 2820 |
. . . . . 6
โข (๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ )) โ (๐ โ No
โ (((๐
ยทs ๐ต)
+s (๐ด
ยทs ๐ ))
-s (๐
ยทs ๐ ))
โ No )) |
73 | 71, 72 | syl5ibrcom 246 |
. . . . 5
โข ((๐ โง (๐ โ ๐
โง ๐ โ ๐)) โ (๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ )) โ ๐ โ No
)) |
74 | 73 | rexlimdvva 3210 |
. . . 4
โข (๐ โ (โ๐ โ ๐
โ๐ โ ๐ ๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ )) โ ๐ โ No
)) |
75 | 74 | abssdv 4061 |
. . 3
โข (๐ โ {๐ โฃ โ๐ โ ๐
โ๐ โ ๐ ๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ ))} โ No
) |
76 | 54, 75 | unssd 4182 |
. 2
โข (๐ โ ({๐ โฃ โ๐ โ ๐ฟ โ๐ โ ๐ ๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โช {๐ โฃ โ๐ โ ๐
โ๐ โ ๐ ๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ ))}) โ No
) |
77 | 40, 35 | mulscld 27504 |
. . 3
โข (๐ โ (๐ด ยทs ๐ต) โ No
) |
78 | 77 | snssd 4805 |
. 2
โข (๐ โ {(๐ด ยทs ๐ต)} โ No
) |
79 | | elun 4144 |
. . . . . . 7
โข (๐ฅ โ ({๐ โฃ โ๐ โ ๐ฟ โ๐ โ ๐ ๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โช {๐ โฃ โ๐ โ ๐
โ๐ โ ๐ ๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ ))}) โ (๐ฅ โ {๐ โฃ โ๐ โ ๐ฟ โ๐ โ ๐ ๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โจ ๐ฅ โ {๐ โฃ โ๐ โ ๐
โ๐ โ ๐ ๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ ))})) |
80 | | vex 3477 |
. . . . . . . . 9
โข ๐ฅ โ V |
81 | | eqeq1 2735 |
. . . . . . . . . 10
โข (๐ = ๐ฅ โ (๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) โ ๐ฅ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)))) |
82 | 81 | 2rexbidv 3218 |
. . . . . . . . 9
โข (๐ = ๐ฅ โ (โ๐ โ ๐ฟ โ๐ โ ๐ ๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) โ โ๐ โ ๐ฟ โ๐ โ ๐ ๐ฅ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)))) |
83 | 80, 82 | elab 3664 |
. . . . . . . 8
โข (๐ฅ โ {๐ โฃ โ๐ โ ๐ฟ โ๐ โ ๐ ๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โ โ๐ โ ๐ฟ โ๐ โ ๐ ๐ฅ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))) |
84 | | eqeq1 2735 |
. . . . . . . . . 10
โข (๐ = ๐ฅ โ (๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ )) โ ๐ฅ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ )))) |
85 | 84 | 2rexbidv 3218 |
. . . . . . . . 9
โข (๐ = ๐ฅ โ (โ๐ โ ๐
โ๐ โ ๐ ๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ )) โ โ๐ โ ๐
โ๐ โ ๐ ๐ฅ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ )))) |
86 | 80, 85 | elab 3664 |
. . . . . . . 8
โข (๐ฅ โ {๐ โฃ โ๐ โ ๐
โ๐ โ ๐ ๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ ))} โ โ๐ โ ๐
โ๐ โ ๐ ๐ฅ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ ))) |
87 | 83, 86 | orbi12i 913 |
. . . . . . 7
โข ((๐ฅ โ {๐ โฃ โ๐ โ ๐ฟ โ๐ โ ๐ ๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โจ ๐ฅ โ {๐ โฃ โ๐ โ ๐
โ๐ โ ๐ ๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ ))}) โ (โ๐ โ ๐ฟ โ๐ โ ๐ ๐ฅ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) โจ โ๐ โ ๐
โ๐ โ ๐ ๐ฅ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ )))) |
88 | 79, 87 | bitri 274 |
. . . . . 6
โข (๐ฅ โ ({๐ โฃ โ๐ โ ๐ฟ โ๐ โ ๐ ๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โช {๐ โฃ โ๐ โ ๐
โ๐ โ ๐ ๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ ))}) โ (โ๐ โ ๐ฟ โ๐ โ ๐ ๐ฅ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) โจ โ๐ โ ๐
โ๐ โ ๐ ๐ฅ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ )))) |
89 | 37, 47, 49 | addsubsd 27463 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ ๐ฟ โง ๐ โ ๐)) โ (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) = (((๐ ยทs ๐ต) -s (๐ ยทs ๐)) +s (๐ด ยทs ๐))) |
90 | | scutcut 27228 |
. . . . . . . . . . . . . . . 16
โข (๐ฟ <<s ๐
โ ((๐ฟ |s ๐
) โ No
โง ๐ฟ <<s {(๐ฟ |s ๐
)} โง {(๐ฟ |s ๐
)} <<s ๐
)) |
91 | 3, 90 | syl 17 |
. . . . . . . . . . . . . . 15
โข (๐ โ ((๐ฟ |s ๐
) โ No
โง ๐ฟ <<s {(๐ฟ |s ๐
)} โง {(๐ฟ |s ๐
)} <<s ๐
)) |
92 | 91 | simp2d 1143 |
. . . . . . . . . . . . . 14
โข (๐ โ ๐ฟ <<s {(๐ฟ |s ๐
)}) |
93 | 92 | adantr 481 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ โ ๐ฟ โง ๐ โ ๐)) โ ๐ฟ <<s {(๐ฟ |s ๐
)}) |
94 | | ovex 7426 |
. . . . . . . . . . . . . . . 16
โข (๐ฟ |s ๐
) โ V |
95 | 94 | snid 4658 |
. . . . . . . . . . . . . . 15
โข (๐ฟ |s ๐
) โ {(๐ฟ |s ๐
)} |
96 | 38, 95 | eqeltrdi 2840 |
. . . . . . . . . . . . . 14
โข (๐ โ ๐ด โ {(๐ฟ |s ๐
)}) |
97 | 96 | adantr 481 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ โ ๐ฟ โง ๐ โ ๐)) โ ๐ด โ {(๐ฟ |s ๐
)}) |
98 | 93, 31, 97 | ssltsepcd 27221 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ โ ๐ฟ โง ๐ โ ๐)) โ ๐ <s ๐ด) |
99 | | scutcut 27228 |
. . . . . . . . . . . . . . . 16
โข (๐ <<s ๐ โ ((๐ |s ๐) โ No
โง ๐ <<s {(๐ |s ๐)} โง {(๐ |s ๐)} <<s ๐)) |
100 | 6, 99 | syl 17 |
. . . . . . . . . . . . . . 15
โข (๐ โ ((๐ |s ๐) โ No
โง ๐ <<s {(๐ |s ๐)} โง {(๐ |s ๐)} <<s ๐)) |
101 | 100 | simp2d 1143 |
. . . . . . . . . . . . . 14
โข (๐ โ ๐ <<s {(๐ |s ๐)}) |
102 | 101 | adantr 481 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ โ ๐ฟ โง ๐ โ ๐)) โ ๐ <<s {(๐ |s ๐)}) |
103 | | ovex 7426 |
. . . . . . . . . . . . . . . 16
โข (๐ |s ๐) โ V |
104 | 103 | snid 4658 |
. . . . . . . . . . . . . . 15
โข (๐ |s ๐) โ {(๐ |s ๐)} |
105 | 33, 104 | eqeltrdi 2840 |
. . . . . . . . . . . . . 14
โข (๐ โ ๐ต โ {(๐ |s ๐)}) |
106 | 105 | adantr 481 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ โ ๐ฟ โง ๐ โ ๐)) โ ๐ต โ {(๐ |s ๐)}) |
107 | 102, 45, 106 | ssltsepcd 27221 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ โ ๐ฟ โง ๐ โ ๐)) โ ๐ <s ๐ต) |
108 | 32, 41, 46, 36, 98, 107 | sltmuld 27506 |
. . . . . . . . . . 11
โข ((๐ โง (๐ โ ๐ฟ โง ๐ โ ๐)) โ ((๐ ยทs ๐ต) -s (๐ ยทs ๐)) <s ((๐ด ยทs ๐ต) -s (๐ด ยทs ๐))) |
109 | 37, 49 | subscld 27449 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ โ ๐ฟ โง ๐ โ ๐)) โ ((๐ ยทs ๐ต) -s (๐ ยทs ๐)) โ No
) |
110 | 77 | adantr 481 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ โ ๐ฟ โง ๐ โ ๐)) โ (๐ด ยทs ๐ต) โ No
) |
111 | 109, 47, 110 | sltaddsubd 27472 |
. . . . . . . . . . 11
โข ((๐ โง (๐ โ ๐ฟ โง ๐ โ ๐)) โ ((((๐ ยทs ๐ต) -s (๐ ยทs ๐)) +s (๐ด ยทs ๐)) <s (๐ด ยทs ๐ต) โ ((๐ ยทs ๐ต) -s (๐ ยทs ๐)) <s ((๐ด ยทs ๐ต) -s (๐ด ยทs ๐)))) |
112 | 108, 111 | mpbird 256 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ ๐ฟ โง ๐ โ ๐)) โ (((๐ ยทs ๐ต) -s (๐ ยทs ๐)) +s (๐ด ยทs ๐)) <s (๐ด ยทs ๐ต)) |
113 | 89, 112 | eqbrtrd 5163 |
. . . . . . . . 9
โข ((๐ โง (๐ โ ๐ฟ โง ๐ โ ๐)) โ (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) <s (๐ด ยทs ๐ต)) |
114 | | breq1 5144 |
. . . . . . . . 9
โข (๐ฅ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) โ (๐ฅ <s (๐ด ยทs ๐ต) โ (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) <s (๐ด ยทs ๐ต))) |
115 | 113, 114 | syl5ibrcom 246 |
. . . . . . . 8
โข ((๐ โง (๐ โ ๐ฟ โง ๐ โ ๐)) โ (๐ฅ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) โ ๐ฅ <s (๐ด ยทs ๐ต))) |
116 | 115 | rexlimdvva 3210 |
. . . . . . 7
โข (๐ โ (โ๐ โ ๐ฟ โ๐ โ ๐ ๐ฅ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) โ ๐ฅ <s (๐ด ยทs ๐ต))) |
117 | 61, 68, 70 | addsubsd 27463 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ ๐
โง ๐ โ ๐)) โ (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ )) = (((๐ ยทs ๐ต) -s (๐ ยทs ๐ )) +s (๐ด ยทs ๐ ))) |
118 | 3 | adantr 481 |
. . . . . . . . . . . . . . 15
โข ((๐ โง (๐ โ ๐
โง ๐ โ ๐)) โ ๐ฟ <<s ๐
) |
119 | 118, 90 | syl 17 |
. . . . . . . . . . . . . 14
โข ((๐ โง (๐ โ ๐
โง ๐ โ ๐)) โ ((๐ฟ |s ๐
) โ No
โง ๐ฟ <<s {(๐ฟ |s ๐
)} โง {(๐ฟ |s ๐
)} <<s ๐
)) |
120 | 119 | simp3d 1144 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ โ ๐
โง ๐ โ ๐)) โ {(๐ฟ |s ๐
)} <<s ๐
) |
121 | 38 | adantr 481 |
. . . . . . . . . . . . . 14
โข ((๐ โง (๐ โ ๐
โง ๐ โ ๐)) โ ๐ด = (๐ฟ |s ๐
)) |
122 | 121, 95 | eqeltrdi 2840 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ โ ๐
โง ๐ โ ๐)) โ ๐ด โ {(๐ฟ |s ๐
)}) |
123 | 120, 122,
58 | ssltsepcd 27221 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ โ ๐
โง ๐ โ ๐)) โ ๐ด <s ๐) |
124 | 6 | adantr 481 |
. . . . . . . . . . . . . . 15
โข ((๐ โง (๐ โ ๐
โง ๐ โ ๐)) โ ๐ <<s ๐) |
125 | 124, 99 | syl 17 |
. . . . . . . . . . . . . 14
โข ((๐ โง (๐ โ ๐
โง ๐ โ ๐)) โ ((๐ |s ๐) โ No
โง ๐ <<s {(๐ |s ๐)} โง {(๐ |s ๐)} <<s ๐)) |
126 | 125 | simp3d 1144 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ โ ๐
โง ๐ โ ๐)) โ {(๐ |s ๐)} <<s ๐) |
127 | 33 | adantr 481 |
. . . . . . . . . . . . . 14
โข ((๐ โง (๐ โ ๐
โง ๐ โ ๐)) โ ๐ต = (๐ |s ๐)) |
128 | 127, 104 | eqeltrdi 2840 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ โ ๐
โง ๐ โ ๐)) โ ๐ต โ {(๐ |s ๐)}) |
129 | 126, 128,
66 | ssltsepcd 27221 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ โ ๐
โง ๐ โ ๐)) โ ๐ต <s ๐ ) |
130 | 62, 59, 60, 67, 123, 129 | sltmuld 27506 |
. . . . . . . . . . 11
โข ((๐ โง (๐ โ ๐
โง ๐ โ ๐)) โ ((๐ด ยทs ๐ ) -s (๐ด ยทs ๐ต)) <s ((๐ ยทs ๐ ) -s (๐ ยทs ๐ต))) |
131 | 61, 70 | subscld 27449 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ โ ๐
โง ๐ โ ๐)) โ ((๐ ยทs ๐ต) -s (๐ ยทs ๐ )) โ No
) |
132 | 77 | adantr 481 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ โ ๐
โง ๐ โ ๐)) โ (๐ด ยทs ๐ต) โ No
) |
133 | 131, 68, 132 | sltaddsubd 27472 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ โ ๐
โง ๐ โ ๐)) โ ((((๐ ยทs ๐ต) -s (๐ ยทs ๐ )) +s (๐ด ยทs ๐ )) <s (๐ด ยทs ๐ต) โ ((๐ ยทs ๐ต) -s (๐ ยทs ๐ )) <s ((๐ด ยทs ๐ต) -s (๐ด ยทs ๐ )))) |
134 | 61, 70, 132, 68 | sltsubsub2bd 27465 |
. . . . . . . . . . . 12
โข ((๐ โง (๐ โ ๐
โง ๐ โ ๐)) โ (((๐ ยทs ๐ต) -s (๐ ยทs ๐ )) <s ((๐ด ยทs ๐ต) -s (๐ด ยทs ๐ )) โ ((๐ด ยทs ๐ ) -s (๐ด ยทs ๐ต)) <s ((๐ ยทs ๐ ) -s (๐ ยทs ๐ต)))) |
135 | 133, 134 | bitrd 278 |
. . . . . . . . . . 11
โข ((๐ โง (๐ โ ๐
โง ๐ โ ๐)) โ ((((๐ ยทs ๐ต) -s (๐ ยทs ๐ )) +s (๐ด ยทs ๐ )) <s (๐ด ยทs ๐ต) โ ((๐ด ยทs ๐ ) -s (๐ด ยทs ๐ต)) <s ((๐ ยทs ๐ ) -s (๐ ยทs ๐ต)))) |
136 | 130, 135 | mpbird 256 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ ๐
โง ๐ โ ๐)) โ (((๐ ยทs ๐ต) -s (๐ ยทs ๐ )) +s (๐ด ยทs ๐ )) <s (๐ด ยทs ๐ต)) |
137 | 117, 136 | eqbrtrd 5163 |
. . . . . . . . 9
โข ((๐ โง (๐ โ ๐
โง ๐ โ ๐)) โ (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ )) <s (๐ด ยทs ๐ต)) |
138 | | breq1 5144 |
. . . . . . . . 9
โข (๐ฅ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ )) โ (๐ฅ <s (๐ด ยทs ๐ต) โ (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ )) <s (๐ด ยทs ๐ต))) |
139 | 137, 138 | syl5ibrcom 246 |
. . . . . . . 8
โข ((๐ โง (๐ โ ๐
โง ๐ โ ๐)) โ (๐ฅ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ )) โ ๐ฅ <s (๐ด ยทs ๐ต))) |
140 | 139 | rexlimdvva 3210 |
. . . . . . 7
โข (๐ โ (โ๐ โ ๐
โ๐ โ ๐ ๐ฅ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ )) โ ๐ฅ <s (๐ด ยทs ๐ต))) |
141 | 116, 140 | jaod 857 |
. . . . . 6
โข (๐ โ ((โ๐ โ ๐ฟ โ๐ โ ๐ ๐ฅ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐)) โจ โ๐ โ ๐
โ๐ โ ๐ ๐ฅ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ ))) โ ๐ฅ <s (๐ด ยทs ๐ต))) |
142 | 88, 141 | biimtrid 241 |
. . . . 5
โข (๐ โ (๐ฅ โ ({๐ โฃ โ๐ โ ๐ฟ โ๐ โ ๐ ๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โช {๐ โฃ โ๐ โ ๐
โ๐ โ ๐ ๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ ))}) โ ๐ฅ <s (๐ด ยทs ๐ต))) |
143 | 142 | imp 407 |
. . . 4
โข ((๐ โง ๐ฅ โ ({๐ โฃ โ๐ โ ๐ฟ โ๐ โ ๐ ๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โช {๐ โฃ โ๐ โ ๐
โ๐ โ ๐ ๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ ))})) โ ๐ฅ <s (๐ด ยทs ๐ต)) |
144 | | velsn 4638 |
. . . . 5
โข (๐ฆ โ {(๐ด ยทs ๐ต)} โ ๐ฆ = (๐ด ยทs ๐ต)) |
145 | | breq2 5145 |
. . . . 5
โข (๐ฆ = (๐ด ยทs ๐ต) โ (๐ฅ <s ๐ฆ โ ๐ฅ <s (๐ด ยทs ๐ต))) |
146 | 144, 145 | sylbi 216 |
. . . 4
โข (๐ฆ โ {(๐ด ยทs ๐ต)} โ (๐ฅ <s ๐ฆ โ ๐ฅ <s (๐ด ยทs ๐ต))) |
147 | 143, 146 | syl5ibrcom 246 |
. . 3
โข ((๐ โง ๐ฅ โ ({๐ โฃ โ๐ โ ๐ฟ โ๐ โ ๐ ๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โช {๐ โฃ โ๐ โ ๐
โ๐ โ ๐ ๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ ))})) โ (๐ฆ โ {(๐ด ยทs ๐ต)} โ ๐ฅ <s ๐ฆ)) |
148 | 147 | 3impia 1117 |
. 2
โข ((๐ โง ๐ฅ โ ({๐ โฃ โ๐ โ ๐ฟ โ๐ โ ๐ ๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โช {๐ โฃ โ๐ โ ๐
โ๐ โ ๐ ๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ ))}) โง ๐ฆ โ {(๐ด ยทs ๐ต)}) โ ๐ฅ <s ๐ฆ) |
149 | 25, 27, 76, 78, 148 | ssltd 27219 |
1
โข (๐ โ ({๐ โฃ โ๐ โ ๐ฟ โ๐ โ ๐ ๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐)) -s (๐ ยทs ๐))} โช {๐ โฃ โ๐ โ ๐
โ๐ โ ๐ ๐ = (((๐ ยทs ๐ต) +s (๐ด ยทs ๐ )) -s (๐ ยทs ๐ ))}) <<s {(๐ด ยทs ๐ต)}) |