Metamath Proof Explorer

Theorem isomgreqve

Description: A set is isomorphic to a hypergraph if it has the same vertices and the same edges. (Contributed by AV, 11-Nov-2022)

Ref Expression
Assertion isomgreqve ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌 ) ∧ ( ( Vtx ‘ 𝐴 ) = ( Vtx ‘ 𝐵 ) ∧ ( iEdg ‘ 𝐴 ) = ( iEdg ‘ 𝐵 ) ) ) → 𝐴 IsomGr 𝐵 )

Proof

Step Hyp Ref Expression
1 fvexd ⊢ ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌 ) ∧ ( ( Vtx ‘ 𝐴 ) = ( Vtx ‘ 𝐵 ) ∧ ( iEdg ‘ 𝐴 ) = ( iEdg ‘ 𝐵 ) ) ) → ( Vtx ‘ 𝐵 ) ∈ V )
2 1 resiexd ⊢ ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌 ) ∧ ( ( Vtx ‘ 𝐴 ) = ( Vtx ‘ 𝐵 ) ∧ ( iEdg ‘ 𝐴 ) = ( iEdg ‘ 𝐵 ) ) ) → ( I ↾ ( Vtx ‘ 𝐵 ) ) ∈ V )
3 f1oi ⊢ ( I ↾ ( Vtx ‘ 𝐵 ) ) : ( Vtx ‘ 𝐵 ) –1-1-onto→ ( Vtx ‘ 𝐵 )
4 simprl ⊢ ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌 ) ∧ ( ( Vtx ‘ 𝐴 ) = ( Vtx ‘ 𝐵 ) ∧ ( iEdg ‘ 𝐴 ) = ( iEdg ‘ 𝐵 ) ) ) → ( Vtx ‘ 𝐴 ) = ( Vtx ‘ 𝐵 ) )
5 4 f1oeq2d ⊢ ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌 ) ∧ ( ( Vtx ‘ 𝐴 ) = ( Vtx ‘ 𝐵 ) ∧ ( iEdg ‘ 𝐴 ) = ( iEdg ‘ 𝐵 ) ) ) → ( ( I ↾ ( Vtx ‘ 𝐵 ) ) : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) ↔ ( I ↾ ( Vtx ‘ 𝐵 ) ) : ( Vtx ‘ 𝐵 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) ) )
6 3 5 mpbiri ⊢ ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌 ) ∧ ( ( Vtx ‘ 𝐴 ) = ( Vtx ‘ 𝐵 ) ∧ ( iEdg ‘ 𝐴 ) = ( iEdg ‘ 𝐵 ) ) ) → ( I ↾ ( Vtx ‘ 𝐵 ) ) : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) )
7 fvexd ⊢ ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌 ) ∧ ( ( Vtx ‘ 𝐴 ) = ( Vtx ‘ 𝐵 ) ∧ ( iEdg ‘ 𝐴 ) = ( iEdg ‘ 𝐵 ) ) ) → ( iEdg ‘ 𝐵 ) ∈ V )
8 7 dmexd ⊢ ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌 ) ∧ ( ( Vtx ‘ 𝐴 ) = ( Vtx ‘ 𝐵 ) ∧ ( iEdg ‘ 𝐴 ) = ( iEdg ‘ 𝐵 ) ) ) → dom ( iEdg ‘ 𝐵 ) ∈ V )
9 8 resiexd ⊢ ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌 ) ∧ ( ( Vtx ‘ 𝐴 ) = ( Vtx ‘ 𝐵 ) ∧ ( iEdg ‘ 𝐴 ) = ( iEdg ‘ 𝐵 ) ) ) → ( I ↾ dom ( iEdg ‘ 𝐵 ) ) ∈ V )
10 f1oi ⊢ ( I ↾ dom ( iEdg ‘ 𝐵 ) ) : dom ( iEdg ‘ 𝐵 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 )
11 simprr ⊢ ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌 ) ∧ ( ( Vtx ‘ 𝐴 ) = ( Vtx ‘ 𝐵 ) ∧ ( iEdg ‘ 𝐴 ) = ( iEdg ‘ 𝐵 ) ) ) → ( iEdg ‘ 𝐴 ) = ( iEdg ‘ 𝐵 ) )
12 11 dmeqd ⊢ ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌 ) ∧ ( ( Vtx ‘ 𝐴 ) = ( Vtx ‘ 𝐵 ) ∧ ( iEdg ‘ 𝐴 ) = ( iEdg ‘ 𝐵 ) ) ) → dom ( iEdg ‘ 𝐴 ) = dom ( iEdg ‘ 𝐵 ) )
13 12 f1oeq2d ⊢ ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌 ) ∧ ( ( Vtx ‘ 𝐴 ) = ( Vtx ‘ 𝐵 ) ∧ ( iEdg ‘ 𝐴 ) = ( iEdg ‘ 𝐵 ) ) ) → ( ( I ↾ dom ( iEdg ‘ 𝐵 ) ) : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ↔ ( I ↾ dom ( iEdg ‘ 𝐵 ) ) : dom ( iEdg ‘ 𝐵 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ) )
14 10 13 mpbiri ⊢ ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌 ) ∧ ( ( Vtx ‘ 𝐴 ) = ( Vtx ‘ 𝐵 ) ∧ ( iEdg ‘ 𝐴 ) = ( iEdg ‘ 𝐵 ) ) ) → ( I ↾ dom ( iEdg ‘ 𝐵 ) ) : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) )
15 eqid ⊢ ( Vtx ‘ 𝐴 ) = ( Vtx ‘ 𝐴 )
16 eqid ⊢ ( iEdg ‘ 𝐴 ) = ( iEdg ‘ 𝐴 )
17 15 16 uhgrss ⊢ ( ( 𝐴 ∈ UHGraph ∧ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ) → ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ⊆ ( Vtx ‘ 𝐴 ) )
18 17 ad4ant14 ⊢ ( ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌 ) ∧ ( ( Vtx ‘ 𝐴 ) = ( Vtx ‘ 𝐵 ) ∧ ( iEdg ‘ 𝐴 ) = ( iEdg ‘ 𝐵 ) ) ) ∧ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ) → ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ⊆ ( Vtx ‘ 𝐴 ) )
19 sseq2 ⊢ ( ( Vtx ‘ 𝐴 ) = ( Vtx ‘ 𝐵 ) → ( ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ⊆ ( Vtx ‘ 𝐴 ) ↔ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ⊆ ( Vtx ‘ 𝐵 ) ) )
20 19 adantr ⊢ ( ( ( Vtx ‘ 𝐴 ) = ( Vtx ‘ 𝐵 ) ∧ ( iEdg ‘ 𝐴 ) = ( iEdg ‘ 𝐵 ) ) → ( ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ⊆ ( Vtx ‘ 𝐴 ) ↔ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ⊆ ( Vtx ‘ 𝐵 ) ) )
21 20 adantl ⊢ ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌 ) ∧ ( ( Vtx ‘ 𝐴 ) = ( Vtx ‘ 𝐵 ) ∧ ( iEdg ‘ 𝐴 ) = ( iEdg ‘ 𝐵 ) ) ) → ( ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ⊆ ( Vtx ‘ 𝐴 ) ↔ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ⊆ ( Vtx ‘ 𝐵 ) ) )
22 21 adantr ⊢ ( ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌 ) ∧ ( ( Vtx ‘ 𝐴 ) = ( Vtx ‘ 𝐵 ) ∧ ( iEdg ‘ 𝐴 ) = ( iEdg ‘ 𝐵 ) ) ) ∧ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ) → ( ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ⊆ ( Vtx ‘ 𝐴 ) ↔ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ⊆ ( Vtx ‘ 𝐵 ) ) )
23 18 22 mpbid ⊢ ( ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌 ) ∧ ( ( Vtx ‘ 𝐴 ) = ( Vtx ‘ 𝐵 ) ∧ ( iEdg ‘ 𝐴 ) = ( iEdg ‘ 𝐵 ) ) ) ∧ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ) → ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ⊆ ( Vtx ‘ 𝐵 ) )
24 resiima ⊢ ( ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ⊆ ( Vtx ‘ 𝐵 ) → ( ( I ↾ ( Vtx ‘ 𝐵 ) ) “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) )
25 23 24 syl ⊢ ( ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌 ) ∧ ( ( Vtx ‘ 𝐴 ) = ( Vtx ‘ 𝐵 ) ∧ ( iEdg ‘ 𝐴 ) = ( iEdg ‘ 𝐵 ) ) ) ∧ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ) → ( ( I ↾ ( Vtx ‘ 𝐵 ) ) “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) )
26 fvresi ⊢ ( 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) → ( ( I ↾ dom ( iEdg ‘ 𝐴 ) ) ‘ 𝑖 ) = 𝑖 )
27 26 adantl ⊢ ( ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌 ) ∧ ( ( Vtx ‘ 𝐴 ) = ( Vtx ‘ 𝐵 ) ∧ ( iEdg ‘ 𝐴 ) = ( iEdg ‘ 𝐵 ) ) ) ∧ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ) → ( ( I ↾ dom ( iEdg ‘ 𝐴 ) ) ‘ 𝑖 ) = 𝑖 )
28 27 fveq2d ⊢ ( ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌 ) ∧ ( ( Vtx ‘ 𝐴 ) = ( Vtx ‘ 𝐵 ) ∧ ( iEdg ‘ 𝐴 ) = ( iEdg ‘ 𝐵 ) ) ) ∧ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ) → ( ( iEdg ‘ 𝐴 ) ‘ ( ( I ↾ dom ( iEdg ‘ 𝐴 ) ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) )
29 id ⊢ ( ( iEdg ‘ 𝐴 ) = ( iEdg ‘ 𝐵 ) → ( iEdg ‘ 𝐴 ) = ( iEdg ‘ 𝐵 ) )
30 dmeq ⊢ ( ( iEdg ‘ 𝐴 ) = ( iEdg ‘ 𝐵 ) → dom ( iEdg ‘ 𝐴 ) = dom ( iEdg ‘ 𝐵 ) )
31 30 reseq2d ⊢ ( ( iEdg ‘ 𝐴 ) = ( iEdg ‘ 𝐵 ) → ( I ↾ dom ( iEdg ‘ 𝐴 ) ) = ( I ↾ dom ( iEdg ‘ 𝐵 ) ) )
32 31 fveq1d ⊢ ( ( iEdg ‘ 𝐴 ) = ( iEdg ‘ 𝐵 ) → ( ( I ↾ dom ( iEdg ‘ 𝐴 ) ) ‘ 𝑖 ) = ( ( I ↾ dom ( iEdg ‘ 𝐵 ) ) ‘ 𝑖 ) )
33 29 32 fveq12d ⊢ ( ( iEdg ‘ 𝐴 ) = ( iEdg ‘ 𝐵 ) → ( ( iEdg ‘ 𝐴 ) ‘ ( ( I ↾ dom ( iEdg ‘ 𝐴 ) ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( ( I ↾ dom ( iEdg ‘ 𝐵 ) ) ‘ 𝑖 ) ) )
34 33 adantl ⊢ ( ( ( Vtx ‘ 𝐴 ) = ( Vtx ‘ 𝐵 ) ∧ ( iEdg ‘ 𝐴 ) = ( iEdg ‘ 𝐵 ) ) → ( ( iEdg ‘ 𝐴 ) ‘ ( ( I ↾ dom ( iEdg ‘ 𝐴 ) ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( ( I ↾ dom ( iEdg ‘ 𝐵 ) ) ‘ 𝑖 ) ) )
35 34 adantl ⊢ ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌 ) ∧ ( ( Vtx ‘ 𝐴 ) = ( Vtx ‘ 𝐵 ) ∧ ( iEdg ‘ 𝐴 ) = ( iEdg ‘ 𝐵 ) ) ) → ( ( iEdg ‘ 𝐴 ) ‘ ( ( I ↾ dom ( iEdg ‘ 𝐴 ) ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( ( I ↾ dom ( iEdg ‘ 𝐵 ) ) ‘ 𝑖 ) ) )
36 35 adantr ⊢ ( ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌 ) ∧ ( ( Vtx ‘ 𝐴 ) = ( Vtx ‘ 𝐵 ) ∧ ( iEdg ‘ 𝐴 ) = ( iEdg ‘ 𝐵 ) ) ) ∧ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ) → ( ( iEdg ‘ 𝐴 ) ‘ ( ( I ↾ dom ( iEdg ‘ 𝐴 ) ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( ( I ↾ dom ( iEdg ‘ 𝐵 ) ) ‘ 𝑖 ) ) )
37 25 28 36 3eqtr2d ⊢ ( ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌 ) ∧ ( ( Vtx ‘ 𝐴 ) = ( Vtx ‘ 𝐵 ) ∧ ( iEdg ‘ 𝐴 ) = ( iEdg ‘ 𝐵 ) ) ) ∧ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ) → ( ( I ↾ ( Vtx ‘ 𝐵 ) ) “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( ( I ↾ dom ( iEdg ‘ 𝐵 ) ) ‘ 𝑖 ) ) )
38 37 ralrimiva ⊢ ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌 ) ∧ ( ( Vtx ‘ 𝐴 ) = ( Vtx ‘ 𝐵 ) ∧ ( iEdg ‘ 𝐴 ) = ( iEdg ‘ 𝐵 ) ) ) → ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( ( I ↾ ( Vtx ‘ 𝐵 ) ) “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( ( I ↾ dom ( iEdg ‘ 𝐵 ) ) ‘ 𝑖 ) ) )
39 14 38 jca ⊢ ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌 ) ∧ ( ( Vtx ‘ 𝐴 ) = ( Vtx ‘ 𝐵 ) ∧ ( iEdg ‘ 𝐴 ) = ( iEdg ‘ 𝐵 ) ) ) → ( ( I ↾ dom ( iEdg ‘ 𝐵 ) ) : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( ( I ↾ ( Vtx ‘ 𝐵 ) ) “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( ( I ↾ dom ( iEdg ‘ 𝐵 ) ) ‘ 𝑖 ) ) ) )
40 f1oeq1 ⊢ ( 𝑔 = ( I ↾ dom ( iEdg ‘ 𝐵 ) ) → ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ↔ ( I ↾ dom ( iEdg ‘ 𝐵 ) ) : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ) )
41 fveq1 ⊢ ( 𝑔 = ( I ↾ dom ( iEdg ‘ 𝐵 ) ) → ( 𝑔 ‘ 𝑖 ) = ( ( I ↾ dom ( iEdg ‘ 𝐵 ) ) ‘ 𝑖 ) )
42 41 fveq2d ⊢ ( 𝑔 = ( I ↾ dom ( iEdg ‘ 𝐵 ) ) → ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( ( I ↾ dom ( iEdg ‘ 𝐵 ) ) ‘ 𝑖 ) ) )
43 42 eqeq2d ⊢ ( 𝑔 = ( I ↾ dom ( iEdg ‘ 𝐵 ) ) → ( ( ( I ↾ ( Vtx ‘ 𝐵 ) ) “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔 ‘ 𝑖 ) ) ↔ ( ( I ↾ ( Vtx ‘ 𝐵 ) ) “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( ( I ↾ dom ( iEdg ‘ 𝐵 ) ) ‘ 𝑖 ) ) ) )
44 43 ralbidv ⊢ ( 𝑔 = ( I ↾ dom ( iEdg ‘ 𝐵 ) ) → ( ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( ( I ↾ ( Vtx ‘ 𝐵 ) ) “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔 ‘ 𝑖 ) ) ↔ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( ( I ↾ ( Vtx ‘ 𝐵 ) ) “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( ( I ↾ dom ( iEdg ‘ 𝐵 ) ) ‘ 𝑖 ) ) ) )
45 40 44 anbi12d ⊢ ( 𝑔 = ( I ↾ dom ( iEdg ‘ 𝐵 ) ) → ( ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( ( I ↾ ( Vtx ‘ 𝐵 ) ) “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔 ‘ 𝑖 ) ) ) ↔ ( ( I ↾ dom ( iEdg ‘ 𝐵 ) ) : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( ( I ↾ ( Vtx ‘ 𝐵 ) ) “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( ( I ↾ dom ( iEdg ‘ 𝐵 ) ) ‘ 𝑖 ) ) ) ) )
46 9 39 45 spcedv ⊢ ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌 ) ∧ ( ( Vtx ‘ 𝐴 ) = ( Vtx ‘ 𝐵 ) ∧ ( iEdg ‘ 𝐴 ) = ( iEdg ‘ 𝐵 ) ) ) → ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( ( I ↾ ( Vtx ‘ 𝐵 ) ) “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔 ‘ 𝑖 ) ) ) )
47 6 46 jca ⊢ ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌 ) ∧ ( ( Vtx ‘ 𝐴 ) = ( Vtx ‘ 𝐵 ) ∧ ( iEdg ‘ 𝐴 ) = ( iEdg ‘ 𝐵 ) ) ) → ( ( I ↾ ( Vtx ‘ 𝐵 ) ) : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( ( I ↾ ( Vtx ‘ 𝐵 ) ) “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) )
48 f1oeq1 ⊢ ( 𝑓 = ( I ↾ ( Vtx ‘ 𝐵 ) ) → ( 𝑓 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) ↔ ( I ↾ ( Vtx ‘ 𝐵 ) ) : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) ) )
49 imaeq1 ⊢ ( 𝑓 = ( I ↾ ( Vtx ‘ 𝐵 ) ) → ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( I ↾ ( Vtx ‘ 𝐵 ) ) “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) )
50 49 eqeq1d ⊢ ( 𝑓 = ( I ↾ ( Vtx ‘ 𝐵 ) ) → ( ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔 ‘ 𝑖 ) ) ↔ ( ( I ↾ ( Vtx ‘ 𝐵 ) ) “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔 ‘ 𝑖 ) ) ) )
51 50 ralbidv ⊢ ( 𝑓 = ( I ↾ ( Vtx ‘ 𝐵 ) ) → ( ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔 ‘ 𝑖 ) ) ↔ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( ( I ↾ ( Vtx ‘ 𝐵 ) ) “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔 ‘ 𝑖 ) ) ) )
52 51 anbi2d ⊢ ( 𝑓 = ( I ↾ ( Vtx ‘ 𝐵 ) ) → ( ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔 ‘ 𝑖 ) ) ) ↔ ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( ( I ↾ ( Vtx ‘ 𝐵 ) ) “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) )
53 52 exbidv ⊢ ( 𝑓 = ( I ↾ ( Vtx ‘ 𝐵 ) ) → ( ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔 ‘ 𝑖 ) ) ) ↔ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( ( I ↾ ( Vtx ‘ 𝐵 ) ) “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) )
54 48 53 anbi12d ⊢ ( 𝑓 = ( I ↾ ( Vtx ‘ 𝐵 ) ) → ( ( 𝑓 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) ↔ ( ( I ↾ ( Vtx ‘ 𝐵 ) ) : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( ( I ↾ ( Vtx ‘ 𝐵 ) ) “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) ) )
55 2 47 54 spcedv ⊢ ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌 ) ∧ ( ( Vtx ‘ 𝐴 ) = ( Vtx ‘ 𝐵 ) ∧ ( iEdg ‘ 𝐴 ) = ( iEdg ‘ 𝐵 ) ) ) → ∃ 𝑓 ( 𝑓 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) )
56 eqid ⊢ ( Vtx ‘ 𝐵 ) = ( Vtx ‘ 𝐵 )
57 eqid ⊢ ( iEdg ‘ 𝐵 ) = ( iEdg ‘ 𝐵 )
58 15 56 16 57 isomgr ⊢ ( ( 𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌 ) → ( 𝐴 IsomGr 𝐵 ↔ ∃ 𝑓 ( 𝑓 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) ) )
59 58 adantr ⊢ ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌 ) ∧ ( ( Vtx ‘ 𝐴 ) = ( Vtx ‘ 𝐵 ) ∧ ( iEdg ‘ 𝐴 ) = ( iEdg ‘ 𝐵 ) ) ) → ( 𝐴 IsomGr 𝐵 ↔ ∃ 𝑓 ( 𝑓 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) ) )
60 55 59 mpbird ⊢ ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵 ∈ 𝑌 ) ∧ ( ( Vtx ‘ 𝐴 ) = ( Vtx ‘ 𝐵 ) ∧ ( iEdg ‘ 𝐴 ) = ( iEdg ‘ 𝐵 ) ) ) → 𝐴 IsomGr 𝐵 )