Metamath Proof Explorer

Theorem grimgrtri

Description: Graph isomorphisms map triangles onto triangles. (Contributed by AV, 27-Jul-2025) (Proof shortened by AV, 24-Aug-2025)

Ref Expression
Hypotheses grimgrtri.g 
|- ( ph -> G e. UHGraph )
grimgrtri.h 
|- ( ph -> H e. UHGraph )
grimgrtri.n 
|- ( ph -> F e. ( G GraphIso H ) )
grimgrtri.t 
|- ( ph -> T e. ( GrTriangles ` G ) )
Assertion grimgrtri 
|- ( ph -> ( F " T ) e. ( GrTriangles ` H ) )

Proof

Step Hyp Ref Expression
1 grimgrtri.g 
 |-  ( ph -> G e. UHGraph )
2 grimgrtri.h 
 |-  ( ph -> H e. UHGraph )
3 grimgrtri.n 
 |-  ( ph -> F e. ( G GraphIso H ) )
4 grimgrtri.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 eqid 
 |-  ( Vtx ` H ) = ( Vtx ` H )
10 5 9 grimf1o 
 |-  ( F e. ( G GraphIso H ) -> F : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) )
11 f1of1 
 |-  ( F : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) -> F : ( Vtx ` G ) -1-1-> ( Vtx ` H ) )
12 3 10 11 3syl 
 |-  ( ph -> F : ( Vtx ` G ) -1-1-> ( Vtx ` H ) )
13 12 ad3antrrr 
 |-  ( ( ( ( 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 ) ) ) ) -> F : ( Vtx ` G ) -1-1-> ( Vtx ` H ) )
14 simplrl 
 |-  ( ( ( ph /\ ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) ) /\ c e. ( Vtx ` G ) ) -> a e. ( Vtx ` G ) )
15 14 adantr 
 |-  ( ( ( ( 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 ) ) ) ) -> a e. ( Vtx ` G ) )
16 simprr 
 |-  ( ( ph /\ ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) ) -> b e. ( Vtx ` G ) )
17 16 adantr 
 |-  ( ( ( ph /\ ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) ) /\ c e. ( Vtx ` G ) ) -> b e. ( Vtx ` G ) )
18 17 adantr 
 |-  ( ( ( ( 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 ) ) ) ) -> b e. ( Vtx ` G ) )
19 simplr 
 |-  ( ( ( ( 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 ) ) ) ) -> c e. ( Vtx ` G ) )
20 15 18 19 3jca 
 |-  ( ( ( ( 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 ) ) ) ) -> ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) /\ c e. ( Vtx ` G ) ) )
21 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 ) )
22 21 adantl 
 |-  ( ( ( ( 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 ) ) ) ) -> ( T = { a , b , c } /\ ( # ` T ) = 3 ) )
23 grtrimap 
 |-  ( F : ( Vtx ` G ) -1-1-> ( Vtx ` H ) -> ( ( ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) /\ c e. ( Vtx ` G ) ) /\ ( T = { a , b , c } /\ ( # ` T ) = 3 ) ) -> ( ( ( F ` a ) e. ( Vtx ` H ) /\ ( F ` b ) e. ( Vtx ` H ) /\ ( F ` c ) e. ( Vtx ` H ) ) /\ ( F " T ) = { ( F ` a ) , ( F ` b ) , ( F ` c ) } /\ ( # ` ( F " T ) ) = 3 ) ) )
24 23 imp 
 |-  ( ( F : ( Vtx ` G ) -1-1-> ( Vtx ` H ) /\ ( ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) /\ c e. ( Vtx ` G ) ) /\ ( T = { a , b , c } /\ ( # ` T ) = 3 ) ) ) -> ( ( ( F ` a ) e. ( Vtx ` H ) /\ ( F ` b ) e. ( Vtx ` H ) /\ ( F ` c ) e. ( Vtx ` H ) ) /\ ( F " T ) = { ( F ` a ) , ( F ` b ) , ( F ` c ) } /\ ( # ` ( F " T ) ) = 3 ) )
