# Metamath Proof Explorer

## Theorem ttgelitv

Description: Betweenness for a subcomplex Hilbert space augmented with betweenness. (Contributed by Thierry Arnoux, 25-Mar-2019)

Ref Expression
Hypotheses ttgval.n ${⊢}{G}={to𝒢}_{\mathrm{Tarski}}\left({H}\right)$
ttgitvval.i ${⊢}{I}=\mathrm{Itv}\left({G}\right)$
ttgitvval.b ${⊢}{P}={\mathrm{Base}}_{{H}}$
ttgitvval.m
ttgitvval.s
ttgelitv.x ${⊢}{\phi }\to {X}\in {P}$
ttgelitv.y ${⊢}{\phi }\to {Y}\in {P}$
ttgelitv.h ${⊢}{\phi }\to {H}\in {V}$
ttgelitv.z ${⊢}{\phi }\to {Z}\in {P}$
Assertion ttgelitv

### Proof

Step Hyp Ref Expression
1 ttgval.n ${⊢}{G}={to𝒢}_{\mathrm{Tarski}}\left({H}\right)$
2 ttgitvval.i ${⊢}{I}=\mathrm{Itv}\left({G}\right)$
3 ttgitvval.b ${⊢}{P}={\mathrm{Base}}_{{H}}$
4 ttgitvval.m
5 ttgitvval.s
6 ttgelitv.x ${⊢}{\phi }\to {X}\in {P}$
7 ttgelitv.y ${⊢}{\phi }\to {Y}\in {P}$
8 ttgelitv.h ${⊢}{\phi }\to {H}\in {V}$
9 ttgelitv.z ${⊢}{\phi }\to {Z}\in {P}$
10 1 2 3 4 5 ttgitvval
11 8 6 7 10 syl3anc
12 11 eleq2d
13 oveq1
14 13 eqeq1d
15 14 rexbidv
16 15 elrab
17 12 16 syl6bb
18 9 17 mpbirand