Metamath Proof Explorer


Theorem isomgrtr

Description: The isomorphy relation is transitive for hypergraphs. (Contributed by AV, 5-Dec-2022)

Ref Expression
Assertion isomgrtr A UHGraph B UHGraph C X A IsomGr B B IsomGr C A IsomGr C

Proof

Step Hyp Ref Expression
1 eqid Vtx A = Vtx A
2 eqid Vtx B = Vtx B
3 eqid iEdg A = iEdg A
4 eqid iEdg B = iEdg B
5 1 2 3 4 isomgr A UHGraph B UHGraph A IsomGr B f f : Vtx A 1-1 onto Vtx B g g : dom iEdg A 1-1 onto dom iEdg B i dom iEdg A f iEdg A i = iEdg B g i
6 5 3adant3 A UHGraph B UHGraph C X A IsomGr B f f : Vtx A 1-1 onto Vtx B g g : dom iEdg A 1-1 onto dom iEdg B i dom iEdg A f iEdg A i = iEdg B g i
7 eqid Vtx C = Vtx C
8 eqid iEdg C = iEdg C
9 2 7 4 8 isomgr B UHGraph C X B IsomGr C v v : Vtx B 1-1 onto Vtx C w w : dom iEdg B 1-1 onto dom iEdg C k dom iEdg B v iEdg B k = iEdg C w k
10 9 3adant1 A UHGraph B UHGraph C X B IsomGr C v v : Vtx B 1-1 onto Vtx C w w : dom iEdg B 1-1 onto dom iEdg C k dom iEdg B v iEdg B k = iEdg C w k
11 6 10 anbi12d A UHGraph B UHGraph C X A IsomGr B B IsomGr C f f : Vtx A 1-1 onto Vtx B g g : dom iEdg A 1-1 onto dom iEdg B i dom iEdg A f iEdg A i = iEdg B g i v v : Vtx B 1-1 onto Vtx C w w : dom iEdg B 1-1 onto dom iEdg C k dom iEdg B v iEdg B k = iEdg C w k
12 vex v V
13 vex f V
14 12 13 coex v f V
15 14 a1i A UHGraph B UHGraph C X f : Vtx A 1-1 onto Vtx B g g : dom iEdg A 1-1 onto dom iEdg B i dom iEdg A f iEdg A i = iEdg B g i v : Vtx B 1-1 onto Vtx C w w : dom iEdg B 1-1 onto dom iEdg C k dom iEdg B v iEdg B k = iEdg C w k v f V
16 simpl v : Vtx B 1-1 onto Vtx C w w : dom iEdg B 1-1 onto dom iEdg C k dom iEdg B v iEdg B k = iEdg C w k v : Vtx B 1-1 onto Vtx C
17 simprl A UHGraph B UHGraph C X f : Vtx A 1-1 onto Vtx B g g : dom iEdg A 1-1 onto dom iEdg B i dom iEdg A f iEdg A i = iEdg B g i f : Vtx A 1-1 onto Vtx B
18 f1oco v : Vtx B 1-1 onto Vtx C f : Vtx A 1-1 onto Vtx B v f : Vtx A 1-1 onto Vtx C
19 16 17 18 syl2anr A UHGraph B UHGraph C X f : Vtx A 1-1 onto Vtx B g g : dom iEdg A 1-1 onto dom iEdg B i dom iEdg A f iEdg A i = iEdg B g i v : Vtx B 1-1 onto Vtx C w w : dom iEdg B 1-1 onto dom iEdg C k dom iEdg B v iEdg B k = iEdg C w k v f : Vtx A 1-1 onto Vtx C
20 vex w V
21 vex g V
22 20 21 coex w g V
23 22 a1i A UHGraph B UHGraph C X f : Vtx A 1-1 onto Vtx B v : Vtx B 1-1 onto Vtx C g : dom iEdg A 1-1 onto dom iEdg B i dom iEdg A f iEdg A i = iEdg B g i w : dom iEdg B 1-1 onto dom iEdg C k dom iEdg B v iEdg B k = iEdg C w k w g V
24 simpl w : dom iEdg B 1-1 onto dom iEdg C k dom iEdg B v iEdg B k = iEdg C w k w : dom iEdg B 1-1 onto dom iEdg C
25 simprl A UHGraph B UHGraph C X f : Vtx A 1-1 onto Vtx B v : Vtx B 1-1 onto Vtx C g : dom iEdg A 1-1 onto dom iEdg B i dom iEdg A f iEdg A i = iEdg B g i g : dom iEdg A 1-1 onto dom iEdg B
26 f1oco w : dom iEdg B 1-1 onto dom iEdg C g : dom iEdg A 1-1 onto dom iEdg B w g : dom iEdg A 1-1 onto dom iEdg C
27 24 25 26 syl2anr A UHGraph B UHGraph C X f : Vtx A 1-1 onto Vtx B v : Vtx B 1-1 onto Vtx C g : dom iEdg A 1-1 onto dom iEdg B i dom iEdg A f iEdg A i = iEdg B g i w : dom iEdg B 1-1 onto dom iEdg C k dom iEdg B v iEdg B k = iEdg C w k w g : dom iEdg A 1-1 onto dom iEdg C
28 isomgrtrlem A UHGraph B UHGraph C X f : Vtx A 1-1 onto Vtx B v : Vtx B 1-1 onto Vtx C g : dom iEdg A 1-1 onto dom iEdg B i dom iEdg A f iEdg A i = iEdg B g i w : dom iEdg B 1-1 onto dom iEdg C k dom iEdg B v iEdg B k = iEdg C w k j dom iEdg A v f iEdg A j = iEdg C w g j
29 27 28 jca A UHGraph B UHGraph C X f : Vtx A 1-1 onto Vtx B v : Vtx B 1-1 onto Vtx C g : dom iEdg A 1-1 onto dom iEdg B i dom iEdg A f iEdg A i = iEdg B g i w : dom iEdg B 1-1 onto dom iEdg C k dom iEdg B v iEdg B k = iEdg C w k w g : dom iEdg A 1-1 onto dom iEdg C j dom iEdg A v f iEdg A j = iEdg C w g j
30 f1oeq1 h = w g h : dom iEdg A 1-1 onto dom iEdg C w g : dom iEdg A 1-1 onto dom iEdg C
31 fveq1 h = w g h j = w g j
32 31 fveq2d h = w g iEdg C h j = iEdg C w g j
33 32 eqeq2d h = w g v f iEdg A j = iEdg C h j v f iEdg A j = iEdg C w g j
34 33 ralbidv h = w g j dom iEdg A v f iEdg A j = iEdg C h j j dom iEdg A v f iEdg A j = iEdg C w g j
35 30 34 anbi12d h = w g h : dom iEdg A 1-1 onto dom iEdg C j dom iEdg A v f iEdg A j = iEdg C h j w g : dom iEdg A 1-1 onto dom iEdg C j dom iEdg A v f iEdg A j = iEdg C w g j
36 23 29 35 spcedv A UHGraph B UHGraph C X f : Vtx A 1-1 onto Vtx B v : Vtx B 1-1 onto Vtx C g : dom iEdg A 1-1 onto dom iEdg B i dom iEdg A f iEdg A i = iEdg B g i w : dom iEdg B 1-1 onto dom iEdg C k dom iEdg B v iEdg B k = iEdg C w k h h : dom iEdg A 1-1 onto dom iEdg C j dom iEdg A v f iEdg A j = iEdg C h j
37 36 ex A UHGraph B UHGraph C X f : Vtx A 1-1 onto Vtx B v : Vtx B 1-1 onto Vtx C g : dom iEdg A 1-1 onto dom iEdg B i dom iEdg A f iEdg A i = iEdg B g i w : dom iEdg B 1-1 onto dom iEdg C k dom iEdg B v iEdg B k = iEdg C w k h h : dom iEdg A 1-1 onto dom iEdg C j dom iEdg A v f iEdg A j = iEdg C h j
38 37 exlimdv A UHGraph B UHGraph C X f : Vtx A 1-1 onto Vtx B v : Vtx B 1-1 onto Vtx C g : dom iEdg A 1-1 onto dom iEdg B i dom iEdg A f iEdg A i = iEdg B g i w w : dom iEdg B 1-1 onto dom iEdg C k dom iEdg B v iEdg B k = iEdg C w k h h : dom iEdg A 1-1 onto dom iEdg C j dom iEdg A v f iEdg A j = iEdg C h j
39 38 ex A UHGraph B UHGraph C X f : Vtx A 1-1 onto Vtx B v : Vtx B 1-1 onto Vtx C g : dom iEdg A 1-1 onto dom iEdg B i dom iEdg A f iEdg A i = iEdg B g i w w : dom iEdg B 1-1 onto dom iEdg C k dom iEdg B v iEdg B k = iEdg C w k h h : dom iEdg A 1-1 onto dom iEdg C j dom iEdg A v f iEdg A j = iEdg C h j
40 39 exlimdv A UHGraph B UHGraph C X f : Vtx A 1-1 onto Vtx B v : Vtx B 1-1 onto Vtx C g g : dom iEdg A 1-1 onto dom iEdg B i dom iEdg A f iEdg A i = iEdg B g i w w : dom iEdg B 1-1 onto dom iEdg C k dom iEdg B v iEdg B k = iEdg C w k h h : dom iEdg A 1-1 onto dom iEdg C j dom iEdg A v f iEdg A j = iEdg C h j
41 40 3exp A UHGraph B UHGraph C X f : Vtx A 1-1 onto Vtx B v : Vtx B 1-1 onto Vtx C g g : dom iEdg A 1-1 onto dom iEdg B i dom iEdg A f iEdg A i = iEdg B g i w w : dom iEdg B 1-1 onto dom iEdg C k dom iEdg B v iEdg B k = iEdg C w k h h : dom iEdg A 1-1 onto dom iEdg C j dom iEdg A v f iEdg A j = iEdg C h j
42 41 com34 A UHGraph B UHGraph C X f : Vtx A 1-1 onto Vtx B g g : dom iEdg A 1-1 onto dom iEdg B i dom iEdg A f iEdg A i = iEdg B g i v : Vtx B 1-1 onto Vtx C w w : dom iEdg B 1-1 onto dom iEdg C k dom iEdg B v iEdg B k = iEdg C w k h h : dom iEdg A 1-1 onto dom iEdg C j dom iEdg A v f iEdg A j = iEdg C h j
43 42 imp32 A UHGraph B UHGraph C X f : Vtx A 1-1 onto Vtx B g g : dom iEdg A 1-1 onto dom iEdg B i dom iEdg A f iEdg A i = iEdg B g i v : Vtx B 1-1 onto Vtx C w w : dom iEdg B 1-1 onto dom iEdg C k dom iEdg B v iEdg B k = iEdg C w k h h : dom iEdg A 1-1 onto dom iEdg C j dom iEdg A v f iEdg A j = iEdg C h j
44 43 imp32 A UHGraph B UHGraph C X f : Vtx A 1-1 onto Vtx B g g : dom iEdg A 1-1 onto dom iEdg B i dom iEdg A f iEdg A i = iEdg B g i v : Vtx B 1-1 onto Vtx C w w : dom iEdg B 1-1 onto dom iEdg C k dom iEdg B v iEdg B k = iEdg C w k h h : dom iEdg A 1-1 onto dom iEdg C j dom iEdg A v f iEdg A j = iEdg C h j
45 19 44 jca A UHGraph B UHGraph C X f : Vtx A 1-1 onto Vtx B g g : dom iEdg A 1-1 onto dom iEdg B i dom iEdg A f iEdg A i = iEdg B g i v : Vtx B 1-1 onto Vtx C w w : dom iEdg B 1-1 onto dom iEdg C k dom iEdg B v iEdg B k = iEdg C w k v f : Vtx A 1-1 onto Vtx C h h : dom iEdg A 1-1 onto dom iEdg C j dom iEdg A v f iEdg A j = iEdg C h j
46 f1oeq1 e = v f e : Vtx A 1-1 onto Vtx C v f : Vtx A 1-1 onto Vtx C
47 imaeq1 e = v f e iEdg A j = v f iEdg A j
48 47 eqeq1d e = v f e iEdg A j = iEdg C h j v f iEdg A j = iEdg C h j
49 48 ralbidv e = v f j dom iEdg A e iEdg A j = iEdg C h j j dom iEdg A v f iEdg A j = iEdg C h j
50 49 anbi2d e = v f h : dom iEdg A 1-1 onto dom iEdg C j dom iEdg A e iEdg A j = iEdg C h j h : dom iEdg A 1-1 onto dom iEdg C j dom iEdg A v f iEdg A j = iEdg C h j
51 50 exbidv e = v f h h : dom iEdg A 1-1 onto dom iEdg C j dom iEdg A e iEdg A j = iEdg C h j h h : dom iEdg A 1-1 onto dom iEdg C j dom iEdg A v f iEdg A j = iEdg C h j
52 46 51 anbi12d e = v f e : Vtx A 1-1 onto Vtx C h h : dom iEdg A 1-1 onto dom iEdg C j dom iEdg A e iEdg A j = iEdg C h j v f : Vtx A 1-1 onto Vtx C h h : dom iEdg A 1-1 onto dom iEdg C j dom iEdg A v f iEdg A j = iEdg C h j
53 15 45 52 spcedv A UHGraph B UHGraph C X f : Vtx A 1-1 onto Vtx B g g : dom iEdg A 1-1 onto dom iEdg B i dom iEdg A f iEdg A i = iEdg B g i v : Vtx B 1-1 onto Vtx C w w : dom iEdg B 1-1 onto dom iEdg C k dom iEdg B v iEdg B k = iEdg C w k e e : Vtx A 1-1 onto Vtx C h h : dom iEdg A 1-1 onto dom iEdg C j dom iEdg A e iEdg A j = iEdg C h j
54 1 7 3 8 isomgr A UHGraph C X A IsomGr C e e : Vtx A 1-1 onto Vtx C h h : dom iEdg A 1-1 onto dom iEdg C j dom iEdg A e iEdg A j = iEdg C h j
55 54 3adant2 A UHGraph B UHGraph C X A IsomGr C e e : Vtx A 1-1 onto Vtx C h h : dom iEdg A 1-1 onto dom iEdg C j dom iEdg A e iEdg A j = iEdg C h j
56 55 ad2antrr A UHGraph B UHGraph C X f : Vtx A 1-1 onto Vtx B g g : dom iEdg A 1-1 onto dom iEdg B i dom iEdg A f iEdg A i = iEdg B g i v : Vtx B 1-1 onto Vtx C w w : dom iEdg B 1-1 onto dom iEdg C k dom iEdg B v iEdg B k = iEdg C w k A IsomGr C e e : Vtx A 1-1 onto Vtx C h h : dom iEdg A 1-1 onto dom iEdg C j dom iEdg A e iEdg A j = iEdg C h j
57 53 56 mpbird A UHGraph B UHGraph C X f : Vtx A 1-1 onto Vtx B g g : dom iEdg A 1-1 onto dom iEdg B i dom iEdg A f iEdg A i = iEdg B g i v : Vtx B 1-1 onto Vtx C w w : dom iEdg B 1-1 onto dom iEdg C k dom iEdg B v iEdg B k = iEdg C w k A IsomGr C
58 57 ex A UHGraph B UHGraph C X f : Vtx A 1-1 onto Vtx B g g : dom iEdg A 1-1 onto dom iEdg B i dom iEdg A f iEdg A i = iEdg B g i v : Vtx B 1-1 onto Vtx C w w : dom iEdg B 1-1 onto dom iEdg C k dom iEdg B v iEdg B k = iEdg C w k A IsomGr C
59 58 exlimdv A UHGraph B UHGraph C X f : Vtx A 1-1 onto Vtx B g g : dom iEdg A 1-1 onto dom iEdg B i dom iEdg A f iEdg A i = iEdg B g i v v : Vtx B 1-1 onto Vtx C w w : dom iEdg B 1-1 onto dom iEdg C k dom iEdg B v iEdg B k = iEdg C w k A IsomGr C
60 59 ex A UHGraph B UHGraph C X f : Vtx A 1-1 onto Vtx B g g : dom iEdg A 1-1 onto dom iEdg B i dom iEdg A f iEdg A i = iEdg B g i v v : Vtx B 1-1 onto Vtx C w w : dom iEdg B 1-1 onto dom iEdg C k dom iEdg B v iEdg B k = iEdg C w k A IsomGr C
61 60 exlimdv A UHGraph B UHGraph C X f f : Vtx A 1-1 onto Vtx B g g : dom iEdg A 1-1 onto dom iEdg B i dom iEdg A f iEdg A i = iEdg B g i v v : Vtx B 1-1 onto Vtx C w w : dom iEdg B 1-1 onto dom iEdg C k dom iEdg B v iEdg B k = iEdg C w k A IsomGr C
62 61 impd A UHGraph B UHGraph C X f f : Vtx A 1-1 onto Vtx B g g : dom iEdg A 1-1 onto dom iEdg B i dom iEdg A f iEdg A i = iEdg B g i v v : Vtx B 1-1 onto Vtx C w w : dom iEdg B 1-1 onto dom iEdg C k dom iEdg B v iEdg B k = iEdg C w k A IsomGr C
63 11 62 sylbid A UHGraph B UHGraph C X A IsomGr B B IsomGr C A IsomGr C