Definition df-leg 25478

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

Assertion

Ref	Expression
df-leg	|- ≤G = ( g e. _V |-> { <. e , f >. | [. ( Base ` g ) / p ]. [. ( dist ` g ) / d ]. [. (Itv ` g ) / i ]. E. x e. p E. y e. p ( f = ( x d y ) /\ E. z e. p ( z e. ( x i y ) /\ e = ( x d z ) ) ) } )

Distinct variable group:   e, d, f, g, i, p, x, y, z

Detailed syntax breakdown of Definition df-leg

Step	Hyp	Ref	Expression
1		cleg 25477	. 2 class ≤G
2		vg	. . 3 setvar g
3		cvv 3200	. . 3 class _V
4		vf	. . . . . . . . . . . 12 setvar f
5	4	cv 1482	. . . . . . . . . . 11 class f
6		vx	. . . . . . . . . . . . 13 setvar x
7	6	cv 1482	. . . . . . . . . . . 12 class x
8		vy	. . . . . . . . . . . . 13 setvar y
9	8	cv 1482	. . . . . . . . . . . 12 class y
10		vd	. . . . . . . . . . . . 13 setvar d
11	10	cv 1482	. . . . . . . . . . . 12 class d
12	7, 9, 11	co 6650	. . . . . . . . . . 11 class ( x d y )
13	5, 12	wceq 1483	. . . . . . . . . 10 wff f = ( x d y )
14		vz	. . . . . . . . . . . . . 14 setvar z
15	14	cv 1482	. . . . . . . . . . . . 13 class z
16		vi	. . . . . . . . . . . . . . 15 setvar i
17	16	cv 1482	. . . . . . . . . . . . . 14 class i
18	7, 9, 17	co 6650	. . . . . . . . . . . . 13 class ( x i y )
19	15, 18	wcel 1990	. . . . . . . . . . . 12 wff z e. ( x i y )
20		ve	. . . . . . . . . . . . . 14 setvar e
21	20	cv 1482	. . . . . . . . . . . . 13 class e
22	7, 15, 11	co 6650	. . . . . . . . . . . . 13 class ( x d z )
23	21, 22	wceq 1483	. . . . . . . . . . . 12 wff e = ( x d z )
24	19, 23	wa 384	. . . . . . . . . . 11 wff ( z e. ( x i y ) /\ e = ( x d z ) )
25		vp	. . . . . . . . . . . 12 setvar p
26	25	cv 1482	. . . . . . . . . . 11 class p
27	24, 14, 26	wrex 2913	. . . . . . . . . 10 wff E. z e. p ( z e. ( x i y ) /\ e = ( x d z ) )
28	13, 27	wa 384	. . . . . . . . 9 wff ( f = ( x d y ) /\ E. z e. p ( z e. ( x i y ) /\ e = ( x d z ) ) )
29	28, 8, 26	wrex 2913	. . . . . . . 8 wff E. y e. p ( f = ( x d y ) /\ E. z e. p ( z e. ( x i y ) /\ e = ( x d z ) ) )
30	29, 6, 26	wrex 2913	. . . . . . 7 wff E. x e. p E. y e. p ( f = ( x d y ) /\ E. z e. p ( z e. ( x i y ) /\ e = ( x d z ) ) )
31	2	cv 1482	. . . . . . . 8 class g
32		citv 25335	. . . . . . . 8 class Itv
33	31, 32	cfv 5888	. . . . . . 7 class (Itv ` g )
34	30, 16, 33	wsbc 3435	. . . . . 6 wff [. (Itv ` g ) / i ]. E. x e. p E. y e. p ( f = ( x d y ) /\ E. z e. p ( z e. ( x i y ) /\ e = ( x d z ) ) )
35		cds 15950	. . . . . . 7 class dist
36	31, 35	cfv 5888	. . . . . 6 class ( dist ` g )
37	34, 10, 36	wsbc 3435	. . . . 5 wff [. ( dist ` g ) / d ]. [. (Itv ` g ) / i ]. E. x e. p E. y e. p ( f = ( x d y ) /\ E. z e. p ( z e. ( x i y ) /\ e = ( x d z ) ) )
38		cbs 15857	. . . . . 6 class Base
39	31, 38	cfv 5888	. . . . 5 class ( Base ` g )
40	37, 25, 39	wsbc 3435	. . . 4 wff [. ( Base ` g ) / p ]. [. ( dist ` g ) / d ]. [. (Itv ` g ) / i ]. E. x e. p E. y e. p ( f = ( x d y ) /\ E. z e. p ( z e. ( x i y ) /\ e = ( x d z ) ) )
41	40, 20, 4	copab 4712	. . 3 class { <. e , f >. | [. ( Base ` g ) / p ]. [. ( dist ` g ) / d ]. [. (Itv ` g ) / i ]. E. x e. p E. y e. p ( f = ( x d y ) /\ E. z e. p ( z e. ( x i y ) /\ e = ( x d z ) ) ) }
42	2, 3, 41	cmpt 4729	. 2 class ( g e. _V |-> { <. e , f >. | [. ( Base ` g ) / p ]. [. ( dist ` g ) / d ]. [. (Itv ` g ) / i ]. E. x e. p E. y e. p ( f = ( x d y ) /\ E. z e. p ( z e. ( x i y ) /\ e = ( x d z ) ) ) } )
43	1, 42	wceq 1483	1 wff ≤G = ( g e. _V |-> { <. e , f >. | [. ( Base ` g ) / p ]. [. ( dist ` g ) / d ]. [. (Itv ` g ) / i ]. E. x e. p E. y e. p ( f = ( x d y ) /\ E. z e. p ( z e. ( x i y ) /\ e = ( x d z ) ) ) } )

This definition is referenced by:  legval  25479