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 AUHGraphBYVtxA=VtxBiEdgA=iEdgBAIsomGrB

Proof

Step Hyp Ref Expression
1 fvexd AUHGraphBYVtxA=VtxBiEdgA=iEdgBVtxBV
2 1 resiexd AUHGraphBYVtxA=VtxBiEdgA=iEdgBIVtxBV
3 f1oi IVtxB:VtxB1-1 ontoVtxB
4 simprl AUHGraphBYVtxA=VtxBiEdgA=iEdgBVtxA=VtxB
5 4 f1oeq2d AUHGraphBYVtxA=VtxBiEdgA=iEdgBIVtxB:VtxA1-1 ontoVtxBIVtxB:VtxB1-1 ontoVtxB
6 3 5 mpbiri AUHGraphBYVtxA=VtxBiEdgA=iEdgBIVtxB:VtxA1-1 ontoVtxB
7 fvexd AUHGraphBYVtxA=VtxBiEdgA=iEdgBiEdgBV
8 7 dmexd AUHGraphBYVtxA=VtxBiEdgA=iEdgBdomiEdgBV
9 8 resiexd AUHGraphBYVtxA=VtxBiEdgA=iEdgBIdomiEdgBV
10 f1oi IdomiEdgB:domiEdgB1-1 ontodomiEdgB
11 simprr AUHGraphBYVtxA=VtxBiEdgA=iEdgBiEdgA=iEdgB
12 11 dmeqd AUHGraphBYVtxA=VtxBiEdgA=iEdgBdomiEdgA=domiEdgB
13 12 f1oeq2d AUHGraphBYVtxA=VtxBiEdgA=iEdgBIdomiEdgB:domiEdgA1-1 ontodomiEdgBIdomiEdgB:domiEdgB1-1 ontodomiEdgB
14 10 13 mpbiri AUHGraphBYVtxA=VtxBiEdgA=iEdgBIdomiEdgB:domiEdgA1-1 ontodomiEdgB
15 eqid VtxA=VtxA
16 eqid iEdgA=iEdgA
17 15 16 uhgrss AUHGraphidomiEdgAiEdgAiVtxA
18 17 ad4ant14 AUHGraphBYVtxA=VtxBiEdgA=iEdgBidomiEdgAiEdgAiVtxA
19 sseq2 VtxA=VtxBiEdgAiVtxAiEdgAiVtxB
20 19 adantr VtxA=VtxBiEdgA=iEdgBiEdgAiVtxAiEdgAiVtxB
21 20 adantl AUHGraphBYVtxA=VtxBiEdgA=iEdgBiEdgAiVtxAiEdgAiVtxB
22 21 adantr AUHGraphBYVtxA=VtxBiEdgA=iEdgBidomiEdgAiEdgAiVtxAiEdgAiVtxB
23 18 22 mpbid AUHGraphBYVtxA=VtxBiEdgA=iEdgBidomiEdgAiEdgAiVtxB
24 resiima iEdgAiVtxBIVtxBiEdgAi=iEdgAi
25 23 24 syl AUHGraphBYVtxA=VtxBiEdgA=iEdgBidomiEdgAIVtxBiEdgAi=iEdgAi
26 fvresi idomiEdgAIdomiEdgAi=i
27 26 adantl AUHGraphBYVtxA=VtxBiEdgA=iEdgBidomiEdgAIdomiEdgAi=i
28 27 fveq2d AUHGraphBYVtxA=VtxBiEdgA=iEdgBidomiEdgAiEdgAIdomiEdgAi=iEdgAi
29 id iEdgA=iEdgBiEdgA=iEdgB
30 dmeq iEdgA=iEdgBdomiEdgA=domiEdgB
31 30 reseq2d iEdgA=iEdgBIdomiEdgA=IdomiEdgB
32 31 fveq1d iEdgA=iEdgBIdomiEdgAi=IdomiEdgBi
33 29 32 fveq12d iEdgA=iEdgBiEdgAIdomiEdgAi=iEdgBIdomiEdgBi
34 33 adantl VtxA=VtxBiEdgA=iEdgBiEdgAIdomiEdgAi=iEdgBIdomiEdgBi
35 34 adantl AUHGraphBYVtxA=VtxBiEdgA=iEdgBiEdgAIdomiEdgAi=iEdgBIdomiEdgBi
36 35 adantr AUHGraphBYVtxA=VtxBiEdgA=iEdgBidomiEdgAiEdgAIdomiEdgAi=iEdgBIdomiEdgBi
37 25 28 36 3eqtr2d AUHGraphBYVtxA=VtxBiEdgA=iEdgBidomiEdgAIVtxBiEdgAi=iEdgBIdomiEdgBi
38 37 ralrimiva AUHGraphBYVtxA=VtxBiEdgA=iEdgBidomiEdgAIVtxBiEdgAi=iEdgBIdomiEdgBi
39 14 38 jca AUHGraphBYVtxA=VtxBiEdgA=iEdgBIdomiEdgB:domiEdgA1-1 ontodomiEdgBidomiEdgAIVtxBiEdgAi=iEdgBIdomiEdgBi
40 f1oeq1 g=IdomiEdgBg:domiEdgA1-1 ontodomiEdgBIdomiEdgB:domiEdgA1-1 ontodomiEdgB
41 fveq1 g=IdomiEdgBgi=IdomiEdgBi
42 41 fveq2d g=IdomiEdgBiEdgBgi=iEdgBIdomiEdgBi
43 42 eqeq2d g=IdomiEdgBIVtxBiEdgAi=iEdgBgiIVtxBiEdgAi=iEdgBIdomiEdgBi
44 43 ralbidv g=IdomiEdgBidomiEdgAIVtxBiEdgAi=iEdgBgiidomiEdgAIVtxBiEdgAi=iEdgBIdomiEdgBi
45 40 44 anbi12d g=IdomiEdgBg:domiEdgA1-1 ontodomiEdgBidomiEdgAIVtxBiEdgAi=iEdgBgiIdomiEdgB:domiEdgA1-1 ontodomiEdgBidomiEdgAIVtxBiEdgAi=iEdgBIdomiEdgBi
46 9 39 45 spcedv AUHGraphBYVtxA=VtxBiEdgA=iEdgBgg:domiEdgA1-1 ontodomiEdgBidomiEdgAIVtxBiEdgAi=iEdgBgi
47 6 46 jca AUHGraphBYVtxA=VtxBiEdgA=iEdgBIVtxB:VtxA1-1 ontoVtxBgg:domiEdgA1-1 ontodomiEdgBidomiEdgAIVtxBiEdgAi=iEdgBgi
48 f1oeq1 f=IVtxBf:VtxA1-1 ontoVtxBIVtxB:VtxA1-1 ontoVtxB
49 imaeq1 f=IVtxBfiEdgAi=IVtxBiEdgAi
50 49 eqeq1d f=IVtxBfiEdgAi=iEdgBgiIVtxBiEdgAi=iEdgBgi
51 50 ralbidv f=IVtxBidomiEdgAfiEdgAi=iEdgBgiidomiEdgAIVtxBiEdgAi=iEdgBgi
52 51 anbi2d f=IVtxBg:domiEdgA1-1 ontodomiEdgBidomiEdgAfiEdgAi=iEdgBgig:domiEdgA1-1 ontodomiEdgBidomiEdgAIVtxBiEdgAi=iEdgBgi
53 52 exbidv f=IVtxBgg:domiEdgA1-1 ontodomiEdgBidomiEdgAfiEdgAi=iEdgBgigg:domiEdgA1-1 ontodomiEdgBidomiEdgAIVtxBiEdgAi=iEdgBgi
54 48 53 anbi12d f=IVtxBf:VtxA1-1 ontoVtxBgg:domiEdgA1-1 ontodomiEdgBidomiEdgAfiEdgAi=iEdgBgiIVtxB:VtxA1-1 ontoVtxBgg:domiEdgA1-1 ontodomiEdgBidomiEdgAIVtxBiEdgAi=iEdgBgi
55 2 47 54 spcedv AUHGraphBYVtxA=VtxBiEdgA=iEdgBff:VtxA1-1 ontoVtxBgg:domiEdgA1-1 ontodomiEdgBidomiEdgAfiEdgAi=iEdgBgi
56 eqid VtxB=VtxB
57 eqid iEdgB=iEdgB
58 15 56 16 57 isomgr AUHGraphBYAIsomGrBff:VtxA1-1 ontoVtxBgg:domiEdgA1-1 ontodomiEdgBidomiEdgAfiEdgAi=iEdgBgi
59 58 adantr AUHGraphBYVtxA=VtxBiEdgA=iEdgBAIsomGrBff:VtxA1-1 ontoVtxBgg:domiEdgA1-1 ontodomiEdgBidomiEdgAfiEdgAi=iEdgBgi
60 55 59 mpbird AUHGraphBYVtxA=VtxBiEdgA=iEdgBAIsomGrB