Metamath Proof Explorer


Theorem isomgrtr

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

Ref Expression
Assertion isomgrtr AUHGraphBUHGraphCXAIsomGrBBIsomGrCAIsomGrC

Proof

Step Hyp Ref Expression
1 eqid VtxA=VtxA
2 eqid VtxB=VtxB
3 eqid iEdgA=iEdgA
4 eqid iEdgB=iEdgB
5 1 2 3 4 isomgr AUHGraphBUHGraphAIsomGrBff:VtxA1-1 ontoVtxBgg:domiEdgA1-1 ontodomiEdgBidomiEdgAfiEdgAi=iEdgBgi
6 5 3adant3 AUHGraphBUHGraphCXAIsomGrBff:VtxA1-1 ontoVtxBgg:domiEdgA1-1 ontodomiEdgBidomiEdgAfiEdgAi=iEdgBgi
7 eqid VtxC=VtxC
8 eqid iEdgC=iEdgC
9 2 7 4 8 isomgr BUHGraphCXBIsomGrCvv:VtxB1-1 ontoVtxCww:domiEdgB1-1 ontodomiEdgCkdomiEdgBviEdgBk=iEdgCwk
10 9 3adant1 AUHGraphBUHGraphCXBIsomGrCvv:VtxB1-1 ontoVtxCww:domiEdgB1-1 ontodomiEdgCkdomiEdgBviEdgBk=iEdgCwk
11 6 10 anbi12d AUHGraphBUHGraphCXAIsomGrBBIsomGrCff:VtxA1-1 ontoVtxBgg:domiEdgA1-1 ontodomiEdgBidomiEdgAfiEdgAi=iEdgBgivv:VtxB1-1 ontoVtxCww:domiEdgB1-1 ontodomiEdgCkdomiEdgBviEdgBk=iEdgCwk
12 vex vV
13 vex fV
14 12 13 coex vfV
15 14 a1i AUHGraphBUHGraphCXf:VtxA1-1 ontoVtxBgg:domiEdgA1-1 ontodomiEdgBidomiEdgAfiEdgAi=iEdgBgiv:VtxB1-1 ontoVtxCww:domiEdgB1-1 ontodomiEdgCkdomiEdgBviEdgBk=iEdgCwkvfV
16 simpl v:VtxB1-1 ontoVtxCww:domiEdgB1-1 ontodomiEdgCkdomiEdgBviEdgBk=iEdgCwkv:VtxB1-1 ontoVtxC
17 simprl AUHGraphBUHGraphCXf:VtxA1-1 ontoVtxBgg:domiEdgA1-1 ontodomiEdgBidomiEdgAfiEdgAi=iEdgBgif:VtxA1-1 ontoVtxB
18 f1oco v:VtxB1-1 ontoVtxCf:VtxA1-1 ontoVtxBvf:VtxA1-1 ontoVtxC
19 16 17 18 syl2anr AUHGraphBUHGraphCXf:VtxA1-1 ontoVtxBgg:domiEdgA1-1 ontodomiEdgBidomiEdgAfiEdgAi=iEdgBgiv:VtxB1-1 ontoVtxCww:domiEdgB1-1 ontodomiEdgCkdomiEdgBviEdgBk=iEdgCwkvf:VtxA1-1 ontoVtxC
20 vex wV
21 vex gV
22 20 21 coex wgV
23 22 a1i AUHGraphBUHGraphCXf:VtxA1-1 ontoVtxBv:VtxB1-1 ontoVtxCg:domiEdgA1-1 ontodomiEdgBidomiEdgAfiEdgAi=iEdgBgiw:domiEdgB1-1 ontodomiEdgCkdomiEdgBviEdgBk=iEdgCwkwgV
24 simpl w:domiEdgB1-1 ontodomiEdgCkdomiEdgBviEdgBk=iEdgCwkw:domiEdgB1-1 ontodomiEdgC
25 simprl AUHGraphBUHGraphCXf:VtxA1-1 ontoVtxBv:VtxB1-1 ontoVtxCg:domiEdgA1-1 ontodomiEdgBidomiEdgAfiEdgAi=iEdgBgig:domiEdgA1-1 ontodomiEdgB
26 f1oco w:domiEdgB1-1 ontodomiEdgCg:domiEdgA1-1 ontodomiEdgBwg:domiEdgA1-1 ontodomiEdgC
27 24 25 26 syl2anr AUHGraphBUHGraphCXf:VtxA1-1 ontoVtxBv:VtxB1-1 ontoVtxCg:domiEdgA1-1 ontodomiEdgBidomiEdgAfiEdgAi=iEdgBgiw:domiEdgB1-1 ontodomiEdgCkdomiEdgBviEdgBk=iEdgCwkwg:domiEdgA1-1 ontodomiEdgC
28 isomgrtrlem AUHGraphBUHGraphCXf:VtxA1-1 ontoVtxBv:VtxB1-1 ontoVtxCg:domiEdgA1-1 ontodomiEdgBidomiEdgAfiEdgAi=iEdgBgiw:domiEdgB1-1 ontodomiEdgCkdomiEdgBviEdgBk=iEdgCwkjdomiEdgAvfiEdgAj=iEdgCwgj
29 27 28 jca AUHGraphBUHGraphCXf:VtxA1-1 ontoVtxBv:VtxB1-1 ontoVtxCg:domiEdgA1-1 ontodomiEdgBidomiEdgAfiEdgAi=iEdgBgiw:domiEdgB1-1 ontodomiEdgCkdomiEdgBviEdgBk=iEdgCwkwg:domiEdgA1-1 ontodomiEdgCjdomiEdgAvfiEdgAj=iEdgCwgj
30 f1oeq1 h=wgh:domiEdgA1-1 ontodomiEdgCwg:domiEdgA1-1 ontodomiEdgC
31 fveq1 h=wghj=wgj
32 31 fveq2d h=wgiEdgChj=iEdgCwgj
33 32 eqeq2d h=wgvfiEdgAj=iEdgChjvfiEdgAj=iEdgCwgj
34 33 ralbidv h=wgjdomiEdgAvfiEdgAj=iEdgChjjdomiEdgAvfiEdgAj=iEdgCwgj
35 30 34 anbi12d h=wgh:domiEdgA1-1 ontodomiEdgCjdomiEdgAvfiEdgAj=iEdgChjwg:domiEdgA1-1 ontodomiEdgCjdomiEdgAvfiEdgAj=iEdgCwgj
36 23 29 35 spcedv AUHGraphBUHGraphCXf:VtxA1-1 ontoVtxBv:VtxB1-1 ontoVtxCg:domiEdgA1-1 ontodomiEdgBidomiEdgAfiEdgAi=iEdgBgiw:domiEdgB1-1 ontodomiEdgCkdomiEdgBviEdgBk=iEdgCwkhh:domiEdgA1-1 ontodomiEdgCjdomiEdgAvfiEdgAj=iEdgChj
37 36 ex AUHGraphBUHGraphCXf:VtxA1-1 ontoVtxBv:VtxB1-1 ontoVtxCg:domiEdgA1-1 ontodomiEdgBidomiEdgAfiEdgAi=iEdgBgiw:domiEdgB1-1 ontodomiEdgCkdomiEdgBviEdgBk=iEdgCwkhh:domiEdgA1-1 ontodomiEdgCjdomiEdgAvfiEdgAj=iEdgChj
38 37 exlimdv AUHGraphBUHGraphCXf:VtxA1-1 ontoVtxBv:VtxB1-1 ontoVtxCg:domiEdgA1-1 ontodomiEdgBidomiEdgAfiEdgAi=iEdgBgiww:domiEdgB1-1 ontodomiEdgCkdomiEdgBviEdgBk=iEdgCwkhh:domiEdgA1-1 ontodomiEdgCjdomiEdgAvfiEdgAj=iEdgChj
39 38 ex AUHGraphBUHGraphCXf:VtxA1-1 ontoVtxBv:VtxB1-1 ontoVtxCg:domiEdgA1-1 ontodomiEdgBidomiEdgAfiEdgAi=iEdgBgiww:domiEdgB1-1 ontodomiEdgCkdomiEdgBviEdgBk=iEdgCwkhh:domiEdgA1-1 ontodomiEdgCjdomiEdgAvfiEdgAj=iEdgChj
40 39 exlimdv AUHGraphBUHGraphCXf:VtxA1-1 ontoVtxBv:VtxB1-1 ontoVtxCgg:domiEdgA1-1 ontodomiEdgBidomiEdgAfiEdgAi=iEdgBgiww:domiEdgB1-1 ontodomiEdgCkdomiEdgBviEdgBk=iEdgCwkhh:domiEdgA1-1 ontodomiEdgCjdomiEdgAvfiEdgAj=iEdgChj
41 40 3exp AUHGraphBUHGraphCXf:VtxA1-1 ontoVtxBv:VtxB1-1 ontoVtxCgg:domiEdgA1-1 ontodomiEdgBidomiEdgAfiEdgAi=iEdgBgiww:domiEdgB1-1 ontodomiEdgCkdomiEdgBviEdgBk=iEdgCwkhh:domiEdgA1-1 ontodomiEdgCjdomiEdgAvfiEdgAj=iEdgChj
42 41 com34 AUHGraphBUHGraphCXf:VtxA1-1 ontoVtxBgg:domiEdgA1-1 ontodomiEdgBidomiEdgAfiEdgAi=iEdgBgiv:VtxB1-1 ontoVtxCww:domiEdgB1-1 ontodomiEdgCkdomiEdgBviEdgBk=iEdgCwkhh:domiEdgA1-1 ontodomiEdgCjdomiEdgAvfiEdgAj=iEdgChj
43 42 imp32 AUHGraphBUHGraphCXf:VtxA1-1 ontoVtxBgg:domiEdgA1-1 ontodomiEdgBidomiEdgAfiEdgAi=iEdgBgiv:VtxB1-1 ontoVtxCww:domiEdgB1-1 ontodomiEdgCkdomiEdgBviEdgBk=iEdgCwkhh:domiEdgA1-1 ontodomiEdgCjdomiEdgAvfiEdgAj=iEdgChj
44 43 imp32 AUHGraphBUHGraphCXf:VtxA1-1 ontoVtxBgg:domiEdgA1-1 ontodomiEdgBidomiEdgAfiEdgAi=iEdgBgiv:VtxB1-1 ontoVtxCww:domiEdgB1-1 ontodomiEdgCkdomiEdgBviEdgBk=iEdgCwkhh:domiEdgA1-1 ontodomiEdgCjdomiEdgAvfiEdgAj=iEdgChj
45 19 44 jca AUHGraphBUHGraphCXf:VtxA1-1 ontoVtxBgg:domiEdgA1-1 ontodomiEdgBidomiEdgAfiEdgAi=iEdgBgiv:VtxB1-1 ontoVtxCww:domiEdgB1-1 ontodomiEdgCkdomiEdgBviEdgBk=iEdgCwkvf:VtxA1-1 ontoVtxChh:domiEdgA1-1 ontodomiEdgCjdomiEdgAvfiEdgAj=iEdgChj
46 f1oeq1 e=vfe:VtxA1-1 ontoVtxCvf:VtxA1-1 ontoVtxC
47 imaeq1 e=vfeiEdgAj=vfiEdgAj
48 47 eqeq1d e=vfeiEdgAj=iEdgChjvfiEdgAj=iEdgChj
49 48 ralbidv e=vfjdomiEdgAeiEdgAj=iEdgChjjdomiEdgAvfiEdgAj=iEdgChj
50 49 anbi2d e=vfh:domiEdgA1-1 ontodomiEdgCjdomiEdgAeiEdgAj=iEdgChjh:domiEdgA1-1 ontodomiEdgCjdomiEdgAvfiEdgAj=iEdgChj
51 50 exbidv e=vfhh:domiEdgA1-1 ontodomiEdgCjdomiEdgAeiEdgAj=iEdgChjhh:domiEdgA1-1 ontodomiEdgCjdomiEdgAvfiEdgAj=iEdgChj
52 46 51 anbi12d e=vfe:VtxA1-1 ontoVtxChh:domiEdgA1-1 ontodomiEdgCjdomiEdgAeiEdgAj=iEdgChjvf:VtxA1-1 ontoVtxChh:domiEdgA1-1 ontodomiEdgCjdomiEdgAvfiEdgAj=iEdgChj
53 15 45 52 spcedv AUHGraphBUHGraphCXf:VtxA1-1 ontoVtxBgg:domiEdgA1-1 ontodomiEdgBidomiEdgAfiEdgAi=iEdgBgiv:VtxB1-1 ontoVtxCww:domiEdgB1-1 ontodomiEdgCkdomiEdgBviEdgBk=iEdgCwkee:VtxA1-1 ontoVtxChh:domiEdgA1-1 ontodomiEdgCjdomiEdgAeiEdgAj=iEdgChj
54 1 7 3 8 isomgr AUHGraphCXAIsomGrCee:VtxA1-1 ontoVtxChh:domiEdgA1-1 ontodomiEdgCjdomiEdgAeiEdgAj=iEdgChj
55 54 3adant2 AUHGraphBUHGraphCXAIsomGrCee:VtxA1-1 ontoVtxChh:domiEdgA1-1 ontodomiEdgCjdomiEdgAeiEdgAj=iEdgChj
56 55 ad2antrr AUHGraphBUHGraphCXf:VtxA1-1 ontoVtxBgg:domiEdgA1-1 ontodomiEdgBidomiEdgAfiEdgAi=iEdgBgiv:VtxB1-1 ontoVtxCww:domiEdgB1-1 ontodomiEdgCkdomiEdgBviEdgBk=iEdgCwkAIsomGrCee:VtxA1-1 ontoVtxChh:domiEdgA1-1 ontodomiEdgCjdomiEdgAeiEdgAj=iEdgChj
57 53 56 mpbird AUHGraphBUHGraphCXf:VtxA1-1 ontoVtxBgg:domiEdgA1-1 ontodomiEdgBidomiEdgAfiEdgAi=iEdgBgiv:VtxB1-1 ontoVtxCww:domiEdgB1-1 ontodomiEdgCkdomiEdgBviEdgBk=iEdgCwkAIsomGrC
58 57 ex AUHGraphBUHGraphCXf:VtxA1-1 ontoVtxBgg:domiEdgA1-1 ontodomiEdgBidomiEdgAfiEdgAi=iEdgBgiv:VtxB1-1 ontoVtxCww:domiEdgB1-1 ontodomiEdgCkdomiEdgBviEdgBk=iEdgCwkAIsomGrC
59 58 exlimdv AUHGraphBUHGraphCXf:VtxA1-1 ontoVtxBgg:domiEdgA1-1 ontodomiEdgBidomiEdgAfiEdgAi=iEdgBgivv:VtxB1-1 ontoVtxCww:domiEdgB1-1 ontodomiEdgCkdomiEdgBviEdgBk=iEdgCwkAIsomGrC
60 59 ex AUHGraphBUHGraphCXf:VtxA1-1 ontoVtxBgg:domiEdgA1-1 ontodomiEdgBidomiEdgAfiEdgAi=iEdgBgivv:VtxB1-1 ontoVtxCww:domiEdgB1-1 ontodomiEdgCkdomiEdgBviEdgBk=iEdgCwkAIsomGrC
61 60 exlimdv AUHGraphBUHGraphCXff:VtxA1-1 ontoVtxBgg:domiEdgA1-1 ontodomiEdgBidomiEdgAfiEdgAi=iEdgBgivv:VtxB1-1 ontoVtxCww:domiEdgB1-1 ontodomiEdgCkdomiEdgBviEdgBk=iEdgCwkAIsomGrC
62 61 impd AUHGraphBUHGraphCXff:VtxA1-1 ontoVtxBgg:domiEdgA1-1 ontodomiEdgBidomiEdgAfiEdgAi=iEdgBgivv:VtxB1-1 ontoVtxCww:domiEdgB1-1 ontodomiEdgCkdomiEdgBviEdgBk=iEdgCwkAIsomGrC
63 11 62 sylbid AUHGraphBUHGraphCXAIsomGrBBIsomGrCAIsomGrC