grimcnv

Description: The converse of a graph isomorphism is a graph isomorphism. (Contributed by AV, 1-May-2025)

		Ref	Expression
	Assertion	grimcnv	$⊢ S \in UHGraph \to (F \in (S GraphIso T) \to F^{-1} \in (T GraphIso S))$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ Vtx (S) = Vtx (S)$
2		eqid	$⊢ Vtx (T) = Vtx (T)$
3		eqid	$⊢ iEdg (S) = iEdg (S)$
4		eqid	$⊢ iEdg (T) = iEdg (T)$
5	1 2 3 4	grimprop	$⊢ F \in (S GraphIso T) \to (F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T) \land \exists j (j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T) \land \forall i \in dom iEdg (S) iEdg (T) (j (i)) = F [iEdg (S) (i)]))$
6	5	adantl	$⊢ (S \in UHGraph \land F \in (S GraphIso T)) \to (F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T) \land \exists j (j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T) \land \forall i \in dom iEdg (S) iEdg (T) (j (i)) = F [iEdg (S) (i)]))$
7		f1ocnv	$⊢ F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T) \to F^{-1} : Vtx (T) \underset{1-1 onto}{⟶} Vtx (S)$
8	7	ad2antrl	$⊢ ((S \in UHGraph \land F \in (S GraphIso T)) \land (F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T) \land \exists j (j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T) \land \forall i \in dom iEdg (S) iEdg (T) (j (i)) = F [iEdg (S) (i)]))) \to F^{-1} : Vtx (T) \underset{1-1 onto}{⟶} Vtx (S)$
9		vex	$⊢ j \in V$
10		cnvexg	$⊢ j \in V \to j^{-1} \in V$
11	9 10	mp1i	$⊢ (((S \in UHGraph \land F \in (S GraphIso T)) \land F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T)) \land (j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T) \land \forall i \in dom iEdg (S) iEdg (T) (j (i)) = F [iEdg (S) (i)])) \to j^{-1} \in V$
12		f1ocnv	$⊢ j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T) \to j^{-1} : dom iEdg (T) \underset{1-1 onto}{⟶} dom iEdg (S)$
13	12	ad2antrl	$⊢ (((S \in UHGraph \land F \in (S GraphIso T)) \land F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T)) \land (j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T) \land \forall i \in dom iEdg (S) iEdg (T) (j (i)) = F [iEdg (S) (i)])) \to j^{-1} : dom iEdg (T) \underset{1-1 onto}{⟶} dom iEdg (S)$
14		f1ofo	$⊢ j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T) \to j : dom iEdg (S) \underset{onto}{⟶} dom iEdg (T)$
15	14	ad2antrl	$⊢ (((S \in UHGraph \land F \in (S GraphIso T)) \land F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T)) \land (j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T) \land \forall i \in dom iEdg (S) iEdg (T) (j (i)) = F [iEdg (S) (i)])) \to j : dom iEdg (S) \underset{onto}{⟶} dom iEdg (T)$
16		foelcdmi	$⊢ (j : dom iEdg (S) \underset{onto}{⟶} dom iEdg (T) \land x \in dom iEdg (T)) \to \exists y \in dom iEdg (S) j (y) = x$
17	15 16	sylan	$⊢ ((((S \in UHGraph \land F \in (S GraphIso T)) \land F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T)) \land (j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T) \land \forall i \in dom iEdg (S) iEdg (T) (j (i)) = F [iEdg (S) (i)])) \land x \in dom iEdg (T)) \to \exists y \in dom iEdg (S) j (y) = x$
18		2fveq3	$⊢ i = y \to iEdg (T) (j (i)) = iEdg (T) (j (y))$
19		fveq2	$⊢ i = y \to iEdg (S) (i) = iEdg (S) (y)$
20	19	imaeq2d	$⊢ i = y \to F [iEdg (S) (i)] = F [iEdg (S) (y)]$
21	18 20	eqeq12d	$⊢ i = y \to (iEdg (T) (j (i)) = F [iEdg (S) (i)] \leftrightarrow iEdg (T) (j (y)) = F [iEdg (S) (y)])$
22	21	rspcv	$⊢ y \in dom iEdg (S) \to (\forall i \in dom iEdg (S) iEdg (T) (j (i)) = F [iEdg (S) (i)] \to iEdg (T) (j (y)) = F [iEdg (S) (y)])$
23	22	adantl	$⊢ ((((S \in UHGraph \land F \in (S GraphIso T)) \land F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T)) \land j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T)) \land y \in dom iEdg (S)) \to (\forall i \in dom iEdg (S) iEdg (T) (j (i)) = F [iEdg (S) (i)] \to iEdg (T) (j (y)) = F [iEdg (S) (y)])$
24		f1ocnvfv1	$⊢ (j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T) \land y \in dom iEdg (S)) \to j^{-1} (j (y)) = y$
25	24	ad4ant23	$⊢ (((((S \in UHGraph \land F \in (S GraphIso T)) \land F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T)) \land j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T)) \land y \in dom iEdg (S)) \land j (y) \in dom iEdg (T)) \to j^{-1} (j (y)) = y$
26	25	fveq2d	$⊢ (((((S \in UHGraph \land F \in (S GraphIso T)) \land F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T)) \land j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T)) \land y \in dom iEdg (S)) \land j (y) \in dom iEdg (T)) \to iEdg (S) (j^{-1} (j (y))) = iEdg (S) (y)$
27		f1of1	$⊢ F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T) \to F : Vtx (S) \underset{1-1}{⟶} Vtx (T)$
28	27	ad2antlr	$⊢ (((S \in UHGraph \land F \in (S GraphIso T)) \land F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T)) \land j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T)) \to F : Vtx (S) \underset{1-1}{⟶} Vtx (T)$
29	1 3	uhgrss	$⊢ (S \in UHGraph \land y \in dom iEdg (S)) \to iEdg (S) (y) \subseteq Vtx (S)$
30	29	ad5ant15	$⊢ ((((S \in UHGraph \land F \in (S GraphIso T)) \land F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T)) \land j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T)) \land y \in dom iEdg (S)) \to iEdg (S) (y) \subseteq Vtx (S)$
31		f1imacnv	$⊢ (F : Vtx (S) \underset{1-1}{⟶} Vtx (T) \land iEdg (S) (y) \subseteq Vtx (S)) \to F^{-1} [F [iEdg (S) (y)]] = iEdg (S) (y)$
32	28 30 31	syl2an2r	$⊢ ((((S \in UHGraph \land F \in (S GraphIso T)) \land F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T)) \land j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T)) \land y \in dom iEdg (S)) \to F^{-1} [F [iEdg (S) (y)]] = iEdg (S) (y)$
33	32	eqcomd	$⊢ ((((S \in UHGraph \land F \in (S GraphIso T)) \land F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T)) \land j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T)) \land y \in dom iEdg (S)) \to iEdg (S) (y) = F^{-1} [F [iEdg (S) (y)]]$
34	33	adantr	$⊢ (((((S \in UHGraph \land F \in (S GraphIso T)) \land F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T)) \land j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T)) \land y \in dom iEdg (S)) \land j (y) \in dom iEdg (T)) \to iEdg (S) (y) = F^{-1} [F [iEdg (S) (y)]]$
35	26 34	eqtrd	$⊢ (((((S \in UHGraph \land F \in (S GraphIso T)) \land F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T)) \land j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T)) \land y \in dom iEdg (S)) \land j (y) \in dom iEdg (T)) \to iEdg (S) (j^{-1} (j (y))) = F^{-1} [F [iEdg (S) (y)]]$
36	35	adantlr	$⊢ ((((((S \in UHGraph \land F \in (S GraphIso T)) \land F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T)) \land j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T)) \land y \in dom iEdg (S)) \land iEdg (T) (j (y)) = F [iEdg (S) (y)]) \land j (y) \in dom iEdg (T)) \to iEdg (S) (j^{-1} (j (y))) = F^{-1} [F [iEdg (S) (y)]]$
37		simplr	$⊢ ((((((S \in UHGraph \land F \in (S GraphIso T)) \land F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T)) \land j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T)) \land y \in dom iEdg (S)) \land iEdg (T) (j (y)) = F [iEdg (S) (y)]) \land j (y) \in dom iEdg (T)) \to iEdg (T) (j (y)) = F [iEdg (S) (y)]$
38	37	eqcomd	$⊢ ((((((S \in UHGraph \land F \in (S GraphIso T)) \land F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T)) \land j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T)) \land y \in dom iEdg (S)) \land iEdg (T) (j (y)) = F [iEdg (S) (y)]) \land j (y) \in dom iEdg (T)) \to F [iEdg (S) (y)] = iEdg (T) (j (y))$
39	38	imaeq2d	$⊢ ((((((S \in UHGraph \land F \in (S GraphIso T)) \land F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T)) \land j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T)) \land y \in dom iEdg (S)) \land iEdg (T) (j (y)) = F [iEdg (S) (y)]) \land j (y) \in dom iEdg (T)) \to F^{-1} [F [iEdg (S) (y)]] = F^{-1} [iEdg (T) (j (y))]$
40	36 39	eqtrd	$⊢ ((((((S \in UHGraph \land F \in (S GraphIso T)) \land F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T)) \land j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T)) \land y \in dom iEdg (S)) \land iEdg (T) (j (y)) = F [iEdg (S) (y)]) \land j (y) \in dom iEdg (T)) \to iEdg (S) (j^{-1} (j (y))) = F^{-1} [iEdg (T) (j (y))]$
41	40	ex	$⊢ (((((S \in UHGraph \land F \in (S GraphIso T)) \land F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T)) \land j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T)) \land y \in dom iEdg (S)) \land iEdg (T) (j (y)) = F [iEdg (S) (y)]) \to (j (y) \in dom iEdg (T) \to iEdg (S) (j^{-1} (j (y))) = F^{-1} [iEdg (T) (j (y))])$
42	41	ex	$⊢ ((((S \in UHGraph \land F \in (S GraphIso T)) \land F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T)) \land j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T)) \land y \in dom iEdg (S)) \to (iEdg (T) (j (y)) = F [iEdg (S) (y)] \to (j (y) \in dom iEdg (T) \to iEdg (S) (j^{-1} (j (y))) = F^{-1} [iEdg (T) (j (y))]))$
43	23 42	syld	$⊢ ((((S \in UHGraph \land F \in (S GraphIso T)) \land F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T)) \land j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T)) \land y \in dom iEdg (S)) \to (\forall i \in dom iEdg (S) iEdg (T) (j (i)) = F [iEdg (S) (i)] \to (j (y) \in dom iEdg (T) \to iEdg (S) (j^{-1} (j (y))) = F^{-1} [iEdg (T) (j (y))]))$
44	43	ex	$⊢ (((S \in UHGraph \land F \in (S GraphIso T)) \land F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T)) \land j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T)) \to (y \in dom iEdg (S) \to (\forall i \in dom iEdg (S) iEdg (T) (j (i)) = F [iEdg (S) (i)] \to (j (y) \in dom iEdg (T) \to iEdg (S) (j^{-1} (j (y))) = F^{-1} [iEdg (T) (j (y))])))$
45	44	com23	$⊢ (((S \in UHGraph \land F \in (S GraphIso T)) \land F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T)) \land j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T)) \to (\forall i \in dom iEdg (S) iEdg (T) (j (i)) = F [iEdg (S) (i)] \to (y \in dom iEdg (S) \to (j (y) \in dom iEdg (T) \to iEdg (S) (j^{-1} (j (y))) = F^{-1} [iEdg (T) (j (y))])))$
46	45	impr	$⊢ (((S \in UHGraph \land F \in (S GraphIso T)) \land F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T)) \land (j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T) \land \forall i \in dom iEdg (S) iEdg (T) (j (i)) = F [iEdg (S) (i)])) \to (y \in dom iEdg (S) \to (j (y) \in dom iEdg (T) \to iEdg (S) (j^{-1} (j (y))) = F^{-1} [iEdg (T) (j (y))]))$
47		eleq1	$⊢ j (y) = x \to (j (y) \in dom iEdg (T) \leftrightarrow x \in dom iEdg (T))$
48		2fveq3	$⊢ j (y) = x \to iEdg (S) (j^{-1} (j (y))) = iEdg (S) (j^{-1} (x))$
49		fveq2	$⊢ j (y) = x \to iEdg (T) (j (y)) = iEdg (T) (x)$
50	49	imaeq2d	$⊢ j (y) = x \to F^{-1} [iEdg (T) (j (y))] = F^{-1} [iEdg (T) (x)]$
51	48 50	eqeq12d	$⊢ j (y) = x \to (iEdg (S) (j^{-1} (j (y))) = F^{-1} [iEdg (T) (j (y))] \leftrightarrow iEdg (S) (j^{-1} (x)) = F^{-1} [iEdg (T) (x)])$
52	47 51	imbi12d	$⊢ j (y) = x \to ((j (y) \in dom iEdg (T) \to iEdg (S) (j^{-1} (j (y))) = F^{-1} [iEdg (T) (j (y))]) \leftrightarrow (x \in dom iEdg (T) \to iEdg (S) (j^{-1} (x)) = F^{-1} [iEdg (T) (x)]))$
53	52	imbi2d	$⊢ j (y) = x \to ((y \in dom iEdg (S) \to (j (y) \in dom iEdg (T) \to iEdg (S) (j^{-1} (j (y))) = F^{-1} [iEdg (T) (j (y))])) \leftrightarrow (y \in dom iEdg (S) \to (x \in dom iEdg (T) \to iEdg (S) (j^{-1} (x)) = F^{-1} [iEdg (T) (x)])))$
54	46 53	syl5ibcom	$⊢ (((S \in UHGraph \land F \in (S GraphIso T)) \land F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T)) \land (j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T) \land \forall i \in dom iEdg (S) iEdg (T) (j (i)) = F [iEdg (S) (i)])) \to (j (y) = x \to (y \in dom iEdg (S) \to (x \in dom iEdg (T) \to iEdg (S) (j^{-1} (x)) = F^{-1} [iEdg (T) (x)])))$
55	54	com24	$⊢ (((S \in UHGraph \land F \in (S GraphIso T)) \land F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T)) \land (j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T) \land \forall i \in dom iEdg (S) iEdg (T) (j (i)) = F [iEdg (S) (i)])) \to (x \in dom iEdg (T) \to (y \in dom iEdg (S) \to (j (y) = x \to iEdg (S) (j^{-1} (x)) = F^{-1} [iEdg (T) (x)])))$
56	55	imp31	$⊢ (((((S \in UHGraph \land F \in (S GraphIso T)) \land F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T)) \land (j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T) \land \forall i \in dom iEdg (S) iEdg (T) (j (i)) = F [iEdg (S) (i)])) \land x \in dom iEdg (T)) \land y \in dom iEdg (S)) \to (j (y) = x \to iEdg (S) (j^{-1} (x)) = F^{-1} [iEdg (T) (x)])$
57	56	rexlimdva	$⊢ ((((S \in UHGraph \land F \in (S GraphIso T)) \land F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T)) \land (j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T) \land \forall i \in dom iEdg (S) iEdg (T) (j (i)) = F [iEdg (S) (i)])) \land x \in dom iEdg (T)) \to (\exists y \in dom iEdg (S) j (y) = x \to iEdg (S) (j^{-1} (x)) = F^{-1} [iEdg (T) (x)])$
58	17 57	mpd	$⊢ ((((S \in UHGraph \land F \in (S GraphIso T)) \land F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T)) \land (j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T) \land \forall i \in dom iEdg (S) iEdg (T) (j (i)) = F [iEdg (S) (i)])) \land x \in dom iEdg (T)) \to iEdg (S) (j^{-1} (x)) = F^{-1} [iEdg (T) (x)]$
59	58	ralrimiva	$⊢ (((S \in UHGraph \land F \in (S GraphIso T)) \land F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T)) \land (j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T) \land \forall i \in dom iEdg (S) iEdg (T) (j (i)) = F [iEdg (S) (i)])) \to \forall x \in dom iEdg (T) iEdg (S) (j^{-1} (x)) = F^{-1} [iEdg (T) (x)]$
60	13 59	jca	$⊢ (((S \in UHGraph \land F \in (S GraphIso T)) \land F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T)) \land (j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T) \land \forall i \in dom iEdg (S) iEdg (T) (j (i)) = F [iEdg (S) (i)])) \to (j^{-1} : dom iEdg (T) \underset{1-1 onto}{⟶} dom iEdg (S) \land \forall x \in dom iEdg (T) iEdg (S) (j^{-1} (x)) = F^{-1} [iEdg (T) (x)])$
61		f1oeq1	$⊢ f = j^{-1} \to (f : dom iEdg (T) \underset{1-1 onto}{⟶} dom iEdg (S) \leftrightarrow j^{-1} : dom iEdg (T) \underset{1-1 onto}{⟶} dom iEdg (S))$
62		fveq1	$⊢ f = j^{-1} \to f (x) = j^{-1} (x)$
63	62	fveqeq2d	$⊢ f = j^{-1} \to (iEdg (S) (f (x)) = F^{-1} [iEdg (T) (x)] \leftrightarrow iEdg (S) (j^{-1} (x)) = F^{-1} [iEdg (T) (x)])$
64	63	ralbidv	$⊢ f = j^{-1} \to (\forall x \in dom iEdg (T) iEdg (S) (f (x)) = F^{-1} [iEdg (T) (x)] \leftrightarrow \forall x \in dom iEdg (T) iEdg (S) (j^{-1} (x)) = F^{-1} [iEdg (T) (x)])$
65	61 64	anbi12d	$⊢ f = j^{-1} \to ((f : dom iEdg (T) \underset{1-1 onto}{⟶} dom iEdg (S) \land \forall x \in dom iEdg (T) iEdg (S) (f (x)) = F^{-1} [iEdg (T) (x)]) \leftrightarrow (j^{-1} : dom iEdg (T) \underset{1-1 onto}{⟶} dom iEdg (S) \land \forall x \in dom iEdg (T) iEdg (S) (j^{-1} (x)) = F^{-1} [iEdg (T) (x)]))$
66	11 60 65	spcedv	$⊢ (((S \in UHGraph \land F \in (S GraphIso T)) \land F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T)) \land (j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T) \land \forall i \in dom iEdg (S) iEdg (T) (j (i)) = F [iEdg (S) (i)])) \to \exists f (f : dom iEdg (T) \underset{1-1 onto}{⟶} dom iEdg (S) \land \forall x \in dom iEdg (T) iEdg (S) (f (x)) = F^{-1} [iEdg (T) (x)])$
67	66	ex	$⊢ ((S \in UHGraph \land F \in (S GraphIso T)) \land F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T)) \to ((j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T) \land \forall i \in dom iEdg (S) iEdg (T) (j (i)) = F [iEdg (S) (i)]) \to \exists f (f : dom iEdg (T) \underset{1-1 onto}{⟶} dom iEdg (S) \land \forall x \in dom iEdg (T) iEdg (S) (f (x)) = F^{-1} [iEdg (T) (x)]))$
68	67	exlimdv	$⊢ ((S \in UHGraph \land F \in (S GraphIso T)) \land F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T)) \to (\exists j (j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T) \land \forall i \in dom iEdg (S) iEdg (T) (j (i)) = F [iEdg (S) (i)]) \to \exists f (f : dom iEdg (T) \underset{1-1 onto}{⟶} dom iEdg (S) \land \forall x \in dom iEdg (T) iEdg (S) (f (x)) = F^{-1} [iEdg (T) (x)]))$
69	68	impr	$⊢ ((S \in UHGraph \land F \in (S GraphIso T)) \land (F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T) \land \exists j (j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T) \land \forall i \in dom iEdg (S) iEdg (T) (j (i)) = F [iEdg (S) (i)]))) \to \exists f (f : dom iEdg (T) \underset{1-1 onto}{⟶} dom iEdg (S) \land \forall x \in dom iEdg (T) iEdg (S) (f (x)) = F^{-1} [iEdg (T) (x)])$
70		grimdmrel	$⊢ Rel dom GraphIso$
71	70	ovrcl	$⊢ F \in (S GraphIso T) \to (S \in V \land T \in V)$
72	71	simprd	$⊢ F \in (S GraphIso T) \to T \in V$
73	71	simpld	$⊢ F \in (S GraphIso T) \to S \in V$
74		cnvexg	$⊢ F \in (S GraphIso T) \to F^{-1} \in V$
75	2 1 4 3	isgrim	$⊢ (T \in V \land S \in V \land F^{-1} \in V) \to (F^{-1} \in (T GraphIso S) \leftrightarrow (F^{-1} : Vtx (T) \underset{1-1 onto}{⟶} Vtx (S) \land \exists f (f : dom iEdg (T) \underset{1-1 onto}{⟶} dom iEdg (S) \land \forall x \in dom iEdg (T) iEdg (S) (f (x)) = F^{-1} [iEdg (T) (x)])))$
76	72 73 74 75	syl3anc	$⊢ F \in (S GraphIso T) \to (F^{-1} \in (T GraphIso S) \leftrightarrow (F^{-1} : Vtx (T) \underset{1-1 onto}{⟶} Vtx (S) \land \exists f (f : dom iEdg (T) \underset{1-1 onto}{⟶} dom iEdg (S) \land \forall x \in dom iEdg (T) iEdg (S) (f (x)) = F^{-1} [iEdg (T) (x)])))$
77	76	ad2antlr	$⊢ ((S \in UHGraph \land F \in (S GraphIso T)) \land (F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T) \land \exists j (j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T) \land \forall i \in dom iEdg (S) iEdg (T) (j (i)) = F [iEdg (S) (i)]))) \to (F^{-1} \in (T GraphIso S) \leftrightarrow (F^{-1} : Vtx (T) \underset{1-1 onto}{⟶} Vtx (S) \land \exists f (f : dom iEdg (T) \underset{1-1 onto}{⟶} dom iEdg (S) \land \forall x \in dom iEdg (T) iEdg (S) (f (x)) = F^{-1} [iEdg (T) (x)])))$
78	8 69 77	mpbir2and	$⊢ ((S \in UHGraph \land F \in (S GraphIso T)) \land (F : Vtx (S) \underset{1-1 onto}{⟶} Vtx (T) \land \exists j (j : dom iEdg (S) \underset{1-1 onto}{⟶} dom iEdg (T) \land \forall i \in dom iEdg (S) iEdg (T) (j (i)) = F [iEdg (S) (i)]))) \to F^{-1} \in (T GraphIso S)$
79	6 78	mpdan	$⊢ (S \in UHGraph \land F \in (S GraphIso T)) \to F^{-1} \in (T GraphIso S)$
80	79	ex	$⊢ S \in UHGraph \to (F \in (S GraphIso T) \to F^{-1} \in (T GraphIso S))$

Metamath Proof Explorer

Theorem grimcnv

Proof