isomuspgrlem1

	Ref	Expression
Hypotheses	isomushgr.v	$⊢ V = Vtx (A)$
	isomushgr.w	$⊢ W = Vtx (B)$
	isomushgr.e	$⊢ E = Edg (A)$
	isomushgr.k	$⊢ K = Edg (B)$
Assertion	isomuspgrlem1	$⊢ ((((A \in USHGraph \land B \in USHGraph) \land f : V \underset{1-1 onto}{⟶} W) \land (g : E \underset{1-1 onto}{⟶} K \land \forall e \in E f [e] = g (e))) \land (a \in V \land b \in V)) \to (\{f (a), f (b)\} \in K \to \{a, b\} \in E)$

Proof

Step	Hyp	Ref	Expression
1		isomushgr.v	$⊢ V = Vtx (A)$
2		isomushgr.w	$⊢ W = Vtx (B)$
3		isomushgr.e	$⊢ E = Edg (A)$
4		isomushgr.k	$⊢ K = Edg (B)$
5		simpl	$⊢ (g : E \underset{1-1 onto}{⟶} K \land \forall e \in E f [e] = g (e)) \to g : E \underset{1-1 onto}{⟶} K$
6	5	ad2antlr	$⊢ ((((A \in USHGraph \land B \in USHGraph) \land f : V \underset{1-1 onto}{⟶} W) \land (g : E \underset{1-1 onto}{⟶} K \land \forall e \in E f [e] = g (e))) \land (a \in V \land b \in V)) \to g : E \underset{1-1 onto}{⟶} K$
7		f1ocnvdm	$⊢ (g : E \underset{1-1 onto}{⟶} K \land \{f (a), f (b)\} \in K) \to g^{-1} (\{f (a), f (b)\}) \in E$
8	6 7	sylan	$⊢ (((((A \in USHGraph \land B \in USHGraph) \land f : V \underset{1-1 onto}{⟶} W) \land (g : E \underset{1-1 onto}{⟶} K \land \forall e \in E f [e] = g (e))) \land (a \in V \land b \in V)) \land \{f (a), f (b)\} \in K) \to g^{-1} (\{f (a), f (b)\}) \in E$
9		uspgrupgr	$⊢ A \in USHGraph \to A \in UPGraph$
10	9	adantr	$⊢ (A \in USHGraph \land B \in USHGraph) \to A \in UPGraph$
11	10	ad4antr	$⊢ (((((A \in USHGraph \land B \in USHGraph) \land f : V \underset{1-1 onto}{⟶} W) \land (g : E \underset{1-1 onto}{⟶} K \land \forall e \in E f [e] = g (e))) \land (a \in V \land b \in V)) \land \{f (a), f (b)\} \in K) \to A \in UPGraph$
12	1 3	upgredg	$⊢ (A \in UPGraph \land g^{-1} (\{f (a), f (b)\}) \in E) \to \exists x \in V \exists y \in V g^{-1} (\{f (a), f (b)\}) = \{x, y\}$
13	11 12	sylan	$⊢ ((((((A \in USHGraph \land B \in USHGraph) \land f : V \underset{1-1 onto}{⟶} W) \land (g : E \underset{1-1 onto}{⟶} K \land \forall e \in E f [e] = g (e))) \land (a \in V \land b \in V)) \land \{f (a), f (b)\} \in K) \land g^{-1} (\{f (a), f (b)\}) \in E) \to \exists x \in V \exists y \in V g^{-1} (\{f (a), f (b)\}) = \{x, y\}$
14		eleq1	$⊢ g^{-1} (\{f (a), f (b)\}) = \{x, y\} \to (g^{-1} (\{f (a), f (b)\}) \in E \leftrightarrow \{x, y\} \in E)$
15	14	biimpd	$⊢ g^{-1} (\{f (a), f (b)\}) = \{x, y\} \to (g^{-1} (\{f (a), f (b)\}) \in E \to \{x, y\} \in E)$
16	15	com12	$⊢ g^{-1} (\{f (a), f (b)\}) \in E \to (g^{-1} (\{f (a), f (b)\}) = \{x, y\} \to \{x, y\} \in E)$
17	16	ad2antlr	$⊢ (((((((A \in USHGraph \land B \in USHGraph) \land f : V \underset{1-1 onto}{⟶} W) \land (g : E \underset{1-1 onto}{⟶} K \land \forall e \in E f [e] = g (e))) \land (a \in V \land b \in V)) \land \{f (a), f (b)\} \in K) \land g^{-1} (\{f (a), f (b)\}) \in E) \land (x \in V \land y \in V)) \to (g^{-1} (\{f (a), f (b)\}) = \{x, y\} \to \{x, y\} \in E)$
18	17	imp	$⊢ ((((((((A \in USHGraph \land B \in USHGraph) \land f : V \underset{1-1 onto}{⟶} W) \land (g : E \underset{1-1 onto}{⟶} K \land \forall e \in E f [e] = g (e))) \land (a \in V \land b \in V)) \land \{f (a), f (b)\} \in K) \land g^{-1} (\{f (a), f (b)\}) \in E) \land (x \in V \land y \in V)) \land g^{-1} (\{f (a), f (b)\}) = \{x, y\}) \to \{x, y\} \in E$
19	5	ad6antlr	$⊢ ((((((((A \in USHGraph \land B \in USHGraph) \land f : V \underset{1-1 onto}{⟶} W) \land (g : E \underset{1-1 onto}{⟶} K \land \forall e \in E f [e] = g (e))) \land (a \in V \land b \in V)) \land \{f (a), f (b)\} \in K) \land g^{-1} (\{f (a), f (b)\}) \in E) \land (x \in V \land y \in V)) \land \{x, y\} \in E) \to g : E \underset{1-1 onto}{⟶} K$
20		simpr	$⊢ ((((((((A \in USHGraph \land B \in USHGraph) \land f : V \underset{1-1 onto}{⟶} W) \land (g : E \underset{1-1 onto}{⟶} K \land \forall e \in E f [e] = g (e))) \land (a \in V \land b \in V)) \land \{f (a), f (b)\} \in K) \land g^{-1} (\{f (a), f (b)\}) \in E) \land (x \in V \land y \in V)) \land \{x, y\} \in E) \to \{x, y\} \in E$
21		simpr	$⊢ (((((A \in USHGraph \land B \in USHGraph) \land f : V \underset{1-1 onto}{⟶} W) \land (g : E \underset{1-1 onto}{⟶} K \land \forall e \in E f [e] = g (e))) \land (a \in V \land b \in V)) \land \{f (a), f (b)\} \in K) \to \{f (a), f (b)\} \in K$
22	21	ad5ant12	$⊢ ((((((((A \in USHGraph \land B \in USHGraph) \land f : V \underset{1-1 onto}{⟶} W) \land (g : E \underset{1-1 onto}{⟶} K \land \forall e \in E f [e] = g (e))) \land (a \in V \land b \in V)) \land \{f (a), f (b)\} \in K) \land g^{-1} (\{f (a), f (b)\}) \in E) \land (x \in V \land y \in V)) \land \{x, y\} \in E) \to \{f (a), f (b)\} \in K$
23	19 20 22	3jca	$⊢ ((((((((A \in USHGraph \land B \in USHGraph) \land f : V \underset{1-1 onto}{⟶} W) \land (g : E \underset{1-1 onto}{⟶} K \land \forall e \in E f [e] = g (e))) \land (a \in V \land b \in V)) \land \{f (a), f (b)\} \in K) \land g^{-1} (\{f (a), f (b)\}) \in E) \land (x \in V \land y \in V)) \land \{x, y\} \in E) \to (g : E \underset{1-1 onto}{⟶} K \land \{x, y\} \in E \land \{f (a), f (b)\} \in K)$
24		f1ocnvfvb	$⊢ (g : E \underset{1-1 onto}{⟶} K \land \{x, y\} \in E \land \{f (a), f (b)\} \in K) \to (g (\{x, y\}) = \{f (a), f (b)\} \leftrightarrow g^{-1} (\{f (a), f (b)\}) = \{x, y\})$
25	23 24	syl	$⊢ ((((((((A \in USHGraph \land B \in USHGraph) \land f : V \underset{1-1 onto}{⟶} W) \land (g : E \underset{1-1 onto}{⟶} K \land \forall e \in E f [e] = g (e))) \land (a \in V \land b \in V)) \land \{f (a), f (b)\} \in K) \land g^{-1} (\{f (a), f (b)\}) \in E) \land (x \in V \land y \in V)) \land \{x, y\} \in E) \to (g (\{x, y\}) = \{f (a), f (b)\} \leftrightarrow g^{-1} (\{f (a), f (b)\}) = \{x, y\})$
26		imaeq2	$⊢ e = \{x, y\} \to f [e] = f [\{x, y\}]$
27		fveq2	$⊢ e = \{x, y\} \to g (e) = g (\{x, y\})$
28	26 27	eqeq12d	$⊢ e = \{x, y\} \to (f [e] = g (e) \leftrightarrow f [\{x, y\}] = g (\{x, y\}))$
29	28	rspccv	$⊢ \forall e \in E f [e] = g (e) \to (\{x, y\} \in E \to f [\{x, y\}] = g (\{x, y\}))$
30	29	adantl	$⊢ (g : E \underset{1-1 onto}{⟶} K \land \forall e \in E f [e] = g (e)) \to (\{x, y\} \in E \to f [\{x, y\}] = g (\{x, y\}))$
31	30	adantl	$⊢ (((A \in USHGraph \land B \in USHGraph) \land f : V \underset{1-1 onto}{⟶} W) \land (g : E \underset{1-1 onto}{⟶} K \land \forall e \in E f [e] = g (e))) \to (\{x, y\} \in E \to f [\{x, y\}] = g (\{x, y\}))$
32	31	ad4antr	$⊢ (((((((A \in USHGraph \land B \in USHGraph) \land f : V \underset{1-1 onto}{⟶} W) \land (g : E \underset{1-1 onto}{⟶} K \land \forall e \in E f [e] = g (e))) \land (a \in V \land b \in V)) \land \{f (a), f (b)\} \in K) \land g^{-1} (\{f (a), f (b)\}) \in E) \land (x \in V \land y \in V)) \to (\{x, y\} \in E \to f [\{x, y\}] = g (\{x, y\}))$
33	32	imp	$⊢ ((((((((A \in USHGraph \land B \in USHGraph) \land f : V \underset{1-1 onto}{⟶} W) \land (g : E \underset{1-1 onto}{⟶} K \land \forall e \in E f [e] = g (e))) \land (a \in V \land b \in V)) \land \{f (a), f (b)\} \in K) \land g^{-1} (\{f (a), f (b)\}) \in E) \land (x \in V \land y \in V)) \land \{x, y\} \in E) \to f [\{x, y\}] = g (\{x, y\})$
34		eqeq1	$⊢ g (\{x, y\}) = f [\{x, y\}] \to (g (\{x, y\}) = \{f (a), f (b)\} \leftrightarrow f [\{x, y\}] = \{f (a), f (b)\})$
35	34	eqcoms	$⊢ f [\{x, y\}] = g (\{x, y\}) \to (g (\{x, y\}) = \{f (a), f (b)\} \leftrightarrow f [\{x, y\}] = \{f (a), f (b)\})$
36	35	adantl	$⊢ (((((((((A \in USHGraph \land B \in USHGraph) \land f : V \underset{1-1 onto}{⟶} W) \land (g : E \underset{1-1 onto}{⟶} K \land \forall e \in E f [e] = g (e))) \land (a \in V \land b \in V)) \land \{f (a), f (b)\} \in K) \land g^{-1} (\{f (a), f (b)\}) \in E) \land (x \in V \land y \in V)) \land \{x, y\} \in E) \land f [\{x, y\}] = g (\{x, y\})) \to (g (\{x, y\}) = \{f (a), f (b)\} \leftrightarrow f [\{x, y\}] = \{f (a), f (b)\})$
37		f1ofn	$⊢ f : V \underset{1-1 onto}{⟶} W \to f Fn V$
38	37	ad6antlr	$⊢ (((((((A \in USHGraph \land B \in USHGraph) \land f : V \underset{1-1 onto}{⟶} W) \land (g : E \underset{1-1 onto}{⟶} K \land \forall e \in E f [e] = g (e))) \land (a \in V \land b \in V)) \land \{f (a), f (b)\} \in K) \land g^{-1} (\{f (a), f (b)\}) \in E) \land (x \in V \land y \in V)) \to f Fn V$
39		simpl	$⊢ (x \in V \land y \in V) \to x \in V$
40	39	adantl	$⊢ (((((((A \in USHGraph \land B \in USHGraph) \land f : V \underset{1-1 onto}{⟶} W) \land (g : E \underset{1-1 onto}{⟶} K \land \forall e \in E f [e] = g (e))) \land (a \in V \land b \in V)) \land \{f (a), f (b)\} \in K) \land g^{-1} (\{f (a), f (b)\}) \in E) \land (x \in V \land y \in V)) \to x \in V$
41		simpr	$⊢ (x \in V \land y \in V) \to y \in V$
42	41	adantl	$⊢ (((((((A \in USHGraph \land B \in USHGraph) \land f : V \underset{1-1 onto}{⟶} W) \land (g : E \underset{1-1 onto}{⟶} K \land \forall e \in E f [e] = g (e))) \land (a \in V \land b \in V)) \land \{f (a), f (b)\} \in K) \land g^{-1} (\{f (a), f (b)\}) \in E) \land (x \in V \land y \in V)) \to y \in V$
43	38 40 42	3jca	$⊢ (((((((A \in USHGraph \land B \in USHGraph) \land f : V \underset{1-1 onto}{⟶} W) \land (g : E \underset{1-1 onto}{⟶} K \land \forall e \in E f [e] = g (e))) \land (a \in V \land b \in V)) \land \{f (a), f (b)\} \in K) \land g^{-1} (\{f (a), f (b)\}) \in E) \land (x \in V \land y \in V)) \to (f Fn V \land x \in V \land y \in V)$
44	43	adantr	$⊢ ((((((((A \in USHGraph \land B \in USHGraph) \land f : V \underset{1-1 onto}{⟶} W) \land (g : E \underset{1-1 onto}{⟶} K \land \forall e \in E f [e] = g (e))) \land (a \in V \land b \in V)) \land \{f (a), f (b)\} \in K) \land g^{-1} (\{f (a), f (b)\}) \in E) \land (x \in V \land y \in V)) \land \{x, y\} \in E) \to (f Fn V \land x \in V \land y \in V)$
45		fnimapr	$⊢ (f Fn V \land x \in V \land y \in V) \to f [\{x, y\}] = \{f (x), f (y)\}$
46	44 45	syl	$⊢ ((((((((A \in USHGraph \land B \in USHGraph) \land f : V \underset{1-1 onto}{⟶} W) \land (g : E \underset{1-1 onto}{⟶} K \land \forall e \in E f [e] = g (e))) \land (a \in V \land b \in V)) \land \{f (a), f (b)\} \in K) \land g^{-1} (\{f (a), f (b)\}) \in E) \land (x \in V \land y \in V)) \land \{x, y\} \in E) \to f [\{x, y\}] = \{f (x), f (y)\}$
47	46	eqeq1d	$⊢ ((((((((A \in USHGraph \land B \in USHGraph) \land f : V \underset{1-1 onto}{⟶} W) \land (g : E \underset{1-1 onto}{⟶} K \land \forall e \in E f [e] = g (e))) \land (a \in V \land b \in V)) \land \{f (a), f (b)\} \in K) \land g^{-1} (\{f (a), f (b)\}) \in E) \land (x \in V \land y \in V)) \land \{x, y\} \in E) \to (f [\{x, y\}] = \{f (a), f (b)\} \leftrightarrow \{f (x), f (y)\} = \{f (a), f (b)\})$
48		fvex	$⊢ f (x) \in V$
49		fvex	$⊢ f (y) \in V$
50		fvex	$⊢ f (a) \in V$
51		fvex	$⊢ f (b) \in V$
52	48 49 50 51	preq12b	$⊢ \{f (x), f (y)\} = \{f (a), f (b)\} \leftrightarrow ((f (x) = f (a) \land f (y) = f (b)) \lor (f (x) = f (b) \land f (y) = f (a)))$
53		f1of1	$⊢ f : V \underset{1-1 onto}{⟶} W \to f : V \underset{1-1}{⟶} W$
54		simpl	$⊢ (a \in V \land b \in V) \to a \in V$
55	54 39	anim12ci	$⊢ ((a \in V \land b \in V) \land (x \in V \land y \in V)) \to (x \in V \land a \in V)$
56		f1veqaeq	$⊢ (f : V \underset{1-1}{⟶} W \land (x \in V \land a \in V)) \to (f (x) = f (a) \to x = a)$
57	53 55 56	syl2anr	$⊢ (((a \in V \land b \in V) \land (x \in V \land y \in V)) \land f : V \underset{1-1 onto}{⟶} W) \to (f (x) = f (a) \to x = a)$
58		simpr	$⊢ (a \in V \land b \in V) \to b \in V$
59	58 41	anim12ci	$⊢ ((a \in V \land b \in V) \land (x \in V \land y \in V)) \to (y \in V \land b \in V)$
60		f1veqaeq	$⊢ (f : V \underset{1-1}{⟶} W \land (y \in V \land b \in V)) \to (f (y) = f (b) \to y = b)$
61	53 59 60	syl2anr	$⊢ (((a \in V \land b \in V) \land (x \in V \land y \in V)) \land f : V \underset{1-1 onto}{⟶} W) \to (f (y) = f (b) \to y = b)$
62	57 61	anim12d	$⊢ (((a \in V \land b \in V) \land (x \in V \land y \in V)) \land f : V \underset{1-1 onto}{⟶} W) \to ((f (x) = f (a) \land f (y) = f (b)) \to (x = a \land y = b))$
63	62	impcom	$⊢ ((f (x) = f (a) \land f (y) = f (b)) \land (((a \in V \land b \in V) \land (x \in V \land y \in V)) \land f : V \underset{1-1 onto}{⟶} W)) \to (x = a \land y = b)$
64	63	orcd	$⊢ ((f (x) = f (a) \land f (y) = f (b)) \land (((a \in V \land b \in V) \land (x \in V \land y \in V)) \land f : V \underset{1-1 onto}{⟶} W)) \to ((x = a \land y = b) \lor (x = b \land y = a))$
65	64	ex	$⊢ (f (x) = f (a) \land f (y) = f (b)) \to ((((a \in V \land b \in V) \land (x \in V \land y \in V)) \land f : V \underset{1-1 onto}{⟶} W) \to ((x = a \land y = b) \lor (x = b \land y = a)))$
66	58 39	anim12ci	$⊢ ((a \in V \land b \in V) \land (x \in V \land y \in V)) \to (x \in V \land b \in V)$
67		f1veqaeq	$⊢ (f : V \underset{1-1}{⟶} W \land (x \in V \land b \in V)) \to (f (x) = f (b) \to x = b)$
68	53 66 67	syl2anr	$⊢ (((a \in V \land b \in V) \land (x \in V \land y \in V)) \land f : V \underset{1-1 onto}{⟶} W) \to (f (x) = f (b) \to x = b)$
69	54 41	anim12ci	$⊢ ((a \in V \land b \in V) \land (x \in V \land y \in V)) \to (y \in V \land a \in V)$
70		f1veqaeq	$⊢ (f : V \underset{1-1}{⟶} W \land (y \in V \land a \in V)) \to (f (y) = f (a) \to y = a)$
71	53 69 70	syl2anr	$⊢ (((a \in V \land b \in V) \land (x \in V \land y \in V)) \land f : V \underset{1-1 onto}{⟶} W) \to (f (y) = f (a) \to y = a)$
72	68 71	anim12d	$⊢ (((a \in V \land b \in V) \land (x \in V \land y \in V)) \land f : V \underset{1-1 onto}{⟶} W) \to ((f (x) = f (b) \land f (y) = f (a)) \to (x = b \land y = a))$
73	72	impcom	$⊢ ((f (x) = f (b) \land f (y) = f (a)) \land (((a \in V \land b \in V) \land (x \in V \land y \in V)) \land f : V \underset{1-1 onto}{⟶} W)) \to (x = b \land y = a)$
74	73	olcd	$⊢ ((f (x) = f (b) \land f (y) = f (a)) \land (((a \in V \land b \in V) \land (x \in V \land y \in V)) \land f : V \underset{1-1 onto}{⟶} W)) \to ((x = a \land y = b) \lor (x = b \land y = a))$
75	74	ex	$⊢ (f (x) = f (b) \land f (y) = f (a)) \to ((((a \in V \land b \in V) \land (x \in V \land y \in V)) \land f : V \underset{1-1 onto}{⟶} W) \to ((x = a \land y = b) \lor (x = b \land y = a)))$
76	65 75	jaoi	$⊢ ((f (x) = f (a) \land f (y) = f (b)) \lor (f (x) = f (b) \land f (y) = f (a))) \to ((((a \in V \land b \in V) \land (x \in V \land y \in V)) \land f : V \underset{1-1 onto}{⟶} W) \to ((x = a \land y = b) \lor (x = b \land y = a)))$
77		vex	$⊢ x \in V$
78		vex	$⊢ y \in V$
79		vex	$⊢ a \in V$
80		vex	$⊢ b \in V$
81	77 78 79 80	preq12b	$⊢ \{x, y\} = \{a, b\} \leftrightarrow ((x = a \land y = b) \lor (x = b \land y = a))$
82	76 81	syl6ibr	$⊢ ((f (x) = f (a) \land f (y) = f (b)) \lor (f (x) = f (b) \land f (y) = f (a))) \to ((((a \in V \land b \in V) \land (x \in V \land y \in V)) \land f : V \underset{1-1 onto}{⟶} W) \to \{x, y\} = \{a, b\})$
83	52 82	sylbi	$⊢ \{f (x), f (y)\} = \{f (a), f (b)\} \to ((((a \in V \land b \in V) \land (x \in V \land y \in V)) \land f : V \underset{1-1 onto}{⟶} W) \to \{x, y\} = \{a, b\})$
84	83	com12	$⊢ (((a \in V \land b \in V) \land (x \in V \land y \in V)) \land f : V \underset{1-1 onto}{⟶} W) \to (\{f (x), f (y)\} = \{f (a), f (b)\} \to \{x, y\} = \{a, b\})$
85	84	expcom	$⊢ f : V \underset{1-1 onto}{⟶} W \to (((a \in V \land b \in V) \land (x \in V \land y \in V)) \to (\{f (x), f (y)\} = \{f (a), f (b)\} \to \{x, y\} = \{a, b\}))$
86	85	expd	$⊢ f : V \underset{1-1 onto}{⟶} W \to ((a \in V \land b \in V) \to ((x \in V \land y \in V) \to (\{f (x), f (y)\} = \{f (a), f (b)\} \to \{x, y\} = \{a, b\})))$
87	86	ad2antlr	$⊢ (((A \in USHGraph \land B \in USHGraph) \land f : V \underset{1-1 onto}{⟶} W) \land (g : E \underset{1-1 onto}{⟶} K \land \forall e \in E f [e] = g (e))) \to ((a \in V \land b \in V) \to ((x \in V \land y \in V) \to (\{f (x), f (y)\} = \{f (a), f (b)\} \to \{x, y\} = \{a, b\})))$
88	87	imp	$⊢ ((((A \in USHGraph \land B \in USHGraph) \land f : V \underset{1-1 onto}{⟶} W) \land (g : E \underset{1-1 onto}{⟶} K \land \forall e \in E f [e] = g (e))) \land (a \in V \land b \in V)) \to ((x \in V \land y \in V) \to (\{f (x), f (y)\} = \{f (a), f (b)\} \to \{x, y\} = \{a, b\}))$
89	88	adantr	$⊢ (((((A \in USHGraph \land B \in USHGraph) \land f : V \underset{1-1 onto}{⟶} W) \land (g : E \underset{1-1 onto}{⟶} K \land \forall e \in E f [e] = g (e))) \land (a \in V \land b \in V)) \land \{f (a), f (b)\} \in K) \to ((x \in V \land y \in V) \to (\{f (x), f (y)\} = \{f (a), f (b)\} \to \{x, y\} = \{a, b\}))$
90	89	adantr	$⊢ ((((((A \in USHGraph \land B \in USHGraph) \land f : V \underset{1-1 onto}{⟶} W) \land (g : E \underset{1-1 onto}{⟶} K \land \forall e \in E f [e] = g (e))) \land (a \in V \land b \in V)) \land \{f (a), f (b)\} \in K) \land g^{-1} (\{f (a), f (b)\}) \in E) \to ((x \in V \land y \in V) \to (\{f (x), f (y)\} = \{f (a), f (b)\} \to \{x, y\} = \{a, b\}))$
91	90	imp31	$⊢ ((((((((A \in USHGraph \land B \in USHGraph) \land f : V \underset{1-1 onto}{⟶} W) \land (g : E \underset{1-1 onto}{⟶} K \land \forall e \in E f [e] = g (e))) \land (a \in V \land b \in V)) \land \{f (a), f (b)\} \in K) \land g^{-1} (\{f (a), f (b)\}) \in E) \land (x \in V \land y \in V)) \land \{f (x), f (y)\} = \{f (a), f (b)\}) \to \{x, y\} = \{a, b\}$
92	91	eleq1d	$⊢ ((((((((A \in USHGraph \land B \in USHGraph) \land f : V \underset{1-1 onto}{⟶} W) \land (g : E \underset{1-1 onto}{⟶} K \land \forall e \in E f [e] = g (e))) \land (a \in V \land b \in V)) \land \{f (a), f (b)\} \in K) \land g^{-1} (\{f (a), f (b)\}) \in E) \land (x \in V \land y \in V)) \land \{f (x), f (y)\} = \{f (a), f (b)\}) \to (\{x, y\} \in E \leftrightarrow \{a, b\} \in E)$
93	92	biimpd	$⊢ ((((((((A \in USHGraph \land B \in USHGraph) \land f : V \underset{1-1 onto}{⟶} W) \land (g : E \underset{1-1 onto}{⟶} K \land \forall e \in E f [e] = g (e))) \land (a \in V \land b \in V)) \land \{f (a), f (b)\} \in K) \land g^{-1} (\{f (a), f (b)\}) \in E) \land (x \in V \land y \in V)) \land \{f (x), f (y)\} = \{f (a), f (b)\}) \to (\{x, y\} \in E \to \{a, b\} \in E)$
94	93	impancom	$⊢ ((((((((A \in USHGraph \land B \in USHGraph) \land f : V \underset{1-1 onto}{⟶} W) \land (g : E \underset{1-1 onto}{⟶} K \land \forall e \in E f [e] = g (e))) \land (a \in V \land b \in V)) \land \{f (a), f (b)\} \in K) \land g^{-1} (\{f (a), f (b)\}) \in E) \land (x \in V \land y \in V)) \land \{x, y\} \in E) \to (\{f (x), f (y)\} = \{f (a), f (b)\} \to \{a, b\} \in E)$
95	47 94	sylbid	$⊢ ((((((((A \in USHGraph \land B \in USHGraph) \land f : V \underset{1-1 onto}{⟶} W) \land (g : E \underset{1-1 onto}{⟶} K \land \forall e \in E f [e] = g (e))) \land (a \in V \land b \in V)) \land \{f (a), f (b)\} \in K) \land g^{-1} (\{f (a), f (b)\}) \in E) \land (x \in V \land y \in V)) \land \{x, y\} \in E) \to (f [\{x, y\}] = \{f (a), f (b)\} \to \{a, b\} \in E)$
96	95	adantr	$⊢ (((((((((A \in USHGraph \land B \in USHGraph) \land f : V \underset{1-1 onto}{⟶} W) \land (g : E \underset{1-1 onto}{⟶} K \land \forall e \in E f [e] = g (e))) \land (a \in V \land b \in V)) \land \{f (a), f (b)\} \in K) \land g^{-1} (\{f (a), f (b)\}) \in E) \land (x \in V \land y \in V)) \land \{x, y\} \in E) \land f [\{x, y\}] = g (\{x, y\})) \to (f [\{x, y\}] = \{f (a), f (b)\} \to \{a, b\} \in E)$
97	36 96	sylbid	$⊢ (((((((((A \in USHGraph \land B \in USHGraph) \land f : V \underset{1-1 onto}{⟶} W) \land (g : E \underset{1-1 onto}{⟶} K \land \forall e \in E f [e] = g (e))) \land (a \in V \land b \in V)) \land \{f (a), f (b)\} \in K) \land g^{-1} (\{f (a), f (b)\}) \in E) \land (x \in V \land y \in V)) \land \{x, y\} \in E) \land f [\{x, y\}] = g (\{x, y\})) \to (g (\{x, y\}) = \{f (a), f (b)\} \to \{a, b\} \in E)$
98	33 97	mpdan	$⊢ ((((((((A \in USHGraph \land B \in USHGraph) \land f : V \underset{1-1 onto}{⟶} W) \land (g : E \underset{1-1 onto}{⟶} K \land \forall e \in E f [e] = g (e))) \land (a \in V \land b \in V)) \land \{f (a), f (b)\} \in K) \land g^{-1} (\{f (a), f (b)\}) \in E) \land (x \in V \land y \in V)) \land \{x, y\} \in E) \to (g (\{x, y\}) = \{f (a), f (b)\} \to \{a, b\} \in E)$
99	25 98	sylbird	$⊢ ((((((((A \in USHGraph \land B \in USHGraph) \land f : V \underset{1-1 onto}{⟶} W) \land (g : E \underset{1-1 onto}{⟶} K \land \forall e \in E f [e] = g (e))) \land (a \in V \land b \in V)) \land \{f (a), f (b)\} \in K) \land g^{-1} (\{f (a), f (b)\}) \in E) \land (x \in V \land y \in V)) \land \{x, y\} \in E) \to (g^{-1} (\{f (a), f (b)\}) = \{x, y\} \to \{a, b\} \in E)$
100	99	impancom	$⊢ ((((((((A \in USHGraph \land B \in USHGraph) \land f : V \underset{1-1 onto}{⟶} W) \land (g : E \underset{1-1 onto}{⟶} K \land \forall e \in E f [e] = g (e))) \land (a \in V \land b \in V)) \land \{f (a), f (b)\} \in K) \land g^{-1} (\{f (a), f (b)\}) \in E) \land (x \in V \land y \in V)) \land g^{-1} (\{f (a), f (b)\}) = \{x, y\}) \to (\{x, y\} \in E \to \{a, b\} \in E)$
101	18 100	mpd	$⊢ ((((((((A \in USHGraph \land B \in USHGraph) \land f : V \underset{1-1 onto}{⟶} W) \land (g : E \underset{1-1 onto}{⟶} K \land \forall e \in E f [e] = g (e))) \land (a \in V \land b \in V)) \land \{f (a), f (b)\} \in K) \land g^{-1} (\{f (a), f (b)\}) \in E) \land (x \in V \land y \in V)) \land g^{-1} (\{f (a), f (b)\}) = \{x, y\}) \to \{a, b\} \in E$
102	101	ex	$⊢ (((((((A \in USHGraph \land B \in USHGraph) \land f : V \underset{1-1 onto}{⟶} W) \land (g : E \underset{1-1 onto}{⟶} K \land \forall e \in E f [e] = g (e))) \land (a \in V \land b \in V)) \land \{f (a), f (b)\} \in K) \land g^{-1} (\{f (a), f (b)\}) \in E) \land (x \in V \land y \in V)) \to (g^{-1} (\{f (a), f (b)\}) = \{x, y\} \to \{a, b\} \in E)$
103	102	rexlimdvva	$⊢ ((((((A \in USHGraph \land B \in USHGraph) \land f : V \underset{1-1 onto}{⟶} W) \land (g : E \underset{1-1 onto}{⟶} K \land \forall e \in E f [e] = g (e))) \land (a \in V \land b \in V)) \land \{f (a), f (b)\} \in K) \land g^{-1} (\{f (a), f (b)\}) \in E) \to (\exists x \in V \exists y \in V g^{-1} (\{f (a), f (b)\}) = \{x, y\} \to \{a, b\} \in E)$
104	13 103	mpd	$⊢ ((((((A \in USHGraph \land B \in USHGraph) \land f : V \underset{1-1 onto}{⟶} W) \land (g : E \underset{1-1 onto}{⟶} K \land \forall e \in E f [e] = g (e))) \land (a \in V \land b \in V)) \land \{f (a), f (b)\} \in K) \land g^{-1} (\{f (a), f (b)\}) \in E) \to \{a, b\} \in E$
105	8 104	mpdan	$⊢ (((((A \in USHGraph \land B \in USHGraph) \land f : V \underset{1-1 onto}{⟶} W) \land (g : E \underset{1-1 onto}{⟶} K \land \forall e \in E f [e] = g (e))) \land (a \in V \land b \in V)) \land \{f (a), f (b)\} \in K) \to \{a, b\} \in E$
106	105	ex	$⊢ ((((A \in USHGraph \land B \in USHGraph) \land f : V \underset{1-1 onto}{⟶} W) \land (g : E \underset{1-1 onto}{⟶} K \land \forall e \in E f [e] = g (e))) \land (a \in V \land b \in V)) \to (\{f (a), f (b)\} \in K \to \{a, b\} \in E)$

Metamath Proof Explorer

Theorem isomuspgrlem1

Proof