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 = ( Base ` G )
istrkg.d 
|- .- = ( dist ` G )
istrkg.i 
|- I = ( Itv ` G )
Assertion istrkgb 
|- ( G e. TarskiGB <-> ( G e. _V /\ ( A. x e. P A. y e. P ( y e. ( x I x ) -> x = y ) /\ A. x e. P A. y e. P A. z e. P A. u e. P A. v e. P ( ( u e. ( x I z ) /\ v e. ( y I z ) ) -> E. a e. P ( a e. ( u I y ) /\ a e. ( v I x ) ) ) /\ A. s e. ~P P A. t e. ~P P ( E. a e. P A. x e. s A. y e. t x e. ( a I y ) -> E. b e. P A. x e. s A. y e. t b e. ( x I y ) ) ) ) )

Proof

Step Hyp Ref Expression
1 istrkg.p 
 |-  P = ( Base ` G )
2 istrkg.d 
 |-  .- = ( dist ` G )
3 istrkg.i 
 |-  I = ( Itv ` G )
4 simpl 
 |-  ( ( p = P /\ i = I ) -> p = P )
5 4 eqcomd 
 |-  ( ( p = P /\ i = I ) -> P = p )
6 5 adantr 
 |-  ( ( ( p = P /\ i = I ) /\ x e. P ) -> P = p )
7 simpllr 
 |-  ( ( ( ( p = P /\ i = I ) /\ x e. P ) /\ y e. P ) -> i = I )
8 7 eqcomd 
 |-  ( ( ( ( p = P /\ i = I ) /\ x e. P ) /\ y e. P ) -> I = i )
9 8 oveqd 
 |-  ( ( ( ( p = P /\ i = I ) /\ x e. P ) /\ y e. P ) -> ( x I x ) = ( x i x ) )
10 9 eleq2d 
 |-  ( ( ( ( p = P /\ i = I ) /\ x e. P ) /\ y e. P ) -> ( y e. ( x I x ) <-> y e. ( x i x ) ) )
11 10 imbi1d 
 |-  ( ( ( ( p = P /\ i = I ) /\ x e. P ) /\ y e. P ) -> ( ( y e. ( x I x ) -> x = y ) <-> ( y e. ( x i x ) -> x = y ) ) )
12 6 11 raleqbidva 
 |-  ( ( ( p = P /\ i = I ) /\ x e. P ) -> ( A. y e. P ( y e. ( x I x ) -> x = y ) <-> A. y e. p ( y e. ( x i x ) -> x = y ) ) )
13 5 12 raleqbidva 
 |-  ( ( p = P /\ i = I ) -> ( A. x e. P A. y e. P ( y e. ( x I x ) -> x = y ) <-> A. x e. p A. y e. p ( y e. ( x i x ) -> x = y ) ) )
14 6 adantr 
 |-  ( ( ( ( p = P /\ i = I ) /\ x e. P ) /\ y e. P ) -> P = p )
15 14 adantr 
 |-  ( ( ( ( ( p = P /\ i = I ) /\ x e. P ) /\ y e. P ) /\ z e. P ) -> P = p )
