clnbgrgrim

Description: Graph isomorphisms between hypergraphs map closed neighborhoods onto closed neighborhoods. (Contributed by AV, 2-Jun-2025)

		Ref	Expression
	Hypothesis	clnbgrgrim.v	$⊢ V = Vtx (G)$
	Assertion	clnbgrgrim	$⊢ (((G \in UHGraph \land H \in UHGraph) \land F \in (G GraphIso H)) \land X \in V) \to H ClNeighbVtx F (X) = F [G ClNeighbVtx X]$

Proof

Step	Hyp	Ref	Expression
1		clnbgrgrim.v	$⊢ V = Vtx (G)$
2		fveqeq2	$⊢ n = X \to (F (n) = F (X) \leftrightarrow F (X) = F (X))$
3	1	clnbgrvtxel	$⊢ X \in V \to X \in (G ClNeighbVtx X)$
4	3	3ad2ant3	$⊢ (F \in (G GraphIso H) \land (G \in UHGraph \land H \in UHGraph) \land X \in V) \to X \in (G ClNeighbVtx X)$
5		eqidd	$⊢ (F \in (G GraphIso H) \land (G \in UHGraph \land H \in UHGraph) \land X \in V) \to F (X) = F (X)$
6	2 4 5	rspcedvdw	$⊢ (F \in (G GraphIso H) \land (G \in UHGraph \land H \in UHGraph) \land X \in V) \to \exists n \in (G ClNeighbVtx X) F (n) = F (X)$
7	6	adantr	$⊢ ((F \in (G GraphIso H) \land (G \in UHGraph \land H \in UHGraph) \land X \in V) \land (x \in Vtx (H) \land F (X) \in Vtx (H))) \to \exists n \in (G ClNeighbVtx X) F (n) = F (X)$
8		eqeq2	$⊢ x = F (X) \to (F (n) = x \leftrightarrow F (n) = F (X))$
9	8	rexbidv	$⊢ x = F (X) \to (\exists n \in (G ClNeighbVtx X) F (n) = x \leftrightarrow \exists n \in (G ClNeighbVtx X) F (n) = F (X))$
10	7 9	syl5ibrcom	$⊢ ((F \in (G GraphIso H) \land (G \in UHGraph \land H \in UHGraph) \land X \in V) \land (x \in Vtx (H) \land F (X) \in Vtx (H))) \to (x = F (X) \to \exists n \in (G ClNeighbVtx X) F (n) = x)$
11		simpl2	$⊢ ((F \in (G GraphIso H) \land (G \in UHGraph \land H \in UHGraph) \land X \in V) \land (x \in Vtx (H) \land F (X) \in Vtx (H))) \to (G \in UHGraph \land H \in UHGraph)$
12		simpl1	$⊢ ((F \in (G GraphIso H) \land (G \in UHGraph \land H \in UHGraph) \land X \in V) \land (x \in Vtx (H) \land F (X) \in Vtx (H))) \to F \in (G GraphIso H)$
13		simp3	$⊢ (F \in (G GraphIso H) \land (G \in UHGraph \land H \in UHGraph) \land X \in V) \to X \in V$
14		simpl	$⊢ (x \in Vtx (H) \land F (X) \in Vtx (H)) \to x \in Vtx (H)$
15	13 14	anim12i	$⊢ ((F \in (G GraphIso H) \land (G \in UHGraph \land H \in UHGraph) \land X \in V) \land (x \in Vtx (H) \land F (X) \in Vtx (H))) \to (X \in V \land x \in Vtx (H))$
16		eqid	$⊢ Vtx (H) = Vtx (H)$
17		eqid	$⊢ Edg (H) = Edg (H)$
18	1 16 17	clnbgrgrimlem	$⊢ ((G \in UHGraph \land H \in UHGraph) \land F \in (G GraphIso H) \land (X \in V \land x \in Vtx (H))) \to ((e \in Edg (H) \land \{F (X), x\} \subseteq e) \to \exists n \in (G ClNeighbVtx X) F (n) = x)$
19	11 12 15 18	syl3anc	$⊢ ((F \in (G GraphIso H) \land (G \in UHGraph \land H \in UHGraph) \land X \in V) \land (x \in Vtx (H) \land F (X) \in Vtx (H))) \to ((e \in Edg (H) \land \{F (X), x\} \subseteq e) \to \exists n \in (G ClNeighbVtx X) F (n) = x)$
20	19	expd	$⊢ ((F \in (G GraphIso H) \land (G \in UHGraph \land H \in UHGraph) \land X \in V) \land (x \in Vtx (H) \land F (X) \in Vtx (H))) \to (e \in Edg (H) \to (\{F (X), x\} \subseteq e \to \exists n \in (G ClNeighbVtx X) F (n) = x))$
21	20	rexlimdv	$⊢ ((F \in (G GraphIso H) \land (G \in UHGraph \land H \in UHGraph) \land X \in V) \land (x \in Vtx (H) \land F (X) \in Vtx (H))) \to (\exists e \in Edg (H) \{F (X), x\} \subseteq e \to \exists n \in (G ClNeighbVtx X) F (n) = x)$
22	10 21	jaod	$⊢ ((F \in (G GraphIso H) \land (G \in UHGraph \land H \in UHGraph) \land X \in V) \land (x \in Vtx (H) \land F (X) \in Vtx (H))) \to ((x = F (X) \lor \exists e \in Edg (H) \{F (X), x\} \subseteq e) \to \exists n \in (G ClNeighbVtx X) F (n) = x)$
23	22	expimpd	$⊢ (F \in (G GraphIso H) \land (G \in UHGraph \land H \in UHGraph) \land X \in V) \to (((x \in Vtx (H) \land F (X) \in Vtx (H)) \land (x = F (X) \lor \exists e \in Edg (H) \{F (X), x\} \subseteq e)) \to \exists n \in (G ClNeighbVtx X) F (n) = x)$
24		eqid	$⊢ iEdg (G) = iEdg (G)$
25		eqid	$⊢ iEdg (H) = iEdg (H)$
26	1 16 24 25	grimprop	$⊢ F \in (G GraphIso H) \to (F : V \underset{1-1 onto}{⟶} Vtx (H) \land \exists g (g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)]))$
27		f1of	$⊢ F : V \underset{1-1 onto}{⟶} Vtx (H) \to F : V ⟶ Vtx (H)$
28	27	adantr	$⊢ (F : V \underset{1-1 onto}{⟶} Vtx (H) \land \exists g (g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)])) \to F : V ⟶ Vtx (H)$
29	28	3ad2ant1	$⊢ ((F : V \underset{1-1 onto}{⟶} Vtx (H) \land \exists g (g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)])) \land (G \in UHGraph \land H \in UHGraph) \land X \in V) \to F : V ⟶ Vtx (H)$
30	29	ad2antrr	$⊢ ((((F : V \underset{1-1 onto}{⟶} Vtx (H) \land \exists g (g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)])) \land (G \in UHGraph \land H \in UHGraph) \land X \in V) \land n \in (G ClNeighbVtx X)) \land F (n) = x) \to F : V ⟶ Vtx (H)$
31	1	clnbgrisvtx	$⊢ n \in (G ClNeighbVtx X) \to n \in V$
32	31	adantl	$⊢ (((F : V \underset{1-1 onto}{⟶} Vtx (H) \land \exists g (g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)])) \land (G \in UHGraph \land H \in UHGraph) \land X \in V) \land n \in (G ClNeighbVtx X)) \to n \in V$
33	32	adantr	$⊢ ((((F : V \underset{1-1 onto}{⟶} Vtx (H) \land \exists g (g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)])) \land (G \in UHGraph \land H \in UHGraph) \land X \in V) \land n \in (G ClNeighbVtx X)) \land F (n) = x) \to n \in V$
34	30 33	ffvelcdmd	$⊢ ((((F : V \underset{1-1 onto}{⟶} Vtx (H) \land \exists g (g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)])) \land (G \in UHGraph \land H \in UHGraph) \land X \in V) \land n \in (G ClNeighbVtx X)) \land F (n) = x) \to F (n) \in Vtx (H)$
35		eleq1	$⊢ x = F (n) \to (x \in Vtx (H) \leftrightarrow F (n) \in Vtx (H))$
36	35	eqcoms	$⊢ F (n) = x \to (x \in Vtx (H) \leftrightarrow F (n) \in Vtx (H))$
37	36	adantl	$⊢ ((((F : V \underset{1-1 onto}{⟶} Vtx (H) \land \exists g (g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)])) \land (G \in UHGraph \land H \in UHGraph) \land X \in V) \land n \in (G ClNeighbVtx X)) \land F (n) = x) \to (x \in Vtx (H) \leftrightarrow F (n) \in Vtx (H))$
38	34 37	mpbird	$⊢ ((((F : V \underset{1-1 onto}{⟶} Vtx (H) \land \exists g (g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)])) \land (G \in UHGraph \land H \in UHGraph) \land X \in V) \land n \in (G ClNeighbVtx X)) \land F (n) = x) \to x \in Vtx (H)$
39		simp3	$⊢ ((F : V \underset{1-1 onto}{⟶} Vtx (H) \land \exists g (g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)])) \land (G \in UHGraph \land H \in UHGraph) \land X \in V) \to X \in V$
40	29 39	ffvelcdmd	$⊢ ((F : V \underset{1-1 onto}{⟶} Vtx (H) \land \exists g (g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)])) \land (G \in UHGraph \land H \in UHGraph) \land X \in V) \to F (X) \in Vtx (H)$
41	40	ad2antrr	$⊢ ((((F : V \underset{1-1 onto}{⟶} Vtx (H) \land \exists g (g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)])) \land (G \in UHGraph \land H \in UHGraph) \land X \in V) \land n \in (G ClNeighbVtx X)) \land F (n) = x) \to F (X) \in Vtx (H)$
42		eqid	$⊢ Edg (G) = Edg (G)$
43	1 42	clnbgrel	$⊢ n \in (G ClNeighbVtx X) \leftrightarrow ((n \in V \land X \in V) \land (n = X \lor \exists k \in Edg (G) \{X, n\} \subseteq k))$
44		fveq2	$⊢ n = X \to F (n) = F (X)$
45	44	orcd	$⊢ n = X \to (F (n) = F (X) \lor \exists e \in Edg (H) \{F (X), F (n)\} \subseteq e)$
46	45	2a1d	$⊢ n = X \to ((n \in V \land X \in V) \to (((F : V \underset{1-1 onto}{⟶} Vtx (H) \land \exists g (g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)])) \land (G \in UHGraph \land H \in UHGraph) \land X \in V) \to (F (n) = F (X) \lor \exists e \in Edg (H) \{F (X), F (n)\} \subseteq e)))$
47	24	uhgredgiedgb	$⊢ G \in UHGraph \to (k \in Edg (G) \leftrightarrow \exists j \in dom iEdg (G) k = iEdg (G) (j))$
48	47	adantr	$⊢ (G \in UHGraph \land H \in UHGraph) \to (k \in Edg (G) \leftrightarrow \exists j \in dom iEdg (G) k = iEdg (G) (j))$
49	48	3ad2ant2	$⊢ ((F : V \underset{1-1 onto}{⟶} Vtx (H) \land \exists g (g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)])) \land (G \in UHGraph \land H \in UHGraph) \land X \in V) \to (k \in Edg (G) \leftrightarrow \exists j \in dom iEdg (G) k = iEdg (G) (j))$
50	49	biimpa	$⊢ (((F : V \underset{1-1 onto}{⟶} Vtx (H) \land \exists g (g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)])) \land (G \in UHGraph \land H \in UHGraph) \land X \in V) \land k \in Edg (G)) \to \exists j \in dom iEdg (G) k = iEdg (G) (j)$
51		2fveq3	$⊢ i = j \to iEdg (H) (g (i)) = iEdg (H) (g (j))$
52		fveq2	$⊢ i = j \to iEdg (G) (i) = iEdg (G) (j)$
53	52	imaeq2d	$⊢ i = j \to F [iEdg (G) (i)] = F [iEdg (G) (j)]$
54	51 53	eqeq12d	$⊢ i = j \to (iEdg (H) (g (i)) = F [iEdg (G) (i)] \leftrightarrow iEdg (H) (g (j)) = F [iEdg (G) (j)])$
55	54	rspcv	$⊢ j \in dom iEdg (G) \to (\forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)] \to iEdg (H) (g (j)) = F [iEdg (G) (j)])$
56	55	3ad2ant3	$⊢ (((F : V \underset{1-1 onto}{⟶} Vtx (H) \land g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land k \in Edg (G) \land (G \in UHGraph \land H \in UHGraph)) \land X \in V \land j \in dom iEdg (G)) \to (\forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)] \to iEdg (H) (g (j)) = F [iEdg (G) (j)])$
57		sseq2	$⊢ k = iEdg (G) (j) \to (\{X, n\} \subseteq k \leftrightarrow \{X, n\} \subseteq iEdg (G) (j))$
58	57	3ad2ant3	$⊢ ((((F : V \underset{1-1 onto}{⟶} Vtx (H) \land g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land k \in Edg (G) \land (G \in UHGraph \land H \in UHGraph)) \land X \in V \land j \in dom iEdg (G)) \land iEdg (H) (g (j)) = F [iEdg (G) (j)] \land k = iEdg (G) (j)) \to (\{X, n\} \subseteq k \leftrightarrow \{X, n\} \subseteq iEdg (G) (j))$
59		sseq2	$⊢ e = iEdg (H) (g (j)) \to (\{F (X), F (n)\} \subseteq e \leftrightarrow \{F (X), F (n)\} \subseteq iEdg (H) (g (j)))$
60	25	uhgrfun	$⊢ H \in UHGraph \to Fun iEdg (H)$
61	60	adantl	$⊢ (G \in UHGraph \land H \in UHGraph) \to Fun iEdg (H)$
62	61	3ad2ant3	$⊢ ((F : V \underset{1-1 onto}{⟶} Vtx (H) \land g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land k \in Edg (G) \land (G \in UHGraph \land H \in UHGraph)) \to Fun iEdg (H)$
63		f1of	$⊢ g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \to g : dom iEdg (G) ⟶ dom iEdg (H)$
64	63	adantl	$⊢ (F : V \underset{1-1 onto}{⟶} Vtx (H) \land g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \to g : dom iEdg (G) ⟶ dom iEdg (H)$
65	64	3ad2ant1	$⊢ ((F : V \underset{1-1 onto}{⟶} Vtx (H) \land g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land k \in Edg (G) \land (G \in UHGraph \land H \in UHGraph)) \to g : dom iEdg (G) ⟶ dom iEdg (H)$
66	65	ffvelcdmda	$⊢ (((F : V \underset{1-1 onto}{⟶} Vtx (H) \land g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land k \in Edg (G) \land (G \in UHGraph \land H \in UHGraph)) \land j \in dom iEdg (G)) \to g (j) \in dom iEdg (H)$
67	25	iedgedg	$⊢ (Fun iEdg (H) \land g (j) \in dom iEdg (H)) \to iEdg (H) (g (j)) \in Edg (H)$
68	62 66 67	syl2an2r	$⊢ (((F : V \underset{1-1 onto}{⟶} Vtx (H) \land g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land k \in Edg (G) \land (G \in UHGraph \land H \in UHGraph)) \land j \in dom iEdg (G)) \to iEdg (H) (g (j)) \in Edg (H)$
69	68	3adant2	$⊢ (((F : V \underset{1-1 onto}{⟶} Vtx (H) \land g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land k \in Edg (G) \land (G \in UHGraph \land H \in UHGraph)) \land X \in V \land j \in dom iEdg (G)) \to iEdg (H) (g (j)) \in Edg (H)$
70	69	adantr	$⊢ ((((F : V \underset{1-1 onto}{⟶} Vtx (H) \land g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land k \in Edg (G) \land (G \in UHGraph \land H \in UHGraph)) \land X \in V \land j \in dom iEdg (G)) \land iEdg (H) (g (j)) = F [iEdg (G) (j)]) \to iEdg (H) (g (j)) \in Edg (H)$
71	70	3ad2ant1	$⊢ (((((F : V \underset{1-1 onto}{⟶} Vtx (H) \land g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land k \in Edg (G) \land (G \in UHGraph \land H \in UHGraph)) \land X \in V \land j \in dom iEdg (G)) \land iEdg (H) (g (j)) = F [iEdg (G) (j)]) \land \{X, n\} \subseteq iEdg (G) (j) \land (n \in V \land X \in V)) \to iEdg (H) (g (j)) \in Edg (H)$
72		f1ofn	$⊢ F : V \underset{1-1 onto}{⟶} Vtx (H) \to F Fn V$
73	72	adantr	$⊢ (F : V \underset{1-1 onto}{⟶} Vtx (H) \land g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \to F Fn V$
74	73	3ad2ant1	$⊢ ((F : V \underset{1-1 onto}{⟶} Vtx (H) \land g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land k \in Edg (G) \land (G \in UHGraph \land H \in UHGraph)) \to F Fn V$
75	74	3ad2ant1	$⊢ (((F : V \underset{1-1 onto}{⟶} Vtx (H) \land g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land k \in Edg (G) \land (G \in UHGraph \land H \in UHGraph)) \land X \in V \land j \in dom iEdg (G)) \to F Fn V$
76	75	adantr	$⊢ ((((F : V \underset{1-1 onto}{⟶} Vtx (H) \land g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land k \in Edg (G) \land (G \in UHGraph \land H \in UHGraph)) \land X \in V \land j \in dom iEdg (G)) \land iEdg (H) (g (j)) = F [iEdg (G) (j)]) \to F Fn V$
77		pm3.22	$⊢ (n \in V \land X \in V) \to (X \in V \land n \in V)$
78	76 77	anim12i	$⊢ (((((F : V \underset{1-1 onto}{⟶} Vtx (H) \land g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land k \in Edg (G) \land (G \in UHGraph \land H \in UHGraph)) \land X \in V \land j \in dom iEdg (G)) \land iEdg (H) (g (j)) = F [iEdg (G) (j)]) \land (n \in V \land X \in V)) \to (F Fn V \land (X \in V \land n \in V))$
79	78	3adant2	$⊢ (((((F : V \underset{1-1 onto}{⟶} Vtx (H) \land g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land k \in Edg (G) \land (G \in UHGraph \land H \in UHGraph)) \land X \in V \land j \in dom iEdg (G)) \land iEdg (H) (g (j)) = F [iEdg (G) (j)]) \land \{X, n\} \subseteq iEdg (G) (j) \land (n \in V \land X \in V)) \to (F Fn V \land (X \in V \land n \in V))$
80		3anass	$⊢ (F Fn V \land X \in V \land n \in V) \leftrightarrow (F Fn V \land (X \in V \land n \in V))$
81	79 80	sylibr	$⊢ (((((F : V \underset{1-1 onto}{⟶} Vtx (H) \land g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land k \in Edg (G) \land (G \in UHGraph \land H \in UHGraph)) \land X \in V \land j \in dom iEdg (G)) \land iEdg (H) (g (j)) = F [iEdg (G) (j)]) \land \{X, n\} \subseteq iEdg (G) (j) \land (n \in V \land X \in V)) \to (F Fn V \land X \in V \land n \in V)$
82		fnimapr	$⊢ (F Fn V \land X \in V \land n \in V) \to F [\{X, n\}] = \{F (X), F (n)\}$
83	81 82	syl	$⊢ (((((F : V \underset{1-1 onto}{⟶} Vtx (H) \land g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land k \in Edg (G) \land (G \in UHGraph \land H \in UHGraph)) \land X \in V \land j \in dom iEdg (G)) \land iEdg (H) (g (j)) = F [iEdg (G) (j)]) \land \{X, n\} \subseteq iEdg (G) (j) \land (n \in V \land X \in V)) \to F [\{X, n\}] = \{F (X), F (n)\}$
84		imass2	$⊢ \{X, n\} \subseteq iEdg (G) (j) \to F [\{X, n\}] \subseteq F [iEdg (G) (j)]$
85	84	3ad2ant2	$⊢ (((((F : V \underset{1-1 onto}{⟶} Vtx (H) \land g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land k \in Edg (G) \land (G \in UHGraph \land H \in UHGraph)) \land X \in V \land j \in dom iEdg (G)) \land iEdg (H) (g (j)) = F [iEdg (G) (j)]) \land \{X, n\} \subseteq iEdg (G) (j) \land (n \in V \land X \in V)) \to F [\{X, n\}] \subseteq F [iEdg (G) (j)]$
86	83 85	eqsstrrd	$⊢ (((((F : V \underset{1-1 onto}{⟶} Vtx (H) \land g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land k \in Edg (G) \land (G \in UHGraph \land H \in UHGraph)) \land X \in V \land j \in dom iEdg (G)) \land iEdg (H) (g (j)) = F [iEdg (G) (j)]) \land \{X, n\} \subseteq iEdg (G) (j) \land (n \in V \land X \in V)) \to \{F (X), F (n)\} \subseteq F [iEdg (G) (j)]$
87		simp1r	$⊢ (((((F : V \underset{1-1 onto}{⟶} Vtx (H) \land g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land k \in Edg (G) \land (G \in UHGraph \land H \in UHGraph)) \land X \in V \land j \in dom iEdg (G)) \land iEdg (H) (g (j)) = F [iEdg (G) (j)]) \land \{X, n\} \subseteq iEdg (G) (j) \land (n \in V \land X \in V)) \to iEdg (H) (g (j)) = F [iEdg (G) (j)]$
88	86 87	sseqtrrd	$⊢ (((((F : V \underset{1-1 onto}{⟶} Vtx (H) \land g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land k \in Edg (G) \land (G \in UHGraph \land H \in UHGraph)) \land X \in V \land j \in dom iEdg (G)) \land iEdg (H) (g (j)) = F [iEdg (G) (j)]) \land \{X, n\} \subseteq iEdg (G) (j) \land (n \in V \land X \in V)) \to \{F (X), F (n)\} \subseteq iEdg (H) (g (j))$
89	59 71 88	rspcedvdw	$⊢ (((((F : V \underset{1-1 onto}{⟶} Vtx (H) \land g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land k \in Edg (G) \land (G \in UHGraph \land H \in UHGraph)) \land X \in V \land j \in dom iEdg (G)) \land iEdg (H) (g (j)) = F [iEdg (G) (j)]) \land \{X, n\} \subseteq iEdg (G) (j) \land (n \in V \land X \in V)) \to \exists e \in Edg (H) \{F (X), F (n)\} \subseteq e$
90	89	3exp	$⊢ ((((F : V \underset{1-1 onto}{⟶} Vtx (H) \land g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land k \in Edg (G) \land (G \in UHGraph \land H \in UHGraph)) \land X \in V \land j \in dom iEdg (G)) \land iEdg (H) (g (j)) = F [iEdg (G) (j)]) \to (\{X, n\} \subseteq iEdg (G) (j) \to ((n \in V \land X \in V) \to \exists e \in Edg (H) \{F (X), F (n)\} \subseteq e))$
91	90	3adant3	$⊢ ((((F : V \underset{1-1 onto}{⟶} Vtx (H) \land g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land k \in Edg (G) \land (G \in UHGraph \land H \in UHGraph)) \land X \in V \land j \in dom iEdg (G)) \land iEdg (H) (g (j)) = F [iEdg (G) (j)] \land k = iEdg (G) (j)) \to (\{X, n\} \subseteq iEdg (G) (j) \to ((n \in V \land X \in V) \to \exists e \in Edg (H) \{F (X), F (n)\} \subseteq e))$
92	58 91	sylbid	$⊢ ((((F : V \underset{1-1 onto}{⟶} Vtx (H) \land g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land k \in Edg (G) \land (G \in UHGraph \land H \in UHGraph)) \land X \in V \land j \in dom iEdg (G)) \land iEdg (H) (g (j)) = F [iEdg (G) (j)] \land k = iEdg (G) (j)) \to (\{X, n\} \subseteq k \to ((n \in V \land X \in V) \to \exists e \in Edg (H) \{F (X), F (n)\} \subseteq e))$
93	92	3exp	$⊢ (((F : V \underset{1-1 onto}{⟶} Vtx (H) \land g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land k \in Edg (G) \land (G \in UHGraph \land H \in UHGraph)) \land X \in V \land j \in dom iEdg (G)) \to (iEdg (H) (g (j)) = F [iEdg (G) (j)] \to (k = iEdg (G) (j) \to (\{X, n\} \subseteq k \to ((n \in V \land X \in V) \to \exists e \in Edg (H) \{F (X), F (n)\} \subseteq e))))$
94	56 93	syld	$⊢ (((F : V \underset{1-1 onto}{⟶} Vtx (H) \land g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land k \in Edg (G) \land (G \in UHGraph \land H \in UHGraph)) \land X \in V \land j \in dom iEdg (G)) \to (\forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)] \to (k = iEdg (G) (j) \to (\{X, n\} \subseteq k \to ((n \in V \land X \in V) \to \exists e \in Edg (H) \{F (X), F (n)\} \subseteq e))))$
95	94	3exp	$⊢ ((F : V \underset{1-1 onto}{⟶} Vtx (H) \land g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land k \in Edg (G) \land (G \in UHGraph \land H \in UHGraph)) \to (X \in V \to (j \in dom iEdg (G) \to (\forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)] \to (k = iEdg (G) (j) \to (\{X, n\} \subseteq k \to ((n \in V \land X \in V) \to \exists e \in Edg (H) \{F (X), F (n)\} \subseteq e))))))$
96	95	com34	$⊢ ((F : V \underset{1-1 onto}{⟶} Vtx (H) \land g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \land k \in Edg (G) \land (G \in UHGraph \land H \in UHGraph)) \to (X \in V \to (\forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)] \to (j \in dom iEdg (G) \to (k = iEdg (G) (j) \to (\{X, n\} \subseteq k \to ((n \in V \land X \in V) \to \exists e \in Edg (H) \{F (X), F (n)\} \subseteq e))))))$
97	96	3exp	$⊢ (F : V \underset{1-1 onto}{⟶} Vtx (H) \land g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \to (k \in Edg (G) \to ((G \in UHGraph \land H \in UHGraph) \to (X \in V \to (\forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)] \to (j \in dom iEdg (G) \to (k = iEdg (G) (j) \to (\{X, n\} \subseteq k \to ((n \in V \land X \in V) \to \exists e \in Edg (H) \{F (X), F (n)\} \subseteq e))))))))$
98	97	com25	$⊢ (F : V \underset{1-1 onto}{⟶} Vtx (H) \land g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H)) \to (\forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)] \to ((G \in UHGraph \land H \in UHGraph) \to (X \in V \to (k \in Edg (G) \to (j \in dom iEdg (G) \to (k = iEdg (G) (j) \to (\{X, n\} \subseteq k \to ((n \in V \land X \in V) \to \exists e \in Edg (H) \{F (X), F (n)\} \subseteq e))))))))$
99	98	expimpd	$⊢ F : V \underset{1-1 onto}{⟶} Vtx (H) \to ((g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)]) \to ((G \in UHGraph \land H \in UHGraph) \to (X \in V \to (k \in Edg (G) \to (j \in dom iEdg (G) \to (k = iEdg (G) (j) \to (\{X, n\} \subseteq k \to ((n \in V \land X \in V) \to \exists e \in Edg (H) \{F (X), F (n)\} \subseteq e))))))))$
100	99	exlimdv	$⊢ F : V \underset{1-1 onto}{⟶} Vtx (H) \to (\exists g (g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)]) \to ((G \in UHGraph \land H \in UHGraph) \to (X \in V \to (k \in Edg (G) \to (j \in dom iEdg (G) \to (k = iEdg (G) (j) \to (\{X, n\} \subseteq k \to ((n \in V \land X \in V) \to \exists e \in Edg (H) \{F (X), F (n)\} \subseteq e))))))))$
101	100	imp	$⊢ (F : V \underset{1-1 onto}{⟶} Vtx (H) \land \exists g (g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)])) \to ((G \in UHGraph \land H \in UHGraph) \to (X \in V \to (k \in Edg (G) \to (j \in dom iEdg (G) \to (k = iEdg (G) (j) \to (\{X, n\} \subseteq k \to ((n \in V \land X \in V) \to \exists e \in Edg (H) \{F (X), F (n)\} \subseteq e)))))))$
102	101	3imp	$⊢ ((F : V \underset{1-1 onto}{⟶} Vtx (H) \land \exists g (g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)])) \land (G \in UHGraph \land H \in UHGraph) \land X \in V) \to (k \in Edg (G) \to (j \in dom iEdg (G) \to (k = iEdg (G) (j) \to (\{X, n\} \subseteq k \to ((n \in V \land X \in V) \to \exists e \in Edg (H) \{F (X), F (n)\} \subseteq e)))))$
103	102	imp31	$⊢ ((((F : V \underset{1-1 onto}{⟶} Vtx (H) \land \exists g (g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)])) \land (G \in UHGraph \land H \in UHGraph) \land X \in V) \land k \in Edg (G)) \land j \in dom iEdg (G)) \to (k = iEdg (G) (j) \to (\{X, n\} \subseteq k \to ((n \in V \land X \in V) \to \exists e \in Edg (H) \{F (X), F (n)\} \subseteq e)))$
104	103	rexlimdva	$⊢ (((F : V \underset{1-1 onto}{⟶} Vtx (H) \land \exists g (g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)])) \land (G \in UHGraph \land H \in UHGraph) \land X \in V) \land k \in Edg (G)) \to (\exists j \in dom iEdg (G) k = iEdg (G) (j) \to (\{X, n\} \subseteq k \to ((n \in V \land X \in V) \to \exists e \in Edg (H) \{F (X), F (n)\} \subseteq e)))$
105	50 104	mpd	$⊢ (((F : V \underset{1-1 onto}{⟶} Vtx (H) \land \exists g (g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)])) \land (G \in UHGraph \land H \in UHGraph) \land X \in V) \land k \in Edg (G)) \to (\{X, n\} \subseteq k \to ((n \in V \land X \in V) \to \exists e \in Edg (H) \{F (X), F (n)\} \subseteq e))$
106	105	ex	$⊢ ((F : V \underset{1-1 onto}{⟶} Vtx (H) \land \exists g (g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)])) \land (G \in UHGraph \land H \in UHGraph) \land X \in V) \to (k \in Edg (G) \to (\{X, n\} \subseteq k \to ((n \in V \land X \in V) \to \exists e \in Edg (H) \{F (X), F (n)\} \subseteq e)))$
107	106	com14	$⊢ (n \in V \land X \in V) \to (k \in Edg (G) \to (\{X, n\} \subseteq k \to (((F : V \underset{1-1 onto}{⟶} Vtx (H) \land \exists g (g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)])) \land (G \in UHGraph \land H \in UHGraph) \land X \in V) \to \exists e \in Edg (H) \{F (X), F (n)\} \subseteq e)))$
108	107	imp	$⊢ ((n \in V \land X \in V) \land k \in Edg (G)) \to (\{X, n\} \subseteq k \to (((F : V \underset{1-1 onto}{⟶} Vtx (H) \land \exists g (g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)])) \land (G \in UHGraph \land H \in UHGraph) \land X \in V) \to \exists e \in Edg (H) \{F (X), F (n)\} \subseteq e))$
109	108	3imp	$⊢ (((n \in V \land X \in V) \land k \in Edg (G)) \land \{X, n\} \subseteq k \land ((F : V \underset{1-1 onto}{⟶} Vtx (H) \land \exists g (g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)])) \land (G \in UHGraph \land H \in UHGraph) \land X \in V)) \to \exists e \in Edg (H) \{F (X), F (n)\} \subseteq e$
110	109	olcd	$⊢ (((n \in V \land X \in V) \land k \in Edg (G)) \land \{X, n\} \subseteq k \land ((F : V \underset{1-1 onto}{⟶} Vtx (H) \land \exists g (g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)])) \land (G \in UHGraph \land H \in UHGraph) \land X \in V)) \to (F (n) = F (X) \lor \exists e \in Edg (H) \{F (X), F (n)\} \subseteq e)$
111	110	3exp	$⊢ ((n \in V \land X \in V) \land k \in Edg (G)) \to (\{X, n\} \subseteq k \to (((F : V \underset{1-1 onto}{⟶} Vtx (H) \land \exists g (g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)])) \land (G \in UHGraph \land H \in UHGraph) \land X \in V) \to (F (n) = F (X) \lor \exists e \in Edg (H) \{F (X), F (n)\} \subseteq e)))$
112	111	rexlimdva	$⊢ (n \in V \land X \in V) \to (\exists k \in Edg (G) \{X, n\} \subseteq k \to (((F : V \underset{1-1 onto}{⟶} Vtx (H) \land \exists g (g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)])) \land (G \in UHGraph \land H \in UHGraph) \land X \in V) \to (F (n) = F (X) \lor \exists e \in Edg (H) \{F (X), F (n)\} \subseteq e)))$
113	112	com12	$⊢ \exists k \in Edg (G) \{X, n\} \subseteq k \to ((n \in V \land X \in V) \to (((F : V \underset{1-1 onto}{⟶} Vtx (H) \land \exists g (g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)])) \land (G \in UHGraph \land H \in UHGraph) \land X \in V) \to (F (n) = F (X) \lor \exists e \in Edg (H) \{F (X), F (n)\} \subseteq e)))$
114	46 113	jaoi	$⊢ (n = X \lor \exists k \in Edg (G) \{X, n\} \subseteq k) \to ((n \in V \land X \in V) \to (((F : V \underset{1-1 onto}{⟶} Vtx (H) \land \exists g (g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)])) \land (G \in UHGraph \land H \in UHGraph) \land X \in V) \to (F (n) = F (X) \lor \exists e \in Edg (H) \{F (X), F (n)\} \subseteq e)))$
115	114	impcom	$⊢ ((n \in V \land X \in V) \land (n = X \lor \exists k \in Edg (G) \{X, n\} \subseteq k)) \to (((F : V \underset{1-1 onto}{⟶} Vtx (H) \land \exists g (g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)])) \land (G \in UHGraph \land H \in UHGraph) \land X \in V) \to (F (n) = F (X) \lor \exists e \in Edg (H) \{F (X), F (n)\} \subseteq e))$
116	43 115	sylbi	$⊢ n \in (G ClNeighbVtx X) \to (((F : V \underset{1-1 onto}{⟶} Vtx (H) \land \exists g (g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)])) \land (G \in UHGraph \land H \in UHGraph) \land X \in V) \to (F (n) = F (X) \lor \exists e \in Edg (H) \{F (X), F (n)\} \subseteq e))$
117	116	impcom	$⊢ (((F : V \underset{1-1 onto}{⟶} Vtx (H) \land \exists g (g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)])) \land (G \in UHGraph \land H \in UHGraph) \land X \in V) \land n \in (G ClNeighbVtx X)) \to (F (n) = F (X) \lor \exists e \in Edg (H) \{F (X), F (n)\} \subseteq e)$
118	117	adantr	$⊢ ((((F : V \underset{1-1 onto}{⟶} Vtx (H) \land \exists g (g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)])) \land (G \in UHGraph \land H \in UHGraph) \land X \in V) \land n \in (G ClNeighbVtx X)) \land F (n) = x) \to (F (n) = F (X) \lor \exists e \in Edg (H) \{F (X), F (n)\} \subseteq e)$
119		eqeq1	$⊢ x = F (n) \to (x = F (X) \leftrightarrow F (n) = F (X))$
120		preq2	$⊢ x = F (n) \to \{F (X), x\} = \{F (X), F (n)\}$
121	120	sseq1d	$⊢ x = F (n) \to (\{F (X), x\} \subseteq e \leftrightarrow \{F (X), F (n)\} \subseteq e)$
122	121	rexbidv	$⊢ x = F (n) \to (\exists e \in Edg (H) \{F (X), x\} \subseteq e \leftrightarrow \exists e \in Edg (H) \{F (X), F (n)\} \subseteq e)$
123	119 122	orbi12d	$⊢ x = F (n) \to ((x = F (X) \lor \exists e \in Edg (H) \{F (X), x\} \subseteq e) \leftrightarrow (F (n) = F (X) \lor \exists e \in Edg (H) \{F (X), F (n)\} \subseteq e))$
124	123	eqcoms	$⊢ F (n) = x \to ((x = F (X) \lor \exists e \in Edg (H) \{F (X), x\} \subseteq e) \leftrightarrow (F (n) = F (X) \lor \exists e \in Edg (H) \{F (X), F (n)\} \subseteq e))$
125	124	adantl	$⊢ ((((F : V \underset{1-1 onto}{⟶} Vtx (H) \land \exists g (g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)])) \land (G \in UHGraph \land H \in UHGraph) \land X \in V) \land n \in (G ClNeighbVtx X)) \land F (n) = x) \to ((x = F (X) \lor \exists e \in Edg (H) \{F (X), x\} \subseteq e) \leftrightarrow (F (n) = F (X) \lor \exists e \in Edg (H) \{F (X), F (n)\} \subseteq e))$
126	118 125	mpbird	$⊢ ((((F : V \underset{1-1 onto}{⟶} Vtx (H) \land \exists g (g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)])) \land (G \in UHGraph \land H \in UHGraph) \land X \in V) \land n \in (G ClNeighbVtx X)) \land F (n) = x) \to (x = F (X) \lor \exists e \in Edg (H) \{F (X), x\} \subseteq e)$
127	38 41 126	jca31	$⊢ ((((F : V \underset{1-1 onto}{⟶} Vtx (H) \land \exists g (g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)])) \land (G \in UHGraph \land H \in UHGraph) \land X \in V) \land n \in (G ClNeighbVtx X)) \land F (n) = x) \to ((x \in Vtx (H) \land F (X) \in Vtx (H)) \land (x = F (X) \lor \exists e \in Edg (H) \{F (X), x\} \subseteq e))$
128	127	ex	$⊢ (((F : V \underset{1-1 onto}{⟶} Vtx (H) \land \exists g (g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)])) \land (G \in UHGraph \land H \in UHGraph) \land X \in V) \land n \in (G ClNeighbVtx X)) \to (F (n) = x \to ((x \in Vtx (H) \land F (X) \in Vtx (H)) \land (x = F (X) \lor \exists e \in Edg (H) \{F (X), x\} \subseteq e)))$
129	128	rexlimdva	$⊢ ((F : V \underset{1-1 onto}{⟶} Vtx (H) \land \exists g (g : dom iEdg (G) \underset{1-1 onto}{⟶} dom iEdg (H) \land \forall i \in dom iEdg (G) iEdg (H) (g (i)) = F [iEdg (G) (i)])) \land (G \in UHGraph \land H \in UHGraph) \land X \in V) \to (\exists n \in (G ClNeighbVtx X) F (n) = x \to ((x \in Vtx (H) \land F (X) \in Vtx (H)) \land (x = F (X) \lor \exists e \in Edg (H) \{F (X), x\} \subseteq e)))$
130	26 129	syl3an1	$⊢ (F \in (G GraphIso H) \land (G \in UHGraph \land H \in UHGraph) \land X \in V) \to (\exists n \in (G ClNeighbVtx X) F (n) = x \to ((x \in Vtx (H) \land F (X) \in Vtx (H)) \land (x = F (X) \lor \exists e \in Edg (H) \{F (X), x\} \subseteq e)))$
131	23 130	impbid	$⊢ (F \in (G GraphIso H) \land (G \in UHGraph \land H \in UHGraph) \land X \in V) \to (((x \in Vtx (H) \land F (X) \in Vtx (H)) \land (x = F (X) \lor \exists e \in Edg (H) \{F (X), x\} \subseteq e)) \leftrightarrow \exists n \in (G ClNeighbVtx X) F (n) = x)$
132	131	3exp	$⊢ F \in (G GraphIso H) \to ((G \in UHGraph \land H \in UHGraph) \to (X \in V \to (((x \in Vtx (H) \land F (X) \in Vtx (H)) \land (x = F (X) \lor \exists e \in Edg (H) \{F (X), x\} \subseteq e)) \leftrightarrow \exists n \in (G ClNeighbVtx X) F (n) = x)))$
133	132	impcom	$⊢ ((G \in UHGraph \land H \in UHGraph) \land F \in (G GraphIso H)) \to (X \in V \to (((x \in Vtx (H) \land F (X) \in Vtx (H)) \land (x = F (X) \lor \exists e \in Edg (H) \{F (X), x\} \subseteq e)) \leftrightarrow \exists n \in (G ClNeighbVtx X) F (n) = x))$
134	133	imp	$⊢ (((G \in UHGraph \land H \in UHGraph) \land F \in (G GraphIso H)) \land X \in V) \to (((x \in Vtx (H) \land F (X) \in Vtx (H)) \land (x = F (X) \lor \exists e \in Edg (H) \{F (X), x\} \subseteq e)) \leftrightarrow \exists n \in (G ClNeighbVtx X) F (n) = x)$
135	16 17	clnbgrel	$⊢ x \in (H ClNeighbVtx F (X)) \leftrightarrow ((x \in Vtx (H) \land F (X) \in Vtx (H)) \land (x = F (X) \lor \exists e \in Edg (H) \{F (X), x\} \subseteq e))$
136	135	a1i	$⊢ (((G \in UHGraph \land H \in UHGraph) \land F \in (G GraphIso H)) \land X \in V) \to (x \in (H ClNeighbVtx F (X)) \leftrightarrow ((x \in Vtx (H) \land F (X) \in Vtx (H)) \land (x = F (X) \lor \exists e \in Edg (H) \{F (X), x\} \subseteq e)))$
137	1 16	grimf1o	$⊢ F \in (G GraphIso H) \to F : V \underset{1-1 onto}{⟶} Vtx (H)$
138	137 72	syl	$⊢ F \in (G GraphIso H) \to F Fn V$
139	138	adantl	$⊢ ((G \in UHGraph \land H \in UHGraph) \land F \in (G GraphIso H)) \to F Fn V$
140	1	clnbgrssvtx	$⊢ G ClNeighbVtx X \subseteq V$
141	140	a1i	$⊢ X \in V \to G ClNeighbVtx X \subseteq V$
142		fvelimab	$⊢ (F Fn V \land G ClNeighbVtx X \subseteq V) \to (x \in F [G ClNeighbVtx X] \leftrightarrow \exists n \in (G ClNeighbVtx X) F (n) = x)$
143	139 141 142	syl2an	$⊢ (((G \in UHGraph \land H \in UHGraph) \land F \in (G GraphIso H)) \land X \in V) \to (x \in F [G ClNeighbVtx X] \leftrightarrow \exists n \in (G ClNeighbVtx X) F (n) = x)$
144	134 136 143	3bitr4d	$⊢ (((G \in UHGraph \land H \in UHGraph) \land F \in (G GraphIso H)) \land X \in V) \to (x \in (H ClNeighbVtx F (X)) \leftrightarrow x \in F [G ClNeighbVtx X])$
145	144	eqrdv	$⊢ (((G \in UHGraph \land H \in UHGraph) \land F \in (G GraphIso H)) \land X \in V) \to H ClNeighbVtx F (X) = F [G ClNeighbVtx X]$

Metamath Proof Explorer

Theorem clnbgrgrim

Proof