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	⊢ ≤G = ( 𝑔 ∈ V ↦ { ⟨ 𝑒 , 𝑓 ⟩ ∣ [ ( Base ‘ 𝑔 ) / 𝑝 ] [ ( dist ‘ 𝑔 ) / 𝑑 ] [ ( Itv ‘ 𝑔 ) / 𝑖 ] ∃ 𝑥 ∈ 𝑝 ∃ 𝑦 ∈ 𝑝 ( 𝑓 = ( 𝑥 𝑑 𝑦 ) ∧ ∃ 𝑧 ∈ 𝑝 ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∧ 𝑒 = ( 𝑥 𝑑 𝑧 ) ) ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cleg	⊢ ≤G
1		vg	⊢ 𝑔
2		cvv	⊢ V
3		ve	⊢ 𝑒
4		vf	⊢ 𝑓
5		cbs	⊢ Base
6	1	cv	⊢ 𝑔
7	6 5	cfv	⊢ ( Base ‘ 𝑔 )
8		vp	⊢ 𝑝
9		cds	⊢ dist
10	6 9	cfv	⊢ ( dist ‘ 𝑔 )
11		vd	⊢ 𝑑
12		citv	⊢ Itv
13	6 12	cfv	⊢ ( Itv ‘ 𝑔 )
14		vi	⊢ 𝑖
15		vx	⊢ 𝑥
16	8	cv	⊢ 𝑝
17		vy	⊢ 𝑦
18	4	cv	⊢ 𝑓
19	15	cv	⊢ 𝑥
20	11	cv	⊢ 𝑑
21	17	cv	⊢ 𝑦
22	19 21 20	co	⊢ ( 𝑥 𝑑 𝑦 )
23	18 22	wceq	⊢ 𝑓 = ( 𝑥 𝑑 𝑦 )
24		vz	⊢ 𝑧
25	24	cv	⊢ 𝑧
26	14	cv	⊢ 𝑖
27	19 21 26	co	⊢ ( 𝑥 𝑖 𝑦 )
28	25 27	wcel	⊢ 𝑧 ∈ ( 𝑥 𝑖 𝑦 )
29	3	cv	⊢ 𝑒
30	19 25 20	co	⊢ ( 𝑥 𝑑 𝑧 )
31	29 30	wceq	⊢ 𝑒 = ( 𝑥 𝑑 𝑧 )
32	28 31	wa	⊢ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∧ 𝑒 = ( 𝑥 𝑑 𝑧 ) )
33	32 24 16	wrex	⊢ ∃ 𝑧 ∈ 𝑝 ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∧ 𝑒 = ( 𝑥 𝑑 𝑧 ) )
34	23 33	wa	⊢ ( 𝑓 = ( 𝑥 𝑑 𝑦 ) ∧ ∃ 𝑧 ∈ 𝑝 ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∧ 𝑒 = ( 𝑥 𝑑 𝑧 ) ) )
35	34 17 16	wrex	⊢ ∃ 𝑦 ∈ 𝑝 ( 𝑓 = ( 𝑥 𝑑 𝑦 ) ∧ ∃ 𝑧 ∈ 𝑝 ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∧ 𝑒 = ( 𝑥 𝑑 𝑧 ) ) )
36	35 15 16	wrex	⊢ ∃ 𝑥 ∈ 𝑝 ∃ 𝑦 ∈ 𝑝 ( 𝑓 = ( 𝑥 𝑑 𝑦 ) ∧ ∃ 𝑧 ∈ 𝑝 ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∧ 𝑒 = ( 𝑥 𝑑 𝑧 ) ) )
37	36 14 13	wsbc	⊢ [ ( Itv ‘ 𝑔 ) / 𝑖 ] ∃ 𝑥 ∈ 𝑝 ∃ 𝑦 ∈ 𝑝 ( 𝑓 = ( 𝑥 𝑑 𝑦 ) ∧ ∃ 𝑧 ∈ 𝑝 ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∧ 𝑒 = ( 𝑥 𝑑 𝑧 ) ) )
38	37 11 10	wsbc	⊢ [ ( dist ‘ 𝑔 ) / 𝑑 ] [ ( Itv ‘ 𝑔 ) / 𝑖 ] ∃ 𝑥 ∈ 𝑝 ∃ 𝑦 ∈ 𝑝 ( 𝑓 = ( 𝑥 𝑑 𝑦 ) ∧ ∃ 𝑧 ∈ 𝑝 ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∧ 𝑒 = ( 𝑥 𝑑 𝑧 ) ) )
39	38 8 7	wsbc	⊢ [ ( Base ‘ 𝑔 ) / 𝑝 ] [ ( dist ‘ 𝑔 ) / 𝑑 ] [ ( Itv ‘ 𝑔 ) / 𝑖 ] ∃ 𝑥 ∈ 𝑝 ∃ 𝑦 ∈ 𝑝 ( 𝑓 = ( 𝑥 𝑑 𝑦 ) ∧ ∃ 𝑧 ∈ 𝑝 ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∧ 𝑒 = ( 𝑥 𝑑 𝑧 ) ) )
40	39 3 4	copab	⊢ { ⟨ 𝑒 , 𝑓 ⟩ ∣ [ ( Base ‘ 𝑔 ) / 𝑝 ] [ ( dist ‘ 𝑔 ) / 𝑑 ] [ ( Itv ‘ 𝑔 ) / 𝑖 ] ∃ 𝑥 ∈ 𝑝 ∃ 𝑦 ∈ 𝑝 ( 𝑓 = ( 𝑥 𝑑 𝑦 ) ∧ ∃ 𝑧 ∈ 𝑝 ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∧ 𝑒 = ( 𝑥 𝑑 𝑧 ) ) ) }
41	1 2 40	cmpt	⊢ ( 𝑔 ∈ V ↦ { ⟨ 𝑒 , 𝑓 ⟩ ∣ [ ( Base ‘ 𝑔 ) / 𝑝 ] [ ( dist ‘ 𝑔 ) / 𝑑 ] [ ( Itv ‘ 𝑔 ) / 𝑖 ] ∃ 𝑥 ∈ 𝑝 ∃ 𝑦 ∈ 𝑝 ( 𝑓 = ( 𝑥 𝑑 𝑦 ) ∧ ∃ 𝑧 ∈ 𝑝 ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∧ 𝑒 = ( 𝑥 𝑑 𝑧 ) ) ) } )
42	0 41	wceq	⊢ ≤G = ( 𝑔 ∈ V ↦ { ⟨ 𝑒 , 𝑓 ⟩ ∣ [ ( Base ‘ 𝑔 ) / 𝑝 ] [ ( dist ‘ 𝑔 ) / 𝑑 ] [ ( Itv ‘ 𝑔 ) / 𝑖 ] ∃ 𝑥 ∈ 𝑝 ∃ 𝑦 ∈ 𝑝 ( 𝑓 = ( 𝑥 𝑑 𝑦 ) ∧ ∃ 𝑧 ∈ 𝑝 ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∧ 𝑒 = ( 𝑥 𝑑 𝑧 ) ) ) } )