df-trkg2d

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.)

		Ref	Expression
	Assertion	df-trkg2d	$⊢ 𝒢_{Tarski}^{2D} = \{f \| \underset{˙}{[} {Base}_{f} / p \underset{˙}{]} \underset{˙}{[} dist (f) / d \underset{˙}{]} \underset{˙}{[} Itv (f) / i \underset{˙}{]} (\exists x \in p \exists y \in p \exists z \in p \neg (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z)) \land \forall x \in p \forall y \in p \forall z \in p \forall u \in p \forall v \in p (((x d u = x d v \land y d u = y d v \land z d u = z d v) \land u \neq v) \to (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z))))\}$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cstrkg2d	$class 𝒢_{Tarski}^{2D}$
1		vf	$setvar f$
2		cbs	$class Base$
3	1	cv	$setvar f$
4	3 2	cfv	$class {Base}_{f}$
5		vp	$setvar p$
6		cds	$class dist$
7	3 6	cfv	$class dist (f)$
8		vd	$setvar d$
9		citv	$class Itv$
10	3 9	cfv	$class Itv (f)$
11		vi	$setvar i$
12		vx	$setvar x$
13	5	cv	$setvar p$
14		vy	$setvar y$
15		vz	$setvar z$
16	15	cv	$setvar z$
17	12	cv	$setvar x$
18	11	cv	$setvar i$
19	14	cv	$setvar y$
20	17 19 18	co	$class (x i y)$
21	16 20	wcel	$wff z \in (x i y)$
22	16 19 18	co	$class (z i y)$
23	17 22	wcel	$wff x \in (z i y)$
24	17 16 18	co	$class (x i z)$
25	19 24	wcel	$wff y \in (x i z)$
26	21 23 25	w3o	$wff (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z))$
27	26	wn	$wff \neg (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z))$
28	27 15 13	wrex	$wff \exists z \in p \neg (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z))$
29	28 14 13	wrex	$wff \exists y \in p \exists z \in p \neg (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z))$
30	29 12 13	wrex	$wff \exists x \in p \exists y \in p \exists z \in p \neg (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z))$
31		vu	$setvar u$
32		vv	$setvar v$
33	8	cv	$setvar d$
34	31	cv	$setvar u$
35	17 34 33	co	$class (x d u)$
36	32	cv	$setvar v$
37	17 36 33	co	$class (x d v)$
38	35 37	wceq	$wff x d u = x d v$
39	19 34 33	co	$class (y d u)$
40	19 36 33	co	$class (y d v)$
41	39 40	wceq	$wff y d u = y d v$
42	16 34 33	co	$class (z d u)$
43	16 36 33	co	$class (z d v)$
44	42 43	wceq	$wff z d u = z d v$
45	38 41 44	w3a	$wff (x d u = x d v \land y d u = y d v \land z d u = z d v)$
46	34 36	wne	$wff u \neq v$
47	45 46	wa	$wff ((x d u = x d v \land y d u = y d v \land z d u = z d v) \land u \neq v)$
48	47 26	wi	$wff (((x d u = x d v \land y d u = y d v \land z d u = z d v) \land u \neq v) \to (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z)))$
49	48 32 13	wral	$wff \forall v \in p (((x d u = x d v \land y d u = y d v \land z d u = z d v) \land u \neq v) \to (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z)))$
50	49 31 13	wral	$wff \forall u \in p \forall v \in p (((x d u = x d v \land y d u = y d v \land z d u = z d v) \land u \neq v) \to (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z)))$
51	50 15 13	wral	$wff \forall z \in p \forall u \in p \forall v \in p (((x d u = x d v \land y d u = y d v \land z d u = z d v) \land u \neq v) \to (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z)))$
52	51 14 13	wral	$wff \forall y \in p \forall z \in p \forall u \in p \forall v \in p (((x d u = x d v \land y d u = y d v \land z d u = z d v) \land u \neq v) \to (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z)))$
53	52 12 13	wral	$wff \forall x \in p \forall y \in p \forall z \in p \forall u \in p \forall v \in p (((x d u = x d v \land y d u = y d v \land z d u = z d v) \land u \neq v) \to (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z)))$
54	30 53	wa	$wff (\exists x \in p \exists y \in p \exists z \in p \neg (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z)) \land \forall x \in p \forall y \in p \forall z \in p \forall u \in p \forall v \in p (((x d u = x d v \land y d u = y d v \land z d u = z d v) \land u \neq v) \to (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z))))$
55	54 11 10	wsbc	$wff \underset{˙}{[} Itv (f) / i \underset{˙}{]} (\exists x \in p \exists y \in p \exists z \in p \neg (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z)) \land \forall x \in p \forall y \in p \forall z \in p \forall u \in p \forall v \in p (((x d u = x d v \land y d u = y d v \land z d u = z d v) \land u \neq v) \to (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z))))$
56	55 8 7	wsbc	$wff \underset{˙}{[} dist (f) / d \underset{˙}{]} \underset{˙}{[} Itv (f) / i \underset{˙}{]} (\exists x \in p \exists y \in p \exists z \in p \neg (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z)) \land \forall x \in p \forall y \in p \forall z \in p \forall u \in p \forall v \in p (((x d u = x d v \land y d u = y d v \land z d u = z d v) \land u \neq v) \to (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z))))$
57	56 5 4	wsbc	$wff \underset{˙}{[} {Base}_{f} / p \underset{˙}{]} \underset{˙}{[} dist (f) / d \underset{˙}{]} \underset{˙}{[} Itv (f) / i \underset{˙}{]} (\exists x \in p \exists y \in p \exists z \in p \neg (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z)) \land \forall x \in p \forall y \in p \forall z \in p \forall u \in p \forall v \in p (((x d u = x d v \land y d u = y d v \land z d u = z d v) \land u \neq v) \to (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z))))$
58	57 1	cab	$class \{f \| \underset{˙}{[} {Base}_{f} / p \underset{˙}{]} \underset{˙}{[} dist (f) / d \underset{˙}{]} \underset{˙}{[} Itv (f) / i \underset{˙}{]} (\exists x \in p \exists y \in p \exists z \in p \neg (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z)) \land \forall x \in p \forall y \in p \forall z \in p \forall u \in p \forall v \in p (((x d u = x d v \land y d u = y d v \land z d u = z d v) \land u \neq v) \to (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z))))\}$
59	0 58	wceq	$wff 𝒢_{Tarski}^{2D} = \{f \| \underset{˙}{[} {Base}_{f} / p \underset{˙}{]} \underset{˙}{[} dist (f) / d \underset{˙}{]} \underset{˙}{[} Itv (f) / i \underset{˙}{]} (\exists x \in p \exists y \in p \exists z \in p \neg (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z)) \land \forall x \in p \forall y \in p \forall z \in p \forall u \in p \forall v \in p (((x d u = x d v \land y d u = y d v \land z d u = z d v) \land u \neq v) \to (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z))))\}$

Metamath Proof Explorer

Definition df-trkg2d

Detailed syntax breakdown