Description: The isomorphy relation is transitive for hypergraphs. (Contributed by AV, 5-Dec-2022)
Ref | Expression | ||
---|---|---|---|
Assertion | isomgrtr | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid | |
|
2 | eqid | |
|
3 | eqid | |
|
4 | eqid | |
|
5 | 1 2 3 4 | isomgr | |
6 | 5 | 3adant3 | |
7 | eqid | |
|
8 | eqid | |
|
9 | 2 7 4 8 | isomgr | |
10 | 9 | 3adant1 | |
11 | 6 10 | anbi12d | |
12 | vex | |
|
13 | vex | |
|
14 | 12 13 | coex | |
15 | 14 | a1i | |
16 | simpl | |
|
17 | simprl | |
|
18 | f1oco | |
|
19 | 16 17 18 | syl2anr | |
20 | vex | |
|
21 | vex | |
|
22 | 20 21 | coex | |
23 | 22 | a1i | |
24 | simpl | |
|
25 | simprl | |
|
26 | f1oco | |
|
27 | 24 25 26 | syl2anr | |
28 | isomgrtrlem | |
|
29 | 27 28 | jca | |
30 | f1oeq1 | |
|
31 | fveq1 | |
|
32 | 31 | fveq2d | |
33 | 32 | eqeq2d | |
34 | 33 | ralbidv | |
35 | 30 34 | anbi12d | |
36 | 23 29 35 | spcedv | |
37 | 36 | ex | |
38 | 37 | exlimdv | |
39 | 38 | ex | |
40 | 39 | exlimdv | |
41 | 40 | 3exp | |
42 | 41 | com34 | |
43 | 42 | imp32 | |
44 | 43 | imp32 | |
45 | 19 44 | jca | |
46 | f1oeq1 | |
|
47 | imaeq1 | |
|
48 | 47 | eqeq1d | |
49 | 48 | ralbidv | |
50 | 49 | anbi2d | |
51 | 50 | exbidv | |
52 | 46 51 | anbi12d | |
53 | 15 45 52 | spcedv | |
54 | 1 7 3 8 | isomgr | |
55 | 54 | 3adant2 | |
56 | 55 | ad2antrr | |
57 | 53 56 | mpbird | |
58 | 57 | ex | |
59 | 58 | exlimdv | |
60 | 59 | ex | |
61 | 60 | exlimdv | |
62 | 61 | impd | |
63 | 11 62 | sylbid | |