Metamath Proof Explorer

Definition df-inag

Description: Definition of the geometrical "in angle" relation. (Contributed by Thierry Arnoux, 15-Aug-2020)

Ref Expression
Assertion df-inag ⊢∈𝒢∠=g∈V⟼pt|p∈Baseg∧t∈Baseg0..^3∧t⁡0≠t⁡1∧t⁡2≠t⁡1∧p≠t⁡1∧∃x∈Basegx∈t⁡0Itv⁡gt⁡2∧x=t⁡1∨xhl𝒢⁡g⁡t⁡1p

Detailed syntax breakdown

Step Hyp Ref Expression
0 cinag class∈𝒢∠
1 vg setvarg
2 cvv classV
3 vp setvarp
4 vt setvart
5 3 cv setvarp
6 cbs classBase
7 1 cv setvarg
8 7 6 cfv classBaseg
9 5 8 wcel wffp∈Baseg
10 4 cv setvart
11 cmap class↑𝑚
12 cc0 class0
13 cfzo class..^
14 c3 class3
15 12 14 13 co class0..^3
16 8 15 11 co classBaseg0..^3
17 10 16 wcel wfft∈Baseg0..^3
18 9 17 wa wffp∈Baseg∧t∈Baseg0..^3
19 12 10 cfv classt⁡0
20 c1 class1
21 20 10 cfv classt⁡1
22 19 21 wne wfft⁡0≠t⁡1
23 c2 class2
24 23 10 cfv classt⁡2
25 24 21 wne wfft⁡2≠t⁡1
26 5 21 wne wffp≠t⁡1
27 22 25 26 w3a wfft⁡0≠t⁡1∧t⁡2≠t⁡1∧p≠t⁡1
28 vx setvarx
29 28 cv setvarx
30 citv classItv
31 7 30 cfv classItv⁡g
32 19 24 31 co classt⁡0Itv⁡gt⁡2
33 29 32 wcel wffx∈t⁡0Itv⁡gt⁡2
34 29 21 wceq wffx=t⁡1
35 chlg classhl𝒢
36 7 35 cfv classhl𝒢⁡g
37 21 36 cfv classhl𝒢⁡g⁡t⁡1
38 29 5 37 wbr wffxhl𝒢⁡g⁡t⁡1p
39 34 38 wo wffx=t⁡1∨xhl𝒢⁡g⁡t⁡1p
40 33 39 wa wffx∈t⁡0Itv⁡gt⁡2∧x=t⁡1∨xhl𝒢⁡g⁡t⁡1p
41 40 28 8 wrex wff∃x∈Basegx∈t⁡0Itv⁡gt⁡2∧x=t⁡1∨xhl𝒢⁡g⁡t⁡1p
42 27 41 wa wfft⁡0≠t⁡1∧t⁡2≠t⁡1∧p≠t⁡1∧∃x∈Basegx∈t⁡0Itv⁡gt⁡2∧x=t⁡1∨xhl𝒢⁡g⁡t⁡1p
43 18 42 wa wffp∈Baseg∧t∈Baseg0..^3∧t⁡0≠t⁡1∧t⁡2≠t⁡1∧p≠t⁡1∧∃x∈Basegx∈t⁡0Itv⁡gt⁡2∧x=t⁡1∨xhl𝒢⁡g⁡t⁡1p
44 43 3 4 copab classpt|p∈Baseg∧t∈Baseg0..^3∧t⁡0≠t⁡1∧t⁡2≠t⁡1∧p≠t⁡1∧∃x∈Basegx∈t⁡0Itv⁡gt⁡2∧x=t⁡1∨xhl𝒢⁡g⁡t⁡1p
45 1 2 44 cmpt classg∈V⟼pt|p∈Baseg∧t∈Baseg0..^3∧t⁡0≠t⁡1∧t⁡2≠t⁡1∧p≠t⁡1∧∃x∈Basegx∈t⁡0Itv⁡gt⁡2∧x=t⁡1∨xhl𝒢⁡g⁡t⁡1p
46 0 45 wceq wff∈𝒢∠=g∈V⟼pt|p∈Baseg∧t∈Baseg0..^3∧t⁡0≠t⁡1∧t⁡2≠t⁡1∧p≠t⁡1∧∃x∈Basegx∈t⁡0Itv⁡gt⁡2∧x=t⁡1∨xhl𝒢⁡g⁡t⁡1p