Metamath Proof Explorer

Theorem grlimgrtri

Description: Local isomorphisms between simple pseudographs map triangles onto triangles. (Contributed by AV, 24-Aug-2025)

Ref Expression
Hypotheses grlimgrtri.g ⊢ ( 𝜑 → 𝐺 ∈ USPGraph )
grlimgrtri.h ⊢ ( 𝜑 → 𝐻 ∈ USPGraph )
grlimgrtri.n ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) )
grlimgrtri.t ⊢ ( 𝜑 → 𝑇 ∈ ( GrTriangles ‘ 𝐺 ) )
Assertion grlimgrtri ( 𝜑 → ∃ 𝑡 𝑡 ∈ ( GrTriangles ‘ 𝐻 ) )

Proof

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