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	$⊢ φ \to G \in UHGraph$
	grimidvtxsdg.h	$⊢ φ \to H \in V$
	grimidvtxsdg.v	$⊢ φ \to Vtx (G) = Vtx (H)$
	grimidvtxsdg.e	$⊢ φ \to iEdg (G) = iEdg (H)$
Assertion	grimidvtxedg	$⊢ φ \to {I ↾}_{Vtx (G)} \in (G GraphIso H)$

Proof

Step	Hyp	Ref	Expression
1		grimidvtxsdg.g	$⊢ φ \to G \in UHGraph$
2		grimidvtxsdg.h	$⊢ φ \to H \in V$
3		grimidvtxsdg.v	$⊢ φ \to Vtx (G) = Vtx (H)$
4		grimidvtxsdg.e	$⊢ φ \to iEdg (G) = iEdg (H)$
5		f1oi	$⊢ ({I ↾}_{Vtx (G)}) : Vtx (G) \underset{1-1 onto}{⟶} Vtx (G)$
6	3	f1oeq3d	$⊢ φ \to (({I ↾}_{Vtx (G)}) : Vtx (G) \underset{1-1 onto}{⟶} Vtx (G) \leftrightarrow ({I ↾}_{Vtx (G)}) : Vtx (G) \underset{1-1 onto}{⟶} Vtx (H))$
7	5 6	mpbii	$⊢ φ \to ({I ↾}_{Vtx (G)}) : Vtx (G) \underset{1-1 onto}{⟶} Vtx (H)$
8		funi	$⊢ Fun I$
9		fvex	$⊢ iEdg (G) \in V$
10	9	dmex	$⊢ dom iEdg (G) \in V$
11		resfunexg	$⊢ (Fun I \land dom iEdg (G) \in V) \to {I ↾}_{dom iEdg (G)} \in V$
12	8 10 11	mp2an	$⊢ {I ↾}_{dom iEdg (G)} \in V$
13	12	a1i	$⊢ φ \to {I ↾}_{dom iEdg (G)} \in V$
14		f1oi	$⊢ ({I ↾}_{dom iEdg (G)}) : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (G)$
15	4	dmeqd	$⊢ φ \to dom iEdg (G) = dom iEdg (H)$
16	15	f1oeq3d	$⊢ φ \to (({I ↾}_{dom iEdg (G)}) : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (G) \leftrightarrow ({I ↾}_{dom iEdg (G)}) : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H))$
17	14 16	mpbii	$⊢ φ \to ({I ↾}_{dom iEdg (G)}) : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)$
18		fvresi	$⊢ i \in dom iEdg (G) \to ({I ↾}_{dom iEdg (G)}) (i) = i$
19	18	adantl	$⊢ (φ \land i \in dom iEdg (G)) \to ({I ↾}_{dom iEdg (G)}) (i) = i$
20	19	fveq2d	$⊢ (φ \land i \in dom iEdg (G)) \to iEdg (G) (({I ↾}_{dom iEdg (G)}) (i)) = iEdg (G) (i)$
21	4	eqcomd	$⊢ φ \to iEdg (H) = iEdg (G)$
22	21	fveq1d	$⊢ φ \to iEdg (H) (({I ↾}_{dom iEdg (G)}) (i)) = iEdg (G) (({I ↾}_{dom iEdg (G)}) (i))$
23	22	adantr	$⊢ (φ \land i \in dom iEdg (G)) \to iEdg (H) (({I ↾}_{dom iEdg (G)}) (i)) = iEdg (G) (({I ↾}_{dom iEdg (G)}) (i))$
24		eqid	$⊢ Vtx (G) = Vtx (G)$
25		eqid	$⊢ iEdg (G) = iEdg (G)$
26	24 25	uhgrss	$⊢ (G \in UHGraph \land i \in dom iEdg (G)) \to iEdg (G) (i) \subseteq Vtx (G)$
27	1 26	sylan	$⊢ (φ \land i \in dom iEdg (G)) \to iEdg (G) (i) \subseteq Vtx (G)$
28		resiima	$⊢ iEdg (G) (i) \subseteq Vtx (G) \to ({I ↾}_{Vtx (G)}) [iEdg (G) (i)] = iEdg (G) (i)$
29	27 28	syl	$⊢ (φ \land i \in dom iEdg (G)) \to ({I ↾}_{Vtx (G)}) [iEdg (G) (i)] = iEdg (G) (i)$
30	20 23 29	3eqtr4d	$⊢ (φ \land i \in dom iEdg (G)) \to iEdg (H) (({I ↾}_{dom iEdg (G)}) (i)) = ({I ↾}_{Vtx (G)}) [iEdg (G) (i)]$
31	30	ralrimiva	$⊢ φ \to \forall i \in dom iEdg (G) iEdg (H) (({I ↾}_{dom iEdg (G)}) (i)) = ({I ↾}_{Vtx (G)}) [iEdg (G) (i)]$
32	17 31	jca	$⊢ φ \to (({I ↾}_{dom iEdg (G)}) : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (({I ↾}_{dom iEdg (G)}) (i)) = ({I ↾}_{Vtx (G)}) [iEdg (G) (i)])$
33		f1oeq1	$⊢ j = {I ↾}_{dom iEdg (G)} \to (j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \leftrightarrow ({I ↾}_{dom iEdg (G)}) : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H))$
34		fveq1	$⊢ j = {I ↾}_{dom iEdg (G)} \to j (i) = ({I ↾}_{dom iEdg (G)}) (i)$
35	34	fveqeq2d	$⊢ j = {I ↾}_{dom iEdg (G)} \to (iEdg (H) (j (i)) = ({I ↾}_{Vtx (G)}) [iEdg (G) (i)] \leftrightarrow iEdg (H) (({I ↾}_{dom iEdg (G)}) (i)) = ({I ↾}_{Vtx (G)}) [iEdg (G) (i)])$
36	35	ralbidv	$⊢ j = {I ↾}_{dom iEdg (G)} \to (\forall i \in dom iEdg (G) iEdg (H) (j (i)) = ({I ↾}_{Vtx (G)}) [iEdg (G) (i)] \leftrightarrow \forall i \in dom iEdg (G) iEdg (H) (({I ↾}_{dom iEdg (G)}) (i)) = ({I ↾}_{Vtx (G)}) [iEdg (G) (i)])$
37	33 36	anbi12d	$⊢ j = {I ↾}_{dom iEdg (G)} \to ((j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (j (i)) = ({I ↾}_{Vtx (G)}) [iEdg (G) (i)]) \leftrightarrow (({I ↾}_{dom iEdg (G)}) : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (({I ↾}_{dom iEdg (G)}) (i)) = ({I ↾}_{Vtx (G)}) [iEdg (G) (i)]))$
38	13 32 37	spcedv	$⊢ φ \to \exists j (j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (j (i)) = ({I ↾}_{Vtx (G)}) [iEdg (G) (i)])$
39		fvex	$⊢ Vtx (G) \in V$
40		resfunexg	$⊢ (Fun I \land Vtx (G) \in V) \to {I ↾}_{Vtx (G)} \in V$
41	8 39 40	mp2an	$⊢ {I ↾}_{Vtx (G)} \in V$
42	41	a1i	$⊢ φ \to {I ↾}_{Vtx (G)} \in V$
43		eqid	$⊢ Vtx (H) = Vtx (H)$
44		eqid	$⊢ iEdg (H) = iEdg (H)$
45	24 43 25 44	isgrim	$⊢ (G \in UHGraph \land H \in V \land {I ↾}_{Vtx (G)} \in V) \to ({I ↾}_{Vtx (G)} \in (G GraphIso H) \leftrightarrow (({I ↾}_{Vtx (G)}) : Vtx (G) \underset{1-1 onto}{⟶} Vtx (H) \land \exists j (j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (j (i)) = ({I ↾}_{Vtx (G)}) [iEdg (G) (i)])))$
46	1 2 42 45	syl3anc	$⊢ φ \to ({I ↾}_{Vtx (G)} \in (G GraphIso H) \leftrightarrow (({I ↾}_{Vtx (G)}) : Vtx (G) \underset{1-1 onto}{⟶} Vtx (H) \land \exists j (j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (j (i)) = ({I ↾}_{Vtx (G)}) [iEdg (G) (i)])))$
47	7 38 46	mpbir2and	$⊢ φ \to {I ↾}_{Vtx (G)} \in (G GraphIso H)$

Metamath Proof Explorer

Theorem grimidvtxedg

Proof