clnbgrgrimlem

Description: Lemma for clnbgrgrim : For two isomorphic hypergraphs, if there is an edge connecting the image of a vertex of the first graph with a vertex of the second graph, the vertex of the second graph is the image of a neighbor of the vertex of the first graph. (Contributed by AV, 2-Jun-2025)

	Ref	Expression
Hypotheses	clnbgrgrim.v	$⊢ V = Vtx (G)$
	clnbgrgrimlem.w	$⊢ W = Vtx (H)$
	clnbgrgrimlem.e	$⊢ E = Edg (H)$
Assertion	clnbgrgrimlem	$⊢ ((G \in UHGraph \land H \in UHGraph) \land F \in (G GraphIso H) \land (X \in V \land Y \in W)) \to ((K \in E \land \{F (X), Y\} \subseteq K) \to \exists n \in (G ClNeighbVtx X) F (n) = Y)$

Proof

Step	Hyp	Ref	Expression
1		clnbgrgrim.v	$⊢ V = Vtx (G)$
2		clnbgrgrimlem.w	$⊢ W = Vtx (H)$
3		clnbgrgrimlem.e	$⊢ E = Edg (H)$
4	3	eleq2i	$⊢ K \in E \leftrightarrow K \in Edg (H)$
5		eqid	$⊢ iEdg (H) = iEdg (H)$
6	5	uhgredgiedgb	$⊢ H \in UHGraph \to (K \in Edg (H) \leftrightarrow \exists k \in dom iEdg (H) K = iEdg (H) (k))$
7	4 6	bitrid	$⊢ H \in UHGraph \to (K \in E \leftrightarrow \exists k \in dom iEdg (H) K = iEdg (H) (k))$
8	7	adantl	$⊢ (G \in UHGraph \land H \in UHGraph) \to (K \in E \leftrightarrow \exists k \in dom iEdg (H) K = iEdg (H) (k))$
9	8	3ad2ant3	$⊢ (F : V \underset{1-1 onto}{⟶} W \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 (G \in UHGraph \land H \in UHGraph)) \to (K \in E \leftrightarrow \exists k \in dom iEdg (H) K = iEdg (H) (k))$
10	9	adantr	$⊢ ((F : V \underset{1-1 onto}{⟶} W \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 (G \in UHGraph \land H \in UHGraph)) \land (X \in V \land Y \in W)) \to (K \in E \leftrightarrow \exists k \in dom iEdg (H) K = iEdg (H) (k))$
11		sseq2	$⊢ K = iEdg (H) (k) \to (\{F (X), Y\} \subseteq K \leftrightarrow \{F (X), Y\} \subseteq iEdg (H) (k))$
12	11	adantl	$⊢ ((((F : V \underset{1-1 onto}{⟶} W \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 (G \in UHGraph \land H \in UHGraph)) \land (X \in V \land Y \in W)) \land k \in dom iEdg (H)) \land K = iEdg (H) (k)) \to (\{F (X), Y\} \subseteq K \leftrightarrow \{F (X), Y\} \subseteq iEdg (H) (k))$
13		simp1	$⊢ (F : V \underset{1-1 onto}{⟶} W \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 (G \in UHGraph \land H \in UHGraph)) \to F : V \underset{1-1 onto}{⟶} W$
14		simpr	$⊢ (X \in V \land Y \in W) \to Y \in W$
15	13 14	anim12i	$⊢ ((F : V \underset{1-1 onto}{⟶} W \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 (G \in UHGraph \land H \in UHGraph)) \land (X \in V \land Y \in W)) \to (F : V \underset{1-1 onto}{⟶} W \land Y \in W)$
16		f1ocnvdm	$⊢ (F : V \underset{1-1 onto}{⟶} W \land Y \in W) \to F^{-1} (Y) \in V$
17	15 16	syl	$⊢ ((F : V \underset{1-1 onto}{⟶} W \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 (G \in UHGraph \land H \in UHGraph)) \land (X \in V \land Y \in W)) \to F^{-1} (Y) \in V$
18		simpl	$⊢ (X \in V \land Y \in W) \to X \in V$
19	18	adantl	$⊢ ((F : V \underset{1-1 onto}{⟶} W \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 (G \in UHGraph \land H \in UHGraph)) \land (X \in V \land Y \in W)) \to X \in V$
20	17 19	jca	$⊢ ((F : V \underset{1-1 onto}{⟶} W \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 (G \in UHGraph \land H \in UHGraph)) \land (X \in V \land Y \in W)) \to (F^{-1} (Y) \in V \land X \in V)$
21	20	ad2antrr	$⊢ ((((F : V \underset{1-1 onto}{⟶} W \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 (G \in UHGraph \land H \in UHGraph)) \land (X \in V \land Y \in W)) \land k \in dom iEdg (H)) \land \{F (X), Y\} \subseteq iEdg (H) (k)) \to (F^{-1} (Y) \in V \land X \in V)$
22		eqid	$⊢ iEdg (G) = iEdg (G)$
23	22	uhgrfun	$⊢ G \in UHGraph \to Fun iEdg (G)$
24	23	adantr	$⊢ (G \in UHGraph \land H \in UHGraph) \to Fun iEdg (G)$
25	24	3ad2ant3	$⊢ (F : V \underset{1-1 onto}{⟶} W \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 (G \in UHGraph \land H \in UHGraph)) \to Fun iEdg (G)$
26	25	ad2antrr	$⊢ (((F : V \underset{1-1 onto}{⟶} W \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 (G \in UHGraph \land H \in UHGraph)) \land (X \in V \land Y \in W)) \land k \in dom iEdg (H)) \to Fun iEdg (G)$
27		simpl2l	$⊢ ((F : V \underset{1-1 onto}{⟶} W \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 (G \in UHGraph \land H \in UHGraph)) \land (X \in V \land Y \in W)) \to j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)$
28		f1ocnvdm	$⊢ (j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land k \in dom iEdg (H)) \to j^{-1} (k) \in dom iEdg (G)$
29	27 28	sylan	$⊢ (((F : V \underset{1-1 onto}{⟶} W \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 (G \in UHGraph \land H \in UHGraph)) \land (X \in V \land Y \in W)) \land k \in dom iEdg (H)) \to j^{-1} (k) \in dom iEdg (G)$
30	26 29	jca	$⊢ (((F : V \underset{1-1 onto}{⟶} W \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 (G \in UHGraph \land H \in UHGraph)) \land (X \in V \land Y \in W)) \land k \in dom iEdg (H)) \to (Fun iEdg (G) \land j^{-1} (k) \in dom iEdg (G))$
31	22	iedgedg	$⊢ (Fun iEdg (G) \land j^{-1} (k) \in dom iEdg (G)) \to iEdg (G) (j^{-1} (k)) \in Edg (G)$
32	30 31	syl	$⊢ (((F : V \underset{1-1 onto}{⟶} W \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 (G \in UHGraph \land H \in UHGraph)) \land (X \in V \land Y \in W)) \land k \in dom iEdg (H)) \to iEdg (G) (j^{-1} (k)) \in Edg (G)$
33	32	adantr	$⊢ ((((F : V \underset{1-1 onto}{⟶} W \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 (G \in UHGraph \land H \in UHGraph)) \land (X \in V \land Y \in W)) \land k \in dom iEdg (H)) \land \{F (X), Y\} \subseteq iEdg (H) (k)) \to iEdg (G) (j^{-1} (k)) \in Edg (G)$
34		sseq2	$⊢ e = iEdg (G) (j^{-1} (k)) \to (\{X, F^{-1} (Y)\} \subseteq e \leftrightarrow \{X, F^{-1} (Y)\} \subseteq iEdg (G) (j^{-1} (k)))$
35	34	adantl	$⊢ (((((F : V \underset{1-1 onto}{⟶} W \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 (G \in UHGraph \land H \in UHGraph)) \land (X \in V \land Y \in W)) \land k \in dom iEdg (H)) \land \{F (X), Y\} \subseteq iEdg (H) (k)) \land e = iEdg (G) (j^{-1} (k))) \to (\{X, F^{-1} (Y)\} \subseteq e \leftrightarrow \{X, F^{-1} (Y)\} \subseteq iEdg (G) (j^{-1} (k)))$
36		2fveq3	$⊢ i = j^{-1} (k) \to iEdg (H) (j (i)) = iEdg (H) (j (j^{-1} (k)))$
37		fveq2	$⊢ i = j^{-1} (k) \to iEdg (G) (i) = iEdg (G) (j^{-1} (k))$
38	37	imaeq2d	$⊢ i = j^{-1} (k) \to F [iEdg (G) (i)] = F [iEdg (G) (j^{-1} (k))]$
39	36 38	eqeq12d	$⊢ i = j^{-1} (k) \to (iEdg (H) (j (i)) = F [iEdg (G) (i)] \leftrightarrow iEdg (H) (j (j^{-1} (k))) = F [iEdg (G) (j^{-1} (k))])$
40	39	rspcv	$⊢ j^{-1} (k) \in dom iEdg (G) \to (\forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)] \to iEdg (H) (j (j^{-1} (k))) = F [iEdg (G) (j^{-1} (k))])$
41	40	adantl	$⊢ (((F : V \underset{1-1 onto}{⟶} W \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land (k \in dom iEdg (H) \land (G \in UHGraph \land H \in UHGraph) \land (X \in V \land Y \in W))) \land j^{-1} (k) \in dom iEdg (G)) \to (\forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)] \to iEdg (H) (j (j^{-1} (k))) = F [iEdg (G) (j^{-1} (k))])$
42		simpr	$⊢ (F : V \underset{1-1 onto}{⟶} W \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \to j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)$
43		simp1	$⊢ (k \in dom iEdg (H) \land (G \in UHGraph \land H \in UHGraph) \land (X \in V \land Y \in W)) \to k \in dom iEdg (H)$
44	42 43	anim12i	$⊢ ((F : V \underset{1-1 onto}{⟶} W \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land (k \in dom iEdg (H) \land (G \in UHGraph \land H \in UHGraph) \land (X \in V \land Y \in W))) \to (j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land k \in dom iEdg (H))$
45	44	adantr	$⊢ (((F : V \underset{1-1 onto}{⟶} W \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land (k \in dom iEdg (H) \land (G \in UHGraph \land H \in UHGraph) \land (X \in V \land Y \in W))) \land j^{-1} (k) \in dom iEdg (G)) \to (j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land k \in dom iEdg (H))$
46		f1ocnvfv2	$⊢ (j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land k \in dom iEdg (H)) \to j (j^{-1} (k)) = k$
47	45 46	syl	$⊢ (((F : V \underset{1-1 onto}{⟶} W \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land (k \in dom iEdg (H) \land (G \in UHGraph \land H \in UHGraph) \land (X \in V \land Y \in W))) \land j^{-1} (k) \in dom iEdg (G)) \to j (j^{-1} (k)) = k$
48	47	fveqeq2d	$⊢ (((F : V \underset{1-1 onto}{⟶} W \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land (k \in dom iEdg (H) \land (G \in UHGraph \land H \in UHGraph) \land (X \in V \land Y \in W))) \land j^{-1} (k) \in dom iEdg (G)) \to (iEdg (H) (j (j^{-1} (k))) = F [iEdg (G) (j^{-1} (k))] \leftrightarrow iEdg (H) (k) = F [iEdg (G) (j^{-1} (k))])$
49		sseq2	$⊢ iEdg (H) (k) = F [iEdg (G) (j^{-1} (k))] \to (\{F (X), Y\} \subseteq iEdg (H) (k) \leftrightarrow \{F (X), Y\} \subseteq F [iEdg (G) (j^{-1} (k))])$
50	49	adantl	$⊢ ((((F : V \underset{1-1 onto}{⟶} W \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land (k \in dom iEdg (H) \land (G \in UHGraph \land H \in UHGraph) \land (X \in V \land Y \in W))) \land j^{-1} (k) \in dom iEdg (G)) \land iEdg (H) (k) = F [iEdg (G) (j^{-1} (k))]) \to (\{F (X), Y\} \subseteq iEdg (H) (k) \leftrightarrow \{F (X), Y\} \subseteq F [iEdg (G) (j^{-1} (k))])$
51		f1ofn	$⊢ F : V \underset{1-1 onto}{⟶} W \to F Fn V$
52	51	ad2antrr	$⊢ ((F : V \underset{1-1 onto}{⟶} W \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land (k \in dom iEdg (H) \land (G \in UHGraph \land H \in UHGraph) \land (X \in V \land Y \in W))) \to F Fn V$
53		simpr3l	$⊢ ((F : V \underset{1-1 onto}{⟶} W \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land (k \in dom iEdg (H) \land (G \in UHGraph \land H \in UHGraph) \land (X \in V \land Y \in W))) \to X \in V$
54		simpl	$⊢ (F : V \underset{1-1 onto}{⟶} W \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \to F : V \underset{1-1 onto}{⟶} W$
55	14	3ad2ant3	$⊢ (k \in dom iEdg (H) \land (G \in UHGraph \land H \in UHGraph) \land (X \in V \land Y \in W)) \to Y \in W$
56	54 55	anim12i	$⊢ ((F : V \underset{1-1 onto}{⟶} W \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land (k \in dom iEdg (H) \land (G \in UHGraph \land H \in UHGraph) \land (X \in V \land Y \in W))) \to (F : V \underset{1-1 onto}{⟶} W \land Y \in W)$
57	56 16	syl	$⊢ ((F : V \underset{1-1 onto}{⟶} W \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land (k \in dom iEdg (H) \land (G \in UHGraph \land H \in UHGraph) \land (X \in V \land Y \in W))) \to F^{-1} (Y) \in V$
58	52 53 57	3jca	$⊢ ((F : V \underset{1-1 onto}{⟶} W \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land (k \in dom iEdg (H) \land (G \in UHGraph \land H \in UHGraph) \land (X \in V \land Y \in W))) \to (F Fn V \land X \in V \land F^{-1} (Y) \in V)$
59	58	adantr	$⊢ (((F : V \underset{1-1 onto}{⟶} W \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land (k \in dom iEdg (H) \land (G \in UHGraph \land H \in UHGraph) \land (X \in V \land Y \in W))) \land j^{-1} (k) \in dom iEdg (G)) \to (F Fn V \land X \in V \land F^{-1} (Y) \in V)$
60		fnimapr	$⊢ (F Fn V \land X \in V \land F^{-1} (Y) \in V) \to F [\{X, F^{-1} (Y)\}] = \{F (X), F (F^{-1} (Y))\}$
61	59 60	syl	$⊢ (((F : V \underset{1-1 onto}{⟶} W \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land (k \in dom iEdg (H) \land (G \in UHGraph \land H \in UHGraph) \land (X \in V \land Y \in W))) \land j^{-1} (k) \in dom iEdg (G)) \to F [\{X, F^{-1} (Y)\}] = \{F (X), F (F^{-1} (Y))\}$
62	56	adantr	$⊢ (((F : V \underset{1-1 onto}{⟶} W \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land (k \in dom iEdg (H) \land (G \in UHGraph \land H \in UHGraph) \land (X \in V \land Y \in W))) \land j^{-1} (k) \in dom iEdg (G)) \to (F : V \underset{1-1 onto}{⟶} W \land Y \in W)$
63		f1ocnvfv2	$⊢ (F : V \underset{1-1 onto}{⟶} W \land Y \in W) \to F (F^{-1} (Y)) = Y$
64	62 63	syl	$⊢ (((F : V \underset{1-1 onto}{⟶} W \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land (k \in dom iEdg (H) \land (G \in UHGraph \land H \in UHGraph) \land (X \in V \land Y \in W))) \land j^{-1} (k) \in dom iEdg (G)) \to F (F^{-1} (Y)) = Y$
65	64	preq2d	$⊢ (((F : V \underset{1-1 onto}{⟶} W \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land (k \in dom iEdg (H) \land (G \in UHGraph \land H \in UHGraph) \land (X \in V \land Y \in W))) \land j^{-1} (k) \in dom iEdg (G)) \to \{F (X), F (F^{-1} (Y))\} = \{F (X), Y\}$
66	61 65	eqtr2d	$⊢ (((F : V \underset{1-1 onto}{⟶} W \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land (k \in dom iEdg (H) \land (G \in UHGraph \land H \in UHGraph) \land (X \in V \land Y \in W))) \land j^{-1} (k) \in dom iEdg (G)) \to \{F (X), Y\} = F [\{X, F^{-1} (Y)\}]$
67	66	sseq1d	$⊢ (((F : V \underset{1-1 onto}{⟶} W \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land (k \in dom iEdg (H) \land (G \in UHGraph \land H \in UHGraph) \land (X \in V \land Y \in W))) \land j^{-1} (k) \in dom iEdg (G)) \to (\{F (X), Y\} \subseteq F [iEdg (G) (j^{-1} (k))] \leftrightarrow F [\{X, F^{-1} (Y)\}] \subseteq F [iEdg (G) (j^{-1} (k))])$
68		f1of1	$⊢ F : V \underset{1-1 onto}{⟶} W \to F : V \underset{1-1}{⟶} W$
69	68	adantr	$⊢ (F : V \underset{1-1 onto}{⟶} W \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \to F : V \underset{1-1}{⟶} W$
70	69	ad2antrr	$⊢ (((F : V \underset{1-1 onto}{⟶} W \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land (k \in dom iEdg (H) \land (G \in UHGraph \land H \in UHGraph) \land (X \in V \land Y \in W))) \land j^{-1} (k) \in dom iEdg (G)) \to F : V \underset{1-1}{⟶} W$
71	53 57	prssd	$⊢ ((F : V \underset{1-1 onto}{⟶} W \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land (k \in dom iEdg (H) \land (G \in UHGraph \land H \in UHGraph) \land (X \in V \land Y \in W))) \to \{X, F^{-1} (Y)\} \subseteq V$
72	71	adantr	$⊢ (((F : V \underset{1-1 onto}{⟶} W \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land (k \in dom iEdg (H) \land (G \in UHGraph \land H \in UHGraph) \land (X \in V \land Y \in W))) \land j^{-1} (k) \in dom iEdg (G)) \to \{X, F^{-1} (Y)\} \subseteq V$
73		simpr2l	$⊢ ((F : V \underset{1-1 onto}{⟶} W \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land (k \in dom iEdg (H) \land (G \in UHGraph \land H \in UHGraph) \land (X \in V \land Y \in W))) \to G \in UHGraph$
74	1 22	uhgrss	$⊢ (G \in UHGraph \land j^{-1} (k) \in dom iEdg (G)) \to iEdg (G) (j^{-1} (k)) \subseteq V$
75	73 74	sylan	$⊢ (((F : V \underset{1-1 onto}{⟶} W \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land (k \in dom iEdg (H) \land (G \in UHGraph \land H \in UHGraph) \land (X \in V \land Y \in W))) \land j^{-1} (k) \in dom iEdg (G)) \to iEdg (G) (j^{-1} (k)) \subseteq V$
76		f1imass	$⊢ (F : V \underset{1-1}{⟶} W \land (\{X, F^{-1} (Y)\} \subseteq V \land iEdg (G) (j^{-1} (k)) \subseteq V)) \to (F [\{X, F^{-1} (Y)\}] \subseteq F [iEdg (G) (j^{-1} (k))] \leftrightarrow \{X, F^{-1} (Y)\} \subseteq iEdg (G) (j^{-1} (k)))$
77	70 72 75 76	syl12anc	$⊢ (((F : V \underset{1-1 onto}{⟶} W \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land (k \in dom iEdg (H) \land (G \in UHGraph \land H \in UHGraph) \land (X \in V \land Y \in W))) \land j^{-1} (k) \in dom iEdg (G)) \to (F [\{X, F^{-1} (Y)\}] \subseteq F [iEdg (G) (j^{-1} (k))] \leftrightarrow \{X, F^{-1} (Y)\} \subseteq iEdg (G) (j^{-1} (k)))$
78	77	biimpd	$⊢ (((F : V \underset{1-1 onto}{⟶} W \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land (k \in dom iEdg (H) \land (G \in UHGraph \land H \in UHGraph) \land (X \in V \land Y \in W))) \land j^{-1} (k) \in dom iEdg (G)) \to (F [\{X, F^{-1} (Y)\}] \subseteq F [iEdg (G) (j^{-1} (k))] \to \{X, F^{-1} (Y)\} \subseteq iEdg (G) (j^{-1} (k)))$
79	67 78	sylbid	$⊢ (((F : V \underset{1-1 onto}{⟶} W \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land (k \in dom iEdg (H) \land (G \in UHGraph \land H \in UHGraph) \land (X \in V \land Y \in W))) \land j^{-1} (k) \in dom iEdg (G)) \to (\{F (X), Y\} \subseteq F [iEdg (G) (j^{-1} (k))] \to \{X, F^{-1} (Y)\} \subseteq iEdg (G) (j^{-1} (k)))$
80	79	adantr	$⊢ ((((F : V \underset{1-1 onto}{⟶} W \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land (k \in dom iEdg (H) \land (G \in UHGraph \land H \in UHGraph) \land (X \in V \land Y \in W))) \land j^{-1} (k) \in dom iEdg (G)) \land iEdg (H) (k) = F [iEdg (G) (j^{-1} (k))]) \to (\{F (X), Y\} \subseteq F [iEdg (G) (j^{-1} (k))] \to \{X, F^{-1} (Y)\} \subseteq iEdg (G) (j^{-1} (k)))$
81	50 80	sylbid	$⊢ ((((F : V \underset{1-1 onto}{⟶} W \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land (k \in dom iEdg (H) \land (G \in UHGraph \land H \in UHGraph) \land (X \in V \land Y \in W))) \land j^{-1} (k) \in dom iEdg (G)) \land iEdg (H) (k) = F [iEdg (G) (j^{-1} (k))]) \to (\{F (X), Y\} \subseteq iEdg (H) (k) \to \{X, F^{-1} (Y)\} \subseteq iEdg (G) (j^{-1} (k)))$
82	81	ex	$⊢ (((F : V \underset{1-1 onto}{⟶} W \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land (k \in dom iEdg (H) \land (G \in UHGraph \land H \in UHGraph) \land (X \in V \land Y \in W))) \land j^{-1} (k) \in dom iEdg (G)) \to (iEdg (H) (k) = F [iEdg (G) (j^{-1} (k))] \to (\{F (X), Y\} \subseteq iEdg (H) (k) \to \{X, F^{-1} (Y)\} \subseteq iEdg (G) (j^{-1} (k))))$
83	48 82	sylbid	$⊢ (((F : V \underset{1-1 onto}{⟶} W \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land (k \in dom iEdg (H) \land (G \in UHGraph \land H \in UHGraph) \land (X \in V \land Y \in W))) \land j^{-1} (k) \in dom iEdg (G)) \to (iEdg (H) (j (j^{-1} (k))) = F [iEdg (G) (j^{-1} (k))] \to (\{F (X), Y\} \subseteq iEdg (H) (k) \to \{X, F^{-1} (Y)\} \subseteq iEdg (G) (j^{-1} (k))))$
84	41 83	syld	$⊢ (((F : V \underset{1-1 onto}{⟶} W \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land (k \in dom iEdg (H) \land (G \in UHGraph \land H \in UHGraph) \land (X \in V \land Y \in W))) \land j^{-1} (k) \in dom iEdg (G)) \to (\forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)] \to (\{F (X), Y\} \subseteq iEdg (H) (k) \to \{X, F^{-1} (Y)\} \subseteq iEdg (G) (j^{-1} (k))))$
85	84	ex	$⊢ ((F : V \underset{1-1 onto}{⟶} W \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land (k \in dom iEdg (H) \land (G \in UHGraph \land H \in UHGraph) \land (X \in V \land Y \in W))) \to (j^{-1} (k) \in dom iEdg (G) \to (\forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)] \to (\{F (X), Y\} \subseteq iEdg (H) (k) \to \{X, F^{-1} (Y)\} \subseteq iEdg (G) (j^{-1} (k)))))$
86	85	com23	$⊢ ((F : V \underset{1-1 onto}{⟶} W \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land (k \in dom iEdg (H) \land (G \in UHGraph \land H \in UHGraph) \land (X \in V \land Y \in W))) \to (\forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)] \to (j^{-1} (k) \in dom iEdg (G) \to (\{F (X), Y\} \subseteq iEdg (H) (k) \to \{X, F^{-1} (Y)\} \subseteq iEdg (G) (j^{-1} (k)))))$
87	86	3exp2	$⊢ (F : V \underset{1-1 onto}{⟶} W \land j : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \to (k \in dom iEdg (H) \to ((G \in UHGraph \land H \in UHGraph) \to ((X \in V \land Y \in W) \to (\forall i \in dom iEdg (G) iEdg (H) (j (i)) = F [iEdg (G) (i)] \to (j^{-1} (k) \in dom iEdg (G) \to (\{F (X), Y\} \subseteq iEdg (H) (k) \to \{X, F^{-1} (Y)\} \subseteq iEdg (G) (j^{-1} (k))))))))$
88	87	com25	$⊢ (F : V \underset{1-1 onto}{⟶} W \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 ((G \in UHGraph \land H \in UHGraph) \to ((X \in V \land Y \in W) \to (k \in dom iEdg (H) \to (j^{-1} (k) \in dom iEdg (G) \to (\{F (X), Y\} \subseteq iEdg (H) (k) \to \{X, F^{-1} (Y)\} \subseteq iEdg (G) (j^{-1} (k))))))))$
89	88	expimpd	$⊢ F : V \underset{1-1 onto}{⟶} W \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 ((G \in UHGraph \land H \in UHGraph) \to ((X \in V \land Y \in W) \to (k \in dom iEdg (H) \to (j^{-1} (k) \in dom iEdg (G) \to (\{F (X), Y\} \subseteq iEdg (H) (k) \to \{X, F^{-1} (Y)\} \subseteq iEdg (G) (j^{-1} (k))))))))$
90	89	3imp1	$⊢ ((F : V \underset{1-1 onto}{⟶} W \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 (G \in UHGraph \land H \in UHGraph)) \land (X \in V \land Y \in W)) \to (k \in dom iEdg (H) \to (j^{-1} (k) \in dom iEdg (G) \to (\{F (X), Y\} \subseteq iEdg (H) (k) \to \{X, F^{-1} (Y)\} \subseteq iEdg (G) (j^{-1} (k)))))$
91	90	imp	$⊢ (((F : V \underset{1-1 onto}{⟶} W \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 (G \in UHGraph \land H \in UHGraph)) \land (X \in V \land Y \in W)) \land k \in dom iEdg (H)) \to (j^{-1} (k) \in dom iEdg (G) \to (\{F (X), Y\} \subseteq iEdg (H) (k) \to \{X, F^{-1} (Y)\} \subseteq iEdg (G) (j^{-1} (k))))$
92	29 91	mpd	$⊢ (((F : V \underset{1-1 onto}{⟶} W \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 (G \in UHGraph \land H \in UHGraph)) \land (X \in V \land Y \in W)) \land k \in dom iEdg (H)) \to (\{F (X), Y\} \subseteq iEdg (H) (k) \to \{X, F^{-1} (Y)\} \subseteq iEdg (G) (j^{-1} (k)))$
93	92	imp	$⊢ ((((F : V \underset{1-1 onto}{⟶} W \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 (G \in UHGraph \land H \in UHGraph)) \land (X \in V \land Y \in W)) \land k \in dom iEdg (H)) \land \{F (X), Y\} \subseteq iEdg (H) (k)) \to \{X, F^{-1} (Y)\} \subseteq iEdg (G) (j^{-1} (k))$
94	33 35 93	rspcedvd	$⊢ ((((F : V \underset{1-1 onto}{⟶} W \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 (G \in UHGraph \land H \in UHGraph)) \land (X \in V \land Y \in W)) \land k \in dom iEdg (H)) \land \{F (X), Y\} \subseteq iEdg (H) (k)) \to \exists e \in Edg (G) \{X, F^{-1} (Y)\} \subseteq e$
95	94	olcd	$⊢ ((((F : V \underset{1-1 onto}{⟶} W \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 (G \in UHGraph \land H \in UHGraph)) \land (X \in V \land Y \in W)) \land k \in dom iEdg (H)) \land \{F (X), Y\} \subseteq iEdg (H) (k)) \to (F^{-1} (Y) = X \lor \exists e \in Edg (G) \{X, F^{-1} (Y)\} \subseteq e)$
96		eqid	$⊢ Edg (G) = Edg (G)$
97	1 96	clnbgrel	$⊢ F^{-1} (Y) \in (G ClNeighbVtx X) \leftrightarrow ((F^{-1} (Y) \in V \land X \in V) \land (F^{-1} (Y) = X \lor \exists e \in Edg (G) \{X, F^{-1} (Y)\} \subseteq e))$
98	21 95 97	sylanbrc	$⊢ ((((F : V \underset{1-1 onto}{⟶} W \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 (G \in UHGraph \land H \in UHGraph)) \land (X \in V \land Y \in W)) \land k \in dom iEdg (H)) \land \{F (X), Y\} \subseteq iEdg (H) (k)) \to F^{-1} (Y) \in (G ClNeighbVtx X)$
99	98	ex	$⊢ (((F : V \underset{1-1 onto}{⟶} W \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 (G \in UHGraph \land H \in UHGraph)) \land (X \in V \land Y \in W)) \land k \in dom iEdg (H)) \to (\{F (X), Y\} \subseteq iEdg (H) (k) \to F^{-1} (Y) \in (G ClNeighbVtx X))$
100	99	adantr	$⊢ ((((F : V \underset{1-1 onto}{⟶} W \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 (G \in UHGraph \land H \in UHGraph)) \land (X \in V \land Y \in W)) \land k \in dom iEdg (H)) \land K = iEdg (H) (k)) \to (\{F (X), Y\} \subseteq iEdg (H) (k) \to F^{-1} (Y) \in (G ClNeighbVtx X))$
101	12 100	sylbid	$⊢ ((((F : V \underset{1-1 onto}{⟶} W \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 (G \in UHGraph \land H \in UHGraph)) \land (X \in V \land Y \in W)) \land k \in dom iEdg (H)) \land K = iEdg (H) (k)) \to (\{F (X), Y\} \subseteq K \to F^{-1} (Y) \in (G ClNeighbVtx X))$
102	101	ex	$⊢ (((F : V \underset{1-1 onto}{⟶} W \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 (G \in UHGraph \land H \in UHGraph)) \land (X \in V \land Y \in W)) \land k \in dom iEdg (H)) \to (K = iEdg (H) (k) \to (\{F (X), Y\} \subseteq K \to F^{-1} (Y) \in (G ClNeighbVtx X)))$
103	102	rexlimdva	$⊢ ((F : V \underset{1-1 onto}{⟶} W \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 (G \in UHGraph \land H \in UHGraph)) \land (X \in V \land Y \in W)) \to (\exists k \in dom iEdg (H) K = iEdg (H) (k) \to (\{F (X), Y\} \subseteq K \to F^{-1} (Y) \in (G ClNeighbVtx X)))$
104	10 103	sylbid	$⊢ ((F : V \underset{1-1 onto}{⟶} W \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 (G \in UHGraph \land H \in UHGraph)) \land (X \in V \land Y \in W)) \to (K \in E \to (\{F (X), Y\} \subseteq K \to F^{-1} (Y) \in (G ClNeighbVtx X)))$
105	104	impd	$⊢ ((F : V \underset{1-1 onto}{⟶} W \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 (G \in UHGraph \land H \in UHGraph)) \land (X \in V \land Y \in W)) \to ((K \in E \land \{F (X), Y\} \subseteq K) \to F^{-1} (Y) \in (G ClNeighbVtx X))$
106	105	3exp1	$⊢ F : V \underset{1-1 onto}{⟶} W \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 ((G \in UHGraph \land H \in UHGraph) \to ((X \in V \land Y \in W) \to ((K \in E \land \{F (X), Y\} \subseteq K) \to F^{-1} (Y) \in (G ClNeighbVtx X)))))$
107	106	exlimdv	$⊢ F : V \underset{1-1 onto}{⟶} W \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 ((G \in UHGraph \land H \in UHGraph) \to ((X \in V \land Y \in W) \to ((K \in E \land \{F (X), Y\} \subseteq K) \to F^{-1} (Y) \in (G ClNeighbVtx X)))))$
108	107	imp	$⊢ (F : V \underset{1-1 onto}{⟶} W \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 ((G \in UHGraph \land H \in UHGraph) \to ((X \in V \land Y \in W) \to ((K \in E \land \{F (X), Y\} \subseteq K) \to F^{-1} (Y) \in (G ClNeighbVtx X))))$
109	1 2 22 5	grimprop	$⊢ F \in (G GraphIso H) \to (F : V \underset{1-1 onto}{⟶} W \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)]))$
110	108 109	syl11	$⊢ (G \in UHGraph \land H \in UHGraph) \to (F \in (G GraphIso H) \to ((X \in V \land Y \in W) \to ((K \in E \land \{F (X), Y\} \subseteq K) \to F^{-1} (Y) \in (G ClNeighbVtx X))))$
111	110	3imp1	$⊢ (((G \in UHGraph \land H \in UHGraph) \land F \in (G GraphIso H) \land (X \in V \land Y \in W)) \land (K \in E \land \{F (X), Y\} \subseteq K)) \to F^{-1} (Y) \in (G ClNeighbVtx X)$
112		fveqeq2	$⊢ n = F^{-1} (Y) \to (F (n) = Y \leftrightarrow F (F^{-1} (Y)) = Y)$
113	112	adantl	$⊢ ((((G \in UHGraph \land H \in UHGraph) \land F \in (G GraphIso H) \land (X \in V \land Y \in W)) \land (K \in E \land \{F (X), Y\} \subseteq K)) \land n = F^{-1} (Y)) \to (F (n) = Y \leftrightarrow F (F^{-1} (Y)) = Y)$
114	1 2	grimf1o	$⊢ F \in (G GraphIso H) \to F : V \underset{1-1 onto}{⟶} W$
115	114 14	anim12i	$⊢ (F \in (G GraphIso H) \land (X \in V \land Y \in W)) \to (F : V \underset{1-1 onto}{⟶} W \land Y \in W)$
116	115	3adant1	$⊢ ((G \in UHGraph \land H \in UHGraph) \land F \in (G GraphIso H) \land (X \in V \land Y \in W)) \to (F : V \underset{1-1 onto}{⟶} W \land Y \in W)$
117	116	adantr	$⊢ (((G \in UHGraph \land H \in UHGraph) \land F \in (G GraphIso H) \land (X \in V \land Y \in W)) \land (K \in E \land \{F (X), Y\} \subseteq K)) \to (F : V \underset{1-1 onto}{⟶} W \land Y \in W)$
118	117 63	syl	$⊢ (((G \in UHGraph \land H \in UHGraph) \land F \in (G GraphIso H) \land (X \in V \land Y \in W)) \land (K \in E \land \{F (X), Y\} \subseteq K)) \to F (F^{-1} (Y)) = Y$
119	111 113 118	rspcedvd	$⊢ (((G \in UHGraph \land H \in UHGraph) \land F \in (G GraphIso H) \land (X \in V \land Y \in W)) \land (K \in E \land \{F (X), Y\} \subseteq K)) \to \exists n \in (G ClNeighbVtx X) F (n) = Y$
120	119	ex	$⊢ ((G \in UHGraph \land H \in UHGraph) \land F \in (G GraphIso H) \land (X \in V \land Y \in W)) \to ((K \in E \land \{F (X), Y\} \subseteq K) \to \exists n \in (G ClNeighbVtx X) F (n) = Y)$

Metamath Proof Explorer

Theorem clnbgrgrimlem

Proof