# 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 ${⊢}\left(\left({A}\in \mathrm{UHGraph}\wedge {B}\in {Y}\right)\wedge \left(\mathrm{Vtx}\left({A}\right)=\mathrm{Vtx}\left({B}\right)\wedge \mathrm{iEdg}\left({A}\right)=\mathrm{iEdg}\left({B}\right)\right)\right)\to {A}\mathrm{IsomGr}{B}$

### Proof

Step Hyp Ref Expression
1 fvexd ${⊢}\left(\left({A}\in \mathrm{UHGraph}\wedge {B}\in {Y}\right)\wedge \left(\mathrm{Vtx}\left({A}\right)=\mathrm{Vtx}\left({B}\right)\wedge \mathrm{iEdg}\left({A}\right)=\mathrm{iEdg}\left({B}\right)\right)\right)\to \mathrm{Vtx}\left({B}\right)\in \mathrm{V}$
2 1 resiexd ${⊢}\left(\left({A}\in \mathrm{UHGraph}\wedge {B}\in {Y}\right)\wedge \left(\mathrm{Vtx}\left({A}\right)=\mathrm{Vtx}\left({B}\right)\wedge \mathrm{iEdg}\left({A}\right)=\mathrm{iEdg}\left({B}\right)\right)\right)\to {\mathrm{I}↾}_{\mathrm{Vtx}\left({B}\right)}\in \mathrm{V}$
3 f1oi ${⊢}\left({\mathrm{I}↾}_{\mathrm{Vtx}\left({B}\right)}\right):\mathrm{Vtx}\left({B}\right)\underset{1-1 onto}{⟶}\mathrm{Vtx}\left({B}\right)$
4 simprl ${⊢}\left(\left({A}\in \mathrm{UHGraph}\wedge {B}\in {Y}\right)\wedge \left(\mathrm{Vtx}\left({A}\right)=\mathrm{Vtx}\left({B}\right)\wedge \mathrm{iEdg}\left({A}\right)=\mathrm{iEdg}\left({B}\right)\right)\right)\to \mathrm{Vtx}\left({A}\right)=\mathrm{Vtx}\left({B}\right)$
5 4 f1oeq2d ${⊢}\left(\left({A}\in \mathrm{UHGraph}\wedge {B}\in {Y}\right)\wedge \left(\mathrm{Vtx}\left({A}\right)=\mathrm{Vtx}\left({B}\right)\wedge \mathrm{iEdg}\left({A}\right)=\mathrm{iEdg}\left({B}\right)\right)\right)\to \left(\left({\mathrm{I}↾}_{\mathrm{Vtx}\left({B}\right)}\right):\mathrm{Vtx}\left({A}\right)\underset{1-1 onto}{⟶}\mathrm{Vtx}\left({B}\right)↔\left({\mathrm{I}↾}_{\mathrm{Vtx}\left({B}\right)}\right):\mathrm{Vtx}\left({B}\right)\underset{1-1 onto}{⟶}\mathrm{Vtx}\left({B}\right)\right)$
6 3 5 mpbiri ${⊢}\left(\left({A}\in \mathrm{UHGraph}\wedge {B}\in {Y}\right)\wedge \left(\mathrm{Vtx}\left({A}\right)=\mathrm{Vtx}\left({B}\right)\wedge \mathrm{iEdg}\left({A}\right)=\mathrm{iEdg}\left({B}\right)\right)\right)\to \left({\mathrm{I}↾}_{\mathrm{Vtx}\left({B}\right)}\right):\mathrm{Vtx}\left({A}\right)\underset{1-1 onto}{⟶}\mathrm{Vtx}\left({B}\right)$
7 fvexd ${⊢}\left(\left({A}\in \mathrm{UHGraph}\wedge {B}\in {Y}\right)\wedge \left(\mathrm{Vtx}\left({A}\right)=\mathrm{Vtx}\left({B}\right)\wedge \mathrm{iEdg}\left({A}\right)=\mathrm{iEdg}\left({B}\right)\right)\right)\to \mathrm{iEdg}\left({B}\right)\in \mathrm{V}$
8 7 dmexd ${⊢}\left(\left({A}\in \mathrm{UHGraph}\wedge {B}\in {Y}\right)\wedge \left(\mathrm{Vtx}\left({A}\right)=\mathrm{Vtx}\left({B}\right)\wedge \mathrm{iEdg}\left({A}\right)=\mathrm{iEdg}\left({B}\right)\right)\right)\to \mathrm{dom}\mathrm{iEdg}\left({B}\right)\in \mathrm{V}$
9 8 resiexd ${⊢}\left(\left({A}\in \mathrm{UHGraph}\wedge {B}\in {Y}\right)\wedge \left(\mathrm{Vtx}\left({A}\right)=\mathrm{Vtx}\left({B}\right)\wedge \mathrm{iEdg}\left({A}\right)=\mathrm{iEdg}\left({B}\right)\right)\right)\to {\mathrm{I}↾}_{\mathrm{dom}\mathrm{iEdg}\left({B}\right)}\in \mathrm{V}$
10 f1oi ${⊢}\left({\mathrm{I}↾}_{\mathrm{dom}\mathrm{iEdg}\left({B}\right)}\right):\mathrm{dom}\mathrm{iEdg}\left({B}\right)\underset{1-1 onto}{⟶}\mathrm{dom}\mathrm{iEdg}\left({B}\right)$
11 simprr ${⊢}\left(\left({A}\in \mathrm{UHGraph}\wedge {B}\in {Y}\right)\wedge \left(\mathrm{Vtx}\left({A}\right)=\mathrm{Vtx}\left({B}\right)\wedge \mathrm{iEdg}\left({A}\right)=\mathrm{iEdg}\left({B}\right)\right)\right)\to \mathrm{iEdg}\left({A}\right)=\mathrm{iEdg}\left({B}\right)$
12 11 dmeqd ${⊢}\left(\left({A}\in \mathrm{UHGraph}\wedge {B}\in {Y}\right)\wedge \left(\mathrm{Vtx}\left({A}\right)=\mathrm{Vtx}\left({B}\right)\wedge \mathrm{iEdg}\left({A}\right)=\mathrm{iEdg}\left({B}\right)\right)\right)\to \mathrm{dom}\mathrm{iEdg}\left({A}\right)=\mathrm{dom}\mathrm{iEdg}\left({B}\right)$
13 12 f1oeq2d ${⊢}\left(\left({A}\in \mathrm{UHGraph}\wedge {B}\in {Y}\right)\wedge \left(\mathrm{Vtx}\left({A}\right)=\mathrm{Vtx}\left({B}\right)\wedge \mathrm{iEdg}\left({A}\right)=\mathrm{iEdg}\left({B}\right)\right)\right)\to \left(\left({\mathrm{I}↾}_{\mathrm{dom}\mathrm{iEdg}\left({B}\right)}\right):\mathrm{dom}\mathrm{iEdg}\left({A}\right)\underset{1-1 onto}{⟶}\mathrm{dom}\mathrm{iEdg}\left({B}\right)↔\left({\mathrm{I}↾}_{\mathrm{dom}\mathrm{iEdg}\left({B}\right)}\right):\mathrm{dom}\mathrm{iEdg}\left({B}\right)\underset{1-1 onto}{⟶}\mathrm{dom}\mathrm{iEdg}\left({B}\right)\right)$
14 10 13 mpbiri ${⊢}\left(\left({A}\in \mathrm{UHGraph}\wedge {B}\in {Y}\right)\wedge \left(\mathrm{Vtx}\left({A}\right)=\mathrm{Vtx}\left({B}\right)\wedge \mathrm{iEdg}\left({A}\right)=\mathrm{iEdg}\left({B}\right)\right)\right)\to \left({\mathrm{I}↾}_{\mathrm{dom}\mathrm{iEdg}\left({B}\right)}\right):\mathrm{dom}\mathrm{iEdg}\left({A}\right)\underset{1-1 onto}{⟶}\mathrm{dom}\mathrm{iEdg}\left({B}\right)$
15 eqid ${⊢}\mathrm{Vtx}\left({A}\right)=\mathrm{Vtx}\left({A}\right)$
16 eqid ${⊢}\mathrm{iEdg}\left({A}\right)=\mathrm{iEdg}\left({A}\right)$
17 15 16 uhgrss ${⊢}\left({A}\in \mathrm{UHGraph}\wedge {i}\in \mathrm{dom}\mathrm{iEdg}\left({A}\right)\right)\to \mathrm{iEdg}\left({A}\right)\left({i}\right)\subseteq \mathrm{Vtx}\left({A}\right)$
18 17 ad4ant14 ${⊢}\left(\left(\left({A}\in \mathrm{UHGraph}\wedge {B}\in {Y}\right)\wedge \left(\mathrm{Vtx}\left({A}\right)=\mathrm{Vtx}\left({B}\right)\wedge \mathrm{iEdg}\left({A}\right)=\mathrm{iEdg}\left({B}\right)\right)\right)\wedge {i}\in \mathrm{dom}\mathrm{iEdg}\left({A}\right)\right)\to \mathrm{iEdg}\left({A}\right)\left({i}\right)\subseteq \mathrm{Vtx}\left({A}\right)$
19 sseq2 ${⊢}\mathrm{Vtx}\left({A}\right)=\mathrm{Vtx}\left({B}\right)\to \left(\mathrm{iEdg}\left({A}\right)\left({i}\right)\subseteq \mathrm{Vtx}\left({A}\right)↔\mathrm{iEdg}\left({A}\right)\left({i}\right)\subseteq \mathrm{Vtx}\left({B}\right)\right)$
20 19 adantr ${⊢}\left(\mathrm{Vtx}\left({A}\right)=\mathrm{Vtx}\left({B}\right)\wedge \mathrm{iEdg}\left({A}\right)=\mathrm{iEdg}\left({B}\right)\right)\to \left(\mathrm{iEdg}\left({A}\right)\left({i}\right)\subseteq \mathrm{Vtx}\left({A}\right)↔\mathrm{iEdg}\left({A}\right)\left({i}\right)\subseteq \mathrm{Vtx}\left({B}\right)\right)$
21 20 adantl ${⊢}\left(\left({A}\in \mathrm{UHGraph}\wedge {B}\in {Y}\right)\wedge \left(\mathrm{Vtx}\left({A}\right)=\mathrm{Vtx}\left({B}\right)\wedge \mathrm{iEdg}\left({A}\right)=\mathrm{iEdg}\left({B}\right)\right)\right)\to \left(\mathrm{iEdg}\left({A}\right)\left({i}\right)\subseteq \mathrm{Vtx}\left({A}\right)↔\mathrm{iEdg}\left({A}\right)\left({i}\right)\subseteq \mathrm{Vtx}\left({B}\right)\right)$
22 21 adantr ${⊢}\left(\left(\left({A}\in \mathrm{UHGraph}\wedge {B}\in {Y}\right)\wedge \left(\mathrm{Vtx}\left({A}\right)=\mathrm{Vtx}\left({B}\right)\wedge \mathrm{iEdg}\left({A}\right)=\mathrm{iEdg}\left({B}\right)\right)\right)\wedge {i}\in \mathrm{dom}\mathrm{iEdg}\left({A}\right)\right)\to \left(\mathrm{iEdg}\left({A}\right)\left({i}\right)\subseteq \mathrm{Vtx}\left({A}\right)↔\mathrm{iEdg}\left({A}\right)\left({i}\right)\subseteq \mathrm{Vtx}\left({B}\right)\right)$
23 18 22 mpbid ${⊢}\left(\left(\left({A}\in \mathrm{UHGraph}\wedge {B}\in {Y}\right)\wedge \left(\mathrm{Vtx}\left({A}\right)=\mathrm{Vtx}\left({B}\right)\wedge \mathrm{iEdg}\left({A}\right)=\mathrm{iEdg}\left({B}\right)\right)\right)\wedge {i}\in \mathrm{dom}\mathrm{iEdg}\left({A}\right)\right)\to \mathrm{iEdg}\left({A}\right)\left({i}\right)\subseteq \mathrm{Vtx}\left({B}\right)$
24 resiima ${⊢}\mathrm{iEdg}\left({A}\right)\left({i}\right)\subseteq \mathrm{Vtx}\left({B}\right)\to \left({\mathrm{I}↾}_{\mathrm{Vtx}\left({B}\right)}\right)\left[\mathrm{iEdg}\left({A}\right)\left({i}\right)\right]=\mathrm{iEdg}\left({A}\right)\left({i}\right)$
25 23 24 syl ${⊢}\left(\left(\left({A}\in \mathrm{UHGraph}\wedge {B}\in {Y}\right)\wedge \left(\mathrm{Vtx}\left({A}\right)=\mathrm{Vtx}\left({B}\right)\wedge \mathrm{iEdg}\left({A}\right)=\mathrm{iEdg}\left({B}\right)\right)\right)\wedge {i}\in \mathrm{dom}\mathrm{iEdg}\left({A}\right)\right)\to \left({\mathrm{I}↾}_{\mathrm{Vtx}\left({B}\right)}\right)\left[\mathrm{iEdg}\left({A}\right)\left({i}\right)\right]=\mathrm{iEdg}\left({A}\right)\left({i}\right)$
26 fvresi ${⊢}{i}\in \mathrm{dom}\mathrm{iEdg}\left({A}\right)\to \left({\mathrm{I}↾}_{\mathrm{dom}\mathrm{iEdg}\left({A}\right)}\right)\left({i}\right)={i}$
27 26 adantl ${⊢}\left(\left(\left({A}\in \mathrm{UHGraph}\wedge {B}\in {Y}\right)\wedge \left(\mathrm{Vtx}\left({A}\right)=\mathrm{Vtx}\left({B}\right)\wedge \mathrm{iEdg}\left({A}\right)=\mathrm{iEdg}\left({B}\right)\right)\right)\wedge {i}\in \mathrm{dom}\mathrm{iEdg}\left({A}\right)\right)\to \left({\mathrm{I}↾}_{\mathrm{dom}\mathrm{iEdg}\left({A}\right)}\right)\left({i}\right)={i}$
28 27 fveq2d ${⊢}\left(\left(\left({A}\in \mathrm{UHGraph}\wedge {B}\in {Y}\right)\wedge \left(\mathrm{Vtx}\left({A}\right)=\mathrm{Vtx}\left({B}\right)\wedge \mathrm{iEdg}\left({A}\right)=\mathrm{iEdg}\left({B}\right)\right)\right)\wedge {i}\in \mathrm{dom}\mathrm{iEdg}\left({A}\right)\right)\to \mathrm{iEdg}\left({A}\right)\left(\left({\mathrm{I}↾}_{\mathrm{dom}\mathrm{iEdg}\left({A}\right)}\right)\left({i}\right)\right)=\mathrm{iEdg}\left({A}\right)\left({i}\right)$
29 id ${⊢}\mathrm{iEdg}\left({A}\right)=\mathrm{iEdg}\left({B}\right)\to \mathrm{iEdg}\left({A}\right)=\mathrm{iEdg}\left({B}\right)$
30 dmeq ${⊢}\mathrm{iEdg}\left({A}\right)=\mathrm{iEdg}\left({B}\right)\to \mathrm{dom}\mathrm{iEdg}\left({A}\right)=\mathrm{dom}\mathrm{iEdg}\left({B}\right)$
31 30 reseq2d ${⊢}\mathrm{iEdg}\left({A}\right)=\mathrm{iEdg}\left({B}\right)\to {\mathrm{I}↾}_{\mathrm{dom}\mathrm{iEdg}\left({A}\right)}={\mathrm{I}↾}_{\mathrm{dom}\mathrm{iEdg}\left({B}\right)}$
32 31 fveq1d ${⊢}\mathrm{iEdg}\left({A}\right)=\mathrm{iEdg}\left({B}\right)\to \left({\mathrm{I}↾}_{\mathrm{dom}\mathrm{iEdg}\left({A}\right)}\right)\left({i}\right)=\left({\mathrm{I}↾}_{\mathrm{dom}\mathrm{iEdg}\left({B}\right)}\right)\left({i}\right)$
33 29 32 fveq12d ${⊢}\mathrm{iEdg}\left({A}\right)=\mathrm{iEdg}\left({B}\right)\to \mathrm{iEdg}\left({A}\right)\left(\left({\mathrm{I}↾}_{\mathrm{dom}\mathrm{iEdg}\left({A}\right)}\right)\left({i}\right)\right)=\mathrm{iEdg}\left({B}\right)\left(\left({\mathrm{I}↾}_{\mathrm{dom}\mathrm{iEdg}\left({B}\right)}\right)\left({i}\right)\right)$
34 33 adantl ${⊢}\left(\mathrm{Vtx}\left({A}\right)=\mathrm{Vtx}\left({B}\right)\wedge \mathrm{iEdg}\left({A}\right)=\mathrm{iEdg}\left({B}\right)\right)\to \mathrm{iEdg}\left({A}\right)\left(\left({\mathrm{I}↾}_{\mathrm{dom}\mathrm{iEdg}\left({A}\right)}\right)\left({i}\right)\right)=\mathrm{iEdg}\left({B}\right)\left(\left({\mathrm{I}↾}_{\mathrm{dom}\mathrm{iEdg}\left({B}\right)}\right)\left({i}\right)\right)$
35 34 adantl ${⊢}\left(\left({A}\in \mathrm{UHGraph}\wedge {B}\in {Y}\right)\wedge \left(\mathrm{Vtx}\left({A}\right)=\mathrm{Vtx}\left({B}\right)\wedge \mathrm{iEdg}\left({A}\right)=\mathrm{iEdg}\left({B}\right)\right)\right)\to \mathrm{iEdg}\left({A}\right)\left(\left({\mathrm{I}↾}_{\mathrm{dom}\mathrm{iEdg}\left({A}\right)}\right)\left({i}\right)\right)=\mathrm{iEdg}\left({B}\right)\left(\left({\mathrm{I}↾}_{\mathrm{dom}\mathrm{iEdg}\left({B}\right)}\right)\left({i}\right)\right)$
36 35 adantr ${⊢}\left(\left(\left({A}\in \mathrm{UHGraph}\wedge {B}\in {Y}\right)\wedge \left(\mathrm{Vtx}\left({A}\right)=\mathrm{Vtx}\left({B}\right)\wedge \mathrm{iEdg}\left({A}\right)=\mathrm{iEdg}\left({B}\right)\right)\right)\wedge {i}\in \mathrm{dom}\mathrm{iEdg}\left({A}\right)\right)\to \mathrm{iEdg}\left({A}\right)\left(\left({\mathrm{I}↾}_{\mathrm{dom}\mathrm{iEdg}\left({A}\right)}\right)\left({i}\right)\right)=\mathrm{iEdg}\left({B}\right)\left(\left({\mathrm{I}↾}_{\mathrm{dom}\mathrm{iEdg}\left({B}\right)}\right)\left({i}\right)\right)$
37 25 28 36 3eqtr2d ${⊢}\left(\left(\left({A}\in \mathrm{UHGraph}\wedge {B}\in {Y}\right)\wedge \left(\mathrm{Vtx}\left({A}\right)=\mathrm{Vtx}\left({B}\right)\wedge \mathrm{iEdg}\left({A}\right)=\mathrm{iEdg}\left({B}\right)\right)\right)\wedge {i}\in \mathrm{dom}\mathrm{iEdg}\left({A}\right)\right)\to \left({\mathrm{I}↾}_{\mathrm{Vtx}\left({B}\right)}\right)\left[\mathrm{iEdg}\left({A}\right)\left({i}\right)\right]=\mathrm{iEdg}\left({B}\right)\left(\left({\mathrm{I}↾}_{\mathrm{dom}\mathrm{iEdg}\left({B}\right)}\right)\left({i}\right)\right)$
38 37 ralrimiva ${⊢}\left(\left({A}\in \mathrm{UHGraph}\wedge {B}\in {Y}\right)\wedge \left(\mathrm{Vtx}\left({A}\right)=\mathrm{Vtx}\left({B}\right)\wedge \mathrm{iEdg}\left({A}\right)=\mathrm{iEdg}\left({B}\right)\right)\right)\to \forall {i}\in \mathrm{dom}\mathrm{iEdg}\left({A}\right)\phantom{\rule{.4em}{0ex}}\left({\mathrm{I}↾}_{\mathrm{Vtx}\left({B}\right)}\right)\left[\mathrm{iEdg}\left({A}\right)\left({i}\right)\right]=\mathrm{iEdg}\left({B}\right)\left(\left({\mathrm{I}↾}_{\mathrm{dom}\mathrm{iEdg}\left({B}\right)}\right)\left({i}\right)\right)$
39 14 38 jca ${⊢}\left(\left({A}\in \mathrm{UHGraph}\wedge {B}\in {Y}\right)\wedge \left(\mathrm{Vtx}\left({A}\right)=\mathrm{Vtx}\left({B}\right)\wedge \mathrm{iEdg}\left({A}\right)=\mathrm{iEdg}\left({B}\right)\right)\right)\to \left(\left({\mathrm{I}↾}_{\mathrm{dom}\mathrm{iEdg}\left({B}\right)}\right):\mathrm{dom}\mathrm{iEdg}\left({A}\right)\underset{1-1 onto}{⟶}\mathrm{dom}\mathrm{iEdg}\left({B}\right)\wedge \forall {i}\in \mathrm{dom}\mathrm{iEdg}\left({A}\right)\phantom{\rule{.4em}{0ex}}\left({\mathrm{I}↾}_{\mathrm{Vtx}\left({B}\right)}\right)\left[\mathrm{iEdg}\left({A}\right)\left({i}\right)\right]=\mathrm{iEdg}\left({B}\right)\left(\left({\mathrm{I}↾}_{\mathrm{dom}\mathrm{iEdg}\left({B}\right)}\right)\left({i}\right)\right)\right)$
40 f1oeq1 ${⊢}{g}={\mathrm{I}↾}_{\mathrm{dom}\mathrm{iEdg}\left({B}\right)}\to \left({g}:\mathrm{dom}\mathrm{iEdg}\left({A}\right)\underset{1-1 onto}{⟶}\mathrm{dom}\mathrm{iEdg}\left({B}\right)↔\left({\mathrm{I}↾}_{\mathrm{dom}\mathrm{iEdg}\left({B}\right)}\right):\mathrm{dom}\mathrm{iEdg}\left({A}\right)\underset{1-1 onto}{⟶}\mathrm{dom}\mathrm{iEdg}\left({B}\right)\right)$
41 fveq1 ${⊢}{g}={\mathrm{I}↾}_{\mathrm{dom}\mathrm{iEdg}\left({B}\right)}\to {g}\left({i}\right)=\left({\mathrm{I}↾}_{\mathrm{dom}\mathrm{iEdg}\left({B}\right)}\right)\left({i}\right)$
42 41 fveq2d ${⊢}{g}={\mathrm{I}↾}_{\mathrm{dom}\mathrm{iEdg}\left({B}\right)}\to \mathrm{iEdg}\left({B}\right)\left({g}\left({i}\right)\right)=\mathrm{iEdg}\left({B}\right)\left(\left({\mathrm{I}↾}_{\mathrm{dom}\mathrm{iEdg}\left({B}\right)}\right)\left({i}\right)\right)$
43 42 eqeq2d ${⊢}{g}={\mathrm{I}↾}_{\mathrm{dom}\mathrm{iEdg}\left({B}\right)}\to \left(\left({\mathrm{I}↾}_{\mathrm{Vtx}\left({B}\right)}\right)\left[\mathrm{iEdg}\left({A}\right)\left({i}\right)\right]=\mathrm{iEdg}\left({B}\right)\left({g}\left({i}\right)\right)↔\left({\mathrm{I}↾}_{\mathrm{Vtx}\left({B}\right)}\right)\left[\mathrm{iEdg}\left({A}\right)\left({i}\right)\right]=\mathrm{iEdg}\left({B}\right)\left(\left({\mathrm{I}↾}_{\mathrm{dom}\mathrm{iEdg}\left({B}\right)}\right)\left({i}\right)\right)\right)$
44 43 ralbidv ${⊢}{g}={\mathrm{I}↾}_{\mathrm{dom}\mathrm{iEdg}\left({B}\right)}\to \left(\forall {i}\in \mathrm{dom}\mathrm{iEdg}\left({A}\right)\phantom{\rule{.4em}{0ex}}\left({\mathrm{I}↾}_{\mathrm{Vtx}\left({B}\right)}\right)\left[\mathrm{iEdg}\left({A}\right)\left({i}\right)\right]=\mathrm{iEdg}\left({B}\right)\left({g}\left({i}\right)\right)↔\forall {i}\in \mathrm{dom}\mathrm{iEdg}\left({A}\right)\phantom{\rule{.4em}{0ex}}\left({\mathrm{I}↾}_{\mathrm{Vtx}\left({B}\right)}\right)\left[\mathrm{iEdg}\left({A}\right)\left({i}\right)\right]=\mathrm{iEdg}\left({B}\right)\left(\left({\mathrm{I}↾}_{\mathrm{dom}\mathrm{iEdg}\left({B}\right)}\right)\left({i}\right)\right)\right)$
45 40 44 anbi12d ${⊢}{g}={\mathrm{I}↾}_{\mathrm{dom}\mathrm{iEdg}\left({B}\right)}\to \left(\left({g}:\mathrm{dom}\mathrm{iEdg}\left({A}\right)\underset{1-1 onto}{⟶}\mathrm{dom}\mathrm{iEdg}\left({B}\right)\wedge \forall {i}\in \mathrm{dom}\mathrm{iEdg}\left({A}\right)\phantom{\rule{.4em}{0ex}}\left({\mathrm{I}↾}_{\mathrm{Vtx}\left({B}\right)}\right)\left[\mathrm{iEdg}\left({A}\right)\left({i}\right)\right]=\mathrm{iEdg}\left({B}\right)\left({g}\left({i}\right)\right)\right)↔\left(\left({\mathrm{I}↾}_{\mathrm{dom}\mathrm{iEdg}\left({B}\right)}\right):\mathrm{dom}\mathrm{iEdg}\left({A}\right)\underset{1-1 onto}{⟶}\mathrm{dom}\mathrm{iEdg}\left({B}\right)\wedge \forall {i}\in \mathrm{dom}\mathrm{iEdg}\left({A}\right)\phantom{\rule{.4em}{0ex}}\left({\mathrm{I}↾}_{\mathrm{Vtx}\left({B}\right)}\right)\left[\mathrm{iEdg}\left({A}\right)\left({i}\right)\right]=\mathrm{iEdg}\left({B}\right)\left(\left({\mathrm{I}↾}_{\mathrm{dom}\mathrm{iEdg}\left({B}\right)}\right)\left({i}\right)\right)\right)\right)$
46 9 39 45 spcedv ${⊢}\left(\left({A}\in \mathrm{UHGraph}\wedge {B}\in {Y}\right)\wedge \left(\mathrm{Vtx}\left({A}\right)=\mathrm{Vtx}\left({B}\right)\wedge \mathrm{iEdg}\left({A}\right)=\mathrm{iEdg}\left({B}\right)\right)\right)\to \exists {g}\phantom{\rule{.4em}{0ex}}\left({g}:\mathrm{dom}\mathrm{iEdg}\left({A}\right)\underset{1-1 onto}{⟶}\mathrm{dom}\mathrm{iEdg}\left({B}\right)\wedge \forall {i}\in \mathrm{dom}\mathrm{iEdg}\left({A}\right)\phantom{\rule{.4em}{0ex}}\left({\mathrm{I}↾}_{\mathrm{Vtx}\left({B}\right)}\right)\left[\mathrm{iEdg}\left({A}\right)\left({i}\right)\right]=\mathrm{iEdg}\left({B}\right)\left({g}\left({i}\right)\right)\right)$
47 6 46 jca ${⊢}\left(\left({A}\in \mathrm{UHGraph}\wedge {B}\in {Y}\right)\wedge \left(\mathrm{Vtx}\left({A}\right)=\mathrm{Vtx}\left({B}\right)\wedge \mathrm{iEdg}\left({A}\right)=\mathrm{iEdg}\left({B}\right)\right)\right)\to \left(\left({\mathrm{I}↾}_{\mathrm{Vtx}\left({B}\right)}\right):\mathrm{Vtx}\left({A}\right)\underset{1-1 onto}{⟶}\mathrm{Vtx}\left({B}\right)\wedge \exists {g}\phantom{\rule{.4em}{0ex}}\left({g}:\mathrm{dom}\mathrm{iEdg}\left({A}\right)\underset{1-1 onto}{⟶}\mathrm{dom}\mathrm{iEdg}\left({B}\right)\wedge \forall {i}\in \mathrm{dom}\mathrm{iEdg}\left({A}\right)\phantom{\rule{.4em}{0ex}}\left({\mathrm{I}↾}_{\mathrm{Vtx}\left({B}\right)}\right)\left[\mathrm{iEdg}\left({A}\right)\left({i}\right)\right]=\mathrm{iEdg}\left({B}\right)\left({g}\left({i}\right)\right)\right)\right)$
48 f1oeq1 ${⊢}{f}={\mathrm{I}↾}_{\mathrm{Vtx}\left({B}\right)}\to \left({f}:\mathrm{Vtx}\left({A}\right)\underset{1-1 onto}{⟶}\mathrm{Vtx}\left({B}\right)↔\left({\mathrm{I}↾}_{\mathrm{Vtx}\left({B}\right)}\right):\mathrm{Vtx}\left({A}\right)\underset{1-1 onto}{⟶}\mathrm{Vtx}\left({B}\right)\right)$
49 imaeq1 ${⊢}{f}={\mathrm{I}↾}_{\mathrm{Vtx}\left({B}\right)}\to {f}\left[\mathrm{iEdg}\left({A}\right)\left({i}\right)\right]=\left({\mathrm{I}↾}_{\mathrm{Vtx}\left({B}\right)}\right)\left[\mathrm{iEdg}\left({A}\right)\left({i}\right)\right]$
50 49 eqeq1d ${⊢}{f}={\mathrm{I}↾}_{\mathrm{Vtx}\left({B}\right)}\to \left({f}\left[\mathrm{iEdg}\left({A}\right)\left({i}\right)\right]=\mathrm{iEdg}\left({B}\right)\left({g}\left({i}\right)\right)↔\left({\mathrm{I}↾}_{\mathrm{Vtx}\left({B}\right)}\right)\left[\mathrm{iEdg}\left({A}\right)\left({i}\right)\right]=\mathrm{iEdg}\left({B}\right)\left({g}\left({i}\right)\right)\right)$
51 50 ralbidv ${⊢}{f}={\mathrm{I}↾}_{\mathrm{Vtx}\left({B}\right)}\to \left(\forall {i}\in \mathrm{dom}\mathrm{iEdg}\left({A}\right)\phantom{\rule{.4em}{0ex}}{f}\left[\mathrm{iEdg}\left({A}\right)\left({i}\right)\right]=\mathrm{iEdg}\left({B}\right)\left({g}\left({i}\right)\right)↔\forall {i}\in \mathrm{dom}\mathrm{iEdg}\left({A}\right)\phantom{\rule{.4em}{0ex}}\left({\mathrm{I}↾}_{\mathrm{Vtx}\left({B}\right)}\right)\left[\mathrm{iEdg}\left({A}\right)\left({i}\right)\right]=\mathrm{iEdg}\left({B}\right)\left({g}\left({i}\right)\right)\right)$
52 51 anbi2d ${⊢}{f}={\mathrm{I}↾}_{\mathrm{Vtx}\left({B}\right)}\to \left(\left({g}:\mathrm{dom}\mathrm{iEdg}\left({A}\right)\underset{1-1 onto}{⟶}\mathrm{dom}\mathrm{iEdg}\left({B}\right)\wedge \forall {i}\in \mathrm{dom}\mathrm{iEdg}\left({A}\right)\phantom{\rule{.4em}{0ex}}{f}\left[\mathrm{iEdg}\left({A}\right)\left({i}\right)\right]=\mathrm{iEdg}\left({B}\right)\left({g}\left({i}\right)\right)\right)↔\left({g}:\mathrm{dom}\mathrm{iEdg}\left({A}\right)\underset{1-1 onto}{⟶}\mathrm{dom}\mathrm{iEdg}\left({B}\right)\wedge \forall {i}\in \mathrm{dom}\mathrm{iEdg}\left({A}\right)\phantom{\rule{.4em}{0ex}}\left({\mathrm{I}↾}_{\mathrm{Vtx}\left({B}\right)}\right)\left[\mathrm{iEdg}\left({A}\right)\left({i}\right)\right]=\mathrm{iEdg}\left({B}\right)\left({g}\left({i}\right)\right)\right)\right)$
53 52 exbidv ${⊢}{f}={\mathrm{I}↾}_{\mathrm{Vtx}\left({B}\right)}\to \left(\exists {g}\phantom{\rule{.4em}{0ex}}\left({g}:\mathrm{dom}\mathrm{iEdg}\left({A}\right)\underset{1-1 onto}{⟶}\mathrm{dom}\mathrm{iEdg}\left({B}\right)\wedge \forall {i}\in \mathrm{dom}\mathrm{iEdg}\left({A}\right)\phantom{\rule{.4em}{0ex}}{f}\left[\mathrm{iEdg}\left({A}\right)\left({i}\right)\right]=\mathrm{iEdg}\left({B}\right)\left({g}\left({i}\right)\right)\right)↔\exists {g}\phantom{\rule{.4em}{0ex}}\left({g}:\mathrm{dom}\mathrm{iEdg}\left({A}\right)\underset{1-1 onto}{⟶}\mathrm{dom}\mathrm{iEdg}\left({B}\right)\wedge \forall {i}\in \mathrm{dom}\mathrm{iEdg}\left({A}\right)\phantom{\rule{.4em}{0ex}}\left({\mathrm{I}↾}_{\mathrm{Vtx}\left({B}\right)}\right)\left[\mathrm{iEdg}\left({A}\right)\left({i}\right)\right]=\mathrm{iEdg}\left({B}\right)\left({g}\left({i}\right)\right)\right)\right)$
54 48 53 anbi12d ${⊢}{f}={\mathrm{I}↾}_{\mathrm{Vtx}\left({B}\right)}\to \left(\left({f}:\mathrm{Vtx}\left({A}\right)\underset{1-1 onto}{⟶}\mathrm{Vtx}\left({B}\right)\wedge \exists {g}\phantom{\rule{.4em}{0ex}}\left({g}:\mathrm{dom}\mathrm{iEdg}\left({A}\right)\underset{1-1 onto}{⟶}\mathrm{dom}\mathrm{iEdg}\left({B}\right)\wedge \forall {i}\in \mathrm{dom}\mathrm{iEdg}\left({A}\right)\phantom{\rule{.4em}{0ex}}{f}\left[\mathrm{iEdg}\left({A}\right)\left({i}\right)\right]=\mathrm{iEdg}\left({B}\right)\left({g}\left({i}\right)\right)\right)\right)↔\left(\left({\mathrm{I}↾}_{\mathrm{Vtx}\left({B}\right)}\right):\mathrm{Vtx}\left({A}\right)\underset{1-1 onto}{⟶}\mathrm{Vtx}\left({B}\right)\wedge \exists {g}\phantom{\rule{.4em}{0ex}}\left({g}:\mathrm{dom}\mathrm{iEdg}\left({A}\right)\underset{1-1 onto}{⟶}\mathrm{dom}\mathrm{iEdg}\left({B}\right)\wedge \forall {i}\in \mathrm{dom}\mathrm{iEdg}\left({A}\right)\phantom{\rule{.4em}{0ex}}\left({\mathrm{I}↾}_{\mathrm{Vtx}\left({B}\right)}\right)\left[\mathrm{iEdg}\left({A}\right)\left({i}\right)\right]=\mathrm{iEdg}\left({B}\right)\left({g}\left({i}\right)\right)\right)\right)\right)$
55 2 47 54 spcedv ${⊢}\left(\left({A}\in \mathrm{UHGraph}\wedge {B}\in {Y}\right)\wedge \left(\mathrm{Vtx}\left({A}\right)=\mathrm{Vtx}\left({B}\right)\wedge \mathrm{iEdg}\left({A}\right)=\mathrm{iEdg}\left({B}\right)\right)\right)\to \exists {f}\phantom{\rule{.4em}{0ex}}\left({f}:\mathrm{Vtx}\left({A}\right)\underset{1-1 onto}{⟶}\mathrm{Vtx}\left({B}\right)\wedge \exists {g}\phantom{\rule{.4em}{0ex}}\left({g}:\mathrm{dom}\mathrm{iEdg}\left({A}\right)\underset{1-1 onto}{⟶}\mathrm{dom}\mathrm{iEdg}\left({B}\right)\wedge \forall {i}\in \mathrm{dom}\mathrm{iEdg}\left({A}\right)\phantom{\rule{.4em}{0ex}}{f}\left[\mathrm{iEdg}\left({A}\right)\left({i}\right)\right]=\mathrm{iEdg}\left({B}\right)\left({g}\left({i}\right)\right)\right)\right)$
56 eqid ${⊢}\mathrm{Vtx}\left({B}\right)=\mathrm{Vtx}\left({B}\right)$
57 eqid ${⊢}\mathrm{iEdg}\left({B}\right)=\mathrm{iEdg}\left({B}\right)$
58 15 56 16 57 isomgr ${⊢}\left({A}\in \mathrm{UHGraph}\wedge {B}\in {Y}\right)\to \left({A}\mathrm{IsomGr}{B}↔\exists {f}\phantom{\rule{.4em}{0ex}}\left({f}:\mathrm{Vtx}\left({A}\right)\underset{1-1 onto}{⟶}\mathrm{Vtx}\left({B}\right)\wedge \exists {g}\phantom{\rule{.4em}{0ex}}\left({g}:\mathrm{dom}\mathrm{iEdg}\left({A}\right)\underset{1-1 onto}{⟶}\mathrm{dom}\mathrm{iEdg}\left({B}\right)\wedge \forall {i}\in \mathrm{dom}\mathrm{iEdg}\left({A}\right)\phantom{\rule{.4em}{0ex}}{f}\left[\mathrm{iEdg}\left({A}\right)\left({i}\right)\right]=\mathrm{iEdg}\left({B}\right)\left({g}\left({i}\right)\right)\right)\right)\right)$
59 58 adantr ${⊢}\left(\left({A}\in \mathrm{UHGraph}\wedge {B}\in {Y}\right)\wedge \left(\mathrm{Vtx}\left({A}\right)=\mathrm{Vtx}\left({B}\right)\wedge \mathrm{iEdg}\left({A}\right)=\mathrm{iEdg}\left({B}\right)\right)\right)\to \left({A}\mathrm{IsomGr}{B}↔\exists {f}\phantom{\rule{.4em}{0ex}}\left({f}:\mathrm{Vtx}\left({A}\right)\underset{1-1 onto}{⟶}\mathrm{Vtx}\left({B}\right)\wedge \exists {g}\phantom{\rule{.4em}{0ex}}\left({g}:\mathrm{dom}\mathrm{iEdg}\left({A}\right)\underset{1-1 onto}{⟶}\mathrm{dom}\mathrm{iEdg}\left({B}\right)\wedge \forall {i}\in \mathrm{dom}\mathrm{iEdg}\left({A}\right)\phantom{\rule{.4em}{0ex}}{f}\left[\mathrm{iEdg}\left({A}\right)\left({i}\right)\right]=\mathrm{iEdg}\left({B}\right)\left({g}\left({i}\right)\right)\right)\right)\right)$
60 55 59 mpbird ${⊢}\left(\left({A}\in \mathrm{UHGraph}\wedge {B}\in {Y}\right)\wedge \left(\mathrm{Vtx}\left({A}\right)=\mathrm{Vtx}\left({B}\right)\wedge \mathrm{iEdg}\left({A}\right)=\mathrm{iEdg}\left({B}\right)\right)\right)\to {A}\mathrm{IsomGr}{B}$