uspgrimprop

Description: An isomorphism of simple pseudographs is a bijection between their vertices that preserves adjacency, i.e. there is an edge in one graph connecting one or two vertices iff there is an edge in the other graph connecting the vertices which are the images of the vertices. (Contributed by AV, 27-Apr-2025)

	Ref	Expression
Hypotheses	isusgrim.v	$⊢ V = Vtx (G)$
	isusgrim.w	$⊢ W = Vtx (H)$
	isusgrim.e	$⊢ E = Edg (G)$
	isusgrim.d	$⊢ D = Edg (H)$
Assertion	uspgrimprop	$⊢ (G \in USHGraph \land H \in USHGraph) \to (F \in (G GraphIso H) \to (F : V \underset{1-1 onto}{⟶} W \land \forall x \in V \forall y \in V (\{x, y\} \in E \leftrightarrow \{F (x), F (y)\} \in D)))$

Proof

Step	Hyp	Ref	Expression
1		isusgrim.v	$⊢ V = Vtx (G)$
2		isusgrim.w	$⊢ W = Vtx (H)$
3		isusgrim.e	$⊢ E = Edg (G)$
4		isusgrim.d	$⊢ D = Edg (H)$
5	1 2 3 4	isuspgrim0	$⊢ (G \in USHGraph \land H \in USHGraph \land F \in (G GraphIso H)) \to (F \in (G GraphIso H) \leftrightarrow (F : V \underset{1-1 onto}{⟶} W \land (e \in E ⟼ F [e]) : E \underset{1-1 onto}{⟶} D))$
6	5	3expa	$⊢ ((G \in USHGraph \land H \in USHGraph) \land F \in (G GraphIso H)) \to (F \in (G GraphIso H) \leftrightarrow (F : V \underset{1-1 onto}{⟶} W \land (e \in E ⟼ F [e]) : E \underset{1-1 onto}{⟶} D))$
7		simprl	$⊢ ((G \in USHGraph \land H \in USHGraph) \land (F : V \underset{1-1 onto}{⟶} W \land (e \in E ⟼ F [e]) : E \underset{1-1 onto}{⟶} D)) \to F : V \underset{1-1 onto}{⟶} W$
8		imaeq2	$⊢ e = \{x, y\} \to F [e] = F [\{x, y\}]$
9		eqidd	$⊢ (F : V \underset{1-1 onto}{⟶} W \land \{x, y\} \in E) \to (e \in E ⟼ F [e]) = (e \in E ⟼ F [e])$
10		simpr	$⊢ (F : V \underset{1-1 onto}{⟶} W \land \{x, y\} \in E) \to \{x, y\} \in E$
11		f1ofun	$⊢ F : V \underset{1-1 onto}{⟶} W \to Fun F$
12		zfpair2	$⊢ \{x, y\} \in V$
13		funimaexg	$⊢ (Fun F \land \{x, y\} \in V) \to F [\{x, y\}] \in V$
14	11 12 13	sylancl	$⊢ F : V \underset{1-1 onto}{⟶} W \to F [\{x, y\}] \in V$
15	14	adantr	$⊢ (F : V \underset{1-1 onto}{⟶} W \land \{x, y\} \in E) \to F [\{x, y\}] \in V$
16	8 9 10 15	fvmptd4	$⊢ (F : V \underset{1-1 onto}{⟶} W \land \{x, y\} \in E) \to (e \in E ⟼ F [e]) (\{x, y\}) = F [\{x, y\}]$
17	16	ex	$⊢ F : V \underset{1-1 onto}{⟶} W \to (\{x, y\} \in E \to (e \in E ⟼ F [e]) (\{x, y\}) = F [\{x, y\}])$
18	17	adantr	$⊢ (F : V \underset{1-1 onto}{⟶} W \land (e \in E ⟼ F [e]) : E \underset{1-1 onto}{⟶} D) \to (\{x, y\} \in E \to (e \in E ⟼ F [e]) (\{x, y\}) = F [\{x, y\}])$
19	18	ad2antlr	$⊢ (((G \in USHGraph \land H \in USHGraph) \land (F : V \underset{1-1 onto}{⟶} W \land (e \in E ⟼ F [e]) : E \underset{1-1 onto}{⟶} D)) \land (x \in V \land y \in V)) \to (\{x, y\} \in E \to (e \in E ⟼ F [e]) (\{x, y\}) = F [\{x, y\}])$
20	19	imp	$⊢ ((((G \in USHGraph \land H \in USHGraph) \land (F : V \underset{1-1 onto}{⟶} W \land (e \in E ⟼ F [e]) : E \underset{1-1 onto}{⟶} D)) \land (x \in V \land y \in V)) \land \{x, y\} \in E) \to (e \in E ⟼ F [e]) (\{x, y\}) = F [\{x, y\}]$
21		f1of	$⊢ (e \in E ⟼ F [e]) : E \underset{1-1 onto}{⟶} D \to (e \in E ⟼ F [e]) : E ⟶ D$
22	21	ad2antll	$⊢ ((G \in USHGraph \land H \in USHGraph) \land (F : V \underset{1-1 onto}{⟶} W \land (e \in E ⟼ F [e]) : E \underset{1-1 onto}{⟶} D)) \to (e \in E ⟼ F [e]) : E ⟶ D$
23		ax-1	$⊢ \emptyset \notin D \to (H \in USHGraph \to \emptyset \notin D)$
24		nnel	$⊢ \neg \emptyset \notin D \leftrightarrow \emptyset \in D$
25		uspgruhgr	$⊢ H \in USHGraph \to H \in UHGraph$
26		uhgredgn0	$⊢ (H \in UHGraph \land \emptyset \in Edg (H)) \to \emptyset \in (𝒫 Vtx (H) ∖ \{\emptyset\})$
27	25 26	sylan	$⊢ (H \in USHGraph \land \emptyset \in Edg (H)) \to \emptyset \in (𝒫 Vtx (H) ∖ \{\emptyset\})$
28		neldifsn	$⊢ \neg \emptyset \in (𝒫 Vtx (H) ∖ \{\emptyset\})$
29	28	pm2.21i	$⊢ \emptyset \in (𝒫 Vtx (H) ∖ \{\emptyset\}) \to \emptyset \notin D$
30	27 29	syl	$⊢ (H \in USHGraph \land \emptyset \in Edg (H)) \to \emptyset \notin D$
31	30	expcom	$⊢ \emptyset \in Edg (H) \to (H \in USHGraph \to \emptyset \notin D)$
32	31 4	eleq2s	$⊢ \emptyset \in D \to (H \in USHGraph \to \emptyset \notin D)$
33	24 32	sylbi	$⊢ \neg \emptyset \notin D \to (H \in USHGraph \to \emptyset \notin D)$
34	23 33	pm2.61i	$⊢ H \in USHGraph \to \emptyset \notin D$
35	34	ad2antlr	$⊢ ((G \in USHGraph \land H \in USHGraph) \land (F : V \underset{1-1 onto}{⟶} W \land (e \in E ⟼ F [e]) : E \underset{1-1 onto}{⟶} D)) \to \emptyset \notin D$
36	22 35	jca	$⊢ ((G \in USHGraph \land H \in USHGraph) \land (F : V \underset{1-1 onto}{⟶} W \land (e \in E ⟼ F [e]) : E \underset{1-1 onto}{⟶} D)) \to ((e \in E ⟼ F [e]) : E ⟶ D \land \emptyset \notin D)$
37	36	adantr	$⊢ (((G \in USHGraph \land H \in USHGraph) \land (F : V \underset{1-1 onto}{⟶} W \land (e \in E ⟼ F [e]) : E \underset{1-1 onto}{⟶} D)) \land (x \in V \land y \in V)) \to ((e \in E ⟼ F [e]) : E ⟶ D \land \emptyset \notin D)$
38		feldmfvelcdm	$⊢ ((e \in E ⟼ F [e]) : E ⟶ D \land \emptyset \notin D) \to (\{x, y\} \in E \leftrightarrow (e \in E ⟼ F [e]) (\{x, y\}) \in D)$
39	37 38	syl	$⊢ (((G \in USHGraph \land H \in USHGraph) \land (F : V \underset{1-1 onto}{⟶} W \land (e \in E ⟼ F [e]) : E \underset{1-1 onto}{⟶} D)) \land (x \in V \land y \in V)) \to (\{x, y\} \in E \leftrightarrow (e \in E ⟼ F [e]) (\{x, y\}) \in D)$
40	39	biimpa	$⊢ ((((G \in USHGraph \land H \in USHGraph) \land (F : V \underset{1-1 onto}{⟶} W \land (e \in E ⟼ F [e]) : E \underset{1-1 onto}{⟶} D)) \land (x \in V \land y \in V)) \land \{x, y\} \in E) \to (e \in E ⟼ F [e]) (\{x, y\}) \in D$
41	20 40	eqeltrrd	$⊢ ((((G \in USHGraph \land H \in USHGraph) \land (F : V \underset{1-1 onto}{⟶} W \land (e \in E ⟼ F [e]) : E \underset{1-1 onto}{⟶} D)) \land (x \in V \land y \in V)) \land \{x, y\} \in E) \to F [\{x, y\}] \in D$
42		imaeq2	$⊢ z = F [\{x, y\}] \to F^{-1} [z] = F^{-1} [F [\{x, y\}]]$
43		imaeq2	$⊢ e = y \to F [e] = F [y]$
44	43	cbvmptv	$⊢ (e \in E ⟼ F [e]) = (y \in E ⟼ F [y])$
45		f1oeq1	$⊢ (e \in E ⟼ F [e]) = (y \in E ⟼ F [y]) \to ((e \in E ⟼ F [e]) : E \underset{1-1 onto}{⟶} D \leftrightarrow (y \in E ⟼ F [y]) : E \underset{1-1 onto}{⟶} D)$
46	44 45	mp1i	$⊢ ((G \in USHGraph \land H \in USHGraph) \land F : V \underset{1-1 onto}{⟶} W) \to ((e \in E ⟼ F [e]) : E \underset{1-1 onto}{⟶} D \leftrightarrow (y \in E ⟼ F [y]) : E \underset{1-1 onto}{⟶} D)$
47		imaeq2	$⊢ e = x \to F [e] = F [x]$
48	47	cbvmptv	$⊢ (e \in E ⟼ F [e]) = (x \in E ⟼ F [x])$
49		simpr	$⊢ ((G \in USHGraph \land H \in USHGraph) \land F : V \underset{1-1 onto}{⟶} W) \to F : V \underset{1-1 onto}{⟶} W$
50	49	adantr	$⊢ (((G \in USHGraph \land H \in USHGraph) \land F : V \underset{1-1 onto}{⟶} W) \land (y \in E ⟼ F [y]) : E \underset{1-1 onto}{⟶} D) \to F : V \underset{1-1 onto}{⟶} W$
51		uspgruhgr	$⊢ G \in USHGraph \to G \in UHGraph$
52		uhgredgss	$⊢ G \in UHGraph \to Edg (G) \subseteq 𝒫 Vtx (G) ∖ \{\emptyset\}$
53		difss2	$⊢ Edg (G) \subseteq 𝒫 Vtx (G) ∖ \{\emptyset\} \to Edg (G) \subseteq 𝒫 Vtx (G)$
54	51 52 53	3syl	$⊢ G \in USHGraph \to Edg (G) \subseteq 𝒫 Vtx (G)$
55	1	pweqi	$⊢ 𝒫 V = 𝒫 Vtx (G)$
56	54 3 55	3sstr4g	$⊢ G \in USHGraph \to E \subseteq 𝒫 V$
57	56	adantr	$⊢ (G \in USHGraph \land H \in USHGraph) \to E \subseteq 𝒫 V$
58	57	ad2antrr	$⊢ (((G \in USHGraph \land H \in USHGraph) \land F : V \underset{1-1 onto}{⟶} W) \land (y \in E ⟼ F [y]) : E \underset{1-1 onto}{⟶} D) \to E \subseteq 𝒫 V$
59		f1ofo	$⊢ (y \in E ⟼ F [y]) : E \underset{1-1 onto}{⟶} D \to (y \in E ⟼ F [y]) : E \underset{onto}{⟶} D$
60	44	rneqi	$⊢ ran (e \in E ⟼ F [e]) = ran (y \in E ⟼ F [y])$
61		forn	$⊢ (y \in E ⟼ F [y]) : E \underset{onto}{⟶} D \to ran (y \in E ⟼ F [y]) = D$
62	60 61	eqtrid	$⊢ (y \in E ⟼ F [y]) : E \underset{onto}{⟶} D \to ran (e \in E ⟼ F [e]) = D$
63	59 62	syl	$⊢ (y \in E ⟼ F [y]) : E \underset{1-1 onto}{⟶} D \to ran (e \in E ⟼ F [e]) = D$
64	63	adantl	$⊢ (((G \in USHGraph \land H \in USHGraph) \land F : V \underset{1-1 onto}{⟶} W) \land (y \in E ⟼ F [y]) : E \underset{1-1 onto}{⟶} D) \to ran (e \in E ⟼ F [e]) = D$
65		uhgredgss	$⊢ H \in UHGraph \to Edg (H) \subseteq 𝒫 Vtx (H) ∖ \{\emptyset\}$
66		difss2	$⊢ Edg (H) \subseteq 𝒫 Vtx (H) ∖ \{\emptyset\} \to Edg (H) \subseteq 𝒫 Vtx (H)$
67	25 65 66	3syl	$⊢ H \in USHGraph \to Edg (H) \subseteq 𝒫 Vtx (H)$
68	2	pweqi	$⊢ 𝒫 W = 𝒫 Vtx (H)$
69	67 4 68	3sstr4g	$⊢ H \in USHGraph \to D \subseteq 𝒫 W$
70	69	adantl	$⊢ (G \in USHGraph \land H \in USHGraph) \to D \subseteq 𝒫 W$
71	70	ad2antrr	$⊢ (((G \in USHGraph \land H \in USHGraph) \land F : V \underset{1-1 onto}{⟶} W) \land (y \in E ⟼ F [y]) : E \underset{1-1 onto}{⟶} D) \to D \subseteq 𝒫 W$
72	64 71	eqsstrd	$⊢ (((G \in USHGraph \land H \in USHGraph) \land F : V \underset{1-1 onto}{⟶} W) \land (y \in E ⟼ F [y]) : E \underset{1-1 onto}{⟶} D) \to ran (e \in E ⟼ F [e]) \subseteq 𝒫 W$
73	1	fvexi	$⊢ V \in V$
74	73	a1i	$⊢ (((G \in USHGraph \land H \in USHGraph) \land F : V \underset{1-1 onto}{⟶} W) \land (y \in E ⟼ F [y]) : E \underset{1-1 onto}{⟶} D) \to V \in V$
75	48 50 58 72 74	mptcnfimad	$⊢ (((G \in USHGraph \land H \in USHGraph) \land F : V \underset{1-1 onto}{⟶} W) \land (y \in E ⟼ F [y]) : E \underset{1-1 onto}{⟶} D) \to {(e \in E ⟼ F [e])}^{-1} = (z \in ran (e \in E ⟼ F [e]) ⟼ F^{-1} [z])$
76	75	ex	$⊢ ((G \in USHGraph \land H \in USHGraph) \land F : V \underset{1-1 onto}{⟶} W) \to ((y \in E ⟼ F [y]) : E \underset{1-1 onto}{⟶} D \to {(e \in E ⟼ F [e])}^{-1} = (z \in ran (e \in E ⟼ F [e]) ⟼ F^{-1} [z]))$
77	46 76	sylbid	$⊢ ((G \in USHGraph \land H \in USHGraph) \land F : V \underset{1-1 onto}{⟶} W) \to ((e \in E ⟼ F [e]) : E \underset{1-1 onto}{⟶} D \to {(e \in E ⟼ F [e])}^{-1} = (z \in ran (e \in E ⟼ F [e]) ⟼ F^{-1} [z]))$
78	77	impr	$⊢ ((G \in USHGraph \land H \in USHGraph) \land (F : V \underset{1-1 onto}{⟶} W \land (e \in E ⟼ F [e]) : E \underset{1-1 onto}{⟶} D)) \to {(e \in E ⟼ F [e])}^{-1} = (z \in ran (e \in E ⟼ F [e]) ⟼ F^{-1} [z])$
79	78	ad2antrr	$⊢ ((((G \in USHGraph \land H \in USHGraph) \land (F : V \underset{1-1 onto}{⟶} W \land (e \in E ⟼ F [e]) : E \underset{1-1 onto}{⟶} D)) \land (x \in V \land y \in V)) \land F [\{x, y\}] \in D) \to {(e \in E ⟼ F [e])}^{-1} = (z \in ran (e \in E ⟼ F [e]) ⟼ F^{-1} [z])$
80		f1ofo	$⊢ (e \in E ⟼ F [e]) : E \underset{1-1 onto}{⟶} D \to (e \in E ⟼ F [e]) : E \underset{onto}{⟶} D$
81		forn	$⊢ (e \in E ⟼ F [e]) : E \underset{onto}{⟶} D \to ran (e \in E ⟼ F [e]) = D$
82	81	eqcomd	$⊢ (e \in E ⟼ F [e]) : E \underset{onto}{⟶} D \to D = ran (e \in E ⟼ F [e])$
83	80 82	syl	$⊢ (e \in E ⟼ F [e]) : E \underset{1-1 onto}{⟶} D \to D = ran (e \in E ⟼ F [e])$
84	83	adantl	$⊢ (F : V \underset{1-1 onto}{⟶} W \land (e \in E ⟼ F [e]) : E \underset{1-1 onto}{⟶} D) \to D = ran (e \in E ⟼ F [e])$
85	84	ad2antlr	$⊢ (((G \in USHGraph \land H \in USHGraph) \land (F : V \underset{1-1 onto}{⟶} W \land (e \in E ⟼ F [e]) : E \underset{1-1 onto}{⟶} D)) \land (x \in V \land y \in V)) \to D = ran (e \in E ⟼ F [e])$
86	85	eleq2d	$⊢ (((G \in USHGraph \land H \in USHGraph) \land (F : V \underset{1-1 onto}{⟶} W \land (e \in E ⟼ F [e]) : E \underset{1-1 onto}{⟶} D)) \land (x \in V \land y \in V)) \to (F [\{x, y\}] \in D \leftrightarrow F [\{x, y\}] \in ran (e \in E ⟼ F [e]))$
87	86	biimpa	$⊢ ((((G \in USHGraph \land H \in USHGraph) \land (F : V \underset{1-1 onto}{⟶} W \land (e \in E ⟼ F [e]) : E \underset{1-1 onto}{⟶} D)) \land (x \in V \land y \in V)) \land F [\{x, y\}] \in D) \to F [\{x, y\}] \in ran (e \in E ⟼ F [e])$
88		dff1o2	$⊢ F : V \underset{1-1 onto}{⟶} W \leftrightarrow (F Fn V \land Fun F^{-1} \land ran F = W)$
89	88	simp2bi	$⊢ F : V \underset{1-1 onto}{⟶} W \to Fun F^{-1}$
90	89	adantr	$⊢ (F : V \underset{1-1 onto}{⟶} W \land (e \in E ⟼ F [e]) : E \underset{1-1 onto}{⟶} D) \to Fun F^{-1}$
91	90	ad2antlr	$⊢ (((G \in USHGraph \land H \in USHGraph) \land (F : V \underset{1-1 onto}{⟶} W \land (e \in E ⟼ F [e]) : E \underset{1-1 onto}{⟶} D)) \land (x \in V \land y \in V)) \to Fun F^{-1}$
92		funimaexg	$⊢ (Fun F^{-1} \land F [\{x, y\}] \in D) \to F^{-1} [F [\{x, y\}]] \in V$
93	91 92	sylan	$⊢ ((((G \in USHGraph \land H \in USHGraph) \land (F : V \underset{1-1 onto}{⟶} W \land (e \in E ⟼ F [e]) : E \underset{1-1 onto}{⟶} D)) \land (x \in V \land y \in V)) \land F [\{x, y\}] \in D) \to F^{-1} [F [\{x, y\}]] \in V$
94	42 79 87 93	fvmptd4	$⊢ ((((G \in USHGraph \land H \in USHGraph) \land (F : V \underset{1-1 onto}{⟶} W \land (e \in E ⟼ F [e]) : E \underset{1-1 onto}{⟶} D)) \land (x \in V \land y \in V)) \land F [\{x, y\}] \in D) \to {(e \in E ⟼ F [e])}^{-1} (F [\{x, y\}]) = F^{-1} [F [\{x, y\}]]$
95		simplrr	$⊢ (((G \in USHGraph \land H \in USHGraph) \land (F : V \underset{1-1 onto}{⟶} W \land (e \in E ⟼ F [e]) : E \underset{1-1 onto}{⟶} D)) \land (x \in V \land y \in V)) \to (e \in E ⟼ F [e]) : E \underset{1-1 onto}{⟶} D$
96		f1ocnvdm	$⊢ ((e \in E ⟼ F [e]) : E \underset{1-1 onto}{⟶} D \land F [\{x, y\}] \in D) \to {(e \in E ⟼ F [e])}^{-1} (F [\{x, y\}]) \in E$
97	95 96	sylan	$⊢ ((((G \in USHGraph \land H \in USHGraph) \land (F : V \underset{1-1 onto}{⟶} W \land (e \in E ⟼ F [e]) : E \underset{1-1 onto}{⟶} D)) \land (x \in V \land y \in V)) \land F [\{x, y\}] \in D) \to {(e \in E ⟼ F [e])}^{-1} (F [\{x, y\}]) \in E$
98	94 97	eqeltrrd	$⊢ ((((G \in USHGraph \land H \in USHGraph) \land (F : V \underset{1-1 onto}{⟶} W \land (e \in E ⟼ F [e]) : E \underset{1-1 onto}{⟶} D)) \land (x \in V \land y \in V)) \land F [\{x, y\}] \in D) \to F^{-1} [F [\{x, y\}]] \in E$
99		f1of1	$⊢ F : V \underset{1-1 onto}{⟶} W \to F : V \underset{1-1}{⟶} W$
100	99	ad2antrl	$⊢ ((G \in USHGraph \land H \in USHGraph) \land (F : V \underset{1-1 onto}{⟶} W \land (e \in E ⟼ F [e]) : E \underset{1-1 onto}{⟶} D)) \to F : V \underset{1-1}{⟶} W$
101		prssi	$⊢ (x \in V \land y \in V) \to \{x, y\} \subseteq V$
102		f1imacnv	$⊢ (F : V \underset{1-1}{⟶} W \land \{x, y\} \subseteq V) \to F^{-1} [F [\{x, y\}]] = \{x, y\}$
103	100 101 102	syl2an	$⊢ (((G \in USHGraph \land H \in USHGraph) \land (F : V \underset{1-1 onto}{⟶} W \land (e \in E ⟼ F [e]) : E \underset{1-1 onto}{⟶} D)) \land (x \in V \land y \in V)) \to F^{-1} [F [\{x, y\}]] = \{x, y\}$
104	103	eqcomd	$⊢ (((G \in USHGraph \land H \in USHGraph) \land (F : V \underset{1-1 onto}{⟶} W \land (e \in E ⟼ F [e]) : E \underset{1-1 onto}{⟶} D)) \land (x \in V \land y \in V)) \to \{x, y\} = F^{-1} [F [\{x, y\}]]$
105	104	eleq1d	$⊢ (((G \in USHGraph \land H \in USHGraph) \land (F : V \underset{1-1 onto}{⟶} W \land (e \in E ⟼ F [e]) : E \underset{1-1 onto}{⟶} D)) \land (x \in V \land y \in V)) \to (\{x, y\} \in E \leftrightarrow F^{-1} [F [\{x, y\}]] \in E)$
106	105	adantr	$⊢ ((((G \in USHGraph \land H \in USHGraph) \land (F : V \underset{1-1 onto}{⟶} W \land (e \in E ⟼ F [e]) : E \underset{1-1 onto}{⟶} D)) \land (x \in V \land y \in V)) \land F [\{x, y\}] \in D) \to (\{x, y\} \in E \leftrightarrow F^{-1} [F [\{x, y\}]] \in E)$
107	98 106	mpbird	$⊢ ((((G \in USHGraph \land H \in USHGraph) \land (F : V \underset{1-1 onto}{⟶} W \land (e \in E ⟼ F [e]) : E \underset{1-1 onto}{⟶} D)) \land (x \in V \land y \in V)) \land F [\{x, y\}] \in D) \to \{x, y\} \in E$
108	41 107	impbida	$⊢ (((G \in USHGraph \land H \in USHGraph) \land (F : V \underset{1-1 onto}{⟶} W \land (e \in E ⟼ F [e]) : E \underset{1-1 onto}{⟶} D)) \land (x \in V \land y \in V)) \to (\{x, y\} \in E \leftrightarrow F [\{x, y\}] \in D)$
109		f1ofn	$⊢ F : V \underset{1-1 onto}{⟶} W \to F Fn V$
110	109	ad2antrl	$⊢ ((G \in USHGraph \land H \in USHGraph) \land (F : V \underset{1-1 onto}{⟶} W \land (e \in E ⟼ F [e]) : E \underset{1-1 onto}{⟶} D)) \to F Fn V$
111	110	anim1i	$⊢ (((G \in USHGraph \land H \in USHGraph) \land (F : V \underset{1-1 onto}{⟶} W \land (e \in E ⟼ F [e]) : E \underset{1-1 onto}{⟶} D)) \land (x \in V \land y \in V)) \to (F Fn V \land (x \in V \land y \in V))$
112		3anass	$⊢ (F Fn V \land x \in V \land y \in V) \leftrightarrow (F Fn V \land (x \in V \land y \in V))$
113	111 112	sylibr	$⊢ (((G \in USHGraph \land H \in USHGraph) \land (F : V \underset{1-1 onto}{⟶} W \land (e \in E ⟼ F [e]) : E \underset{1-1 onto}{⟶} D)) \land (x \in V \land y \in V)) \to (F Fn V \land x \in V \land y \in V)$
114		fnimapr	$⊢ (F Fn V \land x \in V \land y \in V) \to F [\{x, y\}] = \{F (x), F (y)\}$
115	113 114	syl	$⊢ (((G \in USHGraph \land H \in USHGraph) \land (F : V \underset{1-1 onto}{⟶} W \land (e \in E ⟼ F [e]) : E \underset{1-1 onto}{⟶} D)) \land (x \in V \land y \in V)) \to F [\{x, y\}] = \{F (x), F (y)\}$
116	115	eleq1d	$⊢ (((G \in USHGraph \land H \in USHGraph) \land (F : V \underset{1-1 onto}{⟶} W \land (e \in E ⟼ F [e]) : E \underset{1-1 onto}{⟶} D)) \land (x \in V \land y \in V)) \to (F [\{x, y\}] \in D \leftrightarrow \{F (x), F (y)\} \in D)$
117	108 116	bitrd	$⊢ (((G \in USHGraph \land H \in USHGraph) \land (F : V \underset{1-1 onto}{⟶} W \land (e \in E ⟼ F [e]) : E \underset{1-1 onto}{⟶} D)) \land (x \in V \land y \in V)) \to (\{x, y\} \in E \leftrightarrow \{F (x), F (y)\} \in D)$
118	117	ralrimivva	$⊢ ((G \in USHGraph \land H \in USHGraph) \land (F : V \underset{1-1 onto}{⟶} W \land (e \in E ⟼ F [e]) : E \underset{1-1 onto}{⟶} D)) \to \forall x \in V \forall y \in V (\{x, y\} \in E \leftrightarrow \{F (x), F (y)\} \in D)$
119	7 118	jca	$⊢ ((G \in USHGraph \land H \in USHGraph) \land (F : V \underset{1-1 onto}{⟶} W \land (e \in E ⟼ F [e]) : E \underset{1-1 onto}{⟶} D)) \to (F : V \underset{1-1 onto}{⟶} W \land \forall x \in V \forall y \in V (\{x, y\} \in E \leftrightarrow \{F (x), F (y)\} \in D))$
120	119	ex	$⊢ (G \in USHGraph \land H \in USHGraph) \to ((F : V \underset{1-1 onto}{⟶} W \land (e \in E ⟼ F [e]) : E \underset{1-1 onto}{⟶} D) \to (F : V \underset{1-1 onto}{⟶} W \land \forall x \in V \forall y \in V (\{x, y\} \in E \leftrightarrow \{F (x), F (y)\} \in D)))$
121	120	adantr	$⊢ ((G \in USHGraph \land H \in USHGraph) \land F \in (G GraphIso H)) \to ((F : V \underset{1-1 onto}{⟶} W \land (e \in E ⟼ F [e]) : E \underset{1-1 onto}{⟶} D) \to (F : V \underset{1-1 onto}{⟶} W \land \forall x \in V \forall y \in V (\{x, y\} \in E \leftrightarrow \{F (x), F (y)\} \in D)))$
122	6 121	sylbid	$⊢ ((G \in USHGraph \land H \in USHGraph) \land F \in (G GraphIso H)) \to (F \in (G GraphIso H) \to (F : V \underset{1-1 onto}{⟶} W \land \forall x \in V \forall y \in V (\{x, y\} \in E \leftrightarrow \{F (x), F (y)\} \in D)))$
123	122	syldbl2	$⊢ ((G \in USHGraph \land H \in USHGraph) \land F \in (G GraphIso H)) \to (F : V \underset{1-1 onto}{⟶} W \land \forall x \in V \forall y \in V (\{x, y\} \in E \leftrightarrow \{F (x), F (y)\} \in D))$
124	123	ex	$⊢ (G \in USHGraph \land H \in USHGraph) \to (F \in (G GraphIso H) \to (F : V \underset{1-1 onto}{⟶} W \land \forall x \in V \forall y \in V (\{x, y\} \in E \leftrightarrow \{F (x), F (y)\} \in D)))$

Metamath Proof Explorer

Theorem uspgrimprop

Proof