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

Theorem axcontlem10 28826
Description: Lemma for axcont 28829. Given a handful of assumptions, derive the conclusion of the final theorem. (Contributed by Scott Fenton, 20-Jun-2013.)
Hypotheses
Ref Expression
axcontlem10.1 ๐ท = {๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆฃ (๐‘ˆ Btwn โŸจ๐‘, ๐‘โŸฉ โˆจ ๐‘ Btwn โŸจ๐‘, ๐‘ˆโŸฉ)}
axcontlem10.2 ๐น = {โŸจ๐‘ฅ, ๐‘กโŸฉ โˆฃ (๐‘ฅ โˆˆ ๐ท โˆง (๐‘ก โˆˆ (0[,)+โˆž) โˆง โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–)))))}
Assertion
Ref Expression
axcontlem10 (((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ โˆƒ๐‘ โˆˆ (๐”ผโ€˜๐‘)โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ Btwn โŸจ๐‘ฅ, ๐‘ฆโŸฉ)
Distinct variable groups:   ๐ด,๐‘,๐‘,๐‘ฅ   ๐ต,๐‘,๐‘,๐‘ฅ,๐‘ฆ   ๐ท,๐‘,๐‘ก,๐‘ฅ   ๐น,๐‘   ๐‘–,๐น,๐‘,๐‘ก,๐‘ฅ   ๐‘ฆ,๐น   ๐‘,๐‘   ๐‘–,๐‘,๐‘,๐‘ก,๐‘ฅ   ๐‘ฆ,๐‘   ๐‘ˆ,๐‘   ๐‘ˆ,๐‘–,๐‘,๐‘ก,๐‘ฅ   ๐‘ฆ,๐‘ˆ   ๐‘,๐‘   ๐‘–,๐‘,๐‘,๐‘ก,๐‘ฅ   ๐‘ฆ,๐‘
Allowed substitution hints:   ๐ด(๐‘ฆ,๐‘ก,๐‘–)   ๐ต(๐‘ก,๐‘–)   ๐ท(๐‘ฆ,๐‘–,๐‘)

Proof of Theorem axcontlem10
Dummy variables ๐‘˜ ๐‘š ๐‘› ๐‘ž ๐‘Ÿ are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 imassrn 6069 . . . . 5 (๐น โ€œ ๐ด) โІ ran ๐น
2 simpll 765 . . . . . . 7 (((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ ๐‘ โˆˆ โ„•)
3 simprl1 1215 . . . . . . 7 (((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ ๐‘ โˆˆ (๐”ผโ€˜๐‘))
4 simplr1 1212 . . . . . . . 8 (((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ ๐ด โІ (๐”ผโ€˜๐‘))
5 simprl2 1216 . . . . . . . 8 (((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ ๐‘ˆ โˆˆ ๐ด)
64, 5sseldd 3973 . . . . . . 7 (((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘))
7 simprr 771 . . . . . . 7 (((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ ๐‘ โ‰  ๐‘ˆ)
8 axcontlem10.1 . . . . . . . 8 ๐ท = {๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆฃ (๐‘ˆ Btwn โŸจ๐‘, ๐‘โŸฉ โˆจ ๐‘ Btwn โŸจ๐‘, ๐‘ˆโŸฉ)}
9 axcontlem10.2 . . . . . . . 8 ๐น = {โŸจ๐‘ฅ, ๐‘กโŸฉ โˆฃ (๐‘ฅ โˆˆ ๐ท โˆง (๐‘ก โˆˆ (0[,)+โˆž) โˆง โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–)))))}
108, 9axcontlem2 28818 . . . . . . 7 (((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โ†’ ๐น:๐ทโ€“1-1-ontoโ†’(0[,)+โˆž))
112, 3, 6, 7, 10syl31anc 1370 . . . . . 6 (((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ ๐น:๐ทโ€“1-1-ontoโ†’(0[,)+โˆž))
12 f1ofo 6840 . . . . . 6 (๐น:๐ทโ€“1-1-ontoโ†’(0[,)+โˆž) โ†’ ๐น:๐ทโ€“ontoโ†’(0[,)+โˆž))
13 forn 6808 . . . . . 6 (๐น:๐ทโ€“ontoโ†’(0[,)+โˆž) โ†’ ran ๐น = (0[,)+โˆž))
1411, 12, 133syl 18 . . . . 5 (((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ ran ๐น = (0[,)+โˆž))
151, 14sseqtrid 4025 . . . 4 (((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ (๐น โ€œ ๐ด) โІ (0[,)+โˆž))
16 rge0ssre 13463 . . . 4 (0[,)+โˆž) โІ โ„
1715, 16sstrdi 3985 . . 3 (((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ (๐น โ€œ ๐ด) โІ โ„)
18 imassrn 6069 . . . . 5 (๐น โ€œ ๐ต) โІ ran ๐น
1918, 14sseqtrid 4025 . . . 4 (((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ (๐น โ€œ ๐ต) โІ (0[,)+โˆž))
2019, 16sstrdi 3985 . . 3 (((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ (๐น โ€œ ๐ต) โІ โ„)
218, 9axcontlem9 28825 . . 3 (((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)๐‘š โ‰ค ๐‘›)
22 dedekindle 11406 . . 3 (((๐น โ€œ ๐ด) โІ โ„ โˆง (๐น โ€œ ๐ต) โІ โ„ โˆง โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)๐‘š โ‰ค ๐‘›) โ†’ โˆƒ๐‘˜ โˆˆ โ„ โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›))
2317, 20, 21, 22syl3anc 1368 . 2 (((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ โˆƒ๐‘˜ โˆˆ โ„ โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›))
24 simpr 483 . . . . . . . 8 (((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›)) โˆง ๐‘˜ โˆˆ โ„) โ†’ ๐‘˜ โˆˆ โ„)
25 simprl3 1217 . . . . . . . . . . 11 (((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ ๐ต โ‰  โˆ…)
2625ad2antrr 724 . . . . . . . . . 10 (((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›)) โˆง ๐‘˜ โˆˆ โ„) โ†’ ๐ต โ‰  โˆ…)
27 n0 4342 . . . . . . . . . 10 (๐ต โ‰  โˆ… โ†” โˆƒ๐‘ ๐‘ โˆˆ ๐ต)
2826, 27sylib 217 . . . . . . . . 9 (((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›)) โˆง ๐‘˜ โˆˆ โ„) โ†’ โˆƒ๐‘ ๐‘ โˆˆ ๐ต)
29 0red 11245 . . . . . . . . . . . 12 (((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›)) โˆง (๐‘˜ โˆˆ โ„ โˆง ๐‘ โˆˆ ๐ต)) โ†’ 0 โˆˆ โ„)
30 f1of 6833 . . . . . . . . . . . . . . . 16 (๐น:๐ทโ€“1-1-ontoโ†’(0[,)+โˆž) โ†’ ๐น:๐ทโŸถ(0[,)+โˆž))
3111, 30syl 17 . . . . . . . . . . . . . . 15 (((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ ๐น:๐ทโŸถ(0[,)+โˆž))
328axcontlem4 28820 . . . . . . . . . . . . . . . 16 (((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ ๐ด โІ ๐ท)
3332, 5sseldd 3973 . . . . . . . . . . . . . . 15 (((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ ๐‘ˆ โˆˆ ๐ท)
3431, 33ffvelcdmd 7089 . . . . . . . . . . . . . 14 (((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ (๐นโ€˜๐‘ˆ) โˆˆ (0[,)+โˆž))
3516, 34sselid 3970 . . . . . . . . . . . . 13 (((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ (๐นโ€˜๐‘ˆ) โˆˆ โ„)
3635ad2antrr 724 . . . . . . . . . . . 12 (((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›)) โˆง (๐‘˜ โˆˆ โ„ โˆง ๐‘ โˆˆ ๐ต)) โ†’ (๐นโ€˜๐‘ˆ) โˆˆ โ„)
37 simprl 769 . . . . . . . . . . . 12 (((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›)) โˆง (๐‘˜ โˆˆ โ„ โˆง ๐‘ โˆˆ ๐ต)) โ†’ ๐‘˜ โˆˆ โ„)
38 elrege0 13461 . . . . . . . . . . . . . . 15 ((๐นโ€˜๐‘ˆ) โˆˆ (0[,)+โˆž) โ†” ((๐นโ€˜๐‘ˆ) โˆˆ โ„ โˆง 0 โ‰ค (๐นโ€˜๐‘ˆ)))
3938simprbi 495 . . . . . . . . . . . . . 14 ((๐นโ€˜๐‘ˆ) โˆˆ (0[,)+โˆž) โ†’ 0 โ‰ค (๐นโ€˜๐‘ˆ))
4034, 39syl 17 . . . . . . . . . . . . 13 (((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ 0 โ‰ค (๐นโ€˜๐‘ˆ))
4140ad2antrr 724 . . . . . . . . . . . 12 (((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›)) โˆง (๐‘˜ โˆˆ โ„ โˆง ๐‘ โˆˆ ๐ต)) โ†’ 0 โ‰ค (๐นโ€˜๐‘ˆ))
42 f1of1 6832 . . . . . . . . . . . . . . . . . . . 20 (๐น:๐ทโ€“1-1-ontoโ†’(0[,)+โˆž) โ†’ ๐น:๐ทโ€“1-1โ†’(0[,)+โˆž))
4311, 42syl 17 . . . . . . . . . . . . . . . . . . 19 (((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ ๐น:๐ทโ€“1-1โ†’(0[,)+โˆž))
44 f1elima 7268 . . . . . . . . . . . . . . . . . . 19 ((๐น:๐ทโ€“1-1โ†’(0[,)+โˆž) โˆง ๐‘ˆ โˆˆ ๐ท โˆง ๐ด โІ ๐ท) โ†’ ((๐นโ€˜๐‘ˆ) โˆˆ (๐น โ€œ ๐ด) โ†” ๐‘ˆ โˆˆ ๐ด))
4543, 33, 32, 44syl3anc 1368 . . . . . . . . . . . . . . . . . 18 (((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ ((๐นโ€˜๐‘ˆ) โˆˆ (๐น โ€œ ๐ด) โ†” ๐‘ˆ โˆˆ ๐ด))
465, 45mpbird 256 . . . . . . . . . . . . . . . . 17 (((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ (๐นโ€˜๐‘ˆ) โˆˆ (๐น โ€œ ๐ด))
4746adantr 479 . . . . . . . . . . . . . . . 16 ((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง (๐‘˜ โˆˆ โ„ โˆง ๐‘ โˆˆ ๐ต)) โ†’ (๐นโ€˜๐‘ˆ) โˆˆ (๐น โ€œ ๐ด))
48 simpr 483 . . . . . . . . . . . . . . . . . 18 ((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง ๐‘ โˆˆ ๐ต) โ†’ ๐‘ โˆˆ ๐ต)
4943adantr 479 . . . . . . . . . . . . . . . . . . 19 ((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง ๐‘ โˆˆ ๐ต) โ†’ ๐น:๐ทโ€“1-1โ†’(0[,)+โˆž))
50 simpl1 1188 . . . . . . . . . . . . . . . . . . . . . 22 (((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ) โ†’ ๐‘ โˆˆ (๐”ผโ€˜๐‘))
51 simpl2 1189 . . . . . . . . . . . . . . . . . . . . . 22 (((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ) โ†’ ๐‘ˆ โˆˆ ๐ด)
52 simpr 483 . . . . . . . . . . . . . . . . . . . . . 22 (((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ) โ†’ ๐‘ โ‰  ๐‘ˆ)
5350, 51, 523jca 1125 . . . . . . . . . . . . . . . . . . . . 21 (((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ) โ†’ (๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐‘ โ‰  ๐‘ˆ))
548axcontlem3 28819 . . . . . . . . . . . . . . . . . . . . 21 (((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง (๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ ๐ต โІ ๐ท)
5553, 54sylan2 591 . . . . . . . . . . . . . . . . . . . 20 (((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ ๐ต โІ ๐ท)
5655sselda 3972 . . . . . . . . . . . . . . . . . . 19 ((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง ๐‘ โˆˆ ๐ต) โ†’ ๐‘ โˆˆ ๐ท)
5755adantr 479 . . . . . . . . . . . . . . . . . . 19 ((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง ๐‘ โˆˆ ๐ต) โ†’ ๐ต โІ ๐ท)
58 f1elima 7268 . . . . . . . . . . . . . . . . . . 19 ((๐น:๐ทโ€“1-1โ†’(0[,)+โˆž) โˆง ๐‘ โˆˆ ๐ท โˆง ๐ต โІ ๐ท) โ†’ ((๐นโ€˜๐‘) โˆˆ (๐น โ€œ ๐ต) โ†” ๐‘ โˆˆ ๐ต))
5949, 56, 57, 58syl3anc 1368 . . . . . . . . . . . . . . . . . 18 ((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง ๐‘ โˆˆ ๐ต) โ†’ ((๐นโ€˜๐‘) โˆˆ (๐น โ€œ ๐ต) โ†” ๐‘ โˆˆ ๐ต))
6048, 59mpbird 256 . . . . . . . . . . . . . . . . 17 ((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง ๐‘ โˆˆ ๐ต) โ†’ (๐นโ€˜๐‘) โˆˆ (๐น โ€œ ๐ต))
6160adantrl 714 . . . . . . . . . . . . . . . 16 ((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง (๐‘˜ โˆˆ โ„ โˆง ๐‘ โˆˆ ๐ต)) โ†’ (๐นโ€˜๐‘) โˆˆ (๐น โ€œ ๐ต))
6247, 61jca 510 . . . . . . . . . . . . . . 15 ((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง (๐‘˜ โˆˆ โ„ โˆง ๐‘ โˆˆ ๐ต)) โ†’ ((๐นโ€˜๐‘ˆ) โˆˆ (๐น โ€œ ๐ด) โˆง (๐นโ€˜๐‘) โˆˆ (๐น โ€œ ๐ต)))
63 breq1 5146 . . . . . . . . . . . . . . . . 17 (๐‘š = (๐นโ€˜๐‘ˆ) โ†’ (๐‘š โ‰ค ๐‘˜ โ†” (๐นโ€˜๐‘ˆ) โ‰ค ๐‘˜))
6463anbi1d 629 . . . . . . . . . . . . . . . 16 (๐‘š = (๐นโ€˜๐‘ˆ) โ†’ ((๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›) โ†” ((๐นโ€˜๐‘ˆ) โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›)))
65 breq2 5147 . . . . . . . . . . . . . . . . 17 (๐‘› = (๐นโ€˜๐‘) โ†’ (๐‘˜ โ‰ค ๐‘› โ†” ๐‘˜ โ‰ค (๐นโ€˜๐‘)))
6665anbi2d 628 . . . . . . . . . . . . . . . 16 (๐‘› = (๐นโ€˜๐‘) โ†’ (((๐นโ€˜๐‘ˆ) โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›) โ†” ((๐นโ€˜๐‘ˆ) โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค (๐นโ€˜๐‘))))
6764, 66rspc2va 3614 . . . . . . . . . . . . . . 15 ((((๐นโ€˜๐‘ˆ) โˆˆ (๐น โ€œ ๐ด) โˆง (๐นโ€˜๐‘) โˆˆ (๐น โ€œ ๐ต)) โˆง โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›)) โ†’ ((๐นโ€˜๐‘ˆ) โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค (๐นโ€˜๐‘)))
6862, 67sylan 578 . . . . . . . . . . . . . 14 (((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง (๐‘˜ โˆˆ โ„ โˆง ๐‘ โˆˆ ๐ต)) โˆง โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›)) โ†’ ((๐นโ€˜๐‘ˆ) โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค (๐นโ€˜๐‘)))
6968an32s 650 . . . . . . . . . . . . 13 (((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›)) โˆง (๐‘˜ โˆˆ โ„ โˆง ๐‘ โˆˆ ๐ต)) โ†’ ((๐นโ€˜๐‘ˆ) โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค (๐นโ€˜๐‘)))
7069simpld 493 . . . . . . . . . . . 12 (((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›)) โˆง (๐‘˜ โˆˆ โ„ โˆง ๐‘ โˆˆ ๐ต)) โ†’ (๐นโ€˜๐‘ˆ) โ‰ค ๐‘˜)
7129, 36, 37, 41, 70letrd 11399 . . . . . . . . . . 11 (((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›)) โˆง (๐‘˜ โˆˆ โ„ โˆง ๐‘ โˆˆ ๐ต)) โ†’ 0 โ‰ค ๐‘˜)
7271expr 455 . . . . . . . . . 10 (((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›)) โˆง ๐‘˜ โˆˆ โ„) โ†’ (๐‘ โˆˆ ๐ต โ†’ 0 โ‰ค ๐‘˜))
7372exlimdv 1928 . . . . . . . . 9 (((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›)) โˆง ๐‘˜ โˆˆ โ„) โ†’ (โˆƒ๐‘ ๐‘ โˆˆ ๐ต โ†’ 0 โ‰ค ๐‘˜))
7428, 73mpd 15 . . . . . . . 8 (((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›)) โˆง ๐‘˜ โˆˆ โ„) โ†’ 0 โ‰ค ๐‘˜)
75 elrege0 13461 . . . . . . . 8 (๐‘˜ โˆˆ (0[,)+โˆž) โ†” (๐‘˜ โˆˆ โ„ โˆง 0 โ‰ค ๐‘˜))
7624, 74, 75sylanbrc 581 . . . . . . 7 (((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›)) โˆง ๐‘˜ โˆˆ โ„) โ†’ ๐‘˜ โˆˆ (0[,)+โˆž))
7776ex 411 . . . . . 6 ((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›)) โ†’ (๐‘˜ โˆˆ โ„ โ†’ ๐‘˜ โˆˆ (0[,)+โˆž)))
788ssrab3 4072 . . . . . . . . 9 ๐ท โІ (๐”ผโ€˜๐‘)
79 simpr 483 . . . . . . . . . 10 ((โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›) โˆง ๐‘˜ โˆˆ (0[,)+โˆž)) โ†’ ๐‘˜ โˆˆ (0[,)+โˆž))
80 f1ocnvdm 7289 . . . . . . . . . 10 ((๐น:๐ทโ€“1-1-ontoโ†’(0[,)+โˆž) โˆง ๐‘˜ โˆˆ (0[,)+โˆž)) โ†’ (โ—ก๐นโ€˜๐‘˜) โˆˆ ๐ท)
8111, 79, 80syl2an 594 . . . . . . . . 9 ((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง (โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›) โˆง ๐‘˜ โˆˆ (0[,)+โˆž))) โ†’ (โ—ก๐นโ€˜๐‘˜) โˆˆ ๐ท)
8278, 81sselid 3970 . . . . . . . 8 ((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง (โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›) โˆง ๐‘˜ โˆˆ (0[,)+โˆž))) โ†’ (โ—ก๐นโ€˜๐‘˜) โˆˆ (๐”ผโ€˜๐‘))
832, 3, 63jca 1125 . . . . . . . . . . . . . . 15 (((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ (๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)))
8483, 7jca 510 . . . . . . . . . . . . . 14 (((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ ((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ))
8584adantr 479 . . . . . . . . . . . . 13 ((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง ((โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›) โˆง ๐‘˜ โˆˆ (0[,)+โˆž)) โˆง (๐‘ž โˆˆ ๐ด โˆง ๐‘Ÿ โˆˆ ๐ต))) โ†’ ((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ))
8632sselda 3972 . . . . . . . . . . . . . . . 16 ((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง ๐‘ž โˆˆ ๐ด) โ†’ ๐‘ž โˆˆ ๐ท)
8786adantrr 715 . . . . . . . . . . . . . . 15 ((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง (๐‘ž โˆˆ ๐ด โˆง ๐‘Ÿ โˆˆ ๐ต)) โ†’ ๐‘ž โˆˆ ๐ท)
8887adantrl 714 . . . . . . . . . . . . . 14 ((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง ((โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›) โˆง ๐‘˜ โˆˆ (0[,)+โˆž)) โˆง (๐‘ž โˆˆ ๐ด โˆง ๐‘Ÿ โˆˆ ๐ต))) โ†’ ๐‘ž โˆˆ ๐ท)
89 simplr 767 . . . . . . . . . . . . . . 15 (((โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›) โˆง ๐‘˜ โˆˆ (0[,)+โˆž)) โˆง (๐‘ž โˆˆ ๐ด โˆง ๐‘Ÿ โˆˆ ๐ต)) โ†’ ๐‘˜ โˆˆ (0[,)+โˆž))
9011, 89, 80syl2an 594 . . . . . . . . . . . . . 14 ((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง ((โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›) โˆง ๐‘˜ โˆˆ (0[,)+โˆž)) โˆง (๐‘ž โˆˆ ๐ด โˆง ๐‘Ÿ โˆˆ ๐ต))) โ†’ (โ—ก๐นโ€˜๐‘˜) โˆˆ ๐ท)
9155sselda 3972 . . . . . . . . . . . . . . . 16 ((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง ๐‘Ÿ โˆˆ ๐ต) โ†’ ๐‘Ÿ โˆˆ ๐ท)
9291adantrl 714 . . . . . . . . . . . . . . 15 ((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง (๐‘ž โˆˆ ๐ด โˆง ๐‘Ÿ โˆˆ ๐ต)) โ†’ ๐‘Ÿ โˆˆ ๐ท)
9392adantrl 714 . . . . . . . . . . . . . 14 ((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง ((โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›) โˆง ๐‘˜ โˆˆ (0[,)+โˆž)) โˆง (๐‘ž โˆˆ ๐ด โˆง ๐‘Ÿ โˆˆ ๐ต))) โ†’ ๐‘Ÿ โˆˆ ๐ท)
9488, 90, 933jca 1125 . . . . . . . . . . . . 13 ((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง ((โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›) โˆง ๐‘˜ โˆˆ (0[,)+โˆž)) โˆง (๐‘ž โˆˆ ๐ด โˆง ๐‘Ÿ โˆˆ ๐ต))) โ†’ (๐‘ž โˆˆ ๐ท โˆง (โ—ก๐นโ€˜๐‘˜) โˆˆ ๐ท โˆง ๐‘Ÿ โˆˆ ๐ท))
9585, 94jca 510 . . . . . . . . . . . 12 ((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง ((โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›) โˆง ๐‘˜ โˆˆ (0[,)+โˆž)) โˆง (๐‘ž โˆˆ ๐ด โˆง ๐‘Ÿ โˆˆ ๐ต))) โ†’ (((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (๐‘ž โˆˆ ๐ท โˆง (โ—ก๐นโ€˜๐‘˜) โˆˆ ๐ท โˆง ๐‘Ÿ โˆˆ ๐ท)))
96 f1ofun 6835 . . . . . . . . . . . . . . . . . . 19 (๐น:๐ทโ€“1-1-ontoโ†’(0[,)+โˆž) โ†’ Fun ๐น)
9711, 96syl 17 . . . . . . . . . . . . . . . . . 18 (((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ Fun ๐น)
98 fdm 6725 . . . . . . . . . . . . . . . . . . . 20 (๐น:๐ทโŸถ(0[,)+โˆž) โ†’ dom ๐น = ๐ท)
9911, 30, 983syl 18 . . . . . . . . . . . . . . . . . . 19 (((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ dom ๐น = ๐ท)
10032, 99sseqtrrd 4014 . . . . . . . . . . . . . . . . . 18 (((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ ๐ด โІ dom ๐น)
101 funfvima2 7238 . . . . . . . . . . . . . . . . . 18 ((Fun ๐น โˆง ๐ด โІ dom ๐น) โ†’ (๐‘ž โˆˆ ๐ด โ†’ (๐นโ€˜๐‘ž) โˆˆ (๐น โ€œ ๐ด)))
10297, 100, 101syl2anc 582 . . . . . . . . . . . . . . . . 17 (((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ (๐‘ž โˆˆ ๐ด โ†’ (๐นโ€˜๐‘ž) โˆˆ (๐น โ€œ ๐ด)))
10355, 99sseqtrrd 4014 . . . . . . . . . . . . . . . . . 18 (((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ ๐ต โІ dom ๐น)
104 funfvima2 7238 . . . . . . . . . . . . . . . . . 18 ((Fun ๐น โˆง ๐ต โІ dom ๐น) โ†’ (๐‘Ÿ โˆˆ ๐ต โ†’ (๐นโ€˜๐‘Ÿ) โˆˆ (๐น โ€œ ๐ต)))
10597, 103, 104syl2anc 582 . . . . . . . . . . . . . . . . 17 (((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ (๐‘Ÿ โˆˆ ๐ต โ†’ (๐นโ€˜๐‘Ÿ) โˆˆ (๐น โ€œ ๐ต)))
106102, 105anim12d 607 . . . . . . . . . . . . . . . 16 (((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ ((๐‘ž โˆˆ ๐ด โˆง ๐‘Ÿ โˆˆ ๐ต) โ†’ ((๐นโ€˜๐‘ž) โˆˆ (๐น โ€œ ๐ด) โˆง (๐นโ€˜๐‘Ÿ) โˆˆ (๐น โ€œ ๐ต))))
107106imp 405 . . . . . . . . . . . . . . 15 ((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง (๐‘ž โˆˆ ๐ด โˆง ๐‘Ÿ โˆˆ ๐ต)) โ†’ ((๐นโ€˜๐‘ž) โˆˆ (๐น โ€œ ๐ด) โˆง (๐นโ€˜๐‘Ÿ) โˆˆ (๐น โ€œ ๐ต)))
108107adantrl 714 . . . . . . . . . . . . . 14 ((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง ((โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›) โˆง ๐‘˜ โˆˆ (0[,)+โˆž)) โˆง (๐‘ž โˆˆ ๐ด โˆง ๐‘Ÿ โˆˆ ๐ต))) โ†’ ((๐นโ€˜๐‘ž) โˆˆ (๐น โ€œ ๐ด) โˆง (๐นโ€˜๐‘Ÿ) โˆˆ (๐น โ€œ ๐ต)))
109 simprll 777 . . . . . . . . . . . . . 14 ((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง ((โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›) โˆง ๐‘˜ โˆˆ (0[,)+โˆž)) โˆง (๐‘ž โˆˆ ๐ด โˆง ๐‘Ÿ โˆˆ ๐ต))) โ†’ โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›))
110 breq1 5146 . . . . . . . . . . . . . . . 16 (๐‘š = (๐นโ€˜๐‘ž) โ†’ (๐‘š โ‰ค ๐‘˜ โ†” (๐นโ€˜๐‘ž) โ‰ค ๐‘˜))
111110anbi1d 629 . . . . . . . . . . . . . . 15 (๐‘š = (๐นโ€˜๐‘ž) โ†’ ((๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›) โ†” ((๐นโ€˜๐‘ž) โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›)))
112 breq2 5147 . . . . . . . . . . . . . . . 16 (๐‘› = (๐นโ€˜๐‘Ÿ) โ†’ (๐‘˜ โ‰ค ๐‘› โ†” ๐‘˜ โ‰ค (๐นโ€˜๐‘Ÿ)))
113112anbi2d 628 . . . . . . . . . . . . . . 15 (๐‘› = (๐นโ€˜๐‘Ÿ) โ†’ (((๐นโ€˜๐‘ž) โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›) โ†” ((๐นโ€˜๐‘ž) โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค (๐นโ€˜๐‘Ÿ))))
114111, 113rspc2v 3613 . . . . . . . . . . . . . 14 (((๐นโ€˜๐‘ž) โˆˆ (๐น โ€œ ๐ด) โˆง (๐นโ€˜๐‘Ÿ) โˆˆ (๐น โ€œ ๐ต)) โ†’ (โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›) โ†’ ((๐นโ€˜๐‘ž) โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค (๐นโ€˜๐‘Ÿ))))
115108, 109, 114sylc 65 . . . . . . . . . . . . 13 ((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง ((โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›) โˆง ๐‘˜ โˆˆ (0[,)+โˆž)) โˆง (๐‘ž โˆˆ ๐ด โˆง ๐‘Ÿ โˆˆ ๐ต))) โ†’ ((๐นโ€˜๐‘ž) โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค (๐นโ€˜๐‘Ÿ)))
116 f1ocnvfv2 7281 . . . . . . . . . . . . . . . 16 ((๐น:๐ทโ€“1-1-ontoโ†’(0[,)+โˆž) โˆง ๐‘˜ โˆˆ (0[,)+โˆž)) โ†’ (๐นโ€˜(โ—ก๐นโ€˜๐‘˜)) = ๐‘˜)
11711, 89, 116syl2an 594 . . . . . . . . . . . . . . 15 ((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง ((โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›) โˆง ๐‘˜ โˆˆ (0[,)+โˆž)) โˆง (๐‘ž โˆˆ ๐ด โˆง ๐‘Ÿ โˆˆ ๐ต))) โ†’ (๐นโ€˜(โ—ก๐นโ€˜๐‘˜)) = ๐‘˜)
118117breq2d 5155 . . . . . . . . . . . . . 14 ((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง ((โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›) โˆง ๐‘˜ โˆˆ (0[,)+โˆž)) โˆง (๐‘ž โˆˆ ๐ด โˆง ๐‘Ÿ โˆˆ ๐ต))) โ†’ ((๐นโ€˜๐‘ž) โ‰ค (๐นโ€˜(โ—ก๐นโ€˜๐‘˜)) โ†” (๐นโ€˜๐‘ž) โ‰ค ๐‘˜))
119117breq1d 5153 . . . . . . . . . . . . . 14 ((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง ((โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›) โˆง ๐‘˜ โˆˆ (0[,)+โˆž)) โˆง (๐‘ž โˆˆ ๐ด โˆง ๐‘Ÿ โˆˆ ๐ต))) โ†’ ((๐นโ€˜(โ—ก๐นโ€˜๐‘˜)) โ‰ค (๐นโ€˜๐‘Ÿ) โ†” ๐‘˜ โ‰ค (๐นโ€˜๐‘Ÿ)))
120118, 119anbi12d 630 . . . . . . . . . . . . 13 ((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง ((โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›) โˆง ๐‘˜ โˆˆ (0[,)+โˆž)) โˆง (๐‘ž โˆˆ ๐ด โˆง ๐‘Ÿ โˆˆ ๐ต))) โ†’ (((๐นโ€˜๐‘ž) โ‰ค (๐นโ€˜(โ—ก๐นโ€˜๐‘˜)) โˆง (๐นโ€˜(โ—ก๐นโ€˜๐‘˜)) โ‰ค (๐นโ€˜๐‘Ÿ)) โ†” ((๐นโ€˜๐‘ž) โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค (๐นโ€˜๐‘Ÿ))))
121115, 120mpbird 256 . . . . . . . . . . . 12 ((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง ((โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›) โˆง ๐‘˜ โˆˆ (0[,)+โˆž)) โˆง (๐‘ž โˆˆ ๐ด โˆง ๐‘Ÿ โˆˆ ๐ต))) โ†’ ((๐นโ€˜๐‘ž) โ‰ค (๐นโ€˜(โ—ก๐นโ€˜๐‘˜)) โˆง (๐นโ€˜(โ—ก๐นโ€˜๐‘˜)) โ‰ค (๐นโ€˜๐‘Ÿ)))
1228, 9axcontlem8 28824 . . . . . . . . . . . 12 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (๐‘ž โˆˆ ๐ท โˆง (โ—ก๐นโ€˜๐‘˜) โˆˆ ๐ท โˆง ๐‘Ÿ โˆˆ ๐ท)) โ†’ (((๐นโ€˜๐‘ž) โ‰ค (๐นโ€˜(โ—ก๐นโ€˜๐‘˜)) โˆง (๐นโ€˜(โ—ก๐นโ€˜๐‘˜)) โ‰ค (๐นโ€˜๐‘Ÿ)) โ†’ (โ—ก๐นโ€˜๐‘˜) Btwn โŸจ๐‘ž, ๐‘ŸโŸฉ))
12395, 121, 122sylc 65 . . . . . . . . . . 11 ((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง ((โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›) โˆง ๐‘˜ โˆˆ (0[,)+โˆž)) โˆง (๐‘ž โˆˆ ๐ด โˆง ๐‘Ÿ โˆˆ ๐ต))) โ†’ (โ—ก๐นโ€˜๐‘˜) Btwn โŸจ๐‘ž, ๐‘ŸโŸฉ)
124123anassrs 466 . . . . . . . . . 10 (((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง (โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›) โˆง ๐‘˜ โˆˆ (0[,)+โˆž))) โˆง (๐‘ž โˆˆ ๐ด โˆง ๐‘Ÿ โˆˆ ๐ต)) โ†’ (โ—ก๐นโ€˜๐‘˜) Btwn โŸจ๐‘ž, ๐‘ŸโŸฉ)
125124ralrimivva 3191 . . . . . . . . 9 ((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง (โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›) โˆง ๐‘˜ โˆˆ (0[,)+โˆž))) โ†’ โˆ€๐‘ž โˆˆ ๐ด โˆ€๐‘Ÿ โˆˆ ๐ต (โ—ก๐นโ€˜๐‘˜) Btwn โŸจ๐‘ž, ๐‘ŸโŸฉ)
126 opeq1 4869 . . . . . . . . . . 11 (๐‘ž = ๐‘ฅ โ†’ โŸจ๐‘ž, ๐‘ŸโŸฉ = โŸจ๐‘ฅ, ๐‘ŸโŸฉ)
127126breq2d 5155 . . . . . . . . . 10 (๐‘ž = ๐‘ฅ โ†’ ((โ—ก๐นโ€˜๐‘˜) Btwn โŸจ๐‘ž, ๐‘ŸโŸฉ โ†” (โ—ก๐นโ€˜๐‘˜) Btwn โŸจ๐‘ฅ, ๐‘ŸโŸฉ))
128 opeq2 4870 . . . . . . . . . . 11 (๐‘Ÿ = ๐‘ฆ โ†’ โŸจ๐‘ฅ, ๐‘ŸโŸฉ = โŸจ๐‘ฅ, ๐‘ฆโŸฉ)
129128breq2d 5155 . . . . . . . . . 10 (๐‘Ÿ = ๐‘ฆ โ†’ ((โ—ก๐นโ€˜๐‘˜) Btwn โŸจ๐‘ฅ, ๐‘ŸโŸฉ โ†” (โ—ก๐นโ€˜๐‘˜) Btwn โŸจ๐‘ฅ, ๐‘ฆโŸฉ))
130127, 129cbvral2vw 3229 . . . . . . . . 9 (โˆ€๐‘ž โˆˆ ๐ด โˆ€๐‘Ÿ โˆˆ ๐ต (โ—ก๐นโ€˜๐‘˜) Btwn โŸจ๐‘ž, ๐‘ŸโŸฉ โ†” โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต (โ—ก๐นโ€˜๐‘˜) Btwn โŸจ๐‘ฅ, ๐‘ฆโŸฉ)
131125, 130sylib 217 . . . . . . . 8 ((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง (โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›) โˆง ๐‘˜ โˆˆ (0[,)+โˆž))) โ†’ โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต (โ—ก๐นโ€˜๐‘˜) Btwn โŸจ๐‘ฅ, ๐‘ฆโŸฉ)
132 breq1 5146 . . . . . . . . . 10 (๐‘ = (โ—ก๐นโ€˜๐‘˜) โ†’ (๐‘ Btwn โŸจ๐‘ฅ, ๐‘ฆโŸฉ โ†” (โ—ก๐นโ€˜๐‘˜) Btwn โŸจ๐‘ฅ, ๐‘ฆโŸฉ))
1331322ralbidv 3209 . . . . . . . . 9 (๐‘ = (โ—ก๐นโ€˜๐‘˜) โ†’ (โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ Btwn โŸจ๐‘ฅ, ๐‘ฆโŸฉ โ†” โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต (โ—ก๐นโ€˜๐‘˜) Btwn โŸจ๐‘ฅ, ๐‘ฆโŸฉ))
134133rspcev 3602 . . . . . . . 8 (((โ—ก๐นโ€˜๐‘˜) โˆˆ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต (โ—ก๐นโ€˜๐‘˜) Btwn โŸจ๐‘ฅ, ๐‘ฆโŸฉ) โ†’ โˆƒ๐‘ โˆˆ (๐”ผโ€˜๐‘)โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ Btwn โŸจ๐‘ฅ, ๐‘ฆโŸฉ)
13582, 131, 134syl2anc 582 . . . . . . 7 ((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง (โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›) โˆง ๐‘˜ โˆˆ (0[,)+โˆž))) โ†’ โˆƒ๐‘ โˆˆ (๐”ผโ€˜๐‘)โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ Btwn โŸจ๐‘ฅ, ๐‘ฆโŸฉ)
136135expr 455 . . . . . 6 ((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›)) โ†’ (๐‘˜ โˆˆ (0[,)+โˆž) โ†’ โˆƒ๐‘ โˆˆ (๐”ผโ€˜๐‘)โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ Btwn โŸจ๐‘ฅ, ๐‘ฆโŸฉ))
13777, 136syld 47 . . . . 5 ((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›)) โ†’ (๐‘˜ โˆˆ โ„ โ†’ โˆƒ๐‘ โˆˆ (๐”ผโ€˜๐‘)โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ Btwn โŸจ๐‘ฅ, ๐‘ฆโŸฉ))
138137ex 411 . . . 4 (((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ (โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›) โ†’ (๐‘˜ โˆˆ โ„ โ†’ โˆƒ๐‘ โˆˆ (๐”ผโ€˜๐‘)โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ Btwn โŸจ๐‘ฅ, ๐‘ฆโŸฉ)))
139138com23 86 . . 3 (((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ (๐‘˜ โˆˆ โ„ โ†’ (โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›) โ†’ โˆƒ๐‘ โˆˆ (๐”ผโ€˜๐‘)โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ Btwn โŸจ๐‘ฅ, ๐‘ฆโŸฉ)))
140139rexlimdv 3143 . 2 (((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ (โˆƒ๐‘˜ โˆˆ โ„ โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›) โ†’ โˆƒ๐‘ โˆˆ (๐”ผโ€˜๐‘)โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ Btwn โŸจ๐‘ฅ, ๐‘ฆโŸฉ))
14123, 140mpd 15 1 (((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ โˆƒ๐‘ โˆˆ (๐”ผโ€˜๐‘)โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ Btwn โŸจ๐‘ฅ, ๐‘ฆโŸฉ)
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โ†” wb 205   โˆง wa 394   โˆจ wo 845   โˆง w3a 1084   = wceq 1533  โˆƒwex 1773   โˆˆ wcel 2098   โ‰  wne 2930  โˆ€wral 3051  โˆƒwrex 3060  {crab 3419   โІ wss 3940  โˆ…c0 4318  โŸจcop 4630   class class class wbr 5143  {copab 5205  โ—กccnv 5671  dom cdm 5672  ran crn 5673   โ€œ cima 5675  Fun wfun 6536  โŸถwf 6538  โ€“1-1โ†’wf1 6539  โ€“ontoโ†’wfo 6540  โ€“1-1-ontoโ†’wf1o 6541  โ€˜cfv 6542  (class class class)co 7415  โ„cr 11135  0cc0 11136  1c1 11137   + caddc 11139   ยท cmul 11141  +โˆžcpnf 11273   โ‰ค cle 11277   โˆ’ cmin 11472  โ„•cn 12240  [,)cico 13356  ...cfz 13514  ๐”ผcee 28741   Btwn cbtwn 28742
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-sep 5294  ax-nul 5301  ax-pow 5359  ax-pr 5423  ax-un 7737  ax-cnex 11192  ax-resscn 11193  ax-1cn 11194  ax-icn 11195  ax-addcl 11196  ax-addrcl 11197  ax-mulcl 11198  ax-mulrcl 11199  ax-mulcom 11200  ax-addass 11201  ax-mulass 11202  ax-distr 11203  ax-i2m1 11204  ax-1ne0 11205  ax-1rid 11206  ax-rnegex 11207  ax-rrecex 11208  ax-cnre 11209  ax-pre-lttri 11210  ax-pre-lttrn 11211  ax-pre-ltadd 11212  ax-pre-mulgt0 11213  ax-pre-sup 11214
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3364  df-reu 3365  df-rab 3420  df-v 3465  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-pss 3960  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5227  df-tr 5261  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-riota 7371  df-ov 7418  df-oprab 7419  df-mpo 7420  df-om 7868  df-1st 7989  df-2nd 7990  df-frecs 8283  df-wrecs 8314  df-recs 8388  df-rdg 8427  df-er 8721  df-map 8843  df-en 8961  df-dom 8962  df-sdom 8963  df-pnf 11278  df-mnf 11279  df-xr 11280  df-ltxr 11281  df-le 11282  df-sub 11474  df-neg 11475  df-div 11900  df-nn 12241  df-z 12587  df-uz 12851  df-ico 13360  df-icc 13361  df-fz 13515  df-ee 28744  df-btwn 28745
This theorem is referenced by:  axcontlem11  28827
  Copyright terms: Public domain W3C validator