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

Theorem axcontlem10 27971
Description: Lemma for axcont 27974. 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 6028 . . . . 5 (๐น โ€œ ๐ด) โŠ† ran ๐น
2 simpll 766 . . . . . . 7 (((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ ๐‘ โˆˆ โ„•)
3 simprl1 1219 . . . . . . 7 (((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ ๐‘ โˆˆ (๐”ผโ€˜๐‘))
4 simplr1 1216 . . . . . . . 8 (((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ ๐ด โŠ† (๐”ผโ€˜๐‘))
5 simprl2 1220 . . . . . . . 8 (((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ ๐‘ˆ โˆˆ ๐ด)
64, 5sseldd 3949 . . . . . . 7 (((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘))
7 simprr 772 . . . . . . 7 (((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ ๐‘ โ‰  ๐‘ˆ)
8 axcontlem10.1 . . . . . . . 8 ๐ท = {๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆฃ (๐‘ˆ Btwn โŸจ๐‘, ๐‘โŸฉ โˆจ ๐‘ Btwn โŸจ๐‘, ๐‘ˆโŸฉ)}
9 axcontlem10.2 . . . . . . . 8 ๐น = {โŸจ๐‘ฅ, ๐‘กโŸฉ โˆฃ (๐‘ฅ โˆˆ ๐ท โˆง (๐‘ก โˆˆ (0[,)+โˆž) โˆง โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–)))))}
108, 9axcontlem2 27963 . . . . . . 7 (((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โ†’ ๐น:๐ทโ€“1-1-ontoโ†’(0[,)+โˆž))
112, 3, 6, 7, 10syl31anc 1374 . . . . . 6 (((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ ๐น:๐ทโ€“1-1-ontoโ†’(0[,)+โˆž))
12 f1ofo 6795 . . . . . 6 (๐น:๐ทโ€“1-1-ontoโ†’(0[,)+โˆž) โ†’ ๐น:๐ทโ€“ontoโ†’(0[,)+โˆž))
13 forn 6763 . . . . . 6 (๐น:๐ทโ€“ontoโ†’(0[,)+โˆž) โ†’ ran ๐น = (0[,)+โˆž))
1411, 12, 133syl 18 . . . . 5 (((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ ran ๐น = (0[,)+โˆž))
151, 14sseqtrid 4000 . . . 4 (((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ (๐น โ€œ ๐ด) โŠ† (0[,)+โˆž))
16 rge0ssre 13382 . . . 4 (0[,)+โˆž) โŠ† โ„
1715, 16sstrdi 3960 . . 3 (((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ (๐น โ€œ ๐ด) โŠ† โ„)
18 imassrn 6028 . . . . 5 (๐น โ€œ ๐ต) โŠ† ran ๐น
1918, 14sseqtrid 4000 . . . 4 (((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ (๐น โ€œ ๐ต) โŠ† (0[,)+โˆž))
2019, 16sstrdi 3960 . . 3 (((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ (๐น โ€œ ๐ต) โŠ† โ„)
218, 9axcontlem9 27970 . . 3 (((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)๐‘š โ‰ค ๐‘›)
22 dedekindle 11327 . . 3 (((๐น โ€œ ๐ด) โŠ† โ„ โˆง (๐น โ€œ ๐ต) โŠ† โ„ โˆง โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)๐‘š โ‰ค ๐‘›) โ†’ โˆƒ๐‘˜ โˆˆ โ„ โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›))
2317, 20, 21, 22syl3anc 1372 . 2 (((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ โˆƒ๐‘˜ โˆˆ โ„ โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›))
24 simpr 486 . . . . . . . 8 (((((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›)) โˆง ๐‘˜ โˆˆ โ„) โ†’ ๐‘˜ โˆˆ โ„)
25 simprl3 1221 . . . . . . . . . . 11 (((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ ๐ต โ‰  โˆ…)
2625ad2antrr 725 . . . . . . . . . 10 (((((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›)) โˆง ๐‘˜ โˆˆ โ„) โ†’ ๐ต โ‰  โˆ…)
27 n0 4310 . . . . . . . . . 10 (๐ต โ‰  โˆ… โ†” โˆƒ๐‘ ๐‘ โˆˆ ๐ต)
2826, 27sylib 217 . . . . . . . . 9 (((((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›)) โˆง ๐‘˜ โˆˆ โ„) โ†’ โˆƒ๐‘ ๐‘ โˆˆ ๐ต)
29 0red 11166 . . . . . . . . . . . 12 (((((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›)) โˆง (๐‘˜ โˆˆ โ„ โˆง ๐‘ โˆˆ ๐ต)) โ†’ 0 โˆˆ โ„)
30 f1of 6788 . . . . . . . . . . . . . . . 16 (๐น:๐ทโ€“1-1-ontoโ†’(0[,)+โˆž) โ†’ ๐น:๐ทโŸถ(0[,)+โˆž))
3111, 30syl 17 . . . . . . . . . . . . . . 15 (((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ ๐น:๐ทโŸถ(0[,)+โˆž))
328axcontlem4 27965 . . . . . . . . . . . . . . . 16 (((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ ๐ด โŠ† ๐ท)
3332, 5sseldd 3949 . . . . . . . . . . . . . . 15 (((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ ๐‘ˆ โˆˆ ๐ท)
3431, 33ffvelcdmd 7040 . . . . . . . . . . . . . 14 (((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ (๐นโ€˜๐‘ˆ) โˆˆ (0[,)+โˆž))
3516, 34sselid 3946 . . . . . . . . . . . . 13 (((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ (๐นโ€˜๐‘ˆ) โˆˆ โ„)
3635ad2antrr 725 . . . . . . . . . . . 12 (((((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›)) โˆง (๐‘˜ โˆˆ โ„ โˆง ๐‘ โˆˆ ๐ต)) โ†’ (๐นโ€˜๐‘ˆ) โˆˆ โ„)
37 simprl 770 . . . . . . . . . . . 12 (((((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›)) โˆง (๐‘˜ โˆˆ โ„ โˆง ๐‘ โˆˆ ๐ต)) โ†’ ๐‘˜ โˆˆ โ„)
38 elrege0 13380 . . . . . . . . . . . . . . 15 ((๐นโ€˜๐‘ˆ) โˆˆ (0[,)+โˆž) โ†” ((๐นโ€˜๐‘ˆ) โˆˆ โ„ โˆง 0 โ‰ค (๐นโ€˜๐‘ˆ)))
3938simprbi 498 . . . . . . . . . . . . . 14 ((๐นโ€˜๐‘ˆ) โˆˆ (0[,)+โˆž) โ†’ 0 โ‰ค (๐นโ€˜๐‘ˆ))
4034, 39syl 17 . . . . . . . . . . . . 13 (((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ 0 โ‰ค (๐นโ€˜๐‘ˆ))
4140ad2antrr 725 . . . . . . . . . . . 12 (((((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›)) โˆง (๐‘˜ โˆˆ โ„ โˆง ๐‘ โˆˆ ๐ต)) โ†’ 0 โ‰ค (๐นโ€˜๐‘ˆ))
42 f1of1 6787 . . . . . . . . . . . . . . . . . . . 20 (๐น:๐ทโ€“1-1-ontoโ†’(0[,)+โˆž) โ†’ ๐น:๐ทโ€“1-1โ†’(0[,)+โˆž))
4311, 42syl 17 . . . . . . . . . . . . . . . . . . 19 (((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ ๐น:๐ทโ€“1-1โ†’(0[,)+โˆž))
44 f1elima 7214 . . . . . . . . . . . . . . . . . . 19 ((๐น:๐ทโ€“1-1โ†’(0[,)+โˆž) โˆง ๐‘ˆ โˆˆ ๐ท โˆง ๐ด โŠ† ๐ท) โ†’ ((๐นโ€˜๐‘ˆ) โˆˆ (๐น โ€œ ๐ด) โ†” ๐‘ˆ โˆˆ ๐ด))
4543, 33, 32, 44syl3anc 1372 . . . . . . . . . . . . . . . . . 18 (((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ ((๐นโ€˜๐‘ˆ) โˆˆ (๐น โ€œ ๐ด) โ†” ๐‘ˆ โˆˆ ๐ด))
465, 45mpbird 257 . . . . . . . . . . . . . . . . 17 (((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ (๐นโ€˜๐‘ˆ) โˆˆ (๐น โ€œ ๐ด))
4746adantr 482 . . . . . . . . . . . . . . . 16 ((((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง (๐‘˜ โˆˆ โ„ โˆง ๐‘ โˆˆ ๐ต)) โ†’ (๐นโ€˜๐‘ˆ) โˆˆ (๐น โ€œ ๐ด))
48 simpr 486 . . . . . . . . . . . . . . . . . 18 ((((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง ๐‘ โˆˆ ๐ต) โ†’ ๐‘ โˆˆ ๐ต)
4943adantr 482 . . . . . . . . . . . . . . . . . . 19 ((((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง ๐‘ โˆˆ ๐ต) โ†’ ๐น:๐ทโ€“1-1โ†’(0[,)+โˆž))
50 simpl1 1192 . . . . . . . . . . . . . . . . . . . . . 22 (((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ) โ†’ ๐‘ โˆˆ (๐”ผโ€˜๐‘))
51 simpl2 1193 . . . . . . . . . . . . . . . . . . . . . 22 (((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ) โ†’ ๐‘ˆ โˆˆ ๐ด)
52 simpr 486 . . . . . . . . . . . . . . . . . . . . . 22 (((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ) โ†’ ๐‘ โ‰  ๐‘ˆ)
5350, 51, 523jca 1129 . . . . . . . . . . . . . . . . . . . . 21 (((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ) โ†’ (๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐‘ โ‰  ๐‘ˆ))
548axcontlem3 27964 . . . . . . . . . . . . . . . . . . . . 21 (((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง (๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ ๐ต โŠ† ๐ท)
5553, 54sylan2 594 . . . . . . . . . . . . . . . . . . . 20 (((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ ๐ต โŠ† ๐ท)
5655sselda 3948 . . . . . . . . . . . . . . . . . . 19 ((((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง ๐‘ โˆˆ ๐ต) โ†’ ๐‘ โˆˆ ๐ท)
5755adantr 482 . . . . . . . . . . . . . . . . . . 19 ((((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง ๐‘ โˆˆ ๐ต) โ†’ ๐ต โŠ† ๐ท)
58 f1elima 7214 . . . . . . . . . . . . . . . . . . 19 ((๐น:๐ทโ€“1-1โ†’(0[,)+โˆž) โˆง ๐‘ โˆˆ ๐ท โˆง ๐ต โŠ† ๐ท) โ†’ ((๐นโ€˜๐‘) โˆˆ (๐น โ€œ ๐ต) โ†” ๐‘ โˆˆ ๐ต))
5949, 56, 57, 58syl3anc 1372 . . . . . . . . . . . . . . . . . 18 ((((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง ๐‘ โˆˆ ๐ต) โ†’ ((๐นโ€˜๐‘) โˆˆ (๐น โ€œ ๐ต) โ†” ๐‘ โˆˆ ๐ต))
6048, 59mpbird 257 . . . . . . . . . . . . . . . . 17 ((((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง ๐‘ โˆˆ ๐ต) โ†’ (๐นโ€˜๐‘) โˆˆ (๐น โ€œ ๐ต))
6160adantrl 715 . . . . . . . . . . . . . . . 16 ((((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง (๐‘˜ โˆˆ โ„ โˆง ๐‘ โˆˆ ๐ต)) โ†’ (๐นโ€˜๐‘) โˆˆ (๐น โ€œ ๐ต))
6247, 61jca 513 . . . . . . . . . . . . . . 15 ((((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง (๐‘˜ โˆˆ โ„ โˆง ๐‘ โˆˆ ๐ต)) โ†’ ((๐นโ€˜๐‘ˆ) โˆˆ (๐น โ€œ ๐ด) โˆง (๐นโ€˜๐‘) โˆˆ (๐น โ€œ ๐ต)))
63 breq1 5112 . . . . . . . . . . . . . . . . 17 (๐‘š = (๐นโ€˜๐‘ˆ) โ†’ (๐‘š โ‰ค ๐‘˜ โ†” (๐นโ€˜๐‘ˆ) โ‰ค ๐‘˜))
6463anbi1d 631 . . . . . . . . . . . . . . . 16 (๐‘š = (๐นโ€˜๐‘ˆ) โ†’ ((๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›) โ†” ((๐นโ€˜๐‘ˆ) โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›)))
65 breq2 5113 . . . . . . . . . . . . . . . . 17 (๐‘› = (๐นโ€˜๐‘) โ†’ (๐‘˜ โ‰ค ๐‘› โ†” ๐‘˜ โ‰ค (๐นโ€˜๐‘)))
6665anbi2d 630 . . . . . . . . . . . . . . . 16 (๐‘› = (๐นโ€˜๐‘) โ†’ (((๐นโ€˜๐‘ˆ) โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›) โ†” ((๐นโ€˜๐‘ˆ) โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค (๐นโ€˜๐‘))))
6764, 66rspc2va 3593 . . . . . . . . . . . . . . 15 ((((๐นโ€˜๐‘ˆ) โˆˆ (๐น โ€œ ๐ด) โˆง (๐นโ€˜๐‘) โˆˆ (๐น โ€œ ๐ต)) โˆง โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›)) โ†’ ((๐นโ€˜๐‘ˆ) โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค (๐นโ€˜๐‘)))
6862, 67sylan 581 . . . . . . . . . . . . . 14 (((((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง (๐‘˜ โˆˆ โ„ โˆง ๐‘ โˆˆ ๐ต)) โˆง โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›)) โ†’ ((๐นโ€˜๐‘ˆ) โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค (๐นโ€˜๐‘)))
6968an32s 651 . . . . . . . . . . . . 13 (((((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›)) โˆง (๐‘˜ โˆˆ โ„ โˆง ๐‘ โˆˆ ๐ต)) โ†’ ((๐นโ€˜๐‘ˆ) โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค (๐นโ€˜๐‘)))
7069simpld 496 . . . . . . . . . . . 12 (((((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›)) โˆง (๐‘˜ โˆˆ โ„ โˆง ๐‘ โˆˆ ๐ต)) โ†’ (๐นโ€˜๐‘ˆ) โ‰ค ๐‘˜)
7129, 36, 37, 41, 70letrd 11320 . . . . . . . . . . 11 (((((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›)) โˆง (๐‘˜ โˆˆ โ„ โˆง ๐‘ โˆˆ ๐ต)) โ†’ 0 โ‰ค ๐‘˜)
7271expr 458 . . . . . . . . . 10 (((((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›)) โˆง ๐‘˜ โˆˆ โ„) โ†’ (๐‘ โˆˆ ๐ต โ†’ 0 โ‰ค ๐‘˜))
7372exlimdv 1937 . . . . . . . . 9 (((((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›)) โˆง ๐‘˜ โˆˆ โ„) โ†’ (โˆƒ๐‘ ๐‘ โˆˆ ๐ต โ†’ 0 โ‰ค ๐‘˜))
7428, 73mpd 15 . . . . . . . 8 (((((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›)) โˆง ๐‘˜ โˆˆ โ„) โ†’ 0 โ‰ค ๐‘˜)
75 elrege0 13380 . . . . . . . 8 (๐‘˜ โˆˆ (0[,)+โˆž) โ†” (๐‘˜ โˆˆ โ„ โˆง 0 โ‰ค ๐‘˜))
7624, 74, 75sylanbrc 584 . . . . . . 7 (((((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›)) โˆง ๐‘˜ โˆˆ โ„) โ†’ ๐‘˜ โˆˆ (0[,)+โˆž))
7776ex 414 . . . . . 6 ((((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›)) โ†’ (๐‘˜ โˆˆ โ„ โ†’ ๐‘˜ โˆˆ (0[,)+โˆž)))
788ssrab3 4044 . . . . . . . . 9 ๐ท โŠ† (๐”ผโ€˜๐‘)
79 simpr 486 . . . . . . . . . 10 ((โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›) โˆง ๐‘˜ โˆˆ (0[,)+โˆž)) โ†’ ๐‘˜ โˆˆ (0[,)+โˆž))
80 f1ocnvdm 7235 . . . . . . . . . 10 ((๐น:๐ทโ€“1-1-ontoโ†’(0[,)+โˆž) โˆง ๐‘˜ โˆˆ (0[,)+โˆž)) โ†’ (โ—ก๐นโ€˜๐‘˜) โˆˆ ๐ท)
8111, 79, 80syl2an 597 . . . . . . . . 9 ((((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง (โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›) โˆง ๐‘˜ โˆˆ (0[,)+โˆž))) โ†’ (โ—ก๐นโ€˜๐‘˜) โˆˆ ๐ท)
8278, 81sselid 3946 . . . . . . . 8 ((((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง (โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›) โˆง ๐‘˜ โˆˆ (0[,)+โˆž))) โ†’ (โ—ก๐นโ€˜๐‘˜) โˆˆ (๐”ผโ€˜๐‘))
832, 3, 63jca 1129 . . . . . . . . . . . . . . 15 (((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ (๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)))
8483, 7jca 513 . . . . . . . . . . . . . 14 (((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ ((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ))
8584adantr 482 . . . . . . . . . . . . 13 ((((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง ((โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›) โˆง ๐‘˜ โˆˆ (0[,)+โˆž)) โˆง (๐‘ž โˆˆ ๐ด โˆง ๐‘Ÿ โˆˆ ๐ต))) โ†’ ((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ))
8632sselda 3948 . . . . . . . . . . . . . . . 16 ((((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง ๐‘ž โˆˆ ๐ด) โ†’ ๐‘ž โˆˆ ๐ท)
8786adantrr 716 . . . . . . . . . . . . . . 15 ((((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง (๐‘ž โˆˆ ๐ด โˆง ๐‘Ÿ โˆˆ ๐ต)) โ†’ ๐‘ž โˆˆ ๐ท)
8887adantrl 715 . . . . . . . . . . . . . 14 ((((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง ((โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›) โˆง ๐‘˜ โˆˆ (0[,)+โˆž)) โˆง (๐‘ž โˆˆ ๐ด โˆง ๐‘Ÿ โˆˆ ๐ต))) โ†’ ๐‘ž โˆˆ ๐ท)
89 simplr 768 . . . . . . . . . . . . . . 15 (((โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›) โˆง ๐‘˜ โˆˆ (0[,)+โˆž)) โˆง (๐‘ž โˆˆ ๐ด โˆง ๐‘Ÿ โˆˆ ๐ต)) โ†’ ๐‘˜ โˆˆ (0[,)+โˆž))
9011, 89, 80syl2an 597 . . . . . . . . . . . . . 14 ((((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง ((โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›) โˆง ๐‘˜ โˆˆ (0[,)+โˆž)) โˆง (๐‘ž โˆˆ ๐ด โˆง ๐‘Ÿ โˆˆ ๐ต))) โ†’ (โ—ก๐นโ€˜๐‘˜) โˆˆ ๐ท)
9155sselda 3948 . . . . . . . . . . . . . . . 16 ((((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง ๐‘Ÿ โˆˆ ๐ต) โ†’ ๐‘Ÿ โˆˆ ๐ท)
9291adantrl 715 . . . . . . . . . . . . . . 15 ((((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง (๐‘ž โˆˆ ๐ด โˆง ๐‘Ÿ โˆˆ ๐ต)) โ†’ ๐‘Ÿ โˆˆ ๐ท)
9392adantrl 715 . . . . . . . . . . . . . 14 ((((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง ((โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›) โˆง ๐‘˜ โˆˆ (0[,)+โˆž)) โˆง (๐‘ž โˆˆ ๐ด โˆง ๐‘Ÿ โˆˆ ๐ต))) โ†’ ๐‘Ÿ โˆˆ ๐ท)
9488, 90, 933jca 1129 . . . . . . . . . . . . 13 ((((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง ((โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›) โˆง ๐‘˜ โˆˆ (0[,)+โˆž)) โˆง (๐‘ž โˆˆ ๐ด โˆง ๐‘Ÿ โˆˆ ๐ต))) โ†’ (๐‘ž โˆˆ ๐ท โˆง (โ—ก๐นโ€˜๐‘˜) โˆˆ ๐ท โˆง ๐‘Ÿ โˆˆ ๐ท))
9585, 94jca 513 . . . . . . . . . . . 12 ((((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง ((โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›) โˆง ๐‘˜ โˆˆ (0[,)+โˆž)) โˆง (๐‘ž โˆˆ ๐ด โˆง ๐‘Ÿ โˆˆ ๐ต))) โ†’ (((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (๐‘ž โˆˆ ๐ท โˆง (โ—ก๐นโ€˜๐‘˜) โˆˆ ๐ท โˆง ๐‘Ÿ โˆˆ ๐ท)))
96 f1ofun 6790 . . . . . . . . . . . . . . . . . . 19 (๐น:๐ทโ€“1-1-ontoโ†’(0[,)+โˆž) โ†’ Fun ๐น)
9711, 96syl 17 . . . . . . . . . . . . . . . . . 18 (((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ Fun ๐น)
98 fdm 6681 . . . . . . . . . . . . . . . . . . . 20 (๐น:๐ทโŸถ(0[,)+โˆž) โ†’ dom ๐น = ๐ท)
9911, 30, 983syl 18 . . . . . . . . . . . . . . . . . . 19 (((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ dom ๐น = ๐ท)
10032, 99sseqtrrd 3989 . . . . . . . . . . . . . . . . . 18 (((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ ๐ด โŠ† dom ๐น)
101 funfvima2 7185 . . . . . . . . . . . . . . . . . 18 ((Fun ๐น โˆง ๐ด โŠ† dom ๐น) โ†’ (๐‘ž โˆˆ ๐ด โ†’ (๐นโ€˜๐‘ž) โˆˆ (๐น โ€œ ๐ด)))
10297, 100, 101syl2anc 585 . . . . . . . . . . . . . . . . 17 (((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ (๐‘ž โˆˆ ๐ด โ†’ (๐นโ€˜๐‘ž) โˆˆ (๐น โ€œ ๐ด)))
10355, 99sseqtrrd 3989 . . . . . . . . . . . . . . . . . 18 (((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ ๐ต โŠ† dom ๐น)
104 funfvima2 7185 . . . . . . . . . . . . . . . . . 18 ((Fun ๐น โˆง ๐ต โŠ† dom ๐น) โ†’ (๐‘Ÿ โˆˆ ๐ต โ†’ (๐นโ€˜๐‘Ÿ) โˆˆ (๐น โ€œ ๐ต)))
10597, 103, 104syl2anc 585 . . . . . . . . . . . . . . . . 17 (((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ (๐‘Ÿ โˆˆ ๐ต โ†’ (๐นโ€˜๐‘Ÿ) โˆˆ (๐น โ€œ ๐ต)))
106102, 105anim12d 610 . . . . . . . . . . . . . . . 16 (((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ ((๐‘ž โˆˆ ๐ด โˆง ๐‘Ÿ โˆˆ ๐ต) โ†’ ((๐นโ€˜๐‘ž) โˆˆ (๐น โ€œ ๐ด) โˆง (๐นโ€˜๐‘Ÿ) โˆˆ (๐น โ€œ ๐ต))))
107106imp 408 . . . . . . . . . . . . . . 15 ((((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง (๐‘ž โˆˆ ๐ด โˆง ๐‘Ÿ โˆˆ ๐ต)) โ†’ ((๐นโ€˜๐‘ž) โˆˆ (๐น โ€œ ๐ด) โˆง (๐นโ€˜๐‘Ÿ) โˆˆ (๐น โ€œ ๐ต)))
108107adantrl 715 . . . . . . . . . . . . . 14 ((((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง ((โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›) โˆง ๐‘˜ โˆˆ (0[,)+โˆž)) โˆง (๐‘ž โˆˆ ๐ด โˆง ๐‘Ÿ โˆˆ ๐ต))) โ†’ ((๐นโ€˜๐‘ž) โˆˆ (๐น โ€œ ๐ด) โˆง (๐นโ€˜๐‘Ÿ) โˆˆ (๐น โ€œ ๐ต)))
109 simprll 778 . . . . . . . . . . . . . 14 ((((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง ((โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›) โˆง ๐‘˜ โˆˆ (0[,)+โˆž)) โˆง (๐‘ž โˆˆ ๐ด โˆง ๐‘Ÿ โˆˆ ๐ต))) โ†’ โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›))
110 breq1 5112 . . . . . . . . . . . . . . . 16 (๐‘š = (๐นโ€˜๐‘ž) โ†’ (๐‘š โ‰ค ๐‘˜ โ†” (๐นโ€˜๐‘ž) โ‰ค ๐‘˜))
111110anbi1d 631 . . . . . . . . . . . . . . 15 (๐‘š = (๐นโ€˜๐‘ž) โ†’ ((๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›) โ†” ((๐นโ€˜๐‘ž) โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›)))
112 breq2 5113 . . . . . . . . . . . . . . . 16 (๐‘› = (๐นโ€˜๐‘Ÿ) โ†’ (๐‘˜ โ‰ค ๐‘› โ†” ๐‘˜ โ‰ค (๐นโ€˜๐‘Ÿ)))
113112anbi2d 630 . . . . . . . . . . . . . . 15 (๐‘› = (๐นโ€˜๐‘Ÿ) โ†’ (((๐นโ€˜๐‘ž) โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›) โ†” ((๐นโ€˜๐‘ž) โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค (๐นโ€˜๐‘Ÿ))))
114111, 113rspc2v 3592 . . . . . . . . . . . . . 14 (((๐นโ€˜๐‘ž) โˆˆ (๐น โ€œ ๐ด) โˆง (๐นโ€˜๐‘Ÿ) โˆˆ (๐น โ€œ ๐ต)) โ†’ (โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›) โ†’ ((๐นโ€˜๐‘ž) โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค (๐นโ€˜๐‘Ÿ))))
115108, 109, 114sylc 65 . . . . . . . . . . . . 13 ((((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง ((โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›) โˆง ๐‘˜ โˆˆ (0[,)+โˆž)) โˆง (๐‘ž โˆˆ ๐ด โˆง ๐‘Ÿ โˆˆ ๐ต))) โ†’ ((๐นโ€˜๐‘ž) โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค (๐นโ€˜๐‘Ÿ)))
116 f1ocnvfv2 7227 . . . . . . . . . . . . . . . 16 ((๐น:๐ทโ€“1-1-ontoโ†’(0[,)+โˆž) โˆง ๐‘˜ โˆˆ (0[,)+โˆž)) โ†’ (๐นโ€˜(โ—ก๐นโ€˜๐‘˜)) = ๐‘˜)
11711, 89, 116syl2an 597 . . . . . . . . . . . . . . 15 ((((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง ((โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›) โˆง ๐‘˜ โˆˆ (0[,)+โˆž)) โˆง (๐‘ž โˆˆ ๐ด โˆง ๐‘Ÿ โˆˆ ๐ต))) โ†’ (๐นโ€˜(โ—ก๐นโ€˜๐‘˜)) = ๐‘˜)
118117breq2d 5121 . . . . . . . . . . . . . 14 ((((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง ((โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›) โˆง ๐‘˜ โˆˆ (0[,)+โˆž)) โˆง (๐‘ž โˆˆ ๐ด โˆง ๐‘Ÿ โˆˆ ๐ต))) โ†’ ((๐นโ€˜๐‘ž) โ‰ค (๐นโ€˜(โ—ก๐นโ€˜๐‘˜)) โ†” (๐นโ€˜๐‘ž) โ‰ค ๐‘˜))
119117breq1d 5119 . . . . . . . . . . . . . 14 ((((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง ((โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›) โˆง ๐‘˜ โˆˆ (0[,)+โˆž)) โˆง (๐‘ž โˆˆ ๐ด โˆง ๐‘Ÿ โˆˆ ๐ต))) โ†’ ((๐นโ€˜(โ—ก๐นโ€˜๐‘˜)) โ‰ค (๐นโ€˜๐‘Ÿ) โ†” ๐‘˜ โ‰ค (๐นโ€˜๐‘Ÿ)))
120118, 119anbi12d 632 . . . . . . . . . . . . 13 ((((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง ((โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›) โˆง ๐‘˜ โˆˆ (0[,)+โˆž)) โˆง (๐‘ž โˆˆ ๐ด โˆง ๐‘Ÿ โˆˆ ๐ต))) โ†’ (((๐นโ€˜๐‘ž) โ‰ค (๐นโ€˜(โ—ก๐นโ€˜๐‘˜)) โˆง (๐นโ€˜(โ—ก๐นโ€˜๐‘˜)) โ‰ค (๐นโ€˜๐‘Ÿ)) โ†” ((๐นโ€˜๐‘ž) โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค (๐นโ€˜๐‘Ÿ))))
121115, 120mpbird 257 . . . . . . . . . . . 12 ((((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง ((โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›) โˆง ๐‘˜ โˆˆ (0[,)+โˆž)) โˆง (๐‘ž โˆˆ ๐ด โˆง ๐‘Ÿ โˆˆ ๐ต))) โ†’ ((๐นโ€˜๐‘ž) โ‰ค (๐นโ€˜(โ—ก๐นโ€˜๐‘˜)) โˆง (๐นโ€˜(โ—ก๐นโ€˜๐‘˜)) โ‰ค (๐นโ€˜๐‘Ÿ)))
1228, 9axcontlem8 27969 . . . . . . . . . . . 12 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (๐‘ž โˆˆ ๐ท โˆง (โ—ก๐นโ€˜๐‘˜) โˆˆ ๐ท โˆง ๐‘Ÿ โˆˆ ๐ท)) โ†’ (((๐นโ€˜๐‘ž) โ‰ค (๐นโ€˜(โ—ก๐นโ€˜๐‘˜)) โˆง (๐นโ€˜(โ—ก๐นโ€˜๐‘˜)) โ‰ค (๐นโ€˜๐‘Ÿ)) โ†’ (โ—ก๐นโ€˜๐‘˜) Btwn โŸจ๐‘ž, ๐‘ŸโŸฉ))
12395, 121, 122sylc 65 . . . . . . . . . . 11 ((((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง ((โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›) โˆง ๐‘˜ โˆˆ (0[,)+โˆž)) โˆง (๐‘ž โˆˆ ๐ด โˆง ๐‘Ÿ โˆˆ ๐ต))) โ†’ (โ—ก๐นโ€˜๐‘˜) Btwn โŸจ๐‘ž, ๐‘ŸโŸฉ)
124123anassrs 469 . . . . . . . . . 10 (((((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง (โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›) โˆง ๐‘˜ โˆˆ (0[,)+โˆž))) โˆง (๐‘ž โˆˆ ๐ด โˆง ๐‘Ÿ โˆˆ ๐ต)) โ†’ (โ—ก๐นโ€˜๐‘˜) Btwn โŸจ๐‘ž, ๐‘ŸโŸฉ)
125124ralrimivva 3194 . . . . . . . . 9 ((((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง (โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›) โˆง ๐‘˜ โˆˆ (0[,)+โˆž))) โ†’ โˆ€๐‘ž โˆˆ ๐ด โˆ€๐‘Ÿ โˆˆ ๐ต (โ—ก๐นโ€˜๐‘˜) Btwn โŸจ๐‘ž, ๐‘ŸโŸฉ)
126 opeq1 4834 . . . . . . . . . . 11 (๐‘ž = ๐‘ฅ โ†’ โŸจ๐‘ž, ๐‘ŸโŸฉ = โŸจ๐‘ฅ, ๐‘ŸโŸฉ)
127126breq2d 5121 . . . . . . . . . 10 (๐‘ž = ๐‘ฅ โ†’ ((โ—ก๐นโ€˜๐‘˜) Btwn โŸจ๐‘ž, ๐‘ŸโŸฉ โ†” (โ—ก๐นโ€˜๐‘˜) Btwn โŸจ๐‘ฅ, ๐‘ŸโŸฉ))
128 opeq2 4835 . . . . . . . . . . 11 (๐‘Ÿ = ๐‘ฆ โ†’ โŸจ๐‘ฅ, ๐‘ŸโŸฉ = โŸจ๐‘ฅ, ๐‘ฆโŸฉ)
129128breq2d 5121 . . . . . . . . . 10 (๐‘Ÿ = ๐‘ฆ โ†’ ((โ—ก๐นโ€˜๐‘˜) Btwn โŸจ๐‘ฅ, ๐‘ŸโŸฉ โ†” (โ—ก๐นโ€˜๐‘˜) Btwn โŸจ๐‘ฅ, ๐‘ฆโŸฉ))
130127, 129cbvral2vw 3226 . . . . . . . . 9 (โˆ€๐‘ž โˆˆ ๐ด โˆ€๐‘Ÿ โˆˆ ๐ต (โ—ก๐นโ€˜๐‘˜) Btwn โŸจ๐‘ž, ๐‘ŸโŸฉ โ†” โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต (โ—ก๐นโ€˜๐‘˜) Btwn โŸจ๐‘ฅ, ๐‘ฆโŸฉ)
131125, 130sylib 217 . . . . . . . 8 ((((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง (โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›) โˆง ๐‘˜ โˆˆ (0[,)+โˆž))) โ†’ โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต (โ—ก๐นโ€˜๐‘˜) Btwn โŸจ๐‘ฅ, ๐‘ฆโŸฉ)
132 breq1 5112 . . . . . . . . . 10 (๐‘ = (โ—ก๐นโ€˜๐‘˜) โ†’ (๐‘ Btwn โŸจ๐‘ฅ, ๐‘ฆโŸฉ โ†” (โ—ก๐นโ€˜๐‘˜) Btwn โŸจ๐‘ฅ, ๐‘ฆโŸฉ))
1331322ralbidv 3209 . . . . . . . . 9 (๐‘ = (โ—ก๐นโ€˜๐‘˜) โ†’ (โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ Btwn โŸจ๐‘ฅ, ๐‘ฆโŸฉ โ†” โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต (โ—ก๐นโ€˜๐‘˜) Btwn โŸจ๐‘ฅ, ๐‘ฆโŸฉ))
134133rspcev 3583 . . . . . . . 8 (((โ—ก๐นโ€˜๐‘˜) โˆˆ (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต (โ—ก๐นโ€˜๐‘˜) Btwn โŸจ๐‘ฅ, ๐‘ฆโŸฉ) โ†’ โˆƒ๐‘ โˆˆ (๐”ผโ€˜๐‘)โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ Btwn โŸจ๐‘ฅ, ๐‘ฆโŸฉ)
13582, 131, 134syl2anc 585 . . . . . . 7 ((((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง (โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›) โˆง ๐‘˜ โˆˆ (0[,)+โˆž))) โ†’ โˆƒ๐‘ โˆˆ (๐”ผโ€˜๐‘)โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ Btwn โŸจ๐‘ฅ, ๐‘ฆโŸฉ)
136135expr 458 . . . . . 6 ((((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›)) โ†’ (๐‘˜ โˆˆ (0[,)+โˆž) โ†’ โˆƒ๐‘ โˆˆ (๐”ผโ€˜๐‘)โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ Btwn โŸจ๐‘ฅ, ๐‘ฆโŸฉ))
13777, 136syld 47 . . . . 5 ((((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง โˆ€๐‘š โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘› โˆˆ (๐น โ€œ ๐ต)(๐‘š โ‰ค ๐‘˜ โˆง ๐‘˜ โ‰ค ๐‘›)) โ†’ (๐‘˜ โˆˆ โ„ โ†’ โˆƒ๐‘ โˆˆ (๐”ผโ€˜๐‘)โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ Btwn โŸจ๐‘ฅ, ๐‘ฆโŸฉ))
138137ex 414 . . . 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 397   โˆจ wo 846   โˆง w3a 1088   = wceq 1542  โˆƒwex 1782   โˆˆ wcel 2107   โ‰  wne 2940  โˆ€wral 3061  โˆƒwrex 3070  {crab 3406   โŠ† wss 3914  โˆ…c0 4286  โŸจcop 4596   class class class wbr 5109  {copab 5171  โ—กccnv 5636  dom cdm 5637  ran crn 5638   โ€œ cima 5640  Fun wfun 6494  โŸถwf 6496  โ€“1-1โ†’wf1 6497  โ€“ontoโ†’wfo 6498  โ€“1-1-ontoโ†’wf1o 6499  โ€˜cfv 6500  (class class class)co 7361  โ„cr 11058  0cc0 11059  1c1 11060   + caddc 11062   ยท cmul 11064  +โˆžcpnf 11194   โ‰ค cle 11198   โˆ’ cmin 11393  โ„•cn 12161  [,)cico 13275  ...cfz 13433  ๐”ผcee 27886   Btwn cbtwn 27887
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5260  ax-nul 5267  ax-pow 5324  ax-pr 5388  ax-un 7676  ax-cnex 11115  ax-resscn 11116  ax-1cn 11117  ax-icn 11118  ax-addcl 11119  ax-addrcl 11120  ax-mulcl 11121  ax-mulrcl 11122  ax-mulcom 11123  ax-addass 11124  ax-mulass 11125  ax-distr 11126  ax-i2m1 11127  ax-1ne0 11128  ax-1rid 11129  ax-rnegex 11130  ax-rrecex 11131  ax-cnre 11132  ax-pre-lttri 11133  ax-pre-lttrn 11134  ax-pre-ltadd 11135  ax-pre-mulgt0 11136  ax-pre-sup 11137
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3352  df-reu 3353  df-rab 3407  df-v 3449  df-sbc 3744  df-csb 3860  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3933  df-nul 4287  df-if 4491  df-pw 4566  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4870  df-iun 4960  df-br 5110  df-opab 5172  df-mpt 5193  df-tr 5227  df-id 5535  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5592  df-we 5594  df-xp 5643  df-rel 5644  df-cnv 5645  df-co 5646  df-dm 5647  df-rn 5648  df-res 5649  df-ima 5650  df-pred 6257  df-ord 6324  df-on 6325  df-lim 6326  df-suc 6327  df-iota 6452  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-riota 7317  df-ov 7364  df-oprab 7365  df-mpo 7366  df-om 7807  df-1st 7925  df-2nd 7926  df-frecs 8216  df-wrecs 8247  df-recs 8321  df-rdg 8360  df-er 8654  df-map 8773  df-en 8890  df-dom 8891  df-sdom 8892  df-pnf 11199  df-mnf 11200  df-xr 11201  df-ltxr 11202  df-le 11203  df-sub 11395  df-neg 11396  df-div 11821  df-nn 12162  df-z 12508  df-uz 12772  df-ico 13279  df-icc 13280  df-fz 13434  df-ee 27889  df-btwn 27890
This theorem is referenced by:  axcontlem11  27972
  Copyright terms: Public domain W3C validator