This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem grlimgrtri

Description: If one of two locally isomorphic graphs has a triangle, so does the other. The triangle in the other graph is not necessarily the image ( F " T ) of the triangle T in the first graph. (Contributed by AV, 24-Aug-2025)

Ref Expression
Hypotheses grlimgrtri.g 
|- ( ph -> G e. USPGraph )
grlimgrtri.h 
|- ( ph -> H e. USPGraph )
grlimgrtri.n 
|- ( ph -> F e. ( G GraphLocIso H ) )
grlimgrtri.t 
|- ( ph -> T e. ( GrTriangles ` G ) )
Assertion grlimgrtri 
|- ( ph -> E. t t e. ( GrTriangles ` H ) )

Proof

Step Hyp Ref Expression
1 grlimgrtri.g 
 |-  ( ph -> G e. USPGraph )
2 grlimgrtri.h 
 |-  ( ph -> H e. USPGraph )
3 grlimgrtri.n 
 |-  ( ph -> F e. ( G GraphLocIso H ) )
4 grlimgrtri.t 
 |-  ( ph -> T e. ( GrTriangles ` G ) )
5 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
6 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
7 5 6 grtriprop 
 |-  ( T e. ( GrTriangles ` G ) -> E. a e. ( Vtx ` G ) E. b e. ( Vtx ` G ) E. c e. ( Vtx ` G ) ( T = { a , b , c } /\ ( # ` T ) = 3 /\ ( { a , b } e. ( Edg ` G ) /\ { a , c } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) ) )
8 4 7 syl 
 |-  ( ph -> E. a e. ( Vtx ` G ) E. b e. ( Vtx ` G ) E. c e. ( Vtx ` G ) ( T = { a , b , c } /\ ( # ` T ) = 3 /\ ( { a , b } e. ( Edg ` G ) /\ { a , c } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) ) )
9 1 2 3 3jca 
 |-  ( ph -> ( G e. USPGraph /\ H e. USPGraph /\ F e. ( G GraphLocIso H ) ) )
10 eqid 
 |-  ( Vtx ` H ) = ( Vtx ` H )
11 eqid 
 |-  ( G ClNeighbVtx v ) = ( G ClNeighbVtx v )
12 eqid 
 |-  ( H ClNeighbVtx ( F ` v ) ) = ( H ClNeighbVtx ( F ` v ) )
13 eqid 
 |-  ( Edg ` H ) = ( Edg ` H )
14 sseq1 
 |-  ( y = x -> ( y C_ ( G ClNeighbVtx v ) <-> x C_ ( G ClNeighbVtx v ) ) )
15 14 cbvrabv 
 |-  { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx v ) } = { x e. ( Edg ` G ) | x C_ ( G ClNeighbVtx v ) }
16 sseq1 
 |-  ( y = x -> ( y C_ ( H ClNeighbVtx ( F ` v ) ) <-> x C_ ( H ClNeighbVtx ( F ` v ) ) ) )
17 16 cbvrabv 
 |-  { y e. ( Edg ` H ) | y C_ ( H ClNeighbVtx ( F ` v ) ) } = { x e. ( Edg ` H ) | x C_ ( H ClNeighbVtx ( F ` v ) ) }
18 5 10 11 12 6 13 15 17 usgrlimprop 
 |-  ( ( G e. USPGraph /\ H e. USPGraph /\ F e. ( G GraphLocIso H ) ) -> ( F : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) /\ A. v e. ( Vtx ` G ) E. f ( f : ( G ClNeighbVtx v ) -1-1-onto-> ( H ClNeighbVtx ( F ` v ) ) /\ E. g ( g : { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx v ) } -1-1-onto-> { y e. ( Edg ` H ) | y C_ ( H ClNeighbVtx ( F ` v ) ) } /\ A. i e. { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx v ) } ( f " i ) = ( g ` i ) ) ) ) )
19 eqidd 
 |-  ( v = a -> f = f )
20 oveq2 
 |-  ( v = a -> ( G ClNeighbVtx v ) = ( G ClNeighbVtx a ) )
21 fveq2 
 |-  ( v = a -> ( F ` v ) = ( F ` a ) )
22 21 oveq2d 
 |-  ( v = a -> ( H ClNeighbVtx ( F ` v ) ) = ( H ClNeighbVtx ( F ` a ) ) )
23 19 20 22 f1oeq123d 
 |-  ( v = a -> ( f : ( G ClNeighbVtx v ) -1-1-onto-> ( H ClNeighbVtx ( F ` v ) ) <-> f : ( G ClNeighbVtx a ) -1-1-onto-> ( H ClNeighbVtx ( F ` a ) ) ) )
24 eqidd 
 |-  ( v = a -> g = g )
25 20 sseq2d 
 |-  ( v = a -> ( y C_ ( G ClNeighbVtx v ) <-> y C_ ( G ClNeighbVtx a ) ) )
26 25 rabbidv 
 |-  ( v = a -> { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx v ) } = { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } )
27 22 sseq2d 
 |-  ( v = a -> ( y C_ ( H ClNeighbVtx ( F ` v ) ) <-> y C_ ( H ClNeighbVtx ( F ` a ) ) ) )
28 27 rabbidv 
 |-  ( v = a -> { y e. ( Edg ` H ) | y C_ ( H ClNeighbVtx ( F ` v ) ) } = { y e. ( Edg ` H ) | y C_ ( H ClNeighbVtx ( F ` a ) ) } )
29 24 26 28 f1oeq123d 
 |-  ( v = a -> ( g : { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx v ) } -1-1-onto-> { y e. ( Edg ` H ) | y C_ ( H ClNeighbVtx ( F ` v ) ) } <-> g : { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } -1-1-onto-> { y e. ( Edg ` H ) | y C_ ( H ClNeighbVtx ( F ` a ) ) } ) )
30 26 raleqdv 
 |-  ( v = a -> ( A. i e. { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx v ) } ( f " i ) = ( g ` i ) <-> A. i e. { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } ( f " i ) = ( g ` i ) ) )
31 29 30 anbi12d 
 |-  ( v = a -> ( ( g : { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx v ) } -1-1-onto-> { y e. ( Edg ` H ) | y C_ ( H ClNeighbVtx ( F ` v ) ) } /\ A. i e. { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx v ) } ( f " i ) = ( g ` i ) ) <-> ( g : { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } -1-1-onto-> { y e. ( Edg ` H ) | y C_ ( H ClNeighbVtx ( F ` a ) ) } /\ A. i e. { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } ( f " i ) = ( g ` i ) ) ) )
32 31 exbidv 
 |-  ( v = a -> ( E. g ( g : { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx v ) } -1-1-onto-> { y e. ( Edg ` H ) | y C_ ( H ClNeighbVtx ( F ` v ) ) } /\ A. i e. { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx v ) } ( f " i ) = ( g ` i ) ) <-> E. g ( g : { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } -1-1-onto-> { y e. ( Edg ` H ) | y C_ ( H ClNeighbVtx ( F ` a ) ) } /\ A. i e. { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } ( f " i ) = ( g ` i ) ) ) )
33 23 32 anbi12d 
 |-  ( v = a -> ( ( f : ( G ClNeighbVtx v ) -1-1-onto-> ( H ClNeighbVtx ( F ` v ) ) /\ E. g ( g : { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx v ) } -1-1-onto-> { y e. ( Edg ` H ) | y C_ ( H ClNeighbVtx ( F ` v ) ) } /\ A. i e. { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx v ) } ( f " i ) = ( g ` i ) ) ) <-> ( f : ( G ClNeighbVtx a ) -1-1-onto-> ( H ClNeighbVtx ( F ` a ) ) /\ E. g ( g : { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } -1-1-onto-> { y e. ( Edg ` H ) | y C_ ( H ClNeighbVtx ( F ` a ) ) } /\ A. i e. { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } ( f " i ) = ( g ` i ) ) ) ) )
34 33 exbidv 
 |-  ( v = a -> ( E. f ( f : ( G ClNeighbVtx v ) -1-1-onto-> ( H ClNeighbVtx ( F ` v ) ) /\ E. g ( g : { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx v ) } -1-1-onto-> { y e. ( Edg ` H ) | y C_ ( H ClNeighbVtx ( F ` v ) ) } /\ A. i e. { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx v ) } ( f " i ) = ( g ` i ) ) ) <-> E. f ( f : ( G ClNeighbVtx a ) -1-1-onto-> ( H ClNeighbVtx ( F ` a ) ) /\ E. g ( g : { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } -1-1-onto-> { y e. ( Edg ` H ) | y C_ ( H ClNeighbVtx ( F ` a ) ) } /\ A. i e. { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } ( f " i ) = ( g ` i ) ) ) ) )
35 34 rspcv 
 |-  ( a e. ( Vtx ` G ) -> ( A. v e. ( Vtx ` G ) E. f ( f : ( G ClNeighbVtx v ) -1-1-onto-> ( H ClNeighbVtx ( F ` v ) ) /\ E. g ( g : { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx v ) } -1-1-onto-> { y e. ( Edg ` H ) | y C_ ( H ClNeighbVtx ( F ` v ) ) } /\ A. i e. { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx v ) } ( f " i ) = ( g ` i ) ) ) -> E. f ( f : ( G ClNeighbVtx a ) -1-1-onto-> ( H ClNeighbVtx ( F ` a ) ) /\ E. g ( g : { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } -1-1-onto-> { y e. ( Edg ` H ) | y C_ ( H ClNeighbVtx ( F ` a ) ) } /\ A. i e. { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } ( f " i ) = ( g ` i ) ) ) ) )
36 35 3ad2ant1 
 |-  ( ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) /\ c e. ( Vtx ` G ) ) -> ( A. v e. ( Vtx ` G ) E. f ( f : ( G ClNeighbVtx v ) -1-1-onto-> ( H ClNeighbVtx ( F ` v ) ) /\ E. g ( g : { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx v ) } -1-1-onto-> { y e. ( Edg ` H ) | y C_ ( H ClNeighbVtx ( F ` v ) ) } /\ A. i e. { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx v ) } ( f " i ) = ( g ` i ) ) ) -> E. f ( f : ( G ClNeighbVtx a ) -1-1-onto-> ( H ClNeighbVtx ( F ` a ) ) /\ E. g ( g : { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } -1-1-onto-> { y e. ( Edg ` H ) | y C_ ( H ClNeighbVtx ( F ` a ) ) } /\ A. i e. { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } ( f " i ) = ( g ` i ) ) ) ) )
37 36 adantl 
 |-  ( ( ph /\ ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) /\ c e. ( Vtx ` G ) ) ) -> ( A. v e. ( Vtx ` G ) E. f ( f : ( G ClNeighbVtx v ) -1-1-onto-> ( H ClNeighbVtx ( F ` v ) ) /\ E. g ( g : { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx v ) } -1-1-onto-> { y e. ( Edg ` H ) | y C_ ( H ClNeighbVtx ( F ` v ) ) } /\ A. i e. { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx v ) } ( f " i ) = ( g ` i ) ) ) -> E. f ( f : ( G ClNeighbVtx a ) -1-1-onto-> ( H ClNeighbVtx ( F ` a ) ) /\ E. g ( g : { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } -1-1-onto-> { y e. ( Edg ` H ) | y C_ ( H ClNeighbVtx ( F ` a ) ) } /\ A. i e. { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } ( f " i ) = ( g ` i ) ) ) ) )
38 tpex 
 |-  { ( f ` a ) , ( f ` b ) , ( f ` c ) } e. _V
