df-leg

Description: Define the less-than relationship between geometric distance congruence classes. See legval . (Contributed by Thierry Arnoux, 21-Jun-2019)

		Ref	Expression
	Assertion	df-leg	$⊢ \leq_{𝒢} = (g \in V ⟼ \{⟨e, f⟩ \| \underset{˙}{[} {Base}_{g} / p \underset{˙}{]} \underset{˙}{[} dist (g) / d \underset{˙}{]} \underset{˙}{[} Itv (g) / i \underset{˙}{]} \exists x \in p \exists y \in p (f = x d y \land \exists z \in p (z \in (x i y) \land e = x d z))\})$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cleg	$class \leq_{𝒢}$
1		vg	$setvar g$
2		cvv	$class V$
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		vd	$setvar d$
12		citv	$class Itv$
13	6 12	cfv	$class Itv (g)$
14		vi	$setvar i$
15		vx	$setvar x$
16	8	cv	$setvar p$
17		vy	$setvar y$
18	4	cv	$setvar f$
19	15	cv	$setvar x$
20	11	cv	$setvar d$
21	17	cv	$setvar y$
22	19 21 20	co	$class (x d y)$
23	18 22	wceq	$wff f = x d y$
24		vz	$setvar z$
25	24	cv	$setvar z$
26	14	cv	$setvar i$
27	19 21 26	co	$class (x i y)$
28	25 27	wcel	$wff z \in (x i y)$
29	3	cv	$setvar e$
30	19 25 20	co	$class (x d z)$
31	29 30	wceq	$wff e = x d z$
32	28 31	wa	$wff (z \in (x i y) \land e = x d z)$
33	32 24 16	wrex	$wff \exists z \in p (z \in (x i y) \land e = x d z)$
34	23 33	wa	$wff (f = x d y \land \exists z \in p (z \in (x i y) \land e = x d z))$
35	34 17 16	wrex	$wff \exists y \in p (f = x d y \land \exists z \in p (z \in (x i y) \land e = x d z))$
36	35 15 16	wrex	$wff \exists x \in p \exists y \in p (f = x d y \land \exists z \in p (z \in (x i y) \land e = x d z))$
37	36 14 13	wsbc	$wff \underset{˙}{[} Itv (g) / i \underset{˙}{]} \exists x \in p \exists y \in p (f = x d y \land \exists z \in p (z \in (x i y) \land e = x d z))$
38	37 11 10	wsbc	$wff \underset{˙}{[} dist (g) / d \underset{˙}{]} \underset{˙}{[} Itv (g) / i \underset{˙}{]} \exists x \in p \exists y \in p (f = x d y \land \exists z \in p (z \in (x i y) \land e = x d z))$
39	38 8 7	wsbc	$wff \underset{˙}{[} {Base}_{g} / p \underset{˙}{]} \underset{˙}{[} dist (g) / d \underset{˙}{]} \underset{˙}{[} Itv (g) / i \underset{˙}{]} \exists x \in p \exists y \in p (f = x d y \land \exists z \in p (z \in (x i y) \land e = x d z))$
40	39 3 4	copab	$class \{⟨e, f⟩ \| \underset{˙}{[} {Base}_{g} / p \underset{˙}{]} \underset{˙}{[} dist (g) / d \underset{˙}{]} \underset{˙}{[} Itv (g) / i \underset{˙}{]} \exists x \in p \exists y \in p (f = x d y \land \exists z \in p (z \in (x i y) \land e = x d z))\}$
41	1 2 40	cmpt	$class (g \in V ⟼ \{⟨e, f⟩ \| \underset{˙}{[} {Base}_{g} / p \underset{˙}{]} \underset{˙}{[} dist (g) / d \underset{˙}{]} \underset{˙}{[} Itv (g) / i \underset{˙}{]} \exists x \in p \exists y \in p (f = x d y \land \exists z \in p (z \in (x i y) \land e = x d z))\})$
42	0 41	wceq	$wff \leq_{𝒢} = (g \in V ⟼ \{⟨e, f⟩ \| \underset{˙}{[} {Base}_{g} / p \underset{˙}{]} \underset{˙}{[} dist (g) / d \underset{˙}{]} \underset{˙}{[} Itv (g) / i \underset{˙}{]} \exists x \in p \exists y \in p (f = x d y \land \exists z \in p (z \in (x i y) \land e = x d z))\})$

Metamath Proof Explorer

Definition df-leg

Detailed syntax breakdown