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