Theorem istrkgb 25354

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

Hypotheses

Ref	Expression
istrkg.p	|- P = ( Base ` G )
istrkg.d	|- .- = ( dist ` G )
istrkg.i	|- I = (Itv ` G )

Assertion

Ref	Expression
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 ) ) ) ) )

Distinct variable groups:   a, b, s, t, u, v, x, y, z, I   P, a, b, s, t, u, v, x, y, z   .- , a, b, u, v, x, y, z

Allowed substitution hints:   G( x, y, z, v, u, t, s, a, b)   .- ( t, s)

Proof of Theorem istrkgb

Dummy variables f i p are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		istrkg.p	. . 3 |- P = ( Base ` G )
2		istrkg.i	. . 3 |- I = (Itv ` G )
3		simpl 473	. . . . . 6 |- ( ( p = P /\ i = I ) -> p = P )
4	3	eqcomd 2628	. . . . 5 |- ( ( p = P /\ i = I ) -> P = p )
5	4	adantr 481	. . . . . 6 |- ( ( ( p = P /\ i = I ) /\ x e. P ) -> P = p )
6		simpllr 799	. . . . . . . . . 10 |- ( ( ( ( p = P /\ i = I ) /\ x e. P ) /\ y e. P ) -> i = I )
7	6	eqcomd 2628	. . . . . . . . 9 |- ( ( ( ( p = P /\ i = I ) /\ x e. P ) /\ y e. P ) -> I = i )
8	7	oveqd 6667	. . . . . . . 8 |- ( ( ( ( p = P /\ i = I ) /\ x e. P ) /\ y e. P ) -> ( x I x ) = ( x i x ) )
9	8	eleq2d 2687	. . . . . . 7 |- ( ( ( ( p = P /\ i = I ) /\ x e. P ) /\ y e. P ) -> ( y e. ( x I x ) <-> y e. ( x i x ) ) )
10	9	imbi1d 331	. . . . . 6 |- ( ( ( ( p = P /\ i = I ) /\ x e. P ) /\ y e. P ) -> ( ( y e. ( x I x ) -> x = y ) <-> ( y e. ( x i x ) -> x = y ) ) )
11	5, 10	raleqbidva 3154	. . . . 5 |- ( ( ( 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 ) ) )
12	4, 11	raleqbidva 3154	. . . 4 |- ( ( 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 ) ) )
13	5	adantr 481	. . . . . . 7 |- ( ( ( ( p = P /\ i = I ) /\ x e. P ) /\ y e. P ) -> P = p )
14	13	adantr 481	. . . . . . . 8 |- ( ( ( ( ( p = P /\ i = I ) /\ x e. P ) /\ y e. P ) /\ z e. P ) -> P = p )
15	14	adantr 481	. . . . . . . . 9 |- ( ( ( ( ( ( p = P /\ i = I ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ u e. P ) -> P = p )
16		simp-6r 811	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ( p = P /\ i = I ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ u e. P ) /\ v e. P ) -> i = I )
17	16	eqcomd 2628	. . . . . . . . . . . . 13 |- ( ( ( ( ( ( ( p = P /\ i = I ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ u e. P ) /\ v e. P ) -> I = i )
18	17	oveqd 6667	. . . . . . . . . . . 12 |- ( ( ( ( ( ( ( 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 ) )
19	18	eleq2d 2687	. . . . . . . . . . 11 |- ( ( ( ( ( ( ( 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 ) ) )
20	17	oveqd 6667	. . . . . . . . . . . 12 |- ( ( ( ( ( ( ( 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 ) )
21	20	eleq2d 2687	. . . . . . . . . . 11 |- ( ( ( ( ( ( ( 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 ) ) )
22	19, 21	anbi12d 747	. . . . . . . . . 10 |- ( ( ( ( ( ( ( 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 ) ) ) )
23	15	adantr 481	. . . . . . . . . . 11 |- ( ( ( ( ( ( ( p = P /\ i = I ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ u e. P ) /\ v e. P ) -> P = p )
24	17	oveqdr 6674	. . . . . . . . . . . . 13 |- ( ( ( ( ( ( ( ( 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 ) )
25	24	eleq2d 2687	. . . . . . . . . . . 12 |- ( ( ( ( ( ( ( ( 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 ) ) )
26	17	oveqdr 6674	. . . . . . . . . . . . 13 |- ( ( ( ( ( ( ( ( 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 ) )
27	26	eleq2d 2687	. . . . . . . . . . . 12 |- ( ( ( ( ( ( ( ( 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 ) ) )
28	25, 27	anbi12d 747	. . . . . . . . . . 11 |- ( ( ( ( ( ( ( ( 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 ) ) ) )
29	23, 28	rexeqbidva 3155	. . . . . . . . . 10 |- ( ( ( ( ( ( ( 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 ) ) ) )
30	22, 29	imbi12d 334	. . . . . . . . 9 |- ( ( ( ( ( ( ( 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 ) ) ) ) )
31	15, 30	raleqbidva 3154	. . . . . . . 8 |- ( ( ( ( ( ( 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 ) ) ) ) )
32	14, 31	raleqbidva 3154	. . . . . . 7 |- ( ( ( ( ( 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 ) ) ) ) )
33	13, 32	raleqbidva 3154	. . . . . 6 |- ( ( ( ( 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 ) ) ) ) )
34	5, 33	raleqbidva 3154	. . . . 5 |- ( ( ( 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 ) ) ) ) )
35	4, 34	raleqbidva 3154	. . . 4 |- ( ( 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 ) ) ) ) )
36	4	pweqd 4163	. . . . 5 |- ( ( p = P /\ i = I ) -> ~P P = ~P p )
37	36	adantr 481	. . . . . 6 |- ( ( ( p = P /\ i = I ) /\ s e. ~P P ) -> ~P P = ~P p )
38	4	ad2antrr 762	. . . . . . . 8 |- ( ( ( ( p = P /\ i = I ) /\ s e. ~P P ) /\ t e. ~P P ) -> P = p )
39		simp-4r 807	. . . . . . . . . . . 12 |- ( ( ( ( ( p = P /\ i = I ) /\ s e. ~P P ) /\ t e. ~P P ) /\ a e. P ) -> i = I )
40	39	eqcomd 2628	. . . . . . . . . . 11 |- ( ( ( ( ( p = P /\ i = I ) /\ s e. ~P P ) /\ t e. ~P P ) /\ a e. P ) -> I = i )
41	40	oveqd 6667	. . . . . . . . . 10 |- ( ( ( ( ( p = P /\ i = I ) /\ s e. ~P P ) /\ t e. ~P P ) /\ a e. P ) -> ( a I y ) = ( a i y ) )
42	41	eleq2d 2687	. . . . . . . . 9 |- ( ( ( ( ( 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 ) ) )
43	42	2ralbidv 2989	. . . . . . . 8 |- ( ( ( ( ( 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 ) ) )
44	38, 43	rexeqbidva 3155	. . . . . . 7 |- ( ( ( ( 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 ) ) )
45		simp-4r 807	. . . . . . . . . . . 12 |- ( ( ( ( ( p = P /\ i = I ) /\ s e. ~P P ) /\ t e. ~P P ) /\ b e. P ) -> i = I )
46	45	eqcomd 2628	. . . . . . . . . . 11 |- ( ( ( ( ( p = P /\ i = I ) /\ s e. ~P P ) /\ t e. ~P P ) /\ b e. P ) -> I = i )
47	46	oveqd 6667	. . . . . . . . . 10 |- ( ( ( ( ( p = P /\ i = I ) /\ s e. ~P P ) /\ t e. ~P P ) /\ b e. P ) -> ( x I y ) = ( x i y ) )
48	47	eleq2d 2687	. . . . . . . . 9 |- ( ( ( ( ( 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 ) ) )
49	48	2ralbidv 2989	. . . . . . . 8 |- ( ( ( ( ( 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 ) ) )
50	38, 49	rexeqbidva 3155	. . . . . . 7 |- ( ( ( ( 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 ) ) )
51	44, 50	imbi12d 334	. . . . . 6 |- ( ( ( ( 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 ) ) ) )
52	37, 51	raleqbidva 3154	. . . . 5 |- ( ( ( 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 ) ) ) )
53	36, 52	raleqbidva 3154	. . . 4 |- ( ( 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 ) ) ) )
54	12, 35, 53	3anbi123d 1399	. . 3 |- ( ( 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 ) ) ) ) )
55	1, 2, 54	sbcie2s 15916	. 2 |- ( 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 ) ) ) ) )
56		df-trkgb 25348	. 2 |- 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 ) ) ) }
57	55, 56	elab4g 3355	1 |- ( 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 ) ) ) ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   /\ w3a 1037   = wceq 1483   e. wcel 1990   A.wral 2912   E.wrex 2913   _Vcvv 3200   [.wsbc 3435   ~Pcpw 4158   ` cfv 5888  (class class class)co 6650   Basecbs 15857   distcds 15950  TarskiG_Bcstrkgb 25331  Itvcitv 25335

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-nul 4789

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-iota 5851  df-fv 5896  df-ov 6653  df-trkgb 25348

This theorem is referenced by:  axtgbtwnid  25365  axtgpasch  25366  axtgcont1  25367  f1otrg  25751  eengtrkg  25865