Metamath Proof Explorer

Theorem istrkgb

Description: Property of being a Tarski geometry - betweenness part. (Contributed by Thierry Arnoux, 14-Mar-2019)

Ref Expression
Hypotheses istrkg.p ⊢P=BaseG
istrkg.d ⊢-˙=dist⁡G
istrkg.i ⊢I=Itv⁡G
Assertion istrkgb ⊢G∈𝒢TarskiB↔G∈V∧∀x∈P∀y∈Py∈xIx→x=y∧∀x∈P∀y∈P∀z∈P∀u∈P∀v∈Pu∈xIz∧v∈yIz→∃a∈Pa∈uIy∧a∈vIx∧∀s∈𝒫P∀t∈𝒫P∃a∈P∀x∈s∀y∈tx∈aIy→∃b∈P∀x∈s∀y∈tb∈xIy

Proof

Step Hyp Ref Expression
1 istrkg.p ⊢P=BaseG
2 istrkg.d ⊢-˙=dist⁡G
3 istrkg.i ⊢I=Itv⁡G
4 simpl ⊢p=P∧i=I→p=P
5 simpr ⊢p=P∧i=I→i=I
6 5 oveqd ⊢p=P∧i=I→xix=xIx
7 6 eleq2d ⊢p=P∧i=I→y∈xix↔y∈xIx
8 7 imbi1d ⊢p=P∧i=I→y∈xix→x=y↔y∈xIx→x=y
9 4 8 raleqbidv ⊢p=P∧i=I→∀y∈py∈xix→x=y↔∀y∈Py∈xIx→x=y
10 4 9 raleqbidv ⊢p=P∧i=I→∀x∈p∀y∈py∈xix→x=y↔∀x∈P∀y∈Py∈xIx→x=y
11 5 oveqd ⊢p=P∧i=I→xiz=xIz
12 11 eleq2d ⊢p=P∧i=I→u∈xiz↔u∈xIz
13 5 oveqd ⊢p=P∧i=I→yiz=yIz
14 13 eleq2d ⊢p=P∧i=I→v∈yiz↔v∈yIz
15 12 14 anbi12d ⊢p=P∧i=I→u∈xiz∧v∈yiz↔u∈xIz∧v∈yIz
16 5 oveqd ⊢p=P∧i=I→uiy=uIy
17 16 eleq2d ⊢p=P∧i=I→a∈uiy↔a∈uIy
18 5 oveqd ⊢p=P∧i=I→vix=vIx
19 18 eleq2d ⊢p=P∧i=I→a∈vix↔a∈vIx
20 17 19 anbi12d ⊢p=P∧i=I→a∈uiy∧a∈vix↔a∈uIy∧a∈vIx
21 4 20 rexeqbidv ⊢p=P∧i=I→∃a∈pa∈uiy∧a∈vix↔∃a∈Pa∈uIy∧a∈vIx
22 15 21 imbi12d ⊢p=P∧i=I→u∈xiz∧v∈yiz→∃a∈pa∈uiy∧a∈vix↔u∈xIz∧v∈yIz→∃a∈Pa∈uIy∧a∈vIx
23 4 22 raleqbidv ⊢p=P∧i=I→∀v∈pu∈xiz∧v∈yiz→∃a∈pa∈uiy∧a∈vix↔∀v∈Pu∈xIz∧v∈yIz→∃a∈Pa∈uIy∧a∈vIx
24 4 23 raleqbidv ⊢p=P∧i=I→∀u∈p∀v∈pu∈xiz∧v∈yiz→∃a∈pa∈uiy∧a∈vix↔∀u∈P∀v∈Pu∈xIz∧v∈yIz→∃a∈Pa∈uIy∧a∈vIx
25 4 24 raleqbidv ⊢p=P∧i=I→∀z∈p∀u∈p∀v∈pu∈xiz∧v∈yiz→∃a∈pa∈uiy∧a∈vix↔∀z∈P∀u∈P∀v∈Pu∈xIz∧v∈yIz→∃a∈Pa∈uIy∧a∈vIx
26 4 25 raleqbidv ⊢p=P∧i=I→∀y∈p∀z∈p∀u∈p∀v∈pu∈xiz∧v∈yiz→∃a∈pa∈uiy∧a∈vix↔∀y∈P∀z∈P∀u∈P∀v∈Pu∈xIz∧v∈yIz→∃a∈Pa∈uIy∧a∈vIx
27 4 26 raleqbidv ⊢p=P∧i=I→∀x∈p∀y∈p∀z∈p∀u∈p∀v∈pu∈xiz∧v∈yiz→∃a∈pa∈uiy∧a∈vix↔∀x∈P∀y∈P∀z∈P∀u∈P∀v∈Pu∈xIz∧v∈yIz→∃a∈Pa∈uIy∧a∈vIx
28 4 pweqd ⊢p=P∧i=I→𝒫p=𝒫P
29 5 oveqd ⊢p=P∧i=I→aiy=aIy
30 29 eleq2d ⊢p=P∧i=I→x∈aiy↔x∈aIy
31 30 2ralbidv ⊢p=P∧i=I→∀x∈s∀y∈tx∈aiy↔∀x∈s∀y∈tx∈aIy
32 4 31 rexeqbidv ⊢p=P∧i=I→∃a∈p∀x∈s∀y∈tx∈aiy↔∃a∈P∀x∈s∀y∈tx∈aIy
33 5 oveqd ⊢p=P∧i=I→xiy=xIy
34 33 eleq2d ⊢p=P∧i=I→b∈xiy↔b∈xIy
35 34 2ralbidv ⊢p=P∧i=I→∀x∈s∀y∈tb∈xiy↔∀x∈s∀y∈tb∈xIy
36 4 35 rexeqbidv ⊢p=P∧i=I→∃b∈p∀x∈s∀y∈tb∈xiy↔∃b∈P∀x∈s∀y∈tb∈xIy
37 32 36 imbi12d ⊢p=P∧i=I→∃a∈p∀x∈s∀y∈tx∈aiy→∃b∈p∀x∈s∀y∈tb∈xiy↔∃a∈P∀x∈s∀y∈tx∈aIy→∃b∈P∀x∈s∀y∈tb∈xIy
38 28 37 raleqbidv ⊢p=P∧i=I→∀t∈𝒫p∃a∈p∀x∈s∀y∈tx∈aiy→∃b∈p∀x∈s∀y∈tb∈xiy↔∀t∈𝒫P∃a∈P∀x∈s∀y∈tx∈aIy→∃b∈P∀x∈s∀y∈tb∈xIy
39 28 38 raleqbidv ⊢p=P∧i=I→∀s∈𝒫p∀t∈𝒫p∃a∈p∀x∈s∀y∈tx∈aiy→∃b∈p∀x∈s∀y∈tb∈xiy↔∀s∈𝒫P∀t∈𝒫P∃a∈P∀x∈s∀y∈tx∈aIy→∃b∈P∀x∈s∀y∈tb∈xIy
40 10 27 39 3anbi123d ⊢p=P∧i=I→∀x∈p∀y∈py∈xix→x=y∧∀x∈p∀y∈p∀z∈p∀u∈p∀v∈pu∈xiz∧v∈yiz→∃a∈pa∈uiy∧a∈vix∧∀s∈𝒫p∀t∈𝒫p∃a∈p∀x∈s∀y∈tx∈aiy→∃b∈p∀x∈s∀y∈tb∈xiy↔∀x∈P∀y∈Py∈xIx→x=y∧∀x∈P∀y∈P∀z∈P∀u∈P∀v∈Pu∈xIz∧v∈yIz→∃a∈Pa∈uIy∧a∈vIx∧∀s∈𝒫P∀t∈𝒫P∃a∈P∀x∈s∀y∈tx∈aIy→∃b∈P∀x∈s∀y∈tb∈xIy
41 1 3 40 sbcie2s ⊢f=G→[˙Basef/p]˙[˙Itv⁡f/i]˙∀x∈p∀y∈py∈xix→x=y∧∀x∈p∀y∈p∀z∈p∀u∈p∀v∈pu∈xiz∧v∈yiz→∃a∈pa∈uiy∧a∈vix∧∀s∈𝒫p∀t∈𝒫p∃a∈p∀x∈s∀y∈tx∈aiy→∃b∈p∀x∈s∀y∈tb∈xiy↔∀x∈P∀y∈Py∈xIx→x=y∧∀x∈P∀y∈P∀z∈P∀u∈P∀v∈Pu∈xIz∧v∈yIz→∃a∈Pa∈uIy∧a∈vIx∧∀s∈𝒫P∀t∈𝒫P∃a∈P∀x∈s∀y∈tx∈aIy→∃b∈P∀x∈s∀y∈tb∈xIy
42 df-trkgb ⊢𝒢TarskiB=f|[˙Basef/p]˙[˙Itv⁡f/i]˙∀x∈p∀y∈py∈xix→x=y∧∀x∈p∀y∈p∀z∈p∀u∈p∀v∈pu∈xiz∧v∈yiz→∃a∈pa∈uiy∧a∈vix∧∀s∈𝒫p∀t∈𝒫p∃a∈p∀x∈s∀y∈tx∈aiy→∃b∈p∀x∈s∀y∈tb∈xiy
43 41 42 elab4g ⊢G∈𝒢TarskiB↔G∈V∧∀x∈P∀y∈Py∈xIx→x=y∧∀x∈P∀y∈P∀z∈P∀u∈P∀v∈Pu∈xIz∧v∈yIz→∃a∈Pa∈uIy∧a∈vIx∧∀s∈𝒫P∀t∈𝒫P∃a∈P∀x∈s∀y∈tx∈aIy→∃b∈P∀x∈s∀y∈tb∈xIy