Metamath Proof Explorer

Theorem axtgbtwnid

Description: Identity of Betweenness. Axiom A6 of Schwabhauser p. 11. (Contributed by Thierry Arnoux, 15-Mar-2019)

Ref Expression
Hypotheses axtrkg.p 
|- P = ( Base ` G )
axtrkg.d 
|- .- = ( dist ` G )
axtrkg.i 
|- I = ( Itv ` G )
axtrkg.g 
|- ( ph -> G e. TarskiG )
axtgbtwnid.1 
|- ( ph -> X e. P )
axtgbtwnid.2 
|- ( ph -> Y e. P )
axtgbtwnid.3 
|- ( ph -> Y e. ( X I X ) )
Assertion axtgbtwnid 
|- ( ph -> X = Y )

Proof

Step Hyp Ref Expression
1 axtrkg.p 
 |-  P = ( Base ` G )
2 axtrkg.d 
 |-  .- = ( dist ` G )
3 axtrkg.i 
 |-  I = ( Itv ` G )
4 axtrkg.g 
 |-  ( ph -> G e. TarskiG )
5 axtgbtwnid.1 
 |-  ( ph -> X e. P )
6 axtgbtwnid.2 
 |-  ( ph -> Y e. P )
7 axtgbtwnid.3 
 |-  ( ph -> Y e. ( X I X ) )
8 df-trkg 
 |-  TarskiG = ( ( TarskiGC i^i TarskiGB ) i^i ( TarskiGCB i^i { f | [. ( Base ` f ) / p ]. [. ( Itv ` f ) / i ]. ( LineG ` f ) = ( x e. p , y e. ( p \ { x } ) |-> { z e. p | ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) } ) } ) )
9 inss1 
 |-  ( ( TarskiGC i^i TarskiGB ) i^i ( TarskiGCB i^i { f | [. ( Base ` f ) / p ]. [. ( Itv ` f ) / i ]. ( LineG ` f ) = ( x e. p , y e. ( p \ { x } ) |-> { z e. p | ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) } ) } ) ) C_ ( TarskiGC i^i TarskiGB )
10 inss2 
 |-  ( TarskiGC i^i TarskiGB ) C_ TarskiGB
11 9 10 sstri 
 |-  ( ( TarskiGC i^i TarskiGB ) i^i ( TarskiGCB i^i { f | [. ( Base ` f ) / p ]. [. ( Itv ` f ) / i ]. ( LineG ` f ) = ( x e. p , y e. ( p \ { x } ) |-> { z e. p | ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) } ) } ) ) C_ TarskiGB
12 8 11 eqsstri 
 |-  TarskiG C_ TarskiGB
13 12 4 sseldi 
 |-  ( ph -> G e. TarskiGB )
14 1 2 3 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 ) ) ) ) )
15 14 simprbi 
 |-  ( G e. TarskiGB -> ( 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 ) ) ) )
16 15 simp1d 
 |-  ( G e. TarskiGB -> A. x e. P A. y e. P ( y e. ( x I x ) -> x = y ) )
17 13 16 syl 
 |-  ( ph -> A. x e. P A. y e. P ( y e. ( x I x ) -> x = y ) )
18 id 
 |-  ( x = X -> x = X )
19 18 18 oveq12d 
 |-  ( x = X -> ( x I x ) = ( X I X ) )
20 19 eleq2d 
 |-  ( x = X -> ( y e. ( x I x ) <-> y e. ( X I X ) ) )
21 eqeq1 
 |-  ( x = X -> ( x = y <-> X = y ) )
22 20 21 imbi12d 
 |-  ( x = X -> ( ( y e. ( x I x ) -> x = y ) <-> ( y e. ( X I X ) -> X = y ) ) )
23 eleq1 
 |-  ( y = Y -> ( y e. ( X I X ) <-> Y e. ( X I X ) ) )
24 eqeq2 
 |-  ( y = Y -> ( X = y <-> X = Y ) )
25 23 24 imbi12d 
 |-  ( y = Y -> ( ( y e. ( X I X ) -> X = y ) <-> ( Y e. ( X I X ) -> X = Y ) ) )
26 22 25 rspc2v 
 |-  ( ( X e. P /\ Y e. P ) -> ( A. x e. P A. y e. P ( y e. ( x I x ) -> x = y ) -> ( Y e. ( X I X ) -> X = Y ) ) )
27 5 6 26 syl2anc 
 |-  ( ph -> ( A. x e. P A. y e. P ( y e. ( x I x ) -> x = y ) -> ( Y e. ( X I X ) -> X = Y ) ) )
28 17 7 27 mp2d 
 |-  ( ph -> X = Y )