Definition df-inag 25728

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

Assertion

Ref	Expression
df-inag	|- inA = ( g e. _V |-> { <. p , t >. | ( ( p e. ( Base ` g ) /\ t e. ( ( Base ` g ) ^m ( 0..^ 3 ) ) ) /\ ( ( ( t ` 0 ) =/= ( t ` 1 ) /\ ( t ` 2 ) =/= ( t ` 1 ) /\ p =/= ( t ` 1 ) ) /\ E. x e. ( Base ` g ) ( x e. ( ( t ` 0 ) (Itv ` g ) ( t ` 2 ) ) /\ ( x = ( t ` 1 ) \/ x ( (hlG ` g ) ` ( t ` 1 ) ) p ) ) ) ) } )

Distinct variable group:   g, p, t, x

Detailed syntax breakdown of Definition df-inag

Step	Hyp	Ref	Expression
1		cinag 25726	. 2 class inA
2		vg	. . 3 setvar g
3		cvv 3200	. . 3 class _V
4		vp	. . . . . . . 8 setvar p
5	4	cv 1482	. . . . . . 7 class p
6	2	cv 1482	. . . . . . . 8 class g
7		cbs 15857	. . . . . . . 8 class Base
8	6, 7	cfv 5888	. . . . . . 7 class ( Base ` g )
9	5, 8	wcel 1990	. . . . . 6 wff p e. ( Base ` g )
10		vt	. . . . . . . 8 setvar t
11	10	cv 1482	. . . . . . 7 class t
12		cc0 9936	. . . . . . . . 9 class 0
13		c3 11071	. . . . . . . . 9 class 3
14		cfzo 12465	. . . . . . . . 9 class ..^
15	12, 13, 14	co 6650	. . . . . . . 8 class ( 0..^ 3 )
16		cmap 7857	. . . . . . . 8 class ^m
17	8, 15, 16	co 6650	. . . . . . 7 class ( ( Base ` g ) ^m ( 0..^ 3 ) )
18	11, 17	wcel 1990	. . . . . 6 wff t e. ( ( Base ` g ) ^m ( 0..^ 3 ) )
19	9, 18	wa 384	. . . . 5 wff ( p e. ( Base ` g ) /\ t e. ( ( Base ` g ) ^m ( 0..^ 3 ) ) )
20	12, 11	cfv 5888	. . . . . . . 8 class ( t ` 0 )
21		c1 9937	. . . . . . . . 9 class 1
22	21, 11	cfv 5888	. . . . . . . 8 class ( t ` 1 )
23	20, 22	wne 2794	. . . . . . 7 wff ( t ` 0 ) =/= ( t ` 1 )
24		c2 11070	. . . . . . . . 9 class 2
25	24, 11	cfv 5888	. . . . . . . 8 class ( t ` 2 )
26	25, 22	wne 2794	. . . . . . 7 wff ( t ` 2 ) =/= ( t ` 1 )
27	5, 22	wne 2794	. . . . . . 7 wff p =/= ( t ` 1 )
28	23, 26, 27	w3a 1037	. . . . . 6 wff ( ( t ` 0 ) =/= ( t ` 1 ) /\ ( t ` 2 ) =/= ( t ` 1 ) /\ p =/= ( t ` 1 ) )
29		vx	. . . . . . . . . 10 setvar x
30	29	cv 1482	. . . . . . . . 9 class x
31		citv 25335	. . . . . . . . . . 11 class Itv
32	6, 31	cfv 5888	. . . . . . . . . 10 class (Itv ` g )
33	20, 25, 32	co 6650	. . . . . . . . 9 class ( ( t ` 0 ) (Itv ` g ) ( t ` 2 ) )
34	30, 33	wcel 1990	. . . . . . . 8 wff x e. ( ( t ` 0 ) (Itv ` g ) ( t ` 2 ) )
35	30, 22	wceq 1483	. . . . . . . . 9 wff x = ( t ` 1 )
36		chlg 25495	. . . . . . . . . . . 12 class hlG
37	6, 36	cfv 5888	. . . . . . . . . . 11 class (hlG ` g )
38	22, 37	cfv 5888	. . . . . . . . . 10 class ( (hlG ` g ) ` ( t ` 1 ) )
39	30, 5, 38	wbr 4653	. . . . . . . . 9 wff x ( (hlG ` g ) ` ( t ` 1 ) ) p
40	35, 39	wo 383	. . . . . . . 8 wff ( x = ( t ` 1 ) \/ x ( (hlG ` g ) ` ( t ` 1 ) ) p )
41	34, 40	wa 384	. . . . . . 7 wff ( x e. ( ( t ` 0 ) (Itv ` g ) ( t ` 2 ) ) /\ ( x = ( t ` 1 ) \/ x ( (hlG ` g ) ` ( t ` 1 ) ) p ) )
42	41, 29, 8	wrex 2913	. . . . . 6 wff E. x e. ( Base ` g ) ( x e. ( ( t ` 0 ) (Itv ` g ) ( t ` 2 ) ) /\ ( x = ( t ` 1 ) \/ x ( (hlG ` g ) ` ( t ` 1 ) ) p ) )
43	28, 42	wa 384	. . . . 5 wff ( ( ( t ` 0 ) =/= ( t ` 1 ) /\ ( t ` 2 ) =/= ( t ` 1 ) /\ p =/= ( t ` 1 ) ) /\ E. x e. ( Base ` g ) ( x e. ( ( t ` 0 ) (Itv ` g ) ( t ` 2 ) ) /\ ( x = ( t ` 1 ) \/ x ( (hlG ` g ) ` ( t ` 1 ) ) p ) ) )
44	19, 43	wa 384	. . . 4 wff ( ( p e. ( Base ` g ) /\ t e. ( ( Base ` g ) ^m ( 0..^ 3 ) ) ) /\ ( ( ( t ` 0 ) =/= ( t ` 1 ) /\ ( t ` 2 ) =/= ( t ` 1 ) /\ p =/= ( t ` 1 ) ) /\ E. x e. ( Base ` g ) ( x e. ( ( t ` 0 ) (Itv ` g ) ( t ` 2 ) ) /\ ( x = ( t ` 1 ) \/ x ( (hlG ` g ) ` ( t ` 1 ) ) p ) ) ) )
45	44, 4, 10	copab 4712	. . 3 class { <. p , t >. | ( ( p e. ( Base ` g ) /\ t e. ( ( Base ` g ) ^m ( 0..^ 3 ) ) ) /\ ( ( ( t ` 0 ) =/= ( t ` 1 ) /\ ( t ` 2 ) =/= ( t ` 1 ) /\ p =/= ( t ` 1 ) ) /\ E. x e. ( Base ` g ) ( x e. ( ( t ` 0 ) (Itv ` g ) ( t ` 2 ) ) /\ ( x = ( t ` 1 ) \/ x ( (hlG ` g ) ` ( t ` 1 ) ) p ) ) ) ) }
46	2, 3, 45	cmpt 4729	. 2 class ( g e. _V |-> { <. p , t >. | ( ( p e. ( Base ` g ) /\ t e. ( ( Base ` g ) ^m ( 0..^ 3 ) ) ) /\ ( ( ( t ` 0 ) =/= ( t ` 1 ) /\ ( t ` 2 ) =/= ( t ` 1 ) /\ p =/= ( t ` 1 ) ) /\ E. x e. ( Base ` g ) ( x e. ( ( t ` 0 ) (Itv ` g ) ( t ` 2 ) ) /\ ( x = ( t ` 1 ) \/ x ( (hlG ` g ) ` ( t ` 1 ) ) p ) ) ) ) } )
47	1, 46	wceq 1483	1 wff inA = ( g e. _V |-> { <. p , t >. | ( ( p e. ( Base ` g ) /\ t e. ( ( Base ` g ) ^m ( 0..^ 3 ) ) ) /\ ( ( ( t ` 0 ) =/= ( t ` 1 ) /\ ( t ` 2 ) =/= ( t ` 1 ) /\ p =/= ( t ` 1 ) ) /\ E. x e. ( Base ` g ) ( x e. ( ( t ` 0 ) (Itv ` g ) ( t ` 2 ) ) /\ ( x = ( t ` 1 ) \/ x ( (hlG ` g ) ` ( t ` 1 ) ) p ) ) ) ) } )

This definition is referenced by:  isinag  25729