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

Metamath Proof Explorer

Theorem clnbgrgrim

Description: Graph isomorphisms between hypergraphs map closed neighborhoods onto closed neighborhoods. (Contributed by AV, 2-Jun-2025)

Ref Expression
Hypothesis clnbgrgrim.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion clnbgrgrim ( ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ) ∧ 𝑋 ∈ 𝑉 ) → ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑋 ) ) = ( 𝐹 “ ( 𝐺 ClNeighbVtx 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 clnbgrgrim.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 fveqeq2 ⊢ ( 𝑛 = 𝑋 → ( ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑋 ) ↔ ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑋 ) ) )
3 1 clnbgrvtxel ⊢ ( 𝑋 ∈ 𝑉 → 𝑋 ∈ ( 𝐺 ClNeighbVtx 𝑋 ) )
4 3 3ad2ant3 ⊢ ( ( 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝑋 ∈ 𝑉 ) → 𝑋 ∈ ( 𝐺 ClNeighbVtx 𝑋 ) )
5 eqidd ⊢ ( ( 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝑋 ∈ 𝑉 ) → ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑋 ) )
6 2 4 5 rspcedvdw ⊢ ( ( 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝑋 ∈ 𝑉 ) → ∃ 𝑛 ∈ ( 𝐺 ClNeighbVtx 𝑋 ) ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑋 ) )
7 6 adantr ⊢ ( ( ( 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑥 ∈ ( Vtx ‘ 𝐻 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ ( Vtx ‘ 𝐻 ) ) ) → ∃ 𝑛 ∈ ( 𝐺 ClNeighbVtx 𝑋 ) ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑋 ) )
8 eqeq2 ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑋 ) → ( ( 𝐹 ‘ 𝑛 ) = 𝑥 ↔ ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑋 ) ) )
9 8 rexbidv ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑋 ) → ( ∃ 𝑛 ∈ ( 𝐺 ClNeighbVtx 𝑋 ) ( 𝐹 ‘ 𝑛 ) = 𝑥 ↔ ∃ 𝑛 ∈ ( 𝐺 ClNeighbVtx 𝑋 ) ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑋 ) ) )
10 7 9 syl5ibrcom ⊢ ( ( ( 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑥 ∈ ( Vtx ‘ 𝐻 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ ( Vtx ‘ 𝐻 ) ) ) → ( 𝑥 = ( 𝐹 ‘ 𝑋 ) → ∃ 𝑛 ∈ ( 𝐺 ClNeighbVtx 𝑋 ) ( 𝐹 ‘ 𝑛 ) = 𝑥 ) )
11 simpl2 ⊢ ( ( ( 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑥 ∈ ( Vtx ‘ 𝐻 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ ( Vtx ‘ 𝐻 ) ) ) → ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) )
12 simpl1 ⊢ ( ( ( 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑥 ∈ ( Vtx ‘ 𝐻 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ ( Vtx ‘ 𝐻 ) ) ) → 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) )
13 simp3 ⊢ ( ( 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝑋 ∈ 𝑉 ) → 𝑋 ∈ 𝑉 )
14 simpl ⊢ ( ( 𝑥 ∈ ( Vtx ‘ 𝐻 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ ( Vtx ‘ 𝐻 ) ) → 𝑥 ∈ ( Vtx ‘ 𝐻 ) )
15 13 14 anim12i ⊢ ( ( ( 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑥 ∈ ( Vtx ‘ 𝐻 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ ( Vtx ‘ 𝐻 ) ) ) → ( 𝑋 ∈ 𝑉 ∧ 𝑥 ∈ ( Vtx ‘ 𝐻 ) ) )
16 eqid ⊢ ( Vtx ‘ 𝐻 ) = ( Vtx ‘ 𝐻 )
17 eqid ⊢ ( Edg ‘ 𝐻 ) = ( Edg ‘ 𝐻 )
18 1 16 17 clnbgrgrimlem ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑥 ∈ ( Vtx ‘ 𝐻 ) ) ) → ( ( 𝑒 ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑋 ) , 𝑥 } ⊆ 𝑒 ) → ∃ 𝑛 ∈ ( 𝐺 ClNeighbVtx 𝑋 ) ( 𝐹 ‘ 𝑛 ) = 𝑥 ) )
19 11 12 15 18 syl3anc ⊢ ( ( ( 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑥 ∈ ( Vtx ‘ 𝐻 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ ( Vtx ‘ 𝐻 ) ) ) → ( ( 𝑒 ∈ ( Edg ‘ 𝐻 ) ∧ { ( 𝐹 ‘ 𝑋 ) , 𝑥 } ⊆ 𝑒 ) → ∃ 𝑛 ∈ ( 𝐺 ClNeighbVtx 𝑋 ) ( 𝐹 ‘ 𝑛 ) = 𝑥 ) )
20 19 expd ⊢ ( ( ( 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑥 ∈ ( Vtx ‘ 𝐻 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ ( Vtx ‘ 𝐻 ) ) ) → ( 𝑒 ∈ ( Edg ‘ 𝐻 ) → ( { ( 𝐹 ‘ 𝑋 ) , 𝑥 } ⊆ 𝑒 → ∃ 𝑛 ∈ ( 𝐺 ClNeighbVtx 𝑋 ) ( 𝐹 ‘ 𝑛 ) = 𝑥 ) ) )
21 20 rexlimdv ⊢ ( ( ( 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑥 ∈ ( Vtx ‘ 𝐻 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ ( Vtx ‘ 𝐻 ) ) ) → ( ∃ 𝑒 ∈ ( Edg ‘ 𝐻 ) { ( 𝐹 ‘ 𝑋 ) , 𝑥 } ⊆ 𝑒 → ∃ 𝑛 ∈ ( 𝐺 ClNeighbVtx 𝑋 ) ( 𝐹 ‘ 𝑛 ) = 𝑥 ) )
22 10 21 jaod ⊢ ( ( ( 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑥 ∈ ( Vtx ‘ 𝐻 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ ( Vtx ‘ 𝐻 ) ) ) → ( ( 𝑥 = ( 𝐹 ‘ 𝑋 ) ∨ ∃ 𝑒 ∈ ( Edg ‘ 𝐻 ) { ( 𝐹 ‘ 𝑋 ) , 𝑥 } ⊆ 𝑒 ) → ∃ 𝑛 ∈ ( 𝐺 ClNeighbVtx 𝑋 ) ( 𝐹 ‘ 𝑛 ) = 𝑥 ) )
23 22 expimpd ⊢ ( ( 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝑋 ∈ 𝑉 ) → ( ( ( 𝑥 ∈ ( Vtx ‘ 𝐻 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ ( Vtx ‘ 𝐻 ) ) ∧ ( 𝑥 = ( 𝐹 ‘ 𝑋 ) ∨ ∃ 𝑒 ∈ ( Edg ‘ 𝐻 ) { ( 𝐹 ‘ 𝑋 ) , 𝑥 } ⊆ 𝑒 ) ) → ∃ 𝑛 ∈ ( 𝐺 ClNeighbVtx 𝑋 ) ( 𝐹 ‘ 𝑛 ) = 𝑥 ) )
24 eqid ⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
25 eqid ⊢ ( iEdg ‘ 𝐻 ) = ( iEdg ‘ 𝐻 )
26 1 16 24 25 grimprop ⊢ ( 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) → ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) )
27 f1of ⊢ ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) → 𝐹 : 𝑉 ⟶ ( Vtx ‘ 𝐻 ) )
28 27 adantr ⊢ ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) → 𝐹 : 𝑉 ⟶ ( Vtx ‘ 𝐻 ) )
29 28 3ad2ant1 ⊢ ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝑋 ∈ 𝑉 ) → 𝐹 : 𝑉 ⟶ ( Vtx ‘ 𝐻 ) )
30 29 ad2antrr ⊢ ( ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑛 ∈ ( 𝐺 ClNeighbVtx 𝑋 ) ) ∧ ( 𝐹 ‘ 𝑛 ) = 𝑥 ) → 𝐹 : 𝑉 ⟶ ( Vtx ‘ 𝐻 ) )
31 1 clnbgrisvtx ⊢ ( 𝑛 ∈ ( 𝐺 ClNeighbVtx 𝑋 ) → 𝑛 ∈ 𝑉 )
32 31 adantl ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑛 ∈ ( 𝐺 ClNeighbVtx 𝑋 ) ) → 𝑛 ∈ 𝑉 )
33 32 adantr ⊢ ( ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑛 ∈ ( 𝐺 ClNeighbVtx 𝑋 ) ) ∧ ( 𝐹 ‘ 𝑛 ) = 𝑥 ) → 𝑛 ∈ 𝑉 )
34 30 33 ffvelcdmd ⊢ ( ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑛 ∈ ( 𝐺 ClNeighbVtx 𝑋 ) ) ∧ ( 𝐹 ‘ 𝑛 ) = 𝑥 ) → ( 𝐹 ‘ 𝑛 ) ∈ ( Vtx ‘ 𝐻 ) )
35 eleq1 ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑛 ) → ( 𝑥 ∈ ( Vtx ‘ 𝐻 ) ↔ ( 𝐹 ‘ 𝑛 ) ∈ ( Vtx ‘ 𝐻 ) ) )
36 35 eqcoms ⊢ ( ( 𝐹 ‘ 𝑛 ) = 𝑥 → ( 𝑥 ∈ ( Vtx ‘ 𝐻 ) ↔ ( 𝐹 ‘ 𝑛 ) ∈ ( Vtx ‘ 𝐻 ) ) )
37 36 adantl ⊢ ( ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑛 ∈ ( 𝐺 ClNeighbVtx 𝑋 ) ) ∧ ( 𝐹 ‘ 𝑛 ) = 𝑥 ) → ( 𝑥 ∈ ( Vtx ‘ 𝐻 ) ↔ ( 𝐹 ‘ 𝑛 ) ∈ ( Vtx ‘ 𝐻 ) ) )
38 34 37 mpbird ⊢ ( ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑛 ∈ ( 𝐺 ClNeighbVtx 𝑋 ) ) ∧ ( 𝐹 ‘ 𝑛 ) = 𝑥 ) → 𝑥 ∈ ( Vtx ‘ 𝐻 ) )
39 simp3 ⊢ ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝑋 ∈ 𝑉 ) → 𝑋 ∈ 𝑉 )
40 29 39 ffvelcdmd ⊢ ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝑋 ∈ 𝑉 ) → ( 𝐹 ‘ 𝑋 ) ∈ ( Vtx ‘ 𝐻 ) )
41 40 ad2antrr ⊢ ( ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑛 ∈ ( 𝐺 ClNeighbVtx 𝑋 ) ) ∧ ( 𝐹 ‘ 𝑛 ) = 𝑥 ) → ( 𝐹 ‘ 𝑋 ) ∈ ( Vtx ‘ 𝐻 ) )
42 eqid ⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
43 1 42 clnbgrel ⊢ ( 𝑛 ∈ ( 𝐺 ClNeighbVtx 𝑋 ) ↔ ( ( 𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑛 = 𝑋 ∨ ∃ 𝑘 ∈ ( Edg ‘ 𝐺 ) { 𝑋 , 𝑛 } ⊆ 𝑘 ) ) )
44 fveq2 ⊢ ( 𝑛 = 𝑋 → ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑋 ) )
45 44 orcd ⊢ ( 𝑛 = 𝑋 → ( ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑋 ) ∨ ∃ 𝑒 ∈ ( Edg ‘ 𝐻 ) { ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑛 ) } ⊆ 𝑒 ) )
46 45 2a1d ⊢ ( 𝑛 = 𝑋 → ( ( 𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) → ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝑋 ∈ 𝑉 ) → ( ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑋 ) ∨ ∃ 𝑒 ∈ ( Edg ‘ 𝐻 ) { ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑛 ) } ⊆ 𝑒 ) ) ) )
47 24 uhgredgiedgb ⊢ ( 𝐺 ∈ UHGraph → ( 𝑘 ∈ ( Edg ‘ 𝐺 ) ↔ ∃ 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) 𝑘 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ) )
48 47 adantr ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) → ( 𝑘 ∈ ( Edg ‘ 𝐺 ) ↔ ∃ 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) 𝑘 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ) )
49 48 3ad2ant2 ⊢ ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝑋 ∈ 𝑉 ) → ( 𝑘 ∈ ( Edg ‘ 𝐺 ) ↔ ∃ 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) 𝑘 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ) )
50 49 biimpa ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑘 ∈ ( Edg ‘ 𝐺 ) ) → ∃ 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) 𝑘 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) )
51 2fveq3 ⊢ ( 𝑖 = 𝑗 → ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑗 ) ) )
52 fveq2 ⊢ ( 𝑖 = 𝑗 → ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) = ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) )
53 52 imaeq2d ⊢ ( 𝑖 = 𝑗 → ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ) )
54 51 53 eqeq12d ⊢ ( 𝑖 = 𝑗 → ( ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ↔ ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑗 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ) ) )
55 54 rspcv ⊢ ( 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) → ( ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) → ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑗 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ) ) )
56 55 3ad2ant3 ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ 𝑘 ∈ ( Edg ‘ 𝐺 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ) ∧ 𝑋 ∈ 𝑉 ∧ 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ) → ( ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) → ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑗 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ) ) )
57 sseq2 ⊢ ( 𝑘 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) → ( { 𝑋 , 𝑛 } ⊆ 𝑘 ↔ { 𝑋 , 𝑛 } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ) )
58 57 3ad2ant3 ⊢ ( ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ 𝑘 ∈ ( Edg ‘ 𝐺 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ) ∧ 𝑋 ∈ 𝑉 ∧ 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ) ∧ ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑗 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ) ∧ 𝑘 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ) → ( { 𝑋 , 𝑛 } ⊆ 𝑘 ↔ { 𝑋 , 𝑛 } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ) )
59 sseq2 ⊢ ( 𝑒 = ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑗 ) ) → ( { ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑛 ) } ⊆ 𝑒 ↔ { ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑛 ) } ⊆ ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑗 ) ) ) )
60 25 uhgrfun ⊢ ( 𝐻 ∈ UHGraph → Fun ( iEdg ‘ 𝐻 ) )
61 60 adantl ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) → Fun ( iEdg ‘ 𝐻 ) )
62 61 3ad2ant3 ⊢ ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ 𝑘 ∈ ( Edg ‘ 𝐺 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ) → Fun ( iEdg ‘ 𝐻 ) )
63 f1of ⊢ ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) → 𝑔 : dom ( iEdg ‘ 𝐺 ) ⟶ dom ( iEdg ‘ 𝐻 ) )
64 63 adantl ⊢ ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) → 𝑔 : dom ( iEdg ‘ 𝐺 ) ⟶ dom ( iEdg ‘ 𝐻 ) )
65 64 3ad2ant1 ⊢ ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ 𝑘 ∈ ( Edg ‘ 𝐺 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ) → 𝑔 : dom ( iEdg ‘ 𝐺 ) ⟶ dom ( iEdg ‘ 𝐻 ) )
66 65 ffvelcdmda ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ 𝑘 ∈ ( Edg ‘ 𝐺 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ) ∧ 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ) → ( 𝑔 ‘ 𝑗 ) ∈ dom ( iEdg ‘ 𝐻 ) )
67 25 iedgedg ⊢ ( ( Fun ( iEdg ‘ 𝐻 ) ∧ ( 𝑔 ‘ 𝑗 ) ∈ dom ( iEdg ‘ 𝐻 ) ) → ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑗 ) ) ∈ ( Edg ‘ 𝐻 ) )
68 62 66 67 syl2an2r ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ 𝑘 ∈ ( Edg ‘ 𝐺 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ) ∧ 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ) → ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑗 ) ) ∈ ( Edg ‘ 𝐻 ) )
69 68 3adant2 ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ 𝑘 ∈ ( Edg ‘ 𝐺 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ) ∧ 𝑋 ∈ 𝑉 ∧ 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ) → ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑗 ) ) ∈ ( Edg ‘ 𝐻 ) )
70 69 adantr ⊢ ( ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ 𝑘 ∈ ( Edg ‘ 𝐺 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ) ∧ 𝑋 ∈ 𝑉 ∧ 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ) ∧ ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑗 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ) ) → ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑗 ) ) ∈ ( Edg ‘ 𝐻 ) )
71 70 3ad2ant1 ⊢ ( ( ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ 𝑘 ∈ ( Edg ‘ 𝐺 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ) ∧ 𝑋 ∈ 𝑉 ∧ 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ) ∧ ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑗 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ) ) ∧ { 𝑋 , 𝑛 } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ∧ ( 𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) ) → ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑗 ) ) ∈ ( Edg ‘ 𝐻 ) )
72 f1ofn ⊢ ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) → 𝐹 Fn 𝑉 )
73 72 adantr ⊢ ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) → 𝐹 Fn 𝑉 )
74 73 3ad2ant1 ⊢ ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ 𝑘 ∈ ( Edg ‘ 𝐺 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ) → 𝐹 Fn 𝑉 )
75 74 3ad2ant1 ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ 𝑘 ∈ ( Edg ‘ 𝐺 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ) ∧ 𝑋 ∈ 𝑉 ∧ 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ) → 𝐹 Fn 𝑉 )
76 75 adantr ⊢ ( ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ 𝑘 ∈ ( Edg ‘ 𝐺 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ) ∧ 𝑋 ∈ 𝑉 ∧ 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ) ∧ ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑗 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ) ) → 𝐹 Fn 𝑉 )
77 pm3.22 ⊢ ( ( 𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) → ( 𝑋 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) )
78 76 77 anim12i ⊢ ( ( ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ 𝑘 ∈ ( Edg ‘ 𝐺 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ) ∧ 𝑋 ∈ 𝑉 ∧ 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ) ∧ ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑗 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ) ) ∧ ( 𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) ) → ( 𝐹 Fn 𝑉 ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) ) )
79 78 3adant2 ⊢ ( ( ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ 𝑘 ∈ ( Edg ‘ 𝐺 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ) ∧ 𝑋 ∈ 𝑉 ∧ 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ) ∧ ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑗 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ) ) ∧ { 𝑋 , 𝑛 } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ∧ ( 𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) ) → ( 𝐹 Fn 𝑉 ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) ) )
80 3anass ⊢ ( ( 𝐹 Fn 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) ↔ ( 𝐹 Fn 𝑉 ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) ) )
81 79 80 sylibr ⊢ ( ( ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ 𝑘 ∈ ( Edg ‘ 𝐺 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ) ∧ 𝑋 ∈ 𝑉 ∧ 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ) ∧ ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑗 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ) ) ∧ { 𝑋 , 𝑛 } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ∧ ( 𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) ) → ( 𝐹 Fn 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) )
82 fnimapr ⊢ ( ( 𝐹 Fn 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) → ( 𝐹 “ { 𝑋 , 𝑛 } ) = { ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑛 ) } )
83 81 82 syl ⊢ ( ( ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ 𝑘 ∈ ( Edg ‘ 𝐺 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ) ∧ 𝑋 ∈ 𝑉 ∧ 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ) ∧ ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑗 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ) ) ∧ { 𝑋 , 𝑛 } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ∧ ( 𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) ) → ( 𝐹 “ { 𝑋 , 𝑛 } ) = { ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑛 ) } )
84 imass2 ⊢ ( { 𝑋 , 𝑛 } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) → ( 𝐹 “ { 𝑋 , 𝑛 } ) ⊆ ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ) )
85 84 3ad2ant2 ⊢ ( ( ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ 𝑘 ∈ ( Edg ‘ 𝐺 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ) ∧ 𝑋 ∈ 𝑉 ∧ 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ) ∧ ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑗 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ) ) ∧ { 𝑋 , 𝑛 } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ∧ ( 𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) ) → ( 𝐹 “ { 𝑋 , 𝑛 } ) ⊆ ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ) )
86 83 85 eqsstrrd ⊢ ( ( ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ 𝑘 ∈ ( Edg ‘ 𝐺 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ) ∧ 𝑋 ∈ 𝑉 ∧ 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ) ∧ ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑗 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ) ) ∧ { 𝑋 , 𝑛 } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ∧ ( 𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) ) → { ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑛 ) } ⊆ ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ) )
87 simp1r ⊢ ( ( ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ 𝑘 ∈ ( Edg ‘ 𝐺 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ) ∧ 𝑋 ∈ 𝑉 ∧ 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ) ∧ ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑗 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ) ) ∧ { 𝑋 , 𝑛 } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ∧ ( 𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) ) → ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑗 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ) )
88 86 87 sseqtrrd ⊢ ( ( ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ 𝑘 ∈ ( Edg ‘ 𝐺 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ) ∧ 𝑋 ∈ 𝑉 ∧ 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ) ∧ ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑗 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ) ) ∧ { 𝑋 , 𝑛 } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ∧ ( 𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) ) → { ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑛 ) } ⊆ ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑗 ) ) )
89 59 71 88 rspcedvdw ⊢ ( ( ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ 𝑘 ∈ ( Edg ‘ 𝐺 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ) ∧ 𝑋 ∈ 𝑉 ∧ 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ) ∧ ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑗 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ) ) ∧ { 𝑋 , 𝑛 } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ∧ ( 𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) ) → ∃ 𝑒 ∈ ( Edg ‘ 𝐻 ) { ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑛 ) } ⊆ 𝑒 )
90 89 3exp ⊢ ( ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ 𝑘 ∈ ( Edg ‘ 𝐺 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ) ∧ 𝑋 ∈ 𝑉 ∧ 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ) ∧ ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑗 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ) ) → ( { 𝑋 , 𝑛 } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) → ( ( 𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) → ∃ 𝑒 ∈ ( Edg ‘ 𝐻 ) { ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑛 ) } ⊆ 𝑒 ) ) )
91 90 3adant3 ⊢ ( ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ 𝑘 ∈ ( Edg ‘ 𝐺 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ) ∧ 𝑋 ∈ 𝑉 ∧ 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ) ∧ ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑗 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ) ∧ 𝑘 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ) → ( { 𝑋 , 𝑛 } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) → ( ( 𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) → ∃ 𝑒 ∈ ( Edg ‘ 𝐻 ) { ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑛 ) } ⊆ 𝑒 ) ) )
92 58 91 sylbid ⊢ ( ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ 𝑘 ∈ ( Edg ‘ 𝐺 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ) ∧ 𝑋 ∈ 𝑉 ∧ 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ) ∧ ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑗 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ) ∧ 𝑘 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ) → ( { 𝑋 , 𝑛 } ⊆ 𝑘 → ( ( 𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) → ∃ 𝑒 ∈ ( Edg ‘ 𝐻 ) { ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑛 ) } ⊆ 𝑒 ) ) )
93 92 3exp ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ 𝑘 ∈ ( Edg ‘ 𝐺 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ) ∧ 𝑋 ∈ 𝑉 ∧ 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ) → ( ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑗 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ) → ( 𝑘 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) → ( { 𝑋 , 𝑛 } ⊆ 𝑘 → ( ( 𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) → ∃ 𝑒 ∈ ( Edg ‘ 𝐻 ) { ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑛 ) } ⊆ 𝑒 ) ) ) ) )
94 56 93 syld ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ 𝑘 ∈ ( Edg ‘ 𝐺 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ) ∧ 𝑋 ∈ 𝑉 ∧ 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ) → ( ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) → ( 𝑘 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) → ( { 𝑋 , 𝑛 } ⊆ 𝑘 → ( ( 𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) → ∃ 𝑒 ∈ ( Edg ‘ 𝐻 ) { ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑛 ) } ⊆ 𝑒 ) ) ) ) )
95 94 3exp ⊢ ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ 𝑘 ∈ ( Edg ‘ 𝐺 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ) → ( 𝑋 ∈ 𝑉 → ( 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) → ( ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) → ( 𝑘 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) → ( { 𝑋 , 𝑛 } ⊆ 𝑘 → ( ( 𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) → ∃ 𝑒 ∈ ( Edg ‘ 𝐻 ) { ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑛 ) } ⊆ 𝑒 ) ) ) ) ) ) )
96 95 com34 ⊢ ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ 𝑘 ∈ ( Edg ‘ 𝐺 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ) → ( 𝑋 ∈ 𝑉 → ( ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) → ( 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) → ( 𝑘 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) → ( { 𝑋 , 𝑛 } ⊆ 𝑘 → ( ( 𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) → ∃ 𝑒 ∈ ( Edg ‘ 𝐻 ) { ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑛 ) } ⊆ 𝑒 ) ) ) ) ) ) )
97 96 3exp ⊢ ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) → ( 𝑘 ∈ ( Edg ‘ 𝐺 ) → ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) → ( 𝑋 ∈ 𝑉 → ( ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) → ( 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) → ( 𝑘 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) → ( { 𝑋 , 𝑛 } ⊆ 𝑘 → ( ( 𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) → ∃ 𝑒 ∈ ( Edg ‘ 𝐻 ) { ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑛 ) } ⊆ 𝑒 ) ) ) ) ) ) ) ) )
98 97 com25 ⊢ ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) → ( ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) → ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) → ( 𝑋 ∈ 𝑉 → ( 𝑘 ∈ ( Edg ‘ 𝐺 ) → ( 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) → ( 𝑘 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) → ( { 𝑋 , 𝑛 } ⊆ 𝑘 → ( ( 𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) → ∃ 𝑒 ∈ ( Edg ‘ 𝐻 ) { ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑛 ) } ⊆ 𝑒 ) ) ) ) ) ) ) ) )
99 98 expimpd ⊢ ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) → ( ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) → ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) → ( 𝑋 ∈ 𝑉 → ( 𝑘 ∈ ( Edg ‘ 𝐺 ) → ( 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) → ( 𝑘 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) → ( { 𝑋 , 𝑛 } ⊆ 𝑘 → ( ( 𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) → ∃ 𝑒 ∈ ( Edg ‘ 𝐻 ) { ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑛 ) } ⊆ 𝑒 ) ) ) ) ) ) ) ) )
100 99 exlimdv ⊢ ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) → ( ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) → ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) → ( 𝑋 ∈ 𝑉 → ( 𝑘 ∈ ( Edg ‘ 𝐺 ) → ( 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) → ( 𝑘 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) → ( { 𝑋 , 𝑛 } ⊆ 𝑘 → ( ( 𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) → ∃ 𝑒 ∈ ( Edg ‘ 𝐻 ) { ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑛 ) } ⊆ 𝑒 ) ) ) ) ) ) ) ) )
101 100 imp ⊢ ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) → ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) → ( 𝑋 ∈ 𝑉 → ( 𝑘 ∈ ( Edg ‘ 𝐺 ) → ( 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) → ( 𝑘 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) → ( { 𝑋 , 𝑛 } ⊆ 𝑘 → ( ( 𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) → ∃ 𝑒 ∈ ( Edg ‘ 𝐻 ) { ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑛 ) } ⊆ 𝑒 ) ) ) ) ) ) ) )
102 101 3imp ⊢ ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝑋 ∈ 𝑉 ) → ( 𝑘 ∈ ( Edg ‘ 𝐺 ) → ( 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) → ( 𝑘 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) → ( { 𝑋 , 𝑛 } ⊆ 𝑘 → ( ( 𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) → ∃ 𝑒 ∈ ( Edg ‘ 𝐻 ) { ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑛 ) } ⊆ 𝑒 ) ) ) ) ) )
103 102 imp31 ⊢ ( ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑘 ∈ ( Edg ‘ 𝐺 ) ) ∧ 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ) → ( 𝑘 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) → ( { 𝑋 , 𝑛 } ⊆ 𝑘 → ( ( 𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) → ∃ 𝑒 ∈ ( Edg ‘ 𝐻 ) { ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑛 ) } ⊆ 𝑒 ) ) ) )
104 103 rexlimdva ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑘 ∈ ( Edg ‘ 𝐺 ) ) → ( ∃ 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) 𝑘 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) → ( { 𝑋 , 𝑛 } ⊆ 𝑘 → ( ( 𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) → ∃ 𝑒 ∈ ( Edg ‘ 𝐻 ) { ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑛 ) } ⊆ 𝑒 ) ) ) )
105 50 104 mpd ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑘 ∈ ( Edg ‘ 𝐺 ) ) → ( { 𝑋 , 𝑛 } ⊆ 𝑘 → ( ( 𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) → ∃ 𝑒 ∈ ( Edg ‘ 𝐻 ) { ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑛 ) } ⊆ 𝑒 ) ) )
106 105 ex ⊢ ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝑋 ∈ 𝑉 ) → ( 𝑘 ∈ ( Edg ‘ 𝐺 ) → ( { 𝑋 , 𝑛 } ⊆ 𝑘 → ( ( 𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) → ∃ 𝑒 ∈ ( Edg ‘ 𝐻 ) { ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑛 ) } ⊆ 𝑒 ) ) ) )
107 106 com14 ⊢ ( ( 𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) → ( 𝑘 ∈ ( Edg ‘ 𝐺 ) → ( { 𝑋 , 𝑛 } ⊆ 𝑘 → ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝑋 ∈ 𝑉 ) → ∃ 𝑒 ∈ ( Edg ‘ 𝐻 ) { ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑛 ) } ⊆ 𝑒 ) ) ) )
108 107 imp ⊢ ( ( ( 𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑘 ∈ ( Edg ‘ 𝐺 ) ) → ( { 𝑋 , 𝑛 } ⊆ 𝑘 → ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝑋 ∈ 𝑉 ) → ∃ 𝑒 ∈ ( Edg ‘ 𝐻 ) { ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑛 ) } ⊆ 𝑒 ) ) )
109 108 3imp ⊢ ( ( ( ( 𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑘 ∈ ( Edg ‘ 𝐺 ) ) ∧ { 𝑋 , 𝑛 } ⊆ 𝑘 ∧ ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝑋 ∈ 𝑉 ) ) → ∃ 𝑒 ∈ ( Edg ‘ 𝐻 ) { ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑛 ) } ⊆ 𝑒 )
110 109 olcd ⊢ ( ( ( ( 𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑘 ∈ ( Edg ‘ 𝐺 ) ) ∧ { 𝑋 , 𝑛 } ⊆ 𝑘 ∧ ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝑋 ∈ 𝑉 ) ) → ( ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑋 ) ∨ ∃ 𝑒 ∈ ( Edg ‘ 𝐻 ) { ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑛 ) } ⊆ 𝑒 ) )
111 110 3exp ⊢ ( ( ( 𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑘 ∈ ( Edg ‘ 𝐺 ) ) → ( { 𝑋 , 𝑛 } ⊆ 𝑘 → ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝑋 ∈ 𝑉 ) → ( ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑋 ) ∨ ∃ 𝑒 ∈ ( Edg ‘ 𝐻 ) { ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑛 ) } ⊆ 𝑒 ) ) ) )
112 111 rexlimdva ⊢ ( ( 𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) → ( ∃ 𝑘 ∈ ( Edg ‘ 𝐺 ) { 𝑋 , 𝑛 } ⊆ 𝑘 → ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝑋 ∈ 𝑉 ) → ( ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑋 ) ∨ ∃ 𝑒 ∈ ( Edg ‘ 𝐻 ) { ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑛 ) } ⊆ 𝑒 ) ) ) )
113 112 com12 ⊢ ( ∃ 𝑘 ∈ ( Edg ‘ 𝐺 ) { 𝑋 , 𝑛 } ⊆ 𝑘 → ( ( 𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) → ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝑋 ∈ 𝑉 ) → ( ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑋 ) ∨ ∃ 𝑒 ∈ ( Edg ‘ 𝐻 ) { ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑛 ) } ⊆ 𝑒 ) ) ) )
114 46 113 jaoi ⊢ ( ( 𝑛 = 𝑋 ∨ ∃ 𝑘 ∈ ( Edg ‘ 𝐺 ) { 𝑋 , 𝑛 } ⊆ 𝑘 ) → ( ( 𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) → ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝑋 ∈ 𝑉 ) → ( ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑋 ) ∨ ∃ 𝑒 ∈ ( Edg ‘ 𝐻 ) { ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑛 ) } ⊆ 𝑒 ) ) ) )
115 114 impcom ⊢ ( ( ( 𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑛 = 𝑋 ∨ ∃ 𝑘 ∈ ( Edg ‘ 𝐺 ) { 𝑋 , 𝑛 } ⊆ 𝑘 ) ) → ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝑋 ∈ 𝑉 ) → ( ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑋 ) ∨ ∃ 𝑒 ∈ ( Edg ‘ 𝐻 ) { ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑛 ) } ⊆ 𝑒 ) ) )
116 43 115 sylbi ⊢ ( 𝑛 ∈ ( 𝐺 ClNeighbVtx 𝑋 ) → ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝑋 ∈ 𝑉 ) → ( ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑋 ) ∨ ∃ 𝑒 ∈ ( Edg ‘ 𝐻 ) { ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑛 ) } ⊆ 𝑒 ) ) )
117 116 impcom ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑛 ∈ ( 𝐺 ClNeighbVtx 𝑋 ) ) → ( ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑋 ) ∨ ∃ 𝑒 ∈ ( Edg ‘ 𝐻 ) { ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑛 ) } ⊆ 𝑒 ) )
118 117 adantr ⊢ ( ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑛 ∈ ( 𝐺 ClNeighbVtx 𝑋 ) ) ∧ ( 𝐹 ‘ 𝑛 ) = 𝑥 ) → ( ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑋 ) ∨ ∃ 𝑒 ∈ ( Edg ‘ 𝐻 ) { ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑛 ) } ⊆ 𝑒 ) )
119 eqeq1 ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑛 ) → ( 𝑥 = ( 𝐹 ‘ 𝑋 ) ↔ ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑋 ) ) )
120 preq2 ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑛 ) → { ( 𝐹 ‘ 𝑋 ) , 𝑥 } = { ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑛 ) } )
121 120 sseq1d ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑛 ) → ( { ( 𝐹 ‘ 𝑋 ) , 𝑥 } ⊆ 𝑒 ↔ { ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑛 ) } ⊆ 𝑒 ) )
122 121 rexbidv ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑛 ) → ( ∃ 𝑒 ∈ ( Edg ‘ 𝐻 ) { ( 𝐹 ‘ 𝑋 ) , 𝑥 } ⊆ 𝑒 ↔ ∃ 𝑒 ∈ ( Edg ‘ 𝐻 ) { ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑛 ) } ⊆ 𝑒 ) )
123 119 122 orbi12d ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑛 ) → ( ( 𝑥 = ( 𝐹 ‘ 𝑋 ) ∨ ∃ 𝑒 ∈ ( Edg ‘ 𝐻 ) { ( 𝐹 ‘ 𝑋 ) , 𝑥 } ⊆ 𝑒 ) ↔ ( ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑋 ) ∨ ∃ 𝑒 ∈ ( Edg ‘ 𝐻 ) { ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑛 ) } ⊆ 𝑒 ) ) )
124 123 eqcoms ⊢ ( ( 𝐹 ‘ 𝑛 ) = 𝑥 → ( ( 𝑥 = ( 𝐹 ‘ 𝑋 ) ∨ ∃ 𝑒 ∈ ( Edg ‘ 𝐻 ) { ( 𝐹 ‘ 𝑋 ) , 𝑥 } ⊆ 𝑒 ) ↔ ( ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑋 ) ∨ ∃ 𝑒 ∈ ( Edg ‘ 𝐻 ) { ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑛 ) } ⊆ 𝑒 ) ) )
125 124 adantl ⊢ ( ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑛 ∈ ( 𝐺 ClNeighbVtx 𝑋 ) ) ∧ ( 𝐹 ‘ 𝑛 ) = 𝑥 ) → ( ( 𝑥 = ( 𝐹 ‘ 𝑋 ) ∨ ∃ 𝑒 ∈ ( Edg ‘ 𝐻 ) { ( 𝐹 ‘ 𝑋 ) , 𝑥 } ⊆ 𝑒 ) ↔ ( ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑋 ) ∨ ∃ 𝑒 ∈ ( Edg ‘ 𝐻 ) { ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑛 ) } ⊆ 𝑒 ) ) )
126 118 125 mpbird ⊢ ( ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑛 ∈ ( 𝐺 ClNeighbVtx 𝑋 ) ) ∧ ( 𝐹 ‘ 𝑛 ) = 𝑥 ) → ( 𝑥 = ( 𝐹 ‘ 𝑋 ) ∨ ∃ 𝑒 ∈ ( Edg ‘ 𝐻 ) { ( 𝐹 ‘ 𝑋 ) , 𝑥 } ⊆ 𝑒 ) )
127 38 41 126 jca31 ⊢ ( ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑛 ∈ ( 𝐺 ClNeighbVtx 𝑋 ) ) ∧ ( 𝐹 ‘ 𝑛 ) = 𝑥 ) → ( ( 𝑥 ∈ ( Vtx ‘ 𝐻 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ ( Vtx ‘ 𝐻 ) ) ∧ ( 𝑥 = ( 𝐹 ‘ 𝑋 ) ∨ ∃ 𝑒 ∈ ( Edg ‘ 𝐻 ) { ( 𝐹 ‘ 𝑋 ) , 𝑥 } ⊆ 𝑒 ) ) )
128 127 ex ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑛 ∈ ( 𝐺 ClNeighbVtx 𝑋 ) ) → ( ( 𝐹 ‘ 𝑛 ) = 𝑥 → ( ( 𝑥 ∈ ( Vtx ‘ 𝐻 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ ( Vtx ‘ 𝐻 ) ) ∧ ( 𝑥 = ( 𝐹 ‘ 𝑋 ) ∨ ∃ 𝑒 ∈ ( Edg ‘ 𝐻 ) { ( 𝐹 ‘ 𝑋 ) , 𝑥 } ⊆ 𝑒 ) ) ) )
129 128 rexlimdva ⊢ ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝑋 ∈ 𝑉 ) → ( ∃ 𝑛 ∈ ( 𝐺 ClNeighbVtx 𝑋 ) ( 𝐹 ‘ 𝑛 ) = 𝑥 → ( ( 𝑥 ∈ ( Vtx ‘ 𝐻 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ ( Vtx ‘ 𝐻 ) ) ∧ ( 𝑥 = ( 𝐹 ‘ 𝑋 ) ∨ ∃ 𝑒 ∈ ( Edg ‘ 𝐻 ) { ( 𝐹 ‘ 𝑋 ) , 𝑥 } ⊆ 𝑒 ) ) ) )
130 26 129 syl3an1 ⊢ ( ( 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝑋 ∈ 𝑉 ) → ( ∃ 𝑛 ∈ ( 𝐺 ClNeighbVtx 𝑋 ) ( 𝐹 ‘ 𝑛 ) = 𝑥 → ( ( 𝑥 ∈ ( Vtx ‘ 𝐻 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ ( Vtx ‘ 𝐻 ) ) ∧ ( 𝑥 = ( 𝐹 ‘ 𝑋 ) ∨ ∃ 𝑒 ∈ ( Edg ‘ 𝐻 ) { ( 𝐹 ‘ 𝑋 ) , 𝑥 } ⊆ 𝑒 ) ) ) )
131 23 130 impbid ⊢ ( ( 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝑋 ∈ 𝑉 ) → ( ( ( 𝑥 ∈ ( Vtx ‘ 𝐻 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ ( Vtx ‘ 𝐻 ) ) ∧ ( 𝑥 = ( 𝐹 ‘ 𝑋 ) ∨ ∃ 𝑒 ∈ ( Edg ‘ 𝐻 ) { ( 𝐹 ‘ 𝑋 ) , 𝑥 } ⊆ 𝑒 ) ) ↔ ∃ 𝑛 ∈ ( 𝐺 ClNeighbVtx 𝑋 ) ( 𝐹 ‘ 𝑛 ) = 𝑥 ) )
132 131 3exp ⊢ ( 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) → ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) → ( 𝑋 ∈ 𝑉 → ( ( ( 𝑥 ∈ ( Vtx ‘ 𝐻 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ ( Vtx ‘ 𝐻 ) ) ∧ ( 𝑥 = ( 𝐹 ‘ 𝑋 ) ∨ ∃ 𝑒 ∈ ( Edg ‘ 𝐻 ) { ( 𝐹 ‘ 𝑋 ) , 𝑥 } ⊆ 𝑒 ) ) ↔ ∃ 𝑛 ∈ ( 𝐺 ClNeighbVtx 𝑋 ) ( 𝐹 ‘ 𝑛 ) = 𝑥 ) ) ) )
133 132 impcom ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ) → ( 𝑋 ∈ 𝑉 → ( ( ( 𝑥 ∈ ( Vtx ‘ 𝐻 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ ( Vtx ‘ 𝐻 ) ) ∧ ( 𝑥 = ( 𝐹 ‘ 𝑋 ) ∨ ∃ 𝑒 ∈ ( Edg ‘ 𝐻 ) { ( 𝐹 ‘ 𝑋 ) , 𝑥 } ⊆ 𝑒 ) ) ↔ ∃ 𝑛 ∈ ( 𝐺 ClNeighbVtx 𝑋 ) ( 𝐹 ‘ 𝑛 ) = 𝑥 ) ) )
134 133 imp ⊢ ( ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ) ∧ 𝑋 ∈ 𝑉 ) → ( ( ( 𝑥 ∈ ( Vtx ‘ 𝐻 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ ( Vtx ‘ 𝐻 ) ) ∧ ( 𝑥 = ( 𝐹 ‘ 𝑋 ) ∨ ∃ 𝑒 ∈ ( Edg ‘ 𝐻 ) { ( 𝐹 ‘ 𝑋 ) , 𝑥 } ⊆ 𝑒 ) ) ↔ ∃ 𝑛 ∈ ( 𝐺 ClNeighbVtx 𝑋 ) ( 𝐹 ‘ 𝑛 ) = 𝑥 ) )
135 16 17 clnbgrel ⊢ ( 𝑥 ∈ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑋 ) ) ↔ ( ( 𝑥 ∈ ( Vtx ‘ 𝐻 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ ( Vtx ‘ 𝐻 ) ) ∧ ( 𝑥 = ( 𝐹 ‘ 𝑋 ) ∨ ∃ 𝑒 ∈ ( Edg ‘ 𝐻 ) { ( 𝐹 ‘ 𝑋 ) , 𝑥 } ⊆ 𝑒 ) ) )
136 135 a1i ⊢ ( ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ) ∧ 𝑋 ∈ 𝑉 ) → ( 𝑥 ∈ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑋 ) ) ↔ ( ( 𝑥 ∈ ( Vtx ‘ 𝐻 ) ∧ ( 𝐹 ‘ 𝑋 ) ∈ ( Vtx ‘ 𝐻 ) ) ∧ ( 𝑥 = ( 𝐹 ‘ 𝑋 ) ∨ ∃ 𝑒 ∈ ( Edg ‘ 𝐻 ) { ( 𝐹 ‘ 𝑋 ) , 𝑥 } ⊆ 𝑒 ) ) ) )
137 1 16 grimf1o ⊢ ( 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) → 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) )
138 137 72 syl ⊢ ( 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) → 𝐹 Fn 𝑉 )
139 138 adantl ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ) → 𝐹 Fn 𝑉 )
140 1 clnbgrssvtx ⊢ ( 𝐺 ClNeighbVtx 𝑋 ) ⊆ 𝑉
141 140 a1i ⊢ ( 𝑋 ∈ 𝑉 → ( 𝐺 ClNeighbVtx 𝑋 ) ⊆ 𝑉 )
142 fvelimab ⊢ ( ( 𝐹 Fn 𝑉 ∧ ( 𝐺 ClNeighbVtx 𝑋 ) ⊆ 𝑉 ) → ( 𝑥 ∈ ( 𝐹 “ ( 𝐺 ClNeighbVtx 𝑋 ) ) ↔ ∃ 𝑛 ∈ ( 𝐺 ClNeighbVtx 𝑋 ) ( 𝐹 ‘ 𝑛 ) = 𝑥 ) )
143 139 141 142 syl2an ⊢ ( ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ) ∧ 𝑋 ∈ 𝑉 ) → ( 𝑥 ∈ ( 𝐹 “ ( 𝐺 ClNeighbVtx 𝑋 ) ) ↔ ∃ 𝑛 ∈ ( 𝐺 ClNeighbVtx 𝑋 ) ( 𝐹 ‘ 𝑛 ) = 𝑥 ) )
144 134 136 143 3bitr4d ⊢ ( ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ) ∧ 𝑋 ∈ 𝑉 ) → ( 𝑥 ∈ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑋 ) ) ↔ 𝑥 ∈ ( 𝐹 “ ( 𝐺 ClNeighbVtx 𝑋 ) ) ) )
145 144 eqrdv ⊢ ( ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ) ∧ 𝑋 ∈ 𝑉 ) → ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑋 ) ) = ( 𝐹 “ ( 𝐺 ClNeighbVtx 𝑋 ) ) )