df-trkge

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

		Ref	Expression
	Assertion	df-trkge	$⊢ 𝒢_{Tarski}^{E} = \{f \| \underset{˙}{[} {Base}_{f} / p \underset{˙}{]} \underset{˙}{[} Itv (f) / i \underset{˙}{]} \forall x \in p \forall y \in p \forall z \in p \forall u \in p \forall v \in p ((u \in (x i v) \land u \in (y i z) \land x \neq u) \to \exists a \in p \exists b \in p (y \in (x i a) \land z \in (x i b) \land v \in (a i b)))\}$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cstrkge	$class 𝒢_{Tarski}^{E}$
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		citv	$class Itv$
7	3 6	cfv	$class Itv (f)$
8		vi	$setvar i$
9		vx	$setvar x$
10	5	cv	$setvar p$
11		vy	$setvar y$
12		vz	$setvar z$
13		vu	$setvar u$
14		vv	$setvar v$
15	13	cv	$setvar u$
16	9	cv	$setvar x$
17	8	cv	$setvar i$
18	14	cv	$setvar v$
19	16 18 17	co	$class (x i v)$
20	15 19	wcel	$wff u \in (x i v)$
21	11	cv	$setvar y$
22	12	cv	$setvar z$
23	21 22 17	co	$class (y i z)$
24	15 23	wcel	$wff u \in (y i z)$
25	16 15	wne	$wff x \neq u$
26	20 24 25	w3a	$wff (u \in (x i v) \land u \in (y i z) \land x \neq u)$
27		va	$setvar a$
28		vb	$setvar b$
29	27	cv	$setvar a$
30	16 29 17	co	$class (x i a)$
31	21 30	wcel	$wff y \in (x i a)$
32	28	cv	$setvar b$
33	16 32 17	co	$class (x i b)$
34	22 33	wcel	$wff z \in (x i b)$
35	29 32 17	co	$class (a i b)$
36	18 35	wcel	$wff v \in (a i b)$
37	31 34 36	w3a	$wff (y \in (x i a) \land z \in (x i b) \land v \in (a i b))$
38	37 28 10	wrex	$wff \exists b \in p (y \in (x i a) \land z \in (x i b) \land v \in (a i b))$
39	38 27 10	wrex	$wff \exists a \in p \exists b \in p (y \in (x i a) \land z \in (x i b) \land v \in (a i b))$
40	26 39	wi	$wff ((u \in (x i v) \land u \in (y i z) \land x \neq u) \to \exists a \in p \exists b \in p (y \in (x i a) \land z \in (x i b) \land v \in (a i b)))$
41	40 14 10	wral	$wff \forall v \in p ((u \in (x i v) \land u \in (y i z) \land x \neq u) \to \exists a \in p \exists b \in p (y \in (x i a) \land z \in (x i b) \land v \in (a i b)))$
42	41 13 10	wral	$wff \forall u \in p \forall v \in p ((u \in (x i v) \land u \in (y i z) \land x \neq u) \to \exists a \in p \exists b \in p (y \in (x i a) \land z \in (x i b) \land v \in (a i b)))$
43	42 12 10	wral	$wff \forall z \in p \forall u \in p \forall v \in p ((u \in (x i v) \land u \in (y i z) \land x \neq u) \to \exists a \in p \exists b \in p (y \in (x i a) \land z \in (x i b) \land v \in (a i b)))$
44	43 11 10	wral	$wff \forall y \in p \forall z \in p \forall u \in p \forall v \in p ((u \in (x i v) \land u \in (y i z) \land x \neq u) \to \exists a \in p \exists b \in p (y \in (x i a) \land z \in (x i b) \land v \in (a i b)))$
45	44 9 10	wral	$wff \forall x \in p \forall y \in p \forall z \in p \forall u \in p \forall v \in p ((u \in (x i v) \land u \in (y i z) \land x \neq u) \to \exists a \in p \exists b \in p (y \in (x i a) \land z \in (x i b) \land v \in (a i b)))$
46	45 8 7	wsbc	$wff \underset{˙}{[} Itv (f) / i \underset{˙}{]} \forall x \in p \forall y \in p \forall z \in p \forall u \in p \forall v \in p ((u \in (x i v) \land u \in (y i z) \land x \neq u) \to \exists a \in p \exists b \in p (y \in (x i a) \land z \in (x i b) \land v \in (a i b)))$
47	46 5 4	wsbc	$wff \underset{˙}{[} {Base}_{f} / p \underset{˙}{]} \underset{˙}{[} Itv (f) / i \underset{˙}{]} \forall x \in p \forall y \in p \forall z \in p \forall u \in p \forall v \in p ((u \in (x i v) \land u \in (y i z) \land x \neq u) \to \exists a \in p \exists b \in p (y \in (x i a) \land z \in (x i b) \land v \in (a i b)))$
48	47 1	cab	$class \{f \| \underset{˙}{[} {Base}_{f} / p \underset{˙}{]} \underset{˙}{[} Itv (f) / i \underset{˙}{]} \forall x \in p \forall y \in p \forall z \in p \forall u \in p \forall v \in p ((u \in (x i v) \land u \in (y i z) \land x \neq u) \to \exists a \in p \exists b \in p (y \in (x i a) \land z \in (x i b) \land v \in (a i b)))\}$
49	0 48	wceq	$wff 𝒢_{Tarski}^{E} = \{f \| \underset{˙}{[} {Base}_{f} / p \underset{˙}{]} \underset{˙}{[} Itv (f) / i \underset{˙}{]} \forall x \in p \forall y \in p \forall z \in p \forall u \in p \forall v \in p ((u \in (x i v) \land u \in (y i z) \land x \neq u) \to \exists a \in p \exists b \in p (y \in (x i a) \land z \in (x i b) \land v \in (a i b)))\}$

Metamath Proof Explorer

Definition df-trkge

Detailed syntax breakdown