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

Theorem axcontlem9 27970
Description: Lemma for axcont 27974. Given the separation assumption, all values of ๐น over ๐ด are less than or equal to all values of ๐น over ๐ต. (Contributed by Scott Fenton, 20-Jun-2013.)
Hypotheses
Ref Expression
axcontlem9.1 ๐ท = {๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆฃ (๐‘ˆ Btwn โŸจ๐‘, ๐‘โŸฉ โˆจ ๐‘ Btwn โŸจ๐‘, ๐‘ˆโŸฉ)}
axcontlem9.2 ๐น = {โŸจ๐‘ฅ, ๐‘กโŸฉ โˆฃ (๐‘ฅ โˆˆ ๐ท โˆง (๐‘ก โˆˆ (0[,)+โˆž) โˆง โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–)))))}
Assertion
Ref Expression
axcontlem9 (((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ โˆ€๐‘› โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘š โˆˆ (๐น โ€œ ๐ต)๐‘› โ‰ค ๐‘š)
Distinct variable groups:   ๐ด,๐‘š,๐‘›,๐‘,๐‘ฅ   ๐ต,๐‘š,๐‘›,๐‘,๐‘ฅ,๐‘ฆ   ๐‘ก,๐ท,๐‘ฅ   ๐‘–,๐น   ๐‘š,๐น   ๐‘ก,๐น   ๐‘–,๐‘,๐‘ก,๐‘ฅ,๐‘   ๐‘š,๐‘,๐‘›,๐‘   ๐‘ก,๐‘,๐‘ฅ   ๐‘ฆ,๐‘   ๐‘ˆ,๐‘–   ๐‘ˆ,๐‘š,๐‘›,๐‘   ๐‘ก,๐‘ˆ,๐‘ฅ   ๐‘ฆ,๐‘ˆ   ๐‘–,๐‘   ๐‘š,๐‘,๐‘›,๐‘   ๐‘ก,๐‘,๐‘ฅ   ๐‘ฆ,๐‘   ๐น,๐‘
Allowed substitution hints:   ๐ด(๐‘ฆ,๐‘ก,๐‘–)   ๐ต(๐‘ก,๐‘–)   ๐ท(๐‘ฆ,๐‘–,๐‘š,๐‘›,๐‘)   ๐น(๐‘ฅ,๐‘ฆ,๐‘›)

Proof of Theorem axcontlem9
Dummy variables ๐‘Ž ๐‘ are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpll 766 . . . . 5 (((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ ๐‘ โˆˆ โ„•)
2 simprl1 1219 . . . . 5 (((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ ๐‘ โˆˆ (๐”ผโ€˜๐‘))
3 simplr1 1216 . . . . . 6 (((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ ๐ด โŠ† (๐”ผโ€˜๐‘))
4 simprl2 1220 . . . . . 6 (((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ ๐‘ˆ โˆˆ ๐ด)
53, 4sseldd 3949 . . . . 5 (((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘))
6 simprr 772 . . . . 5 (((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ ๐‘ โ‰  ๐‘ˆ)
7 axcontlem9.1 . . . . . 6 ๐ท = {๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆฃ (๐‘ˆ Btwn โŸจ๐‘, ๐‘โŸฉ โˆจ ๐‘ Btwn โŸจ๐‘, ๐‘ˆโŸฉ)}
8 axcontlem9.2 . . . . . 6 ๐น = {โŸจ๐‘ฅ, ๐‘กโŸฉ โˆฃ (๐‘ฅ โˆˆ ๐ท โˆง (๐‘ก โˆˆ (0[,)+โˆž) โˆง โˆ€๐‘– โˆˆ (1...๐‘)(๐‘ฅโ€˜๐‘–) = (((1 โˆ’ ๐‘ก) ยท (๐‘โ€˜๐‘–)) + (๐‘ก ยท (๐‘ˆโ€˜๐‘–)))))}
97, 8axcontlem2 27963 . . . . 5 (((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โ†’ ๐น:๐ทโ€“1-1-ontoโ†’(0[,)+โˆž))
101, 2, 5, 6, 9syl31anc 1374 . . . 4 (((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ ๐น:๐ทโ€“1-1-ontoโ†’(0[,)+โˆž))
11 f1ofun 6790 . . . 4 (๐น:๐ทโ€“1-1-ontoโ†’(0[,)+โˆž) โ†’ Fun ๐น)
12 fvelima 6912 . . . . 5 ((Fun ๐น โˆง ๐‘› โˆˆ (๐น โ€œ ๐ด)) โ†’ โˆƒ๐‘Ž โˆˆ ๐ด (๐นโ€˜๐‘Ž) = ๐‘›)
1312ex 414 . . . 4 (Fun ๐น โ†’ (๐‘› โˆˆ (๐น โ€œ ๐ด) โ†’ โˆƒ๐‘Ž โˆˆ ๐ด (๐นโ€˜๐‘Ž) = ๐‘›))
1410, 11, 133syl 18 . . 3 (((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ (๐‘› โˆˆ (๐น โ€œ ๐ด) โ†’ โˆƒ๐‘Ž โˆˆ ๐ด (๐นโ€˜๐‘Ž) = ๐‘›))
15 fvelima 6912 . . . . 5 ((Fun ๐น โˆง ๐‘š โˆˆ (๐น โ€œ ๐ต)) โ†’ โˆƒ๐‘ โˆˆ ๐ต (๐นโ€˜๐‘) = ๐‘š)
1615ex 414 . . . 4 (Fun ๐น โ†’ (๐‘š โˆˆ (๐น โ€œ ๐ต) โ†’ โˆƒ๐‘ โˆˆ ๐ต (๐นโ€˜๐‘) = ๐‘š))
1710, 11, 163syl 18 . . 3 (((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ (๐‘š โˆˆ (๐น โ€œ ๐ต) โ†’ โˆƒ๐‘ โˆˆ ๐ต (๐นโ€˜๐‘) = ๐‘š))
18 reeanv 3216 . . . 4 (โˆƒ๐‘Ž โˆˆ ๐ด โˆƒ๐‘ โˆˆ ๐ต ((๐นโ€˜๐‘Ž) = ๐‘› โˆง (๐นโ€˜๐‘) = ๐‘š) โ†” (โˆƒ๐‘Ž โˆˆ ๐ด (๐นโ€˜๐‘Ž) = ๐‘› โˆง โˆƒ๐‘ โˆˆ ๐ต (๐นโ€˜๐‘) = ๐‘š))
19 simplr3 1218 . . . . . . . 8 (((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)
20 breq1 5112 . . . . . . . . 9 (๐‘ฅ = ๐‘Ž โ†’ (๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ โ†” ๐‘Ž Btwn โŸจ๐‘, ๐‘ฆโŸฉ))
21 opeq2 4835 . . . . . . . . . 10 (๐‘ฆ = ๐‘ โ†’ โŸจ๐‘, ๐‘ฆโŸฉ = โŸจ๐‘, ๐‘โŸฉ)
2221breq2d 5121 . . . . . . . . 9 (๐‘ฆ = ๐‘ โ†’ (๐‘Ž Btwn โŸจ๐‘, ๐‘ฆโŸฉ โ†” ๐‘Ž Btwn โŸจ๐‘, ๐‘โŸฉ))
2320, 22rspc2v 3592 . . . . . . . 8 ((๐‘Ž โˆˆ ๐ด โˆง ๐‘ โˆˆ ๐ต) โ†’ (โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ โ†’ ๐‘Ž Btwn โŸจ๐‘, ๐‘โŸฉ))
2419, 23mpan9 508 . . . . . . 7 ((((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง (๐‘Ž โˆˆ ๐ด โˆง ๐‘ โˆˆ ๐ต)) โ†’ ๐‘Ž Btwn โŸจ๐‘, ๐‘โŸฉ)
25 simplll 774 . . . . . . . . 9 ((((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง (๐‘Ž โˆˆ ๐ด โˆง ๐‘ โˆˆ ๐ต)) โ†’ ๐‘ โˆˆ โ„•)
262adantr 482 . . . . . . . . 9 ((((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง (๐‘Ž โˆˆ ๐ด โˆง ๐‘ โˆˆ ๐ต)) โ†’ ๐‘ โˆˆ (๐”ผโ€˜๐‘))
275adantr 482 . . . . . . . . 9 ((((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง (๐‘Ž โˆˆ ๐ด โˆง ๐‘ โˆˆ ๐ต)) โ†’ ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘))
2825, 26, 273jca 1129 . . . . . . . 8 ((((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง (๐‘Ž โˆˆ ๐ด โˆง ๐‘ โˆˆ ๐ต)) โ†’ (๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)))
29 simplrr 777 . . . . . . . 8 ((((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง (๐‘Ž โˆˆ ๐ด โˆง ๐‘ โˆˆ ๐ต)) โ†’ ๐‘ โ‰  ๐‘ˆ)
307axcontlem4 27965 . . . . . . . . . . 11 (((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ ๐ด โŠ† ๐ท)
3130sseld 3947 . . . . . . . . . 10 (((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ (๐‘Ž โˆˆ ๐ด โ†’ ๐‘Ž โˆˆ ๐ท))
32 simpl 484 . . . . . . . . . . . 12 (((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ (๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)))
337axcontlem3 27964 . . . . . . . . . . . 12 (((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง (๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ ๐ต โŠ† ๐ท)
3432, 2, 4, 6, 33syl13anc 1373 . . . . . . . . . . 11 (((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ ๐ต โŠ† ๐ท)
3534sseld 3947 . . . . . . . . . 10 (((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ (๐‘ โˆˆ ๐ต โ†’ ๐‘ โˆˆ ๐ท))
3631, 35anim12d 610 . . . . . . . . 9 (((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ ((๐‘Ž โˆˆ ๐ด โˆง ๐‘ โˆˆ ๐ต) โ†’ (๐‘Ž โˆˆ ๐ท โˆง ๐‘ โˆˆ ๐ท)))
3736imp 408 . . . . . . . 8 ((((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง (๐‘Ž โˆˆ ๐ด โˆง ๐‘ โˆˆ ๐ต)) โ†’ (๐‘Ž โˆˆ ๐ท โˆง ๐‘ โˆˆ ๐ท))
387, 8axcontlem7 27968 . . . . . . . 8 ((((๐‘ โˆˆ โ„• โˆง ๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ (๐”ผโ€˜๐‘)) โˆง ๐‘ โ‰  ๐‘ˆ) โˆง (๐‘Ž โˆˆ ๐ท โˆง ๐‘ โˆˆ ๐ท)) โ†’ (๐‘Ž Btwn โŸจ๐‘, ๐‘โŸฉ โ†” (๐นโ€˜๐‘Ž) โ‰ค (๐นโ€˜๐‘)))
3928, 29, 37, 38syl21anc 837 . . . . . . 7 ((((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง (๐‘Ž โˆˆ ๐ด โˆง ๐‘ โˆˆ ๐ต)) โ†’ (๐‘Ž Btwn โŸจ๐‘, ๐‘โŸฉ โ†” (๐นโ€˜๐‘Ž) โ‰ค (๐นโ€˜๐‘)))
4024, 39mpbid 231 . . . . . 6 ((((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง (๐‘Ž โˆˆ ๐ด โˆง ๐‘ โˆˆ ๐ต)) โ†’ (๐นโ€˜๐‘Ž) โ‰ค (๐นโ€˜๐‘))
41 breq12 5114 . . . . . 6 (((๐นโ€˜๐‘Ž) = ๐‘› โˆง (๐นโ€˜๐‘) = ๐‘š) โ†’ ((๐นโ€˜๐‘Ž) โ‰ค (๐นโ€˜๐‘) โ†” ๐‘› โ‰ค ๐‘š))
4240, 41syl5ibcom 244 . . . . 5 ((((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โˆง (๐‘Ž โˆˆ ๐ด โˆง ๐‘ โˆˆ ๐ต)) โ†’ (((๐นโ€˜๐‘Ž) = ๐‘› โˆง (๐นโ€˜๐‘) = ๐‘š) โ†’ ๐‘› โ‰ค ๐‘š))
4342rexlimdvva 3202 . . . 4 (((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ (โˆƒ๐‘Ž โˆˆ ๐ด โˆƒ๐‘ โˆˆ ๐ต ((๐นโ€˜๐‘Ž) = ๐‘› โˆง (๐นโ€˜๐‘) = ๐‘š) โ†’ ๐‘› โ‰ค ๐‘š))
4418, 43biimtrrid 242 . . 3 (((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ ((โˆƒ๐‘Ž โˆˆ ๐ด (๐นโ€˜๐‘Ž) = ๐‘› โˆง โˆƒ๐‘ โˆˆ ๐ต (๐นโ€˜๐‘) = ๐‘š) โ†’ ๐‘› โ‰ค ๐‘š))
4514, 17, 44syl2and 609 . 2 (((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ ((๐‘› โˆˆ (๐น โ€œ ๐ด) โˆง ๐‘š โˆˆ (๐น โ€œ ๐ต)) โ†’ ๐‘› โ‰ค ๐‘š))
4645ralrimivv 3192 1 (((๐‘ โˆˆ โ„• โˆง (๐ด โŠ† (๐”ผโ€˜๐‘) โˆง ๐ต โŠ† (๐”ผโ€˜๐‘) โˆง โˆ€๐‘ฅ โˆˆ ๐ด โˆ€๐‘ฆ โˆˆ ๐ต ๐‘ฅ Btwn โŸจ๐‘, ๐‘ฆโŸฉ)) โˆง ((๐‘ โˆˆ (๐”ผโ€˜๐‘) โˆง ๐‘ˆ โˆˆ ๐ด โˆง ๐ต โ‰  โˆ…) โˆง ๐‘ โ‰  ๐‘ˆ)) โ†’ โˆ€๐‘› โˆˆ (๐น โ€œ ๐ด)โˆ€๐‘š โˆˆ (๐น โ€œ ๐ต)๐‘› โ‰ค ๐‘š)
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โ†” wb 205   โˆง wa 397   โˆจ wo 846   โˆง w3a 1088   = wceq 1542   โˆˆ wcel 2107   โ‰  wne 2940  โˆ€wral 3061  โˆƒwrex 3070  {crab 3406   โŠ† wss 3914  โˆ…c0 4286  โŸจcop 4596   class class class wbr 5109  {copab 5171   โ€œ cima 5640  Fun wfun 6494  โ€“1-1-ontoโ†’wf1o 6499  โ€˜cfv 6500  (class class class)co 7361  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
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:  axcontlem10  27971
  Copyright terms: Public domain W3C validator