Definition df-trkg2d 30743

Description: Define the class of geometries fulfilling the lower dimension axiom, Axiom A8 of [Schwabhauser] p. 12, and the upper dimension axiom, Axiom A9 of [Schwabhauser] p. 13, for dimension 2. (Contributed by Thierry Arnoux, 14-Mar-2019.) (New usage is discouraged.)

Assertion

Ref	Expression
df-trkg2d	|- TarskiG2D = { f | [. ( Base ` f ) / p ]. [. ( dist ` f ) / d ]. [. (Itv ` f ) / i ]. ( E. x e. p E. y e. p E. z e. p -. ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) /\ A. x e. p A. y e. p A. z e. p A. u e. p A. v e. p ( ( ( ( x d u ) = ( x d v ) /\ ( y d u ) = ( y d v ) /\ ( z d u ) = ( z d v ) ) /\ u =/= v ) -> ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) ) ) }

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

Detailed syntax breakdown of Definition df-trkg2d

Step	Hyp	Ref	Expression
1		cstrkg2d 30742	. 2 class TarskiG2D
2		vz	. . . . . . . . . . . . . 14 setvar z
3	2	cv 1482	. . . . . . . . . . . . 13 class z
4		vx	. . . . . . . . . . . . . . 15 setvar x
5	4	cv 1482	. . . . . . . . . . . . . 14 class x
6		vy	. . . . . . . . . . . . . . 15 setvar y
7	6	cv 1482	. . . . . . . . . . . . . 14 class y
8		vi	. . . . . . . . . . . . . . 15 setvar i
9	8	cv 1482	. . . . . . . . . . . . . 14 class i
10	5, 7, 9	co 6650	. . . . . . . . . . . . 13 class ( x i y )
11	3, 10	wcel 1990	. . . . . . . . . . . 12 wff z e. ( x i y )
12	3, 7, 9	co 6650	. . . . . . . . . . . . 13 class ( z i y )
13	5, 12	wcel 1990	. . . . . . . . . . . 12 wff x e. ( z i y )
14	5, 3, 9	co 6650	. . . . . . . . . . . . 13 class ( x i z )
15	7, 14	wcel 1990	. . . . . . . . . . . 12 wff y e. ( x i z )
16	11, 13, 15	w3o 1036	. . . . . . . . . . 11 wff ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) )
17	16	wn 3	. . . . . . . . . 10 wff -. ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) )
18		vp	. . . . . . . . . . 11 setvar p
19	18	cv 1482	. . . . . . . . . 10 class p
20	17, 2, 19	wrex 2913	. . . . . . . . 9 wff E. z e. p -. ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) )
21	20, 6, 19	wrex 2913	. . . . . . . 8 wff E. y e. p E. z e. p -. ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) )
22	21, 4, 19	wrex 2913	. . . . . . 7 wff E. x e. p E. y e. p E. z e. p -. ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) )
23		vu	. . . . . . . . . . . . . . . . . 18 setvar u
24	23	cv 1482	. . . . . . . . . . . . . . . . 17 class u
25		vd	. . . . . . . . . . . . . . . . . 18 setvar d
26	25	cv 1482	. . . . . . . . . . . . . . . . 17 class d
27	5, 24, 26	co 6650	. . . . . . . . . . . . . . . 16 class ( x d u )
28		vv	. . . . . . . . . . . . . . . . . 18 setvar v
29	28	cv 1482	. . . . . . . . . . . . . . . . 17 class v
30	5, 29, 26	co 6650	. . . . . . . . . . . . . . . 16 class ( x d v )
31	27, 30	wceq 1483	. . . . . . . . . . . . . . 15 wff ( x d u ) = ( x d v )
32	7, 24, 26	co 6650	. . . . . . . . . . . . . . . 16 class ( y d u )
33	7, 29, 26	co 6650	. . . . . . . . . . . . . . . 16 class ( y d v )
34	32, 33	wceq 1483	. . . . . . . . . . . . . . 15 wff ( y d u ) = ( y d v )
35	3, 24, 26	co 6650	. . . . . . . . . . . . . . . 16 class ( z d u )
36	3, 29, 26	co 6650	. . . . . . . . . . . . . . . 16 class ( z d v )
37	35, 36	wceq 1483	. . . . . . . . . . . . . . 15 wff ( z d u ) = ( z d v )
38	31, 34, 37	w3a 1037	. . . . . . . . . . . . . 14 wff ( ( x d u ) = ( x d v ) /\ ( y d u ) = ( y d v ) /\ ( z d u ) = ( z d v ) )
39	24, 29	wne 2794	. . . . . . . . . . . . . 14 wff u =/= v
40	38, 39	wa 384	. . . . . . . . . . . . 13 wff ( ( ( x d u ) = ( x d v ) /\ ( y d u ) = ( y d v ) /\ ( z d u ) = ( z d v ) ) /\ u =/= v )
41	40, 16	wi 4	. . . . . . . . . . . 12 wff ( ( ( ( x d u ) = ( x d v ) /\ ( y d u ) = ( y d v ) /\ ( z d u ) = ( z d v ) ) /\ u =/= v ) -> ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) )
42	41, 28, 19	wral 2912	. . . . . . . . . . 11 wff A. v e. p ( ( ( ( x d u ) = ( x d v ) /\ ( y d u ) = ( y d v ) /\ ( z d u ) = ( z d v ) ) /\ u =/= v ) -> ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) )
43	42, 23, 19	wral 2912	. . . . . . . . . 10 wff A. u e. p A. v e. p ( ( ( ( x d u ) = ( x d v ) /\ ( y d u ) = ( y d v ) /\ ( z d u ) = ( z d v ) ) /\ u =/= v ) -> ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) )
44	43, 2, 19	wral 2912	. . . . . . . . 9 wff A. z e. p A. u e. p A. v e. p ( ( ( ( x d u ) = ( x d v ) /\ ( y d u ) = ( y d v ) /\ ( z d u ) = ( z d v ) ) /\ u =/= v ) -> ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) )
45	44, 6, 19	wral 2912	. . . . . . . 8 wff A. y e. p A. z e. p A. u e. p A. v e. p ( ( ( ( x d u ) = ( x d v ) /\ ( y d u ) = ( y d v ) /\ ( z d u ) = ( z d v ) ) /\ u =/= v ) -> ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) )
46	45, 4, 19	wral 2912	. . . . . . 7 wff A. x e. p A. y e. p A. z e. p A. u e. p A. v e. p ( ( ( ( x d u ) = ( x d v ) /\ ( y d u ) = ( y d v ) /\ ( z d u ) = ( z d v ) ) /\ u =/= v ) -> ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) )
47	22, 46	wa 384	. . . . . 6 wff ( E. x e. p E. y e. p E. z e. p -. ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) /\ A. x e. p A. y e. p A. z e. p A. u e. p A. v e. p ( ( ( ( x d u ) = ( x d v ) /\ ( y d u ) = ( y d v ) /\ ( z d u ) = ( z d v ) ) /\ u =/= v ) -> ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) ) )
48		vf	. . . . . . . 8 setvar f
49	48	cv 1482	. . . . . . 7 class f
50		citv 25335	. . . . . . 7 class Itv
51	49, 50	cfv 5888	. . . . . 6 class (Itv ` f )
52	47, 8, 51	wsbc 3435	. . . . 5 wff [. (Itv ` f ) / i ]. ( E. x e. p E. y e. p E. z e. p -. ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) /\ A. x e. p A. y e. p A. z e. p A. u e. p A. v e. p ( ( ( ( x d u ) = ( x d v ) /\ ( y d u ) = ( y d v ) /\ ( z d u ) = ( z d v ) ) /\ u =/= v ) -> ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) ) )
53		cds 15950	. . . . . 6 class dist
54	49, 53	cfv 5888	. . . . 5 class ( dist ` f )
55	52, 25, 54	wsbc 3435	. . . 4 wff [. ( dist ` f ) / d ]. [. (Itv ` f ) / i ]. ( E. x e. p E. y e. p E. z e. p -. ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) /\ A. x e. p A. y e. p A. z e. p A. u e. p A. v e. p ( ( ( ( x d u ) = ( x d v ) /\ ( y d u ) = ( y d v ) /\ ( z d u ) = ( z d v ) ) /\ u =/= v ) -> ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) ) )
56		cbs 15857	. . . . 5 class Base
57	49, 56	cfv 5888	. . . 4 class ( Base ` f )
58	55, 18, 57	wsbc 3435	. . 3 wff [. ( Base ` f ) / p ]. [. ( dist ` f ) / d ]. [. (Itv ` f ) / i ]. ( E. x e. p E. y e. p E. z e. p -. ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) /\ A. x e. p A. y e. p A. z e. p A. u e. p A. v e. p ( ( ( ( x d u ) = ( x d v ) /\ ( y d u ) = ( y d v ) /\ ( z d u ) = ( z d v ) ) /\ u =/= v ) -> ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) ) )
59	58, 48	cab 2608	. 2 class { f | [. ( Base ` f ) / p ]. [. ( dist ` f ) / d ]. [. (Itv ` f ) / i ]. ( E. x e. p E. y e. p E. z e. p -. ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) /\ A. x e. p A. y e. p A. z e. p A. u e. p A. v e. p ( ( ( ( x d u ) = ( x d v ) /\ ( y d u ) = ( y d v ) /\ ( z d u ) = ( z d v ) ) /\ u =/= v ) -> ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) ) ) }
60	1, 59	wceq 1483	1 wff TarskiG2D = { f | [. ( Base ` f ) / p ]. [. ( dist ` f ) / d ]. [. (Itv ` f ) / i ]. ( E. x e. p E. y e. p E. z e. p -. ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) /\ A. x e. p A. y e. p A. z e. p A. u e. p A. v e. p ( ( ( ( x d u ) = ( x d v ) /\ ( y d u ) = ( y d v ) /\ ( z d u ) = ( z d v ) ) /\ u =/= v ) -> ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) ) ) }

This definition is referenced by:  istrkg2d  30744