Theorem isuspgrim

Description: A class is an isomorphism of simple pseudographs iff it 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. This corresponds to the formal definition in Bollobas p. 3 and the definition in Diestel p. 3. (Contributed by AV, 27-Apr-2025)

	Ref	Expression
Hypotheses	isusgrim.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	isusgrim.w	⊢ 𝑊 = ( Vtx ‘ 𝐻 )
	isusgrim.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
	isusgrim.d	⊢ 𝐷 = ( Edg ‘ 𝐻 )
Assertion	isuspgrim	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) → ( 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ↔ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) } ∈ 𝐷 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		isusgrim.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		isusgrim.w	⊢ 𝑊 = ( Vtx ‘ 𝐻 )
3		isusgrim.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
4		isusgrim.d	⊢ 𝐷 = ( Edg ‘ 𝐻 )
5	1 2 3 4	uspgrimprop	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) → ( 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) → ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) } ∈ 𝐷 ) ) ) )
6		f1of	⊢ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 → 𝐹 : 𝑉 ⟶ 𝑊 )
7	1	fvexi	⊢ 𝑉 ∈ V
8	7	a1i	⊢ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 → 𝑉 ∈ V )
9	6 8	fexd	⊢ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 → 𝐹 ∈ V )
10	9	adantl	⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) → 𝐹 ∈ V )
11		simpllr	⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝐹 ∈ V ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) } ∈ 𝐷 ) ) → 𝐹 : 𝑉 –1-1-onto→ 𝑊 )
12	1 2 3 4	isuspgrimlem	⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) } ∈ 𝐷 ) ) → ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) : 𝐸 –1-1-onto→ 𝐷 )
13	12	adantlr	⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝐹 ∈ V ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) } ∈ 𝐷 ) ) → ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) : 𝐸 –1-1-onto→ 𝐷 )
14	1 2 3 4	isuspgrim0	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ V ) → ( 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ↔ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) : 𝐸 –1-1-onto→ 𝐷 ) ) )
15	14	ad5ant124	⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝐹 ∈ V ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) } ∈ 𝐷 ) ) → ( 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ↔ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) : 𝐸 –1-1-onto→ 𝐷 ) ) )
16	11 13 15	mpbir2and	⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝐹 ∈ V ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) } ∈ 𝐷 ) ) → 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) )
17	16	ex	⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝐹 ∈ V ) → ( ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) } ∈ 𝐷 ) → 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ) )
18	10 17	mpdan	⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) → ( ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) } ∈ 𝐷 ) → 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ) )
19	18	expimpd	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) → ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) } ∈ 𝐷 ) ) → 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ) )
20	5 19	impbid	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) → ( 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ↔ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) } ∈ 𝐷 ) ) ) )