MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ssltmul1 Structured version   Visualization version   GIF version

Theorem ssltmul1 27514
Description: One surreal set less-than relationship for cuts of ๐ด and ๐ต. (Contributed by Scott Fenton, 7-Mar-2025.)
Hypotheses
Ref Expression
ssltmul1.1 (๐œ‘ โ†’ ๐ฟ <<s ๐‘…)
ssltmul1.2 (๐œ‘ โ†’ ๐‘€ <<s ๐‘†)
ssltmul1.3 (๐œ‘ โ†’ ๐ด = (๐ฟ |s ๐‘…))
ssltmul1.4 (๐œ‘ โ†’ ๐ต = (๐‘€ |s ๐‘†))
Assertion
Ref Expression
ssltmul1 (๐œ‘ โ†’ ({๐‘Ž โˆฃ โˆƒ๐‘ โˆˆ ๐ฟ โˆƒ๐‘ž โˆˆ ๐‘€ ๐‘Ž = (((๐‘ ยทs ๐ต) +s (๐ด ยทs ๐‘ž)) -s (๐‘ ยทs ๐‘ž))} โˆช {๐‘ โˆฃ โˆƒ๐‘Ÿ โˆˆ ๐‘… โˆƒ๐‘  โˆˆ ๐‘† ๐‘ = (((๐‘Ÿ ยทs ๐ต) +s (๐ด ยทs ๐‘ )) -s (๐‘Ÿ ยทs ๐‘ ))}) <<s {(๐ด ยทs ๐ต)})
Distinct variable groups:   ๐ด,๐‘Ž   ๐ด,๐‘   ๐ด,๐‘,๐‘ž   ๐ด,๐‘Ÿ,๐‘    ๐ต,๐‘Ž   ๐ต,๐‘   ๐ต,๐‘,๐‘ž   ๐ต,๐‘Ÿ,๐‘    ๐ฟ,๐‘Ž,๐‘,๐‘ž   ๐‘€,๐‘Ž,๐‘,๐‘ž   ๐‘…,๐‘,๐‘Ÿ,๐‘    ๐‘†,๐‘,๐‘Ÿ,๐‘    ๐œ‘,๐‘,๐‘Ž,๐‘ž   ๐œ‘,๐‘,๐‘Ÿ,๐‘ 
Allowed substitution hints:   ๐‘…(๐‘ž,๐‘,๐‘Ž)   ๐‘†(๐‘ž,๐‘,๐‘Ž)   ๐ฟ(๐‘ ,๐‘Ÿ,๐‘)   ๐‘€(๐‘ ,๐‘Ÿ,๐‘)

