Metamath Proof Explorer

Theorem cgraer

Description: The angle congruence relation is an equivalence relation. (Contributed by Thierry Arnoux, 31-Aug-2026)

Ref Expression
Hypotheses cgraer.p 
|- P = ( Base ` G )
cgraer.a 
|- A = { d e. ( P ^m ( 0 ..^ 3 ) ) | ( ( d ` 0 ) =/= ( d ` 1 ) /\ ( d ` 1 ) =/= ( d ` 2 ) ) }
cgraer.c 
|- .~ = ( cgrA ` G )
cgraer.g 
|- ( ph -> G e. TarskiG )
Assertion cgraer 
|- ( ph -> ( .~ i^i ( A X. A ) ) Er A )

Proof

Step Hyp Ref Expression
1 cgraer.p 
 |-  P = ( Base ` G )
2 cgraer.a 
 |-  A = { d e. ( P ^m ( 0 ..^ 3 ) ) | ( ( d ` 0 ) =/= ( d ` 1 ) /\ ( d ` 1 ) =/= ( d ` 2 ) ) }
3 cgraer.c 
 |-  .~ = ( cgrA ` G )
4 cgraer.g 
 |-  ( ph -> G e. TarskiG )
5 relinxp 
 |-  Rel ( .~ i^i ( A X. A ) )
6 5 a1i 
 |-  ( ph -> Rel ( .~ i^i ( A X. A ) ) )
7 brinxp2 
 |-  ( e ( .~ i^i ( A X. A ) ) f <-> ( ( e e. A /\ f e. A ) /\ e .~ f ) )
8 7 bilani 
 |-  ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) -> ( ( e e. A /\ f e. A ) /\ e .~ f ) )
9 8 simplrd 
 |-  ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) -> f e. A )
10 8 simplld 
 |-  ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) -> e e. A )
11 3 a1i 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ f = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) -> .~ = ( cgrA ` G ) )
12 11 eqcomd 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ f = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) -> ( cgrA ` G ) = .~ )
13 eqid 
 |-  ( Itv ` G ) = ( Itv ` G )
14 4 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) -> G e. TarskiG )
15 14 ad6antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ f = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) -> G e. TarskiG )
16 eqid 
 |-  ( hlG ` G ) = ( hlG ` G )
17 simp-6r 
 |-  ( ( ( ( ( ( ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) -> x e. P )
18 17 ad6antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ f = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) -> x e. P )
19 simp-11r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ f = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) -> y e. P )
20 simp-10r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ f = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) -> z e. P )
21 simp-6r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ f = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) -> u e. P )
22 simp-5r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ f = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) -> v e. P )
23 simp-4r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ f = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) -> w e. P )
24 8 simprd 
 |-  ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) -> e .~ f )