25 13 20 22 24 syl12anc 
 |-  ( ( ( ( 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 ) ) ) ) -> ( ( ( F ` a ) e. ( Vtx ` H ) /\ ( F ` b ) e. ( Vtx ` H ) /\ ( F ` c ) e. ( Vtx ` H ) ) /\ ( F " T ) = { ( F ` a ) , ( F ` b ) , ( F ` c ) } /\ ( # ` ( F " T ) ) = 3 ) )
26 eqid 
 |-  ( Edg ` H ) = ( Edg ` H )
27 5 6 26 grimedg 
 |-  ( ( G e. UHGraph /\ H e. UHGraph /\ F e. ( G GraphIso H ) ) -> ( { a , b } e. ( Edg ` G ) <-> ( ( F " { a , b } ) e. ( Edg ` H ) /\ { a , b } C_ ( Vtx ` G ) ) ) )
28 5 6 26 grimedg 
 |-  ( ( G e. UHGraph /\ H e. UHGraph /\ F e. ( G GraphIso H ) ) -> ( { a , c } e. ( Edg ` G ) <-> ( ( F " { a , c } ) e. ( Edg ` H ) /\ { a , c } C_ ( Vtx ` G ) ) ) )
29 5 6 26 grimedg 
 |-  ( ( G e. UHGraph /\ H e. UHGraph /\ F e. ( G GraphIso H ) ) -> ( { b , c } e. ( Edg ` G ) <-> ( ( F " { b , c } ) e. ( Edg ` H ) /\ { b , c } C_ ( Vtx ` G ) ) ) )
30 27 28 29 3anbi123d 
 |-  ( ( G e. UHGraph /\ H e. UHGraph /\ F e. ( G GraphIso H ) ) -> ( ( { a , b } e. ( Edg ` G ) /\ { a , c } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) <-> ( ( ( F " { a , b } ) e. ( Edg ` H ) /\ { a , b } C_ ( Vtx ` G ) ) /\ ( ( F " { a , c } ) e. ( Edg ` H ) /\ { a , c } C_ ( Vtx ` G ) ) /\ ( ( F " { b , c } ) e. ( Edg ` H ) /\ { b , c } C_ ( Vtx ` G ) ) ) ) )
31 f1ofn 
 |-  ( F : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) -> F Fn ( Vtx ` G ) )
32 simpl 
 |-  ( ( F Fn ( Vtx ` G ) /\ ( ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) /\ c e. ( Vtx ` G ) ) ) -> F Fn ( Vtx ` G ) )
33 simprll 
 |-  ( ( F Fn ( Vtx ` G ) /\ ( ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) /\ c e. ( Vtx ` G ) ) ) -> a e. ( Vtx ` G ) )
34 simprlr 
 |-  ( ( F Fn ( Vtx ` G ) /\ ( ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) /\ c e. ( Vtx ` G ) ) ) -> b e. ( Vtx ` G ) )
35 fnimapr 
 |-  ( ( F Fn ( Vtx ` G ) /\ a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) -> ( F " { a , b } ) = { ( F ` a ) , ( F ` b ) } )
36 32 33 34 35 syl3anc 
 |-  ( ( F Fn ( Vtx ` G ) /\ ( ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) /\ c e. ( Vtx ` G ) ) ) -> ( F " { a , b } ) = { ( F ` a ) , ( F ` b ) } )
37 36 eleq1d 
 |-  ( ( F Fn ( Vtx ` G ) /\ ( ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) /\ c e. ( Vtx ` G ) ) ) -> ( ( F " { a , b } ) e. ( Edg ` H ) <-> { ( F ` a ) , ( F ` b ) } e. ( Edg ` H ) ) )
38 37 biimpd 
 |-  ( ( F Fn ( Vtx ` G ) /\ ( ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) /\ c e. ( Vtx ` G ) ) ) -> ( ( F " { a , b } ) e. ( Edg ` H ) -> { ( F ` a ) , ( F ` b ) } e. ( Edg ` H ) ) )
39 38 adantrd 
 |-  ( ( F Fn ( Vtx ` G ) /\ ( ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) /\ c e. ( Vtx ` G ) ) ) -> ( ( ( F " { a , b } ) e. ( Edg ` H ) /\ { a , b } C_ ( Vtx ` G ) ) -> { ( F ` a ) , ( F ` b ) } e. ( Edg ` H ) ) )
40 simprr 
 |-  ( ( F Fn ( Vtx ` G ) /\ ( ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) /\ c e. ( Vtx ` G ) ) ) -> c e. ( Vtx ` G ) )
41 fnimapr 
 |-  ( ( F Fn ( Vtx ` G ) /\ a e. ( Vtx ` G ) /\ c e. ( Vtx ` G ) ) -> ( F " { a , c } ) = { ( F ` a ) , ( F ` c ) } )
42 32 33 40 41 syl3anc 
 |-  ( ( F Fn ( Vtx ` G ) /\ ( ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) /\ c e. ( Vtx ` G ) ) ) -> ( F " { a , c } ) = { ( F ` a ) , ( F ` c ) } )
43 42 eleq1d 
 |-  ( ( F Fn ( Vtx ` G ) /\ ( ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) /\ c e. ( Vtx ` G ) ) ) -> ( ( F " { a , c } ) e. ( Edg ` H ) <-> { ( F ` a ) , ( F ` c ) } e. ( Edg ` H ) ) )
44 43 biimpd 
 |-  ( ( F Fn ( Vtx ` G ) /\ ( ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) /\ c e. ( Vtx ` G ) ) ) -> ( ( F " { a , c } ) e. ( Edg ` H ) -> { ( F ` a ) , ( F ` c ) } e. ( Edg ` H ) ) )
45 44 adantrd 
 |-  ( ( F Fn ( Vtx ` G ) /\ ( ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) /\ c e. ( Vtx ` G ) ) ) -> ( ( ( F " { a , c } ) e. ( Edg ` H ) /\ { a , c } C_ ( Vtx ` G ) ) -> { ( F ` a ) , ( F ` c ) } e. ( Edg ` H ) ) )
46 fnimapr 
 |-  ( ( F Fn ( Vtx ` G ) /\ b e. ( Vtx ` G ) /\ c e. ( Vtx ` G ) ) -> ( F " { b , c } ) = { ( F ` b ) , ( F ` c ) } )
47 32 34 40 46 syl3anc 
 |-  ( ( F Fn ( Vtx ` G ) /\ ( ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) /\ c e. ( Vtx ` G ) ) ) -> ( F " { b , c } ) = { ( F ` b ) , ( F ` c ) } )
48 47 eleq1d 
 |-  ( ( F Fn ( Vtx ` G ) /\ ( ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) /\ c e. ( Vtx ` G ) ) ) -> ( ( F " { b , c } ) e. ( Edg ` H ) <-> { ( F ` b ) , ( F ` c ) } e. ( Edg ` H ) ) )
49 48 biimpd 
 |-  ( ( F Fn ( Vtx ` G ) /\ ( ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) /\ c e. ( Vtx ` G ) ) ) -> ( ( F " { b , c } ) e. ( Edg ` H ) -> { ( F ` b ) , ( F ` c ) } e. ( Edg ` H ) ) )
50 49 adantrd 
 |-  ( ( F Fn ( Vtx ` G ) /\ ( ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) /\ c e. ( Vtx ` G ) ) ) -> ( ( ( F " { b , c } ) e. ( Edg ` H ) /\ { b , c } C_ ( Vtx ` G ) ) -> { ( F ` b ) , ( F ` c ) } e. ( Edg ` H ) ) )
51 39 45 50 3anim123d 
 |-  ( ( F Fn ( Vtx ` G ) /\ ( ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) /\ c e. ( Vtx ` G ) ) ) -> ( ( ( ( F " { a , b } ) e. ( Edg ` H ) /\ { a , b } C_ ( Vtx ` G ) ) /\ ( ( F " { a , c } ) e. ( Edg ` H ) /\ { a , c } C_ ( Vtx ` G ) ) /\ ( ( F " { b , c } ) e. ( Edg ` H ) /\ { b , c } C_ ( Vtx ` G ) ) ) -> ( { ( F ` a ) , ( F ` b ) } e. ( Edg ` H ) /\ { ( F ` a ) , ( F ` c ) } e. ( Edg ` H ) /\ { ( F ` b ) , ( F ` c ) } e. ( Edg ` H ) ) ) )
52 51 ex 
 |-  ( F Fn ( Vtx ` G ) -> ( ( ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) /\ c e. ( Vtx ` G ) ) -> ( ( ( ( F " { a , b } ) e. ( Edg ` H ) /\ { a , b } C_ ( Vtx ` G ) ) /\ ( ( F " { a , c } ) e. ( Edg ` H ) /\ { a , c } C_ ( Vtx ` G ) ) /\ ( ( F " { b , c } ) e. ( Edg ` H ) /\ { b , c } C_ ( Vtx ` G ) ) ) -> ( { ( F ` a ) , ( F ` b ) } e. ( Edg ` H ) /\ { ( F ` a ) , ( F ` c ) } e. ( Edg ` H ) /\ { ( F ` b ) , ( F ` c ) } e. ( Edg ` H ) ) ) ) )
53 52 com23 
 |-  ( F Fn ( Vtx ` G ) -> ( ( ( ( F " { a , b } ) e. ( Edg ` H ) /\ { a , b } C_ ( Vtx ` G ) ) /\ ( ( F " { a , c } ) e. ( Edg ` H ) /\ { a , c } C_ ( Vtx ` G ) ) /\ ( ( F " { b , c } ) e. ( Edg ` H ) /\ { b , c } C_ ( Vtx ` G ) ) ) -> ( ( ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) /\ c e. ( Vtx ` G ) ) -> ( { ( F ` a ) , ( F ` b ) } e. ( Edg ` H ) /\ { ( F ` a ) , ( F ` c ) } e. ( Edg ` H ) /\ { ( F ` b ) , ( F ` c ) } e. ( Edg ` H ) ) ) ) )
54 10 31 53 3syl 
 |-  ( F e. ( G GraphIso H ) -> ( ( ( ( F " { a , b } ) e. ( Edg ` H ) /\ { a , b } C_ ( Vtx ` G ) ) /\ ( ( F " { a , c } ) e. ( Edg ` H ) /\ { a , c } C_ ( Vtx ` G ) ) /\ ( ( F " { b , c } ) e. ( Edg ` H ) /\ { b , c } C_ ( Vtx ` G ) ) ) -> ( ( ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) /\ c e. ( Vtx ` G ) ) -> ( { ( F ` a ) , ( F ` b ) } e. ( Edg ` H ) /\ { ( F ` a ) , ( F ` c ) } e. ( Edg ` H ) /\ { ( F ` b ) , ( F ` c ) } e. ( Edg ` H ) ) ) ) )
55 54 3ad2ant3 
 |-  ( ( G e. UHGraph /\ H e. UHGraph /\ F e. ( G GraphIso H ) ) -> ( ( ( ( F " { a , b } ) e. ( Edg ` H ) /\ { a , b } C_ ( Vtx ` G ) ) /\ ( ( F " { a , c } ) e. ( Edg ` H ) /\ { a , c } C_ ( Vtx ` G ) ) /\ ( ( F " { b , c } ) e. ( Edg ` H ) /\ { b , c } C_ ( Vtx ` G ) ) ) -> ( ( ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) /\ c e. ( Vtx ` G ) ) -> ( { ( F ` a ) , ( F ` b ) } e. ( Edg ` H ) /\ { ( F ` a ) , ( F ` c ) } e. ( Edg ` H ) /\ { ( F ` b ) , ( F ` c ) } e. ( Edg ` H ) ) ) ) )
56 30 55 sylbid 
 |-  ( ( G e. UHGraph /\ H e. UHGraph /\ F e. ( G GraphIso H ) ) -> ( ( { a , b } e. ( Edg ` G ) /\ { a , c } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) -> ( ( ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) /\ c e. ( Vtx ` G ) ) -> ( { ( F ` a ) , ( F ` b ) } e. ( Edg ` H ) /\ { ( F ` a ) , ( F ` c ) } e. ( Edg ` H ) /\ { ( F ` b ) , ( F ` c ) } e. ( Edg ` H ) ) ) ) )
57 56 2a1d 
 |-  ( ( G e. UHGraph /\ H e. UHGraph /\ F e. ( G GraphIso H ) ) -> ( T = { a , b , c } -> ( ( # ` T ) = 3 -> ( ( { a , b } e. ( Edg ` G ) /\ { a , c } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) -> ( ( ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) /\ c e. ( Vtx ` G ) ) -> ( { ( F ` a ) , ( F ` b ) } e. ( Edg ` H ) /\ { ( F ` a ) , ( F ` c ) } e. ( Edg ` H ) /\ { ( F ` b ) , ( F ` c ) } e. ( Edg ` H ) ) ) ) ) ) )
58 57 3impd 
 |-  ( ( G e. UHGraph /\ H e. UHGraph /\ F e. ( G GraphIso H ) ) -> ( ( T = { a , b , c } /\ ( # ` T ) = 3 /\ ( { a , b } e. ( Edg ` G ) /\ { a , c } e. ( Edg ` G ) /\ { b , c } e. ( Edg ` G ) ) ) -> ( ( ( a e. ( Vtx ` G ) /\ b e. ( Vtx ` G ) ) /\ c e. ( Vtx ` G ) ) -> ( { ( F ` a ) , ( F ` b ) } e. ( Edg ` H ) /\ { ( F ` a ) , ( F ` c ) } e. ( Edg ` H ) /\ { ( F ` b ) , ( F ` c ) } e. ( Edg ` H ) ) ) ) )
59 58 com23 
 |-  ( ( G e. UHGraph /\ H e. UHGraph /\ F e. ( G GraphIso H ) ) -> ( ( ( 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 ) ) ) -> ( { ( F ` a ) , ( F ` b ) } e. ( Edg ` H ) /\ { ( F ` a ) , ( F ` c ) } e. ( Edg ` H ) /\ { ( F ` b ) , ( F ` c ) } e. ( Edg ` H ) ) ) ) )
60 1 2 3 59 syl3anc 
 |-  ( 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 ) ) ) -> ( { ( F ` a ) , ( F ` b ) } e. ( Edg ` H ) /\ { ( F ` a ) , ( F ` c ) } e. ( Edg ` H ) /\ { ( F ` b ) , ( F ` c ) } e. ( Edg ` H ) ) ) ) )
61 60 impl 
 |-  ( ( ( 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 ) ) ) -> ( { ( F ` a ) , ( F ` b ) } e. ( Edg ` H ) /\ { ( F ` a ) , ( F ` c ) } e. ( Edg ` H ) /\ { ( F ` b ) , ( F ` c ) } e. ( Edg ` H ) ) ) )
62 61 imp 
 |-  ( ( ( ( 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 ) ) ) ) -> ( { ( F ` a ) , ( F ` b ) } e. ( Edg ` H ) /\ { ( F ` a ) , ( F ` c ) } e. ( Edg ` H ) /\ { ( F ` b ) , ( F ` c ) } e. ( Edg ` H ) ) )
63 tpeq1 
 |-  ( x = ( F ` a ) -> { x , y , z } = { ( F ` a ) , y , z } )
64 63 eqeq2d 
 |-  ( x = ( F ` a ) -> ( ( F " T ) = { x , y , z } <-> ( F " T ) = { ( F ` a ) , y , z } ) )
65 preq1 
 |-  ( x = ( F ` a ) -> { x , y } = { ( F ` a ) , y } )
66 65 eleq1d 
 |-  ( x = ( F ` a ) -> ( { x , y } e. ( Edg ` H ) <-> { ( F ` a ) , y } e. ( Edg ` H ) ) )
67 preq1 
 |-  ( x = ( F ` a ) -> { x , z } = { ( F ` a ) , z } )
68 67 eleq1d 
 |-  ( x = ( F ` a ) -> ( { x , z } e. ( Edg ` H ) <-> { ( F ` a ) , z } e. ( Edg ` H ) ) )
69 66 68 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 ) ) ) )
70 64 69 3anbi13d 
 |-  ( x = ( F ` a ) -> ( ( ( F " T ) = { x , y , z } /\ ( # ` ( F " T ) ) = 3 /\ ( { x , y } e. ( Edg ` H ) /\ { x , z } e. ( Edg ` H ) /\ { y , z } e. ( Edg ` H ) ) ) <-> ( ( F " T ) = { ( F ` a ) , y , z } /\ ( # ` ( F " T ) ) = 3 /\ ( { ( F ` a ) , y } e. ( Edg ` H ) /\ { ( F ` a ) , z } e. ( Edg ` H ) /\ { y , z } e. ( Edg ` H ) ) ) ) )
71 tpeq2 
 |-  ( y = ( F ` b ) -> { ( F ` a ) , y , z } = { ( F ` a ) , ( F ` b ) , z } )
72 71 eqeq2d 
 |-  ( y = ( F ` b ) -> ( ( F " T ) = { ( F ` a ) , y , z } <-> ( F " T ) = { ( F ` a ) , ( F ` b ) , z } ) )
73 preq2 
 |-  ( y = ( F ` b ) -> { ( F ` a ) , y } = { ( F ` a ) , ( F ` b ) } )
74 73 eleq1d 
 |-  ( y = ( F ` b ) -> ( { ( F ` a ) , y } e. ( Edg ` H ) <-> { ( F ` a ) , ( F ` b ) } e. ( Edg ` H ) ) )
75 preq1 
 |-  ( y = ( F ` b ) -> { y , z } = { ( F ` b ) , z } )
76 75 eleq1d 
 |-  ( y = ( F ` b ) -> ( { y , z } e. ( Edg ` H ) <-> { ( F ` b ) , z } e. ( Edg ` H ) ) )
77 74 76 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 ) ) ) )
78 72 77 3anbi13d 
 |-  ( y = ( F ` b ) -> ( ( ( F " T ) = { ( F ` a ) , y , z } /\ ( # ` ( F " T ) ) = 3 /\ ( { ( F ` a ) , y } e. ( Edg ` H ) /\ { ( F ` a ) , z } e. ( Edg ` H ) /\ { y , z } e. ( Edg ` H ) ) ) <-> ( ( F " T ) = { ( F ` a ) , ( F ` b ) , z } /\ ( # ` ( F " T ) ) = 3 /\ ( { ( F ` a ) , ( F ` b ) } e. ( Edg ` H ) /\ { ( F ` a ) , z } e. ( Edg ` H ) /\ { ( F ` b ) , z } e. ( Edg ` H ) ) ) ) )
79 tpeq3 
 |-  ( z = ( F ` c ) -> { ( F ` a ) , ( F ` b ) , z } = { ( F ` a ) , ( F ` b ) , ( F ` c ) } )
80 79 eqeq2d 
 |-  ( z = ( F ` c ) -> ( ( F " T ) = { ( F ` a ) , ( F ` b ) , z } <-> ( F " T ) = { ( F ` a ) , ( F ` b ) , ( F ` c ) } ) )
81 preq2 
 |-  ( z = ( F ` c ) -> { ( F ` a ) , z } = { ( F ` a ) , ( F ` c ) } )
82 81 eleq1d 
 |-  ( z = ( F ` c ) -> ( { ( F ` a ) , z } e. ( Edg ` H ) <-> { ( F ` a ) , ( F ` c ) } e. ( Edg ` H ) ) )
83 preq2 
 |-  ( z = ( F ` c ) -> { ( F ` b ) , z } = { ( F ` b ) , ( F ` c ) } )
84 83 eleq1d 
 |-  ( z = ( F ` c ) -> ( { ( F ` b ) , z } e. ( Edg ` H ) <-> { ( F ` b ) , ( F ` c ) } e. ( Edg ` H ) ) )
85 82 84 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 ) ) ) )
86 80 85 3anbi13d 
 |-  ( z = ( F ` c ) -> ( ( ( F " T ) = { ( F ` a ) , ( F ` b ) , z } /\ ( # ` ( F " T ) ) = 3 /\ ( { ( F ` a ) , ( F ` b ) } e. ( Edg ` H ) /\ { ( F ` a ) , z } e. ( Edg ` H ) /\ { ( F ` b ) , z } e. ( Edg ` H ) ) ) <-> ( ( 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 ) ) ) ) )
87 70 78 86 rspc3ev 
 |-  ( ( ( ( F ` a ) e. ( Vtx ` H ) /\ ( F ` b ) e. ( Vtx ` H ) /\ ( F ` c ) e. ( Vtx ` H ) ) /\ ( ( 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 ) ) ) ) -> E. x e. ( Vtx ` H ) E. y e. ( Vtx ` H ) E. z e. ( Vtx ` H ) ( ( F " T ) = { x , y , z } /\ ( # ` ( F " T ) ) = 3 /\ ( { x , y } e. ( Edg ` H ) /\ { x , z } e. ( Edg ` H ) /\ { y , z } e. ( Edg ` H ) ) ) )
88 87 3exp2 
 |-  ( ( ( F ` a ) e. ( Vtx ` H ) /\ ( F ` b ) e. ( Vtx ` H ) /\ ( F ` c ) e. ( Vtx ` H ) ) -> ( ( 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 ) ) -> E. x e. ( Vtx ` H ) E. y e. ( Vtx ` H ) E. z e. ( Vtx ` H ) ( ( F " T ) = { x , y , z } /\ ( # ` ( F " T ) ) = 3 /\ ( { x , y } e. ( Edg ` H ) /\ { x , z } e. ( Edg ` H ) /\ { y , z } e. ( Edg ` H ) ) ) ) ) ) )
89 88 3imp 
 |-  ( ( ( ( F ` a ) e. ( Vtx ` H ) /\ ( F ` b ) e. ( Vtx ` H ) /\ ( F ` c ) e. ( Vtx ` H ) ) /\ ( 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 ) ) -> E. x e. ( Vtx ` H ) E. y e. ( Vtx ` H ) E. z e. ( Vtx ` H ) ( ( F " T ) = { x , y , z } /\ ( # ` ( F " T ) ) = 3 /\ ( { x , y } e. ( Edg ` H ) /\ { x , z } e. ( Edg ` H ) /\ { y , z } e. ( Edg ` H ) ) ) ) )
90 25 62 89 sylc 
 |-  ( ( ( ( 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. x e. ( Vtx ` H ) E. y e. ( Vtx ` H ) E. z e. ( Vtx ` H ) ( ( F " T ) = { x , y , z } /\ ( # ` ( F " T ) ) = 3 /\ ( { x , y } e. ( Edg ` H ) /\ { x , z } e. ( Edg ` H ) /\ { y , z } e. ( Edg ` H ) ) ) )
91 90 rexlimdva2 
 |-  ( ( ph /\ ( a e. ( Vtx ` G ) /\ 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. x e. ( Vtx ` H ) E. y e. ( Vtx ` H ) E. z e. ( Vtx ` H ) ( ( F " T ) = { x , y , z } /\ ( # ` ( F " T ) ) = 3 /\ ( { x , y } e. ( Edg ` H ) /\ { x , z } e. ( Edg ` H ) /\ { y , z } e. ( Edg ` H ) ) ) ) )
92 91 rexlimdvva 
 |-  ( 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. x e. ( Vtx ` H ) E. y e. ( Vtx ` H ) E. z e. ( Vtx ` H ) ( ( F " T ) = { x , y , z } /\ ( # ` ( F " T ) ) = 3 /\ ( { x , y } e. ( Edg ` H ) /\ { x , z } e. ( Edg ` H ) /\ { y , z } e. ( Edg ` H ) ) ) ) )
93 8 92 mpd 
 |-  ( ph -> E. x e. ( Vtx ` H ) E. y e. ( Vtx ` H ) E. z e. ( Vtx ` H ) ( ( F " T ) = { x , y , z } /\ ( # ` ( F " T ) ) = 3 /\ ( { x , y } e. ( Edg ` H ) /\ { x , z } e. ( Edg ` H ) /\ { y , z } e. ( Edg ` H ) ) ) )
94 9 26 isgrtri 
 |-  ( ( F " T ) e. ( GrTriangles ` H ) <-> E. x e. ( Vtx ` H ) E. y e. ( Vtx ` H ) E. z e. ( Vtx ` H ) ( ( F " T ) = { x , y , z } /\ ( # ` ( F " T ) ) = 3 /\ ( { x , y } e. ( Edg ` H ) /\ { x , z } e. ( Edg ` H ) /\ { y , z } e. ( Edg ` H ) ) ) )
95 93 94 sylibr 
 |-  ( ph -> ( F " T ) e. ( GrTriangles ` H ) )