isomgrsym

Description: The isomorphy relation is symmetric for hypergraphs. (Contributed by AV, 11-Nov-2022)

		Ref	Expression
	Assertion	isomgrsym	$⊢ (A \in UHGraph \land B \in Y) \to (A IsomGr B \to B IsomGr A)$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ Vtx (A) = Vtx (A)$
2		eqid	$⊢ Vtx (B) = Vtx (B)$
3		eqid	$⊢ iEdg (A) = iEdg (A)$
4		eqid	$⊢ iEdg (B) = iEdg (B)$
5	1 2 3 4	isomgr	$⊢ (A \in UHGraph \land B \in Y) \to (A IsomGr B \leftrightarrow \exists f (f : Vtx (A) \underset{1-1 onto}{⟶} Vtx (B) \land \exists g (g : dom iEdg (A) \underset{1-1 onto}{⟶} dom iEdg (B) \land \forall i \in dom iEdg (A) f [iEdg (A) (i)] = iEdg (B) (g (i)))))$
6		vex	$⊢ f \in V$
7	6	cnvex	$⊢ f^{-1} \in V$
8	7	a1i	$⊢ ((A \in UHGraph \land B \in Y) \land (f : Vtx (A) \underset{1-1 onto}{⟶} Vtx (B) \land \exists g (g : dom iEdg (A) \underset{1-1 onto}{⟶} dom iEdg (B) \land \forall i \in dom iEdg (A) f [iEdg (A) (i)] = iEdg (B) (g (i))))) \to f^{-1} \in V$
9		f1ocnv	$⊢ f : Vtx (A) \underset{1-1 onto}{⟶} Vtx (B) \to f^{-1} : Vtx (B) \underset{1-1 onto}{⟶} Vtx (A)$
10	9	adantr	$⊢ (f : Vtx (A) \underset{1-1 onto}{⟶} Vtx (B) \land \exists g (g : dom iEdg (A) \underset{1-1 onto}{⟶} dom iEdg (B) \land \forall i \in dom iEdg (A) f [iEdg (A) (i)] = iEdg (B) (g (i)))) \to f^{-1} : Vtx (B) \underset{1-1 onto}{⟶} Vtx (A)$
11	10	adantl	$⊢ ((A \in UHGraph \land B \in Y) \land (f : Vtx (A) \underset{1-1 onto}{⟶} Vtx (B) \land \exists g (g : dom iEdg (A) \underset{1-1 onto}{⟶} dom iEdg (B) \land \forall i \in dom iEdg (A) f [iEdg (A) (i)] = iEdg (B) (g (i))))) \to f^{-1} : Vtx (B) \underset{1-1 onto}{⟶} Vtx (A)$
12		vex	$⊢ g \in V$
13	12	cnvex	$⊢ g^{-1} \in V$
14	13	a1i	$⊢ ((A \in UHGraph \land B \in Y) \land (g : dom iEdg (A) \underset{1-1 onto}{⟶} dom iEdg (B) \land \forall i \in dom iEdg (A) f [iEdg (A) (i)] = iEdg (B) (g (i))) \land f : Vtx (A) \underset{1-1 onto}{⟶} Vtx (B)) \to g^{-1} \in V$
15		f1ocnv	$⊢ g : dom iEdg (A) \underset{1-1 onto}{⟶} dom iEdg (B) \to g^{-1} : dom iEdg (B) \underset{1-1 onto}{⟶} dom iEdg (A)$
16	15	adantr	$⊢ (g : dom iEdg (A) \underset{1-1 onto}{⟶} dom iEdg (B) \land \forall i \in dom iEdg (A) f [iEdg (A) (i)] = iEdg (B) (g (i))) \to g^{-1} : dom iEdg (B) \underset{1-1 onto}{⟶} dom iEdg (A)$
17	16	3ad2ant2	$⊢ ((A \in UHGraph \land B \in Y) \land (g : dom iEdg (A) \underset{1-1 onto}{⟶} dom iEdg (B) \land \forall i \in dom iEdg (A) f [iEdg (A) (i)] = iEdg (B) (g (i))) \land f : Vtx (A) \underset{1-1 onto}{⟶} Vtx (B)) \to g^{-1} : dom iEdg (B) \underset{1-1 onto}{⟶} dom iEdg (A)$
18		f1ocnvdm	$⊢ (g : dom iEdg (A) \underset{1-1 onto}{⟶} dom iEdg (B) \land j \in dom iEdg (B)) \to g^{-1} (j) \in dom iEdg (A)$
19	18	3ad2antl2	$⊢ (((A \in UHGraph \land B \in Y) \land g : dom iEdg (A) \underset{1-1 onto}{⟶} dom iEdg (B) \land f : Vtx (A) \underset{1-1 onto}{⟶} Vtx (B)) \land j \in dom iEdg (B)) \to g^{-1} (j) \in dom iEdg (A)$
20		fveq2	$⊢ i = g^{-1} (j) \to iEdg (A) (i) = iEdg (A) (g^{-1} (j))$
21	20	imaeq2d	$⊢ i = g^{-1} (j) \to f [iEdg (A) (i)] = f [iEdg (A) (g^{-1} (j))]$
22		2fveq3	$⊢ i = g^{-1} (j) \to iEdg (B) (g (i)) = iEdg (B) (g (g^{-1} (j)))$
23	21 22	eqeq12d	$⊢ i = g^{-1} (j) \to (f [iEdg (A) (i)] = iEdg (B) (g (i)) \leftrightarrow f [iEdg (A) (g^{-1} (j))] = iEdg (B) (g (g^{-1} (j))))$
24	23	adantl	$⊢ ((((A \in UHGraph \land B \in Y) \land g : dom iEdg (A) \underset{1-1 onto}{⟶} dom iEdg (B) \land f : Vtx (A) \underset{1-1 onto}{⟶} Vtx (B)) \land j \in dom iEdg (B)) \land i = g^{-1} (j)) \to (f [iEdg (A) (i)] = iEdg (B) (g (i)) \leftrightarrow f [iEdg (A) (g^{-1} (j))] = iEdg (B) (g (g^{-1} (j))))$
25	19 24	rspcdv	$⊢ (((A \in UHGraph \land B \in Y) \land g : dom iEdg (A) \underset{1-1 onto}{⟶} dom iEdg (B) \land f : Vtx (A) \underset{1-1 onto}{⟶} Vtx (B)) \land j \in dom iEdg (B)) \to (\forall i \in dom iEdg (A) f [iEdg (A) (i)] = iEdg (B) (g (i)) \to f [iEdg (A) (g^{-1} (j))] = iEdg (B) (g (g^{-1} (j))))$
26		f1ocnvfv2	$⊢ (g : dom iEdg (A) \underset{1-1 onto}{⟶} dom iEdg (B) \land j \in dom iEdg (B)) \to g (g^{-1} (j)) = j$
27	26	3ad2antl2	$⊢ (((A \in UHGraph \land B \in Y) \land g : dom iEdg (A) \underset{1-1 onto}{⟶} dom iEdg (B) \land f : Vtx (A) \underset{1-1 onto}{⟶} Vtx (B)) \land j \in dom iEdg (B)) \to g (g^{-1} (j)) = j$
28	27	fveq2d	$⊢ (((A \in UHGraph \land B \in Y) \land g : dom iEdg (A) \underset{1-1 onto}{⟶} dom iEdg (B) \land f : Vtx (A) \underset{1-1 onto}{⟶} Vtx (B)) \land j \in dom iEdg (B)) \to iEdg (B) (g (g^{-1} (j))) = iEdg (B) (j)$
29	28	eqeq2d	$⊢ (((A \in UHGraph \land B \in Y) \land g : dom iEdg (A) \underset{1-1 onto}{⟶} dom iEdg (B) \land f : Vtx (A) \underset{1-1 onto}{⟶} Vtx (B)) \land j \in dom iEdg (B)) \to (f [iEdg (A) (g^{-1} (j))] = iEdg (B) (g (g^{-1} (j))) \leftrightarrow f [iEdg (A) (g^{-1} (j))] = iEdg (B) (j))$
30		f1of1	$⊢ f : Vtx (A) \underset{1-1 onto}{⟶} Vtx (B) \to f : Vtx (A) \underset{1-1}{⟶} Vtx (B)$
31	30	3ad2ant3	$⊢ ((A \in UHGraph \land B \in Y) \land g : dom iEdg (A) \underset{1-1 onto}{⟶} dom iEdg (B) \land f : Vtx (A) \underset{1-1 onto}{⟶} Vtx (B)) \to f : Vtx (A) \underset{1-1}{⟶} Vtx (B)$
32	31	adantr	$⊢ (((A \in UHGraph \land B \in Y) \land g : dom iEdg (A) \underset{1-1 onto}{⟶} dom iEdg (B) \land f : Vtx (A) \underset{1-1 onto}{⟶} Vtx (B)) \land j \in dom iEdg (B)) \to f : Vtx (A) \underset{1-1}{⟶} Vtx (B)$
33		simpl1l	$⊢ (((A \in UHGraph \land B \in Y) \land g : dom iEdg (A) \underset{1-1 onto}{⟶} dom iEdg (B) \land f : Vtx (A) \underset{1-1 onto}{⟶} Vtx (B)) \land j \in dom iEdg (B)) \to A \in UHGraph$
34	1 3	uhgrss	$⊢ (A \in UHGraph \land g^{-1} (j) \in dom iEdg (A)) \to iEdg (A) (g^{-1} (j)) \subseteq Vtx (A)$
35	33 19 34	syl2anc	$⊢ (((A \in UHGraph \land B \in Y) \land g : dom iEdg (A) \underset{1-1 onto}{⟶} dom iEdg (B) \land f : Vtx (A) \underset{1-1 onto}{⟶} Vtx (B)) \land j \in dom iEdg (B)) \to iEdg (A) (g^{-1} (j)) \subseteq Vtx (A)$
36	32 35	jca	$⊢ (((A \in UHGraph \land B \in Y) \land g : dom iEdg (A) \underset{1-1 onto}{⟶} dom iEdg (B) \land f : Vtx (A) \underset{1-1 onto}{⟶} Vtx (B)) \land j \in dom iEdg (B)) \to (f : Vtx (A) \underset{1-1}{⟶} Vtx (B) \land iEdg (A) (g^{-1} (j)) \subseteq Vtx (A))$
37	36	adantr	$⊢ ((((A \in UHGraph \land B \in Y) \land g : dom iEdg (A) \underset{1-1 onto}{⟶} dom iEdg (B) \land f : Vtx (A) \underset{1-1 onto}{⟶} Vtx (B)) \land j \in dom iEdg (B)) \land f [iEdg (A) (g^{-1} (j))] = iEdg (B) (j)) \to (f : Vtx (A) \underset{1-1}{⟶} Vtx (B) \land iEdg (A) (g^{-1} (j)) \subseteq Vtx (A))$
38		f1imacnv	$⊢ (f : Vtx (A) \underset{1-1}{⟶} Vtx (B) \land iEdg (A) (g^{-1} (j)) \subseteq Vtx (A)) \to f^{-1} [f [iEdg (A) (g^{-1} (j))]] = iEdg (A) (g^{-1} (j))$
39	37 38	syl	$⊢ ((((A \in UHGraph \land B \in Y) \land g : dom iEdg (A) \underset{1-1 onto}{⟶} dom iEdg (B) \land f : Vtx (A) \underset{1-1 onto}{⟶} Vtx (B)) \land j \in dom iEdg (B)) \land f [iEdg (A) (g^{-1} (j))] = iEdg (B) (j)) \to f^{-1} [f [iEdg (A) (g^{-1} (j))]] = iEdg (A) (g^{-1} (j))$
40		imaeq2	$⊢ f [iEdg (A) (g^{-1} (j))] = iEdg (B) (j) \to f^{-1} [f [iEdg (A) (g^{-1} (j))]] = f^{-1} [iEdg (B) (j)]$
41	40	adantl	$⊢ ((((A \in UHGraph \land B \in Y) \land g : dom iEdg (A) \underset{1-1 onto}{⟶} dom iEdg (B) \land f : Vtx (A) \underset{1-1 onto}{⟶} Vtx (B)) \land j \in dom iEdg (B)) \land f [iEdg (A) (g^{-1} (j))] = iEdg (B) (j)) \to f^{-1} [f [iEdg (A) (g^{-1} (j))]] = f^{-1} [iEdg (B) (j)]$
42	39 41	eqtr3d	$⊢ ((((A \in UHGraph \land B \in Y) \land g : dom iEdg (A) \underset{1-1 onto}{⟶} dom iEdg (B) \land f : Vtx (A) \underset{1-1 onto}{⟶} Vtx (B)) \land j \in dom iEdg (B)) \land f [iEdg (A) (g^{-1} (j))] = iEdg (B) (j)) \to iEdg (A) (g^{-1} (j)) = f^{-1} [iEdg (B) (j)]$
43	42	ex	$⊢ (((A \in UHGraph \land B \in Y) \land g : dom iEdg (A) \underset{1-1 onto}{⟶} dom iEdg (B) \land f : Vtx (A) \underset{1-1 onto}{⟶} Vtx (B)) \land j \in dom iEdg (B)) \to (f [iEdg (A) (g^{-1} (j))] = iEdg (B) (j) \to iEdg (A) (g^{-1} (j)) = f^{-1} [iEdg (B) (j)])$
44	29 43	sylbid	$⊢ (((A \in UHGraph \land B \in Y) \land g : dom iEdg (A) \underset{1-1 onto}{⟶} dom iEdg (B) \land f : Vtx (A) \underset{1-1 onto}{⟶} Vtx (B)) \land j \in dom iEdg (B)) \to (f [iEdg (A) (g^{-1} (j))] = iEdg (B) (g (g^{-1} (j))) \to iEdg (A) (g^{-1} (j)) = f^{-1} [iEdg (B) (j)])$
45	25 44	syld	$⊢ (((A \in UHGraph \land B \in Y) \land g : dom iEdg (A) \underset{1-1 onto}{⟶} dom iEdg (B) \land f : Vtx (A) \underset{1-1 onto}{⟶} Vtx (B)) \land j \in dom iEdg (B)) \to (\forall i \in dom iEdg (A) f [iEdg (A) (i)] = iEdg (B) (g (i)) \to iEdg (A) (g^{-1} (j)) = f^{-1} [iEdg (B) (j)])$
46	45	ex	$⊢ ((A \in UHGraph \land B \in Y) \land g : dom iEdg (A) \underset{1-1 onto}{⟶} dom iEdg (B) \land f : Vtx (A) \underset{1-1 onto}{⟶} Vtx (B)) \to (j \in dom iEdg (B) \to (\forall i \in dom iEdg (A) f [iEdg (A) (i)] = iEdg (B) (g (i)) \to iEdg (A) (g^{-1} (j)) = f^{-1} [iEdg (B) (j)]))$
47	46	com23	$⊢ ((A \in UHGraph \land B \in Y) \land g : dom iEdg (A) \underset{1-1 onto}{⟶} dom iEdg (B) \land f : Vtx (A) \underset{1-1 onto}{⟶} Vtx (B)) \to (\forall i \in dom iEdg (A) f [iEdg (A) (i)] = iEdg (B) (g (i)) \to (j \in dom iEdg (B) \to iEdg (A) (g^{-1} (j)) = f^{-1} [iEdg (B) (j)]))$
48	47	3exp	$⊢ (A \in UHGraph \land B \in Y) \to (g : dom iEdg (A) \underset{1-1 onto}{⟶} dom iEdg (B) \to (f : Vtx (A) \underset{1-1 onto}{⟶} Vtx (B) \to (\forall i \in dom iEdg (A) f [iEdg (A) (i)] = iEdg (B) (g (i)) \to (j \in dom iEdg (B) \to iEdg (A) (g^{-1} (j)) = f^{-1} [iEdg (B) (j)]))))$
49	48	com34	$⊢ (A \in UHGraph \land B \in Y) \to (g : dom iEdg (A) \underset{1-1 onto}{⟶} dom iEdg (B) \to (\forall i \in dom iEdg (A) f [iEdg (A) (i)] = iEdg (B) (g (i)) \to (f : Vtx (A) \underset{1-1 onto}{⟶} Vtx (B) \to (j \in dom iEdg (B) \to iEdg (A) (g^{-1} (j)) = f^{-1} [iEdg (B) (j)]))))$
50	49	impd	$⊢ (A \in UHGraph \land B \in Y) \to ((g : dom iEdg (A) \underset{1-1 onto}{⟶} dom iEdg (B) \land \forall i \in dom iEdg (A) f [iEdg (A) (i)] = iEdg (B) (g (i))) \to (f : Vtx (A) \underset{1-1 onto}{⟶} Vtx (B) \to (j \in dom iEdg (B) \to iEdg (A) (g^{-1} (j)) = f^{-1} [iEdg (B) (j)])))$
51	50	3imp1	$⊢ (((A \in UHGraph \land B \in Y) \land (g : dom iEdg (A) \underset{1-1 onto}{⟶} dom iEdg (B) \land \forall i \in dom iEdg (A) f [iEdg (A) (i)] = iEdg (B) (g (i))) \land f : Vtx (A) \underset{1-1 onto}{⟶} Vtx (B)) \land j \in dom iEdg (B)) \to iEdg (A) (g^{-1} (j)) = f^{-1} [iEdg (B) (j)]$
52	51	eqcomd	$⊢ (((A \in UHGraph \land B \in Y) \land (g : dom iEdg (A) \underset{1-1 onto}{⟶} dom iEdg (B) \land \forall i \in dom iEdg (A) f [iEdg (A) (i)] = iEdg (B) (g (i))) \land f : Vtx (A) \underset{1-1 onto}{⟶} Vtx (B)) \land j \in dom iEdg (B)) \to f^{-1} [iEdg (B) (j)] = iEdg (A) (g^{-1} (j))$
53	52	ralrimiva	$⊢ ((A \in UHGraph \land B \in Y) \land (g : dom iEdg (A) \underset{1-1 onto}{⟶} dom iEdg (B) \land \forall i \in dom iEdg (A) f [iEdg (A) (i)] = iEdg (B) (g (i))) \land f : Vtx (A) \underset{1-1 onto}{⟶} Vtx (B)) \to \forall j \in dom iEdg (B) f^{-1} [iEdg (B) (j)] = iEdg (A) (g^{-1} (j))$
54	17 53	jca	$⊢ ((A \in UHGraph \land B \in Y) \land (g : dom iEdg (A) \underset{1-1 onto}{⟶} dom iEdg (B) \land \forall i \in dom iEdg (A) f [iEdg (A) (i)] = iEdg (B) (g (i))) \land f : Vtx (A) \underset{1-1 onto}{⟶} Vtx (B)) \to (g^{-1} : dom iEdg (B) \underset{1-1 onto}{⟶} dom iEdg (A) \land \forall j \in dom iEdg (B) f^{-1} [iEdg (B) (j)] = iEdg (A) (g^{-1} (j)))$
55		f1oeq1	$⊢ h = g^{-1} \to (h : dom iEdg (B) \underset{1-1 onto}{⟶} dom iEdg (A) \leftrightarrow g^{-1} : dom iEdg (B) \underset{1-1 onto}{⟶} dom iEdg (A))$
56		fveq1	$⊢ h = g^{-1} \to h (j) = g^{-1} (j)$
57	56	fveq2d	$⊢ h = g^{-1} \to iEdg (A) (h (j)) = iEdg (A) (g^{-1} (j))$
58	57	eqeq2d	$⊢ h = g^{-1} \to (f^{-1} [iEdg (B) (j)] = iEdg (A) (h (j)) \leftrightarrow f^{-1} [iEdg (B) (j)] = iEdg (A) (g^{-1} (j)))$
59	58	ralbidv	$⊢ h = g^{-1} \to (\forall j \in dom iEdg (B) f^{-1} [iEdg (B) (j)] = iEdg (A) (h (j)) \leftrightarrow \forall j \in dom iEdg (B) f^{-1} [iEdg (B) (j)] = iEdg (A) (g^{-1} (j)))$
60	55 59	anbi12d	$⊢ h = g^{-1} \to ((h : dom iEdg (B) \underset{1-1 onto}{⟶} dom iEdg (A) \land \forall j \in dom iEdg (B) f^{-1} [iEdg (B) (j)] = iEdg (A) (h (j))) \leftrightarrow (g^{-1} : dom iEdg (B) \underset{1-1 onto}{⟶} dom iEdg (A) \land \forall j \in dom iEdg (B) f^{-1} [iEdg (B) (j)] = iEdg (A) (g^{-1} (j))))$
61	14 54 60	spcedv	$⊢ ((A \in UHGraph \land B \in Y) \land (g : dom iEdg (A) \underset{1-1 onto}{⟶} dom iEdg (B) \land \forall i \in dom iEdg (A) f [iEdg (A) (i)] = iEdg (B) (g (i))) \land f : Vtx (A) \underset{1-1 onto}{⟶} Vtx (B)) \to \exists h (h : dom iEdg (B) \underset{1-1 onto}{⟶} dom iEdg (A) \land \forall j \in dom iEdg (B) f^{-1} [iEdg (B) (j)] = iEdg (A) (h (j)))$
62	61	3exp	$⊢ (A \in UHGraph \land B \in Y) \to ((g : dom iEdg (A) \underset{1-1 onto}{⟶} dom iEdg (B) \land \forall i \in dom iEdg (A) f [iEdg (A) (i)] = iEdg (B) (g (i))) \to (f : Vtx (A) \underset{1-1 onto}{⟶} Vtx (B) \to \exists h (h : dom iEdg (B) \underset{1-1 onto}{⟶} dom iEdg (A) \land \forall j \in dom iEdg (B) f^{-1} [iEdg (B) (j)] = iEdg (A) (h (j)))))$
63	62	exlimdv	$⊢ (A \in UHGraph \land B \in Y) \to (\exists g (g : dom iEdg (A) \underset{1-1 onto}{⟶} dom iEdg (B) \land \forall i \in dom iEdg (A) f [iEdg (A) (i)] = iEdg (B) (g (i))) \to (f : Vtx (A) \underset{1-1 onto}{⟶} Vtx (B) \to \exists h (h : dom iEdg (B) \underset{1-1 onto}{⟶} dom iEdg (A) \land \forall j \in dom iEdg (B) f^{-1} [iEdg (B) (j)] = iEdg (A) (h (j)))))$
64	63	com23	$⊢ (A \in UHGraph \land B \in Y) \to (f : Vtx (A) \underset{1-1 onto}{⟶} Vtx (B) \to (\exists g (g : dom iEdg (A) \underset{1-1 onto}{⟶} dom iEdg (B) \land \forall i \in dom iEdg (A) f [iEdg (A) (i)] = iEdg (B) (g (i))) \to \exists h (h : dom iEdg (B) \underset{1-1 onto}{⟶} dom iEdg (A) \land \forall j \in dom iEdg (B) f^{-1} [iEdg (B) (j)] = iEdg (A) (h (j)))))$
65	64	imp32	$⊢ ((A \in UHGraph \land B \in Y) \land (f : Vtx (A) \underset{1-1 onto}{⟶} Vtx (B) \land \exists g (g : dom iEdg (A) \underset{1-1 onto}{⟶} dom iEdg (B) \land \forall i \in dom iEdg (A) f [iEdg (A) (i)] = iEdg (B) (g (i))))) \to \exists h (h : dom iEdg (B) \underset{1-1 onto}{⟶} dom iEdg (A) \land \forall j \in dom iEdg (B) f^{-1} [iEdg (B) (j)] = iEdg (A) (h (j)))$
66	11 65	jca	$⊢ ((A \in UHGraph \land B \in Y) \land (f : Vtx (A) \underset{1-1 onto}{⟶} Vtx (B) \land \exists g (g : dom iEdg (A) \underset{1-1 onto}{⟶} dom iEdg (B) \land \forall i \in dom iEdg (A) f [iEdg (A) (i)] = iEdg (B) (g (i))))) \to (f^{-1} : Vtx (B) \underset{1-1 onto}{⟶} Vtx (A) \land \exists h (h : dom iEdg (B) \underset{1-1 onto}{⟶} dom iEdg (A) \land \forall j \in dom iEdg (B) f^{-1} [iEdg (B) (j)] = iEdg (A) (h (j))))$
67		f1oeq1	$⊢ e = f^{-1} \to (e : Vtx (B) \underset{1-1 onto}{⟶} Vtx (A) \leftrightarrow f^{-1} : Vtx (B) \underset{1-1 onto}{⟶} Vtx (A))$
68		imaeq1	$⊢ e = f^{-1} \to e [iEdg (B) (j)] = f^{-1} [iEdg (B) (j)]$
69	68	eqeq1d	$⊢ e = f^{-1} \to (e [iEdg (B) (j)] = iEdg (A) (h (j)) \leftrightarrow f^{-1} [iEdg (B) (j)] = iEdg (A) (h (j)))$
70	69	ralbidv	$⊢ e = f^{-1} \to (\forall j \in dom iEdg (B) e [iEdg (B) (j)] = iEdg (A) (h (j)) \leftrightarrow \forall j \in dom iEdg (B) f^{-1} [iEdg (B) (j)] = iEdg (A) (h (j)))$
71	70	anbi2d	$⊢ e = f^{-1} \to ((h : dom iEdg (B) \underset{1-1 onto}{⟶} dom iEdg (A) \land \forall j \in dom iEdg (B) e [iEdg (B) (j)] = iEdg (A) (h (j))) \leftrightarrow (h : dom iEdg (B) \underset{1-1 onto}{⟶} dom iEdg (A) \land \forall j \in dom iEdg (B) f^{-1} [iEdg (B) (j)] = iEdg (A) (h (j))))$
72	71	exbidv	$⊢ e = f^{-1} \to (\exists h (h : dom iEdg (B) \underset{1-1 onto}{⟶} dom iEdg (A) \land \forall j \in dom iEdg (B) e [iEdg (B) (j)] = iEdg (A) (h (j))) \leftrightarrow \exists h (h : dom iEdg (B) \underset{1-1 onto}{⟶} dom iEdg (A) \land \forall j \in dom iEdg (B) f^{-1} [iEdg (B) (j)] = iEdg (A) (h (j))))$
73	67 72	anbi12d	$⊢ e = f^{-1} \to ((e : Vtx (B) \underset{1-1 onto}{⟶} Vtx (A) \land \exists h (h : dom iEdg (B) \underset{1-1 onto}{⟶} dom iEdg (A) \land \forall j \in dom iEdg (B) e [iEdg (B) (j)] = iEdg (A) (h (j)))) \leftrightarrow (f^{-1} : Vtx (B) \underset{1-1 onto}{⟶} Vtx (A) \land \exists h (h : dom iEdg (B) \underset{1-1 onto}{⟶} dom iEdg (A) \land \forall j \in dom iEdg (B) f^{-1} [iEdg (B) (j)] = iEdg (A) (h (j)))))$
74	8 66 73	spcedv	$⊢ ((A \in UHGraph \land B \in Y) \land (f : Vtx (A) \underset{1-1 onto}{⟶} Vtx (B) \land \exists g (g : dom iEdg (A) \underset{1-1 onto}{⟶} dom iEdg (B) \land \forall i \in dom iEdg (A) f [iEdg (A) (i)] = iEdg (B) (g (i))))) \to \exists e (e : Vtx (B) \underset{1-1 onto}{⟶} Vtx (A) \land \exists h (h : dom iEdg (B) \underset{1-1 onto}{⟶} dom iEdg (A) \land \forall j \in dom iEdg (B) e [iEdg (B) (j)] = iEdg (A) (h (j))))$
75	2 1 4 3	isomgr	$⊢ (B \in Y \land A \in UHGraph) \to (B IsomGr A \leftrightarrow \exists e (e : Vtx (B) \underset{1-1 onto}{⟶} Vtx (A) \land \exists h (h : dom iEdg (B) \underset{1-1 onto}{⟶} dom iEdg (A) \land \forall j \in dom iEdg (B) e [iEdg (B) (j)] = iEdg (A) (h (j)))))$
76	75	ancoms	$⊢ (A \in UHGraph \land B \in Y) \to (B IsomGr A \leftrightarrow \exists e (e : Vtx (B) \underset{1-1 onto}{⟶} Vtx (A) \land \exists h (h : dom iEdg (B) \underset{1-1 onto}{⟶} dom iEdg (A) \land \forall j \in dom iEdg (B) e [iEdg (B) (j)] = iEdg (A) (h (j)))))$
77	76	adantr	$⊢ ((A \in UHGraph \land B \in Y) \land (f : Vtx (A) \underset{1-1 onto}{⟶} Vtx (B) \land \exists g (g : dom iEdg (A) \underset{1-1 onto}{⟶} dom iEdg (B) \land \forall i \in dom iEdg (A) f [iEdg (A) (i)] = iEdg (B) (g (i))))) \to (B IsomGr A \leftrightarrow \exists e (e : Vtx (B) \underset{1-1 onto}{⟶} Vtx (A) \land \exists h (h : dom iEdg (B) \underset{1-1 onto}{⟶} dom iEdg (A) \land \forall j \in dom iEdg (B) e [iEdg (B) (j)] = iEdg (A) (h (j)))))$
78	74 77	mpbird	$⊢ ((A \in UHGraph \land B \in Y) \land (f : Vtx (A) \underset{1-1 onto}{⟶} Vtx (B) \land \exists g (g : dom iEdg (A) \underset{1-1 onto}{⟶} dom iEdg (B) \land \forall i \in dom iEdg (A) f [iEdg (A) (i)] = iEdg (B) (g (i))))) \to B IsomGr A$
79	78	ex	$⊢ (A \in UHGraph \land B \in Y) \to ((f : Vtx (A) \underset{1-1 onto}{⟶} Vtx (B) \land \exists g (g : dom iEdg (A) \underset{1-1 onto}{⟶} dom iEdg (B) \land \forall i \in dom iEdg (A) f [iEdg (A) (i)] = iEdg (B) (g (i)))) \to B IsomGr A)$
80	79	exlimdv	$⊢ (A \in UHGraph \land B \in Y) \to (\exists f (f : Vtx (A) \underset{1-1 onto}{⟶} Vtx (B) \land \exists g (g : dom iEdg (A) \underset{1-1 onto}{⟶} dom iEdg (B) \land \forall i \in dom iEdg (A) f [iEdg (A) (i)] = iEdg (B) (g (i)))) \to B IsomGr A)$
81	5 80	sylbid	$⊢ (A \in UHGraph \land B \in Y) \to (A IsomGr B \to B IsomGr A)$

Metamath Proof Explorer

Theorem isomgrsym

Proof