25 24 ad6antr 
 |-  ( ( ( ( ( ( ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) -> e .~ f )
26 25 ad6antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ f = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) -> e .~ f )
27 11 26 breqdi 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ f = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) -> e ( cgrA ` G ) f )
28 simp-9r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ f = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) -> e = <" x y z "> )
29 simpllr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ f = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) -> f = <" u v w "> )
30 27 28 29 3brtr3d 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ f = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) -> <" x y z "> ( cgrA ` G ) <" u v w "> )
31 1 13 15 16 18 19 20 21 22 23 30 cgracom 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ f = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) -> <" u v w "> ( cgrA ` G ) <" x y z "> )
32 12 31 breqdi 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ f = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) -> <" u v w "> .~ <" x y z "> )
33 32 29 28 3brtr4d 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ f = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) -> f .~ e )
34 33 anasss 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ f = <" u v w "> ) /\ ( u =/= v /\ v =/= w ) ) -> f .~ e )
35 34 anasss 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ ( f = <" u v w "> /\ ( u =/= v /\ v =/= w ) ) ) -> f .~ e )
36 35 r19.29an 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ E. w e. P ( f = <" u v w "> /\ ( u =/= v /\ v =/= w ) ) ) -> f .~ e )
37 1 fvexi 
 |-  P e. _V
38 9 ad6antr 
 |-  ( ( ( ( ( ( ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) -> f e. A )
39 37 2 38 elcgrabasi 
 |-  ( ( ( ( ( ( ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) -> E. u e. P E. v e. P E. w e. P ( f = <" u v w "> /\ ( u =/= v /\ v =/= w ) ) )
40 36 39 r19.29vva 
 |-  ( ( ( ( ( ( ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) -> f .~ e )
41 40 anasss 
 |-  ( ( ( ( ( ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ ( x =/= y /\ y =/= z ) ) -> f .~ e )
42 41 anasss 
 |-  ( ( ( ( ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ ( e = <" x y z "> /\ ( x =/= y /\ y =/= z ) ) ) -> f .~ e )
43 42 r19.29an 
 |-  ( ( ( ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) /\ x e. P ) /\ y e. P ) /\ E. z e. P ( e = <" x y z "> /\ ( x =/= y /\ y =/= z ) ) ) -> f .~ e )
44 37 2 10 elcgrabasi 
 |-  ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) -> E. x e. P E. y e. P E. z e. P ( e = <" x y z "> /\ ( x =/= y /\ y =/= z ) ) )
45 43 44 r19.29vva 
 |-  ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) -> f .~ e )
46 brinxp2 
 |-  ( f ( .~ i^i ( A X. A ) ) e <-> ( ( f e. A /\ e e. A ) /\ f .~ e ) )
47 9 10 45 46 syl21anbrc 
 |-  ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) -> f ( .~ i^i ( A X. A ) ) e )
48 10 adantr 
 |-  ( ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) /\ f ( .~ i^i ( A X. A ) ) g ) -> e e. A )
49 48 ad6antr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) /\ f ( .~ i^i ( A X. A ) ) g ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) -> e e. A )
50 49 ad6antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) /\ f ( .~ i^i ( A X. A ) ) g ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ f = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) -> e e. A )
51 50 ad6antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) /\ f ( .~ i^i ( A X. A ) ) g ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ f = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ i e. P ) /\ j e. P ) /\ k e. P ) /\ g = <" i j k "> ) /\ i =/= j ) /\ j =/= k ) -> e e. A )
52 brinxp2 
 |-  ( f ( .~ i^i ( A X. A ) ) g <-> ( ( f e. A /\ g e. A ) /\ f .~ g ) )
53 52 biimpi 
 |-  ( f ( .~ i^i ( A X. A ) ) g -> ( ( f e. A /\ g e. A ) /\ f .~ g ) )
54 53 simplrd 
 |-  ( f ( .~ i^i ( A X. A ) ) g -> g e. A )
55 54 ad7antlr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) /\ f ( .~ i^i ( A X. A ) ) g ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) -> g e. A )
56 55 ad6antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) /\ f ( .~ i^i ( A X. A ) ) g ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ f = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) -> g e. A )
57 56 ad6antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) /\ f ( .~ i^i ( A X. A ) ) g ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ f = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ i e. P ) /\ j e. P ) /\ k e. P ) /\ g = <" i j k "> ) /\ i =/= j ) /\ j =/= k ) -> g e. A )
58 3 eqcomi 
 |-  ( cgrA ` G ) = .~
