Metamath Proof Explorer

Definition df-leag

Description: Definition of the geometrical "angle less than" relation. Definition 11.27 of Schwabhauser p. 102. (Contributed by Thierry Arnoux, 7-Oct-2020)

Ref Expression
Assertion df-leag ⊢ ≤ 𝒢 ∠ = g ∈ V ⟼ a b | a ∈ Base g 0 ..^ 3 ∧ b ∈ Base g 0 ..^ 3 ∧ ∃ x ∈ Base g x ∈ 𝒢 ∠ ⁡ g ⟨“ b ⁡ 0 b ⁡ 1 b ⁡ 2 ”⟩ ∧ ⟨“ a ⁡ 0 a ⁡ 1 a ⁡ 2 ”⟩ ∼ 𝒢 ∠ ⁡ g ⟨“ b ⁡ 0 b ⁡ 1 x ”⟩

Detailed syntax breakdown

Step Hyp Ref Expression
0 cleag class ≤ 𝒢 ∠
1 vg setvar g
2 cvv class V
3 va setvar a
4 vb setvar b
5 3 cv setvar a
6 cbs class Base
7 1 cv setvar g
8 7 6 cfv class Base g
9 cmap class ↑ 𝑚
10 cc0 class 0
11 cfzo class ..^
12 c3 class 3
13 10 12 11 co class 0 ..^ 3
14 8 13 9 co class Base g 0 ..^ 3
15 5 14 wcel wff a ∈ Base g 0 ..^ 3
16 4 cv setvar b
17 16 14 wcel wff b ∈ Base g 0 ..^ 3
18 15 17 wa wff a ∈ Base g 0 ..^ 3 ∧ b ∈ Base g 0 ..^ 3
19 vx setvar x
20 19 cv setvar x
21 cinag class ∈ 𝒢 ∠
22 7 21 cfv class ∈ 𝒢 ∠ ⁡ g
23 10 16 cfv class b ⁡ 0
24 c1 class 1
25 24 16 cfv class b ⁡ 1
26 c2 class 2
27 26 16 cfv class b ⁡ 2
28 23 25 27 cs3 class ⟨“ b ⁡ 0 b ⁡ 1 b ⁡ 2 ”⟩
29 20 28 22 wbr wff x ∈ 𝒢 ∠ ⁡ g ⟨“ b ⁡ 0 b ⁡ 1 b ⁡ 2 ”⟩
30 10 5 cfv class a ⁡ 0
31 24 5 cfv class a ⁡ 1
32 26 5 cfv class a ⁡ 2
33 30 31 32 cs3 class ⟨“ a ⁡ 0 a ⁡ 1 a ⁡ 2 ”⟩
34 ccgra class ∼ 𝒢 ∠
35 7 34 cfv class ∼ 𝒢 ∠ ⁡ g
36 23 25 20 cs3 class ⟨“ b ⁡ 0 b ⁡ 1 x ”⟩
37 33 36 35 wbr wff ⟨“ a ⁡ 0 a ⁡ 1 a ⁡ 2 ”⟩ ∼ 𝒢 ∠ ⁡ g ⟨“ b ⁡ 0 b ⁡ 1 x ”⟩
38 29 37 wa wff x ∈ 𝒢 ∠ ⁡ g ⟨“ b ⁡ 0 b ⁡ 1 b ⁡ 2 ”⟩ ∧ ⟨“ a ⁡ 0 a ⁡ 1 a ⁡ 2 ”⟩ ∼ 𝒢 ∠ ⁡ g ⟨“ b ⁡ 0 b ⁡ 1 x ”⟩
39 38 19 8 wrex wff ∃ x ∈ Base g x ∈ 𝒢 ∠ ⁡ g ⟨“ b ⁡ 0 b ⁡ 1 b ⁡ 2 ”⟩ ∧ ⟨“ a ⁡ 0 a ⁡ 1 a ⁡ 2 ”⟩ ∼ 𝒢 ∠ ⁡ g ⟨“ b ⁡ 0 b ⁡ 1 x ”⟩
40 18 39 wa wff a ∈ Base g 0 ..^ 3 ∧ b ∈ Base g 0 ..^ 3 ∧ ∃ x ∈ Base g x ∈ 𝒢 ∠ ⁡ g ⟨“ b ⁡ 0 b ⁡ 1 b ⁡ 2 ”⟩ ∧ ⟨“ a ⁡ 0 a ⁡ 1 a ⁡ 2 ”⟩ ∼ 𝒢 ∠ ⁡ g ⟨“ b ⁡ 0 b ⁡ 1 x ”⟩
41 40 3 4 copab class a b | a ∈ Base g 0 ..^ 3 ∧ b ∈ Base g 0 ..^ 3 ∧ ∃ x ∈ Base g x ∈ 𝒢 ∠ ⁡ g ⟨“ b ⁡ 0 b ⁡ 1 b ⁡ 2 ”⟩ ∧ ⟨“ a ⁡ 0 a ⁡ 1 a ⁡ 2 ”⟩ ∼ 𝒢 ∠ ⁡ g ⟨“ b ⁡ 0 b ⁡ 1 x ”⟩
42 1 2 41 cmpt class g ∈ V ⟼ a b | a ∈ Base g 0 ..^ 3 ∧ b ∈ Base g 0 ..^ 3 ∧ ∃ x ∈ Base g x ∈ 𝒢 ∠ ⁡ g ⟨“ b ⁡ 0 b ⁡ 1 b ⁡ 2 ”⟩ ∧ ⟨“ a ⁡ 0 a ⁡ 1 a ⁡ 2 ”⟩ ∼ 𝒢 ∠ ⁡ g ⟨“ b ⁡ 0 b ⁡ 1 x ”⟩
43 0 42 wceq wff ≤ 𝒢 ∠ = g ∈ V ⟼ a b | a ∈ Base g 0 ..^ 3 ∧ b ∈ Base g 0 ..^ 3 ∧ ∃ x ∈ Base g x ∈ 𝒢 ∠ ⁡ g ⟨“ b ⁡ 0 b ⁡ 1 b ⁡ 2 ”⟩ ∧ ⟨“ a ⁡ 0 a ⁡ 1 a ⁡ 2 ”⟩ ∼ 𝒢 ∠ ⁡ g ⟨“ b ⁡ 0 b ⁡ 1 x ”⟩