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

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 ⊢ ( 𝜑 → 𝐺 ∈ UHGraph )
grimgrtri.h ⊢ ( 𝜑 → 𝐻 ∈ UHGraph )
grimgrtri.n ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) )
grimgrtri.t ⊢ ( 𝜑 → 𝑇 ∈ ( GrTriangles ‘ 𝐺 ) )
Assertion grimgrtri ( 𝜑 → ( 𝐹 “ 𝑇 ) ∈ ( GrTriangles ‘ 𝐻 ) )

Proof

Step Hyp Ref Expression
1 grimgrtri.g ⊢ ( 𝜑 → 𝐺 ∈ UHGraph )
2 grimgrtri.h ⊢ ( 𝜑 → 𝐻 ∈ UHGraph )
3 grimgrtri.n ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) )
4 grimgrtri.t ⊢ ( 𝜑 → 𝑇 ∈ ( GrTriangles ‘ 𝐺 ) )
5 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
6 eqid ⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
7 5 6 grtriprop ⊢ ( 𝑇 ∈ ( GrTriangles ‘ 𝐺 ) → ∃ 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∃ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ∃ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ( 𝑇 = { 𝑎 , 𝑏 , 𝑐 } ∧ ( ♯ ‘ 𝑇 ) = 3 ∧ ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑎 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ) )
8 4 7 syl ⊢ ( 𝜑 → ∃ 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∃ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ∃ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ( 𝑇 = { 𝑎 , 𝑏 , 𝑐 } ∧ ( ♯ ‘ 𝑇 ) = 3 ∧ ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑎 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ) )
9 eqid ⊢ ( Vtx ‘ 𝐻 ) = ( Vtx ‘ 𝐻 )
10 5 9 grimf1o ⊢ ( 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) → 𝐹 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) )
11 f1of1 ⊢ ( 𝐹 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) → 𝐹 : ( Vtx ‘ 𝐺 ) –1-1→ ( Vtx ‘ 𝐻 ) )
12 3 10 11 3syl ⊢ ( 𝜑 → 𝐹 : ( Vtx ‘ 𝐺 ) –1-1→ ( Vtx ‘ 𝐻 ) )
13 12 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ) ∧ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑇 = { 𝑎 , 𝑏 , 𝑐 } ∧ ( ♯ ‘ 𝑇 ) = 3 ∧ ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑎 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ) ) → 𝐹 : ( Vtx ‘ 𝐺 ) –1-1→ ( Vtx ‘ 𝐻 ) )
14 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ) ∧ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ) → 𝑎 ∈ ( Vtx ‘ 𝐺 ) )
15 14 adantr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ) ∧ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑇 = { 𝑎 , 𝑏 , 𝑐 } ∧ ( ♯ ‘ 𝑇 ) = 3 ∧ ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑎 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ) ) → 𝑎 ∈ ( Vtx ‘ 𝐺 ) )
16 simprr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ) → 𝑏 ∈ ( Vtx ‘ 𝐺 ) )
17 16 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ) ∧ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ) → 𝑏 ∈ ( Vtx ‘ 𝐺 ) )
18 17 adantr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ) ∧ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑇 = { 𝑎 , 𝑏 , 𝑐 } ∧ ( ♯ ‘ 𝑇 ) = 3 ∧ ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑎 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ) ) → 𝑏 ∈ ( Vtx ‘ 𝐺 ) )
19 simplr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ) ∧ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑇 = { 𝑎 , 𝑏 , 𝑐 } ∧ ( ♯ ‘ 𝑇 ) = 3 ∧ ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑎 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ) ) → 𝑐 ∈ ( Vtx ‘ 𝐺 ) )
20 15 18 19 3jca ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ) ∧ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑇 = { 𝑎 , 𝑏 , 𝑐 } ∧ ( ♯ ‘ 𝑇 ) = 3 ∧ ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑎 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ) ) → ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ) )
21 3simpa ⊢ ( ( 𝑇 = { 𝑎 , 𝑏 , 𝑐 } ∧ ( ♯ ‘ 𝑇 ) = 3 ∧ ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑎 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ) → ( 𝑇 = { 𝑎 , 𝑏 , 𝑐 } ∧ ( ♯ ‘ 𝑇 ) = 3 ) )
22 21 adantl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ) ∧ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑇 = { 𝑎 , 𝑏 , 𝑐 } ∧ ( ♯ ‘ 𝑇 ) = 3 ∧ ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑎 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ) ) → ( 𝑇 = { 𝑎 , 𝑏 , 𝑐 } ∧ ( ♯ ‘ 𝑇 ) = 3 ) )
23 grtrimap ⊢ ( 𝐹 : ( Vtx ‘ 𝐺 ) –1-1→ ( Vtx ‘ 𝐻 ) → ( ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑇 = { 𝑎 , 𝑏 , 𝑐 } ∧ ( ♯ ‘ 𝑇 ) = 3 ) ) → ( ( ( 𝐹 ‘ 𝑎 ) ∈ ( Vtx ‘ 𝐻 ) ∧ ( 𝐹 ‘ 𝑏 ) ∈ ( Vtx ‘ 𝐻 ) ∧ ( 𝐹 ‘ 𝑐 ) ∈ ( Vtx ‘ 𝐻 ) ) ∧ ( 𝐹 “ 𝑇 ) = { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) , ( 𝐹 ‘ 𝑐 ) } ∧ ( ♯ ‘ ( 𝐹 “ 𝑇 ) ) = 3 ) ) )
24 23 imp ⊢ ( ( 𝐹 : ( Vtx ‘ 𝐺 ) –1-1→ ( Vtx ‘ 𝐻 ) ∧ ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑇 = { 𝑎 , 𝑏 , 𝑐 } ∧ ( ♯ ‘ 𝑇 ) = 3 ) ) ) → ( ( ( 𝐹 ‘ 𝑎 ) ∈ ( Vtx ‘ 𝐻 ) ∧ ( 𝐹 ‘ 𝑏 ) ∈ ( Vtx ‘ 𝐻 ) ∧ ( 𝐹 ‘ 𝑐 ) ∈ ( Vtx ‘ 𝐻 ) ) ∧ ( 𝐹 “ 𝑇 ) = { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) , ( 𝐹 ‘ 𝑐 ) } ∧ ( ♯ ‘ ( 𝐹 “ 𝑇 ) ) = 3 ) )
25 13 20 22 24 syl12anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ) ∧ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑇 = { 𝑎 , 𝑏 , 𝑐 } ∧ ( ♯ ‘ 𝑇 ) = 3 ∧ ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑎 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ) ) → ( ( ( 𝐹 ‘ 𝑎 ) ∈ ( Vtx ‘ 𝐻 ) ∧ ( 𝐹 ‘ 𝑏 ) ∈ ( Vtx ‘ 𝐻 ) ∧ ( 𝐹 ‘ 𝑐 ) ∈ ( Vtx ‘ 𝐻 ) ) ∧ ( 𝐹 “ 𝑇 ) = { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) , ( 𝐹 ‘ 𝑐 ) } ∧ ( ♯ ‘ ( 𝐹 “ 𝑇 ) ) = 3 ) )
26 eqid ⊢ ( Edg ‘ 𝐻 ) = ( Edg ‘ 𝐻 )
27 5 6 26 grimedg ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ) → ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ↔ ( ( 𝐹 “ { 𝑎 , 𝑏 } ) ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑎 , 𝑏 } ⊆ ( Vtx ‘ 𝐺 ) ) ) )
28 5 6 26 grimedg ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ) → ( { 𝑎 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ↔ ( ( 𝐹 “ { 𝑎 , 𝑐 } ) ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑎 , 𝑐 } ⊆ ( Vtx ‘ 𝐺 ) ) ) )
29 5 6 26 grimedg ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ) → ( { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ↔ ( ( 𝐹 “ { 𝑏 , 𝑐 } ) ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑏 , 𝑐 } ⊆ ( Vtx ‘ 𝐺 ) ) ) )
30 27 28 29 3anbi123d ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ) → ( ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑎 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ↔ ( ( ( 𝐹 “ { 𝑎 , 𝑏 } ) ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑎 , 𝑏 } ⊆ ( Vtx ‘ 𝐺 ) ) ∧ ( ( 𝐹 “ { 𝑎 , 𝑐 } ) ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑎 , 𝑐 } ⊆ ( Vtx ‘ 𝐺 ) ) ∧ ( ( 𝐹 “ { 𝑏 , 𝑐 } ) ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑏 , 𝑐 } ⊆ ( Vtx ‘ 𝐺 ) ) ) ) )
31 f1ofn ⊢ ( 𝐹 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) → 𝐹 Fn ( Vtx ‘ 𝐺 ) )
32 simpl ⊢ ( ( 𝐹 Fn ( Vtx ‘ 𝐺 ) ∧ ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ) ) → 𝐹 Fn ( Vtx ‘ 𝐺 ) )
33 simprll ⊢ ( ( 𝐹 Fn ( Vtx ‘ 𝐺 ) ∧ ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ) ) → 𝑎 ∈ ( Vtx ‘ 𝐺 ) )
34 simprlr ⊢ ( ( 𝐹 Fn ( Vtx ‘ 𝐺 ) ∧ ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ) ) → 𝑏 ∈ ( Vtx ‘ 𝐺 ) )
35 fnimapr ⊢ ( ( 𝐹 Fn ( Vtx ‘ 𝐺 ) ∧ 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) → ( 𝐹 “ { 𝑎 , 𝑏 } ) = { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) } )
36 32 33 34 35 syl3anc ⊢ ( ( 𝐹 Fn ( Vtx ‘ 𝐺 ) ∧ ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ) ) → ( 𝐹 “ { 𝑎 , 𝑏 } ) = { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) } )
37 36 eleq1d ⊢ ( ( 𝐹 Fn ( Vtx ‘ 𝐺 ) ∧ ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ) ) → ( ( 𝐹 “ { 𝑎 , 𝑏 } ) ∈ ( Edg ‘ 𝐻 ) ↔ { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) } ∈ ( Edg ‘ 𝐻 ) ) )
38 37 biimpd ⊢ ( ( 𝐹 Fn ( Vtx ‘ 𝐺 ) ∧ ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ) ) → ( ( 𝐹 “ { 𝑎 , 𝑏 } ) ∈ ( Edg ‘ 𝐻 ) → { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) } ∈ ( Edg ‘ 𝐻 ) ) )
39 38 adantrd ⊢ ( ( 𝐹 Fn ( Vtx ‘ 𝐺 ) ∧ ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ) ) → ( ( ( 𝐹 “ { 𝑎 , 𝑏 } ) ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑎 , 𝑏 } ⊆ ( Vtx ‘ 𝐺 ) ) → { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) } ∈ ( Edg ‘ 𝐻 ) ) )
40 simprr ⊢ ( ( 𝐹 Fn ( Vtx ‘ 𝐺 ) ∧ ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ) ) → 𝑐 ∈ ( Vtx ‘ 𝐺 ) )
41 fnimapr ⊢ ( ( 𝐹 Fn ( Vtx ‘ 𝐺 ) ∧ 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ) → ( 𝐹 “ { 𝑎 , 𝑐 } ) = { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑐 ) } )
42 32 33 40 41 syl3anc ⊢ ( ( 𝐹 Fn ( Vtx ‘ 𝐺 ) ∧ ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ) ) → ( 𝐹 “ { 𝑎 , 𝑐 } ) = { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑐 ) } )
43 42 eleq1d ⊢ ( ( 𝐹 Fn ( Vtx ‘ 𝐺 ) ∧ ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ) ) → ( ( 𝐹 “ { 𝑎 , 𝑐 } ) ∈ ( Edg ‘ 𝐻 ) ↔ { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑐 ) } ∈ ( Edg ‘ 𝐻 ) ) )
44 43 biimpd ⊢ ( ( 𝐹 Fn ( Vtx ‘ 𝐺 ) ∧ ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ) ) → ( ( 𝐹 “ { 𝑎 , 𝑐 } ) ∈ ( Edg ‘ 𝐻 ) → { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑐 ) } ∈ ( Edg ‘ 𝐻 ) ) )
45 44 adantrd ⊢ ( ( 𝐹 Fn ( Vtx ‘ 𝐺 ) ∧ ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ) ) → ( ( ( 𝐹 “ { 𝑎 , 𝑐 } ) ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑎 , 𝑐 } ⊆ ( Vtx ‘ 𝐺 ) ) → { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑐 ) } ∈ ( Edg ‘ 𝐻 ) ) )
46 fnimapr ⊢ ( ( 𝐹 Fn ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ) → ( 𝐹 “ { 𝑏 , 𝑐 } ) = { ( 𝐹 ‘ 𝑏 ) , ( 𝐹 ‘ 𝑐 ) } )
47 32 34 40 46 syl3anc ⊢ ( ( 𝐹 Fn ( Vtx ‘ 𝐺 ) ∧ ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ) ) → ( 𝐹 “ { 𝑏 , 𝑐 } ) = { ( 𝐹 ‘ 𝑏 ) , ( 𝐹 ‘ 𝑐 ) } )
48 47 eleq1d ⊢ ( ( 𝐹 Fn ( Vtx ‘ 𝐺 ) ∧ ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ) ) → ( ( 𝐹 “ { 𝑏 , 𝑐 } ) ∈ ( Edg ‘ 𝐻 ) ↔ { ( 𝐹 ‘ 𝑏 ) , ( 𝐹 ‘ 𝑐 ) } ∈ ( Edg ‘ 𝐻 ) ) )
49 48 biimpd ⊢ ( ( 𝐹 Fn ( Vtx ‘ 𝐺 ) ∧ ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ) ) → ( ( 𝐹 “ { 𝑏 , 𝑐 } ) ∈ ( Edg ‘ 𝐻 ) → { ( 𝐹 ‘ 𝑏 ) , ( 𝐹 ‘ 𝑐 ) } ∈ ( Edg ‘ 𝐻 ) ) )
50 49 adantrd ⊢ ( ( 𝐹 Fn ( Vtx ‘ 𝐺 ) ∧ ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ) ) → ( ( ( 𝐹 “ { 𝑏 , 𝑐 } ) ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑏 , 𝑐 } ⊆ ( Vtx ‘ 𝐺 ) ) → { ( 𝐹 ‘ 𝑏 ) , ( 𝐹 ‘ 𝑐 ) } ∈ ( Edg ‘ 𝐻 ) ) )
51 39 45 50 3anim123d ⊢ ( ( 𝐹 Fn ( Vtx ‘ 𝐺 ) ∧ ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ) ) → ( ( ( ( 𝐹 “ { 𝑎 , 𝑏 } ) ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑎 , 𝑏 } ⊆ ( Vtx ‘ 𝐺 ) ) ∧ ( ( 𝐹 “ { 𝑎 , 𝑐 } ) ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑎 , 𝑐 } ⊆ ( Vtx ‘ 𝐺 ) ) ∧ ( ( 𝐹 “ { 𝑏 , 𝑐 } ) ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑏 , 𝑐 } ⊆ ( Vtx ‘ 𝐺 ) ) ) → ( { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) } ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑐 ) } ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑏 ) , ( 𝐹 ‘ 𝑐 ) } ∈ ( Edg ‘ 𝐻 ) ) ) )
52 51 ex ⊢ ( 𝐹 Fn ( Vtx ‘ 𝐺 ) → ( ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ) → ( ( ( ( 𝐹 “ { 𝑎 , 𝑏 } ) ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑎 , 𝑏 } ⊆ ( Vtx ‘ 𝐺 ) ) ∧ ( ( 𝐹 “ { 𝑎 , 𝑐 } ) ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑎 , 𝑐 } ⊆ ( Vtx ‘ 𝐺 ) ) ∧ ( ( 𝐹 “ { 𝑏 , 𝑐 } ) ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑏 , 𝑐 } ⊆ ( Vtx ‘ 𝐺 ) ) ) → ( { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) } ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑐 ) } ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑏 ) , ( 𝐹 ‘ 𝑐 ) } ∈ ( Edg ‘ 𝐻 ) ) ) ) )
53 52 com23 ⊢ ( 𝐹 Fn ( Vtx ‘ 𝐺 ) → ( ( ( ( 𝐹 “ { 𝑎 , 𝑏 } ) ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑎 , 𝑏 } ⊆ ( Vtx ‘ 𝐺 ) ) ∧ ( ( 𝐹 “ { 𝑎 , 𝑐 } ) ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑎 , 𝑐 } ⊆ ( Vtx ‘ 𝐺 ) ) ∧ ( ( 𝐹 “ { 𝑏 , 𝑐 } ) ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑏 , 𝑐 } ⊆ ( Vtx ‘ 𝐺 ) ) ) → ( ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ) → ( { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) } ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑐 ) } ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑏 ) , ( 𝐹 ‘ 𝑐 ) } ∈ ( Edg ‘ 𝐻 ) ) ) ) )
54 10 31 53 3syl ⊢ ( 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) → ( ( ( ( 𝐹 “ { 𝑎 , 𝑏 } ) ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑎 , 𝑏 } ⊆ ( Vtx ‘ 𝐺 ) ) ∧ ( ( 𝐹 “ { 𝑎 , 𝑐 } ) ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑎 , 𝑐 } ⊆ ( Vtx ‘ 𝐺 ) ) ∧ ( ( 𝐹 “ { 𝑏 , 𝑐 } ) ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑏 , 𝑐 } ⊆ ( Vtx ‘ 𝐺 ) ) ) → ( ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ) → ( { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) } ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑐 ) } ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑏 ) , ( 𝐹 ‘ 𝑐 ) } ∈ ( Edg ‘ 𝐻 ) ) ) ) )
55 54 3ad2ant3 ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ) → ( ( ( ( 𝐹 “ { 𝑎 , 𝑏 } ) ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑎 , 𝑏 } ⊆ ( Vtx ‘ 𝐺 ) ) ∧ ( ( 𝐹 “ { 𝑎 , 𝑐 } ) ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑎 , 𝑐 } ⊆ ( Vtx ‘ 𝐺 ) ) ∧ ( ( 𝐹 “ { 𝑏 , 𝑐 } ) ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑏 , 𝑐 } ⊆ ( Vtx ‘ 𝐺 ) ) ) → ( ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ) → ( { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) } ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑐 ) } ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑏 ) , ( 𝐹 ‘ 𝑐 ) } ∈ ( Edg ‘ 𝐻 ) ) ) ) )
56 30 55 sylbid ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ) → ( ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑎 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) → ( ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ) → ( { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) } ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑐 ) } ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑏 ) , ( 𝐹 ‘ 𝑐 ) } ∈ ( Edg ‘ 𝐻 ) ) ) ) )
57 56 2a1d ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ) → ( 𝑇 = { 𝑎 , 𝑏 , 𝑐 } → ( ( ♯ ‘ 𝑇 ) = 3 → ( ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑎 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) → ( ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ) → ( { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) } ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑐 ) } ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑏 ) , ( 𝐹 ‘ 𝑐 ) } ∈ ( Edg ‘ 𝐻 ) ) ) ) ) ) )
58 57 3impd ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ) → ( ( 𝑇 = { 𝑎 , 𝑏 , 𝑐 } ∧ ( ♯ ‘ 𝑇 ) = 3 ∧ ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑎 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ) → ( ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ) → ( { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) } ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑐 ) } ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑏 ) , ( 𝐹 ‘ 𝑐 ) } ∈ ( Edg ‘ 𝐻 ) ) ) ) )
59 58 com23 ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ) → ( ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ) → ( ( 𝑇 = { 𝑎 , 𝑏 , 𝑐 } ∧ ( ♯ ‘ 𝑇 ) = 3 ∧ ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑎 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ) → ( { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) } ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑐 ) } ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑏 ) , ( 𝐹 ‘ 𝑐 ) } ∈ ( Edg ‘ 𝐻 ) ) ) ) )
60 1 2 3 59 syl3anc ⊢ ( 𝜑 → ( ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ) → ( ( 𝑇 = { 𝑎 , 𝑏 , 𝑐 } ∧ ( ♯ ‘ 𝑇 ) = 3 ∧ ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑎 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ) → ( { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) } ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑐 ) } ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑏 ) , ( 𝐹 ‘ 𝑐 ) } ∈ ( Edg ‘ 𝐻 ) ) ) ) )
61 60 impl ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ) ∧ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ) → ( ( 𝑇 = { 𝑎 , 𝑏 , 𝑐 } ∧ ( ♯ ‘ 𝑇 ) = 3 ∧ ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑎 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ) → ( { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) } ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑐 ) } ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑏 ) , ( 𝐹 ‘ 𝑐 ) } ∈ ( Edg ‘ 𝐻 ) ) ) )
62 61 imp ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ) ∧ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑇 = { 𝑎 , 𝑏 , 𝑐 } ∧ ( ♯ ‘ 𝑇 ) = 3 ∧ ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑎 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ) ) → ( { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) } ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑐 ) } ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑏 ) , ( 𝐹 ‘ 𝑐 ) } ∈ ( Edg ‘ 𝐻 ) ) )
63 tpeq1 ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑎 ) → { 𝑥 , 𝑦 , 𝑧 } = { ( 𝐹 ‘ 𝑎 ) , 𝑦 , 𝑧 } )
64 63 eqeq2d ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑎 ) → ( ( 𝐹 “ 𝑇 ) = { 𝑥 , 𝑦 , 𝑧 } ↔ ( 𝐹 “ 𝑇 ) = { ( 𝐹 ‘ 𝑎 ) , 𝑦 , 𝑧 } ) )
65 preq1 ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑎 ) → { 𝑥 , 𝑦 } = { ( 𝐹 ‘ 𝑎 ) , 𝑦 } )
66 65 eleq1d ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑎 ) → ( { 𝑥 , 𝑦 } ∈ ( Edg ‘ 𝐻 ) ↔ { ( 𝐹 ‘ 𝑎 ) , 𝑦 } ∈ ( Edg ‘ 𝐻 ) ) )
67 preq1 ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑎 ) → { 𝑥 , 𝑧 } = { ( 𝐹 ‘ 𝑎 ) , 𝑧 } )
68 67 eleq1d ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑎 ) → ( { 𝑥 , 𝑧 } ∈ ( Edg ‘ 𝐻 ) ↔ { ( 𝐹 ‘ 𝑎 ) , 𝑧 } ∈ ( Edg ‘ 𝐻 ) ) )
69 66 68 3anbi12d ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑎 ) → ( ( { 𝑥 , 𝑦 } ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑥 , 𝑧 } ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑦 , 𝑧 } ∈ ( Edg ‘ 𝐻 ) ) ↔ ( { ( 𝐹 ‘ 𝑎 ) , 𝑦 } ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑎 ) , 𝑧 } ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑦 , 𝑧 } ∈ ( Edg ‘ 𝐻 ) ) ) )
70 64 69 3anbi13d ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑎 ) → ( ( ( 𝐹 “ 𝑇 ) = { 𝑥 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ ( 𝐹 “ 𝑇 ) ) = 3 ∧ ( { 𝑥 , 𝑦 } ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑥 , 𝑧 } ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑦 , 𝑧 } ∈ ( Edg ‘ 𝐻 ) ) ) ↔ ( ( 𝐹 “ 𝑇 ) = { ( 𝐹 ‘ 𝑎 ) , 𝑦 , 𝑧 } ∧ ( ♯ ‘ ( 𝐹 “ 𝑇 ) ) = 3 ∧ ( { ( 𝐹 ‘ 𝑎 ) , 𝑦 } ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑎 ) , 𝑧 } ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑦 , 𝑧 } ∈ ( Edg ‘ 𝐻 ) ) ) ) )
71 tpeq2 ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑏 ) → { ( 𝐹 ‘ 𝑎 ) , 𝑦 , 𝑧 } = { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) , 𝑧 } )
72 71 eqeq2d ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑏 ) → ( ( 𝐹 “ 𝑇 ) = { ( 𝐹 ‘ 𝑎 ) , 𝑦 , 𝑧 } ↔ ( 𝐹 “ 𝑇 ) = { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) , 𝑧 } ) )
73 preq2 ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑏 ) → { ( 𝐹 ‘ 𝑎 ) , 𝑦 } = { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) } )
74 73 eleq1d ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑏 ) → ( { ( 𝐹 ‘ 𝑎 ) , 𝑦 } ∈ ( Edg ‘ 𝐻 ) ↔ { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) } ∈ ( Edg ‘ 𝐻 ) ) )
75 preq1 ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑏 ) → { 𝑦 , 𝑧 } = { ( 𝐹 ‘ 𝑏 ) , 𝑧 } )
76 75 eleq1d ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑏 ) → ( { 𝑦 , 𝑧 } ∈ ( Edg ‘ 𝐻 ) ↔ { ( 𝐹 ‘ 𝑏 ) , 𝑧 } ∈ ( Edg ‘ 𝐻 ) ) )
77 74 76 3anbi13d ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑏 ) → ( ( { ( 𝐹 ‘ 𝑎 ) , 𝑦 } ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑎 ) , 𝑧 } ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑦 , 𝑧 } ∈ ( Edg ‘ 𝐻 ) ) ↔ ( { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) } ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑎 ) , 𝑧 } ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑏 ) , 𝑧 } ∈ ( Edg ‘ 𝐻 ) ) ) )
78 72 77 3anbi13d ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑏 ) → ( ( ( 𝐹 “ 𝑇 ) = { ( 𝐹 ‘ 𝑎 ) , 𝑦 , 𝑧 } ∧ ( ♯ ‘ ( 𝐹 “ 𝑇 ) ) = 3 ∧ ( { ( 𝐹 ‘ 𝑎 ) , 𝑦 } ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑎 ) , 𝑧 } ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑦 , 𝑧 } ∈ ( Edg ‘ 𝐻 ) ) ) ↔ ( ( 𝐹 “ 𝑇 ) = { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) , 𝑧 } ∧ ( ♯ ‘ ( 𝐹 “ 𝑇 ) ) = 3 ∧ ( { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) } ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑎 ) , 𝑧 } ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑏 ) , 𝑧 } ∈ ( Edg ‘ 𝐻 ) ) ) ) )
79 tpeq3 ⊢ ( 𝑧 = ( 𝐹 ‘ 𝑐 ) → { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) , 𝑧 } = { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) , ( 𝐹 ‘ 𝑐 ) } )
80 79 eqeq2d ⊢ ( 𝑧 = ( 𝐹 ‘ 𝑐 ) → ( ( 𝐹 “ 𝑇 ) = { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) , 𝑧 } ↔ ( 𝐹 “ 𝑇 ) = { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) , ( 𝐹 ‘ 𝑐 ) } ) )
81 preq2 ⊢ ( 𝑧 = ( 𝐹 ‘ 𝑐 ) → { ( 𝐹 ‘ 𝑎 ) , 𝑧 } = { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑐 ) } )
82 81 eleq1d ⊢ ( 𝑧 = ( 𝐹 ‘ 𝑐 ) → ( { ( 𝐹 ‘ 𝑎 ) , 𝑧 } ∈ ( Edg ‘ 𝐻 ) ↔ { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑐 ) } ∈ ( Edg ‘ 𝐻 ) ) )
83 preq2 ⊢ ( 𝑧 = ( 𝐹 ‘ 𝑐 ) → { ( 𝐹 ‘ 𝑏 ) , 𝑧 } = { ( 𝐹 ‘ 𝑏 ) , ( 𝐹 ‘ 𝑐 ) } )
84 83 eleq1d ⊢ ( 𝑧 = ( 𝐹 ‘ 𝑐 ) → ( { ( 𝐹 ‘ 𝑏 ) , 𝑧 } ∈ ( Edg ‘ 𝐻 ) ↔ { ( 𝐹 ‘ 𝑏 ) , ( 𝐹 ‘ 𝑐 ) } ∈ ( Edg ‘ 𝐻 ) ) )
85 82 84 3anbi23d ⊢ ( 𝑧 = ( 𝐹 ‘ 𝑐 ) → ( ( { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) } ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑎 ) , 𝑧 } ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑏 ) , 𝑧 } ∈ ( Edg ‘ 𝐻 ) ) ↔ ( { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) } ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑐 ) } ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑏 ) , ( 𝐹 ‘ 𝑐 ) } ∈ ( Edg ‘ 𝐻 ) ) ) )
86 80 85 3anbi13d ⊢ ( 𝑧 = ( 𝐹 ‘ 𝑐 ) → ( ( ( 𝐹 “ 𝑇 ) = { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) , 𝑧 } ∧ ( ♯ ‘ ( 𝐹 “ 𝑇 ) ) = 3 ∧ ( { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) } ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑎 ) , 𝑧 } ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑏 ) , 𝑧 } ∈ ( Edg ‘ 𝐻 ) ) ) ↔ ( ( 𝐹 “ 𝑇 ) = { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) , ( 𝐹 ‘ 𝑐 ) } ∧ ( ♯ ‘ ( 𝐹 “ 𝑇 ) ) = 3 ∧ ( { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) } ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑐 ) } ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑏 ) , ( 𝐹 ‘ 𝑐 ) } ∈ ( Edg ‘ 𝐻 ) ) ) ) )
87 70 78 86 rspc3ev ⊢ ( ( ( ( 𝐹 ‘ 𝑎 ) ∈ ( Vtx ‘ 𝐻 ) ∧ ( 𝐹 ‘ 𝑏 ) ∈ ( Vtx ‘ 𝐻 ) ∧ ( 𝐹 ‘ 𝑐 ) ∈ ( Vtx ‘ 𝐻 ) ) ∧ ( ( 𝐹 “ 𝑇 ) = { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) , ( 𝐹 ‘ 𝑐 ) } ∧ ( ♯ ‘ ( 𝐹 “ 𝑇 ) ) = 3 ∧ ( { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) } ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑐 ) } ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑏 ) , ( 𝐹 ‘ 𝑐 ) } ∈ ( Edg ‘ 𝐻 ) ) ) ) → ∃ 𝑥 ∈ ( Vtx ‘ 𝐻 ) ∃ 𝑦 ∈ ( Vtx ‘ 𝐻 ) ∃ 𝑧 ∈ ( Vtx ‘ 𝐻 ) ( ( 𝐹 “ 𝑇 ) = { 𝑥 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ ( 𝐹 “ 𝑇 ) ) = 3 ∧ ( { 𝑥 , 𝑦 } ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑥 , 𝑧 } ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑦 , 𝑧 } ∈ ( Edg ‘ 𝐻 ) ) ) )
88 87 3exp2 ⊢ ( ( ( 𝐹 ‘ 𝑎 ) ∈ ( Vtx ‘ 𝐻 ) ∧ ( 𝐹 ‘ 𝑏 ) ∈ ( Vtx ‘ 𝐻 ) ∧ ( 𝐹 ‘ 𝑐 ) ∈ ( Vtx ‘ 𝐻 ) ) → ( ( 𝐹 “ 𝑇 ) = { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) , ( 𝐹 ‘ 𝑐 ) } → ( ( ♯ ‘ ( 𝐹 “ 𝑇 ) ) = 3 → ( ( { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) } ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑐 ) } ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑏 ) , ( 𝐹 ‘ 𝑐 ) } ∈ ( Edg ‘ 𝐻 ) ) → ∃ 𝑥 ∈ ( Vtx ‘ 𝐻 ) ∃ 𝑦 ∈ ( Vtx ‘ 𝐻 ) ∃ 𝑧 ∈ ( Vtx ‘ 𝐻 ) ( ( 𝐹 “ 𝑇 ) = { 𝑥 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ ( 𝐹 “ 𝑇 ) ) = 3 ∧ ( { 𝑥 , 𝑦 } ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑥 , 𝑧 } ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑦 , 𝑧 } ∈ ( Edg ‘ 𝐻 ) ) ) ) ) ) )
89 88 3imp ⊢ ( ( ( ( 𝐹 ‘ 𝑎 ) ∈ ( Vtx ‘ 𝐻 ) ∧ ( 𝐹 ‘ 𝑏 ) ∈ ( Vtx ‘ 𝐻 ) ∧ ( 𝐹 ‘ 𝑐 ) ∈ ( Vtx ‘ 𝐻 ) ) ∧ ( 𝐹 “ 𝑇 ) = { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) , ( 𝐹 ‘ 𝑐 ) } ∧ ( ♯ ‘ ( 𝐹 “ 𝑇 ) ) = 3 ) → ( ( { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) } ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑐 ) } ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑏 ) , ( 𝐹 ‘ 𝑐 ) } ∈ ( Edg ‘ 𝐻 ) ) → ∃ 𝑥 ∈ ( Vtx ‘ 𝐻 ) ∃ 𝑦 ∈ ( Vtx ‘ 𝐻 ) ∃ 𝑧 ∈ ( Vtx ‘ 𝐻 ) ( ( 𝐹 “ 𝑇 ) = { 𝑥 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ ( 𝐹 “ 𝑇 ) ) = 3 ∧ ( { 𝑥 , 𝑦 } ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑥 , 𝑧 } ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑦 , 𝑧 } ∈ ( Edg ‘ 𝐻 ) ) ) ) )
90 25 62 89 sylc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ) ∧ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑇 = { 𝑎 , 𝑏 , 𝑐 } ∧ ( ♯ ‘ 𝑇 ) = 3 ∧ ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑎 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ) ) → ∃ 𝑥 ∈ ( Vtx ‘ 𝐻 ) ∃ 𝑦 ∈ ( Vtx ‘ 𝐻 ) ∃ 𝑧 ∈ ( Vtx ‘ 𝐻 ) ( ( 𝐹 “ 𝑇 ) = { 𝑥 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ ( 𝐹 “ 𝑇 ) ) = 3 ∧ ( { 𝑥 , 𝑦 } ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑥 , 𝑧 } ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑦 , 𝑧 } ∈ ( Edg ‘ 𝐻 ) ) ) )
91 90 rexlimdva2 ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ) → ( ∃ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ( 𝑇 = { 𝑎 , 𝑏 , 𝑐 } ∧ ( ♯ ‘ 𝑇 ) = 3 ∧ ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑎 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ) → ∃ 𝑥 ∈ ( Vtx ‘ 𝐻 ) ∃ 𝑦 ∈ ( Vtx ‘ 𝐻 ) ∃ 𝑧 ∈ ( Vtx ‘ 𝐻 ) ( ( 𝐹 “ 𝑇 ) = { 𝑥 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ ( 𝐹 “ 𝑇 ) ) = 3 ∧ ( { 𝑥 , 𝑦 } ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑥 , 𝑧 } ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑦 , 𝑧 } ∈ ( Edg ‘ 𝐻 ) ) ) ) )
92 91 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∃ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ∃ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ( 𝑇 = { 𝑎 , 𝑏 , 𝑐 } ∧ ( ♯ ‘ 𝑇 ) = 3 ∧ ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑎 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ) → ∃ 𝑥 ∈ ( Vtx ‘ 𝐻 ) ∃ 𝑦 ∈ ( Vtx ‘ 𝐻 ) ∃ 𝑧 ∈ ( Vtx ‘ 𝐻 ) ( ( 𝐹 “ 𝑇 ) = { 𝑥 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ ( 𝐹 “ 𝑇 ) ) = 3 ∧ ( { 𝑥 , 𝑦 } ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑥 , 𝑧 } ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑦 , 𝑧 } ∈ ( Edg ‘ 𝐻 ) ) ) ) )
93 8 92 mpd ⊢ ( 𝜑 → ∃ 𝑥 ∈ ( Vtx ‘ 𝐻 ) ∃ 𝑦 ∈ ( Vtx ‘ 𝐻 ) ∃ 𝑧 ∈ ( Vtx ‘ 𝐻 ) ( ( 𝐹 “ 𝑇 ) = { 𝑥 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ ( 𝐹 “ 𝑇 ) ) = 3 ∧ ( { 𝑥 , 𝑦 } ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑥 , 𝑧 } ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑦 , 𝑧 } ∈ ( Edg ‘ 𝐻 ) ) ) )
94 9 26 isgrtri ⊢ ( ( 𝐹 “ 𝑇 ) ∈ ( GrTriangles ‘ 𝐻 ) ↔ ∃ 𝑥 ∈ ( Vtx ‘ 𝐻 ) ∃ 𝑦 ∈ ( Vtx ‘ 𝐻 ) ∃ 𝑧 ∈ ( Vtx ‘ 𝐻 ) ( ( 𝐹 “ 𝑇 ) = { 𝑥 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ ( 𝐹 “ 𝑇 ) ) = 3 ∧ ( { 𝑥 , 𝑦 } ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑥 , 𝑧 } ∈ ( Edg ‘ 𝐻 ) ∧ { 𝑦 , 𝑧 } ∈ ( Edg ‘ 𝐻 ) ) ) )
95 93 94 sylibr ⊢ ( 𝜑 → ( 𝐹 “ 𝑇 ) ∈ ( GrTriangles ‘ 𝐻 ) )