# Metamath Proof Explorer

## Theorem isomgr

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

Ref Expression
Hypotheses isomgr.v 𝑉 = ( Vtx ‘ 𝐴 )
isomgr.w 𝑊 = ( Vtx ‘ 𝐵 )
isomgr.i 𝐼 = ( iEdg ‘ 𝐴 )
isomgr.j 𝐽 = ( iEdg ‘ 𝐵 )
Assertion isomgr ( ( 𝐴𝑋𝐵𝑌 ) → ( 𝐴 IsomGr 𝐵 ↔ ∃ 𝑓 ( 𝑓 : 𝑉1-1-onto𝑊 ∧ ∃ 𝑔 ( 𝑔 : dom 𝐼1-1-onto→ dom 𝐽 ∧ ∀ 𝑖 ∈ dom 𝐼 ( 𝑓 “ ( 𝐼𝑖 ) ) = ( 𝐽 ‘ ( 𝑔𝑖 ) ) ) ) ) )

### Proof

Step Hyp Ref Expression
1 isomgr.v 𝑉 = ( Vtx ‘ 𝐴 )
2 isomgr.w 𝑊 = ( Vtx ‘ 𝐵 )
3 isomgr.i 𝐼 = ( iEdg ‘ 𝐴 )
4 isomgr.j 𝐽 = ( iEdg ‘ 𝐵 )
5 eqidd ( ( 𝑥 = 𝐴𝑦 = 𝐵 ) → 𝑓 = 𝑓 )
6 fveq2 ( 𝑥 = 𝐴 → ( Vtx ‘ 𝑥 ) = ( Vtx ‘ 𝐴 ) )
7 6 adantr ( ( 𝑥 = 𝐴𝑦 = 𝐵 ) → ( Vtx ‘ 𝑥 ) = ( Vtx ‘ 𝐴 ) )
8 7 1 eqtr4di ( ( 𝑥 = 𝐴𝑦 = 𝐵 ) → ( Vtx ‘ 𝑥 ) = 𝑉 )
9 fveq2 ( 𝑦 = 𝐵 → ( Vtx ‘ 𝑦 ) = ( Vtx ‘ 𝐵 ) )
10 9 adantl ( ( 𝑥 = 𝐴𝑦 = 𝐵 ) → ( Vtx ‘ 𝑦 ) = ( Vtx ‘ 𝐵 ) )
11 10 2 eqtr4di ( ( 𝑥 = 𝐴𝑦 = 𝐵 ) → ( Vtx ‘ 𝑦 ) = 𝑊 )
12 5 8 11 f1oeq123d ( ( 𝑥 = 𝐴𝑦 = 𝐵 ) → ( 𝑓 : ( Vtx ‘ 𝑥 ) –1-1-onto→ ( Vtx ‘ 𝑦 ) ↔ 𝑓 : 𝑉1-1-onto𝑊 ) )
13 eqidd ( ( 𝑥 = 𝐴𝑦 = 𝐵 ) → 𝑔 = 𝑔 )
14 fveq2 ( 𝑥 = 𝐴 → ( iEdg ‘ 𝑥 ) = ( iEdg ‘ 𝐴 ) )
15 14 adantr ( ( 𝑥 = 𝐴𝑦 = 𝐵 ) → ( iEdg ‘ 𝑥 ) = ( iEdg ‘ 𝐴 ) )
16 15 3 eqtr4di ( ( 𝑥 = 𝐴𝑦 = 𝐵 ) → ( iEdg ‘ 𝑥 ) = 𝐼 )
17 16 dmeqd ( ( 𝑥 = 𝐴𝑦 = 𝐵 ) → dom ( iEdg ‘ 𝑥 ) = dom 𝐼 )
18 fveq2 ( 𝑦 = 𝐵 → ( iEdg ‘ 𝑦 ) = ( iEdg ‘ 𝐵 ) )
19 18 adantl ( ( 𝑥 = 𝐴𝑦 = 𝐵 ) → ( iEdg ‘ 𝑦 ) = ( iEdg ‘ 𝐵 ) )
20 19 4 eqtr4di ( ( 𝑥 = 𝐴𝑦 = 𝐵 ) → ( iEdg ‘ 𝑦 ) = 𝐽 )
21 20 dmeqd ( ( 𝑥 = 𝐴𝑦 = 𝐵 ) → dom ( iEdg ‘ 𝑦 ) = dom 𝐽 )
22 13 17 21 f1oeq123d ( ( 𝑥 = 𝐴𝑦 = 𝐵 ) → ( 𝑔 : dom ( iEdg ‘ 𝑥 ) –1-1-onto→ dom ( iEdg ‘ 𝑦 ) ↔ 𝑔 : dom 𝐼1-1-onto→ dom 𝐽 ) )
23 16 fveq1d ( ( 𝑥 = 𝐴𝑦 = 𝐵 ) → ( ( iEdg ‘ 𝑥 ) ‘ 𝑖 ) = ( 𝐼𝑖 ) )
24 23 imaeq2d ( ( 𝑥 = 𝐴𝑦 = 𝐵 ) → ( 𝑓 “ ( ( iEdg ‘ 𝑥 ) ‘ 𝑖 ) ) = ( 𝑓 “ ( 𝐼𝑖 ) ) )
25 20 fveq1d ( ( 𝑥 = 𝐴𝑦 = 𝐵 ) → ( ( iEdg ‘ 𝑦 ) ‘ ( 𝑔𝑖 ) ) = ( 𝐽 ‘ ( 𝑔𝑖 ) ) )
26 24 25 eqeq12d ( ( 𝑥 = 𝐴𝑦 = 𝐵 ) → ( ( 𝑓 “ ( ( iEdg ‘ 𝑥 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝑦 ) ‘ ( 𝑔𝑖 ) ) ↔ ( 𝑓 “ ( 𝐼𝑖 ) ) = ( 𝐽 ‘ ( 𝑔𝑖 ) ) ) )
27 17 26 raleqbidv ( ( 𝑥 = 𝐴𝑦 = 𝐵 ) → ( ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑥 ) ( 𝑓 “ ( ( iEdg ‘ 𝑥 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝑦 ) ‘ ( 𝑔𝑖 ) ) ↔ ∀ 𝑖 ∈ dom 𝐼 ( 𝑓 “ ( 𝐼𝑖 ) ) = ( 𝐽 ‘ ( 𝑔𝑖 ) ) ) )
28 22 27 anbi12d ( ( 𝑥 = 𝐴𝑦 = 𝐵 ) → ( ( 𝑔 : dom ( iEdg ‘ 𝑥 ) –1-1-onto→ dom ( iEdg ‘ 𝑦 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑥 ) ( 𝑓 “ ( ( iEdg ‘ 𝑥 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝑦 ) ‘ ( 𝑔𝑖 ) ) ) ↔ ( 𝑔 : dom 𝐼1-1-onto→ dom 𝐽 ∧ ∀ 𝑖 ∈ dom 𝐼 ( 𝑓 “ ( 𝐼𝑖 ) ) = ( 𝐽 ‘ ( 𝑔𝑖 ) ) ) ) )
29 28 exbidv ( ( 𝑥 = 𝐴𝑦 = 𝐵 ) → ( ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝑥 ) –1-1-onto→ dom ( iEdg ‘ 𝑦 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑥 ) ( 𝑓 “ ( ( iEdg ‘ 𝑥 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝑦 ) ‘ ( 𝑔𝑖 ) ) ) ↔ ∃ 𝑔 ( 𝑔 : dom 𝐼1-1-onto→ dom 𝐽 ∧ ∀ 𝑖 ∈ dom 𝐼 ( 𝑓 “ ( 𝐼𝑖 ) ) = ( 𝐽 ‘ ( 𝑔𝑖 ) ) ) ) )
30 12 29 anbi12d ( ( 𝑥 = 𝐴𝑦 = 𝐵 ) → ( ( 𝑓 : ( Vtx ‘ 𝑥 ) –1-1-onto→ ( Vtx ‘ 𝑦 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝑥 ) –1-1-onto→ dom ( iEdg ‘ 𝑦 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑥 ) ( 𝑓 “ ( ( iEdg ‘ 𝑥 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝑦 ) ‘ ( 𝑔𝑖 ) ) ) ) ↔ ( 𝑓 : 𝑉1-1-onto𝑊 ∧ ∃ 𝑔 ( 𝑔 : dom 𝐼1-1-onto→ dom 𝐽 ∧ ∀ 𝑖 ∈ dom 𝐼 ( 𝑓 “ ( 𝐼𝑖 ) ) = ( 𝐽 ‘ ( 𝑔𝑖 ) ) ) ) ) )
31 30 exbidv ( ( 𝑥 = 𝐴𝑦 = 𝐵 ) → ( ∃ 𝑓 ( 𝑓 : ( Vtx ‘ 𝑥 ) –1-1-onto→ ( Vtx ‘ 𝑦 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝑥 ) –1-1-onto→ dom ( iEdg ‘ 𝑦 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑥 ) ( 𝑓 “ ( ( iEdg ‘ 𝑥 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝑦 ) ‘ ( 𝑔𝑖 ) ) ) ) ↔ ∃ 𝑓 ( 𝑓 : 𝑉1-1-onto𝑊 ∧ ∃ 𝑔 ( 𝑔 : dom 𝐼1-1-onto→ dom 𝐽 ∧ ∀ 𝑖 ∈ dom 𝐼 ( 𝑓 “ ( 𝐼𝑖 ) ) = ( 𝐽 ‘ ( 𝑔𝑖 ) ) ) ) ) )
32 df-isomgr IsomGr = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑓 ( 𝑓 : ( Vtx ‘ 𝑥 ) –1-1-onto→ ( Vtx ‘ 𝑦 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝑥 ) –1-1-onto→ dom ( iEdg ‘ 𝑦 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑥 ) ( 𝑓 “ ( ( iEdg ‘ 𝑥 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝑦 ) ‘ ( 𝑔𝑖 ) ) ) ) }
33 31 32 brabga ( ( 𝐴𝑋𝐵𝑌 ) → ( 𝐴 IsomGr 𝐵 ↔ ∃ 𝑓 ( 𝑓 : 𝑉1-1-onto𝑊 ∧ ∃ 𝑔 ( 𝑔 : dom 𝐼1-1-onto→ dom 𝐽 ∧ ∀ 𝑖 ∈ dom 𝐼 ( 𝑓 “ ( 𝐼𝑖 ) ) = ( 𝐽 ‘ ( 𝑔𝑖 ) ) ) ) ) )