59 58 a1i 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) /\ f ( .~ i^i ( A X. A ) ) g ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ f = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ i e. P ) /\ j e. P ) /\ k e. P ) /\ g = <" i j k "> ) /\ i =/= j ) /\ j =/= k ) -> ( cgrA ` G ) = .~ )
60 4 ad8antr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) /\ f ( .~ i^i ( A X. A ) ) g ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) -> G e. TarskiG )
61 60 ad6antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) /\ f ( .~ i^i ( A X. A ) ) g ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ f = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) -> G e. TarskiG )
62 61 ad6antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) /\ f ( .~ i^i ( A X. A ) ) g ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ f = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ i e. P ) /\ j e. P ) /\ k e. P ) /\ g = <" i j k "> ) /\ i =/= j ) /\ j =/= k ) -> G e. TarskiG )
63 simp-6r 
 |-  ( ( ( ( ( ( ( ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) /\ f ( .~ i^i ( A X. A ) ) g ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) -> x e. P )
64 63 ad6antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) /\ f ( .~ i^i ( A X. A ) ) g ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ f = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) -> x e. P )
65 64 ad6antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) /\ f ( .~ i^i ( A X. A ) ) g ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ f = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ i e. P ) /\ j e. P ) /\ k e. P ) /\ g = <" i j k "> ) /\ i =/= j ) /\ j =/= k ) -> x e. P )
66 simp-11r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) /\ f ( .~ i^i ( A X. A ) ) g ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ f = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) -> y e. P )
67 66 ad6antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) /\ f ( .~ i^i ( A X. A ) ) g ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ f = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ i e. P ) /\ j e. P ) /\ k e. P ) /\ g = <" i j k "> ) /\ i =/= j ) /\ j =/= k ) -> y e. P )
68 simp-10r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) /\ f ( .~ i^i ( A X. A ) ) g ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ f = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) -> z e. P )
69 68 ad6antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) /\ f ( .~ i^i ( A X. A ) ) g ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ f = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ i e. P ) /\ j e. P ) /\ k e. P ) /\ g = <" i j k "> ) /\ i =/= j ) /\ j =/= k ) -> z e. P )
70 simp-6r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) /\ f ( .~ i^i ( A X. A ) ) g ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ f = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) -> u e. P )
71 70 ad6antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) /\ f ( .~ i^i ( A X. A ) ) g ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ f = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ i e. P ) /\ j e. P ) /\ k e. P ) /\ g = <" i j k "> ) /\ i =/= j ) /\ j =/= k ) -> u e. P )
72 simp-11r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) /\ f ( .~ i^i ( A X. A ) ) g ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ f = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ i e. P ) /\ j e. P ) /\ k e. P ) /\ g = <" i j k "> ) /\ i =/= j ) /\ j =/= k ) -> v e. P )
73 simp-10r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) /\ f ( .~ i^i ( A X. A ) ) g ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ f = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ i e. P ) /\ j e. P ) /\ k e. P ) /\ g = <" i j k "> ) /\ i =/= j ) /\ j =/= k ) -> w e. P )
74 3 a1i 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) /\ f ( .~ i^i ( A X. A ) ) g ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ f = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ i e. P ) /\ j e. P ) /\ k e. P ) /\ g = <" i j k "> ) /\ i =/= j ) /\ j =/= k ) -> .~ = ( cgrA ` G ) )
75 24 ad7antr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) /\ f ( .~ i^i ( A X. A ) ) g ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) -> e .~ f )
76 75 ad6antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) /\ f ( .~ i^i ( A X. A ) ) g ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ f = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) -> e .~ f )
77 76 ad6antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) /\ f ( .~ i^i ( A X. A ) ) g ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ f = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ i e. P ) /\ j e. P ) /\ k e. P ) /\ g = <" i j k "> ) /\ i =/= j ) /\ j =/= k ) -> e .~ f )
78 74 77 breqdi 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) /\ f ( .~ i^i ( A X. A ) ) g ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ f = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ i e. P ) /\ j e. P ) /\ k e. P ) /\ g = <" i j k "> ) /\ i =/= j ) /\ j =/= k ) -> e ( cgrA ` G ) f )
79 simp-9r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) /\ f ( .~ i^i ( A X. A ) ) g ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ f = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) -> e = <" x y z "> )
80 79 ad6antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) /\ f ( .~ i^i ( A X. A ) ) g ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ f = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ i e. P ) /\ j e. P ) /\ k e. P ) /\ g = <" i j k "> ) /\ i =/= j ) /\ j =/= k ) -> e = <" x y z "> )
81 simp-9r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) /\ f ( .~ i^i ( A X. A ) ) g ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ f = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ i e. P ) /\ j e. P ) /\ k e. P ) /\ g = <" i j k "> ) /\ i =/= j ) /\ j =/= k ) -> f = <" u v w "> )
82 78 80 81 3brtr3d 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) /\ f ( .~ i^i ( A X. A ) ) g ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ f = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ i e. P ) /\ j e. P ) /\ k e. P ) /\ g = <" i j k "> ) /\ i =/= j ) /\ j =/= k ) -> <" x y z "> ( cgrA ` G ) <" u v w "> )
83 simp-6r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) /\ f ( .~ i^i ( A X. A ) ) g ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ f = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ i e. P ) /\ j e. P ) /\ k e. P ) /\ g = <" i j k "> ) /\ i =/= j ) /\ j =/= k ) -> i e. P )
84 simp-5r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) /\ f ( .~ i^i ( A X. A ) ) g ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ f = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ i e. P ) /\ j e. P ) /\ k e. P ) /\ g = <" i j k "> ) /\ i =/= j ) /\ j =/= k ) -> j e. P )
85 simp-4r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) /\ f ( .~ i^i ( A X. A ) ) g ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ f = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ i e. P ) /\ j e. P ) /\ k e. P ) /\ g = <" i j k "> ) /\ i =/= j ) /\ j =/= k ) -> k e. P )
86 53 simprd 
 |-  ( f ( .~ i^i ( A X. A ) ) g -> f .~ g )
