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

Metamath Proof Explorer

Theorem grimco

Description: The composition of graph isomorphisms is a graph isomorphism. (Contributed by AV, 3-May-2025)

Ref Expression
Assertion grimco ( ( 𝐹 ∈ ( 𝑇 GraphIso 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 GraphIso 𝑇 ) ) → ( 𝐹 ∘ 𝐺 ) ∈ ( 𝑆 GraphIso 𝑈 ) )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( Vtx ‘ 𝑇 ) = ( Vtx ‘ 𝑇 )
2 eqid ⊢ ( Vtx ‘ 𝑈 ) = ( Vtx ‘ 𝑈 )
3 eqid ⊢ ( iEdg ‘ 𝑇 ) = ( iEdg ‘ 𝑇 )
4 eqid ⊢ ( iEdg ‘ 𝑈 ) = ( iEdg ‘ 𝑈 )
5 1 2 3 4 grimprop ⊢ ( 𝐹 ∈ ( 𝑇 GraphIso 𝑈 ) → ( 𝐹 : ( Vtx ‘ 𝑇 ) –1-1-onto→ ( Vtx ‘ 𝑈 ) ∧ ∃ 𝑓 ( 𝑓 : dom ( iEdg ‘ 𝑇 ) –1-1-onto→ dom ( iEdg ‘ 𝑈 ) ∧ ∀ 𝑥 ∈ dom ( iEdg ‘ 𝑇 ) ( ( iEdg ‘ 𝑈 ) ‘ ( 𝑓 ‘ 𝑥 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ 𝑥 ) ) ) ) )
6 eqid ⊢ ( Vtx ‘ 𝑆 ) = ( Vtx ‘ 𝑆 )
7 eqid ⊢ ( iEdg ‘ 𝑆 ) = ( iEdg ‘ 𝑆 )
8 6 1 7 3 grimprop ⊢ ( 𝐺 ∈ ( 𝑆 GraphIso 𝑇 ) → ( 𝐺 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ∀ 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑔 ‘ 𝑦 ) ) = ( 𝐺 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) ) ) )
9 f1oco ⊢ ( ( 𝐹 : ( Vtx ‘ 𝑇 ) –1-1-onto→ ( Vtx ‘ 𝑈 ) ∧ 𝐺 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) → ( 𝐹 ∘ 𝐺 ) : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑈 ) )
10 9 ad2ant2r ⊢ ( ( ( 𝐹 : ( Vtx ‘ 𝑇 ) –1-1-onto→ ( Vtx ‘ 𝑈 ) ∧ ∃ 𝑓 ( 𝑓 : dom ( iEdg ‘ 𝑇 ) –1-1-onto→ dom ( iEdg ‘ 𝑈 ) ∧ ∀ 𝑥 ∈ dom ( iEdg ‘ 𝑇 ) ( ( iEdg ‘ 𝑈 ) ‘ ( 𝑓 ‘ 𝑥 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ 𝑥 ) ) ) ) ∧ ( 𝐺 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ∀ 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑔 ‘ 𝑦 ) ) = ( 𝐺 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) ) ) ) → ( 𝐹 ∘ 𝐺 ) : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑈 ) )
11 vex ⊢ 𝑓 ∈ V
12 vex ⊢ 𝑔 ∈ V
13 11 12 coex ⊢ ( 𝑓 ∘ 𝑔 ) ∈ V
14 13 a1i ⊢ ( ( ( 𝐹 : ( Vtx ‘ 𝑇 ) –1-1-onto→ ( Vtx ‘ 𝑈 ) ∧ 𝐺 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) ∧ ( ( 𝑔 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ∀ 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑔 ‘ 𝑦 ) ) = ( 𝐺 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) ) ∧ ( 𝑓 : dom ( iEdg ‘ 𝑇 ) –1-1-onto→ dom ( iEdg ‘ 𝑈 ) ∧ ∀ 𝑥 ∈ dom ( iEdg ‘ 𝑇 ) ( ( iEdg ‘ 𝑈 ) ‘ ( 𝑓 ‘ 𝑥 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ 𝑥 ) ) ) ) ) → ( 𝑓 ∘ 𝑔 ) ∈ V )
15 f1oco ⊢ ( ( 𝑓 : dom ( iEdg ‘ 𝑇 ) –1-1-onto→ dom ( iEdg ‘ 𝑈 ) ∧ 𝑔 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ) → ( 𝑓 ∘ 𝑔 ) : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑈 ) )
16 15 a1d ⊢ ( ( 𝑓 : dom ( iEdg ‘ 𝑇 ) –1-1-onto→ dom ( iEdg ‘ 𝑈 ) ∧ 𝑔 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ) → ( ∀ 𝑥 ∈ dom ( iEdg ‘ 𝑇 ) ( ( iEdg ‘ 𝑈 ) ‘ ( 𝑓 ‘ 𝑥 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ 𝑥 ) ) → ( 𝑓 ∘ 𝑔 ) : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑈 ) ) )
17 16 expcom ⊢ ( 𝑔 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) → ( 𝑓 : dom ( iEdg ‘ 𝑇 ) –1-1-onto→ dom ( iEdg ‘ 𝑈 ) → ( ∀ 𝑥 ∈ dom ( iEdg ‘ 𝑇 ) ( ( iEdg ‘ 𝑈 ) ‘ ( 𝑓 ‘ 𝑥 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ 𝑥 ) ) → ( 𝑓 ∘ 𝑔 ) : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑈 ) ) ) )
18 17 impd ⊢ ( 𝑔 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) → ( ( 𝑓 : dom ( iEdg ‘ 𝑇 ) –1-1-onto→ dom ( iEdg ‘ 𝑈 ) ∧ ∀ 𝑥 ∈ dom ( iEdg ‘ 𝑇 ) ( ( iEdg ‘ 𝑈 ) ‘ ( 𝑓 ‘ 𝑥 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ 𝑥 ) ) ) → ( 𝑓 ∘ 𝑔 ) : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑈 ) ) )
19 18 adantr ⊢ ( ( 𝑔 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ∀ 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑔 ‘ 𝑦 ) ) = ( 𝐺 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) ) → ( ( 𝑓 : dom ( iEdg ‘ 𝑇 ) –1-1-onto→ dom ( iEdg ‘ 𝑈 ) ∧ ∀ 𝑥 ∈ dom ( iEdg ‘ 𝑇 ) ( ( iEdg ‘ 𝑈 ) ‘ ( 𝑓 ‘ 𝑥 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ 𝑥 ) ) ) → ( 𝑓 ∘ 𝑔 ) : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑈 ) ) )
20 19 imp ⊢ ( ( ( 𝑔 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ∀ 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑔 ‘ 𝑦 ) ) = ( 𝐺 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) ) ∧ ( 𝑓 : dom ( iEdg ‘ 𝑇 ) –1-1-onto→ dom ( iEdg ‘ 𝑈 ) ∧ ∀ 𝑥 ∈ dom ( iEdg ‘ 𝑇 ) ( ( iEdg ‘ 𝑈 ) ‘ ( 𝑓 ‘ 𝑥 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ 𝑥 ) ) ) ) → ( 𝑓 ∘ 𝑔 ) : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑈 ) )
21 20 adantl ⊢ ( ( ( 𝐹 : ( Vtx ‘ 𝑇 ) –1-1-onto→ ( Vtx ‘ 𝑈 ) ∧ 𝐺 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) ∧ ( ( 𝑔 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ∀ 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑔 ‘ 𝑦 ) ) = ( 𝐺 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) ) ∧ ( 𝑓 : dom ( iEdg ‘ 𝑇 ) –1-1-onto→ dom ( iEdg ‘ 𝑈 ) ∧ ∀ 𝑥 ∈ dom ( iEdg ‘ 𝑇 ) ( ( iEdg ‘ 𝑈 ) ‘ ( 𝑓 ‘ 𝑥 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ 𝑥 ) ) ) ) ) → ( 𝑓 ∘ 𝑔 ) : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑈 ) )
22 2fveq3 ⊢ ( 𝑦 = 𝑖 → ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑔 ‘ 𝑦 ) ) = ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑔 ‘ 𝑖 ) ) )
23 fveq2 ⊢ ( 𝑦 = 𝑖 → ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) = ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) )
24 23 imaeq2d ⊢ ( 𝑦 = 𝑖 → ( 𝐺 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) = ( 𝐺 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) )
25 22 24 eqeq12d ⊢ ( 𝑦 = 𝑖 → ( ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑔 ‘ 𝑦 ) ) = ( 𝐺 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) ↔ ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐺 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) ) )
26 25 rspcv ⊢ ( 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) → ( ∀ 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑔 ‘ 𝑦 ) ) = ( 𝐺 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) → ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐺 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) ) )
27 26 adantl ⊢ ( ( ( ( 𝐹 : ( Vtx ‘ 𝑇 ) –1-1-onto→ ( Vtx ‘ 𝑈 ) ∧ 𝐺 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) ∧ 𝑔 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ) ∧ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ) → ( ∀ 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑔 ‘ 𝑦 ) ) = ( 𝐺 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) → ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐺 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) ) )
28 27 adantr ⊢ ( ( ( ( ( 𝐹 : ( Vtx ‘ 𝑇 ) –1-1-onto→ ( Vtx ‘ 𝑈 ) ∧ 𝐺 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) ∧ 𝑔 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ) ∧ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ) ∧ ( 𝑓 : dom ( iEdg ‘ 𝑇 ) –1-1-onto→ dom ( iEdg ‘ 𝑈 ) ∧ ∀ 𝑥 ∈ dom ( iEdg ‘ 𝑇 ) ( ( iEdg ‘ 𝑈 ) ‘ ( 𝑓 ‘ 𝑥 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ 𝑥 ) ) ) ) → ( ∀ 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑔 ‘ 𝑦 ) ) = ( 𝐺 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) → ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐺 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) ) )
29 f1of ⊢ ( 𝑔 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) → 𝑔 : dom ( iEdg ‘ 𝑆 ) ⟶ dom ( iEdg ‘ 𝑇 ) )
30 29 adantl ⊢ ( ( ( 𝐹 : ( Vtx ‘ 𝑇 ) –1-1-onto→ ( Vtx ‘ 𝑈 ) ∧ 𝐺 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) ∧ 𝑔 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ) → 𝑔 : dom ( iEdg ‘ 𝑆 ) ⟶ dom ( iEdg ‘ 𝑇 ) )
31 30 ffvelcdmda ⊢ ( ( ( ( 𝐹 : ( Vtx ‘ 𝑇 ) –1-1-onto→ ( Vtx ‘ 𝑈 ) ∧ 𝐺 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) ∧ 𝑔 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ) ∧ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ) → ( 𝑔 ‘ 𝑖 ) ∈ dom ( iEdg ‘ 𝑇 ) )
32 31 adantr ⊢ ( ( ( ( ( 𝐹 : ( Vtx ‘ 𝑇 ) –1-1-onto→ ( Vtx ‘ 𝑈 ) ∧ 𝐺 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) ∧ 𝑔 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ) ∧ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ) ∧ 𝑓 : dom ( iEdg ‘ 𝑇 ) –1-1-onto→ dom ( iEdg ‘ 𝑈 ) ) → ( 𝑔 ‘ 𝑖 ) ∈ dom ( iEdg ‘ 𝑇 ) )
33 2fveq3 ⊢ ( 𝑥 = ( 𝑔 ‘ 𝑖 ) → ( ( iEdg ‘ 𝑈 ) ‘ ( 𝑓 ‘ 𝑥 ) ) = ( ( iEdg ‘ 𝑈 ) ‘ ( 𝑓 ‘ ( 𝑔 ‘ 𝑖 ) ) ) )
34 fveq2 ⊢ ( 𝑥 = ( 𝑔 ‘ 𝑖 ) → ( ( iEdg ‘ 𝑇 ) ‘ 𝑥 ) = ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑔 ‘ 𝑖 ) ) )
35 34 imaeq2d ⊢ ( 𝑥 = ( 𝑔 ‘ 𝑖 ) → ( 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ 𝑥 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑔 ‘ 𝑖 ) ) ) )
36 33 35 eqeq12d ⊢ ( 𝑥 = ( 𝑔 ‘ 𝑖 ) → ( ( ( iEdg ‘ 𝑈 ) ‘ ( 𝑓 ‘ 𝑥 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ 𝑥 ) ) ↔ ( ( iEdg ‘ 𝑈 ) ‘ ( 𝑓 ‘ ( 𝑔 ‘ 𝑖 ) ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) )
37 36 rspcv ⊢ ( ( 𝑔 ‘ 𝑖 ) ∈ dom ( iEdg ‘ 𝑇 ) → ( ∀ 𝑥 ∈ dom ( iEdg ‘ 𝑇 ) ( ( iEdg ‘ 𝑈 ) ‘ ( 𝑓 ‘ 𝑥 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ 𝑥 ) ) → ( ( iEdg ‘ 𝑈 ) ‘ ( 𝑓 ‘ ( 𝑔 ‘ 𝑖 ) ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) )
38 32 37 syl ⊢ ( ( ( ( ( 𝐹 : ( Vtx ‘ 𝑇 ) –1-1-onto→ ( Vtx ‘ 𝑈 ) ∧ 𝐺 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) ∧ 𝑔 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ) ∧ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ) ∧ 𝑓 : dom ( iEdg ‘ 𝑇 ) –1-1-onto→ dom ( iEdg ‘ 𝑈 ) ) → ( ∀ 𝑥 ∈ dom ( iEdg ‘ 𝑇 ) ( ( iEdg ‘ 𝑈 ) ‘ ( 𝑓 ‘ 𝑥 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ 𝑥 ) ) → ( ( iEdg ‘ 𝑈 ) ‘ ( 𝑓 ‘ ( 𝑔 ‘ 𝑖 ) ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) )
39 30 adantr ⊢ ( ( ( ( 𝐹 : ( Vtx ‘ 𝑇 ) –1-1-onto→ ( Vtx ‘ 𝑈 ) ∧ 𝐺 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) ∧ 𝑔 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ) ∧ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ) → 𝑔 : dom ( iEdg ‘ 𝑆 ) ⟶ dom ( iEdg ‘ 𝑇 ) )
40 39 adantr ⊢ ( ( ( ( ( 𝐹 : ( Vtx ‘ 𝑇 ) –1-1-onto→ ( Vtx ‘ 𝑈 ) ∧ 𝐺 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) ∧ 𝑔 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ) ∧ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ) ∧ 𝑓 : dom ( iEdg ‘ 𝑇 ) –1-1-onto→ dom ( iEdg ‘ 𝑈 ) ) → 𝑔 : dom ( iEdg ‘ 𝑆 ) ⟶ dom ( iEdg ‘ 𝑇 ) )
41 simpr ⊢ ( ( ( ( 𝐹 : ( Vtx ‘ 𝑇 ) –1-1-onto→ ( Vtx ‘ 𝑈 ) ∧ 𝐺 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) ∧ 𝑔 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ) ∧ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ) → 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) )
42 41 adantr ⊢ ( ( ( ( ( 𝐹 : ( Vtx ‘ 𝑇 ) –1-1-onto→ ( Vtx ‘ 𝑈 ) ∧ 𝐺 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) ∧ 𝑔 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ) ∧ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ) ∧ 𝑓 : dom ( iEdg ‘ 𝑇 ) –1-1-onto→ dom ( iEdg ‘ 𝑈 ) ) → 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) )
43 40 42 fvco3d ⊢ ( ( ( ( ( 𝐹 : ( Vtx ‘ 𝑇 ) –1-1-onto→ ( Vtx ‘ 𝑈 ) ∧ 𝐺 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) ∧ 𝑔 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ) ∧ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ) ∧ 𝑓 : dom ( iEdg ‘ 𝑇 ) –1-1-onto→ dom ( iEdg ‘ 𝑈 ) ) → ( ( 𝑓 ∘ 𝑔 ) ‘ 𝑖 ) = ( 𝑓 ‘ ( 𝑔 ‘ 𝑖 ) ) )
44 43 adantr ⊢ ( ( ( ( ( ( 𝐹 : ( Vtx ‘ 𝑇 ) –1-1-onto→ ( Vtx ‘ 𝑈 ) ∧ 𝐺 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) ∧ 𝑔 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ) ∧ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ) ∧ 𝑓 : dom ( iEdg ‘ 𝑇 ) –1-1-onto→ dom ( iEdg ‘ 𝑈 ) ) ∧ ( ( iEdg ‘ 𝑈 ) ‘ ( 𝑓 ‘ ( 𝑔 ‘ 𝑖 ) ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) → ( ( 𝑓 ∘ 𝑔 ) ‘ 𝑖 ) = ( 𝑓 ‘ ( 𝑔 ‘ 𝑖 ) ) )
45 44 fveq2d ⊢ ( ( ( ( ( ( 𝐹 : ( Vtx ‘ 𝑇 ) –1-1-onto→ ( Vtx ‘ 𝑈 ) ∧ 𝐺 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) ∧ 𝑔 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ) ∧ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ) ∧ 𝑓 : dom ( iEdg ‘ 𝑇 ) –1-1-onto→ dom ( iEdg ‘ 𝑈 ) ) ∧ ( ( iEdg ‘ 𝑈 ) ‘ ( 𝑓 ‘ ( 𝑔 ‘ 𝑖 ) ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) → ( ( iEdg ‘ 𝑈 ) ‘ ( ( 𝑓 ∘ 𝑔 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝑈 ) ‘ ( 𝑓 ‘ ( 𝑔 ‘ 𝑖 ) ) ) )
46 simpr ⊢ ( ( ( ( ( ( 𝐹 : ( Vtx ‘ 𝑇 ) –1-1-onto→ ( Vtx ‘ 𝑈 ) ∧ 𝐺 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) ∧ 𝑔 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ) ∧ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ) ∧ 𝑓 : dom ( iEdg ‘ 𝑇 ) –1-1-onto→ dom ( iEdg ‘ 𝑈 ) ) ∧ ( ( iEdg ‘ 𝑈 ) ‘ ( 𝑓 ‘ ( 𝑔 ‘ 𝑖 ) ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) → ( ( iEdg ‘ 𝑈 ) ‘ ( 𝑓 ‘ ( 𝑔 ‘ 𝑖 ) ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑔 ‘ 𝑖 ) ) ) )
47 45 46 eqtrd ⊢ ( ( ( ( ( ( 𝐹 : ( Vtx ‘ 𝑇 ) –1-1-onto→ ( Vtx ‘ 𝑈 ) ∧ 𝐺 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) ∧ 𝑔 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ) ∧ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ) ∧ 𝑓 : dom ( iEdg ‘ 𝑇 ) –1-1-onto→ dom ( iEdg ‘ 𝑈 ) ) ∧ ( ( iEdg ‘ 𝑈 ) ‘ ( 𝑓 ‘ ( 𝑔 ‘ 𝑖 ) ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) → ( ( iEdg ‘ 𝑈 ) ‘ ( ( 𝑓 ∘ 𝑔 ) ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑔 ‘ 𝑖 ) ) ) )
48 47 ex ⊢ ( ( ( ( ( 𝐹 : ( Vtx ‘ 𝑇 ) –1-1-onto→ ( Vtx ‘ 𝑈 ) ∧ 𝐺 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) ∧ 𝑔 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ) ∧ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ) ∧ 𝑓 : dom ( iEdg ‘ 𝑇 ) –1-1-onto→ dom ( iEdg ‘ 𝑈 ) ) → ( ( ( iEdg ‘ 𝑈 ) ‘ ( 𝑓 ‘ ( 𝑔 ‘ 𝑖 ) ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑔 ‘ 𝑖 ) ) ) → ( ( iEdg ‘ 𝑈 ) ‘ ( ( 𝑓 ∘ 𝑔 ) ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) )
49 38 48 syld ⊢ ( ( ( ( ( 𝐹 : ( Vtx ‘ 𝑇 ) –1-1-onto→ ( Vtx ‘ 𝑈 ) ∧ 𝐺 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) ∧ 𝑔 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ) ∧ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ) ∧ 𝑓 : dom ( iEdg ‘ 𝑇 ) –1-1-onto→ dom ( iEdg ‘ 𝑈 ) ) → ( ∀ 𝑥 ∈ dom ( iEdg ‘ 𝑇 ) ( ( iEdg ‘ 𝑈 ) ‘ ( 𝑓 ‘ 𝑥 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ 𝑥 ) ) → ( ( iEdg ‘ 𝑈 ) ‘ ( ( 𝑓 ∘ 𝑔 ) ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) )
50 49 impr ⊢ ( ( ( ( ( 𝐹 : ( Vtx ‘ 𝑇 ) –1-1-onto→ ( Vtx ‘ 𝑈 ) ∧ 𝐺 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) ∧ 𝑔 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ) ∧ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ) ∧ ( 𝑓 : dom ( iEdg ‘ 𝑇 ) –1-1-onto→ dom ( iEdg ‘ 𝑈 ) ∧ ∀ 𝑥 ∈ dom ( iEdg ‘ 𝑇 ) ( ( iEdg ‘ 𝑈 ) ‘ ( 𝑓 ‘ 𝑥 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ 𝑥 ) ) ) ) → ( ( iEdg ‘ 𝑈 ) ‘ ( ( 𝑓 ∘ 𝑔 ) ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑔 ‘ 𝑖 ) ) ) )
51 imaeq2 ⊢ ( ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐺 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) → ( 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑔 ‘ 𝑖 ) ) ) = ( 𝐹 “ ( 𝐺 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) ) )
52 imaco ⊢ ( ( 𝐹 ∘ 𝐺 ) “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) = ( 𝐹 “ ( 𝐺 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) )
53 51 52 eqtr4di ⊢ ( ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐺 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) → ( 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑔 ‘ 𝑖 ) ) ) = ( ( 𝐹 ∘ 𝐺 ) “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) )
54 50 53 sylan9eq ⊢ ( ( ( ( ( ( 𝐹 : ( Vtx ‘ 𝑇 ) –1-1-onto→ ( Vtx ‘ 𝑈 ) ∧ 𝐺 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) ∧ 𝑔 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ) ∧ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ) ∧ ( 𝑓 : dom ( iEdg ‘ 𝑇 ) –1-1-onto→ dom ( iEdg ‘ 𝑈 ) ∧ ∀ 𝑥 ∈ dom ( iEdg ‘ 𝑇 ) ( ( iEdg ‘ 𝑈 ) ‘ ( 𝑓 ‘ 𝑥 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ 𝑥 ) ) ) ) ∧ ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐺 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) ) → ( ( iEdg ‘ 𝑈 ) ‘ ( ( 𝑓 ∘ 𝑔 ) ‘ 𝑖 ) ) = ( ( 𝐹 ∘ 𝐺 ) “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) )
55 54 ex ⊢ ( ( ( ( ( 𝐹 : ( Vtx ‘ 𝑇 ) –1-1-onto→ ( Vtx ‘ 𝑈 ) ∧ 𝐺 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) ∧ 𝑔 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ) ∧ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ) ∧ ( 𝑓 : dom ( iEdg ‘ 𝑇 ) –1-1-onto→ dom ( iEdg ‘ 𝑈 ) ∧ ∀ 𝑥 ∈ dom ( iEdg ‘ 𝑇 ) ( ( iEdg ‘ 𝑈 ) ‘ ( 𝑓 ‘ 𝑥 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ 𝑥 ) ) ) ) → ( ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐺 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) → ( ( iEdg ‘ 𝑈 ) ‘ ( ( 𝑓 ∘ 𝑔 ) ‘ 𝑖 ) ) = ( ( 𝐹 ∘ 𝐺 ) “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) ) )
56 28 55 syld ⊢ ( ( ( ( ( 𝐹 : ( Vtx ‘ 𝑇 ) –1-1-onto→ ( Vtx ‘ 𝑈 ) ∧ 𝐺 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) ∧ 𝑔 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ) ∧ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ) ∧ ( 𝑓 : dom ( iEdg ‘ 𝑇 ) –1-1-onto→ dom ( iEdg ‘ 𝑈 ) ∧ ∀ 𝑥 ∈ dom ( iEdg ‘ 𝑇 ) ( ( iEdg ‘ 𝑈 ) ‘ ( 𝑓 ‘ 𝑥 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ 𝑥 ) ) ) ) → ( ∀ 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑔 ‘ 𝑦 ) ) = ( 𝐺 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) → ( ( iEdg ‘ 𝑈 ) ‘ ( ( 𝑓 ∘ 𝑔 ) ‘ 𝑖 ) ) = ( ( 𝐹 ∘ 𝐺 ) “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) ) )
57 56 exp31 ⊢ ( ( ( 𝐹 : ( Vtx ‘ 𝑇 ) –1-1-onto→ ( Vtx ‘ 𝑈 ) ∧ 𝐺 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) ∧ 𝑔 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ) → ( 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) → ( ( 𝑓 : dom ( iEdg ‘ 𝑇 ) –1-1-onto→ dom ( iEdg ‘ 𝑈 ) ∧ ∀ 𝑥 ∈ dom ( iEdg ‘ 𝑇 ) ( ( iEdg ‘ 𝑈 ) ‘ ( 𝑓 ‘ 𝑥 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ 𝑥 ) ) ) → ( ∀ 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑔 ‘ 𝑦 ) ) = ( 𝐺 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) → ( ( iEdg ‘ 𝑈 ) ‘ ( ( 𝑓 ∘ 𝑔 ) ‘ 𝑖 ) ) = ( ( 𝐹 ∘ 𝐺 ) “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) ) ) ) )
58 57 com24 ⊢ ( ( ( 𝐹 : ( Vtx ‘ 𝑇 ) –1-1-onto→ ( Vtx ‘ 𝑈 ) ∧ 𝐺 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) ∧ 𝑔 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ) → ( ∀ 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑔 ‘ 𝑦 ) ) = ( 𝐺 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) → ( ( 𝑓 : dom ( iEdg ‘ 𝑇 ) –1-1-onto→ dom ( iEdg ‘ 𝑈 ) ∧ ∀ 𝑥 ∈ dom ( iEdg ‘ 𝑇 ) ( ( iEdg ‘ 𝑈 ) ‘ ( 𝑓 ‘ 𝑥 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ 𝑥 ) ) ) → ( 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) → ( ( iEdg ‘ 𝑈 ) ‘ ( ( 𝑓 ∘ 𝑔 ) ‘ 𝑖 ) ) = ( ( 𝐹 ∘ 𝐺 ) “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) ) ) ) )
59 58 expimpd ⊢ ( ( 𝐹 : ( Vtx ‘ 𝑇 ) –1-1-onto→ ( Vtx ‘ 𝑈 ) ∧ 𝐺 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) → ( ( 𝑔 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ∀ 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑔 ‘ 𝑦 ) ) = ( 𝐺 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) ) → ( ( 𝑓 : dom ( iEdg ‘ 𝑇 ) –1-1-onto→ dom ( iEdg ‘ 𝑈 ) ∧ ∀ 𝑥 ∈ dom ( iEdg ‘ 𝑇 ) ( ( iEdg ‘ 𝑈 ) ‘ ( 𝑓 ‘ 𝑥 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ 𝑥 ) ) ) → ( 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) → ( ( iEdg ‘ 𝑈 ) ‘ ( ( 𝑓 ∘ 𝑔 ) ‘ 𝑖 ) ) = ( ( 𝐹 ∘ 𝐺 ) “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) ) ) ) )
60 59 imp32 ⊢ ( ( ( 𝐹 : ( Vtx ‘ 𝑇 ) –1-1-onto→ ( Vtx ‘ 𝑈 ) ∧ 𝐺 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) ∧ ( ( 𝑔 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ∀ 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑔 ‘ 𝑦 ) ) = ( 𝐺 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) ) ∧ ( 𝑓 : dom ( iEdg ‘ 𝑇 ) –1-1-onto→ dom ( iEdg ‘ 𝑈 ) ∧ ∀ 𝑥 ∈ dom ( iEdg ‘ 𝑇 ) ( ( iEdg ‘ 𝑈 ) ‘ ( 𝑓 ‘ 𝑥 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ 𝑥 ) ) ) ) ) → ( 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) → ( ( iEdg ‘ 𝑈 ) ‘ ( ( 𝑓 ∘ 𝑔 ) ‘ 𝑖 ) ) = ( ( 𝐹 ∘ 𝐺 ) “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) ) )
61 60 ralrimiv ⊢ ( ( ( 𝐹 : ( Vtx ‘ 𝑇 ) –1-1-onto→ ( Vtx ‘ 𝑈 ) ∧ 𝐺 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) ∧ ( ( 𝑔 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ∀ 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑔 ‘ 𝑦 ) ) = ( 𝐺 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) ) ∧ ( 𝑓 : dom ( iEdg ‘ 𝑇 ) –1-1-onto→ dom ( iEdg ‘ 𝑈 ) ∧ ∀ 𝑥 ∈ dom ( iEdg ‘ 𝑇 ) ( ( iEdg ‘ 𝑈 ) ‘ ( 𝑓 ‘ 𝑥 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ 𝑥 ) ) ) ) ) → ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑈 ) ‘ ( ( 𝑓 ∘ 𝑔 ) ‘ 𝑖 ) ) = ( ( 𝐹 ∘ 𝐺 ) “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) )
62 21 61 jca ⊢ ( ( ( 𝐹 : ( Vtx ‘ 𝑇 ) –1-1-onto→ ( Vtx ‘ 𝑈 ) ∧ 𝐺 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) ∧ ( ( 𝑔 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ∀ 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑔 ‘ 𝑦 ) ) = ( 𝐺 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) ) ∧ ( 𝑓 : dom ( iEdg ‘ 𝑇 ) –1-1-onto→ dom ( iEdg ‘ 𝑈 ) ∧ ∀ 𝑥 ∈ dom ( iEdg ‘ 𝑇 ) ( ( iEdg ‘ 𝑈 ) ‘ ( 𝑓 ‘ 𝑥 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ 𝑥 ) ) ) ) ) → ( ( 𝑓 ∘ 𝑔 ) : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑈 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑈 ) ‘ ( ( 𝑓 ∘ 𝑔 ) ‘ 𝑖 ) ) = ( ( 𝐹 ∘ 𝐺 ) “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) ) )
63 f1oeq1 ⊢ ( 𝑗 = ( 𝑓 ∘ 𝑔 ) → ( 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑈 ) ↔ ( 𝑓 ∘ 𝑔 ) : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑈 ) ) )
64 fveq1 ⊢ ( 𝑗 = ( 𝑓 ∘ 𝑔 ) → ( 𝑗 ‘ 𝑖 ) = ( ( 𝑓 ∘ 𝑔 ) ‘ 𝑖 ) )
65 64 fveqeq2d ⊢ ( 𝑗 = ( 𝑓 ∘ 𝑔 ) → ( ( ( iEdg ‘ 𝑈 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( ( 𝐹 ∘ 𝐺 ) “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) ↔ ( ( iEdg ‘ 𝑈 ) ‘ ( ( 𝑓 ∘ 𝑔 ) ‘ 𝑖 ) ) = ( ( 𝐹 ∘ 𝐺 ) “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) ) )
66 65 ralbidv ⊢ ( 𝑗 = ( 𝑓 ∘ 𝑔 ) → ( ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑈 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( ( 𝐹 ∘ 𝐺 ) “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) ↔ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑈 ) ‘ ( ( 𝑓 ∘ 𝑔 ) ‘ 𝑖 ) ) = ( ( 𝐹 ∘ 𝐺 ) “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) ) )
67 63 66 anbi12d ⊢ ( 𝑗 = ( 𝑓 ∘ 𝑔 ) → ( ( 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑈 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑈 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( ( 𝐹 ∘ 𝐺 ) “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) ) ↔ ( ( 𝑓 ∘ 𝑔 ) : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑈 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑈 ) ‘ ( ( 𝑓 ∘ 𝑔 ) ‘ 𝑖 ) ) = ( ( 𝐹 ∘ 𝐺 ) “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) ) ) )
68 14 62 67 spcedv ⊢ ( ( ( 𝐹 : ( Vtx ‘ 𝑇 ) –1-1-onto→ ( Vtx ‘ 𝑈 ) ∧ 𝐺 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) ∧ ( ( 𝑔 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ∀ 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑔 ‘ 𝑦 ) ) = ( 𝐺 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) ) ∧ ( 𝑓 : dom ( iEdg ‘ 𝑇 ) –1-1-onto→ dom ( iEdg ‘ 𝑈 ) ∧ ∀ 𝑥 ∈ dom ( iEdg ‘ 𝑇 ) ( ( iEdg ‘ 𝑈 ) ‘ ( 𝑓 ‘ 𝑥 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ 𝑥 ) ) ) ) ) → ∃ 𝑗 ( 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑈 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑈 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( ( 𝐹 ∘ 𝐺 ) “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) ) )
69 68 exp32 ⊢ ( ( 𝐹 : ( Vtx ‘ 𝑇 ) –1-1-onto→ ( Vtx ‘ 𝑈 ) ∧ 𝐺 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) → ( ( 𝑔 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ∀ 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑔 ‘ 𝑦 ) ) = ( 𝐺 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) ) → ( ( 𝑓 : dom ( iEdg ‘ 𝑇 ) –1-1-onto→ dom ( iEdg ‘ 𝑈 ) ∧ ∀ 𝑥 ∈ dom ( iEdg ‘ 𝑇 ) ( ( iEdg ‘ 𝑈 ) ‘ ( 𝑓 ‘ 𝑥 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ 𝑥 ) ) ) → ∃ 𝑗 ( 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑈 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑈 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( ( 𝐹 ∘ 𝐺 ) “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) ) ) ) )
70 69 exlimdv ⊢ ( ( 𝐹 : ( Vtx ‘ 𝑇 ) –1-1-onto→ ( Vtx ‘ 𝑈 ) ∧ 𝐺 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) → ( ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ∀ 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑔 ‘ 𝑦 ) ) = ( 𝐺 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) ) → ( ( 𝑓 : dom ( iEdg ‘ 𝑇 ) –1-1-onto→ dom ( iEdg ‘ 𝑈 ) ∧ ∀ 𝑥 ∈ dom ( iEdg ‘ 𝑇 ) ( ( iEdg ‘ 𝑈 ) ‘ ( 𝑓 ‘ 𝑥 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ 𝑥 ) ) ) → ∃ 𝑗 ( 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑈 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑈 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( ( 𝐹 ∘ 𝐺 ) “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) ) ) ) )
71 70 expimpd ⊢ ( 𝐹 : ( Vtx ‘ 𝑇 ) –1-1-onto→ ( Vtx ‘ 𝑈 ) → ( ( 𝐺 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ∀ 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑔 ‘ 𝑦 ) ) = ( 𝐺 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) ) ) → ( ( 𝑓 : dom ( iEdg ‘ 𝑇 ) –1-1-onto→ dom ( iEdg ‘ 𝑈 ) ∧ ∀ 𝑥 ∈ dom ( iEdg ‘ 𝑇 ) ( ( iEdg ‘ 𝑈 ) ‘ ( 𝑓 ‘ 𝑥 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ 𝑥 ) ) ) → ∃ 𝑗 ( 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑈 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑈 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( ( 𝐹 ∘ 𝐺 ) “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) ) ) ) )
72 71 com23 ⊢ ( 𝐹 : ( Vtx ‘ 𝑇 ) –1-1-onto→ ( Vtx ‘ 𝑈 ) → ( ( 𝑓 : dom ( iEdg ‘ 𝑇 ) –1-1-onto→ dom ( iEdg ‘ 𝑈 ) ∧ ∀ 𝑥 ∈ dom ( iEdg ‘ 𝑇 ) ( ( iEdg ‘ 𝑈 ) ‘ ( 𝑓 ‘ 𝑥 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ 𝑥 ) ) ) → ( ( 𝐺 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ∀ 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑔 ‘ 𝑦 ) ) = ( 𝐺 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) ) ) → ∃ 𝑗 ( 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑈 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑈 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( ( 𝐹 ∘ 𝐺 ) “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) ) ) ) )
73 72 exlimdv ⊢ ( 𝐹 : ( Vtx ‘ 𝑇 ) –1-1-onto→ ( Vtx ‘ 𝑈 ) → ( ∃ 𝑓 ( 𝑓 : dom ( iEdg ‘ 𝑇 ) –1-1-onto→ dom ( iEdg ‘ 𝑈 ) ∧ ∀ 𝑥 ∈ dom ( iEdg ‘ 𝑇 ) ( ( iEdg ‘ 𝑈 ) ‘ ( 𝑓 ‘ 𝑥 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ 𝑥 ) ) ) → ( ( 𝐺 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ∀ 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑔 ‘ 𝑦 ) ) = ( 𝐺 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) ) ) → ∃ 𝑗 ( 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑈 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑈 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( ( 𝐹 ∘ 𝐺 ) “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) ) ) ) )
74 73 imp31 ⊢ ( ( ( 𝐹 : ( Vtx ‘ 𝑇 ) –1-1-onto→ ( Vtx ‘ 𝑈 ) ∧ ∃ 𝑓 ( 𝑓 : dom ( iEdg ‘ 𝑇 ) –1-1-onto→ dom ( iEdg ‘ 𝑈 ) ∧ ∀ 𝑥 ∈ dom ( iEdg ‘ 𝑇 ) ( ( iEdg ‘ 𝑈 ) ‘ ( 𝑓 ‘ 𝑥 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ 𝑥 ) ) ) ) ∧ ( 𝐺 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ∀ 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑔 ‘ 𝑦 ) ) = ( 𝐺 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) ) ) ) → ∃ 𝑗 ( 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑈 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑈 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( ( 𝐹 ∘ 𝐺 ) “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) ) )
75 10 74 jca ⊢ ( ( ( 𝐹 : ( Vtx ‘ 𝑇 ) –1-1-onto→ ( Vtx ‘ 𝑈 ) ∧ ∃ 𝑓 ( 𝑓 : dom ( iEdg ‘ 𝑇 ) –1-1-onto→ dom ( iEdg ‘ 𝑈 ) ∧ ∀ 𝑥 ∈ dom ( iEdg ‘ 𝑇 ) ( ( iEdg ‘ 𝑈 ) ‘ ( 𝑓 ‘ 𝑥 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ 𝑥 ) ) ) ) ∧ ( 𝐺 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ∀ 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑔 ‘ 𝑦 ) ) = ( 𝐺 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) ) ) ) → ( ( 𝐹 ∘ 𝐺 ) : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑈 ) ∧ ∃ 𝑗 ( 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑈 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑈 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( ( 𝐹 ∘ 𝐺 ) “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) ) ) )
76 5 8 75 syl2an ⊢ ( ( 𝐹 ∈ ( 𝑇 GraphIso 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 GraphIso 𝑇 ) ) → ( ( 𝐹 ∘ 𝐺 ) : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑈 ) ∧ ∃ 𝑗 ( 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑈 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑈 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( ( 𝐹 ∘ 𝐺 ) “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) ) ) )
77 grimdmrel ⊢ Rel dom GraphIso
78 77 ovrcl ⊢ ( 𝐺 ∈ ( 𝑆 GraphIso 𝑇 ) → ( 𝑆 ∈ V ∧ 𝑇 ∈ V ) )
79 78 simpld ⊢ ( 𝐺 ∈ ( 𝑆 GraphIso 𝑇 ) → 𝑆 ∈ V )
80 79 adantl ⊢ ( ( 𝐹 ∈ ( 𝑇 GraphIso 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 GraphIso 𝑇 ) ) → 𝑆 ∈ V )
81 77 ovrcl ⊢ ( 𝐹 ∈ ( 𝑇 GraphIso 𝑈 ) → ( 𝑇 ∈ V ∧ 𝑈 ∈ V ) )
82 81 simprd ⊢ ( 𝐹 ∈ ( 𝑇 GraphIso 𝑈 ) → 𝑈 ∈ V )
83 82 adantr ⊢ ( ( 𝐹 ∈ ( 𝑇 GraphIso 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 GraphIso 𝑇 ) ) → 𝑈 ∈ V )
84 coexg ⊢ ( ( 𝐹 ∈ ( 𝑇 GraphIso 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 GraphIso 𝑇 ) ) → ( 𝐹 ∘ 𝐺 ) ∈ V )
85 6 2 7 4 isgrim ⊢ ( ( 𝑆 ∈ V ∧ 𝑈 ∈ V ∧ ( 𝐹 ∘ 𝐺 ) ∈ V ) → ( ( 𝐹 ∘ 𝐺 ) ∈ ( 𝑆 GraphIso 𝑈 ) ↔ ( ( 𝐹 ∘ 𝐺 ) : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑈 ) ∧ ∃ 𝑗 ( 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑈 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑈 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( ( 𝐹 ∘ 𝐺 ) “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) ) ) ) )
86 80 83 84 85 syl3anc ⊢ ( ( 𝐹 ∈ ( 𝑇 GraphIso 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 GraphIso 𝑇 ) ) → ( ( 𝐹 ∘ 𝐺 ) ∈ ( 𝑆 GraphIso 𝑈 ) ↔ ( ( 𝐹 ∘ 𝐺 ) : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑈 ) ∧ ∃ 𝑗 ( 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑈 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑈 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( ( 𝐹 ∘ 𝐺 ) “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) ) ) ) )
87 76 86 mpbird ⊢ ( ( 𝐹 ∈ ( 𝑇 GraphIso 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 GraphIso 𝑇 ) ) → ( 𝐹 ∘ 𝐺 ) ∈ ( 𝑆 GraphIso 𝑈 ) )