Metamath Proof Explorer

Theorem grimidvtxedg

Description: The identity relation restricted to the set of vertices of a graph is a graph isomorphism between the graph and a graph with the same vertices and edges. (Contributed by AV, 4-May-2025)

Ref Expression
Hypotheses grimidvtxsdg.g ⊢ ( 𝜑 → 𝐺 ∈ UHGraph )
grimidvtxsdg.h ⊢ ( 𝜑 → 𝐻 ∈ 𝑉 )
grimidvtxsdg.v ⊢ ( 𝜑 → ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐻 ) )
grimidvtxsdg.e ⊢ ( 𝜑 → ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐻 ) )
Assertion grimidvtxedg ( 𝜑 → ( I ↾ ( Vtx ‘ 𝐺 ) ) ∈ ( 𝐺 GraphIso 𝐻 ) )

Proof

Step Hyp Ref Expression
1 grimidvtxsdg.g ⊢ ( 𝜑 → 𝐺 ∈ UHGraph )
2 grimidvtxsdg.h ⊢ ( 𝜑 → 𝐻 ∈ 𝑉 )
3 grimidvtxsdg.v ⊢ ( 𝜑 → ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐻 ) )
4 grimidvtxsdg.e ⊢ ( 𝜑 → ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐻 ) )
5 f1oi ⊢ ( I ↾ ( Vtx ‘ 𝐺 ) ) : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐺 )
6 3 f1oeq3d ⊢ ( 𝜑 → ( ( I ↾ ( Vtx ‘ 𝐺 ) ) : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐺 ) ↔ ( I ↾ ( Vtx ‘ 𝐺 ) ) : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) ) )
7 5 6 mpbii ⊢ ( 𝜑 → ( I ↾ ( Vtx ‘ 𝐺 ) ) : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) )
8 funi ⊢ Fun I
9 fvex ⊢ ( iEdg ‘ 𝐺 ) ∈ V
10 9 dmex ⊢ dom ( iEdg ‘ 𝐺 ) ∈ V
11 resfunexg ⊢ ( ( Fun I ∧ dom ( iEdg ‘ 𝐺 ) ∈ V ) → ( I ↾ dom ( iEdg ‘ 𝐺 ) ) ∈ V )
12 8 10 11 mp2an ⊢ ( I ↾ dom ( iEdg ‘ 𝐺 ) ) ∈ V
13 12 a1i ⊢ ( 𝜑 → ( I ↾ dom ( iEdg ‘ 𝐺 ) ) ∈ V )
14 f1oi ⊢ ( I ↾ dom ( iEdg ‘ 𝐺 ) ) : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐺 )
15 4 dmeqd ⊢ ( 𝜑 → dom ( iEdg ‘ 𝐺 ) = dom ( iEdg ‘ 𝐻 ) )
16 15 f1oeq3d ⊢ ( 𝜑 → ( ( I ↾ dom ( iEdg ‘ 𝐺 ) ) : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐺 ) ↔ ( I ↾ dom ( iEdg ‘ 𝐺 ) ) : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) )
17 14 16 mpbii ⊢ ( 𝜑 → ( I ↾ dom ( iEdg ‘ 𝐺 ) ) : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) )
18 fvresi ⊢ ( 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) → ( ( I ↾ dom ( iEdg ‘ 𝐺 ) ) ‘ 𝑖 ) = 𝑖 )
19 18 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ) → ( ( I ↾ dom ( iEdg ‘ 𝐺 ) ) ‘ 𝑖 ) = 𝑖 )
20 19 fveq2d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ) → ( ( iEdg ‘ 𝐺 ) ‘ ( ( I ↾ dom ( iEdg ‘ 𝐺 ) ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) )
21 4 eqcomd ⊢ ( 𝜑 → ( iEdg ‘ 𝐻 ) = ( iEdg ‘ 𝐺 ) )
22 21 fveq1d ⊢ ( 𝜑 → ( ( iEdg ‘ 𝐻 ) ‘ ( ( I ↾ dom ( iEdg ‘ 𝐺 ) ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐺 ) ‘ ( ( I ↾ dom ( iEdg ‘ 𝐺 ) ) ‘ 𝑖 ) ) )
23 22 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ) → ( ( iEdg ‘ 𝐻 ) ‘ ( ( I ↾ dom ( iEdg ‘ 𝐺 ) ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐺 ) ‘ ( ( I ↾ dom ( iEdg ‘ 𝐺 ) ) ‘ 𝑖 ) ) )
24 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
25 eqid ⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
26 24 25 uhgrss ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ) → ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ ( Vtx ‘ 𝐺 ) )
27 1 26 sylan ⊢ ( ( 𝜑 ∧ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ) → ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ ( Vtx ‘ 𝐺 ) )
28 resiima ⊢ ( ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ ( Vtx ‘ 𝐺 ) → ( ( I ↾ ( Vtx ‘ 𝐺 ) ) “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) )
29 27 28 syl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ) → ( ( I ↾ ( Vtx ‘ 𝐺 ) ) “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) )
30 20 23 29 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ) → ( ( iEdg ‘ 𝐻 ) ‘ ( ( I ↾ dom ( iEdg ‘ 𝐺 ) ) ‘ 𝑖 ) ) = ( ( I ↾ ( Vtx ‘ 𝐺 ) ) “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) )
31 30 ralrimiva ⊢ ( 𝜑 → ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( ( I ↾ dom ( iEdg ‘ 𝐺 ) ) ‘ 𝑖 ) ) = ( ( I ↾ ( Vtx ‘ 𝐺 ) ) “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) )
32 17 31 jca ⊢ ( 𝜑 → ( ( I ↾ dom ( iEdg ‘ 𝐺 ) ) : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( ( I ↾ dom ( iEdg ‘ 𝐺 ) ) ‘ 𝑖 ) ) = ( ( I ↾ ( Vtx ‘ 𝐺 ) ) “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) )
33 f1oeq1 ⊢ ( 𝑗 = ( I ↾ dom ( iEdg ‘ 𝐺 ) ) → ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ↔ ( I ↾ dom ( iEdg ‘ 𝐺 ) ) : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) )
34 fveq1 ⊢ ( 𝑗 = ( I ↾ dom ( iEdg ‘ 𝐺 ) ) → ( 𝑗 ‘ 𝑖 ) = ( ( I ↾ dom ( iEdg ‘ 𝐺 ) ) ‘ 𝑖 ) )
35 34 fveqeq2d ⊢ ( 𝑗 = ( I ↾ dom ( iEdg ‘ 𝐺 ) ) → ( ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( ( I ↾ ( Vtx ‘ 𝐺 ) ) “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ↔ ( ( iEdg ‘ 𝐻 ) ‘ ( ( I ↾ dom ( iEdg ‘ 𝐺 ) ) ‘ 𝑖 ) ) = ( ( I ↾ ( Vtx ‘ 𝐺 ) ) “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) )
36 35 ralbidv ⊢ ( 𝑗 = ( I ↾ dom ( iEdg ‘ 𝐺 ) ) → ( ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( ( I ↾ ( Vtx ‘ 𝐺 ) ) “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ↔ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( ( I ↾ dom ( iEdg ‘ 𝐺 ) ) ‘ 𝑖 ) ) = ( ( I ↾ ( Vtx ‘ 𝐺 ) ) “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) )
37 33 36 anbi12d ⊢ ( 𝑗 = ( I ↾ dom ( iEdg ‘ 𝐺 ) ) → ( ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( ( I ↾ ( Vtx ‘ 𝐺 ) ) “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ↔ ( ( I ↾ dom ( iEdg ‘ 𝐺 ) ) : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( ( I ↾ dom ( iEdg ‘ 𝐺 ) ) ‘ 𝑖 ) ) = ( ( I ↾ ( Vtx ‘ 𝐺 ) ) “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) )
38 13 32 37 spcedv ⊢ ( 𝜑 → ∃ 𝑗 ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( ( I ↾ ( Vtx ‘ 𝐺 ) ) “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) )
39 fvex ⊢ ( Vtx ‘ 𝐺 ) ∈ V
40 resfunexg ⊢ ( ( Fun I ∧ ( Vtx ‘ 𝐺 ) ∈ V ) → ( I ↾ ( Vtx ‘ 𝐺 ) ) ∈ V )
41 8 39 40 mp2an ⊢ ( I ↾ ( Vtx ‘ 𝐺 ) ) ∈ V
42 41 a1i ⊢ ( 𝜑 → ( I ↾ ( Vtx ‘ 𝐺 ) ) ∈ V )
43 eqid ⊢ ( Vtx ‘ 𝐻 ) = ( Vtx ‘ 𝐻 )
44 eqid ⊢ ( iEdg ‘ 𝐻 ) = ( iEdg ‘ 𝐻 )
45 24 43 25 44 isgrim ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ 𝑉 ∧ ( I ↾ ( Vtx ‘ 𝐺 ) ) ∈ V ) → ( ( I ↾ ( Vtx ‘ 𝐺 ) ) ∈ ( 𝐺 GraphIso 𝐻 ) ↔ ( ( I ↾ ( Vtx ‘ 𝐺 ) ) : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ∃ 𝑗 ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( ( I ↾ ( Vtx ‘ 𝐺 ) ) “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ) )
46 1 2 42 45 syl3anc ⊢ ( 𝜑 → ( ( I ↾ ( Vtx ‘ 𝐺 ) ) ∈ ( 𝐺 GraphIso 𝐻 ) ↔ ( ( I ↾ ( Vtx ‘ 𝐺 ) ) : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ∃ 𝑗 ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( ( I ↾ ( Vtx ‘ 𝐺 ) ) “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ) )
47 7 38 46 mpbir2and ⊢ ( 𝜑 → ( I ↾ ( Vtx ‘ 𝐺 ) ) ∈ ( 𝐺 GraphIso 𝐻 ) )