87 86 ad7antlr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) /\ f ( .~ i^i ( A X. A ) ) g ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) -> f .~ g )
88 87 ad6antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) /\ f ( .~ i^i ( A X. A ) ) g ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ f = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) -> f .~ g )
89 88 ad6antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) /\ f ( .~ i^i ( A X. A ) ) g ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ f = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ i e. P ) /\ j e. P ) /\ k e. P ) /\ g = <" i j k "> ) /\ i =/= j ) /\ j =/= k ) -> f .~ g )
90 74 89 breqdi 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) /\ f ( .~ i^i ( A X. A ) ) g ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ f = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ i e. P ) /\ j e. P ) /\ k e. P ) /\ g = <" i j k "> ) /\ i =/= j ) /\ j =/= k ) -> f ( cgrA ` G ) g )
91 simpllr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) /\ f ( .~ i^i ( A X. A ) ) g ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ f = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ i e. P ) /\ j e. P ) /\ k e. P ) /\ g = <" i j k "> ) /\ i =/= j ) /\ j =/= k ) -> g = <" i j k "> )
92 90 81 91 3brtr3d 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) /\ f ( .~ i^i ( A X. A ) ) g ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ f = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ i e. P ) /\ j e. P ) /\ k e. P ) /\ g = <" i j k "> ) /\ i =/= j ) /\ j =/= k ) -> <" u v w "> ( cgrA ` G ) <" i j k "> )
93 1 13 62 16 65 67 69 71 72 73 82 83 84 85 92 cgratr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) /\ f ( .~ i^i ( A X. A ) ) g ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ f = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ i e. P ) /\ j e. P ) /\ k e. P ) /\ g = <" i j k "> ) /\ i =/= j ) /\ j =/= k ) -> <" x y z "> ( cgrA ` G ) <" i j k "> )
94 59 93 breqdi 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) /\ f ( .~ i^i ( A X. A ) ) g ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ f = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ i e. P ) /\ j e. P ) /\ k e. P ) /\ g = <" i j k "> ) /\ i =/= j ) /\ j =/= k ) -> <" x y z "> .~ <" i j k "> )
95 94 80 91 3brtr4d 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) /\ f ( .~ i^i ( A X. A ) ) g ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ f = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ i e. P ) /\ j e. P ) /\ k e. P ) /\ g = <" i j k "> ) /\ i =/= j ) /\ j =/= k ) -> e .~ g )
96 brinxp2 
 |-  ( e ( .~ i^i ( A X. A ) ) g <-> ( ( e e. A /\ g e. A ) /\ e .~ g ) )
97 51 57 95 96 syl21anbrc 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) /\ f ( .~ i^i ( A X. A ) ) g ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ f = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ i e. P ) /\ j e. P ) /\ k e. P ) /\ g = <" i j k "> ) /\ i =/= j ) /\ j =/= k ) -> e ( .~ i^i ( A X. A ) ) g )
98 97 anasss 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) /\ f ( .~ i^i ( A X. A ) ) g ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ f = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ i e. P ) /\ j e. P ) /\ k e. P ) /\ g = <" i j k "> ) /\ ( i =/= j /\ j =/= k ) ) -> e ( .~ i^i ( A X. A ) ) g )
99 98 anasss 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) /\ f ( .~ i^i ( A X. A ) ) g ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ f = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ i e. P ) /\ j e. P ) /\ k e. P ) /\ ( g = <" i j k "> /\ ( i =/= j /\ j =/= k ) ) ) -> e ( .~ i^i ( A X. A ) ) g )
100 99 r19.29an 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) /\ f ( .~ i^i ( A X. A ) ) g ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ f = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) /\ i e. P ) /\ j e. P ) /\ E. k e. P ( g = <" i j k "> /\ ( i =/= j /\ j =/= k ) ) ) -> e ( .~ i^i ( A X. A ) ) g )
101 37 2 56 elcgrabasi 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) /\ f ( .~ i^i ( A X. A ) ) g ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ f = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) -> E. i e. P E. j e. P E. k e. P ( g = <" i j k "> /\ ( i =/= j /\ j =/= k ) ) )
102 100 101 r19.29vva 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) /\ f ( .~ i^i ( A X. A ) ) g ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ f = <" u v w "> ) /\ u =/= v ) /\ v =/= w ) -> e ( .~ i^i ( A X. A ) ) g )
103 102 anasss 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) /\ f ( .~ i^i ( A X. A ) ) g ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ f = <" u v w "> ) /\ ( u =/= v /\ v =/= w ) ) -> e ( .~ i^i ( A X. A ) ) g )
104 103 anasss 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) /\ f ( .~ i^i ( A X. A ) ) g ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ ( f = <" u v w "> /\ ( u =/= v /\ v =/= w ) ) ) -> e ( .~ i^i ( A X. A ) ) g )
105 104 r19.29an 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) /\ f ( .~ i^i ( A X. A ) ) g ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) /\ u e. P ) /\ v e. P ) /\ E. w e. P ( f = <" u v w "> /\ ( u =/= v /\ v =/= w ) ) ) -> e ( .~ i^i ( A X. A ) ) g )
106 39 adantl6r 
 |-  ( ( ( ( ( ( ( ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) /\ f ( .~ i^i ( A X. A ) ) g ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) -> E. u e. P E. v e. P E. w e. P ( f = <" u v w "> /\ ( u =/= v /\ v =/= w ) ) )
107 105 106 r19.29vva 
 |-  ( ( ( ( ( ( ( ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) /\ f ( .~ i^i ( A X. A ) ) g ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) -> e ( .~ i^i ( A X. A ) ) g )
108 107 anasss 
 |-  ( ( ( ( ( ( ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) /\ f ( .~ i^i ( A X. A ) ) g ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ ( x =/= y /\ y =/= z ) ) -> e ( .~ i^i ( A X. A ) ) g )
109 108 anasss 
 |-  ( ( ( ( ( ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) /\ f ( .~ i^i ( A X. A ) ) g ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ ( e = <" x y z "> /\ ( x =/= y /\ y =/= z ) ) ) -> e ( .~ i^i ( A X. A ) ) g )
110 109 r19.29an 
 |-  ( ( ( ( ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) /\ f ( .~ i^i ( A X. A ) ) g ) /\ x e. P ) /\ y e. P ) /\ E. z e. P ( e = <" x y z "> /\ ( x =/= y /\ y =/= z ) ) ) -> e ( .~ i^i ( A X. A ) ) g )
111 37 2 48 elcgrabasi 
 |-  ( ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) /\ f ( .~ i^i ( A X. A ) ) g ) -> E. x e. P E. y e. P E. z e. P ( e = <" x y z "> /\ ( x =/= y /\ y =/= z ) ) )
112 110 111 r19.29vva 
 |-  ( ( ( ph /\ e ( .~ i^i ( A X. A ) ) f ) /\ f ( .~ i^i ( A X. A ) ) g ) -> e ( .~ i^i ( A X. A ) ) g )
113 112 anasss 
 |-  ( ( ph /\ ( e ( .~ i^i ( A X. A ) ) f /\ f ( .~ i^i ( A X. A ) ) g ) ) -> e ( .~ i^i ( A X. A ) ) g )
114 simpr 
 |-  ( ( ph /\ e e. A ) -> e e. A )
115 58 a1i 
 |-  ( ( ( ( ( ( ( ( ph /\ e e. A ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) -> ( cgrA ` G ) = .~ )
