isubgrgrim

Description: Isomorphic subgraphs induced by subsets of vertices of two graphs. (Contributed by AV, 29-May-2025)

	Ref	Expression
Hypotheses	isubgrgrim.v	$⊢ V = Vtx (G)$
	isubgrgrim.w	$⊢ W = Vtx (H)$
	isubgrgrim.i	$⊢ I = iEdg (G)$
	isubgrgrim.j	$⊢ J = iEdg (H)$
	isubgrgrim.k	$⊢ K = \{x \in dom I \| I (x) \subseteq N\}$
	isubgrgrim.l	$⊢ L = \{x \in dom J \| J (x) \subseteq M\}$
Assertion	isubgrgrim	$⊢ ((G \in U \land H \in T) \land (N \subseteq V \land M \subseteq W)) \to ((G ISubGr N) ≃_{𝑔𝑟} (H ISubGr M) \leftrightarrow \exists f (f : N \underset{1-1 onto}{⟶} M \land \exists g (g : K \underset{1-1 onto}{⟶} L \land \forall i \in K f [I (i)] = J (g (i)))))$

Proof

Step	Hyp	Ref	Expression
1		isubgrgrim.v	$⊢ V = Vtx (G)$
2		isubgrgrim.w	$⊢ W = Vtx (H)$
3		isubgrgrim.i	$⊢ I = iEdg (G)$
4		isubgrgrim.j	$⊢ J = iEdg (H)$
5		isubgrgrim.k	$⊢ K = \{x \in dom I \| I (x) \subseteq N\}$
6		isubgrgrim.l	$⊢ L = \{x \in dom J \| J (x) \subseteq M\}$
7		ovex	$⊢ G ISubGr N \in V$
8		ovex	$⊢ H ISubGr M \in V$
9	7 8	pm3.2i	$⊢ (G ISubGr N \in V \land H ISubGr M \in V)$
10		eqid	$⊢ Vtx (G ISubGr N) = Vtx (G ISubGr N)$
11		eqid	$⊢ Vtx (H ISubGr M) = Vtx (H ISubGr M)$
12		eqid	$⊢ iEdg (G ISubGr N) = iEdg (G ISubGr N)$
13		eqid	$⊢ iEdg (H ISubGr M) = iEdg (H ISubGr M)$
14	10 11 12 13	dfgric2	$⊢ (G ISubGr N \in V \land H ISubGr M \in V) \to ((G ISubGr N) ≃_{𝑔𝑟} (H ISubGr M) \leftrightarrow \exists f (f : Vtx (G ISubGr N) \underset{1-1 onto}{⟶} Vtx (H ISubGr M) \land \exists g (g : dom iEdg (G ISubGr N) \underset{1-1 onto}{⟶} dom iEdg (H ISubGr M) \land \forall i \in dom iEdg (G ISubGr N) f [iEdg (G ISubGr N) (i)] = iEdg (H ISubGr M) (g (i)))))$
15	9 14	mp1i	$⊢ ((G \in U \land H \in T) \land (N \subseteq V \land M \subseteq W)) \to ((G ISubGr N) ≃_{𝑔𝑟} (H ISubGr M) \leftrightarrow \exists f (f : Vtx (G ISubGr N) \underset{1-1 onto}{⟶} Vtx (H ISubGr M) \land \exists g (g : dom iEdg (G ISubGr N) \underset{1-1 onto}{⟶} dom iEdg (H ISubGr M) \land \forall i \in dom iEdg (G ISubGr N) f [iEdg (G ISubGr N) (i)] = iEdg (H ISubGr M) (g (i)))))$
16		eqidd	$⊢ ((G \in U \land H \in T) \land (N \subseteq V \land M \subseteq W)) \to f = f$
17	1	isubgrvtx	$⊢ (G \in U \land N \subseteq V) \to Vtx (G ISubGr N) = N$
18	17	ad2ant2r	$⊢ ((G \in U \land H \in T) \land (N \subseteq V \land M \subseteq W)) \to Vtx (G ISubGr N) = N$
19	2	isubgrvtx	$⊢ (H \in T \land M \subseteq W) \to Vtx (H ISubGr M) = M$
20	19	ad2ant2l	$⊢ ((G \in U \land H \in T) \land (N \subseteq V \land M \subseteq W)) \to Vtx (H ISubGr M) = M$
21	16 18 20	f1oeq123d	$⊢ ((G \in U \land H \in T) \land (N \subseteq V \land M \subseteq W)) \to (f : Vtx (G ISubGr N) \underset{1-1 onto}{⟶} Vtx (H ISubGr M) \leftrightarrow f : N \underset{1-1 onto}{⟶} M)$
22		eqidd	$⊢ ((G \in U \land H \in T) \land (N \subseteq V \land M \subseteq W)) \to g = g$
23	1 3	isubgriedg	$⊢ (G \in U \land N \subseteq V) \to iEdg (G ISubGr N) = {I ↾}_{\{x \in dom I \| I (x) \subseteq N\}}$
24	23	ad2ant2r	$⊢ ((G \in U \land H \in T) \land (N \subseteq V \land M \subseteq W)) \to iEdg (G ISubGr N) = {I ↾}_{\{x \in dom I \| I (x) \subseteq N\}}$
25	24	dmeqd	$⊢ ((G \in U \land H \in T) \land (N \subseteq V \land M \subseteq W)) \to dom iEdg (G ISubGr N) = dom ({I ↾}_{\{x \in dom I \| I (x) \subseteq N\}})$
26		ssrab2	$⊢ \{x \in dom I \| I (x) \subseteq N\} \subseteq dom I$
27	26	a1i	$⊢ ((G \in U \land H \in T) \land (N \subseteq V \land M \subseteq W)) \to \{x \in dom I \| I (x) \subseteq N\} \subseteq dom I$
28		ssdmres	$⊢ \{x \in dom I \| I (x) \subseteq N\} \subseteq dom I \leftrightarrow dom ({I ↾}_{\{x \in dom I \| I (x) \subseteq N\}}) = \{x \in dom I \| I (x) \subseteq N\}$
29	27 28	sylib	$⊢ ((G \in U \land H \in T) \land (N \subseteq V \land M \subseteq W)) \to dom ({I ↾}_{\{x \in dom I \| I (x) \subseteq N\}}) = \{x \in dom I \| I (x) \subseteq N\}$
30	5	eqcomi	$⊢ \{x \in dom I \| I (x) \subseteq N\} = K$
31	30	a1i	$⊢ ((G \in U \land H \in T) \land (N \subseteq V \land M \subseteq W)) \to \{x \in dom I \| I (x) \subseteq N\} = K$
32	25 29 31	3eqtrd	$⊢ ((G \in U \land H \in T) \land (N \subseteq V \land M \subseteq W)) \to dom iEdg (G ISubGr N) = K$
33	2 4	isubgriedg	$⊢ (H \in T \land M \subseteq W) \to iEdg (H ISubGr M) = {J ↾}_{\{x \in dom J \| J (x) \subseteq M\}}$
34	33	ad2ant2l	$⊢ ((G \in U \land H \in T) \land (N \subseteq V \land M \subseteq W)) \to iEdg (H ISubGr M) = {J ↾}_{\{x \in dom J \| J (x) \subseteq M\}}$
35	34	dmeqd	$⊢ ((G \in U \land H \in T) \land (N \subseteq V \land M \subseteq W)) \to dom iEdg (H ISubGr M) = dom ({J ↾}_{\{x \in dom J \| J (x) \subseteq M\}})$
36		ssrab2	$⊢ \{x \in dom J \| J (x) \subseteq M\} \subseteq dom J$
37	36	a1i	$⊢ ((G \in U \land H \in T) \land (N \subseteq V \land M \subseteq W)) \to \{x \in dom J \| J (x) \subseteq M\} \subseteq dom J$
38		ssdmres	$⊢ \{x \in dom J \| J (x) \subseteq M\} \subseteq dom J \leftrightarrow dom ({J ↾}_{\{x \in dom J \| J (x) \subseteq M\}}) = \{x \in dom J \| J (x) \subseteq M\}$
39	37 38	sylib	$⊢ ((G \in U \land H \in T) \land (N \subseteq V \land M \subseteq W)) \to dom ({J ↾}_{\{x \in dom J \| J (x) \subseteq M\}}) = \{x \in dom J \| J (x) \subseteq M\}$
40	6	eqcomi	$⊢ \{x \in dom J \| J (x) \subseteq M\} = L$
41	40	a1i	$⊢ ((G \in U \land H \in T) \land (N \subseteq V \land M \subseteq W)) \to \{x \in dom J \| J (x) \subseteq M\} = L$
42	35 39 41	3eqtrd	$⊢ ((G \in U \land H \in T) \land (N \subseteq V \land M \subseteq W)) \to dom iEdg (H ISubGr M) = L$
43	22 32 42	f1oeq123d	$⊢ ((G \in U \land H \in T) \land (N \subseteq V \land M \subseteq W)) \to (g : dom iEdg (G ISubGr N) \underset{1-1 onto}{⟶} dom iEdg (H ISubGr M) \leftrightarrow g : K \underset{1-1 onto}{⟶} L)$
44	43	anbi1d	$⊢ ((G \in U \land H \in T) \land (N \subseteq V \land M \subseteq W)) \to ((g : dom iEdg (G ISubGr N) \underset{1-1 onto}{⟶} dom iEdg (H ISubGr M) \land \forall i \in dom iEdg (G ISubGr N) f [iEdg (G ISubGr N) (i)] = iEdg (H ISubGr M) (g (i))) \leftrightarrow (g : K \underset{1-1 onto}{⟶} L \land \forall i \in dom iEdg (G ISubGr N) f [iEdg (G ISubGr N) (i)] = iEdg (H ISubGr M) (g (i))))$
45	31	reseq2d	$⊢ ((G \in U \land H \in T) \land (N \subseteq V \land M \subseteq W)) \to {I ↾}_{\{x \in dom I \| I (x) \subseteq N\}} = {I ↾}_{K}$
46	24 45	eqtrd	$⊢ ((G \in U \land H \in T) \land (N \subseteq V \land M \subseteq W)) \to iEdg (G ISubGr N) = {I ↾}_{K}$
47	46	fveq1d	$⊢ ((G \in U \land H \in T) \land (N \subseteq V \land M \subseteq W)) \to iEdg (G ISubGr N) (i) = ({I ↾}_{K}) (i)$
48	47	imaeq2d	$⊢ ((G \in U \land H \in T) \land (N \subseteq V \land M \subseteq W)) \to f [iEdg (G ISubGr N) (i)] = f [({I ↾}_{K}) (i)]$
49	40	reseq2i	$⊢ {J ↾}_{\{x \in dom J \| J (x) \subseteq M\}} = {J ↾}_{L}$
50	34 49	eqtrdi	$⊢ ((G \in U \land H \in T) \land (N \subseteq V \land M \subseteq W)) \to iEdg (H ISubGr M) = {J ↾}_{L}$
51	50	fveq1d	$⊢ ((G \in U \land H \in T) \land (N \subseteq V \land M \subseteq W)) \to iEdg (H ISubGr M) (g (i)) = ({J ↾}_{L}) (g (i))$
52	48 51	eqeq12d	$⊢ ((G \in U \land H \in T) \land (N \subseteq V \land M \subseteq W)) \to (f [iEdg (G ISubGr N) (i)] = iEdg (H ISubGr M) (g (i)) \leftrightarrow f [({I ↾}_{K}) (i)] = ({J ↾}_{L}) (g (i)))$
53	32 52	raleqbidv	$⊢ ((G \in U \land H \in T) \land (N \subseteq V \land M \subseteq W)) \to (\forall i \in dom iEdg (G ISubGr N) f [iEdg (G ISubGr N) (i)] = iEdg (H ISubGr M) (g (i)) \leftrightarrow \forall i \in K f [({I ↾}_{K}) (i)] = ({J ↾}_{L}) (g (i)))$
54	53	adantr	$⊢ (((G \in U \land H \in T) \land (N \subseteq V \land M \subseteq W)) \land g : K \underset{1-1 onto}{⟶} L) \to (\forall i \in dom iEdg (G ISubGr N) f [iEdg (G ISubGr N) (i)] = iEdg (H ISubGr M) (g (i)) \leftrightarrow \forall i \in K f [({I ↾}_{K}) (i)] = ({J ↾}_{L}) (g (i)))$
55		fvres	$⊢ i \in K \to ({I ↾}_{K}) (i) = I (i)$
56	55	adantl	$⊢ (((G \in U \land H \in T) \land (N \subseteq V \land M \subseteq W)) \land i \in K) \to ({I ↾}_{K}) (i) = I (i)$
57	56	imaeq2d	$⊢ (((G \in U \land H \in T) \land (N \subseteq V \land M \subseteq W)) \land i \in K) \to f [({I ↾}_{K}) (i)] = f [I (i)]$
58	57	adantlr	$⊢ ((((G \in U \land H \in T) \land (N \subseteq V \land M \subseteq W)) \land g : K \underset{1-1 onto}{⟶} L) \land i \in K) \to f [({I ↾}_{K}) (i)] = f [I (i)]$
59		f1of	$⊢ g : K \underset{1-1 onto}{⟶} L \to g : K ⟶ L$
60	59	adantl	$⊢ (((G \in U \land H \in T) \land (N \subseteq V \land M \subseteq W)) \land g : K \underset{1-1 onto}{⟶} L) \to g : K ⟶ L$
61	60	ffvelcdmda	$⊢ ((((G \in U \land H \in T) \land (N \subseteq V \land M \subseteq W)) \land g : K \underset{1-1 onto}{⟶} L) \land i \in K) \to g (i) \in L$
62	61	fvresd	$⊢ ((((G \in U \land H \in T) \land (N \subseteq V \land M \subseteq W)) \land g : K \underset{1-1 onto}{⟶} L) \land i \in K) \to ({J ↾}_{L}) (g (i)) = J (g (i))$
63	58 62	eqeq12d	$⊢ ((((G \in U \land H \in T) \land (N \subseteq V \land M \subseteq W)) \land g : K \underset{1-1 onto}{⟶} L) \land i \in K) \to (f [({I ↾}_{K}) (i)] = ({J ↾}_{L}) (g (i)) \leftrightarrow f [I (i)] = J (g (i)))$
64	63	ralbidva	$⊢ (((G \in U \land H \in T) \land (N \subseteq V \land M \subseteq W)) \land g : K \underset{1-1 onto}{⟶} L) \to (\forall i \in K f [({I ↾}_{K}) (i)] = ({J ↾}_{L}) (g (i)) \leftrightarrow \forall i \in K f [I (i)] = J (g (i)))$
65	54 64	bitrd	$⊢ (((G \in U \land H \in T) \land (N \subseteq V \land M \subseteq W)) \land g : K \underset{1-1 onto}{⟶} L) \to (\forall i \in dom iEdg (G ISubGr N) f [iEdg (G ISubGr N) (i)] = iEdg (H ISubGr M) (g (i)) \leftrightarrow \forall i \in K f [I (i)] = J (g (i)))$
66	65	pm5.32da	$⊢ ((G \in U \land H \in T) \land (N \subseteq V \land M \subseteq W)) \to ((g : K \underset{1-1 onto}{⟶} L \land \forall i \in dom iEdg (G ISubGr N) f [iEdg (G ISubGr N) (i)] = iEdg (H ISubGr M) (g (i))) \leftrightarrow (g : K \underset{1-1 onto}{⟶} L \land \forall i \in K f [I (i)] = J (g (i))))$
67	44 66	bitrd	$⊢ ((G \in U \land H \in T) \land (N \subseteq V \land M \subseteq W)) \to ((g : dom iEdg (G ISubGr N) \underset{1-1 onto}{⟶} dom iEdg (H ISubGr M) \land \forall i \in dom iEdg (G ISubGr N) f [iEdg (G ISubGr N) (i)] = iEdg (H ISubGr M) (g (i))) \leftrightarrow (g : K \underset{1-1 onto}{⟶} L \land \forall i \in K f [I (i)] = J (g (i))))$
68	67	exbidv	$⊢ ((G \in U \land H \in T) \land (N \subseteq V \land M \subseteq W)) \to (\exists g (g : dom iEdg (G ISubGr N) \underset{1-1 onto}{⟶} dom iEdg (H ISubGr M) \land \forall i \in dom iEdg (G ISubGr N) f [iEdg (G ISubGr N) (i)] = iEdg (H ISubGr M) (g (i))) \leftrightarrow \exists g (g : K \underset{1-1 onto}{⟶} L \land \forall i \in K f [I (i)] = J (g (i))))$
69	21 68	anbi12d	$⊢ ((G \in U \land H \in T) \land (N \subseteq V \land M \subseteq W)) \to ((f : Vtx (G ISubGr N) \underset{1-1 onto}{⟶} Vtx (H ISubGr M) \land \exists g (g : dom iEdg (G ISubGr N) \underset{1-1 onto}{⟶} dom iEdg (H ISubGr M) \land \forall i \in dom iEdg (G ISubGr N) f [iEdg (G ISubGr N) (i)] = iEdg (H ISubGr M) (g (i)))) \leftrightarrow (f : N \underset{1-1 onto}{⟶} M \land \exists g (g : K \underset{1-1 onto}{⟶} L \land \forall i \in K f [I (i)] = J (g (i)))))$
70	69	exbidv	$⊢ ((G \in U \land H \in T) \land (N \subseteq V \land M \subseteq W)) \to (\exists f (f : Vtx (G ISubGr N) \underset{1-1 onto}{⟶} Vtx (H ISubGr M) \land \exists g (g : dom iEdg (G ISubGr N) \underset{1-1 onto}{⟶} dom iEdg (H ISubGr M) \land \forall i \in dom iEdg (G ISubGr N) f [iEdg (G ISubGr N) (i)] = iEdg (H ISubGr M) (g (i)))) \leftrightarrow \exists f (f : N \underset{1-1 onto}{⟶} M \land \exists g (g : K \underset{1-1 onto}{⟶} L \land \forall i \in K f [I (i)] = J (g (i)))))$
71	15 70	bitrd	$⊢ ((G \in U \land H \in T) \land (N \subseteq V \land M \subseteq W)) \to ((G ISubGr N) ≃_{𝑔𝑟} (H ISubGr M) \leftrightarrow \exists f (f : N \underset{1-1 onto}{⟶} M \land \exists g (g : K \underset{1-1 onto}{⟶} L \land \forall i \in K f [I (i)] = J (g (i)))))$

Metamath Proof Explorer

Theorem isubgrgrim

Proof