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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fvexd | |
|
2 | 1 | resiexd | |
3 | f1oi | |
|
4 | simprl | |
|
5 | 4 | f1oeq2d | |
6 | 3 5 | mpbiri | |
7 | fvexd | |
|
8 | 7 | dmexd | |
9 | 8 | resiexd | |
10 | f1oi | |
|
11 | simprr | |
|
12 | 11 | dmeqd | |
13 | 12 | f1oeq2d | |
14 | 10 13 | mpbiri | |
15 | eqid | |
|
16 | eqid | |
|
17 | 15 16 | uhgrss | |
18 | 17 | ad4ant14 | |
19 | sseq2 | |
|
20 | 19 | adantr | |
21 | 20 | adantl | |
22 | 21 | adantr | |
23 | 18 22 | mpbid | |
24 | resiima | |
|
25 | 23 24 | syl | |
26 | fvresi | |
|
27 | 26 | adantl | |
28 | 27 | fveq2d | |
29 | id | |
|
30 | dmeq | |
|
31 | 30 | reseq2d | |
32 | 31 | fveq1d | |
33 | 29 32 | fveq12d | |
34 | 33 | adantl | |
35 | 34 | adantl | |
36 | 35 | adantr | |
37 | 25 28 36 | 3eqtr2d | |
38 | 37 | ralrimiva | |
39 | 14 38 | jca | |
40 | f1oeq1 | |
|
41 | fveq1 | |
|
42 | 41 | fveq2d | |
43 | 42 | eqeq2d | |
44 | 43 | ralbidv | |
45 | 40 44 | anbi12d | |
46 | 9 39 45 | spcedv | |
47 | 6 46 | jca | |
48 | f1oeq1 | |
|
49 | imaeq1 | |
|
50 | 49 | eqeq1d | |
51 | 50 | ralbidv | |
52 | 51 | anbi2d | |
53 | 52 | exbidv | |
54 | 48 53 | anbi12d | |
55 | 2 47 54 | spcedv | |
56 | eqid | |
|
57 | eqid | |
|
58 | 15 56 16 57 | isomgr | |
59 | 58 | adantr | |
60 | 55 59 | mpbird | |