116 4 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ e e. A ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) -> G e. TarskiG )
117 simp-6r 
 |-  ( ( ( ( ( ( ( ( ph /\ e e. A ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) -> x e. P )
118 simp-5r 
 |-  ( ( ( ( ( ( ( ( ph /\ e e. A ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) -> y e. P )
119 simp-4r 
 |-  ( ( ( ( ( ( ( ( ph /\ e e. A ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) -> z e. P )
120 simplr 
 |-  ( ( ( ( ( ( ( ( ph /\ e e. A ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) -> x =/= y )
121 simpr 
 |-  ( ( ( ( ( ( ( ( ph /\ e e. A ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) -> y =/= z )
122 1 13 116 16 117 118 119 120 121 cgraid 
 |-  ( ( ( ( ( ( ( ( ph /\ e e. A ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) -> <" x y z "> ( cgrA ` G ) <" x y z "> )
123 115 122 breqdi 
 |-  ( ( ( ( ( ( ( ( ph /\ e e. A ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) -> <" x y z "> .~ <" x y z "> )
124 simpllr 
 |-  ( ( ( ( ( ( ( ( ph /\ e e. A ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) -> e = <" x y z "> )
125 123 124 124 3brtr4d 
 |-  ( ( ( ( ( ( ( ( ph /\ e e. A ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ x =/= y ) /\ y =/= z ) -> e .~ e )
126 125 anasss 
 |-  ( ( ( ( ( ( ( ph /\ e e. A ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ ( x =/= y /\ y =/= z ) ) -> e .~ e )
127 126 anasss 
 |-  ( ( ( ( ( ( ph /\ e e. A ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ ( e = <" x y z "> /\ ( x =/= y /\ y =/= z ) ) ) -> e .~ e )
128 127 r19.29an 
 |-  ( ( ( ( ( ph /\ e e. A ) /\ x e. P ) /\ y e. P ) /\ E. z e. P ( e = <" x y z "> /\ ( x =/= y /\ y =/= z ) ) ) -> e .~ e )
129 37 2 114 elcgrabasi 
 |-  ( ( ph /\ e e. A ) -> E. x e. P E. y e. P E. z e. P ( e = <" x y z "> /\ ( x =/= y /\ y =/= z ) ) )
130 128 129 r19.29vva 
 |-  ( ( ph /\ e e. A ) -> e .~ e )
131 brinxp2 
 |-  ( e ( .~ i^i ( A X. A ) ) e <-> ( ( e e. A /\ e e. A ) /\ e .~ e ) )
132 114 114 130 131 syl21anbrc 
 |-  ( ( ph /\ e e. A ) -> e ( .~ i^i ( A X. A ) ) e )
133 131 bilani 
 |-  ( ( ph /\ e ( .~ i^i ( A X. A ) ) e ) -> ( ( e e. A /\ e e. A ) /\ e .~ e ) )
134 133 simplld 
 |-  ( ( ph /\ e ( .~ i^i ( A X. A ) ) e ) -> e e. A )
135 132 134 impbida 
 |-  ( ph -> ( e e. A <-> e ( .~ i^i ( A X. A ) ) e ) )
136 6 47 113 135 iserd 
 |-  ( ph -> ( .~ i^i ( A X. A ) ) Er A )