grimedg

Description: For two isomorphic graphs, a set of vertices is an edge in one graph iff its image by a graph isomorphism is an edge of the other graph. (Contributed by AV, 7-Jun-2025)

	Ref	Expression
Hypotheses	grimedg.v	$⊢ V = Vtx (G)$
	grimedg.i	$⊢ I = Edg (G)$
	grimedg.e	$⊢ E = Edg (H)$
Assertion	grimedg	$⊢ (G \in UHGraph \land H \in UHGraph \land F \in (G GraphIso H)) \to (K \in I \leftrightarrow (F [K] \in E \land K \subseteq V))$

Proof

Step	Hyp	Ref	Expression
1		grimedg.v	$⊢ V = Vtx (G)$
2		grimedg.i	$⊢ I = Edg (G)$
3		grimedg.e	$⊢ E = Edg (H)$
4		eqid	$⊢ Vtx (H) = Vtx (H)$
5		eqid	$⊢ iEdg (G) = iEdg (G)$
6		eqid	$⊢ iEdg (H) = iEdg (H)$
7	1 4 5 6	grimprop	$⊢ F \in (G GraphIso H) \to (F : V \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)) = F [iEdg (G) (i)]))$
8	2	eleq2i	$⊢ K \in I \leftrightarrow K \in Edg (G)$
9	5	uhgredgiedgb	$⊢ G \in UHGraph \to (K \in Edg (G) \leftrightarrow \exists k \in dom iEdg (G) K = iEdg (G) (k))$
10	9	ad2antll	$⊢ ((F : V \underset{1-1 onto}{⟶} Vtx (H) \land (j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)])) \land (H \in UHGraph \land G \in UHGraph)) \to (K \in Edg (G) \leftrightarrow \exists k \in dom iEdg (G) K = iEdg (G) (k))$
11	8 10	bitrid	$⊢ ((F : V \underset{1-1 onto}{⟶} Vtx (H) \land (j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)])) \land (H \in UHGraph \land G \in UHGraph)) \to (K \in I \leftrightarrow \exists k \in dom iEdg (G) K = iEdg (G) (k))$
12		2fveq3	$⊢ i = k \to iEdg (H) (j (i)) = iEdg (H) (j (k))$
13		fveq2	$⊢ i = k \to iEdg (G) (i) = iEdg (G) (k)$
14	13	imaeq2d	$⊢ i = k \to F [iEdg (G) (i)] = F [iEdg (G) (k)]$
15	12 14	eqeq12d	$⊢ i = k \to (iEdg (H) (j (i)) = F [iEdg (G) (i)] \leftrightarrow iEdg (H) (j (k)) = F [iEdg (G) (k)])$
16	15	rspcv	$⊢ k \in dom iEdg (G) \to (\forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)] \to iEdg (H) (j (k)) = F [iEdg (G) (k)])$
17	16	adantl	$⊢ ((H \in UHGraph \land G \in UHGraph) \land k \in dom iEdg (G)) \to (\forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)] \to iEdg (H) (j (k)) = F [iEdg (G) (k)])$
18	6	uhgrfun	$⊢ H \in UHGraph \to Fun iEdg (H)$
19	18	ad2antrr	$⊢ ((H \in UHGraph \land G \in UHGraph) \land k \in dom iEdg (G)) \to Fun iEdg (H)$
20		f1of	$⊢ j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \to j : dom iEdg (G) ⟶ dom iEdg (H)$
21	20	ad2antll	$⊢ (((H \in UHGraph \land G \in UHGraph) \land k \in dom iEdg (G)) \land (F : V \underset{1-1 onto}{⟶} Vtx (H) \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H))) \to j : dom iEdg (G) ⟶ dom iEdg (H)$
22		simplr	$⊢ (((H \in UHGraph \land G \in UHGraph) \land k \in dom iEdg (G)) \land (F : V \underset{1-1 onto}{⟶} Vtx (H) \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H))) \to k \in dom iEdg (G)$
23	21 22	ffvelcdmd	$⊢ (((H \in UHGraph \land G \in UHGraph) \land k \in dom iEdg (G)) \land (F : V \underset{1-1 onto}{⟶} Vtx (H) \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H))) \to j (k) \in dom iEdg (H)$
24	6	iedgedg	$⊢ (Fun iEdg (H) \land j (k) \in dom iEdg (H)) \to iEdg (H) (j (k)) \in Edg (H)$
25	24 3	eleqtrrdi	$⊢ (Fun iEdg (H) \land j (k) \in dom iEdg (H)) \to iEdg (H) (j (k)) \in E$
26	19 23 25	syl2an2r	$⊢ (((H \in UHGraph \land G \in UHGraph) \land k \in dom iEdg (G)) \land (F : V \underset{1-1 onto}{⟶} Vtx (H) \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H))) \to iEdg (H) (j (k)) \in E$
27		eleq1	$⊢ F [iEdg (G) (k)] = iEdg (H) (j (k)) \to (F [iEdg (G) (k)] \in E \leftrightarrow iEdg (H) (j (k)) \in E)$
28	27	eqcoms	$⊢ iEdg (H) (j (k)) = F [iEdg (G) (k)] \to (F [iEdg (G) (k)] \in E \leftrightarrow iEdg (H) (j (k)) \in E)$
29	26 28	syl5ibrcom	$⊢ (((H \in UHGraph \land G \in UHGraph) \land k \in dom iEdg (G)) \land (F : V \underset{1-1 onto}{⟶} Vtx (H) \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H))) \to (iEdg (H) (j (k)) = F [iEdg (G) (k)] \to F [iEdg (G) (k)] \in E)$
30	29	ex	$⊢ ((H \in UHGraph \land G \in UHGraph) \land k \in dom iEdg (G)) \to ((F : V \underset{1-1 onto}{⟶} Vtx (H) \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \to (iEdg (H) (j (k)) = F [iEdg (G) (k)] \to F [iEdg (G) (k)] \in E))$
31	30	com23	$⊢ ((H \in UHGraph \land G \in UHGraph) \land k \in dom iEdg (G)) \to (iEdg (H) (j (k)) = F [iEdg (G) (k)] \to ((F : V \underset{1-1 onto}{⟶} Vtx (H) \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \to F [iEdg (G) (k)] \in E))$
32	17 31	syld	$⊢ ((H \in UHGraph \land G \in UHGraph) \land k \in dom iEdg (G)) \to (\forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)] \to ((F : V \underset{1-1 onto}{⟶} Vtx (H) \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \to F [iEdg (G) (k)] \in E))$
33	32	com13	$⊢ (F : V \underset{1-1 onto}{⟶} Vtx (H) \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \to (\forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)] \to (((H \in UHGraph \land G \in UHGraph) \land k \in dom iEdg (G)) \to F [iEdg (G) (k)] \in E))$
34	33	impr	$⊢ (F : V \underset{1-1 onto}{⟶} Vtx (H) \land (j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)])) \to (((H \in UHGraph \land G \in UHGraph) \land k \in dom iEdg (G)) \to F [iEdg (G) (k)] \in E)$
35	34	impl	$⊢ (((F : V \underset{1-1 onto}{⟶} Vtx (H) \land (j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)])) \land (H \in UHGraph \land G \in UHGraph)) \land k \in dom iEdg (G)) \to F [iEdg (G) (k)] \in E$
36	35	adantr	$⊢ ((((F : V \underset{1-1 onto}{⟶} Vtx (H) \land (j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)])) \land (H \in UHGraph \land G \in UHGraph)) \land k \in dom iEdg (G)) \land K = iEdg (G) (k)) \to F [iEdg (G) (k)] \in E$
37		imaeq2	$⊢ K = iEdg (G) (k) \to F [K] = F [iEdg (G) (k)]$
38	37	eleq1d	$⊢ K = iEdg (G) (k) \to (F [K] \in E \leftrightarrow F [iEdg (G) (k)] \in E)$
39	38	adantl	$⊢ ((((F : V \underset{1-1 onto}{⟶} Vtx (H) \land (j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)])) \land (H \in UHGraph \land G \in UHGraph)) \land k \in dom iEdg (G)) \land K = iEdg (G) (k)) \to (F [K] \in E \leftrightarrow F [iEdg (G) (k)] \in E)$
40	36 39	mpbird	$⊢ ((((F : V \underset{1-1 onto}{⟶} Vtx (H) \land (j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)])) \land (H \in UHGraph \land G \in UHGraph)) \land k \in dom iEdg (G)) \land K = iEdg (G) (k)) \to F [K] \in E$
41	1 5	uhgrss	$⊢ (G \in UHGraph \land k \in dom iEdg (G)) \to iEdg (G) (k) \subseteq V$
42	41	ex	$⊢ G \in UHGraph \to (k \in dom iEdg (G) \to iEdg (G) (k) \subseteq V)$
43	42	ad2antll	$⊢ ((F : V \underset{1-1 onto}{⟶} Vtx (H) \land (j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)])) \land (H \in UHGraph \land G \in UHGraph)) \to (k \in dom iEdg (G) \to iEdg (G) (k) \subseteq V)$
44	43	imp	$⊢ (((F : V \underset{1-1 onto}{⟶} Vtx (H) \land (j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)])) \land (H \in UHGraph \land G \in UHGraph)) \land k \in dom iEdg (G)) \to iEdg (G) (k) \subseteq V$
45	44	adantr	$⊢ ((((F : V \underset{1-1 onto}{⟶} Vtx (H) \land (j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)])) \land (H \in UHGraph \land G \in UHGraph)) \land k \in dom iEdg (G)) \land K = iEdg (G) (k)) \to iEdg (G) (k) \subseteq V$
46		sseq1	$⊢ K = iEdg (G) (k) \to (K \subseteq V \leftrightarrow iEdg (G) (k) \subseteq V)$
47	46	adantl	$⊢ ((((F : V \underset{1-1 onto}{⟶} Vtx (H) \land (j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)])) \land (H \in UHGraph \land G \in UHGraph)) \land k \in dom iEdg (G)) \land K = iEdg (G) (k)) \to (K \subseteq V \leftrightarrow iEdg (G) (k) \subseteq V)$
48	45 47	mpbird	$⊢ ((((F : V \underset{1-1 onto}{⟶} Vtx (H) \land (j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)])) \land (H \in UHGraph \land G \in UHGraph)) \land k \in dom iEdg (G)) \land K = iEdg (G) (k)) \to K \subseteq V$
49	40 48	jca	$⊢ ((((F : V \underset{1-1 onto}{⟶} Vtx (H) \land (j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)])) \land (H \in UHGraph \land G \in UHGraph)) \land k \in dom iEdg (G)) \land K = iEdg (G) (k)) \to (F [K] \in E \land K \subseteq V)$
50	49	ex	$⊢ (((F : V \underset{1-1 onto}{⟶} Vtx (H) \land (j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)])) \land (H \in UHGraph \land G \in UHGraph)) \land k \in dom iEdg (G)) \to (K = iEdg (G) (k) \to (F [K] \in E \land K \subseteq V))$
51	50	rexlimdva	$⊢ ((F : V \underset{1-1 onto}{⟶} Vtx (H) \land (j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)])) \land (H \in UHGraph \land G \in UHGraph)) \to (\exists k \in dom iEdg (G) K = iEdg (G) (k) \to (F [K] \in E \land K \subseteq V))$
52	11 51	sylbid	$⊢ ((F : V \underset{1-1 onto}{⟶} Vtx (H) \land (j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)])) \land (H \in UHGraph \land G \in UHGraph)) \to (K \in I \to (F [K] \in E \land K \subseteq V))$
53	3	eleq2i	$⊢ F [K] \in E \leftrightarrow F [K] \in Edg (H)$
54	6	uhgredgiedgb	$⊢ H \in UHGraph \to (F [K] \in Edg (H) \leftrightarrow \exists k \in dom iEdg (H) F [K] = iEdg (H) (k))$
55	54	ad2antrl	$⊢ ((F : V \underset{1-1 onto}{⟶} Vtx (H) \land (j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)])) \land (H \in UHGraph \land G \in UHGraph)) \to (F [K] \in Edg (H) \leftrightarrow \exists k \in dom iEdg (H) F [K] = iEdg (H) (k))$
56	53 55	bitrid	$⊢ ((F : V \underset{1-1 onto}{⟶} Vtx (H) \land (j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)])) \land (H \in UHGraph \land G \in UHGraph)) \to (F [K] \in E \leftrightarrow \exists k \in dom iEdg (H) F [K] = iEdg (H) (k))$
57		f1ofo	$⊢ j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \to j : dom iEdg (G) \underset{onto}{⟶} dom iEdg (H)$
58	57	adantr	$⊢ (j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)]) \to j : dom iEdg (G) \underset{onto}{⟶} dom iEdg (H)$
59	58	ad2antlr	$⊢ ((F : V \underset{1-1 onto}{⟶} Vtx (H) \land (j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)])) \land (H \in UHGraph \land G \in UHGraph)) \to j : dom iEdg (G) \underset{onto}{⟶} dom iEdg (H)$
60		foelrn	$⊢ (j : dom iEdg (G) \underset{onto}{⟶} dom iEdg (H) \land k \in dom iEdg (H)) \to \exists l \in dom iEdg (G) k = j (l)$
61	59 60	sylan	$⊢ (((F : V \underset{1-1 onto}{⟶} Vtx (H) \land (j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)])) \land (H \in UHGraph \land G \in UHGraph)) \land k \in dom iEdg (H)) \to \exists l \in dom iEdg (G) k = j (l)$
62		2fveq3	$⊢ i = l \to iEdg (H) (j (i)) = iEdg (H) (j (l))$
63		fveq2	$⊢ i = l \to iEdg (G) (i) = iEdg (G) (l)$
64	63	imaeq2d	$⊢ i = l \to F [iEdg (G) (i)] = F [iEdg (G) (l)]$
65	62 64	eqeq12d	$⊢ i = l \to (iEdg (H) (j (i)) = F [iEdg (G) (i)] \leftrightarrow iEdg (H) (j (l)) = F [iEdg (G) (l)])$
66	65	rspcv	$⊢ l \in dom iEdg (G) \to (\forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)] \to iEdg (H) (j (l)) = F [iEdg (G) (l)])$
67	66	adantl	$⊢ (((F : V \underset{1-1 onto}{⟶} Vtx (H) \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land F [K] = iEdg (H) (k) \land ((H \in UHGraph \land G \in UHGraph) \land k \in dom iEdg (H))) \land l \in dom iEdg (G)) \to (\forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)] \to iEdg (H) (j (l)) = F [iEdg (G) (l)])$
68		fveq2	$⊢ k = j (l) \to iEdg (H) (k) = iEdg (H) (j (l))$
69	68	eqeq2d	$⊢ k = j (l) \to (F [K] = iEdg (H) (k) \leftrightarrow F [K] = iEdg (H) (j (l)))$
70	69	ad2antll	$⊢ (((F : V \underset{1-1 onto}{⟶} Vtx (H) \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land ((H \in UHGraph \land G \in UHGraph) \land k \in dom iEdg (H))) \land (l \in dom iEdg (G) \land k = j (l))) \to (F [K] = iEdg (H) (k) \leftrightarrow F [K] = iEdg (H) (j (l)))$
71		simpl	$⊢ (H \in UHGraph \land G \in UHGraph) \to H \in UHGraph$
72	71	ad2antrl	$⊢ ((F : V \underset{1-1 onto}{⟶} Vtx (H) \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land ((H \in UHGraph \land G \in UHGraph) \land k \in dom iEdg (H))) \to H \in UHGraph$
73		simplrr	$⊢ (((F : V \underset{1-1 onto}{⟶} Vtx (H) \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land ((H \in UHGraph \land G \in UHGraph) \land k \in dom iEdg (H))) \land (l \in dom iEdg (G) \land k = j (l))) \to k \in dom iEdg (H)$
74		eleq1	$⊢ k = j (l) \to (k \in dom iEdg (H) \leftrightarrow j (l) \in dom iEdg (H))$
75	74	ad2antll	$⊢ (((F : V \underset{1-1 onto}{⟶} Vtx (H) \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land ((H \in UHGraph \land G \in UHGraph) \land k \in dom iEdg (H))) \land (l \in dom iEdg (G) \land k = j (l))) \to (k \in dom iEdg (H) \leftrightarrow j (l) \in dom iEdg (H))$
76	73 75	mpbid	$⊢ (((F : V \underset{1-1 onto}{⟶} Vtx (H) \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land ((H \in UHGraph \land G \in UHGraph) \land k \in dom iEdg (H))) \land (l \in dom iEdg (G) \land k = j (l))) \to j (l) \in dom iEdg (H)$
77	4 6	uhgrss	$⊢ (H \in UHGraph \land j (l) \in dom iEdg (H)) \to iEdg (H) (j (l)) \subseteq Vtx (H)$
78	72 76 77	syl2an2r	$⊢ (((F : V \underset{1-1 onto}{⟶} Vtx (H) \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land ((H \in UHGraph \land G \in UHGraph) \land k \in dom iEdg (H))) \land (l \in dom iEdg (G) \land k = j (l))) \to iEdg (H) (j (l)) \subseteq Vtx (H)$
79	78	ad2antrr	$⊢ (((((F : V \underset{1-1 onto}{⟶} Vtx (H) \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land ((H \in UHGraph \land G \in UHGraph) \land k \in dom iEdg (H))) \land (l \in dom iEdg (G) \land k = j (l))) \land iEdg (H) (j (l)) = F [iEdg (G) (l)]) \land F [K] = iEdg (H) (j (l))) \to iEdg (H) (j (l)) \subseteq Vtx (H)$
80		sseq1	$⊢ F [K] = iEdg (H) (j (l)) \to (F [K] \subseteq Vtx (H) \leftrightarrow iEdg (H) (j (l)) \subseteq Vtx (H))$
81	80	adantl	$⊢ (((((F : V \underset{1-1 onto}{⟶} Vtx (H) \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land ((H \in UHGraph \land G \in UHGraph) \land k \in dom iEdg (H))) \land (l \in dom iEdg (G) \land k = j (l))) \land iEdg (H) (j (l)) = F [iEdg (G) (l)]) \land F [K] = iEdg (H) (j (l))) \to (F [K] \subseteq Vtx (H) \leftrightarrow iEdg (H) (j (l)) \subseteq Vtx (H))$
82	79 81	mpbird	$⊢ (((((F : V \underset{1-1 onto}{⟶} Vtx (H) \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land ((H \in UHGraph \land G \in UHGraph) \land k \in dom iEdg (H))) \land (l \in dom iEdg (G) \land k = j (l))) \land iEdg (H) (j (l)) = F [iEdg (G) (l)]) \land F [K] = iEdg (H) (j (l))) \to F [K] \subseteq Vtx (H)$
83		eqeq2	$⊢ iEdg (H) (j (l)) = F [iEdg (G) (l)] \to (F [K] = iEdg (H) (j (l)) \leftrightarrow F [K] = F [iEdg (G) (l)])$
84	83	adantl	$⊢ ((((F : V \underset{1-1 onto}{⟶} Vtx (H) \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land ((H \in UHGraph \land G \in UHGraph) \land k \in dom iEdg (H))) \land (l \in dom iEdg (G) \land k = j (l))) \land iEdg (H) (j (l)) = F [iEdg (G) (l)]) \to (F [K] = iEdg (H) (j (l)) \leftrightarrow F [K] = F [iEdg (G) (l)])$
85		f1of1	$⊢ F : V \underset{1-1 onto}{⟶} Vtx (H) \to F : V \underset{1-1}{⟶} Vtx (H)$
86	85	ad3antrrr	$⊢ (((F : V \underset{1-1 onto}{⟶} Vtx (H) \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land ((H \in UHGraph \land G \in UHGraph) \land k \in dom iEdg (H))) \land (l \in dom iEdg (G) \land k = j (l))) \to F : V \underset{1-1}{⟶} Vtx (H)$
87	86	ad3antrrr	$⊢ ((((((F : V \underset{1-1 onto}{⟶} Vtx (H) \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land ((H \in UHGraph \land G \in UHGraph) \land k \in dom iEdg (H))) \land (l \in dom iEdg (G) \land k = j (l))) \land iEdg (H) (j (l)) = F [iEdg (G) (l)]) \land F [K] \subseteq Vtx (H)) \land K \subseteq V) \to F : V \underset{1-1}{⟶} Vtx (H)$
88		simplr	$⊢ ((H \in UHGraph \land G \in UHGraph) \land k \in dom iEdg (H)) \to G \in UHGraph$
89	88	adantl	$⊢ ((F : V \underset{1-1 onto}{⟶} Vtx (H) \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land ((H \in UHGraph \land G \in UHGraph) \land k \in dom iEdg (H))) \to G \in UHGraph$
90		simpl	$⊢ (l \in dom iEdg (G) \land k = j (l)) \to l \in dom iEdg (G)$
91	1 5	uhgrss	$⊢ (G \in UHGraph \land l \in dom iEdg (G)) \to iEdg (G) (l) \subseteq V$
92	89 90 91	syl2an	$⊢ (((F : V \underset{1-1 onto}{⟶} Vtx (H) \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land ((H \in UHGraph \land G \in UHGraph) \land k \in dom iEdg (H))) \land (l \in dom iEdg (G) \land k = j (l))) \to iEdg (G) (l) \subseteq V$
93	92	ad2antrr	$⊢ (((((F : V \underset{1-1 onto}{⟶} Vtx (H) \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land ((H \in UHGraph \land G \in UHGraph) \land k \in dom iEdg (H))) \land (l \in dom iEdg (G) \land k = j (l))) \land iEdg (H) (j (l)) = F [iEdg (G) (l)]) \land F [K] \subseteq Vtx (H)) \to iEdg (G) (l) \subseteq V$
94	93	anim1ci	$⊢ ((((((F : V \underset{1-1 onto}{⟶} Vtx (H) \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land ((H \in UHGraph \land G \in UHGraph) \land k \in dom iEdg (H))) \land (l \in dom iEdg (G) \land k = j (l))) \land iEdg (H) (j (l)) = F [iEdg (G) (l)]) \land F [K] \subseteq Vtx (H)) \land K \subseteq V) \to (K \subseteq V \land iEdg (G) (l) \subseteq V)$
95		f1imaeq	$⊢ (F : V \underset{1-1}{⟶} Vtx (H) \land (K \subseteq V \land iEdg (G) (l) \subseteq V)) \to (F [K] = F [iEdg (G) (l)] \leftrightarrow K = iEdg (G) (l))$
96	87 94 95	syl2anc	$⊢ ((((((F : V \underset{1-1 onto}{⟶} Vtx (H) \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land ((H \in UHGraph \land G \in UHGraph) \land k \in dom iEdg (H))) \land (l \in dom iEdg (G) \land k = j (l))) \land iEdg (H) (j (l)) = F [iEdg (G) (l)]) \land F [K] \subseteq Vtx (H)) \land K \subseteq V) \to (F [K] = F [iEdg (G) (l)] \leftrightarrow K = iEdg (G) (l))$
97	5	uhgrfun	$⊢ G \in UHGraph \to Fun iEdg (G)$
98	97	ad2antlr	$⊢ ((H \in UHGraph \land G \in UHGraph) \land k \in dom iEdg (H)) \to Fun iEdg (G)$
99	98	adantl	$⊢ ((F : V \underset{1-1 onto}{⟶} Vtx (H) \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land ((H \in UHGraph \land G \in UHGraph) \land k \in dom iEdg (H))) \to Fun iEdg (G)$
100	5	iedgedg	$⊢ (Fun iEdg (G) \land l \in dom iEdg (G)) \to iEdg (G) (l) \in Edg (G)$
101	99 90 100	syl2an	$⊢ (((F : V \underset{1-1 onto}{⟶} Vtx (H) \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land ((H \in UHGraph \land G \in UHGraph) \land k \in dom iEdg (H))) \land (l \in dom iEdg (G) \land k = j (l))) \to iEdg (G) (l) \in Edg (G)$
102	101 2	eleqtrrdi	$⊢ (((F : V \underset{1-1 onto}{⟶} Vtx (H) \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land ((H \in UHGraph \land G \in UHGraph) \land k \in dom iEdg (H))) \land (l \in dom iEdg (G) \land k = j (l))) \to iEdg (G) (l) \in I$
103		eleq1	$⊢ K = iEdg (G) (l) \to (K \in I \leftrightarrow iEdg (G) (l) \in I)$
104	102 103	syl5ibrcom	$⊢ (((F : V \underset{1-1 onto}{⟶} Vtx (H) \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land ((H \in UHGraph \land G \in UHGraph) \land k \in dom iEdg (H))) \land (l \in dom iEdg (G) \land k = j (l))) \to (K = iEdg (G) (l) \to K \in I)$
105	104	ad3antrrr	$⊢ ((((((F : V \underset{1-1 onto}{⟶} Vtx (H) \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land ((H \in UHGraph \land G \in UHGraph) \land k \in dom iEdg (H))) \land (l \in dom iEdg (G) \land k = j (l))) \land iEdg (H) (j (l)) = F [iEdg (G) (l)]) \land F [K] \subseteq Vtx (H)) \land K \subseteq V) \to (K = iEdg (G) (l) \to K \in I)$
106	96 105	sylbid	$⊢ ((((((F : V \underset{1-1 onto}{⟶} Vtx (H) \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land ((H \in UHGraph \land G \in UHGraph) \land k \in dom iEdg (H))) \land (l \in dom iEdg (G) \land k = j (l))) \land iEdg (H) (j (l)) = F [iEdg (G) (l)]) \land F [K] \subseteq Vtx (H)) \land K \subseteq V) \to (F [K] = F [iEdg (G) (l)] \to K \in I)$
107	106	ex	$⊢ (((((F : V \underset{1-1 onto}{⟶} Vtx (H) \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land ((H \in UHGraph \land G \in UHGraph) \land k \in dom iEdg (H))) \land (l \in dom iEdg (G) \land k = j (l))) \land iEdg (H) (j (l)) = F [iEdg (G) (l)]) \land F [K] \subseteq Vtx (H)) \to (K \subseteq V \to (F [K] = F [iEdg (G) (l)] \to K \in I))$
108	107	com23	$⊢ (((((F : V \underset{1-1 onto}{⟶} Vtx (H) \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land ((H \in UHGraph \land G \in UHGraph) \land k \in dom iEdg (H))) \land (l \in dom iEdg (G) \land k = j (l))) \land iEdg (H) (j (l)) = F [iEdg (G) (l)]) \land F [K] \subseteq Vtx (H)) \to (F [K] = F [iEdg (G) (l)] \to (K \subseteq V \to K \in I))$
109	108	ex	$⊢ ((((F : V \underset{1-1 onto}{⟶} Vtx (H) \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land ((H \in UHGraph \land G \in UHGraph) \land k \in dom iEdg (H))) \land (l \in dom iEdg (G) \land k = j (l))) \land iEdg (H) (j (l)) = F [iEdg (G) (l)]) \to (F [K] \subseteq Vtx (H) \to (F [K] = F [iEdg (G) (l)] \to (K \subseteq V \to K \in I)))$
110	109	com23	$⊢ ((((F : V \underset{1-1 onto}{⟶} Vtx (H) \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land ((H \in UHGraph \land G \in UHGraph) \land k \in dom iEdg (H))) \land (l \in dom iEdg (G) \land k = j (l))) \land iEdg (H) (j (l)) = F [iEdg (G) (l)]) \to (F [K] = F [iEdg (G) (l)] \to (F [K] \subseteq Vtx (H) \to (K \subseteq V \to K \in I)))$
111	84 110	sylbid	$⊢ ((((F : V \underset{1-1 onto}{⟶} Vtx (H) \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land ((H \in UHGraph \land G \in UHGraph) \land k \in dom iEdg (H))) \land (l \in dom iEdg (G) \land k = j (l))) \land iEdg (H) (j (l)) = F [iEdg (G) (l)]) \to (F [K] = iEdg (H) (j (l)) \to (F [K] \subseteq Vtx (H) \to (K \subseteq V \to K \in I)))$
112	111	imp	$⊢ (((((F : V \underset{1-1 onto}{⟶} Vtx (H) \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land ((H \in UHGraph \land G \in UHGraph) \land k \in dom iEdg (H))) \land (l \in dom iEdg (G) \land k = j (l))) \land iEdg (H) (j (l)) = F [iEdg (G) (l)]) \land F [K] = iEdg (H) (j (l))) \to (F [K] \subseteq Vtx (H) \to (K \subseteq V \to K \in I))$
113	82 112	mpd	$⊢ (((((F : V \underset{1-1 onto}{⟶} Vtx (H) \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land ((H \in UHGraph \land G \in UHGraph) \land k \in dom iEdg (H))) \land (l \in dom iEdg (G) \land k = j (l))) \land iEdg (H) (j (l)) = F [iEdg (G) (l)]) \land F [K] = iEdg (H) (j (l))) \to (K \subseteq V \to K \in I)$
114	113	exp31	$⊢ (((F : V \underset{1-1 onto}{⟶} Vtx (H) \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land ((H \in UHGraph \land G \in UHGraph) \land k \in dom iEdg (H))) \land (l \in dom iEdg (G) \land k = j (l))) \to (iEdg (H) (j (l)) = F [iEdg (G) (l)] \to (F [K] = iEdg (H) (j (l)) \to (K \subseteq V \to K \in I)))$
115	114	com23	$⊢ (((F : V \underset{1-1 onto}{⟶} Vtx (H) \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land ((H \in UHGraph \land G \in UHGraph) \land k \in dom iEdg (H))) \land (l \in dom iEdg (G) \land k = j (l))) \to (F [K] = iEdg (H) (j (l)) \to (iEdg (H) (j (l)) = F [iEdg (G) (l)] \to (K \subseteq V \to K \in I)))$
116	70 115	sylbid	$⊢ (((F : V \underset{1-1 onto}{⟶} Vtx (H) \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land ((H \in UHGraph \land G \in UHGraph) \land k \in dom iEdg (H))) \land (l \in dom iEdg (G) \land k = j (l))) \to (F [K] = iEdg (H) (k) \to (iEdg (H) (j (l)) = F [iEdg (G) (l)] \to (K \subseteq V \to K \in I)))$
117	116	exp31	$⊢ (F : V \underset{1-1 onto}{⟶} Vtx (H) \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \to (((H \in UHGraph \land G \in UHGraph) \land k \in dom iEdg (H)) \to ((l \in dom iEdg (G) \land k = j (l)) \to (F [K] = iEdg (H) (k) \to (iEdg (H) (j (l)) = F [iEdg (G) (l)] \to (K \subseteq V \to K \in I)))))$
118	117	com23	$⊢ (F : V \underset{1-1 onto}{⟶} Vtx (H) \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \to ((l \in dom iEdg (G) \land k = j (l)) \to (((H \in UHGraph \land G \in UHGraph) \land k \in dom iEdg (H)) \to (F [K] = iEdg (H) (k) \to (iEdg (H) (j (l)) = F [iEdg (G) (l)] \to (K \subseteq V \to K \in I)))))$
119	118	com24	$⊢ (F : V \underset{1-1 onto}{⟶} Vtx (H) \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \to (F [K] = iEdg (H) (k) \to (((H \in UHGraph \land G \in UHGraph) \land k \in dom iEdg (H)) \to ((l \in dom iEdg (G) \land k = j (l)) \to (iEdg (H) (j (l)) = F [iEdg (G) (l)] \to (K \subseteq V \to K \in I)))))$
120	119	3imp	$⊢ ((F : V \underset{1-1 onto}{⟶} Vtx (H) \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land F [K] = iEdg (H) (k) \land ((H \in UHGraph \land G \in UHGraph) \land k \in dom iEdg (H))) \to ((l \in dom iEdg (G) \land k = j (l)) \to (iEdg (H) (j (l)) = F [iEdg (G) (l)] \to (K \subseteq V \to K \in I)))$
121	120	expdimp	$⊢ (((F : V \underset{1-1 onto}{⟶} Vtx (H) \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land F [K] = iEdg (H) (k) \land ((H \in UHGraph \land G \in UHGraph) \land k \in dom iEdg (H))) \land l \in dom iEdg (G)) \to (k = j (l) \to (iEdg (H) (j (l)) = F [iEdg (G) (l)] \to (K \subseteq V \to K \in I)))$
122	67 121	syl5d	$⊢ (((F : V \underset{1-1 onto}{⟶} Vtx (H) \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land F [K] = iEdg (H) (k) \land ((H \in UHGraph \land G \in UHGraph) \land k \in dom iEdg (H))) \land l \in dom iEdg (G)) \to (k = j (l) \to (\forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)] \to (K \subseteq V \to K \in I)))$
123	122	rexlimdva	$⊢ ((F : V \underset{1-1 onto}{⟶} Vtx (H) \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land F [K] = iEdg (H) (k) \land ((H \in UHGraph \land G \in UHGraph) \land k \in dom iEdg (H))) \to (\exists l \in dom iEdg (G) k = j (l) \to (\forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)] \to (K \subseteq V \to K \in I)))$
124	123	3exp	$⊢ (F : V \underset{1-1 onto}{⟶} Vtx (H) \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \to (F [K] = iEdg (H) (k) \to (((H \in UHGraph \land G \in UHGraph) \land k \in dom iEdg (H)) \to (\exists l \in dom iEdg (G) k = j (l) \to (\forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)] \to (K \subseteq V \to K \in I)))))$
125	124	com25	$⊢ (F : V \underset{1-1 onto}{⟶} Vtx (H) \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \to (\forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)] \to (((H \in UHGraph \land G \in UHGraph) \land k \in dom iEdg (H)) \to (\exists l \in dom iEdg (G) k = j (l) \to (F [K] = iEdg (H) (k) \to (K \subseteq V \to K \in I)))))$
126	125	impr	$⊢ (F : V \underset{1-1 onto}{⟶} Vtx (H) \land (j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)])) \to (((H \in UHGraph \land G \in UHGraph) \land k \in dom iEdg (H)) \to (\exists l \in dom iEdg (G) k = j (l) \to (F [K] = iEdg (H) (k) \to (K \subseteq V \to K \in I))))$
127	126	impl	$⊢ (((F : V \underset{1-1 onto}{⟶} Vtx (H) \land (j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)])) \land (H \in UHGraph \land G \in UHGraph)) \land k \in dom iEdg (H)) \to (\exists l \in dom iEdg (G) k = j (l) \to (F [K] = iEdg (H) (k) \to (K \subseteq V \to K \in I)))$
128	61 127	mpd	$⊢ (((F : V \underset{1-1 onto}{⟶} Vtx (H) \land (j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)])) \land (H \in UHGraph \land G \in UHGraph)) \land k \in dom iEdg (H)) \to (F [K] = iEdg (H) (k) \to (K \subseteq V \to K \in I))$
129	128	rexlimdva	$⊢ ((F : V \underset{1-1 onto}{⟶} Vtx (H) \land (j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)])) \land (H \in UHGraph \land G \in UHGraph)) \to (\exists k \in dom iEdg (H) F [K] = iEdg (H) (k) \to (K \subseteq V \to K \in I))$
130	56 129	sylbid	$⊢ ((F : V \underset{1-1 onto}{⟶} Vtx (H) \land (j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)])) \land (H \in UHGraph \land G \in UHGraph)) \to (F [K] \in E \to (K \subseteq V \to K \in I))$
131	130	impd	$⊢ ((F : V \underset{1-1 onto}{⟶} Vtx (H) \land (j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)])) \land (H \in UHGraph \land G \in UHGraph)) \to ((F [K] \in E \land K \subseteq V) \to K \in I)$
132	52 131	impbid	$⊢ ((F : V \underset{1-1 onto}{⟶} Vtx (H) \land (j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)])) \land (H \in UHGraph \land G \in UHGraph)) \to (K \in I \leftrightarrow (F [K] \in E \land K \subseteq V))$
133	132	exp31	$⊢ F : V \underset{1-1 onto}{⟶} Vtx (H) \to ((j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)]) \to ((H \in UHGraph \land G \in UHGraph) \to (K \in I \leftrightarrow (F [K] \in E \land K \subseteq V))))$
134	133	exlimdv	$⊢ F : V \underset{1-1 onto}{⟶} Vtx (H) \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)) = F [iEdg (G) (i)]) \to ((H \in UHGraph \land G \in UHGraph) \to (K \in I \leftrightarrow (F [K] \in E \land K \subseteq V))))$
135	134	imp	$⊢ (F : V \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)) = F [iEdg (G) (i)])) \to ((H \in UHGraph \land G \in UHGraph) \to (K \in I \leftrightarrow (F [K] \in E \land K \subseteq V)))$
136	7 135	syl	$⊢ F \in (G GraphIso H) \to ((H \in UHGraph \land G \in UHGraph) \to (K \in I \leftrightarrow (F [K] \in E \land K \subseteq V)))$
137	136	expd	$⊢ F \in (G GraphIso H) \to (H \in UHGraph \to (G \in UHGraph \to (K \in I \leftrightarrow (F [K] \in E \land K \subseteq V))))$
138	137	com13	$⊢ G \in UHGraph \to (H \in UHGraph \to (F \in (G GraphIso H) \to (K \in I \leftrightarrow (F [K] \in E \land K \subseteq V))))$
139	138	3imp	$⊢ (G \in UHGraph \land H \in UHGraph \land F \in (G GraphIso H)) \to (K \in I \leftrightarrow (F [K] \in E \land K \subseteq V))$

Metamath Proof Explorer

Theorem grimedg

Proof