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

Theorem precsexlem10 28254
Description: Lemma for surreal reciprocal. Show that the union of the left sets is less than the union of the right sets. Note that this is the first theorem in the surreal numbers to require the axiom of infinity. (Contributed by Scott Fenton, 15-Mar-2025.)
Hypotheses
Ref Expression
precsexlem.1 ๐น = rec((๐‘ โˆˆ V โ†ฆ โฆ‹(1st โ€˜๐‘) / ๐‘™โฆŒโฆ‹(2nd โ€˜๐‘) / ๐‘ŸโฆŒโŸจ(๐‘™ โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ๐‘™ ๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐‘…)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐‘… โˆˆ ๐‘Ÿ ๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐ฟ)})), (๐‘Ÿ โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐ฟ โˆˆ ๐‘™ ๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐ฟ)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ๐‘Ÿ ๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐‘…)}))โŸฉ), โŸจ{ 0s }, โˆ…โŸฉ)
precsexlem.2 ๐ฟ = (1st โˆ˜ ๐น)
precsexlem.3 ๐‘… = (2nd โˆ˜ ๐น)
precsexlem.4 (๐œ‘ โ†’ ๐ด โˆˆ No )
precsexlem.5 (๐œ‘ โ†’ 0s <s ๐ด)
precsexlem.6 (๐œ‘ โ†’ โˆ€๐‘ฅ๐‘‚ โˆˆ (( L โ€˜๐ด) โˆช ( R โ€˜๐ด))( 0s <s ๐‘ฅ๐‘‚ โ†’ โˆƒ๐‘ฆ โˆˆ No (๐‘ฅ๐‘‚ ยทs ๐‘ฆ) = 1s ))
Assertion
Ref Expression
precsexlem10 (๐œ‘ โ†’ โˆช (๐ฟ โ€œ ฯ‰) <<s โˆช (๐‘… โ€œ ฯ‰))
Distinct variable groups:   ๐ด,๐‘Ž,๐‘™,๐‘,๐‘Ÿ,๐‘ฅ,๐‘ฅ๐‘‚,๐‘ฅ๐ฟ,๐‘ฅ๐‘…,๐‘ฆ,๐‘ฆ๐ฟ,๐‘ฆ๐‘…   ๐น,๐‘™,๐‘   ๐ฟ,๐‘Ž,๐‘™,๐‘ฅ๐ฟ,๐‘ฅ๐‘…,๐‘ฆ๐ฟ,๐‘ฆ๐‘…   ๐‘…,๐‘Ž,๐‘™,๐‘Ÿ,๐‘ฅ๐ฟ,๐‘ฅ๐‘…,๐‘ฆ๐ฟ,๐‘ฆ๐‘…   ๐œ‘,๐‘Ž,๐‘ฅ๐ฟ,๐‘ฅ๐‘…,๐‘ฆ๐ฟ,๐‘ฆ๐‘…   ๐ฟ,๐‘Ÿ   ๐œ‘,๐‘Ÿ
Allowed substitution hints:   ๐œ‘(๐‘ฅ,๐‘ฆ,๐‘,๐‘™,๐‘ฅ๐‘‚)   ๐‘…(๐‘ฅ,๐‘ฆ,๐‘,๐‘ฅ๐‘‚)   ๐น(๐‘ฅ,๐‘ฆ,๐‘Ÿ,๐‘Ž,๐‘ฅ๐‘‚,๐‘ฅ๐ฟ,๐‘ฅ๐‘…,๐‘ฆ๐ฟ,๐‘ฆ๐‘…)   ๐ฟ(๐‘ฅ,๐‘ฆ,๐‘,๐‘ฅ๐‘‚)

