# Metamath Proof Explorer

## Theorem tgbtwndiff

Description: There is always a c distinct from B such that B lies between A and c . Theorem 3.14 of Schwabhauser p. 32. The condition "the space is of dimension 1 or more" is written here as 2 <_ ( #P ) for simplicity. (Contributed by Thierry Arnoux, 23-Mar-2019)

Ref Expression
Hypotheses tgbtwndiff.p ${⊢}{P}={\mathrm{Base}}_{{G}}$
tgbtwndiff.d
tgbtwndiff.i ${⊢}{I}=\mathrm{Itv}\left({G}\right)$
tgbtwndiff.g ${⊢}{\phi }\to {G}\in {𝒢}_{\mathrm{Tarski}}$
tgbtwndiff.a ${⊢}{\phi }\to {A}\in {P}$
tgbtwndiff.b ${⊢}{\phi }\to {B}\in {P}$
tgbtwndiff.l ${⊢}{\phi }\to 2\le \left|{P}\right|$
Assertion tgbtwndiff ${⊢}{\phi }\to \exists {c}\in {P}\phantom{\rule{.4em}{0ex}}\left({B}\in \left({A}{I}{c}\right)\wedge {B}\ne {c}\right)$

### Proof

Step Hyp Ref Expression
1 tgbtwndiff.p ${⊢}{P}={\mathrm{Base}}_{{G}}$
2 tgbtwndiff.d
3 tgbtwndiff.i ${⊢}{I}=\mathrm{Itv}\left({G}\right)$
4 tgbtwndiff.g ${⊢}{\phi }\to {G}\in {𝒢}_{\mathrm{Tarski}}$
5 tgbtwndiff.a ${⊢}{\phi }\to {A}\in {P}$
6 tgbtwndiff.b ${⊢}{\phi }\to {B}\in {P}$
7 tgbtwndiff.l ${⊢}{\phi }\to 2\le \left|{P}\right|$
8 4 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge {u}\in {P}\right)\wedge {v}\in {P}\right)\wedge {u}\ne {v}\right)\to {G}\in {𝒢}_{\mathrm{Tarski}}$
9 5 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge {u}\in {P}\right)\wedge {v}\in {P}\right)\wedge {u}\ne {v}\right)\to {A}\in {P}$
10 6 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge {u}\in {P}\right)\wedge {v}\in {P}\right)\wedge {u}\ne {v}\right)\to {B}\in {P}$
11 simpllr ${⊢}\left(\left(\left({\phi }\wedge {u}\in {P}\right)\wedge {v}\in {P}\right)\wedge {u}\ne {v}\right)\to {u}\in {P}$
12 simplr ${⊢}\left(\left(\left({\phi }\wedge {u}\in {P}\right)\wedge {v}\in {P}\right)\wedge {u}\ne {v}\right)\to {v}\in {P}$
13 1 2 3 8 9 10 11 12 axtgsegcon
18 simpr
19 18 oveq2d
20 simplr
21 19 20 eqtr2d
22 1 2 3 14 15 16 17 21 axtgcgrid
23 simp-4r
24 23 neneqd
25 22 24 pm2.65da
26 25 neqned
27 26 ex
28 27 anim2d
29 28 reximdva
30 13 29 mpd ${⊢}\left(\left(\left({\phi }\wedge {u}\in {P}\right)\wedge {v}\in {P}\right)\wedge {u}\ne {v}\right)\to \exists {c}\in {P}\phantom{\rule{.4em}{0ex}}\left({B}\in \left({A}{I}{c}\right)\wedge {B}\ne {c}\right)$
31 1 2 3 4 7 tglowdim1 ${⊢}{\phi }\to \exists {u}\in {P}\phantom{\rule{.4em}{0ex}}\exists {v}\in {P}\phantom{\rule{.4em}{0ex}}{u}\ne {v}$
32 30 31 r19.29vva ${⊢}{\phi }\to \exists {c}\in {P}\phantom{\rule{.4em}{0ex}}\left({B}\in \left({A}{I}{c}\right)\wedge {B}\ne {c}\right)$