Proof of Theorem ssltmul1
Dummy variables ๐‘ฅ ๐‘ฆ are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2731 . . . . 5 (๐‘ โˆˆ ๐ฟ, ๐‘ž โˆˆ ๐‘€ โ†ฆ (((๐‘ ยทs ๐ต) +s (๐ด ยทs ๐‘ž)) -s (๐‘ ยทs ๐‘ž))) = (๐‘ โˆˆ ๐ฟ, ๐‘ž โˆˆ ๐‘€ โ†ฆ (((๐‘ ยทs ๐ต) +s (๐ด ยทs ๐‘ž)) -s (๐‘ ยทs ๐‘ž)))
21rnmpo 7525 . . . 4 ran (๐‘ โˆˆ ๐ฟ, ๐‘ž โˆˆ ๐‘€ โ†ฆ (((๐‘ ยทs ๐ต) +s (๐ด ยทs ๐‘ž)) -s (๐‘ ยทs ๐‘ž))) = {๐‘Ž โˆฃ โˆƒ๐‘ โˆˆ ๐ฟ โˆƒ๐‘ž โˆˆ ๐‘€ ๐‘Ž = (((๐‘ ยทs ๐ต) +s (๐ด ยทs ๐‘ž)) -s (๐‘ ยทs ๐‘ž))}
3 ssltmul1.1 . . . . . . 7 (๐œ‘ โ†’ ๐ฟ <<s ๐‘…)
4 ssltex1 27214 . . . . . . 7 (๐ฟ <<s ๐‘… โ†’ ๐ฟ โˆˆ V)
53, 4syl 17 . . . . . 6 (๐œ‘ โ†’ ๐ฟ โˆˆ V)
6 ssltmul1.2 . . . . . . 7 (๐œ‘ โ†’ ๐‘€ <<s ๐‘†)
7 ssltex1 27214 . . . . . . 7 (๐‘€ <<s ๐‘† โ†’ ๐‘€ โˆˆ V)
86, 7syl 17 . . . . . 6 (๐œ‘ โ†’ ๐‘€ โˆˆ V)
91mpoexg 8045 . . . . . 6 ((๐ฟ โˆˆ V โˆง ๐‘€ โˆˆ V) โ†’ (๐‘ โˆˆ ๐ฟ, ๐‘ž โˆˆ ๐‘€ โ†ฆ (((๐‘ ยทs ๐ต) +s (๐ด ยทs ๐‘ž)) -s (๐‘ ยทs ๐‘ž))) โˆˆ V)
105, 8, 9syl2anc 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)
1210, 11syl 17 . . . 4 (๐œ‘ โ†’ ran (๐‘ โˆˆ ๐ฟ, ๐‘ž โˆˆ ๐‘€ โ†ฆ (((๐‘ ยทs ๐ต) +s (๐ด ยทs ๐‘ž)) -s (๐‘ ยทs ๐‘ž))) โˆˆ V)
132, 12eqeltrrid 2837 . . 3 (๐œ‘ โ†’ {๐‘Ž โˆฃ โˆƒ๐‘ โˆˆ ๐ฟ โˆƒ๐‘ž โˆˆ ๐‘€ ๐‘Ž = (((๐‘ ยทs ๐ต) +s (๐ด ยทs ๐‘ž)) -s (๐‘ ยทs ๐‘ž))} โˆˆ V)
14 eqid 2731 . . . . 5 (๐‘Ÿ โˆˆ ๐‘…, ๐‘  โˆˆ ๐‘† โ†ฆ (((๐‘Ÿ ยทs ๐ต) +s (๐ด ยทs ๐‘ )) -s (๐‘Ÿ ยทs ๐‘ ))) = (๐‘Ÿ โˆˆ ๐‘…, ๐‘  โˆˆ ๐‘† โ†ฆ (((๐‘Ÿ ยทs ๐ต) +s (๐ด ยทs ๐‘ )) -s (๐‘Ÿ ยทs ๐‘ )))
1514rnmpo 7525 . . . 4 ran (๐‘Ÿ โˆˆ ๐‘…, ๐‘  โˆˆ ๐‘† โ†ฆ (((๐‘Ÿ ยทs ๐ต) +s (๐ด ยทs ๐‘ )) -s (๐‘Ÿ ยทs ๐‘ ))) = {๐‘ โˆฃ โˆƒ๐‘Ÿ โˆˆ ๐‘… โˆƒ๐‘  โˆˆ ๐‘† ๐‘ = (((๐‘Ÿ ยทs ๐ต) +s (๐ด ยทs ๐‘ )) -s (๐‘Ÿ ยทs ๐‘ ))}
16 ssltex2 27215 . . . . . . 7 (๐ฟ <<s ๐‘… โ†’ ๐‘… โˆˆ V)
173, 16syl 17 . . . . . 6 (๐œ‘ โ†’ ๐‘… โˆˆ V)
18 ssltex2 27215 . . . . . . 7 (๐‘€ <<s ๐‘† โ†’ ๐‘† โˆˆ V)
196, 18syl 17 . . . . . 6 (๐œ‘ โ†’ ๐‘† โˆˆ V)
2014mpoexg 8045 . . . . . 6 ((๐‘… โˆˆ V โˆง ๐‘† โˆˆ V) โ†’ (๐‘Ÿ โˆˆ ๐‘…, ๐‘  โˆˆ ๐‘† โ†ฆ (((๐‘Ÿ ยทs ๐ต) +s (๐ด ยทs ๐‘ )) -s (๐‘Ÿ ยทs ๐‘ ))) โˆˆ V)
2117, 19, 20syl2anc 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)
2321, 22syl 17 . . . 4 (๐œ‘ โ†’ ran (๐‘Ÿ โˆˆ ๐‘…, ๐‘  โˆˆ ๐‘† โ†ฆ (((๐‘Ÿ ยทs ๐ต) +s (๐ด ยทs ๐‘ )) -s (๐‘Ÿ ยทs ๐‘ ))) โˆˆ V)
2415, 23eqeltrrid 2837 . . 3 (๐œ‘ โ†’ {๐‘ โˆฃ โˆƒ๐‘Ÿ โˆˆ ๐‘… โˆƒ๐‘  โˆˆ ๐‘† ๐‘ = (((๐‘Ÿ ยทs ๐ต) +s (๐ด ยทs ๐‘ )) -s (๐‘Ÿ ยทs ๐‘ ))} โˆˆ V)
2513, 24unexd 7724 . 2 (๐œ‘ โ†’ ({๐‘Ž โˆฃ โˆƒ๐‘ โˆˆ ๐ฟ โˆƒ๐‘ž โˆˆ ๐‘€ ๐‘Ž = (((๐‘ ยทs ๐ต) +s (๐ด ยทs ๐‘ž)) -s (๐‘ ยทs ๐‘ž))} โˆช {๐‘ โˆฃ โˆƒ๐‘Ÿ โˆˆ ๐‘… โˆƒ๐‘  โˆˆ ๐‘† ๐‘ = (((๐‘Ÿ ยทs ๐ต) +s (๐ด ยทs ๐‘ )) -s (๐‘Ÿ ยทs ๐‘ ))}) โˆˆ V)
26 snex 5424 . . 3 {(๐ด ยทs ๐ต)} โˆˆ V
2726a1i 11 . 2 (๐œ‘ โ†’ {(๐ด ยทs ๐ต)} โˆˆ V)
28 ssltss1 27216 . . . . . . . . . . . 12 (๐ฟ <<s ๐‘… โ†’ ๐ฟ โŠ† No )
293, 28syl 17 . . . . . . . . . . 11 (๐œ‘ โ†’ ๐ฟ โŠ† No )
3029adantr 481 . . . . . . . . . 10 ((๐œ‘ โˆง (๐‘ โˆˆ ๐ฟ โˆง ๐‘ž โˆˆ ๐‘€)) โ†’ ๐ฟ โŠ† No )
31 simprl 769 . . . . . . . . . 10 ((๐œ‘ โˆง (๐‘ โˆˆ ๐ฟ โˆง ๐‘ž โˆˆ ๐‘€)) โ†’ ๐‘ โˆˆ ๐ฟ)
3230, 31sseldd 3979 . . . . . . . . 9 ((๐œ‘ โˆง (๐‘ โˆˆ ๐ฟ โˆง ๐‘ž โˆˆ ๐‘€)) โ†’ ๐‘ โˆˆ No )
33 ssltmul1.4 . . . . . . . . . . 11 (๐œ‘ โ†’ ๐ต = (๐‘€ |s ๐‘†))
346scutcld 27230 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐‘€ |s ๐‘†) โˆˆ No )
3533, 34eqeltrd 2832 . . . . . . . . . 10 (๐œ‘ โ†’ ๐ต โˆˆ No )
3635adantr 481 . . . . . . . . 9 ((๐œ‘ โˆง (๐‘ โˆˆ ๐ฟ โˆง ๐‘ž โˆˆ ๐‘€)) โ†’ ๐ต โˆˆ No )
3732, 36mulscld 27504 . . . . . . . 8 ((๐œ‘ โˆง (๐‘ โˆˆ ๐ฟ โˆง ๐‘ž โˆˆ ๐‘€)) โ†’ (๐‘ ยทs ๐ต) โˆˆ No )
38 ssltmul1.3 . . . . . . . . . . 11 (๐œ‘ โ†’ ๐ด = (๐ฟ |s ๐‘…))
393scutcld 27230 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐ฟ |s ๐‘…) โˆˆ No )
4038, 39eqeltrd 2832 . . . . . . . . . 10 (๐œ‘ โ†’ ๐ด โˆˆ No )
4140adantr 481 . . . . . . . . 9 ((๐œ‘ โˆง (๐‘ โˆˆ ๐ฟ โˆง ๐‘ž โˆˆ ๐‘€)) โ†’ ๐ด โˆˆ No )
42 ssltss1 27216 . . . . . . . . . . . 12 (๐‘€ <<s ๐‘† โ†’ ๐‘€ โŠ† No )
436, 42syl 17 . . . . . . . . . . 11 (๐œ‘ โ†’ ๐‘€ โŠ† No )
4443adantr 481 . . . . . . . . . 10 ((๐œ‘ โˆง (๐‘ โˆˆ ๐ฟ โˆง ๐‘ž โˆˆ ๐‘€)) โ†’ ๐‘€ โŠ† No )
45 simprr 771 . . . . . . . . . 10 ((๐œ‘ โˆง (๐‘ โˆˆ ๐ฟ โˆง ๐‘ž โˆˆ ๐‘€)) โ†’ ๐‘ž โˆˆ ๐‘€)
4644, 45sseldd 3979 . . . . . . . . 9 ((๐œ‘ โˆง (๐‘ โˆˆ ๐ฟ โˆง ๐‘ž โˆˆ ๐‘€)) โ†’ ๐‘ž โˆˆ No )
4741, 46mulscld 27504 . . . . . . . 8 ((๐œ‘ โˆง (๐‘ โˆˆ ๐ฟ โˆง ๐‘ž โˆˆ ๐‘€)) โ†’ (๐ด ยทs ๐‘ž) โˆˆ No )
4837, 47addscld 27380 . . . . . . 7 ((๐œ‘ โˆง (๐‘ โˆˆ ๐ฟ โˆง ๐‘ž โˆˆ ๐‘€)) โ†’ ((๐‘ ยทs ๐ต) +s (๐ด ยทs ๐‘ž)) โˆˆ No )
4932, 46mulscld 27504 . . . . . . 7 ((๐œ‘ โˆง (๐‘ โˆˆ ๐ฟ โˆง ๐‘ž โˆˆ ๐‘€)) โ†’ (๐‘ ยทs ๐‘ž) โˆˆ No )
5048, 49subscld 27449 . . . . . 6 ((๐œ‘ โˆง (๐‘ โˆˆ ๐ฟ โˆง ๐‘ž โˆˆ ๐‘€)) โ†’ (((๐‘ ยทs ๐ต) +s (๐ด ยทs ๐‘ž)) -s (๐‘ ยทs ๐‘ž)) โˆˆ No )
51 eleq1 2820 . . . . . 6 (๐‘Ž = (((๐‘ ยทs ๐ต) +s (๐ด ยทs ๐‘ž)) -s (๐‘ ยทs ๐‘ž)) โ†’ (๐‘Ž โˆˆ No โ†” (((๐‘ ยทs ๐ต) +s (๐ด ยทs ๐‘ž)) -s (๐‘ ยทs ๐‘ž)) โˆˆ No ))
5250, 51syl5ibrcom 246 . . . . 5 ((๐œ‘ โˆง (๐‘ โˆˆ ๐ฟ โˆง ๐‘ž โˆˆ ๐‘€)) โ†’ (๐‘Ž = (((๐‘ ยทs ๐ต) +s (๐ด ยทs ๐‘ž)) -s (๐‘ ยทs ๐‘ž)) โ†’ ๐‘Ž โˆˆ No ))
5352rexlimdvva 3210 . . . 4 (๐œ‘ โ†’ (โˆƒ๐‘ โˆˆ ๐ฟ โˆƒ๐‘ž โˆˆ ๐‘€ ๐‘Ž = (((๐‘ ยทs ๐ต) +s (๐ด ยทs ๐‘ž)) -s (๐‘ ยทs ๐‘ž)) โ†’ ๐‘Ž โˆˆ No ))
5453abssdv 4061 . . 3 (๐œ‘ โ†’ {๐‘Ž โˆฃ โˆƒ๐‘ โˆˆ ๐ฟ โˆƒ๐‘ž โˆˆ ๐‘€ ๐‘Ž = (((๐‘ ยทs ๐ต) +s (๐ด ยทs ๐‘ž)) -s (๐‘ ยทs ๐‘ž))} โŠ† No )
55 ssltss2 27217 . . . . . . . . . . . 12 (๐ฟ <<s ๐‘… โ†’ ๐‘… โŠ† No )
563, 55syl 17 . . . . . . . . . . 11 (๐œ‘ โ†’ ๐‘… โŠ† No )
5756adantr 481 . . . . . . . . . 10 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ ๐‘… โˆง ๐‘  โˆˆ ๐‘†)) โ†’ ๐‘… โŠ† No )
58 simprl 769 . . . . . . . . . 10 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ ๐‘… โˆง ๐‘  โˆˆ ๐‘†)) โ†’ ๐‘Ÿ โˆˆ ๐‘…)
5957, 58sseldd 3979 . . . . . . . . 9 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ ๐‘… โˆง ๐‘  โˆˆ ๐‘†)) โ†’ ๐‘Ÿ โˆˆ No )
6035adantr 481 . . . . . . . . 9 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ ๐‘… โˆง ๐‘  โˆˆ ๐‘†)) โ†’ ๐ต โˆˆ No )
6159, 60mulscld 27504 . . . . . . . 8 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ ๐‘… โˆง ๐‘  โˆˆ ๐‘†)) โ†’ (๐‘Ÿ ยทs ๐ต) โˆˆ No )
6240adantr 481 . . . . . . . . 9 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ ๐‘… โˆง ๐‘  โˆˆ ๐‘†)) โ†’ ๐ด โˆˆ No )
63 ssltss2 27217 . . . . . . . . . . . 12 (๐‘€ <<s ๐‘† โ†’ ๐‘† โŠ† No )
646, 63syl 17 . . . . . . . . . . 11 (๐œ‘ โ†’ ๐‘† โŠ† No )
6564adantr 481 . . . . . . . . . 10 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ ๐‘… โˆง ๐‘  โˆˆ ๐‘†)) โ†’ ๐‘† โŠ† No )
66 simprr 771 . . . . . . . . . 10 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ ๐‘… โˆง ๐‘  โˆˆ ๐‘†)) โ†’ ๐‘  โˆˆ ๐‘†)
6765, 66sseldd 3979 . . . . . . . . 9 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ ๐‘… โˆง ๐‘  โˆˆ ๐‘†)) โ†’ ๐‘  โˆˆ No )
6862, 67mulscld 27504 . . . . . . . 8 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ ๐‘… โˆง ๐‘  โˆˆ ๐‘†)) โ†’ (๐ด ยทs ๐‘ ) โˆˆ No )
6961, 68addscld 27380 . . . . . . 7 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ ๐‘… โˆง ๐‘  โˆˆ ๐‘†)) โ†’ ((๐‘Ÿ ยทs ๐ต) +s (๐ด ยทs ๐‘ )) โˆˆ No )
7059, 67mulscld 27504 . . . . . . 7 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ ๐‘… โˆง ๐‘  โˆˆ ๐‘†)) โ†’ (๐‘Ÿ ยทs ๐‘ ) โˆˆ No )
7169, 70subscld 27449 . . . . . 6 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ ๐‘… โˆง ๐‘  โˆˆ ๐‘†)) โ†’ (((๐‘Ÿ ยทs ๐ต) +s (๐ด ยทs ๐‘ )) -s (๐‘Ÿ ยทs ๐‘ )) โˆˆ No )
72 eleq1 2820 . . . . . 6 (๐‘ = (((๐‘Ÿ ยทs ๐ต) +s (๐ด ยทs ๐‘ )) -s (๐‘Ÿ ยทs ๐‘ )) โ†’ (๐‘ โˆˆ No โ†” (((๐‘Ÿ ยทs ๐ต) +s (๐ด ยทs ๐‘ )) -s (๐‘Ÿ ยทs ๐‘ )) โˆˆ No ))
7371, 72syl5ibrcom 246 . . . . 5 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ ๐‘… โˆง ๐‘  โˆˆ ๐‘†)) โ†’ (๐‘ = (((๐‘Ÿ ยทs ๐ต) +s (๐ด ยทs ๐‘ )) -s (๐‘Ÿ ยทs ๐‘ )) โ†’ ๐‘ โˆˆ No ))
7473rexlimdvva 3210 . . . 4 (๐œ‘ โ†’ (โˆƒ๐‘Ÿ โˆˆ ๐‘… โˆƒ๐‘  โˆˆ ๐‘† ๐‘ = (((๐‘Ÿ ยทs ๐ต) +s (๐ด ยทs ๐‘ )) -s (๐‘Ÿ ยทs ๐‘ )) โ†’ ๐‘ โˆˆ No ))
7574abssdv 4061 . . 3 (๐œ‘ โ†’ {๐‘ โˆฃ โˆƒ๐‘Ÿ โˆˆ ๐‘… โˆƒ๐‘  โˆˆ ๐‘† ๐‘ = (((๐‘Ÿ ยทs ๐ต) +s (๐ด ยทs ๐‘ )) -s (๐‘Ÿ ยทs ๐‘ ))} โŠ† No )
7654, 75unssd 4182 . 2 (๐œ‘ โ†’ ({๐‘Ž โˆฃ โˆƒ๐‘ โˆˆ ๐ฟ โˆƒ๐‘ž โˆˆ ๐‘€ ๐‘Ž = (((๐‘ ยทs ๐ต) +s (๐ด ยทs ๐‘ž)) -s (๐‘ ยทs ๐‘ž))} โˆช {๐‘ โˆฃ โˆƒ๐‘Ÿ โˆˆ ๐‘… โˆƒ๐‘  โˆˆ ๐‘† ๐‘ = (((๐‘Ÿ ยทs ๐ต) +s (๐ด ยทs ๐‘ )) -s (๐‘Ÿ ยทs ๐‘ ))}) โŠ† No )
7740, 35mulscld 27504 . . 3 (๐œ‘ โ†’ (๐ด ยทs ๐ต) โˆˆ No )
7877snssd 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 ๐‘ž))))
82812rexbidv 3218 . . . . . . . . 9 (๐‘Ž = ๐‘ฅ โ†’ (โˆƒ๐‘ โˆˆ ๐ฟ โˆƒ๐‘ž โˆˆ ๐‘€ ๐‘Ž = (((๐‘ ยทs ๐ต) +s (๐ด ยทs ๐‘ž)) -s (๐‘ ยทs ๐‘ž)) โ†” โˆƒ๐‘ โˆˆ ๐ฟ โˆƒ๐‘ž โˆˆ ๐‘€ ๐‘ฅ = (((๐‘ ยทs ๐ต) +s (๐ด ยทs ๐‘ž)) -s (๐‘ ยทs ๐‘ž))))
8380, 82elab 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 ๐‘ ))))
85842rexbidv 3218 . . . . . . . . 9 (๐‘ = ๐‘ฅ โ†’ (โˆƒ๐‘Ÿ โˆˆ ๐‘… โˆƒ๐‘  โˆˆ ๐‘† ๐‘ = (((๐‘Ÿ ยทs ๐ต) +s (๐ด ยทs ๐‘ )) -s (๐‘Ÿ ยทs ๐‘ )) โ†” โˆƒ๐‘Ÿ โˆˆ ๐‘… โˆƒ๐‘  โˆˆ ๐‘† ๐‘ฅ = (((๐‘Ÿ ยทs ๐ต) +s (๐ด ยทs ๐‘ )) -s (๐‘Ÿ ยทs ๐‘ ))))
8680, 85elab 3664 . . . . . . . 8 (๐‘ฅ โˆˆ {๐‘ โˆฃ โˆƒ๐‘Ÿ โˆˆ ๐‘… โˆƒ๐‘  โˆˆ ๐‘† ๐‘ = (((๐‘Ÿ ยทs ๐ต) +s (๐ด ยทs ๐‘ )) -s (๐‘Ÿ ยทs ๐‘ ))} โ†” โˆƒ๐‘Ÿ โˆˆ ๐‘… โˆƒ๐‘  โˆˆ ๐‘† ๐‘ฅ = (((๐‘Ÿ ยทs ๐ต) +s (๐ด ยทs ๐‘ )) -s (๐‘Ÿ ยทs ๐‘ )))
8783, 86orbi12i 913 . . . . . . 7 ((๐‘ฅ โˆˆ {๐‘Ž โˆฃ โˆƒ๐‘ โˆˆ ๐ฟ โˆƒ๐‘ž โˆˆ ๐‘€ ๐‘Ž = (((๐‘ ยทs ๐ต) +s (๐ด ยทs ๐‘ž)) -s (๐‘ ยทs ๐‘ž))} โˆจ ๐‘ฅ โˆˆ {๐‘ โˆฃ โˆƒ๐‘Ÿ โˆˆ ๐‘… โˆƒ๐‘  โˆˆ ๐‘† ๐‘ = (((๐‘Ÿ ยทs ๐ต) +s (๐ด ยทs ๐‘ )) -s (๐‘Ÿ ยทs ๐‘ ))}) โ†” (โˆƒ๐‘ โˆˆ ๐ฟ โˆƒ๐‘ž โˆˆ ๐‘€ ๐‘ฅ = (((๐‘ ยทs ๐ต) +s (๐ด ยทs ๐‘ž)) -s (๐‘ ยทs ๐‘ž)) โˆจ โˆƒ๐‘Ÿ โˆˆ ๐‘… โˆƒ๐‘  โˆˆ ๐‘† ๐‘ฅ = (((๐‘Ÿ ยทs ๐ต) +s (๐ด ยทs ๐‘ )) -s (๐‘Ÿ ยทs ๐‘ ))))
8879, 87bitri 274 . . . . . 6 (๐‘ฅ โˆˆ ({๐‘Ž โˆฃ โˆƒ๐‘ โˆˆ ๐ฟ โˆƒ๐‘ž โˆˆ ๐‘€ ๐‘Ž = (((๐‘ ยทs ๐ต) +s (๐ด ยทs ๐‘ž)) -s (๐‘ ยทs ๐‘ž))} โˆช {๐‘ โˆฃ โˆƒ๐‘Ÿ โˆˆ ๐‘… โˆƒ๐‘  โˆˆ ๐‘† ๐‘ = (((๐‘Ÿ ยทs ๐ต) +s (๐ด ยทs ๐‘ )) -s (๐‘Ÿ ยทs ๐‘ ))}) โ†” (โˆƒ๐‘ โˆˆ ๐ฟ โˆƒ๐‘ž โˆˆ ๐‘€ ๐‘ฅ = (((๐‘ ยทs ๐ต) +s (๐ด ยทs ๐‘ž)) -s (๐‘ ยทs ๐‘ž)) โˆจ โˆƒ๐‘Ÿ โˆˆ ๐‘… โˆƒ๐‘  โˆˆ ๐‘† ๐‘ฅ = (((๐‘Ÿ ยทs ๐ต) +s (๐ด ยทs ๐‘ )) -s (๐‘Ÿ ยทs ๐‘ ))))
8937, 47, 49addsubsd 27463 . . . . . . . . . 10 ((๐œ‘ โˆง (๐‘ โˆˆ ๐ฟ โˆง ๐‘ž โˆˆ ๐‘€)) โ†’ (((๐‘ ยทs ๐ต) +s (๐ด ยทs ๐‘ž)) -s (๐‘ ยทs ๐‘ž)) = (((๐‘ ยทs ๐ต) -s (๐‘ ยทs ๐‘ž)) +s (๐ด ยทs ๐‘ž)))
90 scutcut 27228 . . . . . . . . . . . . . . . 16 (๐ฟ <<s ๐‘… โ†’ ((๐ฟ |s ๐‘…) โˆˆ No โˆง ๐ฟ <<s {(๐ฟ |s ๐‘…)} โˆง {(๐ฟ |s ๐‘…)} <<s ๐‘…))
913, 90syl 17 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ((๐ฟ |s ๐‘…) โˆˆ No โˆง ๐ฟ <<s {(๐ฟ |s ๐‘…)} โˆง {(๐ฟ |s ๐‘…)} <<s ๐‘…))
9291simp2d 1143 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ๐ฟ <<s {(๐ฟ |s ๐‘…)})
9392adantr 481 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (๐‘ โˆˆ ๐ฟ โˆง ๐‘ž โˆˆ ๐‘€)) โ†’ ๐ฟ <<s {(๐ฟ |s ๐‘…)})
94 ovex 7426 . . . . . . . . . . . . . . . 16 (๐ฟ |s ๐‘…) โˆˆ V
9594snid 4658 . . . . . . . . . . . . . . 15 (๐ฟ |s ๐‘…) โˆˆ {(๐ฟ |s ๐‘…)}
9638, 95eqeltrdi 2840 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ๐ด โˆˆ {(๐ฟ |s ๐‘…)})
9796adantr 481 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (๐‘ โˆˆ ๐ฟ โˆง ๐‘ž โˆˆ ๐‘€)) โ†’ ๐ด โˆˆ {(๐ฟ |s ๐‘…)})
9893, 31, 97ssltsepcd 27221 . . . . . . . . . . . 12 ((๐œ‘ โˆง (๐‘ โˆˆ ๐ฟ โˆง ๐‘ž โˆˆ ๐‘€)) โ†’ ๐‘ <s ๐ด)
99 scutcut 27228 . . . . . . . . . . . . . . . 16 (๐‘€ <<s ๐‘† โ†’ ((๐‘€ |s ๐‘†) โˆˆ No โˆง ๐‘€ <<s {(๐‘€ |s ๐‘†)} โˆง {(๐‘€ |s ๐‘†)} <<s ๐‘†))
1006, 99syl 17 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ((๐‘€ |s ๐‘†) โˆˆ No โˆง ๐‘€ <<s {(๐‘€ |s ๐‘†)} โˆง {(๐‘€ |s ๐‘†)} <<s ๐‘†))
101100simp2d 1143 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ๐‘€ <<s {(๐‘€ |s ๐‘†)})
102101adantr 481 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (๐‘ โˆˆ ๐ฟ โˆง ๐‘ž โˆˆ ๐‘€)) โ†’ ๐‘€ <<s {(๐‘€ |s ๐‘†)})
103 ovex 7426 . . . . . . . . . . . . . . . 16 (๐‘€ |s ๐‘†) โˆˆ V
104103snid 4658 . . . . . . . . . . . . . . 15 (๐‘€ |s ๐‘†) โˆˆ {(๐‘€ |s ๐‘†)}
10533, 104eqeltrdi 2840 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ๐ต โˆˆ {(๐‘€ |s ๐‘†)})
106105adantr 481 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (๐‘ โˆˆ ๐ฟ โˆง ๐‘ž โˆˆ ๐‘€)) โ†’ ๐ต โˆˆ {(๐‘€ |s ๐‘†)})
107102, 45, 106ssltsepcd 27221 . . . . . . . . . . . 12 ((๐œ‘ โˆง (๐‘ โˆˆ ๐ฟ โˆง ๐‘ž โˆˆ ๐‘€)) โ†’ ๐‘ž <s ๐ต)
10832, 41, 46, 36, 98, 107sltmuld 27506 . . . . . . . . . . 11 ((๐œ‘ โˆง (๐‘ โˆˆ ๐ฟ โˆง ๐‘ž โˆˆ ๐‘€)) โ†’ ((๐‘ ยทs ๐ต) -s (๐‘ ยทs ๐‘ž)) <s ((๐ด ยทs ๐ต) -s (๐ด ยทs ๐‘ž)))
10937, 49subscld 27449 . . . . . . . . . . . 12 ((๐œ‘ โˆง (๐‘ โˆˆ ๐ฟ โˆง ๐‘ž โˆˆ ๐‘€)) โ†’ ((๐‘ ยทs ๐ต) -s (๐‘ ยทs ๐‘ž)) โˆˆ No )
11077adantr 481 . . . . . . . . . . . 12 ((๐œ‘ โˆง (๐‘ โˆˆ ๐ฟ โˆง ๐‘ž โˆˆ ๐‘€)) โ†’ (๐ด ยทs ๐ต) โˆˆ No )
111109, 47, 110sltaddsubd 27472 . . . . . . . . . . 11 ((๐œ‘ โˆง (๐‘ โˆˆ ๐ฟ โˆง ๐‘ž โˆˆ ๐‘€)) โ†’ ((((๐‘ ยทs ๐ต) -s (๐‘ ยทs ๐‘ž)) +s (๐ด ยทs ๐‘ž)) <s (๐ด ยทs ๐ต) โ†” ((๐‘ ยทs ๐ต) -s (๐‘ ยทs ๐‘ž)) <s ((๐ด ยทs ๐ต) -s (๐ด ยทs ๐‘ž))))
112108, 111mpbird 256 . . . . . . . . . 10 ((๐œ‘ โˆง (๐‘ โˆˆ ๐ฟ โˆง ๐‘ž โˆˆ ๐‘€)) โ†’ (((๐‘ ยทs ๐ต) -s (๐‘ ยทs ๐‘ž)) +s (๐ด ยทs ๐‘ž)) <s (๐ด ยทs ๐ต))
11389, 112eqbrtrd 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 ๐ต)))
115113, 114syl5ibrcom 246 . . . . . . . 8 ((๐œ‘ โˆง (๐‘ โˆˆ ๐ฟ โˆง ๐‘ž โˆˆ ๐‘€)) โ†’ (๐‘ฅ = (((๐‘ ยทs ๐ต) +s (๐ด ยทs ๐‘ž)) -s (๐‘ ยทs ๐‘ž)) โ†’ ๐‘ฅ <s (๐ด ยทs ๐ต)))
116115rexlimdvva 3210 . . . . . . 7 (๐œ‘ โ†’ (โˆƒ๐‘ โˆˆ ๐ฟ โˆƒ๐‘ž โˆˆ ๐‘€ ๐‘ฅ = (((๐‘ ยทs ๐ต) +s (๐ด ยทs ๐‘ž)) -s (๐‘ ยทs ๐‘ž)) โ†’ ๐‘ฅ <s (๐ด ยทs ๐ต)))
11761, 68, 70addsubsd 27463 . . . . . . . . . 10 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ ๐‘… โˆง ๐‘  โˆˆ ๐‘†)) โ†’ (((๐‘Ÿ ยทs ๐ต) +s (๐ด ยทs ๐‘ )) -s (๐‘Ÿ ยทs ๐‘ )) = (((๐‘Ÿ ยทs ๐ต) -s (๐‘Ÿ ยทs ๐‘ )) +s (๐ด ยทs ๐‘ )))
1183adantr 481 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ ๐‘… โˆง ๐‘  โˆˆ ๐‘†)) โ†’ ๐ฟ <<s ๐‘…)
119118, 90syl 17 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ ๐‘… โˆง ๐‘  โˆˆ ๐‘†)) โ†’ ((๐ฟ |s ๐‘…) โˆˆ No โˆง ๐ฟ <<s {(๐ฟ |s ๐‘…)} โˆง {(๐ฟ |s ๐‘…)} <<s ๐‘…))
120119simp3d 1144 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ ๐‘… โˆง ๐‘  โˆˆ ๐‘†)) โ†’ {(๐ฟ |s ๐‘…)} <<s ๐‘…)
12138adantr 481 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ ๐‘… โˆง ๐‘  โˆˆ ๐‘†)) โ†’ ๐ด = (๐ฟ |s ๐‘…))
122121, 95eqeltrdi 2840 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ ๐‘… โˆง ๐‘  โˆˆ ๐‘†)) โ†’ ๐ด โˆˆ {(๐ฟ |s ๐‘…)})
123120, 122, 58ssltsepcd 27221 . . . . . . . . . . . 12 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ ๐‘… โˆง ๐‘  โˆˆ ๐‘†)) โ†’ ๐ด <s ๐‘Ÿ)
1246adantr 481 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ ๐‘… โˆง ๐‘  โˆˆ ๐‘†)) โ†’ ๐‘€ <<s ๐‘†)
125124, 99syl 17 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ ๐‘… โˆง ๐‘  โˆˆ ๐‘†)) โ†’ ((๐‘€ |s ๐‘†) โˆˆ No โˆง ๐‘€ <<s {(๐‘€ |s ๐‘†)} โˆง {(๐‘€ |s ๐‘†)} <<s ๐‘†))
126125simp3d 1144 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ ๐‘… โˆง ๐‘  โˆˆ ๐‘†)) โ†’ {(๐‘€ |s ๐‘†)} <<s ๐‘†)
12733adantr 481 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ ๐‘… โˆง ๐‘  โˆˆ ๐‘†)) โ†’ ๐ต = (๐‘€ |s ๐‘†))
128127, 104eqeltrdi 2840 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ ๐‘… โˆง ๐‘  โˆˆ ๐‘†)) โ†’ ๐ต โˆˆ {(๐‘€ |s ๐‘†)})
129126, 128, 66ssltsepcd 27221 . . . . . . . . . . . 12 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ ๐‘… โˆง ๐‘  โˆˆ ๐‘†)) โ†’ ๐ต <s ๐‘ )
13062, 59, 60, 67, 123, 129sltmuld 27506 . . . . . . . . . . 11 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ ๐‘… โˆง ๐‘  โˆˆ ๐‘†)) โ†’ ((๐ด ยทs ๐‘ ) -s (๐ด ยทs ๐ต)) <s ((๐‘Ÿ ยทs ๐‘ ) -s (๐‘Ÿ ยทs ๐ต)))
13161, 70subscld 27449 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ ๐‘… โˆง ๐‘  โˆˆ ๐‘†)) โ†’ ((๐‘Ÿ ยทs ๐ต) -s (๐‘Ÿ ยทs ๐‘ )) โˆˆ No )
13277adantr 481 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ ๐‘… โˆง ๐‘  โˆˆ ๐‘†)) โ†’ (๐ด ยทs ๐ต) โˆˆ No )
133131, 68, 132sltaddsubd 27472 . . . . . . . . . . . 12 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ ๐‘… โˆง ๐‘  โˆˆ ๐‘†)) โ†’ ((((๐‘Ÿ ยทs ๐ต) -s (๐‘Ÿ ยทs ๐‘ )) +s (๐ด ยทs ๐‘ )) <s (๐ด ยทs ๐ต) โ†” ((๐‘Ÿ ยทs ๐ต) -s (๐‘Ÿ ยทs ๐‘ )) <s ((๐ด ยทs ๐ต) -s (๐ด ยทs ๐‘ ))))
13461, 70, 132, 68sltsubsub2bd 27465 . . . . . . . . . . . 12 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ ๐‘… โˆง ๐‘  โˆˆ ๐‘†)) โ†’ (((๐‘Ÿ ยทs ๐ต) -s (๐‘Ÿ ยทs ๐‘ )) <s ((๐ด ยทs ๐ต) -s (๐ด ยทs ๐‘ )) โ†” ((๐ด ยทs ๐‘ ) -s (๐ด ยทs ๐ต)) <s ((๐‘Ÿ ยทs ๐‘ ) -s (๐‘Ÿ ยทs ๐ต))))
135133, 134bitrd 278 . . . . . . . . . . 11 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ ๐‘… โˆง ๐‘  โˆˆ ๐‘†)) โ†’ ((((๐‘Ÿ ยทs ๐ต) -s (๐‘Ÿ ยทs ๐‘ )) +s (๐ด ยทs ๐‘ )) <s (๐ด ยทs ๐ต) โ†” ((๐ด ยทs ๐‘ ) -s (๐ด ยทs ๐ต)) <s ((๐‘Ÿ ยทs ๐‘ ) -s (๐‘Ÿ ยทs ๐ต))))
136130, 135mpbird 256 . . . . . . . . . 10 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ ๐‘… โˆง ๐‘  โˆˆ ๐‘†)) โ†’ (((๐‘Ÿ ยทs ๐ต) -s (๐‘Ÿ ยทs ๐‘ )) +s (๐ด ยทs ๐‘ )) <s (๐ด ยทs ๐ต))
137117, 136eqbrtrd 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 ๐ต)))
139137, 138syl5ibrcom 246 . . . . . . . 8 ((๐œ‘ โˆง (๐‘Ÿ โˆˆ ๐‘… โˆง ๐‘  โˆˆ ๐‘†)) โ†’ (๐‘ฅ = (((๐‘Ÿ ยทs ๐ต) +s (๐ด ยทs ๐‘ )) -s (๐‘Ÿ ยทs ๐‘ )) โ†’ ๐‘ฅ <s (๐ด ยทs ๐ต)))
140139rexlimdvva 3210 . . . . . . 7 (๐œ‘ โ†’ (โˆƒ๐‘Ÿ โˆˆ ๐‘… โˆƒ๐‘  โˆˆ ๐‘† ๐‘ฅ = (((๐‘Ÿ ยทs ๐ต) +s (๐ด ยทs ๐‘ )) -s (๐‘Ÿ ยทs ๐‘ )) โ†’ ๐‘ฅ <s (๐ด ยทs ๐ต)))
141116, 140jaod 857 . . . . . 6 (๐œ‘ โ†’ ((โˆƒ๐‘ โˆˆ ๐ฟ โˆƒ๐‘ž โˆˆ ๐‘€ ๐‘ฅ = (((๐‘ ยทs ๐ต) +s (๐ด ยทs ๐‘ž)) -s (๐‘ ยทs ๐‘ž)) โˆจ โˆƒ๐‘Ÿ โˆˆ ๐‘… โˆƒ๐‘  โˆˆ ๐‘† ๐‘ฅ = (((๐‘Ÿ ยทs ๐ต) +s (๐ด ยทs ๐‘ )) -s (๐‘Ÿ ยทs ๐‘ ))) โ†’ ๐‘ฅ <s (๐ด ยทs ๐ต)))
14288, 141biimtrid 241 . . . . 5 (๐œ‘ โ†’ (๐‘ฅ โˆˆ ({๐‘Ž โˆฃ โˆƒ๐‘ โˆˆ ๐ฟ โˆƒ๐‘ž โˆˆ ๐‘€ ๐‘Ž = (((๐‘ ยทs ๐ต) +s (๐ด ยทs ๐‘ž)) -s (๐‘ ยทs ๐‘ž))} โˆช {๐‘ โˆฃ โˆƒ๐‘Ÿ โˆˆ ๐‘… โˆƒ๐‘  โˆˆ ๐‘† ๐‘ = (((๐‘Ÿ ยทs ๐ต) +s (๐ด ยทs ๐‘ )) -s (๐‘Ÿ ยทs ๐‘ ))}) โ†’ ๐‘ฅ <s (๐ด ยทs ๐ต)))
143142imp 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 ๐ต)))
146144, 145sylbi 216 . . . 4 (๐‘ฆ โˆˆ {(๐ด ยทs ๐ต)} โ†’ (๐‘ฅ <s ๐‘ฆ โ†” ๐‘ฅ <s (๐ด ยทs ๐ต)))
147143, 146syl5ibrcom 246 . . 3 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ({๐‘Ž โˆฃ โˆƒ๐‘ โˆˆ ๐ฟ โˆƒ๐‘ž โˆˆ ๐‘€ ๐‘Ž = (((๐‘ ยทs ๐ต) +s (๐ด ยทs ๐‘ž)) -s (๐‘ ยทs ๐‘ž))} โˆช {๐‘ โˆฃ โˆƒ๐‘Ÿ โˆˆ ๐‘… โˆƒ๐‘  โˆˆ ๐‘† ๐‘ = (((๐‘Ÿ ยทs ๐ต) +s (๐ด ยทs ๐‘ )) -s (๐‘Ÿ ยทs ๐‘ ))})) โ†’ (๐‘ฆ โˆˆ {(๐ด ยทs ๐ต)} โ†’ ๐‘ฅ <s ๐‘ฆ))
1481473impia 1117 . 2 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ({๐‘Ž โˆฃ โˆƒ๐‘ โˆˆ ๐ฟ โˆƒ๐‘ž โˆˆ ๐‘€ ๐‘Ž = (((๐‘ ยทs ๐ต) +s (๐ด ยทs ๐‘ž)) -s (๐‘ ยทs ๐‘ž))} โˆช {๐‘ โˆฃ โˆƒ๐‘Ÿ โˆˆ ๐‘… โˆƒ๐‘  โˆˆ ๐‘† ๐‘ = (((๐‘Ÿ ยทs ๐ต) +s (๐ด ยทs ๐‘ )) -s (๐‘Ÿ ยทs ๐‘ ))}) โˆง ๐‘ฆ โˆˆ {(๐ด ยทs ๐ต)}) โ†’ ๐‘ฅ <s ๐‘ฆ)
14925, 27, 76, 78, 148ssltd 27219 1 (๐œ‘ โ†’ ({๐‘Ž โˆฃ โˆƒ๐‘ โˆˆ ๐ฟ โˆƒ๐‘ž โˆˆ ๐‘€ ๐‘Ž = (((๐‘ ยทs ๐ต) +s (๐ด ยทs ๐‘ž)) -s (๐‘ ยทs ๐‘ž))} โˆช {๐‘ โˆฃ โˆƒ๐‘Ÿ โˆˆ ๐‘… โˆƒ๐‘  โˆˆ ๐‘† ๐‘ = (((๐‘Ÿ ยทs ๐ต) +s (๐ด ยทs ๐‘ )) -s (๐‘Ÿ ยทs ๐‘ ))}) <<s {(๐ด ยทs ๐ต)})
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โ†” wb 205   โˆง wa 396   โˆจ wo 845   โˆง w3a 1087   = wceq 1541   โˆˆ wcel 2106  {cab 2708  โˆƒwrex 3069  Vcvv 3473   โˆช cun 3942   โŠ† wss 3944  {csn 4622   class class class wbr 5141  ran crn 5670  (class class class)co 7393   โˆˆ cmpo 7395   No csur 27070   <s cslt 27071   <<s csslt 27208   |s cscut 27210   +s cadds 27359   -s csubs 27411   ยทs cmuls 27476
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-rep 5278  ax-sep 5292  ax-nul 5299  ax-pow 5356  ax-pr 5420  ax-un 7708
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-rmo 3375  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3963  df-nul 4319  df-if 4523  df-pw 4598  df-sn 4623  df-pr 4625  df-tp 4627  df-op 4629  df-ot 4631  df-uni 4902  df-int 4944  df-iun 4992  df-br 5142  df-opab 5204  df-mpt 5225  df-tr 5259  df-id 5567  df-eprel 5573  df-po 5581  df-so 5582  df-fr 5624  df-se 5625  df-we 5626  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-pred 6289  df-ord 6356  df-on 6357  df-suc 6359  df-iota 6484  df-fun 6534  df-fn 6535  df-f 6536  df-f1 6537  df-fo 6538  df-f1o 6539  df-fv 6540  df-riota 7349  df-ov 7396  df-oprab 7397  df-mpo 7398  df-1st 7957  df-2nd 7958  df-frecs 8248  df-wrecs 8279  df-recs 8353  df-1o 8448  df-2o 8449  df-nadd 8648  df-no 27073  df-slt 27074  df-bday 27075  df-sle 27175  df-sslt 27209  df-scut 27211  df-0s 27251  df-made 27265  df-old 27266  df-left 27268  df-right 27269  df-norec 27338  df-norec2 27349  df-adds 27360  df-negs 27412  df-subs 27413  df-muls 27477
This theorem is referenced by:  mulsuniflem  27516
  Copyright terms: Public domain W3C validator