This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem grictr

Description: Graph isomorphism is transitive. (Contributed by AV, 5-Dec-2022) (Revised by AV, 3-May-2025)

Ref Expression
Assertion grictr ( ( 𝑅 ≃𝑔𝑟 𝑆 ∧ 𝑆 ≃𝑔𝑟 𝑇 ) → 𝑅 ≃𝑔𝑟 𝑇 )

Proof

Step Hyp Ref Expression
1 brgric ⊢ ( 𝑅 ≃𝑔𝑟 𝑆 ↔ ( 𝑅 GraphIso 𝑆 ) ≠ ∅ )
2 brgric ⊢ ( 𝑆 ≃𝑔𝑟 𝑇 ↔ ( 𝑆 GraphIso 𝑇 ) ≠ ∅ )
3 n0 ⊢ ( ( 𝑅 GraphIso 𝑆 ) ≠ ∅ ↔ ∃ 𝑔 𝑔 ∈ ( 𝑅 GraphIso 𝑆 ) )
4 n0 ⊢ ( ( 𝑆 GraphIso 𝑇 ) ≠ ∅ ↔ ∃ 𝑓 𝑓 ∈ ( 𝑆 GraphIso 𝑇 ) )
5 exdistrv ⊢ ( ∃ 𝑔 ∃ 𝑓 ( 𝑔 ∈ ( 𝑅 GraphIso 𝑆 ) ∧ 𝑓 ∈ ( 𝑆 GraphIso 𝑇 ) ) ↔ ( ∃ 𝑔 𝑔 ∈ ( 𝑅 GraphIso 𝑆 ) ∧ ∃ 𝑓 𝑓 ∈ ( 𝑆 GraphIso 𝑇 ) ) )
6 grimco ⊢ ( ( 𝑓 ∈ ( 𝑆 GraphIso 𝑇 ) ∧ 𝑔 ∈ ( 𝑅 GraphIso 𝑆 ) ) → ( 𝑓 ∘ 𝑔 ) ∈ ( 𝑅 GraphIso 𝑇 ) )
7 6 ancoms ⊢ ( ( 𝑔 ∈ ( 𝑅 GraphIso 𝑆 ) ∧ 𝑓 ∈ ( 𝑆 GraphIso 𝑇 ) ) → ( 𝑓 ∘ 𝑔 ) ∈ ( 𝑅 GraphIso 𝑇 ) )
8 brgrici ⊢ ( ( 𝑓 ∘ 𝑔 ) ∈ ( 𝑅 GraphIso 𝑇 ) → 𝑅 ≃𝑔𝑟 𝑇 )
9 7 8 syl ⊢ ( ( 𝑔 ∈ ( 𝑅 GraphIso 𝑆 ) ∧ 𝑓 ∈ ( 𝑆 GraphIso 𝑇 ) ) → 𝑅 ≃𝑔𝑟 𝑇 )
10 9 exlimivv ⊢ ( ∃ 𝑔 ∃ 𝑓 ( 𝑔 ∈ ( 𝑅 GraphIso 𝑆 ) ∧ 𝑓 ∈ ( 𝑆 GraphIso 𝑇 ) ) → 𝑅 ≃𝑔𝑟 𝑇 )
11 5 10 sylbir ⊢ ( ( ∃ 𝑔 𝑔 ∈ ( 𝑅 GraphIso 𝑆 ) ∧ ∃ 𝑓 𝑓 ∈ ( 𝑆 GraphIso 𝑇 ) ) → 𝑅 ≃𝑔𝑟 𝑇 )
12 3 4 11 syl2anb ⊢ ( ( ( 𝑅 GraphIso 𝑆 ) ≠ ∅ ∧ ( 𝑆 GraphIso 𝑇 ) ≠ ∅ ) → 𝑅 ≃𝑔𝑟 𝑇 )
13 1 2 12 syl2anb ⊢ ( ( 𝑅 ≃𝑔𝑟 𝑆 ∧ 𝑆 ≃𝑔𝑟 𝑇 ) → 𝑅 ≃𝑔𝑟 𝑇 )