39 38 a1i 
 |-  ( ( ( ph /\ ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) /\ c e. ( Vtx ` G ) ) ) /\ ( ( g : { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } -1-1-onto-> { y e. ( Edg ` H ) | y C_ ( H ClNeighbVtx ( F ` a ) ) } /\ A. i e. { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } ( f " i ) = ( g ` i ) ) /\ f : ( G ClNeighbVtx a ) -1-1-onto-> ( H ClNeighbVtx ( F ` a ) ) /\ F : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) ) /\ ( T = { a , b , c } /\ ( # ` T ) = 3 /\ ( { a , b } e. ( Edg ` G ) /\ { a , c } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) ) ) -> { ( f ` a ) , ( f ` b ) , ( f ` c ) } e. _V )
40 f1of1 
 |-  ( f : ( G ClNeighbVtx a ) -1-1-onto-> ( H ClNeighbVtx ( F ` a ) ) -> f : ( G ClNeighbVtx a ) -1-1-> ( H ClNeighbVtx ( F ` a ) ) )
41 40 3ad2ant2 
 |-  ( ( ( g : { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } -1-1-onto-> { y e. ( Edg ` H ) | y C_ ( H ClNeighbVtx ( F ` a ) ) } /\ A. i e. { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } ( f " i ) = ( g ` i ) ) /\ f : ( G ClNeighbVtx a ) -1-1-onto-> ( H ClNeighbVtx ( F ` a ) ) /\ F : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) ) -> f : ( G ClNeighbVtx a ) -1-1-> ( H ClNeighbVtx ( F ` a ) ) )
42 41 3ad2ant2 
 |-  ( ( ( ph /\ ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) /\ c e. ( Vtx ` G ) ) ) /\ ( ( g : { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } -1-1-onto-> { y e. ( Edg ` H ) | y C_ ( H ClNeighbVtx ( F ` a ) ) } /\ A. i e. { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } ( f " i ) = ( g ` i ) ) /\ f : ( G ClNeighbVtx a ) -1-1-onto-> ( H ClNeighbVtx ( F ` a ) ) /\ F : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) ) /\ ( T = { a , b , c } /\ ( # ` T ) = 3 /\ ( { a , b } e. ( Edg ` G ) /\ { a , c } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) ) ) -> f : ( G ClNeighbVtx a ) -1-1-> ( H ClNeighbVtx ( F ` a ) ) )
43 5 clnbgrvtxel 
 |-  ( a e. ( Vtx ` G ) -> a e. ( G ClNeighbVtx a ) )
44 43 3ad2ant1 
 |-  ( ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) /\ c e. ( Vtx ` G ) ) -> a e. ( G ClNeighbVtx a ) )
45 44 adantr 
 |-  ( ( ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) /\ c e. ( Vtx ` G ) ) /\ ( { a , b } e. ( Edg ` G ) /\ { a , c } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) ) -> a e. ( G ClNeighbVtx a ) )
46 simplr 
 |-  ( ( ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) /\ { a , b } e. ( Edg ` G ) ) -> b e. ( Vtx ` G ) )
47 simpll 
 |-  ( ( ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) /\ { a , b } e. ( Edg ` G ) ) -> a e. ( Vtx ` G ) )
48 simpr 
 |-  ( ( ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) /\ { a , b } e. ( Edg ` G ) ) -> { a , b } e. ( Edg ` G ) )
49 5 6 predgclnbgrel 
 |-  ( ( b e. ( Vtx ` G ) /\ a e. ( Vtx ` G ) /\ { a , b } e. ( Edg ` G ) ) -> b e. ( G ClNeighbVtx a ) )
50 46 47 48 49 syl3anc 
 |-  ( ( ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) /\ { a , b } e. ( Edg ` G ) ) -> b e. ( G ClNeighbVtx a ) )
51 50 2a1d 
 |-  ( ( ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) /\ { a , b } e. ( Edg ` G ) ) -> ( { a , c } e. ( Edg ` G ) -> ( { b , c } e. ( Edg ` G ) -> b e. ( G ClNeighbVtx a ) ) ) )
52 51 ex 
 |-  ( ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) -> ( { a , b } e. ( Edg ` G ) -> ( { a , c } e. ( Edg ` G ) -> ( { b , c } e. ( Edg ` G ) -> b e. ( G ClNeighbVtx a ) ) ) ) )
53 52 3impd 
 |-  ( ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) -> ( ( { a , b } e. ( Edg ` G ) /\ { a , c } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) -> b e. ( G ClNeighbVtx a ) ) )
54 53 3adant3 
 |-  ( ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) /\ c e. ( Vtx ` G ) ) -> ( ( { a , b } e. ( Edg ` G ) /\ { a , c } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) -> b e. ( G ClNeighbVtx a ) ) )
55 54 imp 
 |-  ( ( ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) /\ c e. ( Vtx ` G ) ) /\ ( { a , b } e. ( Edg ` G ) /\ { a , c } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) ) -> b e. ( G ClNeighbVtx a ) )
56 simplr 
 |-  ( ( ( a e. ( Vtx ` G ) /\ c e. ( Vtx ` G ) ) /\ { a , c } e. ( Edg ` G ) ) -> c e. ( Vtx ` G ) )
57 simpll 
 |-  ( ( ( a e. ( Vtx ` G ) /\ c e. ( Vtx ` G ) ) /\ { a , c } e. ( Edg ` G ) ) -> a e. ( Vtx ` G ) )
58 simpr 
 |-  ( ( ( a e. ( Vtx ` G ) /\ c e. ( Vtx ` G ) ) /\ { a , c } e. ( Edg ` G ) ) -> { a , c } e. ( Edg ` G ) )
59 5 6 predgclnbgrel 
 |-  ( ( c e. ( Vtx ` G ) /\ a e. ( Vtx ` G ) /\ { a , c } e. ( Edg ` G ) ) -> c e. ( G ClNeighbVtx a ) )
60 56 57 58 59 syl3anc 
 |-  ( ( ( a e. ( Vtx ` G ) /\ c e. ( Vtx ` G ) ) /\ { a , c } e. ( Edg ` G ) ) -> c e. ( G ClNeighbVtx a ) )
61 60 a1d 
 |-  ( ( ( a e. ( Vtx ` G ) /\ c e. ( Vtx ` G ) ) /\ { a , c } e. ( Edg ` G ) ) -> ( { b , c } e. ( Edg ` G ) -> c e. ( G ClNeighbVtx a ) ) )
62 61 ex 
 |-  ( ( a e. ( Vtx ` G ) /\ c e. ( Vtx ` G ) ) -> ( { a , c } e. ( Edg ` G ) -> ( { b , c } e. ( Edg ` G ) -> c e. ( G ClNeighbVtx a ) ) ) )
63 62 a1d 
 |-  ( ( a e. ( Vtx ` G ) /\ c e. ( Vtx ` G ) ) -> ( { a , b } e. ( Edg ` G ) -> ( { a , c } e. ( Edg ` G ) -> ( { b , c } e. ( Edg ` G ) -> c e. ( G ClNeighbVtx a ) ) ) ) )
64 63 3impd 
 |-  ( ( a e. ( Vtx ` G ) /\ c e. ( Vtx ` G ) ) -> ( ( { a , b } e. ( Edg ` G ) /\ { a , c } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) -> c e. ( G ClNeighbVtx a ) ) )
65 64 3adant2 
 |-  ( ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) /\ c e. ( Vtx ` G ) ) -> ( ( { a , b } e. ( Edg ` G ) /\ { a , c } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) -> c e. ( G ClNeighbVtx a ) ) )
66 65 imp 
 |-  ( ( ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) /\ c e. ( Vtx ` G ) ) /\ ( { a , b } e. ( Edg ` G ) /\ { a , c } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) ) -> c e. ( G ClNeighbVtx a ) )
67 45 55 66 3jca 
 |-  ( ( ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) /\ c e. ( Vtx ` G ) ) /\ ( { a , b } e. ( Edg ` G ) /\ { a , c } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) ) -> ( a e. ( G ClNeighbVtx a ) /\ b e. ( G ClNeighbVtx a ) /\ c e. ( G ClNeighbVtx a ) ) )
68 67 ex 
 |-  ( ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) /\ c e. ( Vtx ` G ) ) -> ( ( { a , b } e. ( Edg ` G ) /\ { a , c } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) -> ( a e. ( G ClNeighbVtx a ) /\ b e. ( G ClNeighbVtx a ) /\ c e. ( G ClNeighbVtx a ) ) ) )
69 68 2a1d 
 |-  ( ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) /\ c e. ( Vtx ` G ) ) -> ( T = { a , b , c } -> ( ( # ` T ) = 3 -> ( ( { a , b } e. ( Edg ` G ) /\ { a , c } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) -> ( a e. ( G ClNeighbVtx a ) /\ b e. ( G ClNeighbVtx a ) /\ c e. ( G ClNeighbVtx a ) ) ) ) ) )
70 69 3impd 
 |-  ( ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) /\ c e. ( Vtx ` G ) ) -> ( ( T = { a , b , c } /\ ( # ` T ) = 3 /\ ( { a , b } e. ( Edg ` G ) /\ { a , c } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) ) -> ( a e. ( G ClNeighbVtx a ) /\ b e. ( G ClNeighbVtx a ) /\ c e. ( G ClNeighbVtx a ) ) ) )
71 70 a1d 
 |-  ( ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) /\ c e. ( Vtx ` G ) ) -> ( ( ( g : { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } -1-1-onto-> { y e. ( Edg ` H ) | y C_ ( H ClNeighbVtx ( F ` a ) ) } /\ A. i e. { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } ( f " i ) = ( g ` i ) ) /\ f : ( G ClNeighbVtx a ) -1-1-onto-> ( H ClNeighbVtx ( F ` a ) ) /\ F : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) ) -> ( ( T = { a , b , c } /\ ( # ` T ) = 3 /\ ( { a , b } e. ( Edg ` G ) /\ { a , c } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) ) -> ( a e. ( G ClNeighbVtx a ) /\ b e. ( G ClNeighbVtx a ) /\ c e. ( G ClNeighbVtx a ) ) ) ) )
72 71 adantl 
 |-  ( ( ph /\ ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) /\ c e. ( Vtx ` G ) ) ) -> ( ( ( g : { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } -1-1-onto-> { y e. ( Edg ` H ) | y C_ ( H ClNeighbVtx ( F ` a ) ) } /\ A. i e. { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } ( f " i ) = ( g ` i ) ) /\ f : ( G ClNeighbVtx a ) -1-1-onto-> ( H ClNeighbVtx ( F ` a ) ) /\ F : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) ) -> ( ( T = { a , b , c } /\ ( # ` T ) = 3 /\ ( { a , b } e. ( Edg ` G ) /\ { a , c } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) ) -> ( a e. ( G ClNeighbVtx a ) /\ b e. ( G ClNeighbVtx a ) /\ c e. ( G ClNeighbVtx a ) ) ) ) )
73 72 3imp 
 |-  ( ( ( ph /\ ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) /\ c e. ( Vtx ` G ) ) ) /\ ( ( g : { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } -1-1-onto-> { y e. ( Edg ` H ) | y C_ ( H ClNeighbVtx ( F ` a ) ) } /\ A. i e. { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } ( f " i ) = ( g ` i ) ) /\ f : ( G ClNeighbVtx a ) -1-1-onto-> ( H ClNeighbVtx ( F ` a ) ) /\ F : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) ) /\ ( T = { a , b , c } /\ ( # ` T ) = 3 /\ ( { a , b } e. ( Edg ` G ) /\ { a , c } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) ) ) -> ( a e. ( G ClNeighbVtx a ) /\ b e. ( G ClNeighbVtx a ) /\ c e. ( G ClNeighbVtx a ) ) )
74 3simpa 
 |-  ( ( T = { a , b , c } /\ ( # ` T ) = 3 /\ ( { a , b } e. ( Edg ` G ) /\ { a , c } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) ) -> ( T = { a , b , c } /\ ( # ` T ) = 3 ) )
75 74 3ad2ant3 
 |-  ( ( ( ph /\ ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) /\ c e. ( Vtx ` G ) ) ) /\ ( ( g : { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } -1-1-onto-> { y e. ( Edg ` H ) | y C_ ( H ClNeighbVtx ( F ` a ) ) } /\ A. i e. { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } ( f " i ) = ( g ` i ) ) /\ f : ( G ClNeighbVtx a ) -1-1-onto-> ( H ClNeighbVtx ( F ` a ) ) /\ F : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) ) /\ ( T = { a , b , c } /\ ( # ` T ) = 3 /\ ( { a , b } e. ( Edg ` G ) /\ { a , c } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) ) ) -> ( T = { a , b , c } /\ ( # ` T ) = 3 ) )
76 73 75 jca 
 |-  ( ( ( ph /\ ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) /\ c e. ( Vtx ` G ) ) ) /\ ( ( g : { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } -1-1-onto-> { y e. ( Edg ` H ) | y C_ ( H ClNeighbVtx ( F ` a ) ) } /\ A. i e. { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } ( f " i ) = ( g ` i ) ) /\ f : ( G ClNeighbVtx a ) -1-1-onto-> ( H ClNeighbVtx ( F ` a ) ) /\ F : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) ) /\ ( T = { a , b , c } /\ ( # ` T ) = 3 /\ ( { a , b } e. ( Edg ` G ) /\ { a , c } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) ) ) -> ( ( a e. ( G ClNeighbVtx a ) /\ b e. ( G ClNeighbVtx a ) /\ c e. ( G ClNeighbVtx a ) ) /\ ( T = { a , b , c } /\ ( # ` T ) = 3 ) ) )
77 grtrimap 
 |-  ( f : ( G ClNeighbVtx a ) -1-1-> ( H ClNeighbVtx ( F ` a ) ) -> ( ( ( a e. ( G ClNeighbVtx a ) /\ b e. ( G ClNeighbVtx a ) /\ c e. ( G ClNeighbVtx a ) ) /\ ( T = { a , b , c } /\ ( # ` T ) = 3 ) ) -> ( ( ( f ` a ) e. ( H ClNeighbVtx ( F ` a ) ) /\ ( f ` b ) e. ( H ClNeighbVtx ( F ` a ) ) /\ ( f ` c ) e. ( H ClNeighbVtx ( F ` a ) ) ) /\ ( f " T ) = { ( f ` a ) , ( f ` b ) , ( f ` c ) } /\ ( # ` ( f " T ) ) = 3 ) ) )
78 42 76 77 sylc 
 |-  ( ( ( ph /\ ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) /\ c e. ( Vtx ` G ) ) ) /\ ( ( g : { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } -1-1-onto-> { y e. ( Edg ` H ) | y C_ ( H ClNeighbVtx ( F ` a ) ) } /\ A. i e. { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } ( f " i ) = ( g ` i ) ) /\ f : ( G ClNeighbVtx a ) -1-1-onto-> ( H ClNeighbVtx ( F ` a ) ) /\ F : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) ) /\ ( T = { a , b , c } /\ ( # ` T ) = 3 /\ ( { a , b } e. ( Edg ` G ) /\ { a , c } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) ) ) -> ( ( ( f ` a ) e. ( H ClNeighbVtx ( F ` a ) ) /\ ( f ` b ) e. ( H ClNeighbVtx ( F ` a ) ) /\ ( f ` c ) e. ( H ClNeighbVtx ( F ` a ) ) ) /\ ( f " T ) = { ( f ` a ) , ( f ` b ) , ( f ` c ) } /\ ( # ` ( f " T ) ) = 3 ) )
79 tpeq1 
 |-  ( x = ( f ` a ) -> { x , y , z } = { ( f ` a ) , y , z } )
80 79 eqeq2d 
 |-  ( x = ( f ` a ) -> ( { ( f ` a ) , ( f ` b ) , ( f ` c ) } = { x , y , z } <-> { ( f ` a ) , ( f ` b ) , ( f ` c ) } = { ( f ` a ) , y , z } ) )
81 preq1 
 |-  ( x = ( f ` a ) -> { x , y } = { ( f ` a ) , y } )
82 81 eleq1d 
 |-  ( x = ( f ` a ) -> ( { x , y } e. ( Edg ` H ) <-> { ( f ` a ) , y } e. ( Edg ` H ) ) )
83 preq1 
 |-  ( x = ( f ` a ) -> { x , z } = { ( f ` a ) , z } )
84 83 eleq1d 
 |-  ( x = ( f ` a ) -> ( { x , z } e. ( Edg ` H ) <-> { ( f ` a ) , z } e. ( Edg ` H ) ) )
85 82 84 3anbi12d 
 |-  ( x = ( f ` a ) -> ( ( { x , y } e. ( Edg ` H ) /\ { x , z } e. ( Edg ` H ) /\ { y , z } e. ( Edg ` H ) ) <-> ( { ( f ` a ) , y } e. ( Edg ` H ) /\ { ( f ` a ) , z } e. ( Edg ` H ) /\ { y , z } e. ( Edg ` H ) ) ) )
86 80 85 3anbi13d 
 |-  ( x = ( f ` a ) -> ( ( { ( f ` a ) , ( f ` b ) , ( f ` c ) } = { x , y , z } /\ ( # ` { ( f ` a ) , ( f ` b ) , ( f ` c ) } ) = 3 /\ ( { x , y } e. ( Edg ` H ) /\ { x , z } e. ( Edg ` H ) /\ { y , z } e. ( Edg ` H ) ) ) <-> ( { ( f ` a ) , ( f ` b ) , ( f ` c ) } = { ( f ` a ) , y , z } /\ ( # ` { ( f ` a ) , ( f ` b ) , ( f ` c ) } ) = 3 /\ ( { ( f ` a ) , y } e. ( Edg ` H ) /\ { ( f ` a ) , z } e. ( Edg ` H ) /\ { y , z } e. ( Edg ` H ) ) ) ) )
87 tpeq2 
 |-  ( y = ( f ` b ) -> { ( f ` a ) , y , z } = { ( f ` a ) , ( f ` b ) , z } )
88 87 eqeq2d 
 |-  ( y = ( f ` b ) -> ( { ( f ` a ) , ( f ` b ) , ( f ` c ) } = { ( f ` a ) , y , z } <-> { ( f ` a ) , ( f ` b ) , ( f ` c ) } = { ( f ` a ) , ( f ` b ) , z } ) )
89 preq2 
 |-  ( y = ( f ` b ) -> { ( f ` a ) , y } = { ( f ` a ) , ( f ` b ) } )
90 89 eleq1d 
 |-  ( y = ( f ` b ) -> ( { ( f ` a ) , y } e. ( Edg ` H ) <-> { ( f ` a ) , ( f ` b ) } e. ( Edg ` H ) ) )
91 preq1 
 |-  ( y = ( f ` b ) -> { y , z } = { ( f ` b ) , z } )
92 91 eleq1d 
 |-  ( y = ( f ` b ) -> ( { y , z } e. ( Edg ` H ) <-> { ( f ` b ) , z } e. ( Edg ` H ) ) )
93 90 92 3anbi13d 
 |-  ( y = ( f ` b ) -> ( ( { ( f ` a ) , y } e. ( Edg ` H ) /\ { ( f ` a ) , z } e. ( Edg ` H ) /\ { y , z } e. ( Edg ` H ) ) <-> ( { ( f ` a ) , ( f ` b ) } e. ( Edg ` H ) /\ { ( f ` a ) , z } e. ( Edg ` H ) /\ { ( f ` b ) , z } e. ( Edg ` H ) ) ) )
94 88 93 3anbi13d 
 |-  ( y = ( f ` b ) -> ( ( { ( f ` a ) , ( f ` b ) , ( f ` c ) } = { ( f ` a ) , y , z } /\ ( # ` { ( f ` a ) , ( f ` b ) , ( f ` c ) } ) = 3 /\ ( { ( f ` a ) , y } e. ( Edg ` H ) /\ { ( f ` a ) , z } e. ( Edg ` H ) /\ { y , z } e. ( Edg ` H ) ) ) <-> ( { ( f ` a ) , ( f ` b ) , ( f ` c ) } = { ( f ` a ) , ( f ` b ) , z } /\ ( # ` { ( f ` a ) , ( f ` b ) , ( f ` c ) } ) = 3 /\ ( { ( f ` a ) , ( f ` b ) } e. ( Edg ` H ) /\ { ( f ` a ) , z } e. ( Edg ` H ) /\ { ( f ` b ) , z } e. ( Edg ` H ) ) ) ) )
95 tpeq3 
 |-  ( z = ( f ` c ) -> { ( f ` a ) , ( f ` b ) , z } = { ( f ` a ) , ( f ` b ) , ( f ` c ) } )
96 95 eqeq2d 
 |-  ( z = ( f ` c ) -> ( { ( f ` a ) , ( f ` b ) , ( f ` c ) } = { ( f ` a ) , ( f ` b ) , z } <-> { ( f ` a ) , ( f ` b ) , ( f ` c ) } = { ( f ` a ) , ( f ` b ) , ( f ` c ) } ) )
97 preq2 
 |-  ( z = ( f ` c ) -> { ( f ` a ) , z } = { ( f ` a ) , ( f ` c ) } )
98 97 eleq1d 
 |-  ( z = ( f ` c ) -> ( { ( f ` a ) , z } e. ( Edg ` H ) <-> { ( f ` a ) , ( f ` c ) } e. ( Edg ` H ) ) )
99 preq2 
 |-  ( z = ( f ` c ) -> { ( f ` b ) , z } = { ( f ` b ) , ( f ` c ) } )
100 99 eleq1d 
 |-  ( z = ( f ` c ) -> ( { ( f ` b ) , z } e. ( Edg ` H ) <-> { ( f ` b ) , ( f ` c ) } e. ( Edg ` H ) ) )
101 98 100 3anbi23d 
 |-  ( z = ( f ` c ) -> ( ( { ( f ` a ) , ( f ` b ) } e. ( Edg ` H ) /\ { ( f ` a ) , z } e. ( Edg ` H ) /\ { ( f ` b ) , z } e. ( Edg ` H ) ) <-> ( { ( f ` a ) , ( f ` b ) } e. ( Edg ` H ) /\ { ( f ` a ) , ( f ` c ) } e. ( Edg ` H ) /\ { ( f ` b ) , ( f ` c ) } e. ( Edg ` H ) ) ) )
102 96 101 3anbi13d 
 |-  ( z = ( f ` c ) -> ( ( { ( f ` a ) , ( f ` b ) , ( f ` c ) } = { ( f ` a ) , ( f ` b ) , z } /\ ( # ` { ( f ` a ) , ( f ` b ) , ( f ` c ) } ) = 3 /\ ( { ( f ` a ) , ( f ` b ) } e. ( Edg ` H ) /\ { ( f ` a ) , z } e. ( Edg ` H ) /\ { ( f ` b ) , z } e. ( Edg ` H ) ) ) <-> ( { ( f ` a ) , ( f ` b ) , ( f ` c ) } = { ( f ` a ) , ( f ` b ) , ( f ` c ) } /\ ( # ` { ( f ` a ) , ( f ` b ) , ( f ` c ) } ) = 3 /\ ( { ( f ` a ) , ( f ` b ) } e. ( Edg ` H ) /\ { ( f ` a ) , ( f ` c ) } e. ( Edg ` H ) /\ { ( f ` b ) , ( f ` c ) } e. ( Edg ` H ) ) ) ) )
103 10 clnbgrisvtx 
 |-  ( ( f ` a ) e. ( H ClNeighbVtx ( F ` a ) ) -> ( f ` a ) e. ( Vtx ` H ) )
104 103 3ad2ant1 
 |-  ( ( ( f ` a ) e. ( H ClNeighbVtx ( F ` a ) ) /\ ( f ` b ) e. ( H ClNeighbVtx ( F ` a ) ) /\ ( f ` c ) e. ( H ClNeighbVtx ( F ` a ) ) ) -> ( f ` a ) e. ( Vtx ` H ) )
105 104 3ad2ant1 
 |-  ( ( ( ( f ` a ) e. ( H ClNeighbVtx ( F ` a ) ) /\ ( f ` b ) e. ( H ClNeighbVtx ( F ` a ) ) /\ ( f ` c ) e. ( H ClNeighbVtx ( F ` a ) ) ) /\ ( f " T ) = { ( f ` a ) , ( f ` b ) , ( f ` c ) } /\ ( # ` ( f " T ) ) = 3 ) -> ( f ` a ) e. ( Vtx ` H ) )
106 105 adantl 
 |-  ( ( ( ( ph /\ ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) /\ c e. ( Vtx ` G ) ) ) /\ ( ( g : { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } -1-1-onto-> { y e. ( Edg ` H ) | y C_ ( H ClNeighbVtx ( F ` a ) ) } /\ A. i e. { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } ( f " i ) = ( g ` i ) ) /\ f : ( G ClNeighbVtx a ) -1-1-onto-> ( H ClNeighbVtx ( F ` a ) ) /\ F : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) ) /\ ( T = { a , b , c } /\ ( # ` T ) = 3 /\ ( { a , b } e. ( Edg ` G ) /\ { a , c } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) ) ) /\ ( ( ( f ` a ) e. ( H ClNeighbVtx ( F ` a ) ) /\ ( f ` b ) e. ( H ClNeighbVtx ( F ` a ) ) /\ ( f ` c ) e. ( H ClNeighbVtx ( F ` a ) ) ) /\ ( f " T ) = { ( f ` a ) , ( f ` b ) , ( f ` c ) } /\ ( # ` ( f " T ) ) = 3 ) ) -> ( f ` a ) e. ( Vtx ` H ) )
107 10 clnbgrisvtx 
 |-  ( ( f ` b ) e. ( H ClNeighbVtx ( F ` a ) ) -> ( f ` b ) e. ( Vtx ` H ) )
108 107 3ad2ant2 
 |-  ( ( ( f ` a ) e. ( H ClNeighbVtx ( F ` a ) ) /\ ( f ` b ) e. ( H ClNeighbVtx ( F ` a ) ) /\ ( f ` c ) e. ( H ClNeighbVtx ( F ` a ) ) ) -> ( f ` b ) e. ( Vtx ` H ) )
109 108 3ad2ant1 
 |-  ( ( ( ( f ` a ) e. ( H ClNeighbVtx ( F ` a ) ) /\ ( f ` b ) e. ( H ClNeighbVtx ( F ` a ) ) /\ ( f ` c ) e. ( H ClNeighbVtx ( F ` a ) ) ) /\ ( f " T ) = { ( f ` a ) , ( f ` b ) , ( f ` c ) } /\ ( # ` ( f " T ) ) = 3 ) -> ( f ` b ) e. ( Vtx ` H ) )
110 109 adantl 
 |-  ( ( ( ( ph /\ ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) /\ c e. ( Vtx ` G ) ) ) /\ ( ( g : { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } -1-1-onto-> { y e. ( Edg ` H ) | y C_ ( H ClNeighbVtx ( F ` a ) ) } /\ A. i e. { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } ( f " i ) = ( g ` i ) ) /\ f : ( G ClNeighbVtx a ) -1-1-onto-> ( H ClNeighbVtx ( F ` a ) ) /\ F : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) ) /\ ( T = { a , b , c } /\ ( # ` T ) = 3 /\ ( { a , b } e. ( Edg ` G ) /\ { a , c } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) ) ) /\ ( ( ( f ` a ) e. ( H ClNeighbVtx ( F ` a ) ) /\ ( f ` b ) e. ( H ClNeighbVtx ( F ` a ) ) /\ ( f ` c ) e. ( H ClNeighbVtx ( F ` a ) ) ) /\ ( f " T ) = { ( f ` a ) , ( f ` b ) , ( f ` c ) } /\ ( # ` ( f " T ) ) = 3 ) ) -> ( f ` b ) e. ( Vtx ` H ) )
111 10 clnbgrisvtx 
 |-  ( ( f ` c ) e. ( H ClNeighbVtx ( F ` a ) ) -> ( f ` c ) e. ( Vtx ` H ) )
112 111 3ad2ant3 
 |-  ( ( ( f ` a ) e. ( H ClNeighbVtx ( F ` a ) ) /\ ( f ` b ) e. ( H ClNeighbVtx ( F ` a ) ) /\ ( f ` c ) e. ( H ClNeighbVtx ( F ` a ) ) ) -> ( f ` c ) e. ( Vtx ` H ) )
113 112 3ad2ant1 
 |-  ( ( ( ( f ` a ) e. ( H ClNeighbVtx ( F ` a ) ) /\ ( f ` b ) e. ( H ClNeighbVtx ( F ` a ) ) /\ ( f ` c ) e. ( H ClNeighbVtx ( F ` a ) ) ) /\ ( f " T ) = { ( f ` a ) , ( f ` b ) , ( f ` c ) } /\ ( # ` ( f " T ) ) = 3 ) -> ( f ` c ) e. ( Vtx ` H ) )
114 113 adantl 
 |-  ( ( ( ( ph /\ ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) /\ c e. ( Vtx ` G ) ) ) /\ ( ( g : { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } -1-1-onto-> { y e. ( Edg ` H ) | y C_ ( H ClNeighbVtx ( F ` a ) ) } /\ A. i e. { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } ( f " i ) = ( g ` i ) ) /\ f : ( G ClNeighbVtx a ) -1-1-onto-> ( H ClNeighbVtx ( F ` a ) ) /\ F : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) ) /\ ( T = { a , b , c } /\ ( # ` T ) = 3 /\ ( { a , b } e. ( Edg ` G ) /\ { a , c } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) ) ) /\ ( ( ( f ` a ) e. ( H ClNeighbVtx ( F ` a ) ) /\ ( f ` b ) e. ( H ClNeighbVtx ( F ` a ) ) /\ ( f ` c ) e. ( H ClNeighbVtx ( F ` a ) ) ) /\ ( f " T ) = { ( f ` a ) , ( f ` b ) , ( f ` c ) } /\ ( # ` ( f " T ) ) = 3 ) ) -> ( f ` c ) e. ( Vtx ` H ) )
115 eqidd 
 |-  ( ( ( ( ph /\ ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) /\ c e. ( Vtx ` G ) ) ) /\ ( ( g : { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } -1-1-onto-> { y e. ( Edg ` H ) | y C_ ( H ClNeighbVtx ( F ` a ) ) } /\ A. i e. { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } ( f " i ) = ( g ` i ) ) /\ f : ( G ClNeighbVtx a ) -1-1-onto-> ( H ClNeighbVtx ( F ` a ) ) /\ F : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) ) /\ ( T = { a , b , c } /\ ( # ` T ) = 3 /\ ( { a , b } e. ( Edg ` G ) /\ { a , c } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) ) ) /\ ( ( ( f ` a ) e. ( H ClNeighbVtx ( F ` a ) ) /\ ( f ` b ) e. ( H ClNeighbVtx ( F ` a ) ) /\ ( f ` c ) e. ( H ClNeighbVtx ( F ` a ) ) ) /\ ( f " T ) = { ( f ` a ) , ( f ` b ) , ( f ` c ) } /\ ( # ` ( f " T ) ) = 3 ) ) -> { ( f ` a ) , ( f ` b ) , ( f ` c ) } = { ( f ` a ) , ( f ` b ) , ( f ` c ) } )
116 fveq2 
 |-  ( { ( f ` a ) , ( f ` b ) , ( f ` c ) } = ( f " T ) -> ( # ` { ( f ` a ) , ( f ` b ) , ( f ` c ) } ) = ( # ` ( f " T ) ) )
117 116 eqcoms 
 |-  ( ( f " T ) = { ( f ` a ) , ( f ` b ) , ( f ` c ) } -> ( # ` { ( f ` a ) , ( f ` b ) , ( f ` c ) } ) = ( # ` ( f " T ) ) )
118 117 3ad2ant2 
 |-  ( ( ( ( f ` a ) e. ( H ClNeighbVtx ( F ` a ) ) /\ ( f ` b ) e. ( H ClNeighbVtx ( F ` a ) ) /\ ( f ` c ) e. ( H ClNeighbVtx ( F ` a ) ) ) /\ ( f " T ) = { ( f ` a ) , ( f ` b ) , ( f ` c ) } /\ ( # ` ( f " T ) ) = 3 ) -> ( # ` { ( f ` a ) , ( f ` b ) , ( f ` c ) } ) = ( # ` ( f " T ) ) )
119 simp3 
 |-  ( ( ( ( f ` a ) e. ( H ClNeighbVtx ( F ` a ) ) /\ ( f ` b ) e. ( H ClNeighbVtx ( F ` a ) ) /\ ( f ` c ) e. ( H ClNeighbVtx ( F ` a ) ) ) /\ ( f " T ) = { ( f ` a ) , ( f ` b ) , ( f ` c ) } /\ ( # ` ( f " T ) ) = 3 ) -> ( # ` ( f " T ) ) = 3 )
120 118 119 eqtrd 
 |-  ( ( ( ( f ` a ) e. ( H ClNeighbVtx ( F ` a ) ) /\ ( f ` b ) e. ( H ClNeighbVtx ( F ` a ) ) /\ ( f ` c ) e. ( H ClNeighbVtx ( F ` a ) ) ) /\ ( f " T ) = { ( f ` a ) , ( f ` b ) , ( f ` c ) } /\ ( # ` ( f " T ) ) = 3 ) -> ( # ` { ( f ` a ) , ( f ` b ) , ( f ` c ) } ) = 3 )
121 120 adantl 
 |-  ( ( ( ( ph /\ ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) /\ c e. ( Vtx ` G ) ) ) /\ ( ( g : { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } -1-1-onto-> { y e. ( Edg ` H ) | y C_ ( H ClNeighbVtx ( F ` a ) ) } /\ A. i e. { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } ( f " i ) = ( g ` i ) ) /\ f : ( G ClNeighbVtx a ) -1-1-onto-> ( H ClNeighbVtx ( F ` a ) ) /\ F : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) ) /\ ( T = { a , b , c } /\ ( # ` T ) = 3 /\ ( { a , b } e. ( Edg ` G ) /\ { a , c } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) ) ) /\ ( ( ( f ` a ) e. ( H ClNeighbVtx ( F ` a ) ) /\ ( f ` b ) e. ( H ClNeighbVtx ( F ` a ) ) /\ ( f ` c ) e. ( H ClNeighbVtx ( F ` a ) ) ) /\ ( f " T ) = { ( f ` a ) , ( f ` b ) , ( f ` c ) } /\ ( # ` ( f " T ) ) = 3 ) ) -> ( # ` { ( f ` a ) , ( f ` b ) , ( f ` c ) } ) = 3 )
122 uspgruhgr 
 |-  ( G e. USPGraph -> G e. UHGraph )
123 1 122 syl 
 |-  ( ph -> G e. UHGraph )
124 123 adantr 
 |-  ( ( ph /\ ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) /\ c e. ( Vtx ` G ) ) ) -> G e. UHGraph )
125 simp3 
 |-  ( ( T = { a , b , c } /\ ( # ` T ) = 3 /\ ( { a , b } e. ( Edg ` G ) /\ { a , c } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) ) -> ( { a , b } e. ( Edg ` G ) /\ { a , c } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) )
126 124 125 anim12i 
 |-  ( ( ( ph /\ ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) /\ c e. ( Vtx ` G ) ) ) /\ ( T = { a , b , c } /\ ( # ` T ) = 3 /\ ( { a , b } e. ( Edg ` G ) /\ { a , c } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) ) ) -> ( G e. UHGraph /\ ( { a , b } e. ( Edg ` G ) /\ { a , c } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) ) )
127 126 3adant2 
 |-  ( ( ( ph /\ ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) /\ c e. ( Vtx ` G ) ) ) /\ ( ( g : { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } -1-1-onto-> { y e. ( Edg ` H ) | y C_ ( H ClNeighbVtx ( F ` a ) ) } /\ A. i e. { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } ( f " i ) = ( g ` i ) ) /\ f : ( G ClNeighbVtx a ) -1-1-onto-> ( H ClNeighbVtx ( F ` a ) ) /\ F : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) ) /\ ( T = { a , b , c } /\ ( # ` T ) = 3 /\ ( { a , b } e. ( Edg ` G ) /\ { a , c } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) ) ) -> ( G e. UHGraph /\ ( { a , b } e. ( Edg ` G ) /\ { a , c } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) ) )
128 127 adantr 
 |-  ( ( ( ( ph /\ ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) /\ c e. ( Vtx ` G ) ) ) /\ ( ( g : { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } -1-1-onto-> { y e. ( Edg ` H ) | y C_ ( H ClNeighbVtx ( F ` a ) ) } /\ A. i e. { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } ( f " i ) = ( g ` i ) ) /\ f : ( G ClNeighbVtx a ) -1-1-onto-> ( H ClNeighbVtx ( F ` a ) ) /\ F : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) ) /\ ( T = { a , b , c } /\ ( # ` T ) = 3 /\ ( { a , b } e. ( Edg ` G ) /\ { a , c } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) ) ) /\ ( ( ( f ` a ) e. ( H ClNeighbVtx ( F ` a ) ) /\ ( f ` b ) e. ( H ClNeighbVtx ( F ` a ) ) /\ ( f ` c ) e. ( H ClNeighbVtx ( F ` a ) ) ) /\ ( f " T ) = { ( f ` a ) , ( f ` b ) , ( f ` c ) } /\ ( # ` ( f " T ) ) = 3 ) ) -> ( G e. UHGraph /\ ( { a , b } e. ( Edg ` G ) /\ { a , c } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) ) )
129 eqid 
 |-  ( G ClNeighbVtx a ) = ( G ClNeighbVtx a )
130 eqid 
 |-  { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } = { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) }
131 5 129 6 130 grlimgrtrilem1 
 |-  ( ( G e. UHGraph /\ ( { a , b } e. ( Edg ` G ) /\ { a , c } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) ) -> ( { a , b } e. { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } /\ { a , c } e. { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } /\ { b , c } e. { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } ) )
132 128 131 syl 
 |-  ( ( ( ( ph /\ ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) /\ c e. ( Vtx ` G ) ) ) /\ ( ( g : { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } -1-1-onto-> { y e. ( Edg ` H ) | y C_ ( H ClNeighbVtx ( F ` a ) ) } /\ A. i e. { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } ( f " i ) = ( g ` i ) ) /\ f : ( G ClNeighbVtx a ) -1-1-onto-> ( H ClNeighbVtx ( F ` a ) ) /\ F : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) ) /\ ( T = { a , b , c } /\ ( # ` T ) = 3 /\ ( { a , b } e. ( Edg ` G ) /\ { a , c } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) ) ) /\ ( ( ( f ` a ) e. ( H ClNeighbVtx ( F ` a ) ) /\ ( f ` b ) e. ( H ClNeighbVtx ( F ` a ) ) /\ ( f ` c ) e. ( H ClNeighbVtx ( F ` a ) ) ) /\ ( f " T ) = { ( f ` a ) , ( f ` b ) , ( f ` c ) } /\ ( # ` ( f " T ) ) = 3 ) ) -> ( { a , b } e. { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } /\ { a , c } e. { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } /\ { b , c } e. { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } ) )
133 eqid 
 |-  ( H ClNeighbVtx ( F ` a ) ) = ( H ClNeighbVtx ( F ` a ) )
134 eqid 
 |-  { y e. ( Edg ` H ) | y C_ ( H ClNeighbVtx ( F ` a ) ) } = { y e. ( Edg ` H ) | y C_ ( H ClNeighbVtx ( F ` a ) ) }
135 5 129 6 130 133 13 134 grlimgrtrilem2 
 |-  ( ( ( f : ( G ClNeighbVtx a ) -1-1-onto-> ( H ClNeighbVtx ( F ` a ) ) /\ g : { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } -1-1-onto-> { y e. ( Edg ` H ) | y C_ ( H ClNeighbVtx ( F ` a ) ) } ) /\ A. i e. { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } ( f " i ) = ( g ` i ) /\ { a , b } e. { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } ) -> { ( f ` a ) , ( f ` b ) } e. ( Edg ` H ) )
136 135 3expia 
 |-  ( ( ( f : ( G ClNeighbVtx a ) -1-1-onto-> ( H ClNeighbVtx ( F ` a ) ) /\ g : { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } -1-1-onto-> { y e. ( Edg ` H ) | y C_ ( H ClNeighbVtx ( F ` a ) ) } ) /\ A. i e. { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } ( f " i ) = ( g ` i ) ) -> ( { a , b } e. { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } -> { ( f ` a ) , ( f ` b ) } e. ( Edg ` H ) ) )
137 5 129 6 130 133 13 134 grlimgrtrilem2 
 |-  ( ( ( f : ( G ClNeighbVtx a ) -1-1-onto-> ( H ClNeighbVtx ( F ` a ) ) /\ g : { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } -1-1-onto-> { y e. ( Edg ` H ) | y C_ ( H ClNeighbVtx ( F ` a ) ) } ) /\ A. i e. { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } ( f " i ) = ( g ` i ) /\ { a , c } e. { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } ) -> { ( f ` a ) , ( f ` c ) } e. ( Edg ` H ) )
138 137 3expia 
 |-  ( ( ( f : ( G ClNeighbVtx a ) -1-1-onto-> ( H ClNeighbVtx ( F ` a ) ) /\ g : { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } -1-1-onto-> { y e. ( Edg ` H ) | y C_ ( H ClNeighbVtx ( F ` a ) ) } ) /\ A. i e. { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } ( f " i ) = ( g ` i ) ) -> ( { a , c } e. { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } -> { ( f ` a ) , ( f ` c ) } e. ( Edg ` H ) ) )
139 5 129 6 130 133 13 134 grlimgrtrilem2 
 |-  ( ( ( f : ( G ClNeighbVtx a ) -1-1-onto-> ( H ClNeighbVtx ( F ` a ) ) /\ g : { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } -1-1-onto-> { y e. ( Edg ` H ) | y C_ ( H ClNeighbVtx ( F ` a ) ) } ) /\ A. i e. { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } ( f " i ) = ( g ` i ) /\ { b , c } e. { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } ) -> { ( f ` b ) , ( f ` c ) } e. ( Edg ` H ) )
140 139 3expia 
 |-  ( ( ( f : ( G ClNeighbVtx a ) -1-1-onto-> ( H ClNeighbVtx ( F ` a ) ) /\ g : { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } -1-1-onto-> { y e. ( Edg ` H ) | y C_ ( H ClNeighbVtx ( F ` a ) ) } ) /\ A. i e. { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } ( f " i ) = ( g ` i ) ) -> ( { b , c } e. { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } -> { ( f ` b ) , ( f ` c ) } e. ( Edg ` H ) ) )
141 136 138 140 3anim123d 
 |-  ( ( ( f : ( G ClNeighbVtx a ) -1-1-onto-> ( H ClNeighbVtx ( F ` a ) ) /\ g : { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } -1-1-onto-> { y e. ( Edg ` H ) | y C_ ( H ClNeighbVtx ( F ` a ) ) } ) /\ A. i e. { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } ( f " i ) = ( g ` i ) ) -> ( ( { a , b } e. { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } /\ { a , c } e. { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } /\ { b , c } e. { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } ) -> ( { ( f ` a ) , ( f ` b ) } e. ( Edg ` H ) /\ { ( f ` a ) , ( f ` c ) } e. ( Edg ` H ) /\ { ( f ` b ) , ( f ` c ) } e. ( Edg ` H ) ) ) )
142 141 anasss 
 |-  ( ( f : ( G ClNeighbVtx a ) -1-1-onto-> ( H ClNeighbVtx ( F ` a ) ) /\ ( g : { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } -1-1-onto-> { y e. ( Edg ` H ) | y C_ ( H ClNeighbVtx ( F ` a ) ) } /\ A. i e. { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } ( f " i ) = ( g ` i ) ) ) -> ( ( { a , b } e. { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } /\ { a , c } e. { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } /\ { b , c } e. { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } ) -> ( { ( f ` a ) , ( f ` b ) } e. ( Edg ` H ) /\ { ( f ` a ) , ( f ` c ) } e. ( Edg ` H ) /\ { ( f ` b ) , ( f ` c ) } e. ( Edg ` H ) ) ) )
143 142 ancoms 
 |-  ( ( ( g : { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } -1-1-onto-> { y e. ( Edg ` H ) | y C_ ( H ClNeighbVtx ( F ` a ) ) } /\ A. i e. { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } ( f " i ) = ( g ` i ) ) /\ f : ( G ClNeighbVtx a ) -1-1-onto-> ( H ClNeighbVtx ( F ` a ) ) ) -> ( ( { a , b } e. { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } /\ { a , c } e. { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } /\ { b , c } e. { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } ) -> ( { ( f ` a ) , ( f ` b ) } e. ( Edg ` H ) /\ { ( f ` a ) , ( f ` c ) } e. ( Edg ` H ) /\ { ( f ` b ) , ( f ` c ) } e. ( Edg ` H ) ) ) )
144 143 3adant3 
 |-  ( ( ( g : { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } -1-1-onto-> { y e. ( Edg ` H ) | y C_ ( H ClNeighbVtx ( F ` a ) ) } /\ A. i e. { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } ( f " i ) = ( g ` i ) ) /\ f : ( G ClNeighbVtx a ) -1-1-onto-> ( H ClNeighbVtx ( F ` a ) ) /\ F : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) ) -> ( ( { a , b } e. { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } /\ { a , c } e. { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } /\ { b , c } e. { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } ) -> ( { ( f ` a ) , ( f ` b ) } e. ( Edg ` H ) /\ { ( f ` a ) , ( f ` c ) } e. ( Edg ` H ) /\ { ( f ` b ) , ( f ` c ) } e. ( Edg ` H ) ) ) )
145 144 3ad2ant2 
 |-  ( ( ( ph /\ ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) /\ c e. ( Vtx ` G ) ) ) /\ ( ( g : { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } -1-1-onto-> { y e. ( Edg ` H ) | y C_ ( H ClNeighbVtx ( F ` a ) ) } /\ A. i e. { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } ( f " i ) = ( g ` i ) ) /\ f : ( G ClNeighbVtx a ) -1-1-onto-> ( H ClNeighbVtx ( F ` a ) ) /\ F : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) ) /\ ( T = { a , b , c } /\ ( # ` T ) = 3 /\ ( { a , b } e. ( Edg ` G ) /\ { a , c } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) ) ) -> ( ( { a , b } e. { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } /\ { a , c } e. { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } /\ { b , c } e. { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } ) -> ( { ( f ` a ) , ( f ` b ) } e. ( Edg ` H ) /\ { ( f ` a ) , ( f ` c ) } e. ( Edg ` H ) /\ { ( f ` b ) , ( f ` c ) } e. ( Edg ` H ) ) ) )
146 145 adantr 
 |-  ( ( ( ( ph /\ ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) /\ c e. ( Vtx ` G ) ) ) /\ ( ( g : { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } -1-1-onto-> { y e. ( Edg ` H ) | y C_ ( H ClNeighbVtx ( F ` a ) ) } /\ A. i e. { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } ( f " i ) = ( g ` i ) ) /\ f : ( G ClNeighbVtx a ) -1-1-onto-> ( H ClNeighbVtx ( F ` a ) ) /\ F : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) ) /\ ( T = { a , b , c } /\ ( # ` T ) = 3 /\ ( { a , b } e. ( Edg ` G ) /\ { a , c } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) ) ) /\ ( ( ( f ` a ) e. ( H ClNeighbVtx ( F ` a ) ) /\ ( f ` b ) e. ( H ClNeighbVtx ( F ` a ) ) /\ ( f ` c ) e. ( H ClNeighbVtx ( F ` a ) ) ) /\ ( f " T ) = { ( f ` a ) , ( f ` b ) , ( f ` c ) } /\ ( # ` ( f " T ) ) = 3 ) ) -> ( ( { a , b } e. { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } /\ { a , c } e. { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } /\ { b , c } e. { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } ) -> ( { ( f ` a ) , ( f ` b ) } e. ( Edg ` H ) /\ { ( f ` a ) , ( f ` c ) } e. ( Edg ` H ) /\ { ( f ` b ) , ( f ` c ) } e. ( Edg ` H ) ) ) )
147 132 146 mpd 
 |-  ( ( ( ( ph /\ ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) /\ c e. ( Vtx ` G ) ) ) /\ ( ( g : { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } -1-1-onto-> { y e. ( Edg ` H ) | y C_ ( H ClNeighbVtx ( F ` a ) ) } /\ A. i e. { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } ( f " i ) = ( g ` i ) ) /\ f : ( G ClNeighbVtx a ) -1-1-onto-> ( H ClNeighbVtx ( F ` a ) ) /\ F : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) ) /\ ( T = { a , b , c } /\ ( # ` T ) = 3 /\ ( { a , b } e. ( Edg ` G ) /\ { a , c } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) ) ) /\ ( ( ( f ` a ) e. ( H ClNeighbVtx ( F ` a ) ) /\ ( f ` b ) e. ( H ClNeighbVtx ( F ` a ) ) /\ ( f ` c ) e. ( H ClNeighbVtx ( F ` a ) ) ) /\ ( f " T ) = { ( f ` a ) , ( f ` b ) , ( f ` c ) } /\ ( # ` ( f " T ) ) = 3 ) ) -> ( { ( f ` a ) , ( f ` b ) } e. ( Edg ` H ) /\ { ( f ` a ) , ( f ` c ) } e. ( Edg ` H ) /\ { ( f ` b ) , ( f ` c ) } e. ( Edg ` H ) ) )
148 115 121 147 3jca 
 |-  ( ( ( ( ph /\ ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) /\ c e. ( Vtx ` G ) ) ) /\ ( ( g : { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } -1-1-onto-> { y e. ( Edg ` H ) | y C_ ( H ClNeighbVtx ( F ` a ) ) } /\ A. i e. { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } ( f " i ) = ( g ` i ) ) /\ f : ( G ClNeighbVtx a ) -1-1-onto-> ( H ClNeighbVtx ( F ` a ) ) /\ F : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) ) /\ ( T = { a , b , c } /\ ( # ` T ) = 3 /\ ( { a , b } e. ( Edg ` G ) /\ { a , c } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) ) ) /\ ( ( ( f ` a ) e. ( H ClNeighbVtx ( F ` a ) ) /\ ( f ` b ) e. ( H ClNeighbVtx ( F ` a ) ) /\ ( f ` c ) e. ( H ClNeighbVtx ( F ` a ) ) ) /\ ( f " T ) = { ( f ` a ) , ( f ` b ) , ( f ` c ) } /\ ( # ` ( f " T ) ) = 3 ) ) -> ( { ( f ` a ) , ( f ` b ) , ( f ` c ) } = { ( f ` a ) , ( f ` b ) , ( f ` c ) } /\ ( # ` { ( f ` a ) , ( f ` b ) , ( f ` c ) } ) = 3 /\ ( { ( f ` a ) , ( f ` b ) } e. ( Edg ` H ) /\ { ( f ` a ) , ( f ` c ) } e. ( Edg ` H ) /\ { ( f ` b ) , ( f ` c ) } e. ( Edg ` H ) ) ) )
149 86 94 102 106 110 114 148 3rspcedvdw 
 |-  ( ( ( ( ph /\ ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) /\ c e. ( Vtx ` G ) ) ) /\ ( ( g : { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } -1-1-onto-> { y e. ( Edg ` H ) | y C_ ( H ClNeighbVtx ( F ` a ) ) } /\ A. i e. { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } ( f " i ) = ( g ` i ) ) /\ f : ( G ClNeighbVtx a ) -1-1-onto-> ( H ClNeighbVtx ( F ` a ) ) /\ F : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) ) /\ ( T = { a , b , c } /\ ( # ` T ) = 3 /\ ( { a , b } e. ( Edg ` G ) /\ { a , c } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) ) ) /\ ( ( ( f ` a ) e. ( H ClNeighbVtx ( F ` a ) ) /\ ( f ` b ) e. ( H ClNeighbVtx ( F ` a ) ) /\ ( f ` c ) e. ( H ClNeighbVtx ( F ` a ) ) ) /\ ( f " T ) = { ( f ` a ) , ( f ` b ) , ( f ` c ) } /\ ( # ` ( f " T ) ) = 3 ) ) -> E. x e. ( Vtx ` H ) E. y e. ( Vtx ` H ) E. z e. ( Vtx ` H ) ( { ( f ` a ) , ( f ` b ) , ( f ` c ) } = { x , y , z } /\ ( # ` { ( f ` a ) , ( f ` b ) , ( f ` c ) } ) = 3 /\ ( { x , y } e. ( Edg ` H ) /\ { x , z } e. ( Edg ` H ) /\ { y , z } e. ( Edg ` H ) ) ) )
150 78 149 mpdan 
 |-  ( ( ( ph /\ ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) /\ c e. ( Vtx ` G ) ) ) /\ ( ( g : { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } -1-1-onto-> { y e. ( Edg ` H ) | y C_ ( H ClNeighbVtx ( F ` a ) ) } /\ A. i e. { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } ( f " i ) = ( g ` i ) ) /\ f : ( G ClNeighbVtx a ) -1-1-onto-> ( H ClNeighbVtx ( F ` a ) ) /\ F : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) ) /\ ( T = { a , b , c } /\ ( # ` T ) = 3 /\ ( { a , b } e. ( Edg ` G ) /\ { a , c } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) ) ) -> E. x e. ( Vtx ` H ) E. y e. ( Vtx ` H ) E. z e. ( Vtx ` H ) ( { ( f ` a ) , ( f ` b ) , ( f ` c ) } = { x , y , z } /\ ( # ` { ( f ` a ) , ( f ` b ) , ( f ` c ) } ) = 3 /\ ( { x , y } e. ( Edg ` H ) /\ { x , z } e. ( Edg ` H ) /\ { y , z } e. ( Edg ` H ) ) ) )
151 eqeq1 
 |-  ( t = { ( f ` a ) , ( f ` b ) , ( f ` c ) } -> ( t = { x , y , z } <-> { ( f ` a ) , ( f ` b ) , ( f ` c ) } = { x , y , z } ) )
152 fveqeq2 
 |-  ( t = { ( f ` a ) , ( f ` b ) , ( f ` c ) } -> ( ( # ` t ) = 3 <-> ( # ` { ( f ` a ) , ( f ` b ) , ( f ` c ) } ) = 3 ) )
153 151 152 3anbi12d 
 |-  ( t = { ( f ` a ) , ( f ` b ) , ( f ` c ) } -> ( ( t = { x , y , z } /\ ( # ` t ) = 3 /\ ( { x , y } e. ( Edg ` H ) /\ { x , z } e. ( Edg ` H ) /\ { y , z } e. ( Edg ` H ) ) ) <-> ( { ( f ` a ) , ( f ` b ) , ( f ` c ) } = { x , y , z } /\ ( # ` { ( f ` a ) , ( f ` b ) , ( f ` c ) } ) = 3 /\ ( { x , y } e. ( Edg ` H ) /\ { x , z } e. ( Edg ` H ) /\ { y , z } e. ( Edg ` H ) ) ) ) )
154 153 rexbidv 
 |-  ( t = { ( f ` a ) , ( f ` b ) , ( f ` c ) } -> ( E. z e. ( Vtx ` H ) ( t = { x , y , z } /\ ( # ` t ) = 3 /\ ( { x , y } e. ( Edg ` H ) /\ { x , z } e. ( Edg ` H ) /\ { y , z } e. ( Edg ` H ) ) ) <-> E. z e. ( Vtx ` H ) ( { ( f ` a ) , ( f ` b ) , ( f ` c ) } = { x , y , z } /\ ( # ` { ( f ` a ) , ( f ` b ) , ( f ` c ) } ) = 3 /\ ( { x , y } e. ( Edg ` H ) /\ { x , z } e. ( Edg ` H ) /\ { y , z } e. ( Edg ` H ) ) ) ) )
155 154 2rexbidv 
 |-  ( t = { ( f ` a ) , ( f ` b ) , ( f ` c ) } -> ( E. x e. ( Vtx ` H ) E. y e. ( Vtx ` H ) E. z e. ( Vtx ` H ) ( t = { x , y , z } /\ ( # ` t ) = 3 /\ ( { x , y } e. ( Edg ` H ) /\ { x , z } e. ( Edg ` H ) /\ { y , z } e. ( Edg ` H ) ) ) <-> E. x e. ( Vtx ` H ) E. y e. ( Vtx ` H ) E. z e. ( Vtx ` H ) ( { ( f ` a ) , ( f ` b ) , ( f ` c ) } = { x , y , z } /\ ( # ` { ( f ` a ) , ( f ` b ) , ( f ` c ) } ) = 3 /\ ( { x , y } e. ( Edg ` H ) /\ { x , z } e. ( Edg ` H ) /\ { y , z } e. ( Edg ` H ) ) ) ) )
156 39 150 155 spcedv 
 |-  ( ( ( ph /\ ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) /\ c e. ( Vtx ` G ) ) ) /\ ( ( g : { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } -1-1-onto-> { y e. ( Edg ` H ) | y C_ ( H ClNeighbVtx ( F ` a ) ) } /\ A. i e. { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } ( f " i ) = ( g ` i ) ) /\ f : ( G ClNeighbVtx a ) -1-1-onto-> ( H ClNeighbVtx ( F ` a ) ) /\ F : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) ) /\ ( T = { a , b , c } /\ ( # ` T ) = 3 /\ ( { a , b } e. ( Edg ` G ) /\ { a , c } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) ) ) -> E. t E. x e. ( Vtx ` H ) E. y e. ( Vtx ` H ) E. z e. ( Vtx ` H ) ( t = { x , y , z } /\ ( # ` t ) = 3 /\ ( { x , y } e. ( Edg ` H ) /\ { x , z } e. ( Edg ` H ) /\ { y , z } e. ( Edg ` H ) ) ) )
157 156 3exp 
 |-  ( ( ph /\ ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) /\ c e. ( Vtx ` G ) ) ) -> ( ( ( g : { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } -1-1-onto-> { y e. ( Edg ` H ) | y C_ ( H ClNeighbVtx ( F ` a ) ) } /\ A. i e. { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } ( f " i ) = ( g ` i ) ) /\ f : ( G ClNeighbVtx a ) -1-1-onto-> ( H ClNeighbVtx ( F ` a ) ) /\ F : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) ) -> ( ( T = { a , b , c } /\ ( # ` T ) = 3 /\ ( { a , b } e. ( Edg ` G ) /\ { a , c } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) ) -> E. t E. x e. ( Vtx ` H ) E. y e. ( Vtx ` H ) E. z e. ( Vtx ` H ) ( t = { x , y , z } /\ ( # ` t ) = 3 /\ ( { x , y } e. ( Edg ` H ) /\ { x , z } e. ( Edg ` H ) /\ { y , z } e. ( Edg ` H ) ) ) ) ) )
158 157 3expd 
 |-  ( ( ph /\ ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) /\ c e. ( Vtx ` G ) ) ) -> ( ( g : { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } -1-1-onto-> { y e. ( Edg ` H ) | y C_ ( H ClNeighbVtx ( F ` a ) ) } /\ A. i e. { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } ( f " i ) = ( g ` i ) ) -> ( f : ( G ClNeighbVtx a ) -1-1-onto-> ( H ClNeighbVtx ( F ` a ) ) -> ( F : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) -> ( ( T = { a , b , c } /\ ( # ` T ) = 3 /\ ( { a , b } e. ( Edg ` G ) /\ { a , c } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) ) -> E. t E. x e. ( Vtx ` H ) E. y e. ( Vtx ` H ) E. z e. ( Vtx ` H ) ( t = { x , y , z } /\ ( # ` t ) = 3 /\ ( { x , y } e. ( Edg ` H ) /\ { x , z } e. ( Edg ` H ) /\ { y , z } e. ( Edg ` H ) ) ) ) ) ) ) )
159 158 exlimdv 
 |-  ( ( ph /\ ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) /\ c e. ( Vtx ` G ) ) ) -> ( E. g ( g : { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } -1-1-onto-> { y e. ( Edg ` H ) | y C_ ( H ClNeighbVtx ( F ` a ) ) } /\ A. i e. { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } ( f " i ) = ( g ` i ) ) -> ( f : ( G ClNeighbVtx a ) -1-1-onto-> ( H ClNeighbVtx ( F ` a ) ) -> ( F : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) -> ( ( T = { a , b , c } /\ ( # ` T ) = 3 /\ ( { a , b } e. ( Edg ` G ) /\ { a , c } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) ) -> E. t E. x e. ( Vtx ` H ) E. y e. ( Vtx ` H ) E. z e. ( Vtx ` H ) ( t = { x , y , z } /\ ( # ` t ) = 3 /\ ( { x , y } e. ( Edg ` H ) /\ { x , z } e. ( Edg ` H ) /\ { y , z } e. ( Edg ` H ) ) ) ) ) ) ) )
160 159 impcomd 
 |-  ( ( ph /\ ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) /\ c e. ( Vtx ` G ) ) ) -> ( ( f : ( G ClNeighbVtx a ) -1-1-onto-> ( H ClNeighbVtx ( F ` a ) ) /\ E. g ( g : { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } -1-1-onto-> { y e. ( Edg ` H ) | y C_ ( H ClNeighbVtx ( F ` a ) ) } /\ A. i e. { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } ( f " i ) = ( g ` i ) ) ) -> ( F : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) -> ( ( T = { a , b , c } /\ ( # ` T ) = 3 /\ ( { a , b } e. ( Edg ` G ) /\ { a , c } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) ) -> E. t E. x e. ( Vtx ` H ) E. y e. ( Vtx ` H ) E. z e. ( Vtx ` H ) ( t = { x , y , z } /\ ( # ` t ) = 3 /\ ( { x , y } e. ( Edg ` H ) /\ { x , z } e. ( Edg ` H ) /\ { y , z } e. ( Edg ` H ) ) ) ) ) ) )
161 160 exlimdv 
 |-  ( ( ph /\ ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) /\ c e. ( Vtx ` G ) ) ) -> ( E. f ( f : ( G ClNeighbVtx a ) -1-1-onto-> ( H ClNeighbVtx ( F ` a ) ) /\ E. g ( g : { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } -1-1-onto-> { y e. ( Edg ` H ) | y C_ ( H ClNeighbVtx ( F ` a ) ) } /\ A. i e. { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx a ) } ( f " i ) = ( g ` i ) ) ) -> ( F : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) -> ( ( T = { a , b , c } /\ ( # ` T ) = 3 /\ ( { a , b } e. ( Edg ` G ) /\ { a , c } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) ) -> E. t E. x e. ( Vtx ` H ) E. y e. ( Vtx ` H ) E. z e. ( Vtx ` H ) ( t = { x , y , z } /\ ( # ` t ) = 3 /\ ( { x , y } e. ( Edg ` H ) /\ { x , z } e. ( Edg ` H ) /\ { y , z } e. ( Edg ` H ) ) ) ) ) ) )
162 37 161 syld 
 |-  ( ( ph /\ ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) /\ c e. ( Vtx ` G ) ) ) -> ( A. v e. ( Vtx ` G ) E. f ( f : ( G ClNeighbVtx v ) -1-1-onto-> ( H ClNeighbVtx ( F ` v ) ) /\ E. g ( g : { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx v ) } -1-1-onto-> { y e. ( Edg ` H ) | y C_ ( H ClNeighbVtx ( F ` v ) ) } /\ A. i e. { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx v ) } ( f " i ) = ( g ` i ) ) ) -> ( F : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) -> ( ( T = { a , b , c } /\ ( # ` T ) = 3 /\ ( { a , b } e. ( Edg ` G ) /\ { a , c } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) ) -> E. t E. x e. ( Vtx ` H ) E. y e. ( Vtx ` H ) E. z e. ( Vtx ` H ) ( t = { x , y , z } /\ ( # ` t ) = 3 /\ ( { x , y } e. ( Edg ` H ) /\ { x , z } e. ( Edg ` H ) /\ { y , z } e. ( Edg ` H ) ) ) ) ) ) )
163 162 com13 
 |-  ( F : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) -> ( A. v e. ( Vtx ` G ) E. f ( f : ( G ClNeighbVtx v ) -1-1-onto-> ( H ClNeighbVtx ( F ` v ) ) /\ E. g ( g : { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx v ) } -1-1-onto-> { y e. ( Edg ` H ) | y C_ ( H ClNeighbVtx ( F ` v ) ) } /\ A. i e. { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx v ) } ( f " i ) = ( g ` i ) ) ) -> ( ( ph /\ ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) /\ c e. ( Vtx ` G ) ) ) -> ( ( T = { a , b , c } /\ ( # ` T ) = 3 /\ ( { a , b } e. ( Edg ` G ) /\ { a , c } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) ) -> E. t E. x e. ( Vtx ` H ) E. y e. ( Vtx ` H ) E. z e. ( Vtx ` H ) ( t = { x , y , z } /\ ( # ` t ) = 3 /\ ( { x , y } e. ( Edg ` H ) /\ { x , z } e. ( Edg ` H ) /\ { y , z } e. ( Edg ` H ) ) ) ) ) ) )
164 163 imp 
 |-  ( ( F : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) /\ A. v e. ( Vtx ` G ) E. f ( f : ( G ClNeighbVtx v ) -1-1-onto-> ( H ClNeighbVtx ( F ` v ) ) /\ E. g ( g : { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx v ) } -1-1-onto-> { y e. ( Edg ` H ) | y C_ ( H ClNeighbVtx ( F ` v ) ) } /\ A. i e. { y e. ( Edg ` G ) | y C_ ( G ClNeighbVtx v ) } ( f " i ) = ( g ` i ) ) ) ) -> ( ( ph /\ ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) /\ c e. ( Vtx ` G ) ) ) -> ( ( T = { a , b , c } /\ ( # ` T ) = 3 /\ ( { a , b } e. ( Edg ` G ) /\ { a , c } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) ) -> E. t E. x e. ( Vtx ` H ) E. y e. ( Vtx ` H ) E. z e. ( Vtx ` H ) ( t = { x , y , z } /\ ( # ` t ) = 3 /\ ( { x , y } e. ( Edg ` H ) /\ { x , z } e. ( Edg ` H ) /\ { y , z } e. ( Edg ` H ) ) ) ) ) )
165 9 18 164 3syl 
 |-  ( ph -> ( ( ph /\ ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) /\ c e. ( Vtx ` G ) ) ) -> ( ( T = { a , b , c } /\ ( # ` T ) = 3 /\ ( { a , b } e. ( Edg ` G ) /\ { a , c } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) ) -> E. t E. x e. ( Vtx ` H ) E. y e. ( Vtx ` H ) E. z e. ( Vtx ` H ) ( t = { x , y , z } /\ ( # ` t ) = 3 /\ ( { x , y } e. ( Edg ` H ) /\ { x , z } e. ( Edg ` H ) /\ { y , z } e. ( Edg ` H ) ) ) ) ) )
166 165 anabsi5 
 |-  ( ( ph /\ ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) /\ c e. ( Vtx ` G ) ) ) -> ( ( T = { a , b , c } /\ ( # ` T ) = 3 /\ ( { a , b } e. ( Edg ` G ) /\ { a , c } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) ) -> E. t E. x e. ( Vtx ` H ) E. y e. ( Vtx ` H ) E. z e. ( Vtx ` H ) ( t = { x , y , z } /\ ( # ` t ) = 3 /\ ( { x , y } e. ( Edg ` H ) /\ { x , z } e. ( Edg ` H ) /\ { y , z } e. ( Edg ` H ) ) ) ) )
167 166 rexlimdvvva 
 |-  ( ph -> ( E. a e. ( Vtx ` G ) E. b e. ( Vtx ` G ) E. c e. ( Vtx ` G ) ( T = { a , b , c } /\ ( # ` T ) = 3 /\ ( { a , b } e. ( Edg ` G ) /\ { a , c } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) ) -> E. t E. x e. ( Vtx ` H ) E. y e. ( Vtx ` H ) E. z e. ( Vtx ` H ) ( t = { x , y , z } /\ ( # ` t ) = 3 /\ ( { x , y } e. ( Edg ` H ) /\ { x , z } e. ( Edg ` H ) /\ { y , z } e. ( Edg ` H ) ) ) ) )
168 8 167 mpd 
 |-  ( ph -> E. t E. x e. ( Vtx ` H ) E. y e. ( Vtx ` H ) E. z e. ( Vtx ` H ) ( t = { x , y , z } /\ ( # ` t ) = 3 /\ ( { x , y } e. ( Edg ` H ) /\ { x , z } e. ( Edg ` H ) /\ { y , z } e. ( Edg ` H ) ) ) )
169 10 13 isgrtri 
 |-  ( t e. ( GrTriangles ` H ) <-> E. x e. ( Vtx ` H ) E. y e. ( Vtx ` H ) E. z e. ( Vtx ` H ) ( t = { x , y , z } /\ ( # ` t ) = 3 /\ ( { x , y } e. ( Edg ` H ) /\ { x , z } e. ( Edg ` H ) /\ { y , z } e. ( Edg ` H ) ) ) )
170 169 exbii 
 |-  ( E. t t e. ( GrTriangles ` H ) <-> E. t E. x e. ( Vtx ` H ) E. y e. ( Vtx ` H ) E. z e. ( Vtx ` H ) ( t = { x , y , z } /\ ( # ` t ) = 3 /\ ( { x , y } e. ( Edg ` H ) /\ { x , z } e. ( Edg ` H ) /\ { y , z } e. ( Edg ` H ) ) ) )
171 168 170 sylibr 
 |-  ( ph -> E. t t e. ( GrTriangles ` H ) )