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

Theorem axcontlem10 28739
Description: Lemma for axcont 28742. 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 6064 . . . . 5 (๐น โ€œ ๐ด) โІ ran ๐น
2 simpll 764 . . . . . . 7 (((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ ๐‘ โˆˆ โ„•)
3 simprl1 1215 . . . . . . 7 (((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ ๐‘ โˆˆ (๐”ผโ€˜๐‘))
4 simplr1 1212 . . . . . . . 8 (((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ ๐ด โІ (๐”ผโ€˜๐‘))
5 simprl2 1216 . . . . . . . 8 (((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ ๐‘ˆ โˆˆ ๐ด)
64, 5sseldd 3978 . . . . . . 7 (((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘))
7 simprr 770 . . . . . . 7 (((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ ๐‘ โ‰  ๐‘ˆ)
8 axcontlem10.1 . . . . . . . 8 ๐ท = {๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆฃ (๐‘ˆ Btwn โŸจ๐‘, ๐‘โŸฉ โˆจ ๐‘ Btwn โŸจ๐‘, ๐‘ˆโŸฉ)}
9 axcontlem10.2 . . . . . . . 8 ๐น = {โŸจ๐‘ฅ, ๐‘กโŸฉ โˆฃ (๐‘ฅ โˆˆ ๐ท โˆง (๐‘ก โˆˆ (0[,)+โˆž) โˆง โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–)))))}
108, 9axcontlem2 28731 . . . . . . 7 (((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โ†’ ๐น:๐ทโ€“1-1-ontoโ†’(0[,)+โˆž))
112, 3, 6, 7, 10syl31anc 1370 . . . . . 6 (((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ ๐น:๐ทโ€“1-1-ontoโ†’(0[,)+โˆž))
12 f1ofo 6834 . . . . . 6 (๐น:๐ทโ€“1-1-ontoโ†’(0[,)+โˆž) โ†’ ๐น:๐ทโ€“ontoโ†’(0[,)+โˆž))
13 forn 6802 . . . . . 6 (๐น:๐ทโ€“ontoโ†’(0[,)+โˆž) โ†’ ran ๐น = (0[,)+โˆž))
1411, 12, 133syl 18 . . . . 5 (((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ ran ๐น = (0[,)+โˆž))
151, 14sseqtrid 4029 . . . 4 (((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ (๐น โ€œ ๐ด) โІ (0[,)+โˆž))
16 rge0ssre 13439 . . . 4 (0[,)+โˆž) โІ โ„
1715, 16sstrdi 3989 . . 3 (((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ (๐น โ€œ ๐ด) โІ โ„)
18 imassrn 6064 . . . . 5 (๐น โ€œ ๐ต) โІ ran ๐น
1918, 14sseqtrid 4029 . . . 4 (((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ (๐น โ€œ ๐ต) โІ (0[,)+โˆž))
2019, 16sstrdi 3989 . . 3 (((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ (๐น โ€œ ๐ต) โІ โ„)
218, 9axcontlem9 28738 . . 3 (((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)๐‘š โ‰ค ๐‘›)
22 dedekindle 11382 . . 3 (((๐น โ€œ ๐ด) โІ โ„ โˆง (๐น โ€œ ๐ต) โІ โ„ โˆง โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)๐‘š โ‰ค ๐‘›) โ†’ โˆƒ๐‘˜ โˆˆ โ„ โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›))
2317, 20, 21, 22syl3anc 1368 . 2 (((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ โˆƒ๐‘˜ โˆˆ โ„ โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›))
24 simpr 484 . . . . . . . 8 (((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›)) โˆง ๐‘˜ โˆˆ โ„) โ†’ ๐‘˜ โˆˆ โ„)
25 simprl3 1217 . . . . . . . . . . 11 (((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ ๐ต โ‰  โˆ…)
2625ad2antrr 723 . . . . . . . . . 10 (((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›)) โˆง ๐‘˜ โˆˆ โ„) โ†’ ๐ต โ‰  โˆ…)
27 n0 4341 . . . . . . . . . 10 (๐ต โ‰  โˆ… โ†” โˆƒ๐‘ ๐‘ โˆˆ ๐ต)
2826, 27sylib 217 . . . . . . . . 9 (((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›)) โˆง ๐‘˜ โˆˆ โ„) โ†’ โˆƒ๐‘ ๐‘ โˆˆ ๐ต)
29 0red 11221 . . . . . . . . . . . 12 (((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›)) โˆง (๐‘˜ โˆˆ โ„ โˆง ๐‘ โˆˆ ๐ต)) โ†’ 0 โˆˆ โ„)
30 f1of 6827 . . . . . . . . . . . . . . . 16 (๐น:๐ทโ€“1-1-ontoโ†’(0[,)+โˆž) โ†’ ๐น:๐ทโŸถ(0[,)+โˆž))
3111, 30syl 17 . . . . . . . . . . . . . . 15 (((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ ๐น:๐ทโŸถ(0[,)+โˆž))
328axcontlem4 28733 . . . . . . . . . . . . . . . 16 (((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ ๐ด โІ ๐ท)
3332, 5sseldd 3978 . . . . . . . . . . . . . . 15 (((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ ๐‘ˆ โˆˆ ๐ท)
3431, 33ffvelcdmd 7081 . . . . . . . . . . . . . 14 (((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ (๐นโ€˜๐‘ˆ) โˆˆ (0[,)+โˆž))
3516, 34sselid 3975 . . . . . . . . . . . . 13 (((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ (๐นโ€˜๐‘ˆ) โˆˆ โ„)
3635ad2antrr 723 . . . . . . . . . . . 12 (((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›)) โˆง (๐‘˜ โˆˆ โ„ โˆง ๐‘ โˆˆ ๐ต)) โ†’ (๐นโ€˜๐‘ˆ) โˆˆ โ„)
37 simprl 768 . . . . . . . . . . . 12 (((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›)) โˆง (๐‘˜ โˆˆ โ„ โˆง ๐‘ โˆˆ ๐ต)) โ†’ ๐‘˜ โˆˆ โ„)
38 elrege0 13437 . . . . . . . . . . . . . . 15 ((๐นโ€˜๐‘ˆ) โˆˆ (0[,)+โˆž) โ†” ((๐นโ€˜๐‘ˆ) โˆˆ โ„ โˆง 0 โ‰ค (๐นโ€˜๐‘ˆ)))
3938simprbi 496 . . . . . . . . . . . . . 14 ((๐นโ€˜๐‘ˆ) โˆˆ (0[,)+โˆž) โ†’ 0 โ‰ค (๐นโ€˜๐‘ˆ))
4034, 39syl 17 . . . . . . . . . . . . 13 (((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ 0 โ‰ค (๐นโ€˜๐‘ˆ))
4140ad2antrr 723 . . . . . . . . . . . 12 (((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›)) โˆง (๐‘˜ โˆˆ โ„ โˆง ๐‘ โˆˆ ๐ต)) โ†’ 0 โ‰ค (๐นโ€˜๐‘ˆ))
42 f1of1 6826 . . . . . . . . . . . . . . . . . . . 20 (๐น:๐ทโ€“1-1-ontoโ†’(0[,)+โˆž) โ†’ ๐น:๐ทโ€“1-1โ†’(0[,)+โˆž))
4311, 42syl 17 . . . . . . . . . . . . . . . . . . 19 (((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ ๐น:๐ทโ€“1-1โ†’(0[,)+โˆž))
44 f1elima 7258 . . . . . . . . . . . . . . . . . . 19 ((๐น:๐ทโ€“1-1โ†’(0[,)+โˆž) โˆง ๐‘ˆ โˆˆ ๐ท โˆง ๐ด โІ ๐ท) โ†’ ((๐นโ€˜๐‘ˆ) โˆˆ (๐น โ€œ ๐ด) โ†” ๐‘ˆ โˆˆ ๐ด))
4543, 33, 32, 44syl3anc 1368 . . . . . . . . . . . . . . . . . 18 (((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ ((๐นโ€˜๐‘ˆ) โˆˆ (๐น โ€œ ๐ด) โ†” ๐‘ˆ โˆˆ ๐ด))
465, 45mpbird 257 . . . . . . . . . . . . . . . . 17 (((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ (๐นโ€˜๐‘ˆ) โˆˆ (๐น โ€œ ๐ด))
4746adantr 480 . . . . . . . . . . . . . . . 16 ((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง (๐‘˜ โˆˆ โ„ โˆง ๐‘ โˆˆ ๐ต)) โ†’ (๐นโ€˜๐‘ˆ) โˆˆ (๐น โ€œ ๐ด))
48 simpr 484 . . . . . . . . . . . . . . . . . 18 ((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง ๐‘ โˆˆ ๐ต) โ†’ ๐‘ โˆˆ ๐ต)
4943adantr 480 . . . . . . . . . . . . . . . . . . 19 ((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง ๐‘ โˆˆ ๐ต) โ†’ ๐น:๐ทโ€“1-1โ†’(0[,)+โˆž))
50 simpl1 1188 . . . . . . . . . . . . . . . . . . . . . 22 (((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ) โ†’ ๐‘ โˆˆ (๐”ผโ€˜๐‘))
51 simpl2 1189 . . . . . . . . . . . . . . . . . . . . . 22 (((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ) โ†’ ๐‘ˆ โˆˆ ๐ด)
52 simpr 484 . . . . . . . . . . . . . . . . . . . . . 22 (((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ) โ†’ ๐‘ โ‰  ๐‘ˆ)
5350, 51, 523jca 1125 . . . . . . . . . . . . . . . . . . . . 21 (((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ) โ†’ (๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐‘ โ‰  ๐‘ˆ))
548axcontlem3 28732 . . . . . . . . . . . . . . . . . . . . 21 (((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง (๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ ๐ต โІ ๐ท)
5553, 54sylan2 592 . . . . . . . . . . . . . . . . . . . 20 (((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ ๐ต โІ ๐ท)
5655sselda 3977 . . . . . . . . . . . . . . . . . . 19 ((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง ๐‘ โˆˆ ๐ต) โ†’ ๐‘ โˆˆ ๐ท)
5755adantr 480 . . . . . . . . . . . . . . . . . . 19 ((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง ๐‘ โˆˆ ๐ต) โ†’ ๐ต โІ ๐ท)
58 f1elima 7258 . . . . . . . . . . . . . . . . . . 19 ((๐น:๐ทโ€“1-1โ†’(0[,)+โˆž) โˆง ๐‘ โˆˆ ๐ท โˆง ๐ต โІ ๐ท) โ†’ ((๐นโ€˜๐‘) โˆˆ (๐น โ€œ ๐ต) โ†” ๐‘ โˆˆ ๐ต))
5949, 56, 57, 58syl3anc 1368 . . . . . . . . . . . . . . . . . 18 ((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง ๐‘ โˆˆ ๐ต) โ†’ ((๐นโ€˜๐‘) โˆˆ (๐น โ€œ ๐ต) โ†” ๐‘ โˆˆ ๐ต))
6048, 59mpbird 257 . . . . . . . . . . . . . . . . 17 ((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง ๐‘ โˆˆ ๐ต) โ†’ (๐นโ€˜๐‘) โˆˆ (๐น โ€œ ๐ต))
6160adantrl 713 . . . . . . . . . . . . . . . 16 ((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง (๐‘˜ โˆˆ โ„ โˆง ๐‘ โˆˆ ๐ต)) โ†’ (๐นโ€˜๐‘) โˆˆ (๐น โ€œ ๐ต))
6247, 61jca 511 . . . . . . . . . . . . . . 15 ((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง (๐‘˜ โˆˆ โ„ โˆง ๐‘ โˆˆ ๐ต)) โ†’ ((๐นโ€˜๐‘ˆ) โˆˆ (๐น โ€œ ๐ด) โˆง (๐นโ€˜๐‘) โˆˆ (๐น โ€œ ๐ต)))
63 breq1 5144 . . . . . . . . . . . . . . . . 17 (๐‘š = (๐นโ€˜๐‘ˆ) โ†’ (๐‘š โ‰ค ๐‘˜ โ†” (๐นโ€˜๐‘ˆ) โ‰ค ๐‘˜))
6463anbi1d 629 . . . . . . . . . . . . . . . 16 (๐‘š = (๐นโ€˜๐‘ˆ) โ†’ ((๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›) โ†” ((๐นโ€˜๐‘ˆ) โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›)))
65 breq2 5145 . . . . . . . . . . . . . . . . 17 (๐‘› = (๐นโ€˜๐‘) โ†’ (๐‘˜ โ‰ค ๐‘› โ†” ๐‘˜ โ‰ค (๐นโ€˜๐‘)))
6665anbi2d 628 . . . . . . . . . . . . . . . 16 (๐‘› = (๐นโ€˜๐‘) โ†’ (((๐นโ€˜๐‘ˆ) โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›) โ†” ((๐นโ€˜๐‘ˆ) โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค (๐นโ€˜๐‘))))
6764, 66rspc2va 3618 . . . . . . . . . . . . . . 15 ((((๐นโ€˜๐‘ˆ) โˆˆ (๐น โ€œ ๐ด) โˆง (๐นโ€˜๐‘) โˆˆ (๐น โ€œ ๐ต)) โˆง โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›)) โ†’ ((๐นโ€˜๐‘ˆ) โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค (๐นโ€˜๐‘)))
6862, 67sylan 579 . . . . . . . . . . . . . 14 (((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง (๐‘˜ โˆˆ โ„ โˆง ๐‘ โˆˆ ๐ต)) โˆง โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›)) โ†’ ((๐นโ€˜๐‘ˆ) โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค (๐นโ€˜๐‘)))
6968an32s 649 . . . . . . . . . . . . 13 (((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›)) โˆง (๐‘˜ โˆˆ โ„ โˆง ๐‘ โˆˆ ๐ต)) โ†’ ((๐นโ€˜๐‘ˆ) โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค (๐นโ€˜๐‘)))
7069simpld 494 . . . . . . . . . . . 12 (((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›)) โˆง (๐‘˜ โˆˆ โ„ โˆง ๐‘ โˆˆ ๐ต)) โ†’ (๐นโ€˜๐‘ˆ) โ‰ค ๐‘˜)
7129, 36, 37, 41, 70letrd 11375 . . . . . . . . . . 11 (((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›)) โˆง (๐‘˜ โˆˆ โ„ โˆง ๐‘ โˆˆ ๐ต)) โ†’ 0 โ‰ค ๐‘˜)
7271expr 456 . . . . . . . . . 10 (((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›)) โˆง ๐‘˜ โˆˆ โ„) โ†’ (๐‘ โˆˆ ๐ต โ†’ 0 โ‰ค ๐‘˜))
7372exlimdv 1928 . . . . . . . . 9 (((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›)) โˆง ๐‘˜ โˆˆ โ„) โ†’ (โˆƒ๐‘ ๐‘ โˆˆ ๐ต โ†’ 0 โ‰ค ๐‘˜))
7428, 73mpd 15 . . . . . . . 8 (((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›)) โˆง ๐‘˜ โˆˆ โ„) โ†’ 0 โ‰ค ๐‘˜)
75 elrege0 13437 . . . . . . . 8 (๐‘˜ โˆˆ (0[,)+โˆž) โ†” (๐‘˜ โˆˆ โ„ โˆง 0 โ‰ค ๐‘˜))
7624, 74, 75sylanbrc 582 . . . . . . 7 (((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›)) โˆง ๐‘˜ โˆˆ โ„) โ†’ ๐‘˜ โˆˆ (0[,)+โˆž))
7776ex 412 . . . . . 6 ((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›)) โ†’ (๐‘˜ โˆˆ โ„ โ†’ ๐‘˜ โˆˆ (0[,)+โˆž)))
788ssrab3 4075 . . . . . . . . 9 ๐ท โІ (๐”ผโ€˜๐‘)
79 simpr 484 . . . . . . . . . 10 ((โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›) โˆง ๐‘˜ โˆˆ (0[,)+โˆž)) โ†’ ๐‘˜ โˆˆ (0[,)+โˆž))
80 f1ocnvdm 7279 . . . . . . . . . 10 ((๐น:๐ทโ€“1-1-ontoโ†’(0[,)+โˆž) โˆง ๐‘˜ โˆˆ (0[,)+โˆž)) โ†’ (โ—ก๐นโ€˜๐‘˜) โˆˆ ๐ท)
8111, 79, 80syl2an 595 . . . . . . . . 9 ((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง (โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›) โˆง ๐‘˜ โˆˆ (0[,)+โˆž))) โ†’ (โ—ก๐นโ€˜๐‘˜) โˆˆ ๐ท)
8278, 81sselid 3975 . . . . . . . 8 ((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง (โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›) โˆง ๐‘˜ โˆˆ (0[,)+โˆž))) โ†’ (โ—ก๐นโ€˜๐‘˜) โˆˆ (๐”ผโ€˜๐‘))
832, 3, 63jca 1125 . . . . . . . . . . . . . . 15 (((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ (๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)))
8483, 7jca 511 . . . . . . . . . . . . . 14 (((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ ((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ))
8584adantr 480 . . . . . . . . . . . . 13 ((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง ((โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›) โˆง ๐‘˜ โˆˆ (0[,)+โˆž)) โˆง (๐‘ž โˆˆ ๐ด โˆง ๐‘Ÿ โˆˆ ๐ต))) โ†’ ((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ))
8632sselda 3977 . . . . . . . . . . . . . . . 16 ((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง ๐‘ž โˆˆ ๐ด) โ†’ ๐‘ž โˆˆ ๐ท)
8786adantrr 714 . . . . . . . . . . . . . . 15 ((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง (๐‘ž โˆˆ ๐ด โˆง ๐‘Ÿ โˆˆ ๐ต)) โ†’ ๐‘ž โˆˆ ๐ท)
8887adantrl 713 . . . . . . . . . . . . . 14 ((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง ((โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›) โˆง ๐‘˜ โˆˆ (0[,)+โˆž)) โˆง (๐‘ž โˆˆ ๐ด โˆง ๐‘Ÿ โˆˆ ๐ต))) โ†’ ๐‘ž โˆˆ ๐ท)
89 simplr 766 . . . . . . . . . . . . . . 15 (((โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›) โˆง ๐‘˜ โˆˆ (0[,)+โˆž)) โˆง (๐‘ž โˆˆ ๐ด โˆง ๐‘Ÿ โˆˆ ๐ต)) โ†’ ๐‘˜ โˆˆ (0[,)+โˆž))
9011, 89, 80syl2an 595 . . . . . . . . . . . . . 14 ((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง ((โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›) โˆง ๐‘˜ โˆˆ (0[,)+โˆž)) โˆง (๐‘ž โˆˆ ๐ด โˆง ๐‘Ÿ โˆˆ ๐ต))) โ†’ (โ—ก๐นโ€˜๐‘˜) โˆˆ ๐ท)
9155sselda 3977 . . . . . . . . . . . . . . . 16 ((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง ๐‘Ÿ โˆˆ ๐ต) โ†’ ๐‘Ÿ โˆˆ ๐ท)
9291adantrl 713 . . . . . . . . . . . . . . 15 ((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง (๐‘ž โˆˆ ๐ด โˆง ๐‘Ÿ โˆˆ ๐ต)) โ†’ ๐‘Ÿ โˆˆ ๐ท)
9392adantrl 713 . . . . . . . . . . . . . 14 ((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง ((โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›) โˆง ๐‘˜ โˆˆ (0[,)+โˆž)) โˆง (๐‘ž โˆˆ ๐ด โˆง ๐‘Ÿ โˆˆ ๐ต))) โ†’ ๐‘Ÿ โˆˆ ๐ท)
9488, 90, 933jca 1125 . . . . . . . . . . . . 13 ((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง ((โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›) โˆง ๐‘˜ โˆˆ (0[,)+โˆž)) โˆง (๐‘ž โˆˆ ๐ด โˆง ๐‘Ÿ โˆˆ ๐ต))) โ†’ (๐‘ž โˆˆ ๐ท โˆง (โ—ก๐นโ€˜๐‘˜) โˆˆ ๐ท โˆง ๐‘Ÿ โˆˆ ๐ท))
9585, 94jca 511 . . . . . . . . . . . 12 ((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง ((โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›) โˆง ๐‘˜ โˆˆ (0[,)+โˆž)) โˆง (๐‘ž โˆˆ ๐ด โˆง ๐‘Ÿ โˆˆ ๐ต))) โ†’ (((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (๐‘ž โˆˆ ๐ท โˆง (โ—ก๐นโ€˜๐‘˜) โˆˆ ๐ท โˆง ๐‘Ÿ โˆˆ ๐ท)))
96 f1ofun 6829 . . . . . . . . . . . . . . . . . . 19 (๐น:๐ทโ€“1-1-ontoโ†’(0[,)+โˆž) โ†’ Fun ๐น)
9711, 96syl 17 . . . . . . . . . . . . . . . . . 18 (((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ Fun ๐น)
98 fdm 6720 . . . . . . . . . . . . . . . . . . . 20 (๐น:๐ทโŸถ(0[,)+โˆž) โ†’ dom ๐น = ๐ท)
9911, 30, 983syl 18 . . . . . . . . . . . . . . . . . . 19 (((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ dom ๐น = ๐ท)
10032, 99sseqtrrd 4018 . . . . . . . . . . . . . . . . . 18 (((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ ๐ด โІ dom ๐น)
101 funfvima2 7228 . . . . . . . . . . . . . . . . . 18 ((Fun ๐น โˆง ๐ด โІ dom ๐น) โ†’ (๐‘ž โˆˆ ๐ด โ†’ (๐นโ€˜๐‘ž) โˆˆ (๐น โ€œ ๐ด)))
10297, 100, 101syl2anc 583 . . . . . . . . . . . . . . . . 17 (((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ (๐‘ž โˆˆ ๐ด โ†’ (๐นโ€˜๐‘ž) โˆˆ (๐น โ€œ ๐ด)))
10355, 99sseqtrrd 4018 . . . . . . . . . . . . . . . . . 18 (((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ ๐ต โІ dom ๐น)
104 funfvima2 7228 . . . . . . . . . . . . . . . . . 18 ((Fun ๐น โˆง ๐ต โІ dom ๐น) โ†’ (๐‘Ÿ โˆˆ ๐ต โ†’ (๐นโ€˜๐‘Ÿ) โˆˆ (๐น โ€œ ๐ต)))
10597, 103, 104syl2anc 583 . . . . . . . . . . . . . . . . 17 (((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ (๐‘Ÿ โˆˆ ๐ต โ†’ (๐นโ€˜๐‘Ÿ) โˆˆ (๐น โ€œ ๐ต)))
106102, 105anim12d 608 . . . . . . . . . . . . . . . 16 (((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ ((๐‘ž โˆˆ ๐ด โˆง ๐‘Ÿ โˆˆ ๐ต) โ†’ ((๐นโ€˜๐‘ž) โˆˆ (๐น โ€œ ๐ด) โˆง (๐นโ€˜๐‘Ÿ) โˆˆ (๐น โ€œ ๐ต))))
107106imp 406 . . . . . . . . . . . . . . 15 ((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง (๐‘ž โˆˆ ๐ด โˆง ๐‘Ÿ โˆˆ ๐ต)) โ†’ ((๐นโ€˜๐‘ž) โˆˆ (๐น โ€œ ๐ด) โˆง (๐นโ€˜๐‘Ÿ) โˆˆ (๐น โ€œ ๐ต)))
108107adantrl 713 . . . . . . . . . . . . . 14 ((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง ((โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›) โˆง ๐‘˜ โˆˆ (0[,)+โˆž)) โˆง (๐‘ž โˆˆ ๐ด โˆง ๐‘Ÿ โˆˆ ๐ต))) โ†’ ((๐นโ€˜๐‘ž) โˆˆ (๐น โ€œ ๐ด) โˆง (๐นโ€˜๐‘Ÿ) โˆˆ (๐น โ€œ ๐ต)))
109 simprll 776 . . . . . . . . . . . . . 14 ((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง ((โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›) โˆง ๐‘˜ โˆˆ (0[,)+โˆž)) โˆง (๐‘ž โˆˆ ๐ด โˆง ๐‘Ÿ โˆˆ ๐ต))) โ†’ โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›))
110 breq1 5144 . . . . . . . . . . . . . . . 16 (๐‘š = (๐นโ€˜๐‘ž) โ†’ (๐‘š โ‰ค ๐‘˜ โ†” (๐นโ€˜๐‘ž) โ‰ค ๐‘˜))
111110anbi1d 629 . . . . . . . . . . . . . . 15 (๐‘š = (๐นโ€˜๐‘ž) โ†’ ((๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›) โ†” ((๐นโ€˜๐‘ž) โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›)))
112 breq2 5145 . . . . . . . . . . . . . . . 16 (๐‘› = (๐นโ€˜๐‘Ÿ) โ†’ (๐‘˜ โ‰ค ๐‘› โ†” ๐‘˜ โ‰ค (๐นโ€˜๐‘Ÿ)))
113112anbi2d 628 . . . . . . . . . . . . . . 15 (๐‘› = (๐นโ€˜๐‘Ÿ) โ†’ (((๐นโ€˜๐‘ž) โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›) โ†” ((๐นโ€˜๐‘ž) โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค (๐นโ€˜๐‘Ÿ))))
114111, 113rspc2v 3617 . . . . . . . . . . . . . 14 (((๐นโ€˜๐‘ž) โˆˆ (๐น โ€œ ๐ด) โˆง (๐นโ€˜๐‘Ÿ) โˆˆ (๐น โ€œ ๐ต)) โ†’ (โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›) โ†’ ((๐นโ€˜๐‘ž) โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค (๐นโ€˜๐‘Ÿ))))
115108, 109, 114sylc 65 . . . . . . . . . . . . 13 ((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง ((โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›) โˆง ๐‘˜ โˆˆ (0[,)+โˆž)) โˆง (๐‘ž โˆˆ ๐ด โˆง ๐‘Ÿ โˆˆ ๐ต))) โ†’ ((๐นโ€˜๐‘ž) โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค (๐นโ€˜๐‘Ÿ)))
116 f1ocnvfv2 7271 . . . . . . . . . . . . . . . 16 ((๐น:๐ทโ€“1-1-ontoโ†’(0[,)+โˆž) โˆง ๐‘˜ โˆˆ (0[,)+โˆž)) โ†’ (๐นโ€˜(โ—ก๐นโ€˜๐‘˜)) = ๐‘˜)
11711, 89, 116syl2an 595 . . . . . . . . . . . . . . 15 ((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง ((โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›) โˆง ๐‘˜ โˆˆ (0[,)+โˆž)) โˆง (๐‘ž โˆˆ ๐ด โˆง ๐‘Ÿ โˆˆ ๐ต))) โ†’ (๐นโ€˜(โ—ก๐นโ€˜๐‘˜)) = ๐‘˜)
118117breq2d 5153 . . . . . . . . . . . . . 14 ((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง ((โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›) โˆง ๐‘˜ โˆˆ (0[,)+โˆž)) โˆง (๐‘ž โˆˆ ๐ด โˆง ๐‘Ÿ โˆˆ ๐ต))) โ†’ ((๐นโ€˜๐‘ž) โ‰ค (๐นโ€˜(โ—ก๐นโ€˜๐‘˜)) โ†” (๐นโ€˜๐‘ž) โ‰ค ๐‘˜))
119117breq1d 5151 . . . . . . . . . . . . . 14 ((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง ((โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›) โˆง ๐‘˜ โˆˆ (0[,)+โˆž)) โˆง (๐‘ž โˆˆ ๐ด โˆง ๐‘Ÿ โˆˆ ๐ต))) โ†’ ((๐นโ€˜(โ—ก๐นโ€˜๐‘˜)) โ‰ค (๐นโ€˜๐‘Ÿ) โ†” ๐‘˜ โ‰ค (๐นโ€˜๐‘Ÿ)))
120118, 119anbi12d 630 . . . . . . . . . . . . 13 ((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง ((โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›) โˆง ๐‘˜ โˆˆ (0[,)+โˆž)) โˆง (๐‘ž โˆˆ ๐ด โˆง ๐‘Ÿ โˆˆ ๐ต))) โ†’ (((๐นโ€˜๐‘ž) โ‰ค (๐นโ€˜(โ—ก๐นโ€˜๐‘˜)) โˆง (๐นโ€˜(โ—ก๐นโ€˜๐‘˜)) โ‰ค (๐นโ€˜๐‘Ÿ)) โ†” ((๐นโ€˜๐‘ž) โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค (๐นโ€˜๐‘Ÿ))))
121115, 120mpbird 257 . . . . . . . . . . . 12 ((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง ((โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›) โˆง ๐‘˜ โˆˆ (0[,)+โˆž)) โˆง (๐‘ž โˆˆ ๐ด โˆง ๐‘Ÿ โˆˆ ๐ต))) โ†’ ((๐นโ€˜๐‘ž) โ‰ค (๐นโ€˜(โ—ก๐นโ€˜๐‘˜)) โˆง (๐นโ€˜(โ—ก๐นโ€˜๐‘˜)) โ‰ค (๐นโ€˜๐‘Ÿ)))
1228, 9axcontlem8 28737 . . . . . . . . . . . 12 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (๐‘ž โˆˆ ๐ท โˆง (โ—ก๐นโ€˜๐‘˜) โˆˆ ๐ท โˆง ๐‘Ÿ โˆˆ ๐ท)) โ†’ (((๐นโ€˜๐‘ž) โ‰ค (๐นโ€˜(โ—ก๐นโ€˜๐‘˜)) โˆง (๐นโ€˜(โ—ก๐นโ€˜๐‘˜)) โ‰ค (๐นโ€˜๐‘Ÿ)) โ†’ (โ—ก๐นโ€˜๐‘˜) Btwn โŸจ๐‘ž, ๐‘ŸโŸฉ))
12395, 121, 122sylc 65 . . . . . . . . . . 11 ((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง ((โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›) โˆง ๐‘˜ โˆˆ (0[,)+โˆž)) โˆง (๐‘ž โˆˆ ๐ด โˆง ๐‘Ÿ โˆˆ ๐ต))) โ†’ (โ—ก๐นโ€˜๐‘˜) Btwn โŸจ๐‘ž, ๐‘ŸโŸฉ)
124123anassrs 467 . . . . . . . . . 10 (((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง (โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›) โˆง ๐‘˜ โˆˆ (0[,)+โˆž))) โˆง (๐‘ž โˆˆ ๐ด โˆง ๐‘Ÿ โˆˆ ๐ต)) โ†’ (โ—ก๐นโ€˜๐‘˜) Btwn โŸจ๐‘ž, ๐‘ŸโŸฉ)
125124ralrimivva 3194 . . . . . . . . 9 ((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง (โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›) โˆง ๐‘˜ โˆˆ (0[,)+โˆž))) โ†’ โˆ€๐‘ž โˆˆ ๐ด โˆ€๐‘Ÿ โˆˆ ๐ต (โ—ก๐นโ€˜๐‘˜) Btwn โŸจ๐‘ž, ๐‘ŸโŸฉ)
126 opeq1 4868 . . . . . . . . . . 11 (๐‘ž = ๐‘ฅ โ†’ โŸจ๐‘ž, ๐‘ŸโŸฉ = โŸจ๐‘ฅ, ๐‘ŸโŸฉ)
127126breq2d 5153 . . . . . . . . . 10 (๐‘ž = ๐‘ฅ โ†’ ((โ—ก๐นโ€˜๐‘˜) Btwn โŸจ๐‘ž, ๐‘ŸโŸฉ โ†” (โ—ก๐นโ€˜๐‘˜) Btwn โŸจ๐‘ฅ, ๐‘ŸโŸฉ))
128 opeq2 4869 . . . . . . . . . . 11 (๐‘Ÿ = ๐‘ฆ โ†’ โŸจ๐‘ฅ, ๐‘ŸโŸฉ = โŸจ๐‘ฅ, ๐‘ฆโŸฉ)
129128breq2d 5153 . . . . . . . . . 10 (๐‘Ÿ = ๐‘ฆ โ†’ ((โ—ก๐นโ€˜๐‘˜) Btwn โŸจ๐‘ฅ, ๐‘ŸโŸฉ โ†” (โ—ก๐นโ€˜๐‘˜) Btwn โŸจ๐‘ฅ, ๐‘ฆโŸฉ))
130127, 129cbvral2vw 3232 . . . . . . . . 9 (โˆ€๐‘ž โˆˆ ๐ด โˆ€๐‘Ÿ โˆˆ ๐ต (โ—ก๐นโ€˜๐‘˜) Btwn โŸจ๐‘ž, ๐‘ŸโŸฉ โ†” โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต (โ—ก๐นโ€˜๐‘˜) Btwn โŸจ๐‘ฅ, ๐‘ฆโŸฉ)
131125, 130sylib 217 . . . . . . . 8 ((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง (โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›) โˆง ๐‘˜ โˆˆ (0[,)+โˆž))) โ†’ โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต (โ—ก๐นโ€˜๐‘˜) Btwn โŸจ๐‘ฅ, ๐‘ฆโŸฉ)
132 breq1 5144 . . . . . . . . . 10 (๐‘ = (โ—ก๐นโ€˜๐‘˜) โ†’ (๐‘ Btwn โŸจ๐‘ฅ, ๐‘ฆโŸฉ โ†” (โ—ก๐นโ€˜๐‘˜) Btwn โŸจ๐‘ฅ, ๐‘ฆโŸฉ))
1331322ralbidv 3212 . . . . . . . . 9 (๐‘ = (โ—ก๐นโ€˜๐‘˜) โ†’ (โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ Btwn โŸจ๐‘ฅ, ๐‘ฆโŸฉ โ†” โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต (โ—ก๐นโ€˜๐‘˜) Btwn โŸจ๐‘ฅ, ๐‘ฆโŸฉ))
134133rspcev 3606 . . . . . . . 8 (((โ—ก๐นโ€˜๐‘˜) โˆˆ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต (โ—ก๐นโ€˜๐‘˜) Btwn โŸจ๐‘ฅ, ๐‘ฆโŸฉ) โ†’ โˆƒ๐‘ โˆˆ (๐”ผโ€˜๐‘)โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ Btwn โŸจ๐‘ฅ, ๐‘ฆโŸฉ)
13582, 131, 134syl2anc 583 . . . . . . 7 ((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง (โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›) โˆง ๐‘˜ โˆˆ (0[,)+โˆž))) โ†’ โˆƒ๐‘ โˆˆ (๐”ผโ€˜๐‘)โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ Btwn โŸจ๐‘ฅ, ๐‘ฆโŸฉ)
136135expr 456 . . . . . 6 ((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›)) โ†’ (๐‘˜ โˆˆ (0[,)+โˆž) โ†’ โˆƒ๐‘ โˆˆ (๐”ผโ€˜๐‘)โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ Btwn โŸจ๐‘ฅ, ๐‘ฆโŸฉ))
13777, 136syld 47 . . . . 5 ((((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›)) โ†’ (๐‘˜ โˆˆ โ„ โ†’ โˆƒ๐‘ โˆˆ (๐”ผโ€˜๐‘)โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ Btwn โŸจ๐‘ฅ, ๐‘ฆโŸฉ))
138137ex 412 . . . 4 (((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ (โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›) โ†’ (๐‘˜ โˆˆ โ„ โ†’ โˆƒ๐‘ โˆˆ (๐”ผโ€˜๐‘)โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ Btwn โŸจ๐‘ฅ, ๐‘ฆโŸฉ)))
139138com23 86 . . 3 (((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ (๐‘˜ โˆˆ โ„ โ†’ (โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›) โ†’ โˆƒ๐‘ โˆˆ (๐”ผโ€˜๐‘)โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ Btwn โŸจ๐‘ฅ, ๐‘ฆโŸฉ)))
140139rexlimdv 3147 . 2 (((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ (โˆƒ๐‘˜ โˆˆ โ„ โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›) โ†’ โˆƒ๐‘ โˆˆ (๐”ผโ€˜๐‘)โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ Btwn โŸจ๐‘ฅ, ๐‘ฆโŸฉ))
14123, 140mpd 15 1 (((๐‘ โˆˆ โ„• โˆง (๐ด โІ (๐”ผโ€˜๐‘) โˆง ๐ต โІ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ โˆƒ๐‘ โˆˆ (๐”ผโ€˜๐‘)โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ Btwn โŸจ๐‘ฅ, ๐‘ฆโŸฉ)
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โ†” wb 205   โˆง wa 395   โˆจ wo 844   โˆง w3a 1084   = wceq 1533  โˆƒwex 1773   โˆˆ wcel 2098   โ‰  wne 2934  โˆ€wral 3055  โˆƒwrex 3064  {crab 3426   โІ wss 3943  โˆ…c0 4317  โŸจcop 4629   class class class wbr 5141  {copab 5203  โ—กccnv 5668  dom cdm 5669  ran crn 5670   โ€œ cima 5672  Fun wfun 6531  โŸถwf 6533  โ€“1-1โ†’wf1 6534  โ€“ontoโ†’wfo 6535  โ€“1-1-ontoโ†’wf1o 6536  โ€˜cfv 6537  (class class class)co 7405  โ„cr 11111  0cc0 11112  1c1 11113   + caddc 11115   ยท cmul 11117  +โˆžcpnf 11249   โ‰ค cle 11253   โˆ’ cmin 11448  โ„•cn 12216  [,)cico 13332  ...cfz 13490  ๐”ผcee 28654   Btwn cbtwn 28655
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 2163  ax-ext 2697  ax-sep 5292  ax-nul 5299  ax-pow 5356  ax-pr 5420  ax-un 7722  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189  ax-pre-sup 11190
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  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 2704  df-cleq 2718  df-clel 2804  df-nfc 2879  df-ne 2935  df-nel 3041  df-ral 3056  df-rex 3065  df-rmo 3370  df-reu 3371  df-rab 3427  df-v 3470  df-sbc 3773  df-csb 3889  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-pss 3962  df-nul 4318  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4903  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-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 6294  df-ord 6361  df-on 6362  df-lim 6363  df-suc 6364  df-iota 6489  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-om 7853  df-1st 7974  df-2nd 7975  df-frecs 8267  df-wrecs 8298  df-recs 8372  df-rdg 8411  df-er 8705  df-map 8824  df-en 8942  df-dom 8943  df-sdom 8944  df-pnf 11254  df-mnf 11255  df-xr 11256  df-ltxr 11257  df-le 11258  df-sub 11450  df-neg 11451  df-div 11876  df-nn 12217  df-z 12563  df-uz 12827  df-ico 13336  df-icc 13337  df-fz 13491  df-ee 28657  df-btwn 28658
This theorem is referenced by:  axcontlem11  28740
  Copyright terms: Public domain W3C validator