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 simpr 
 |-  ( ( p = P /\ i = I ) -> i = I )
6 5 oveqd 
 |-  ( ( p = P /\ i = I ) -> ( x i x ) = ( x I x ) )
7 6 eleq2d 
 |-  ( ( p = P /\ i = I ) -> ( y e. ( x i x ) <-> y e. ( x I x ) ) )
8 7 imbi1d 
 |-  ( ( p = P /\ i = I ) -> ( ( y e. ( x i x ) -> x = y ) <-> ( y e. ( x I x ) -> x = y ) ) )
9 4 8 raleqbidv 
 |-  ( ( p = P /\ i = I ) -> ( A. y e. p ( y e. ( x i x ) -> x = y ) <-> A. y e. P ( y e. ( x I x ) -> x = y ) ) )
10 4 9 raleqbidv 
 |-  ( ( 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 ) ) )
11 5 oveqd 
 |-  ( ( p = P /\ i = I ) -> ( x i z ) = ( x I z ) )
12 11 eleq2d 
 |-  ( ( p = P /\ i = I ) -> ( u e. ( x i z ) <-> u e. ( x I z ) ) )
13 5 oveqd 
 |-  ( ( p = P /\ i = I ) -> ( y i z ) = ( y I z ) )
14 13 eleq2d 
 |-  ( ( p = P /\ i = I ) -> ( v e. ( y i z ) <-> v e. ( y I z ) ) )
15 12 14 anbi12d 
 |-  ( ( p = P /\ i = I ) -> ( ( u e. ( x i z ) /\ v e. ( y i z ) ) <-> ( u e. ( x I z ) /\ v e. ( y I z ) ) ) )
16 5 oveqd 
 |-  ( ( p = P /\ i = I ) -> ( u i y ) = ( u I y ) )
17 16 eleq2d 
 |-  ( ( p = P /\ i = I ) -> ( a e. ( u i y ) <-> a e. ( u I y ) ) )
18 5 oveqd 
 |-  ( ( p = P /\ i = I ) -> ( v i x ) = ( v I x ) )
19 18 eleq2d 
 |-  ( ( p = P /\ i = I ) -> ( a e. ( v i x ) <-> a e. ( v I x ) ) )
20 17 19 anbi12d 
 |-  ( ( p = P /\ i = I ) -> ( ( a e. ( u i y ) /\ a e. ( v i x ) ) <-> ( a e. ( u I y ) /\ a e. ( v I x ) ) ) )
21 4 20 rexeqbidv 
 |-  ( ( p = P /\ i = I ) -> ( 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 ) ) ) )
22 15 21 imbi12d 
 |-  ( ( p = P /\ i = I ) -> ( ( ( 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 ) ) ) ) )
23 4 22 raleqbidv 
 |-  ( ( p = P /\ i = I ) -> ( 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 ) ) ) ) )
24 4 23 raleqbidv 
 |-  ( ( p = P /\ i = I ) -> ( 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 ) ) ) ) )
25 4 24 raleqbidv 
 |-  ( ( p = P /\ i = I ) -> ( 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 ) ) ) ) )
26 4 25 raleqbidv 
 |-  ( ( p = P /\ i = I ) -> ( 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 ) ) ) ) )
27 4 26 raleqbidv 
 |-  ( ( 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 ) ) ) ) )
28 4 pweqd 
 |-  ( ( p = P /\ i = I ) -> ~P p = ~P P )
29 5 oveqd 
 |-  ( ( p = P /\ i = I ) -> ( a i y ) = ( a I y ) )
30 29 eleq2d 
 |-  ( ( p = P /\ i = I ) -> ( x e. ( a i y ) <-> x e. ( a I y ) ) )
31 30 2ralbidv 
 |-  ( ( p = P /\ i = I ) -> ( 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 ) ) )
32 4 31 rexeqbidv 
 |-  ( ( p = P /\ i = I ) -> ( 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 ) ) )
33 5 oveqd 
 |-  ( ( p = P /\ i = I ) -> ( x i y ) = ( x I y ) )
34 33 eleq2d 
 |-  ( ( p = P /\ i = I ) -> ( b e. ( x i y ) <-> b e. ( x I y ) ) )
35 34 2ralbidv 
 |-  ( ( p = P /\ i = I ) -> ( 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 ) ) )
36 4 35 rexeqbidv 
 |-  ( ( p = P /\ i = I ) -> ( 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 ) ) )
37 32 36 imbi12d 
 |-  ( ( p = P /\ i = I ) -> ( ( 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 ) ) ) )
38 28 37 raleqbidv 
 |-  ( ( p = P /\ i = I ) -> ( 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 ) ) ) )
39 28 38 raleqbidv 
 |-  ( ( 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 ) ) ) )
40 10 27 39 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 ) ) ) ) )
41 1 3 40 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 ) ) ) ) )
42 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 ) ) ) }
43 41 42 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 ) ) ) ) )