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 ⟼ p t | p ∈ Base g ∧ t ∈ Base g 0 ..^ 3 ∧ t ⁡ 0 ≠ t ⁡ 1 ∧ t ⁡ 2 ≠ t ⁡ 1 ∧ p ≠ t ⁡ 1 ∧ ∃ x ∈ Base g x ∈ t ⁡ 0 Itv ⁡ g t ⁡ 2 ∧ x = t ⁡ 1 ∨ x hl 𝒢 ⁡ g ⁡ t ⁡ 1 p

Detailed syntax breakdown

Step Hyp Ref Expression
0 cinag class ∈ 𝒢 ∠
1 vg setvar g
2 cvv class V
3 vp setvar p
4 vt setvar t
5 3 cv setvar p
6 cbs class Base
7 1 cv setvar g
8 7 6 cfv class Base g
9 5 8 wcel wff p ∈ Base g
10 4 cv setvar t
11 cmap class ↑ 𝑚
12 cc0 class 0
13 cfzo class ..^
14 c3 class 3
15 12 14 13 co class 0 ..^ 3
16 8 15 11 co class Base g 0 ..^ 3
17 10 16 wcel wff t ∈ Base g 0 ..^ 3
18 9 17 wa wff p ∈ Base g ∧ t ∈ Base g 0 ..^ 3
19 12 10 cfv class t ⁡ 0
20 c1 class 1
21 20 10 cfv class t ⁡ 1
22 19 21 wne wff t ⁡ 0 ≠ t ⁡ 1
23 c2 class 2
24 23 10 cfv class t ⁡ 2
25 24 21 wne wff t ⁡ 2 ≠ t ⁡ 1
26 5 21 wne wff p ≠ t ⁡ 1
27 22 25 26 w3a wff t ⁡ 0 ≠ t ⁡ 1 ∧ t ⁡ 2 ≠ t ⁡ 1 ∧ p ≠ t ⁡ 1
28 vx setvar x
29 28 cv setvar x
30 citv class Itv
31 7 30 cfv class Itv ⁡ g
32 19 24 31 co class t ⁡ 0 Itv ⁡ g t ⁡ 2
33 29 32 wcel wff x ∈ t ⁡ 0 Itv ⁡ g t ⁡ 2
34 29 21 wceq wff x = t ⁡ 1
35 chlg class hl 𝒢
36 7 35 cfv class hl 𝒢 ⁡ g
37 21 36 cfv class hl 𝒢 ⁡ g ⁡ t ⁡ 1
38 29 5 37 wbr wff x hl 𝒢 ⁡ g ⁡ t ⁡ 1 p
39 34 38 wo wff x = t ⁡ 1 ∨ x hl 𝒢 ⁡ g ⁡ t ⁡ 1 p
40 33 39 wa wff x ∈ t ⁡ 0 Itv ⁡ g t ⁡ 2 ∧ x = t ⁡ 1 ∨ x hl 𝒢 ⁡ g ⁡ t ⁡ 1 p
41 40 28 8 wrex wff ∃ x ∈ Base g x ∈ t ⁡ 0 Itv ⁡ g t ⁡ 2 ∧ x = t ⁡ 1 ∨ x hl 𝒢 ⁡ g ⁡ t ⁡ 1 p
42 27 41 wa wff t ⁡ 0 ≠ t ⁡ 1 ∧ t ⁡ 2 ≠ t ⁡ 1 ∧ p ≠ t ⁡ 1 ∧ ∃ x ∈ Base g x ∈ t ⁡ 0 Itv ⁡ g t ⁡ 2 ∧ x = t ⁡ 1 ∨ x hl 𝒢 ⁡ g ⁡ t ⁡ 1 p
43 18 42 wa wff p ∈ Base g ∧ t ∈ Base g 0 ..^ 3 ∧ t ⁡ 0 ≠ t ⁡ 1 ∧ t ⁡ 2 ≠ t ⁡ 1 ∧ p ≠ t ⁡ 1 ∧ ∃ x ∈ Base g x ∈ t ⁡ 0 Itv ⁡ g t ⁡ 2 ∧ x = t ⁡ 1 ∨ x hl 𝒢 ⁡ g ⁡ t ⁡ 1 p
44 43 3 4 copab class p t | p ∈ Base g ∧ t ∈ Base g 0 ..^ 3 ∧ t ⁡ 0 ≠ t ⁡ 1 ∧ t ⁡ 2 ≠ t ⁡ 1 ∧ p ≠ t ⁡ 1 ∧ ∃ x ∈ Base g x ∈ t ⁡ 0 Itv ⁡ g t ⁡ 2 ∧ x = t ⁡ 1 ∨ x hl 𝒢 ⁡ g ⁡ t ⁡ 1 p
45 1 2 44 cmpt class g ∈ V ⟼ p t | p ∈ Base g ∧ t ∈ Base g 0 ..^ 3 ∧ t ⁡ 0 ≠ t ⁡ 1 ∧ t ⁡ 2 ≠ t ⁡ 1 ∧ p ≠ t ⁡ 1 ∧ ∃ x ∈ Base g x ∈ t ⁡ 0 Itv ⁡ g t ⁡ 2 ∧ x = t ⁡ 1 ∨ x hl 𝒢 ⁡ g ⁡ t ⁡ 1 p
46 0 45 wceq wff ∈ 𝒢 ∠ = g ∈ V ⟼ p t | p ∈ Base g ∧ t ∈ Base g 0 ..^ 3 ∧ t ⁡ 0 ≠ t ⁡ 1 ∧ t ⁡ 2 ≠ t ⁡ 1 ∧ p ≠ t ⁡ 1 ∧ ∃ x ∈ Base g x ∈ t ⁡ 0 Itv ⁡ g t ⁡ 2 ∧ x = t ⁡ 1 ∨ x hl 𝒢 ⁡ g ⁡ t ⁡ 1 p