isomgr

Description: The isomorphy relation for two graphs. (Contributed by AV, 11-Nov-2022)

	Ref	Expression
Hypotheses	isomgr.v	$⊢ V = Vtx (A)$
	isomgr.w	$⊢ W = Vtx (B)$
	isomgr.i	$⊢ I = iEdg (A)$
	isomgr.j	$⊢ J = iEdg (B)$
Assertion	isomgr	$⊢ (A \in X \land B \in Y) \to (A IsomGr B \leftrightarrow \exists f (f : V \underset{1-1 onto}{⟶} W \land \exists g (g : dom I \underset{1-1 onto}{⟶} dom J \land \forall i \in dom I f [I (i)] = J (g (i)))))$

Proof

Step	Hyp	Ref	Expression
1		isomgr.v	$⊢ V = Vtx (A)$
2		isomgr.w	$⊢ W = Vtx (B)$
3		isomgr.i	$⊢ I = iEdg (A)$
4		isomgr.j	$⊢ J = iEdg (B)$
5		eqidd	$⊢ (x = A \land y = B) \to f = f$
6		fveq2	$⊢ x = A \to Vtx (x) = Vtx (A)$
7	6	adantr	$⊢ (x = A \land y = B) \to Vtx (x) = Vtx (A)$
8	7 1	eqtr4di	$⊢ (x = A \land y = B) \to Vtx (x) = V$
9		fveq2	$⊢ y = B \to Vtx (y) = Vtx (B)$
10	9	adantl	$⊢ (x = A \land y = B) \to Vtx (y) = Vtx (B)$
11	10 2	eqtr4di	$⊢ (x = A \land y = B) \to Vtx (y) = W$
12	5 8 11	f1oeq123d	$⊢ (x = A \land y = B) \to (f : Vtx (x) \underset{1-1 onto}{⟶} Vtx (y) \leftrightarrow f : V \underset{1-1 onto}{⟶} W)$
13		eqidd	$⊢ (x = A \land y = B) \to g = g$
14		fveq2	$⊢ x = A \to iEdg (x) = iEdg (A)$
15	14	adantr	$⊢ (x = A \land y = B) \to iEdg (x) = iEdg (A)$
16	15 3	eqtr4di	$⊢ (x = A \land y = B) \to iEdg (x) = I$
17	16	dmeqd	$⊢ (x = A \land y = B) \to dom iEdg (x) = dom I$
18		fveq2	$⊢ y = B \to iEdg (y) = iEdg (B)$
19	18	adantl	$⊢ (x = A \land y = B) \to iEdg (y) = iEdg (B)$
20	19 4	eqtr4di	$⊢ (x = A \land y = B) \to iEdg (y) = J$
21	20	dmeqd	$⊢ (x = A \land y = B) \to dom iEdg (y) = dom J$
22	13 17 21	f1oeq123d	$⊢ (x = A \land y = B) \to (g : dom iEdg (x) \underset{1-1 onto}{⟶} dom iEdg (y) \leftrightarrow g : dom I \underset{1-1 onto}{⟶} dom J)$
23	16	fveq1d	$⊢ (x = A \land y = B) \to iEdg (x) (i) = I (i)$
24	23	imaeq2d	$⊢ (x = A \land y = B) \to f [iEdg (x) (i)] = f [I (i)]$
25	20	fveq1d	$⊢ (x = A \land y = B) \to iEdg (y) (g (i)) = J (g (i))$
26	24 25	eqeq12d	$⊢ (x = A \land y = B) \to (f [iEdg (x) (i)] = iEdg (y) (g (i)) \leftrightarrow f [I (i)] = J (g (i)))$
27	17 26	raleqbidv	$⊢ (x = A \land y = B) \to (\forall i \in dom iEdg (x) f [iEdg (x) (i)] = iEdg (y) (g (i)) \leftrightarrow \forall i \in dom I f [I (i)] = J (g (i)))$
28	22 27	anbi12d	$⊢ (x = A \land y = B) \to ((g : dom iEdg (x) \underset{1-1 onto}{⟶} dom iEdg (y) \land \forall i \in dom iEdg (x) f [iEdg (x) (i)] = iEdg (y) (g (i))) \leftrightarrow (g : dom I \underset{1-1 onto}{⟶} dom J \land \forall i \in dom I f [I (i)] = J (g (i))))$
29	28	exbidv	$⊢ (x = A \land y = B) \to (\exists g (g : dom iEdg (x) \underset{1-1 onto}{⟶} dom iEdg (y) \land \forall i \in dom iEdg (x) f [iEdg (x) (i)] = iEdg (y) (g (i))) \leftrightarrow \exists g (g : dom I \underset{1-1 onto}{⟶} dom J \land \forall i \in dom I f [I (i)] = J (g (i))))$
30	12 29	anbi12d	$⊢ (x = A \land y = B) \to ((f : Vtx (x) \underset{1-1 onto}{⟶} Vtx (y) \land \exists g (g : dom iEdg (x) \underset{1-1 onto}{⟶} dom iEdg (y) \land \forall i \in dom iEdg (x) f [iEdg (x) (i)] = iEdg (y) (g (i)))) \leftrightarrow (f : V \underset{1-1 onto}{⟶} W \land \exists g (g : dom I \underset{1-1 onto}{⟶} dom J \land \forall i \in dom I f [I (i)] = J (g (i)))))$
31	30	exbidv	$⊢ (x = A \land y = B) \to (\exists f (f : Vtx (x) \underset{1-1 onto}{⟶} Vtx (y) \land \exists g (g : dom iEdg (x) \underset{1-1 onto}{⟶} dom iEdg (y) \land \forall i \in dom iEdg (x) f [iEdg (x) (i)] = iEdg (y) (g (i)))) \leftrightarrow \exists f (f : V \underset{1-1 onto}{⟶} W \land \exists g (g : dom I \underset{1-1 onto}{⟶} dom J \land \forall i \in dom I f [I (i)] = J (g (i)))))$
32		df-isomgr	$⊢ IsomGr = \{⟨x, y⟩ \| \exists f (f : Vtx (x) \underset{1-1 onto}{⟶} Vtx (y) \land \exists g (g : dom iEdg (x) \underset{1-1 onto}{⟶} dom iEdg (y) \land \forall i \in dom iEdg (x) f [iEdg (x) (i)] = iEdg (y) (g (i))))\}$
33	31 32	brabga	$⊢ (A \in X \land B \in Y) \to (A IsomGr B \leftrightarrow \exists f (f : V \underset{1-1 onto}{⟶} W \land \exists g (g : dom I \underset{1-1 onto}{⟶} dom J \land \forall i \in dom I f [I (i)] = J (g (i)))))$

Metamath Proof Explorer

Theorem isomgr

Proof