df-afs

Description: The outer five segment configuration is an abbreviation for the conditions of the Five Segment Axiom ( axtg5seg ). See df-ofs . Definition 2.10 of Schwabhauser p. 28. (Contributed by Scott Fenton, 21-Sep-2013) (Revised by Thierry Arnoux, 15-Mar-2019)

		Ref	Expression
	Assertion	df-afs	$⊢ AFS = (g \in 𝒢_{Tarski} ⟼ \{⟨e, f⟩ \| \underset{˙}{[} {Base}_{g} / p \underset{˙}{]} \underset{˙}{[} dist (g) / h \underset{˙}{]} \underset{˙}{[} Itv (g) / i \underset{˙}{]} \exists a \in p \exists b \in p \exists c \in p \exists d \in p \exists x \in p \exists y \in p \exists z \in p \exists w \in p (e = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land f = ⟨⟨x, y⟩, ⟨z, w⟩⟩ \land ((b \in (a i c) \land y \in (x i z)) \land (a h b = x h y \land b h c = y h z) \land (a h d = x h w \land b h d = y h w)))\})$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cafs	$class AFS$
1		vg	$setvar g$
2		cstrkg	$class 𝒢_{Tarski}$
3		ve	$setvar e$
4		vf	$setvar f$
5		cbs	$class Base$
6	1	cv	$setvar g$
7	6 5	cfv	$class {Base}_{g}$
8		vp	$setvar p$
9		cds	$class dist$
10	6 9	cfv	$class dist (g)$
11		vh	$setvar h$
12		citv	$class Itv$
13	6 12	cfv	$class Itv (g)$
14		vi	$setvar i$
15		va	$setvar a$
16	8	cv	$setvar p$
17		vb	$setvar b$
18		vc	$setvar c$
19		vd	$setvar d$
20		vx	$setvar x$
21		vy	$setvar y$
22		vz	$setvar z$
23		vw	$setvar w$
24	3	cv	$setvar e$
25	15	cv	$setvar a$
26	17	cv	$setvar b$
27	25 26	cop	$class ⟨a, b⟩$
28	18	cv	$setvar c$
29	19	cv	$setvar d$
30	28 29	cop	$class ⟨c, d⟩$
31	27 30	cop	$class ⟨⟨a, b⟩, ⟨c, d⟩⟩$
32	24 31	wceq	$wff e = ⟨⟨a, b⟩, ⟨c, d⟩⟩$
33	4	cv	$setvar f$
34	20	cv	$setvar x$
35	21	cv	$setvar y$
36	34 35	cop	$class ⟨x, y⟩$
37	22	cv	$setvar z$
38	23	cv	$setvar w$
39	37 38	cop	$class ⟨z, w⟩$
40	36 39	cop	$class ⟨⟨x, y⟩, ⟨z, w⟩⟩$
41	33 40	wceq	$wff f = ⟨⟨x, y⟩, ⟨z, w⟩⟩$
42	14	cv	$setvar i$
43	25 28 42	co	$class (a i c)$
44	26 43	wcel	$wff b \in (a i c)$
45	34 37 42	co	$class (x i z)$
46	35 45	wcel	$wff y \in (x i z)$
47	44 46	wa	$wff (b \in (a i c) \land y \in (x i z))$
48	11	cv	$setvar h$
49	25 26 48	co	$class (a h b)$
50	34 35 48	co	$class (x h y)$
51	49 50	wceq	$wff a h b = x h y$
52	26 28 48	co	$class (b h c)$
53	35 37 48	co	$class (y h z)$
54	52 53	wceq	$wff b h c = y h z$
55	51 54	wa	$wff (a h b = x h y \land b h c = y h z)$
56	25 29 48	co	$class (a h d)$
57	34 38 48	co	$class (x h w)$
58	56 57	wceq	$wff a h d = x h w$
59	26 29 48	co	$class (b h d)$
60	35 38 48	co	$class (y h w)$
61	59 60	wceq	$wff b h d = y h w$
62	58 61	wa	$wff (a h d = x h w \land b h d = y h w)$
63	47 55 62	w3a	$wff ((b \in (a i c) \land y \in (x i z)) \land (a h b = x h y \land b h c = y h z) \land (a h d = x h w \land b h d = y h w))$
64	32 41 63	w3a	$wff (e = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land f = ⟨⟨x, y⟩, ⟨z, w⟩⟩ \land ((b \in (a i c) \land y \in (x i z)) \land (a h b = x h y \land b h c = y h z) \land (a h d = x h w \land b h d = y h w)))$
65	64 23 16	wrex	$wff \exists w \in p (e = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land f = ⟨⟨x, y⟩, ⟨z, w⟩⟩ \land ((b \in (a i c) \land y \in (x i z)) \land (a h b = x h y \land b h c = y h z) \land (a h d = x h w \land b h d = y h w)))$
66	65 22 16	wrex	$wff \exists z \in p \exists w \in p (e = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land f = ⟨⟨x, y⟩, ⟨z, w⟩⟩ \land ((b \in (a i c) \land y \in (x i z)) \land (a h b = x h y \land b h c = y h z) \land (a h d = x h w \land b h d = y h w)))$
67	66 21 16	wrex	$wff \exists y \in p \exists z \in p \exists w \in p (e = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land f = ⟨⟨x, y⟩, ⟨z, w⟩⟩ \land ((b \in (a i c) \land y \in (x i z)) \land (a h b = x h y \land b h c = y h z) \land (a h d = x h w \land b h d = y h w)))$
68	67 20 16	wrex	$wff \exists x \in p \exists y \in p \exists z \in p \exists w \in p (e = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land f = ⟨⟨x, y⟩, ⟨z, w⟩⟩ \land ((b \in (a i c) \land y \in (x i z)) \land (a h b = x h y \land b h c = y h z) \land (a h d = x h w \land b h d = y h w)))$
69	68 19 16	wrex	$wff \exists d \in p \exists x \in p \exists y \in p \exists z \in p \exists w \in p (e = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land f = ⟨⟨x, y⟩, ⟨z, w⟩⟩ \land ((b \in (a i c) \land y \in (x i z)) \land (a h b = x h y \land b h c = y h z) \land (a h d = x h w \land b h d = y h w)))$
70	69 18 16	wrex	$wff \exists c \in p \exists d \in p \exists x \in p \exists y \in p \exists z \in p \exists w \in p (e = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land f = ⟨⟨x, y⟩, ⟨z, w⟩⟩ \land ((b \in (a i c) \land y \in (x i z)) \land (a h b = x h y \land b h c = y h z) \land (a h d = x h w \land b h d = y h w)))$
71	70 17 16	wrex	$wff \exists b \in p \exists c \in p \exists d \in p \exists x \in p \exists y \in p \exists z \in p \exists w \in p (e = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land f = ⟨⟨x, y⟩, ⟨z, w⟩⟩ \land ((b \in (a i c) \land y \in (x i z)) \land (a h b = x h y \land b h c = y h z) \land (a h d = x h w \land b h d = y h w)))$
72	71 15 16	wrex	$wff \exists a \in p \exists b \in p \exists c \in p \exists d \in p \exists x \in p \exists y \in p \exists z \in p \exists w \in p (e = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land f = ⟨⟨x, y⟩, ⟨z, w⟩⟩ \land ((b \in (a i c) \land y \in (x i z)) \land (a h b = x h y \land b h c = y h z) \land (a h d = x h w \land b h d = y h w)))$
73	72 14 13	wsbc	$wff \underset{˙}{[} Itv (g) / i \underset{˙}{]} \exists a \in p \exists b \in p \exists c \in p \exists d \in p \exists x \in p \exists y \in p \exists z \in p \exists w \in p (e = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land f = ⟨⟨x, y⟩, ⟨z, w⟩⟩ \land ((b \in (a i c) \land y \in (x i z)) \land (a h b = x h y \land b h c = y h z) \land (a h d = x h w \land b h d = y h w)))$
74	73 11 10	wsbc	$wff \underset{˙}{[} dist (g) / h \underset{˙}{]} \underset{˙}{[} Itv (g) / i \underset{˙}{]} \exists a \in p \exists b \in p \exists c \in p \exists d \in p \exists x \in p \exists y \in p \exists z \in p \exists w \in p (e = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land f = ⟨⟨x, y⟩, ⟨z, w⟩⟩ \land ((b \in (a i c) \land y \in (x i z)) \land (a h b = x h y \land b h c = y h z) \land (a h d = x h w \land b h d = y h w)))$
75	74 8 7	wsbc	$wff \underset{˙}{[} {Base}_{g} / p \underset{˙}{]} \underset{˙}{[} dist (g) / h \underset{˙}{]} \underset{˙}{[} Itv (g) / i \underset{˙}{]} \exists a \in p \exists b \in p \exists c \in p \exists d \in p \exists x \in p \exists y \in p \exists z \in p \exists w \in p (e = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land f = ⟨⟨x, y⟩, ⟨z, w⟩⟩ \land ((b \in (a i c) \land y \in (x i z)) \land (a h b = x h y \land b h c = y h z) \land (a h d = x h w \land b h d = y h w)))$
76	75 3 4	copab	$class \{⟨e, f⟩ \| \underset{˙}{[} {Base}_{g} / p \underset{˙}{]} \underset{˙}{[} dist (g) / h \underset{˙}{]} \underset{˙}{[} Itv (g) / i \underset{˙}{]} \exists a \in p \exists b \in p \exists c \in p \exists d \in p \exists x \in p \exists y \in p \exists z \in p \exists w \in p (e = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land f = ⟨⟨x, y⟩, ⟨z, w⟩⟩ \land ((b \in (a i c) \land y \in (x i z)) \land (a h b = x h y \land b h c = y h z) \land (a h d = x h w \land b h d = y h w)))\}$
77	1 2 76	cmpt	$class (g \in 𝒢_{Tarski} ⟼ \{⟨e, f⟩ \| \underset{˙}{[} {Base}_{g} / p \underset{˙}{]} \underset{˙}{[} dist (g) / h \underset{˙}{]} \underset{˙}{[} Itv (g) / i \underset{˙}{]} \exists a \in p \exists b \in p \exists c \in p \exists d \in p \exists x \in p \exists y \in p \exists z \in p \exists w \in p (e = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land f = ⟨⟨x, y⟩, ⟨z, w⟩⟩ \land ((b \in (a i c) \land y \in (x i z)) \land (a h b = x h y \land b h c = y h z) \land (a h d = x h w \land b h d = y h w)))\})$
78	0 77	wceq	$wff AFS = (g \in 𝒢_{Tarski} ⟼ \{⟨e, f⟩ \| \underset{˙}{[} {Base}_{g} / p \underset{˙}{]} \underset{˙}{[} dist (g) / h \underset{˙}{]} \underset{˙}{[} Itv (g) / i \underset{˙}{]} \exists a \in p \exists b \in p \exists c \in p \exists d \in p \exists x \in p \exists y \in p \exists z \in p \exists w \in p (e = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land f = ⟨⟨x, y⟩, ⟨z, w⟩⟩ \land ((b \in (a i c) \land y \in (x i z)) \land (a h b = x h y \land b h c = y h z) \land (a h d = x h w \land b h d = y h w)))\})$

Metamath Proof Explorer

Definition df-afs

Detailed syntax breakdown