Definition df-trkge 25350

Description: Define the class of geometries fulfilling Euclid's axiom, Axiom A10 of [Schwabhauser] p. 13. (Contributed by Thierry Arnoux, 14-Mar-2019.)

Assertion

Ref	Expression
df-trkge	|- TarskiGE = { f | [. ( Base ` f ) / p ]. [. (Itv ` f ) / 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 v ) /\ u e. ( y i z ) /\ x =/= u ) -> E. a e. p E. b e. p ( y e. ( x i a ) /\ z e. ( x i b ) /\ v e. ( a i b ) ) ) }

Distinct variable group:   a, b, f, p, i, u, v, x, y, z

Detailed syntax breakdown of Definition df-trkge

Step	Hyp	Ref	Expression
1		cstrkge 25334	. 2 class TarskiGE
2		vu	. . . . . . . . . . . . . 14 setvar u
3	2	cv 1482	. . . . . . . . . . . . 13 class u
4		vx	. . . . . . . . . . . . . . 15 setvar x
5	4	cv 1482	. . . . . . . . . . . . . 14 class x
6		vv	. . . . . . . . . . . . . . 15 setvar v
7	6	cv 1482	. . . . . . . . . . . . . 14 class v
8		vi	. . . . . . . . . . . . . . 15 setvar i
9	8	cv 1482	. . . . . . . . . . . . . 14 class i
10	5, 7, 9	co 6650	. . . . . . . . . . . . 13 class ( x i v )
11	3, 10	wcel 1990	. . . . . . . . . . . 12 wff u e. ( x i v )
12		vy	. . . . . . . . . . . . . . 15 setvar y
13	12	cv 1482	. . . . . . . . . . . . . 14 class y
14		vz	. . . . . . . . . . . . . . 15 setvar z
15	14	cv 1482	. . . . . . . . . . . . . 14 class z
16	13, 15, 9	co 6650	. . . . . . . . . . . . 13 class ( y i z )
17	3, 16	wcel 1990	. . . . . . . . . . . 12 wff u e. ( y i z )
18	5, 3	wne 2794	. . . . . . . . . . . 12 wff x =/= u
19	11, 17, 18	w3a 1037	. . . . . . . . . . 11 wff ( u e. ( x i v ) /\ u e. ( y i z ) /\ x =/= u )
20		va	. . . . . . . . . . . . . . . . 17 setvar a
21	20	cv 1482	. . . . . . . . . . . . . . . 16 class a
22	5, 21, 9	co 6650	. . . . . . . . . . . . . . 15 class ( x i a )
23	13, 22	wcel 1990	. . . . . . . . . . . . . 14 wff y e. ( x i a )
24		vb	. . . . . . . . . . . . . . . . 17 setvar b
25	24	cv 1482	. . . . . . . . . . . . . . . 16 class b
26	5, 25, 9	co 6650	. . . . . . . . . . . . . . 15 class ( x i b )
27	15, 26	wcel 1990	. . . . . . . . . . . . . 14 wff z e. ( x i b )
28	21, 25, 9	co 6650	. . . . . . . . . . . . . . 15 class ( a i b )
29	7, 28	wcel 1990	. . . . . . . . . . . . . 14 wff v e. ( a i b )
30	23, 27, 29	w3a 1037	. . . . . . . . . . . . 13 wff ( y e. ( x i a ) /\ z e. ( x i b ) /\ v e. ( a i b ) )
31		vp	. . . . . . . . . . . . . 14 setvar p
32	31	cv 1482	. . . . . . . . . . . . 13 class p
33	30, 24, 32	wrex 2913	. . . . . . . . . . . 12 wff E. b e. p ( y e. ( x i a ) /\ z e. ( x i b ) /\ v e. ( a i b ) )
34	33, 20, 32	wrex 2913	. . . . . . . . . . 11 wff E. a e. p E. b e. p ( y e. ( x i a ) /\ z e. ( x i b ) /\ v e. ( a i b ) )
35	19, 34	wi 4	. . . . . . . . . 10 wff ( ( u e. ( x i v ) /\ u e. ( y i z ) /\ x =/= u ) -> E. a e. p E. b e. p ( y e. ( x i a ) /\ z e. ( x i b ) /\ v e. ( a i b ) ) )
36	35, 6, 32	wral 2912	. . . . . . . . 9 wff A. v e. p ( ( u e. ( x i v ) /\ u e. ( y i z ) /\ x =/= u ) -> E. a e. p E. b e. p ( y e. ( x i a ) /\ z e. ( x i b ) /\ v e. ( a i b ) ) )
37	36, 2, 32	wral 2912	. . . . . . . 8 wff A. u e. p A. v e. p ( ( u e. ( x i v ) /\ u e. ( y i z ) /\ x =/= u ) -> E. a e. p E. b e. p ( y e. ( x i a ) /\ z e. ( x i b ) /\ v e. ( a i b ) ) )
38	37, 14, 32	wral 2912	. . . . . . 7 wff A. z e. p A. u e. p A. v e. p ( ( u e. ( x i v ) /\ u e. ( y i z ) /\ x =/= u ) -> E. a e. p E. b e. p ( y e. ( x i a ) /\ z e. ( x i b ) /\ v e. ( a i b ) ) )
39	38, 12, 32	wral 2912	. . . . . 6 wff A. y e. p A. z e. p A. u e. p A. v e. p ( ( u e. ( x i v ) /\ u e. ( y i z ) /\ x =/= u ) -> E. a e. p E. b e. p ( y e. ( x i a ) /\ z e. ( x i b ) /\ v e. ( a i b ) ) )
40	39, 4, 32	wral 2912	. . . . 5 wff A. x e. p A. y e. p A. z e. p A. u e. p A. v e. p ( ( u e. ( x i v ) /\ u e. ( y i z ) /\ x =/= u ) -> E. a e. p E. b e. p ( y e. ( x i a ) /\ z e. ( x i b ) /\ v e. ( a i b ) ) )
41		vf	. . . . . . 7 setvar f
42	41	cv 1482	. . . . . 6 class f
43		citv 25335	. . . . . 6 class Itv
44	42, 43	cfv 5888	. . . . 5 class (Itv ` f )
45	40, 8, 44	wsbc 3435	. . . 4 wff [. (Itv ` f ) / 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 v ) /\ u e. ( y i z ) /\ x =/= u ) -> E. a e. p E. b e. p ( y e. ( x i a ) /\ z e. ( x i b ) /\ v e. ( a i b ) ) )
46		cbs 15857	. . . . 5 class Base
47	42, 46	cfv 5888	. . . 4 class ( Base ` f )
48	45, 31, 47	wsbc 3435	. . 3 wff [. ( Base ` f ) / p ]. [. (Itv ` f ) / 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 v ) /\ u e. ( y i z ) /\ x =/= u ) -> E. a e. p E. b e. p ( y e. ( x i a ) /\ z e. ( x i b ) /\ v e. ( a i b ) ) )
49	48, 41	cab 2608	. 2 class { f | [. ( Base ` f ) / p ]. [. (Itv ` f ) / 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 v ) /\ u e. ( y i z ) /\ x =/= u ) -> E. a e. p E. b e. p ( y e. ( x i a ) /\ z e. ( x i b ) /\ v e. ( a i b ) ) ) }
50	1, 49	wceq 1483	1 wff TarskiGE = { f | [. ( Base ` f ) / p ]. [. (Itv ` f ) / 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 v ) /\ u e. ( y i z ) /\ x =/= u ) -> E. a e. p E. b e. p ( y e. ( x i a ) /\ z e. ( x i b ) /\ v e. ( a i b ) ) ) }

This definition is referenced by:  istrkge  25356