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