| 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 𝑈 ) ) |