Proof of Theorem precsexlem10
Dummy variables ๐‘– ๐‘— ๐‘ ๐‘ are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fo1st 8032 . . . . . . . 8 1st :Vโ€“ontoโ†’V
2 fofun 6821 . . . . . . . 8 (1st :Vโ€“ontoโ†’V โ†’ Fun 1st )
31, 2ax-mp 5 . . . . . . 7 Fun 1st
4 rdgfun 8454 . . . . . . . 8 Fun rec((๐‘ โˆˆ V โ†ฆ โฆ‹(1st โ€˜๐‘) / ๐‘™โฆŒโฆ‹(2nd โ€˜๐‘) / ๐‘ŸโฆŒโŸจ(๐‘™ โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ๐‘™ ๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐‘…)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐‘… โˆˆ ๐‘Ÿ ๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐ฟ)})), (๐‘Ÿ โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐ฟ โˆˆ ๐‘™ ๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐ฟ)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ๐‘Ÿ ๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐‘…)}))โŸฉ), โŸจ{ 0s }, โˆ…โŸฉ)
5 precsexlem.1 . . . . . . . . 9 ๐น = rec((๐‘ โˆˆ V โ†ฆ โฆ‹(1st โ€˜๐‘) / ๐‘™โฆŒโฆ‹(2nd โ€˜๐‘) / ๐‘ŸโฆŒโŸจ(๐‘™ โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ๐‘™ ๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐‘…)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐‘… โˆˆ ๐‘Ÿ ๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐ฟ)})), (๐‘Ÿ โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐ฟ โˆˆ ๐‘™ ๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐ฟ)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ๐‘Ÿ ๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐‘…)}))โŸฉ), โŸจ{ 0s }, โˆ…โŸฉ)
65funeqi 6588 . . . . . . . 8 (Fun ๐น โ†” Fun rec((๐‘ โˆˆ V โ†ฆ โฆ‹(1st โ€˜๐‘) / ๐‘™โฆŒโฆ‹(2nd โ€˜๐‘) / ๐‘ŸโฆŒโŸจ(๐‘™ โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ๐‘™ ๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐‘…)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐‘… โˆˆ ๐‘Ÿ ๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐ฟ)})), (๐‘Ÿ โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐ฟ โˆˆ ๐‘™ ๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐ฟ)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ๐‘Ÿ ๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐‘…)}))โŸฉ), โŸจ{ 0s }, โˆ…โŸฉ))
74, 6mpbir 231 . . . . . . 7 Fun ๐น
8 funco 6607 . . . . . . 7 ((Fun 1st โˆง Fun ๐น) โ†’ Fun (1st โˆ˜ ๐น))
93, 7, 8mp2an 692 . . . . . 6 Fun (1st โˆ˜ ๐น)
10 precsexlem.2 . . . . . . 7 ๐ฟ = (1st โˆ˜ ๐น)
1110funeqi 6588 . . . . . 6 (Fun ๐ฟ โ†” Fun (1st โˆ˜ ๐น))
129, 11mpbir 231 . . . . 5 Fun ๐ฟ
13 dcomex 10484 . . . . . 6 ฯ‰ โˆˆ V
1413funimaex 6655 . . . . 5 (Fun ๐ฟ โ†’ (๐ฟ โ€œ ฯ‰) โˆˆ V)
1512, 14ax-mp 5 . . . 4 (๐ฟ โ€œ ฯ‰) โˆˆ V
1615uniex 7759 . . 3 โˆช (๐ฟ โ€œ ฯ‰) โˆˆ V
1716a1i 11 . 2 (๐œ‘ โ†’ โˆช (๐ฟ โ€œ ฯ‰) โˆˆ V)
18 fo2nd 8033 . . . . . . . 8 2nd :Vโ€“ontoโ†’V
19 fofun 6821 . . . . . . . 8 (2nd :Vโ€“ontoโ†’V โ†’ Fun 2nd )
2018, 19ax-mp 5 . . . . . . 7 Fun 2nd
21 funco 6607 . . . . . . 7 ((Fun 2nd โˆง Fun ๐น) โ†’ Fun (2nd โˆ˜ ๐น))
2220, 7, 21mp2an 692 . . . . . 6 Fun (2nd โˆ˜ ๐น)
23 precsexlem.3 . . . . . . 7 ๐‘… = (2nd โˆ˜ ๐น)
2423funeqi 6588 . . . . . 6 (Fun ๐‘… โ†” Fun (2nd โˆ˜ ๐น))
2522, 24mpbir 231 . . . . 5 Fun ๐‘…
2613funimaex 6655 . . . . 5 (Fun ๐‘… โ†’ (๐‘… โ€œ ฯ‰) โˆˆ V)
2725, 26ax-mp 5 . . . 4 (๐‘… โ€œ ฯ‰) โˆˆ V
2827uniex 7759 . . 3 โˆช (๐‘… โ€œ ฯ‰) โˆˆ V
2928a1i 11 . 2 (๐œ‘ โ†’ โˆช (๐‘… โ€œ ฯ‰) โˆˆ V)
30 funiunfv 7267 . . . 4 (Fun ๐ฟ โ†’ โˆช ๐‘– โˆˆ ฯ‰ (๐ฟโ€˜๐‘–) = โˆช (๐ฟ โ€œ ฯ‰))
3112, 30ax-mp 5 . . 3 โˆช ๐‘– โˆˆ ฯ‰ (๐ฟโ€˜๐‘–) = โˆช (๐ฟ โ€œ ฯ‰)
32 precsexlem.4 . . . . . 6 (๐œ‘ โ†’ ๐ด โˆˆ No )
33 precsexlem.5 . . . . . 6 (๐œ‘ โ†’ 0s <s ๐ด)
34 precsexlem.6 . . . . . 6 (๐œ‘ โ†’ โˆ€๐‘ฅ๐‘‚ โˆˆ (( L โ€˜๐ด) โˆช ( R โ€˜๐ด))( 0s <s ๐‘ฅ๐‘‚ โ†’ โˆƒ๐‘ฆ โˆˆ No (๐‘ฅ๐‘‚ ยทs ๐‘ฆ) = 1s ))
355, 10, 23, 32, 33, 34precsexlem8 28252 . . . . 5 ((๐œ‘ โˆง ๐‘– โˆˆ ฯ‰) โ†’ ((๐ฟโ€˜๐‘–) โІ No โˆง (๐‘…โ€˜๐‘–) โІ No ))
3635simpld 494 . . . 4 ((๐œ‘ โˆง ๐‘– โˆˆ ฯ‰) โ†’ (๐ฟโ€˜๐‘–) โІ No )
3736iunssd 5054 . . 3 (๐œ‘ โ†’ โˆช ๐‘– โˆˆ ฯ‰ (๐ฟโ€˜๐‘–) โІ No )
3831, 37eqsstrrid 4044 . 2 (๐œ‘ โ†’ โˆช (๐ฟ โ€œ ฯ‰) โІ No )
39 funiunfv 7267 . . . 4 (Fun ๐‘… โ†’ โˆช ๐‘– โˆˆ ฯ‰ (๐‘…โ€˜๐‘–) = โˆช (๐‘… โ€œ ฯ‰))
4025, 39ax-mp 5 . . 3 โˆช ๐‘– โˆˆ ฯ‰ (๐‘…โ€˜๐‘–) = โˆช (๐‘… โ€œ ฯ‰)
4135simprd 495 . . . 4 ((๐œ‘ โˆง ๐‘– โˆˆ ฯ‰) โ†’ (๐‘…โ€˜๐‘–) โІ No )
4241iunssd 5054 . . 3 (๐œ‘ โ†’ โˆช ๐‘– โˆˆ ฯ‰ (๐‘…โ€˜๐‘–) โІ No )
4340, 42eqsstrrid 4044 . 2 (๐œ‘ โ†’ โˆช (๐‘… โ€œ ฯ‰) โІ No )
4431eleq2i 2830 . . . . . . 7 (๐‘ โˆˆ โˆช ๐‘– โˆˆ ฯ‰ (๐ฟโ€˜๐‘–) โ†” ๐‘ โˆˆ โˆช (๐ฟ โ€œ ฯ‰))
45 eliun 4999 . . . . . . 7 (๐‘ โˆˆ โˆช ๐‘– โˆˆ ฯ‰ (๐ฟโ€˜๐‘–) โ†” โˆƒ๐‘– โˆˆ ฯ‰ ๐‘ โˆˆ (๐ฟโ€˜๐‘–))
4644, 45bitr3i 277 . . . . . 6 (๐‘ โˆˆ โˆช (๐ฟ โ€œ ฯ‰) โ†” โˆƒ๐‘– โˆˆ ฯ‰ ๐‘ โˆˆ (๐ฟโ€˜๐‘–))
47 funiunfv 7267 . . . . . . . . 9 (Fun ๐‘… โ†’ โˆช ๐‘— โˆˆ ฯ‰ (๐‘…โ€˜๐‘—) = โˆช (๐‘… โ€œ ฯ‰))
4825, 47ax-mp 5 . . . . . . . 8 โˆช ๐‘— โˆˆ ฯ‰ (๐‘…โ€˜๐‘—) = โˆช (๐‘… โ€œ ฯ‰)
4948eleq2i 2830 . . . . . . 7 (๐‘ โˆˆ โˆช ๐‘— โˆˆ ฯ‰ (๐‘…โ€˜๐‘—) โ†” ๐‘ โˆˆ โˆช (๐‘… โ€œ ฯ‰))
50 eliun 4999 . . . . . . 7 (๐‘ โˆˆ โˆช ๐‘— โˆˆ ฯ‰ (๐‘…โ€˜๐‘—) โ†” โˆƒ๐‘— โˆˆ ฯ‰ ๐‘ โˆˆ (๐‘…โ€˜๐‘—))
5149, 50bitr3i 277 . . . . . 6 (๐‘ โˆˆ โˆช (๐‘… โ€œ ฯ‰) โ†” โˆƒ๐‘— โˆˆ ฯ‰ ๐‘ โˆˆ (๐‘…โ€˜๐‘—))
5246, 51anbi12i 628 . . . . 5 ((๐‘ โˆˆ โˆช (๐ฟ โ€œ ฯ‰) โˆง ๐‘ โˆˆ โˆช (๐‘… โ€œ ฯ‰)) โ†” (โˆƒ๐‘– โˆˆ ฯ‰ ๐‘ โˆˆ (๐ฟโ€˜๐‘–) โˆง โˆƒ๐‘— โˆˆ ฯ‰ ๐‘ โˆˆ (๐‘…โ€˜๐‘—)))
53 reeanv 3226 . . . . 5 (โˆƒ๐‘– โˆˆ ฯ‰ โˆƒ๐‘— โˆˆ ฯ‰ (๐‘ โˆˆ (๐ฟโ€˜๐‘–) โˆง ๐‘ โˆˆ (๐‘…โ€˜๐‘—)) โ†” (โˆƒ๐‘– โˆˆ ฯ‰ ๐‘ โˆˆ (๐ฟโ€˜๐‘–) โˆง โˆƒ๐‘— โˆˆ ฯ‰ ๐‘ โˆˆ (๐‘…โ€˜๐‘—)))
5452, 53bitr4i 278 . . . 4 ((๐‘ โˆˆ โˆช (๐ฟ โ€œ ฯ‰) โˆง ๐‘ โˆˆ โˆช (๐‘… โ€œ ฯ‰)) โ†” โˆƒ๐‘– โˆˆ ฯ‰ โˆƒ๐‘— โˆˆ ฯ‰ (๐‘ โˆˆ (๐ฟโ€˜๐‘–) โˆง ๐‘ โˆˆ (๐‘…โ€˜๐‘—)))
55 omun 7909 . . . . . . . . 9 ((๐‘– โˆˆ ฯ‰ โˆง ๐‘— โˆˆ ฯ‰) โ†’ (๐‘– โˆช ๐‘—) โˆˆ ฯ‰)
56 ssun1 4187 . . . . . . . . . 10 ๐‘– โІ (๐‘– โˆช ๐‘—)
575, 10, 23precsexlem6 28250 . . . . . . . . . 10 ((๐‘– โˆˆ ฯ‰ โˆง (๐‘– โˆช ๐‘—) โˆˆ ฯ‰ โˆง ๐‘– โІ (๐‘– โˆช ๐‘—)) โ†’ (๐ฟโ€˜๐‘–) โІ (๐ฟโ€˜(๐‘– โˆช ๐‘—)))
5856, 57mp3an3 1449 . . . . . . . . 9 ((๐‘– โˆˆ ฯ‰ โˆง (๐‘– โˆช ๐‘—) โˆˆ ฯ‰) โ†’ (๐ฟโ€˜๐‘–) โІ (๐ฟโ€˜(๐‘– โˆช ๐‘—)))
5955, 58syldan 591 . . . . . . . 8 ((๐‘– โˆˆ ฯ‰ โˆง ๐‘— โˆˆ ฯ‰) โ†’ (๐ฟโ€˜๐‘–) โІ (๐ฟโ€˜(๐‘– โˆช ๐‘—)))
6059adantl 481 . . . . . . 7 ((๐œ‘ โˆง (๐‘– โˆˆ ฯ‰ โˆง ๐‘— โˆˆ ฯ‰)) โ†’ (๐ฟโ€˜๐‘–) โІ (๐ฟโ€˜(๐‘– โˆช ๐‘—)))
6160sseld 3993 . . . . . 6 ((๐œ‘ โˆง (๐‘– โˆˆ ฯ‰ โˆง ๐‘— โˆˆ ฯ‰)) โ†’ (๐‘ โˆˆ (๐ฟโ€˜๐‘–) โ†’ ๐‘ โˆˆ (๐ฟโ€˜(๐‘– โˆช ๐‘—))))
62 simpr 484 . . . . . . . . 9 ((๐‘– โˆˆ ฯ‰ โˆง ๐‘— โˆˆ ฯ‰) โ†’ ๐‘— โˆˆ ฯ‰)
63 ssun2 4188 . . . . . . . . . 10 ๐‘— โІ (๐‘– โˆช ๐‘—)
645, 10, 23precsexlem7 28251 . . . . . . . . . 10 ((๐‘— โˆˆ ฯ‰ โˆง (๐‘– โˆช ๐‘—) โˆˆ ฯ‰ โˆง ๐‘— โІ (๐‘– โˆช ๐‘—)) โ†’ (๐‘…โ€˜๐‘—) โІ (๐‘…โ€˜(๐‘– โˆช ๐‘—)))
6563, 64mp3an3 1449 . . . . . . . . 9 ((๐‘— โˆˆ ฯ‰ โˆง (๐‘– โˆช ๐‘—) โˆˆ ฯ‰) โ†’ (๐‘…โ€˜๐‘—) โІ (๐‘…โ€˜(๐‘– โˆช ๐‘—)))
6662, 55, 65syl2anc 584 . . . . . . . 8 ((๐‘– โˆˆ ฯ‰ โˆง ๐‘— โˆˆ ฯ‰) โ†’ (๐‘…โ€˜๐‘—) โІ (๐‘…โ€˜(๐‘– โˆช ๐‘—)))
6766sseld 3993 . . . . . . 7 ((๐‘– โˆˆ ฯ‰ โˆง ๐‘— โˆˆ ฯ‰) โ†’ (๐‘ โˆˆ (๐‘…โ€˜๐‘—) โ†’ ๐‘ โˆˆ (๐‘…โ€˜(๐‘– โˆช ๐‘—))))
6867adantl 481 . . . . . 6 ((๐œ‘ โˆง (๐‘– โˆˆ ฯ‰ โˆง ๐‘— โˆˆ ฯ‰)) โ†’ (๐‘ โˆˆ (๐‘…โ€˜๐‘—) โ†’ ๐‘ โˆˆ (๐‘…โ€˜(๐‘– โˆช ๐‘—))))
6932ad2antrr 726 . . . . . . . . . . . 12 (((๐œ‘ โˆง (๐‘– โˆช ๐‘—) โˆˆ ฯ‰) โˆง (๐‘ โˆˆ (๐ฟโ€˜(๐‘– โˆช ๐‘—)) โˆง ๐‘ โˆˆ (๐‘…โ€˜(๐‘– โˆช ๐‘—)))) โ†’ ๐ด โˆˆ No )
705, 10, 23, 32, 33, 34precsexlem8 28252 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง (๐‘– โˆช ๐‘—) โˆˆ ฯ‰) โ†’ ((๐ฟโ€˜(๐‘– โˆช ๐‘—)) โІ No โˆง (๐‘…โ€˜(๐‘– โˆช ๐‘—)) โІ No ))
7170simpld 494 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (๐‘– โˆช ๐‘—) โˆˆ ฯ‰) โ†’ (๐ฟโ€˜(๐‘– โˆช ๐‘—)) โІ No )
7271sselda 3994 . . . . . . . . . . . . 13 (((๐œ‘ โˆง (๐‘– โˆช ๐‘—) โˆˆ ฯ‰) โˆง ๐‘ โˆˆ (๐ฟโ€˜(๐‘– โˆช ๐‘—))) โ†’ ๐‘ โˆˆ No )
7372adantrr 717 . . . . . . . . . . . 12 (((๐œ‘ โˆง (๐‘– โˆช ๐‘—) โˆˆ ฯ‰) โˆง (๐‘ โˆˆ (๐ฟโ€˜(๐‘– โˆช ๐‘—)) โˆง ๐‘ โˆˆ (๐‘…โ€˜(๐‘– โˆช ๐‘—)))) โ†’ ๐‘ โˆˆ No )
7469, 73mulscld 28175 . . . . . . . . . . 11 (((๐œ‘ โˆง (๐‘– โˆช ๐‘—) โˆˆ ฯ‰) โˆง (๐‘ โˆˆ (๐ฟโ€˜(๐‘– โˆช ๐‘—)) โˆง ๐‘ โˆˆ (๐‘…โ€˜(๐‘– โˆช ๐‘—)))) โ†’ (๐ด ยทs ๐‘) โˆˆ No )
7570simprd 495 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (๐‘– โˆช ๐‘—) โˆˆ ฯ‰) โ†’ (๐‘…โ€˜(๐‘– โˆช ๐‘—)) โІ No )
7675sselda 3994 . . . . . . . . . . . . 13 (((๐œ‘ โˆง (๐‘– โˆช ๐‘—) โˆˆ ฯ‰) โˆง ๐‘ โˆˆ (๐‘…โ€˜(๐‘– โˆช ๐‘—))) โ†’ ๐‘ โˆˆ No )
7776adantrl 716 . . . . . . . . . . . 12 (((๐œ‘ โˆง (๐‘– โˆช ๐‘—) โˆˆ ฯ‰) โˆง (๐‘ โˆˆ (๐ฟโ€˜(๐‘– โˆช ๐‘—)) โˆง ๐‘ โˆˆ (๐‘…โ€˜(๐‘– โˆช ๐‘—)))) โ†’ ๐‘ โˆˆ No )
7869, 77mulscld 28175 . . . . . . . . . . 11 (((๐œ‘ โˆง (๐‘– โˆช ๐‘—) โˆˆ ฯ‰) โˆง (๐‘ โˆˆ (๐ฟโ€˜(๐‘– โˆช ๐‘—)) โˆง ๐‘ โˆˆ (๐‘…โ€˜(๐‘– โˆช ๐‘—)))) โ†’ (๐ด ยทs ๐‘) โˆˆ No )
7974, 78jca 511 . . . . . . . . . 10 (((๐œ‘ โˆง (๐‘– โˆช ๐‘—) โˆˆ ฯ‰) โˆง (๐‘ โˆˆ (๐ฟโ€˜(๐‘– โˆช ๐‘—)) โˆง ๐‘ โˆˆ (๐‘…โ€˜(๐‘– โˆช ๐‘—)))) โ†’ ((๐ด ยทs ๐‘) โˆˆ No โˆง (๐ด ยทs ๐‘) โˆˆ No ))
805, 10, 23, 32, 33, 34precsexlem9 28253 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (๐‘– โˆช ๐‘—) โˆˆ ฯ‰) โ†’ (โˆ€๐‘ โˆˆ (๐ฟโ€˜(๐‘– โˆช ๐‘—))(๐ด ยทs ๐‘) <s 1s โˆง โˆ€๐‘ โˆˆ (๐‘…โ€˜(๐‘– โˆช ๐‘—)) 1s <s (๐ด ยทs ๐‘)))
8180simpld 494 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (๐‘– โˆช ๐‘—) โˆˆ ฯ‰) โ†’ โˆ€๐‘ โˆˆ (๐ฟโ€˜(๐‘– โˆช ๐‘—))(๐ด ยทs ๐‘) <s 1s )
82 rsp 3244 . . . . . . . . . . . . 13 (โˆ€๐‘ โˆˆ (๐ฟโ€˜(๐‘– โˆช ๐‘—))(๐ด ยทs ๐‘) <s 1s โ†’ (๐‘ โˆˆ (๐ฟโ€˜(๐‘– โˆช ๐‘—)) โ†’ (๐ด ยทs ๐‘) <s 1s ))
8381, 82syl 17 . . . . . . . . . . . 12 ((๐œ‘ โˆง (๐‘– โˆช ๐‘—) โˆˆ ฯ‰) โ†’ (๐‘ โˆˆ (๐ฟโ€˜(๐‘– โˆช ๐‘—)) โ†’ (๐ด ยทs ๐‘) <s 1s ))
8480simprd 495 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (๐‘– โˆช ๐‘—) โˆˆ ฯ‰) โ†’ โˆ€๐‘ โˆˆ (๐‘…โ€˜(๐‘– โˆช ๐‘—)) 1s <s (๐ด ยทs ๐‘))
85 rsp 3244 . . . . . . . . . . . . 13 (โˆ€๐‘ โˆˆ (๐‘…โ€˜(๐‘– โˆช ๐‘—)) 1s <s (๐ด ยทs ๐‘) โ†’ (๐‘ โˆˆ (๐‘…โ€˜(๐‘– โˆช ๐‘—)) โ†’ 1s <s (๐ด ยทs ๐‘)))
8684, 85syl 17 . . . . . . . . . . . 12 ((๐œ‘ โˆง (๐‘– โˆช ๐‘—) โˆˆ ฯ‰) โ†’ (๐‘ โˆˆ (๐‘…โ€˜(๐‘– โˆช ๐‘—)) โ†’ 1s <s (๐ด ยทs ๐‘)))
8783, 86anim12d 609 . . . . . . . . . . 11 ((๐œ‘ โˆง (๐‘– โˆช ๐‘—) โˆˆ ฯ‰) โ†’ ((๐‘ โˆˆ (๐ฟโ€˜(๐‘– โˆช ๐‘—)) โˆง ๐‘ โˆˆ (๐‘…โ€˜(๐‘– โˆช ๐‘—))) โ†’ ((๐ด ยทs ๐‘) <s 1s โˆง 1s <s (๐ด ยทs ๐‘))))
8887imp 406 . . . . . . . . . 10 (((๐œ‘ โˆง (๐‘– โˆช ๐‘—) โˆˆ ฯ‰) โˆง (๐‘ โˆˆ (๐ฟโ€˜(๐‘– โˆช ๐‘—)) โˆง ๐‘ โˆˆ (๐‘…โ€˜(๐‘– โˆช ๐‘—)))) โ†’ ((๐ด ยทs ๐‘) <s 1s โˆง 1s <s (๐ด ยทs ๐‘)))
89 1sno 27886 . . . . . . . . . . 11 1s โˆˆ No
90 slttr 27806 . . . . . . . . . . 11 (((๐ด ยทs ๐‘) โˆˆ No โˆง 1s โˆˆ No โˆง (๐ด ยทs ๐‘) โˆˆ No ) โ†’ (((๐ด ยทs ๐‘) <s 1s โˆง 1s <s (๐ด ยทs ๐‘)) โ†’ (๐ด ยทs ๐‘) <s (๐ด ยทs ๐‘)))
9189, 90mp3an2 1448 . . . . . . . . . 10 (((๐ด ยทs ๐‘) โˆˆ No โˆง (๐ด ยทs ๐‘) โˆˆ No ) โ†’ (((๐ด ยทs ๐‘) <s 1s โˆง 1s <s (๐ด ยทs ๐‘)) โ†’ (๐ด ยทs ๐‘) <s (๐ด ยทs ๐‘)))
9279, 88, 91sylc 65 . . . . . . . . 9 (((๐œ‘ โˆง (๐‘– โˆช ๐‘—) โˆˆ ฯ‰) โˆง (๐‘ โˆˆ (๐ฟโ€˜(๐‘– โˆช ๐‘—)) โˆง ๐‘ โˆˆ (๐‘…โ€˜(๐‘– โˆช ๐‘—)))) โ†’ (๐ด ยทs ๐‘) <s (๐ด ยทs ๐‘))
9333ad2antrr 726 . . . . . . . . . 10 (((๐œ‘ โˆง (๐‘– โˆช ๐‘—) โˆˆ ฯ‰) โˆง (๐‘ โˆˆ (๐ฟโ€˜(๐‘– โˆช ๐‘—)) โˆง ๐‘ โˆˆ (๐‘…โ€˜(๐‘– โˆช ๐‘—)))) โ†’ 0s <s ๐ด)
9473, 77, 69, 93sltmul2d 28212 . . . . . . . . 9 (((๐œ‘ โˆง (๐‘– โˆช ๐‘—) โˆˆ ฯ‰) โˆง (๐‘ โˆˆ (๐ฟโ€˜(๐‘– โˆช ๐‘—)) โˆง ๐‘ โˆˆ (๐‘…โ€˜(๐‘– โˆช ๐‘—)))) โ†’ (๐‘ <s ๐‘ โ†” (๐ด ยทs ๐‘) <s (๐ด ยทs ๐‘)))
9592, 94mpbird 257 . . . . . . . 8 (((๐œ‘ โˆง (๐‘– โˆช ๐‘—) โˆˆ ฯ‰) โˆง (๐‘ โˆˆ (๐ฟโ€˜(๐‘– โˆช ๐‘—)) โˆง ๐‘ โˆˆ (๐‘…โ€˜(๐‘– โˆช ๐‘—)))) โ†’ ๐‘ <s ๐‘)
9695ex 412 . . . . . . 7 ((๐œ‘ โˆง (๐‘– โˆช ๐‘—) โˆˆ ฯ‰) โ†’ ((๐‘ โˆˆ (๐ฟโ€˜(๐‘– โˆช ๐‘—)) โˆง ๐‘ โˆˆ (๐‘…โ€˜(๐‘– โˆช ๐‘—))) โ†’ ๐‘ <s ๐‘))
9755, 96sylan2 593 . . . . . 6 ((๐œ‘ โˆง (๐‘– โˆˆ ฯ‰ โˆง ๐‘— โˆˆ ฯ‰)) โ†’ ((๐‘ โˆˆ (๐ฟโ€˜(๐‘– โˆช ๐‘—)) โˆง ๐‘ โˆˆ (๐‘…โ€˜(๐‘– โˆช ๐‘—))) โ†’ ๐‘ <s ๐‘))
9861, 68, 97syl2and 608 . . . . 5 ((๐œ‘ โˆง (๐‘– โˆˆ ฯ‰ โˆง ๐‘— โˆˆ ฯ‰)) โ†’ ((๐‘ โˆˆ (๐ฟโ€˜๐‘–) โˆง ๐‘ โˆˆ (๐‘…โ€˜๐‘—)) โ†’ ๐‘ <s ๐‘))
9998rexlimdvva 3210 . . . 4 (๐œ‘ โ†’ (โˆƒ๐‘– โˆˆ ฯ‰ โˆƒ๐‘— โˆˆ ฯ‰ (๐‘ โˆˆ (๐ฟโ€˜๐‘–) โˆง ๐‘ โˆˆ (๐‘…โ€˜๐‘—)) โ†’ ๐‘ <s ๐‘))
10054, 99biimtrid 242 . . 3 (๐œ‘ โ†’ ((๐‘ โˆˆ โˆช (๐ฟ โ€œ ฯ‰) โˆง ๐‘ โˆˆ โˆช (๐‘… โ€œ ฯ‰)) โ†’ ๐‘ <s ๐‘))
1011003impib 1115 . 2 ((๐œ‘ โˆง ๐‘ โˆˆ โˆช (๐ฟ โ€œ ฯ‰) โˆง ๐‘ โˆˆ โˆช (๐‘… โ€œ ฯ‰)) โ†’ ๐‘ <s ๐‘)
10217, 29, 38, 43, 101ssltd 27850 1 (๐œ‘ โ†’ โˆช (๐ฟ โ€œ ฯ‰) <<s โˆช (๐‘… โ€œ ฯ‰))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โˆง wa 395   = wceq 1536   โˆˆ wcel 2105  {cab 2711  โˆ€wral 3058  โˆƒwrex 3067  {crab 3432  Vcvv 3477  โฆ‹csb 3907   โˆช cun 3960   โІ wss 3962  โˆ…c0 4338  {csn 4630  โŸจcop 4636  โˆช cuni 4911  โˆช ciun 4995   class class class wbr 5147   โ†ฆ cmpt 5230   โ€œ cima 5691   โˆ˜ ccom 5692  Fun wfun 6556  โ€“ontoโ†’wfo 6560  โ€˜cfv 6562  (class class class)co 7430  ฯ‰com 7886  1st c1st 8010  2nd c2nd 8011  reccrdg 8447   No csur 27698   <s cslt 27699   <<s csslt 27839   0s c0s 27881   1s c1s 27882   L cleft 27898   R cright 27899   +s cadds 28006   -s csubs 28066   ยทs cmuls 28146   /su cdivs 28227
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-dc 10483
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-ral 3059  df-rex 3068  df-rmo 3377  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-tp 4635  df-op 4637  df-ot 4639  df-uni 4912  df-int 4951  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-se 5641  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-om 7887  df-1st 8012  df-2nd 8013  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-1o 8504  df-2o 8505  df-oadd 8508  df-nadd 8702  df-no 27701  df-slt 27702  df-bday 27703  df-sle 27804  df-sslt 27840  df-scut 27842  df-0s 27883  df-1s 27884  df-made 27900  df-old 27901  df-left 27903  df-right 27904  df-norec 27985  df-norec2 27996  df-adds 28007  df-negs 28067  df-subs 28068  df-muls 28147  df-divs 28228
This theorem is referenced by:  precsexlem11  28255  precsex  28256
  Copyright terms: Public domain W3C validator