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⟼ab|a∈Baseg0..^3∧b∈Baseg0..^3∧∃x∈Basegx∈𝒢∠⁡g⟨“b⁡0b⁡1b⁡2”⟩∧⟨“a⁡0a⁡1a⁡2”⟩∼𝒢∠⁡g⟨“b⁡0b⁡1x”⟩

Detailed syntax breakdown

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