16 15 adantr 
 |-  ( ( ( ( ( ( p = P /\ i = I ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ u e. P ) -> P = p )
17 simp-6r 
 |-  ( ( ( ( ( ( ( p = P /\ i = I ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ u e. P ) /\ v e. P ) -> i = I )
18 17 eqcomd 
 |-  ( ( ( ( ( ( ( p = P /\ i = I ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ u e. P ) /\ v e. P ) -> I = i )
19 18 oveqd 
 |-  ( ( ( ( ( ( ( p = P /\ i = I ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ u e. P ) /\ v e. P ) -> ( x I z ) = ( x i z ) )
20 19 eleq2d 
 |-  ( ( ( ( ( ( ( p = P /\ i = I ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ u e. P ) /\ v e. P ) -> ( u e. ( x I z ) <-> u e. ( x i z ) ) )
21 18 oveqd 
 |-  ( ( ( ( ( ( ( p = P /\ i = I ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ u e. P ) /\ v e. P ) -> ( y I z ) = ( y i z ) )
22 21 eleq2d 
 |-  ( ( ( ( ( ( ( p = P /\ i = I ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ u e. P ) /\ v e. P ) -> ( v e. ( y I z ) <-> v e. ( y i z ) ) )
23 20 22 anbi12d 
 |-  ( ( ( ( ( ( ( p = P /\ i = I ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ u e. P ) /\ v e. P ) -> ( ( u e. ( x I z ) /\ v e. ( y I z ) ) <-> ( u e. ( x i z ) /\ v e. ( y i z ) ) ) )
24 16 adantr 
 |-  ( ( ( ( ( ( ( p = P /\ i = I ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ u e. P ) /\ v e. P ) -> P = p )
25 18 oveqdr 
 |-  ( ( ( ( ( ( ( ( p = P /\ i = I ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ u e. P ) /\ v e. P ) /\ a e. P ) -> ( u I y ) = ( u i y ) )
26 25 eleq2d 
 |-  ( ( ( ( ( ( ( ( p = P /\ i = I ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ u e. P ) /\ v e. P ) /\ a e. P ) -> ( a e. ( u I y ) <-> a e. ( u i y ) ) )
27 18 oveqdr 
 |-  ( ( ( ( ( ( ( ( p = P /\ i = I ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ u e. P ) /\ v e. P ) /\ a e. P ) -> ( v I x ) = ( v i x ) )
28 27 eleq2d 
 |-  ( ( ( ( ( ( ( ( p = P /\ i = I ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ u e. P ) /\ v e. P ) /\ a e. P ) -> ( a e. ( v I x ) <-> a e. ( v i x ) ) )
29 26 28 anbi12d 
 |-  ( ( ( ( ( ( ( ( p = P /\ i = I ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ u e. P ) /\ v e. P ) /\ a e. P ) -> ( ( a e. ( u I y ) /\ a e. ( v I x ) ) <-> ( a e. ( u i y ) /\ a e. ( v i x ) ) ) )
30 24 29 rexeqbidva 
 |-  ( ( ( ( ( ( ( p = P /\ i = I ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ u e. P ) /\ v e. P ) -> ( E. a e. P ( a e. ( u I y ) /\ a e. ( v I x ) ) <-> E. a e. p ( a e. ( u i y ) /\ a e. ( v i x ) ) ) )
31 23 30 imbi12d 
 |-  ( ( ( ( ( ( ( p = P /\ i = I ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ u e. P ) /\ v e. P ) -> ( ( ( u e. ( x I z ) /\ v e. ( y I z ) ) -> E. a e. P ( a e. ( u I y ) /\ a e. ( v I x ) ) ) <-> ( ( u e. ( x i z ) /\ v e. ( y i z ) ) -> E. a e. p ( a e. ( u i y ) /\ a e. ( v i x ) ) ) ) )
32 16 31 raleqbidva 
 |-  ( ( ( ( ( ( p = P /\ i = I ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ u e. P ) -> ( A. v e. P ( ( u e. ( x I z ) /\ v e. ( y I z ) ) -> E. a e. P ( a e. ( u I y ) /\ a e. ( v I x ) ) ) <-> A. v e. p ( ( u e. ( x i z ) /\ v e. ( y i z ) ) -> E. a e. p ( a e. ( u i y ) /\ a e. ( v i x ) ) ) ) )
33 15 32 raleqbidva 
 |-  ( ( ( ( ( p = P /\ i = I ) /\ x e. P ) /\ y e. P ) /\ z e. P ) -> ( A. u e. P A. v e. P ( ( u e. ( x I z ) /\ v e. ( y I z ) ) -> E. a e. P ( a e. ( u I y ) /\ a e. ( v I x ) ) ) <-> A. u e. p A. v e. p ( ( u e. ( x i z ) /\ v e. ( y i z ) ) -> E. a e. p ( a e. ( u i y ) /\ a e. ( v i x ) ) ) ) )
34 14 33 raleqbidva 
 |-  ( ( ( ( p = P /\ i = I ) /\ x e. P ) /\ y e. P ) -> ( A. z e. P A. u e. P A. v e. P ( ( u e. ( x I z ) /\ v e. ( y I z ) ) -> E. a e. P ( a e. ( u I y ) /\ a e. ( v I x ) ) ) <-> A. z e. p A. u e. p A. v e. p ( ( u e. ( x i z ) /\ v e. ( y i z ) ) -> E. a e. p ( a e. ( u i y ) /\ a e. ( v i x ) ) ) ) )
35 6 34 raleqbidva 
 |-  ( ( ( p = P /\ i = I ) /\ x e. P ) -> ( A. y e. P A. z e. P A. u e. P A. v e. P ( ( u e. ( x I z ) /\ v e. ( y I z ) ) -> E. a e. P ( a e. ( u I y ) /\ a e. ( v I x ) ) ) <-> A. y e. p A. z e. p A. u e. p A. v e. p ( ( u e. ( x i z ) /\ v e. ( y i z ) ) -> E. a e. p ( a e. ( u i y ) /\ a e. ( v i x ) ) ) ) )
36 5 35 raleqbidva 
 |-  ( ( p = P /\ i = I ) -> ( A. x e. P A. y e. P A. z e. P A. u e. P A. v e. P ( ( u e. ( x I z ) /\ v e. ( y I z ) ) -> E. a e. P ( a e. ( u I y ) /\ a e. ( v I x ) ) ) <-> A. x e. p A. y e. p A. z e. p A. u e. p A. v e. p ( ( u e. ( x i z ) /\ v e. ( y i z ) ) -> E. a e. p ( a e. ( u i y ) /\ a e. ( v i x ) ) ) ) )
37 5 pweqd 
 |-  ( ( p = P /\ i = I ) -> ~P P = ~P p )
38 37 adantr 
 |-  ( ( ( p = P /\ i = I ) /\ s e. ~P P ) -> ~P P = ~P p )
39 5 ad2antrr 
 |-  ( ( ( ( p = P /\ i = I ) /\ s e. ~P P ) /\ t e. ~P P ) -> P = p )
40 simp-4r 
 |-  ( ( ( ( ( p = P /\ i = I ) /\ s e. ~P P ) /\ t e. ~P P ) /\ a e. P ) -> i = I )
41 40 eqcomd 
 |-  ( ( ( ( ( p = P /\ i = I ) /\ s e. ~P P ) /\ t e. ~P P ) /\ a e. P ) -> I = i )
42 41 oveqd 
 |-  ( ( ( ( ( p = P /\ i = I ) /\ s e. ~P P ) /\ t e. ~P P ) /\ a e. P ) -> ( a I y ) = ( a i y ) )
43 42 eleq2d 
 |-  ( ( ( ( ( p = P /\ i = I ) /\ s e. ~P P ) /\ t e. ~P P ) /\ a e. P ) -> ( x e. ( a I y ) <-> x e. ( a i y ) ) )
44 43 2ralbidv 
 |-  ( ( ( ( ( p = P /\ i = I ) /\ s e. ~P P ) /\ t e. ~P P ) /\ a e. P ) -> ( A. x e. s A. y e. t x e. ( a I y ) <-> A. x e. s A. y e. t x e. ( a i y ) ) )
45 39 44 rexeqbidva 
 |-  ( ( ( ( p = P /\ i = I ) /\ s e. ~P P ) /\ t e. ~P P ) -> ( E. a e. P A. x e. s A. y e. t x e. ( a I y ) <-> E. a e. p A. x e. s A. y e. t x e. ( a i y ) ) )
46 simp-4r 
 |-  ( ( ( ( ( p = P /\ i = I ) /\ s e. ~P P ) /\ t e. ~P P ) /\ b e. P ) -> i = I )
47 46 eqcomd 
 |-  ( ( ( ( ( p = P /\ i = I ) /\ s e. ~P P ) /\ t e. ~P P ) /\ b e. P ) -> I = i )
48 47 oveqd 
 |-  ( ( ( ( ( p = P /\ i = I ) /\ s e. ~P P ) /\ t e. ~P P ) /\ b e. P ) -> ( x I y ) = ( x i y ) )
49 48 eleq2d 
 |-  ( ( ( ( ( p = P /\ i = I ) /\ s e. ~P P ) /\ t e. ~P P ) /\ b e. P ) -> ( b e. ( x I y ) <-> b e. ( x i y ) ) )
50 49 2ralbidv 
 |-  ( ( ( ( ( p = P /\ i = I ) /\ s e. ~P P ) /\ t e. ~P P ) /\ b e. P ) -> ( A. x e. s A. y e. t b e. ( x I y ) <-> A. x e. s A. y e. t b e. ( x i y ) ) )
51 39 50 rexeqbidva 
 |-  ( ( ( ( p = P /\ i = I ) /\ s e. ~P P ) /\ t e. ~P P ) -> ( E. b e. P A. x e. s A. y e. t b e. ( x I y ) <-> E. b e. p A. x e. s A. y e. t b e. ( x i y ) ) )
52 45 51 imbi12d 
 |-  ( ( ( ( p = P /\ i = I ) /\ s e. ~P P ) /\ t e. ~P P ) -> ( ( E. a e. P A. x e. s A. y e. t x e. ( a I y ) -> E. b e. P A. x e. s A. y e. t b e. ( x I y ) ) <-> ( E. a e. p A. x e. s A. y e. t x e. ( a i y ) -> E. b e. p A. x e. s A. y e. t b e. ( x i y ) ) ) )
53 38 52 raleqbidva 
 |-  ( ( ( p = P /\ i = I ) /\ s e. ~P P ) -> ( A. t e. ~P P ( E. a e. P A. x e. s A. y e. t x e. ( a I y ) -> E. b e. P A. x e. s A. y e. t b e. ( x I y ) ) <-> A. t e. ~P p ( E. a e. p A. x e. s A. y e. t x e. ( a i y ) -> E. b e. p A. x e. s A. y e. t b e. ( x i y ) ) ) )
54 37 53 raleqbidva 
 |-  ( ( p = P /\ i = I ) -> ( A. s e. ~P P A. t e. ~P P ( E. a e. P A. x e. s A. y e. t x e. ( a I y ) -> E. b e. P A. x e. s A. y e. t b e. ( x I y ) ) <-> A. s e. ~P p A. t e. ~P p ( E. a e. p A. x e. s A. y e. t x e. ( a i y ) -> E. b e. p A. x e. s A. y e. t b e. ( x i y ) ) ) )
55 13 36 54 3anbi123d 
 |-  ( ( p = P /\ i = I ) -> ( ( A. x e. P A. y e. P ( y e. ( x I x ) -> x = y ) /\ A. x e. P A. y e. P A. z e. P A. u e. P A. v e. P ( ( u e. ( x I z ) /\ v e. ( y I z ) ) -> E. a e. P ( a e. ( u I y ) /\ a e. ( v I x ) ) ) /\ A. s e. ~P P A. t e. ~P P ( E. a e. P A. x e. s A. y e. t x e. ( a I y ) -> E. b e. P A. x e. s A. y e. t b e. ( x I y ) ) ) <-> ( A. x e. p A. y e. p ( y e. ( x i x ) -> x = y ) /\ A. x e. p A. y e. p A. z e. p A. u e. p A. v e. p ( ( u e. ( x i z ) /\ v e. ( y i z ) ) -> E. a e. p ( a e. ( u i y ) /\ a e. ( v i x ) ) ) /\ A. s e. ~P p A. t e. ~P p ( E. a e. p A. x e. s A. y e. t x e. ( a i y ) -> E. b e. p A. x e. s A. y e. t b e. ( x i y ) ) ) ) )
56 1 3 55 sbcie2s 
 |-  ( f = G -> ( [. ( Base ` f ) / p ]. [. ( Itv ` f ) / i ]. ( A. x e. p A. y e. p ( y e. ( x i x ) -> x = y ) /\ A. x e. p A. y e. p A. z e. p A. u e. p A. v e. p ( ( u e. ( x i z ) /\ v e. ( y i z ) ) -> E. a e. p ( a e. ( u i y ) /\ a e. ( v i x ) ) ) /\ A. s e. ~P p A. t e. ~P p ( E. a e. p A. x e. s A. y e. t x e. ( a i y ) -> E. b e. p A. x e. s A. y e. t b e. ( x i y ) ) ) <-> ( A. x e. P A. y e. P ( y e. ( x I x ) -> x = y ) /\ A. x e. P A. y e. P A. z e. P A. u e. P A. v e. P ( ( u e. ( x I z ) /\ v e. ( y I z ) ) -> E. a e. P ( a e. ( u I y ) /\ a e. ( v I x ) ) ) /\ A. s e. ~P P A. t e. ~P P ( E. a e. P A. x e. s A. y e. t x e. ( a I y ) -> E. b e. P A. x e. s A. y e. t b e. ( x I y ) ) ) ) )
57 df-trkgb 
 |-  TarskiGB = { f | [. ( Base ` f ) / p ]. [. ( Itv ` f ) / i ]. ( A. x e. p A. y e. p ( y e. ( x i x ) -> x = y ) /\ A. x e. p A. y e. p A. z e. p A. u e. p A. v e. p ( ( u e. ( x i z ) /\ v e. ( y i z ) ) -> E. a e. p ( a e. ( u i y ) /\ a e. ( v i x ) ) ) /\ A. s e. ~P p A. t e. ~P p ( E. a e. p A. x e. s A. y e. t x e. ( a i y ) -> E. b e. p A. x e. s A. y e. t b e. ( x i y ) ) ) }
58 56 57 elab4g 
 |-  ( G e. TarskiGB <-> ( G e. _V /\ ( A. x e. P A. y e. P ( y e. ( x I x ) -> x = y ) /\ A. x e. P A. y e. P A. z e. P A. u e. P A. v e. P ( ( u e. ( x I z ) /\ v e. ( y I z ) ) -> E. a e. P ( a e. ( u I y ) /\ a e. ( v I x ) ) ) /\ A. s e. ~P P A. t e. ~P P ( E. a e. P A. x e. s A. y e. t x e. ( a I y ) -> E. b e. P A. x e. s A. y e. t b e. ( x I y ) ) ) ) )