Definition 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	$$⊢{\le }_{𝒢}=\left(g\in \mathrm{V}⟼\left\{⟨e,f⟩|\underset{\dot{}}{[}{\mathrm{Base}}_g/p\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{dist}\left(g\right)/d\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{Itv}\left(g\right)/i\underset{\dot{}}{]}\exists x\in p\exists y\in p\left(f=xdy\wedge \exists z\in p\left(z\in \left(xiy\right)\wedge e=xdz\right)\right)\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cleg	$$class{\le }_{𝒢}$$
1		vg	$$setvarg$$
2		cvv	$$class\mathrm{V}$$
3		ve	$$setvare$$
4		vf	$$setvarf$$
5		cbs	$$class\mathrm{Base}$$
6	1	cv	$$setvarg$$
7	6 5	cfv	$$class{\mathrm{Base}}_g$$
8		vp	$$setvarp$$
9		cds	$$class\mathrm{dist}$$
10	6 9	cfv	$$class\mathrm{dist}\left(g\right)$$
11		vd	$$setvard$$
12		citv	$$class\mathrm{Itv}$$
13	6 12	cfv	$$class\mathrm{Itv}\left(g\right)$$
14		vi	$$setvari$$
15		vx	$$setvarx$$
16	8	cv	$$setvarp$$
17		vy	$$setvary$$
18	4	cv	$$setvarf$$
19	15	cv	$$setvarx$$
20	11	cv	$$setvard$$
21	17	cv	$$setvary$$
22	19 21 20	co	$$class\left(xdy\right)$$
23	18 22	wceq	$$wfff=xdy$$
24		vz	$$setvarz$$
25	24	cv	$$setvarz$$
26	14	cv	$$setvari$$
27	19 21 26	co	$$class\left(xiy\right)$$
28	25 27	wcel	$$wffz\in \left(xiy\right)$$
29	3	cv	$$setvare$$
30	19 25 20	co	$$class\left(xdz\right)$$
31	29 30	wceq	$$wffe=xdz$$
32	28 31	wa	$$wff\left(z\in \left(xiy\right)\wedge e=xdz\right)$$
33	32 24 16	wrex	$$wff\exists z\in p\left(z\in \left(xiy\right)\wedge e=xdz\right)$$
34	23 33	wa	$$wff\left(f=xdy\wedge \exists z\in p\left(z\in \left(xiy\right)\wedge e=xdz\right)\right)$$
35	34 17 16	wrex	$$wff\exists y\in p\left(f=xdy\wedge \exists z\in p\left(z\in \left(xiy\right)\wedge e=xdz\right)\right)$$
36	35 15 16	wrex	$$wff\exists x\in p\exists y\in p\left(f=xdy\wedge \exists z\in p\left(z\in \left(xiy\right)\wedge e=xdz\right)\right)$$
37	36 14 13	wsbc	$$wff\underset{\dot{}}{[}\mathrm{Itv}\left(g\right)/i\underset{\dot{}}{]}\exists x\in p\exists y\in p\left(f=xdy\wedge \exists z\in p\left(z\in \left(xiy\right)\wedge e=xdz\right)\right)$$
38	37 11 10	wsbc	$$wff\underset{\dot{}}{[}\mathrm{dist}\left(g\right)/d\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{Itv}\left(g\right)/i\underset{\dot{}}{]}\exists x\in p\exists y\in p\left(f=xdy\wedge \exists z\in p\left(z\in \left(xiy\right)\wedge e=xdz\right)\right)$$
39	38 8 7	wsbc	$$wff\underset{\dot{}}{[}{\mathrm{Base}}_g/p\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{dist}\left(g\right)/d\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{Itv}\left(g\right)/i\underset{\dot{}}{]}\exists x\in p\exists y\in p\left(f=xdy\wedge \exists z\in p\left(z\in \left(xiy\right)\wedge e=xdz\right)\right)$$
40	39 3 4	copab	$$class\left\{⟨e,f⟩|\underset{\dot{}}{[}{\mathrm{Base}}_g/p\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{dist}\left(g\right)/d\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{Itv}\left(g\right)/i\underset{\dot{}}{]}\exists x\in p\exists y\in p\left(f=xdy\wedge \exists z\in p\left(z\in \left(xiy\right)\wedge e=xdz\right)\right)\right\}$$
41	1 2 40	cmpt	$$class\left(g\in \mathrm{V}⟼\left\{⟨e,f⟩|\underset{\dot{}}{[}{\mathrm{Base}}_g/p\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{dist}\left(g\right)/d\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{Itv}\left(g\right)/i\underset{\dot{}}{]}\exists x\in p\exists y\in p\left(f=xdy\wedge \exists z\in p\left(z\in \left(xiy\right)\wedge e=xdz\right)\right)\right\}\right)$$
42	0 41	wceq	$$wff{\le }_{𝒢}=\left(g\in \mathrm{V}⟼\left\{⟨e,f⟩|\underset{\dot{}}{[}{\mathrm{Base}}_g/p\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{dist}\left(g\right)/d\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{Itv}\left(g\right)/i\underset{\dot{}}{]}\exists x\in p\exists y\in p\left(f=xdy\wedge \exists z\in p\left(z\in \left(xiy\right)\wedge e=xdz\right)\right)\right\}\right)$$