| 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 |
5
|
adantl |
⊢ ( ( 𝑆 ∈ UHGraph ∧ 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) ) → ( 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ ∃ 𝑗 ( 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) ) ) ) |
| 7 |
|
f1ocnv |
⊢ ( 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) → ◡ 𝐹 : ( Vtx ‘ 𝑇 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) ) |
| 8 |
7
|
ad2antrl |
⊢ ( ( ( 𝑆 ∈ UHGraph ∧ 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) ) ∧ ( 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ ∃ 𝑗 ( 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) ) ) ) → ◡ 𝐹 : ( Vtx ‘ 𝑇 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) ) |
| 9 |
|
vex |
⊢ 𝑗 ∈ V |
| 10 |
|
cnvexg |
⊢ ( 𝑗 ∈ V → ◡ 𝑗 ∈ V ) |
| 11 |
9 10
|
mp1i |
⊢ ( ( ( ( 𝑆 ∈ UHGraph ∧ 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) ) ∧ 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) ) ) → ◡ 𝑗 ∈ V ) |
| 12 |
|
f1ocnv |
⊢ ( 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) → ◡ 𝑗 : dom ( iEdg ‘ 𝑇 ) –1-1-onto→ dom ( iEdg ‘ 𝑆 ) ) |
| 13 |
12
|
ad2antrl |
⊢ ( ( ( ( 𝑆 ∈ UHGraph ∧ 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) ) ∧ 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) ) ) → ◡ 𝑗 : dom ( iEdg ‘ 𝑇 ) –1-1-onto→ dom ( iEdg ‘ 𝑆 ) ) |
| 14 |
|
f1ofo |
⊢ ( 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) → 𝑗 : dom ( iEdg ‘ 𝑆 ) –onto→ dom ( iEdg ‘ 𝑇 ) ) |
| 15 |
14
|
ad2antrl |
⊢ ( ( ( ( 𝑆 ∈ UHGraph ∧ 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) ) ∧ 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) ) ) → 𝑗 : dom ( iEdg ‘ 𝑆 ) –onto→ dom ( iEdg ‘ 𝑇 ) ) |
| 16 |
|
foelcdmi |
⊢ ( ( 𝑗 : dom ( iEdg ‘ 𝑆 ) –onto→ dom ( iEdg ‘ 𝑇 ) ∧ 𝑥 ∈ dom ( iEdg ‘ 𝑇 ) ) → ∃ 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) ( 𝑗 ‘ 𝑦 ) = 𝑥 ) |
| 17 |
15 16
|
sylan |
⊢ ( ( ( ( ( 𝑆 ∈ UHGraph ∧ 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) ) ∧ 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) ) ) ∧ 𝑥 ∈ dom ( iEdg ‘ 𝑇 ) ) → ∃ 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) ( 𝑗 ‘ 𝑦 ) = 𝑥 ) |
| 18 |
|
2fveq3 |
⊢ ( 𝑖 = 𝑦 → ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑦 ) ) ) |
| 19 |
|
fveq2 |
⊢ ( 𝑖 = 𝑦 → ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) = ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) |
| 20 |
19
|
imaeq2d |
⊢ ( 𝑖 = 𝑦 → ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) ) |
| 21 |
18 20
|
eqeq12d |
⊢ ( 𝑖 = 𝑦 → ( ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) ↔ ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑦 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) ) ) |
| 22 |
21
|
rspcv |
⊢ ( 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) → ( ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) → ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑦 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) ) ) |
| 23 |
22
|
adantl |
⊢ ( ( ( ( ( 𝑆 ∈ UHGraph ∧ 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) ) ∧ 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) ∧ 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ) ∧ 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) ) → ( ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) → ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑦 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) ) ) |
| 24 |
|
f1ocnvfv1 |
⊢ ( ( 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) ) → ( ◡ 𝑗 ‘ ( 𝑗 ‘ 𝑦 ) ) = 𝑦 ) |
| 25 |
24
|
ad4ant23 |
⊢ ( ( ( ( ( ( 𝑆 ∈ UHGraph ∧ 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) ) ∧ 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) ∧ 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ) ∧ 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) ) ∧ ( 𝑗 ‘ 𝑦 ) ∈ dom ( iEdg ‘ 𝑇 ) ) → ( ◡ 𝑗 ‘ ( 𝑗 ‘ 𝑦 ) ) = 𝑦 ) |
| 26 |
25
|
fveq2d |
⊢ ( ( ( ( ( ( 𝑆 ∈ UHGraph ∧ 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) ) ∧ 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) ∧ 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ) ∧ 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) ) ∧ ( 𝑗 ‘ 𝑦 ) ∈ dom ( iEdg ‘ 𝑇 ) ) → ( ( iEdg ‘ 𝑆 ) ‘ ( ◡ 𝑗 ‘ ( 𝑗 ‘ 𝑦 ) ) ) = ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) |
| 27 |
|
f1of1 |
⊢ ( 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) → 𝐹 : ( Vtx ‘ 𝑆 ) –1-1→ ( Vtx ‘ 𝑇 ) ) |
| 28 |
27
|
ad2antlr |
⊢ ( ( ( ( 𝑆 ∈ UHGraph ∧ 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) ) ∧ 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) ∧ 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ) → 𝐹 : ( Vtx ‘ 𝑆 ) –1-1→ ( Vtx ‘ 𝑇 ) ) |
| 29 |
1 3
|
uhgrss |
⊢ ( ( 𝑆 ∈ UHGraph ∧ 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) ) → ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ⊆ ( Vtx ‘ 𝑆 ) ) |
| 30 |
29
|
ad5ant15 |
⊢ ( ( ( ( ( 𝑆 ∈ UHGraph ∧ 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) ) ∧ 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) ∧ 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ) ∧ 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) ) → ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ⊆ ( Vtx ‘ 𝑆 ) ) |
| 31 |
|
f1imacnv |
⊢ ( ( 𝐹 : ( Vtx ‘ 𝑆 ) –1-1→ ( Vtx ‘ 𝑇 ) ∧ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ⊆ ( Vtx ‘ 𝑆 ) ) → ( ◡ 𝐹 “ ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) ) = ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) |
| 32 |
28 30 31
|
syl2an2r |
⊢ ( ( ( ( ( 𝑆 ∈ UHGraph ∧ 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) ) ∧ 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) ∧ 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ) ∧ 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) ) → ( ◡ 𝐹 “ ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) ) = ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) |
| 33 |
32
|
eqcomd |
⊢ ( ( ( ( ( 𝑆 ∈ UHGraph ∧ 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) ) ∧ 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) ∧ 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ) ∧ 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) ) → ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) = ( ◡ 𝐹 “ ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) ) ) |
| 34 |
33
|
adantr |
⊢ ( ( ( ( ( ( 𝑆 ∈ UHGraph ∧ 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) ) ∧ 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) ∧ 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ) ∧ 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) ) ∧ ( 𝑗 ‘ 𝑦 ) ∈ dom ( iEdg ‘ 𝑇 ) ) → ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) = ( ◡ 𝐹 “ ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) ) ) |
| 35 |
26 34
|
eqtrd |
⊢ ( ( ( ( ( ( 𝑆 ∈ UHGraph ∧ 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) ) ∧ 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) ∧ 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ) ∧ 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) ) ∧ ( 𝑗 ‘ 𝑦 ) ∈ dom ( iEdg ‘ 𝑇 ) ) → ( ( iEdg ‘ 𝑆 ) ‘ ( ◡ 𝑗 ‘ ( 𝑗 ‘ 𝑦 ) ) ) = ( ◡ 𝐹 “ ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) ) ) |
| 36 |
35
|
adantlr |
⊢ ( ( ( ( ( ( ( 𝑆 ∈ UHGraph ∧ 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) ) ∧ 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) ∧ 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ) ∧ 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) ) ∧ ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑦 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) ) ∧ ( 𝑗 ‘ 𝑦 ) ∈ dom ( iEdg ‘ 𝑇 ) ) → ( ( iEdg ‘ 𝑆 ) ‘ ( ◡ 𝑗 ‘ ( 𝑗 ‘ 𝑦 ) ) ) = ( ◡ 𝐹 “ ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) ) ) |
| 37 |
|
simplr |
⊢ ( ( ( ( ( ( ( 𝑆 ∈ UHGraph ∧ 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) ) ∧ 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) ∧ 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ) ∧ 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) ) ∧ ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑦 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) ) ∧ ( 𝑗 ‘ 𝑦 ) ∈ dom ( iEdg ‘ 𝑇 ) ) → ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑦 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) ) |
| 38 |
37
|
eqcomd |
⊢ ( ( ( ( ( ( ( 𝑆 ∈ UHGraph ∧ 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) ) ∧ 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) ∧ 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ) ∧ 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) ) ∧ ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑦 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) ) ∧ ( 𝑗 ‘ 𝑦 ) ∈ dom ( iEdg ‘ 𝑇 ) ) → ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) = ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑦 ) ) ) |
| 39 |
38
|
imaeq2d |
⊢ ( ( ( ( ( ( ( 𝑆 ∈ UHGraph ∧ 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) ) ∧ 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) ∧ 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ) ∧ 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) ) ∧ ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑦 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) ) ∧ ( 𝑗 ‘ 𝑦 ) ∈ dom ( iEdg ‘ 𝑇 ) ) → ( ◡ 𝐹 “ ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) ) = ( ◡ 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑦 ) ) ) ) |
| 40 |
36 39
|
eqtrd |
⊢ ( ( ( ( ( ( ( 𝑆 ∈ UHGraph ∧ 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) ) ∧ 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) ∧ 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ) ∧ 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) ) ∧ ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑦 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) ) ∧ ( 𝑗 ‘ 𝑦 ) ∈ dom ( iEdg ‘ 𝑇 ) ) → ( ( iEdg ‘ 𝑆 ) ‘ ( ◡ 𝑗 ‘ ( 𝑗 ‘ 𝑦 ) ) ) = ( ◡ 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑦 ) ) ) ) |
| 41 |
40
|
ex |
⊢ ( ( ( ( ( ( 𝑆 ∈ UHGraph ∧ 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) ) ∧ 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) ∧ 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ) ∧ 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) ) ∧ ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑦 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) ) → ( ( 𝑗 ‘ 𝑦 ) ∈ dom ( iEdg ‘ 𝑇 ) → ( ( iEdg ‘ 𝑆 ) ‘ ( ◡ 𝑗 ‘ ( 𝑗 ‘ 𝑦 ) ) ) = ( ◡ 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑦 ) ) ) ) ) |
| 42 |
41
|
ex |
⊢ ( ( ( ( ( 𝑆 ∈ UHGraph ∧ 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) ) ∧ 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) ∧ 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ) ∧ 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) ) → ( ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑦 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) → ( ( 𝑗 ‘ 𝑦 ) ∈ dom ( iEdg ‘ 𝑇 ) → ( ( iEdg ‘ 𝑆 ) ‘ ( ◡ 𝑗 ‘ ( 𝑗 ‘ 𝑦 ) ) ) = ( ◡ 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑦 ) ) ) ) ) ) |
| 43 |
23 42
|
syld |
⊢ ( ( ( ( ( 𝑆 ∈ UHGraph ∧ 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) ) ∧ 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) ∧ 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ) ∧ 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) ) → ( ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) → ( ( 𝑗 ‘ 𝑦 ) ∈ dom ( iEdg ‘ 𝑇 ) → ( ( iEdg ‘ 𝑆 ) ‘ ( ◡ 𝑗 ‘ ( 𝑗 ‘ 𝑦 ) ) ) = ( ◡ 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑦 ) ) ) ) ) ) |
| 44 |
43
|
ex |
⊢ ( ( ( ( 𝑆 ∈ UHGraph ∧ 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) ) ∧ 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) ∧ 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ) → ( 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) → ( ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) → ( ( 𝑗 ‘ 𝑦 ) ∈ dom ( iEdg ‘ 𝑇 ) → ( ( iEdg ‘ 𝑆 ) ‘ ( ◡ 𝑗 ‘ ( 𝑗 ‘ 𝑦 ) ) ) = ( ◡ 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑦 ) ) ) ) ) ) ) |
| 45 |
44
|
com23 |
⊢ ( ( ( ( 𝑆 ∈ UHGraph ∧ 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) ) ∧ 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) ∧ 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ) → ( ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) → ( 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) → ( ( 𝑗 ‘ 𝑦 ) ∈ dom ( iEdg ‘ 𝑇 ) → ( ( iEdg ‘ 𝑆 ) ‘ ( ◡ 𝑗 ‘ ( 𝑗 ‘ 𝑦 ) ) ) = ( ◡ 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑦 ) ) ) ) ) ) ) |
| 46 |
45
|
impr |
⊢ ( ( ( ( 𝑆 ∈ UHGraph ∧ 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) ) ∧ 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) ) ) → ( 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) → ( ( 𝑗 ‘ 𝑦 ) ∈ dom ( iEdg ‘ 𝑇 ) → ( ( iEdg ‘ 𝑆 ) ‘ ( ◡ 𝑗 ‘ ( 𝑗 ‘ 𝑦 ) ) ) = ( ◡ 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑦 ) ) ) ) ) ) |
| 47 |
|
eleq1 |
⊢ ( ( 𝑗 ‘ 𝑦 ) = 𝑥 → ( ( 𝑗 ‘ 𝑦 ) ∈ dom ( iEdg ‘ 𝑇 ) ↔ 𝑥 ∈ dom ( iEdg ‘ 𝑇 ) ) ) |
| 48 |
|
2fveq3 |
⊢ ( ( 𝑗 ‘ 𝑦 ) = 𝑥 → ( ( iEdg ‘ 𝑆 ) ‘ ( ◡ 𝑗 ‘ ( 𝑗 ‘ 𝑦 ) ) ) = ( ( iEdg ‘ 𝑆 ) ‘ ( ◡ 𝑗 ‘ 𝑥 ) ) ) |
| 49 |
|
fveq2 |
⊢ ( ( 𝑗 ‘ 𝑦 ) = 𝑥 → ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑦 ) ) = ( ( iEdg ‘ 𝑇 ) ‘ 𝑥 ) ) |
| 50 |
49
|
imaeq2d |
⊢ ( ( 𝑗 ‘ 𝑦 ) = 𝑥 → ( ◡ 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑦 ) ) ) = ( ◡ 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ 𝑥 ) ) ) |
| 51 |
48 50
|
eqeq12d |
⊢ ( ( 𝑗 ‘ 𝑦 ) = 𝑥 → ( ( ( iEdg ‘ 𝑆 ) ‘ ( ◡ 𝑗 ‘ ( 𝑗 ‘ 𝑦 ) ) ) = ( ◡ 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑦 ) ) ) ↔ ( ( iEdg ‘ 𝑆 ) ‘ ( ◡ 𝑗 ‘ 𝑥 ) ) = ( ◡ 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ 𝑥 ) ) ) ) |
| 52 |
47 51
|
imbi12d |
⊢ ( ( 𝑗 ‘ 𝑦 ) = 𝑥 → ( ( ( 𝑗 ‘ 𝑦 ) ∈ dom ( iEdg ‘ 𝑇 ) → ( ( iEdg ‘ 𝑆 ) ‘ ( ◡ 𝑗 ‘ ( 𝑗 ‘ 𝑦 ) ) ) = ( ◡ 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑦 ) ) ) ) ↔ ( 𝑥 ∈ dom ( iEdg ‘ 𝑇 ) → ( ( iEdg ‘ 𝑆 ) ‘ ( ◡ 𝑗 ‘ 𝑥 ) ) = ( ◡ 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ 𝑥 ) ) ) ) ) |
| 53 |
52
|
imbi2d |
⊢ ( ( 𝑗 ‘ 𝑦 ) = 𝑥 → ( ( 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) → ( ( 𝑗 ‘ 𝑦 ) ∈ dom ( iEdg ‘ 𝑇 ) → ( ( iEdg ‘ 𝑆 ) ‘ ( ◡ 𝑗 ‘ ( 𝑗 ‘ 𝑦 ) ) ) = ( ◡ 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑦 ) ) ) ) ) ↔ ( 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) → ( 𝑥 ∈ dom ( iEdg ‘ 𝑇 ) → ( ( iEdg ‘ 𝑆 ) ‘ ( ◡ 𝑗 ‘ 𝑥 ) ) = ( ◡ 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ 𝑥 ) ) ) ) ) ) |
| 54 |
46 53
|
syl5ibcom |
⊢ ( ( ( ( 𝑆 ∈ UHGraph ∧ 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) ) ∧ 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) ) ) → ( ( 𝑗 ‘ 𝑦 ) = 𝑥 → ( 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) → ( 𝑥 ∈ dom ( iEdg ‘ 𝑇 ) → ( ( iEdg ‘ 𝑆 ) ‘ ( ◡ 𝑗 ‘ 𝑥 ) ) = ( ◡ 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ 𝑥 ) ) ) ) ) ) |
| 55 |
54
|
com24 |
⊢ ( ( ( ( 𝑆 ∈ UHGraph ∧ 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) ) ∧ 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) ) ) → ( 𝑥 ∈ dom ( iEdg ‘ 𝑇 ) → ( 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) → ( ( 𝑗 ‘ 𝑦 ) = 𝑥 → ( ( iEdg ‘ 𝑆 ) ‘ ( ◡ 𝑗 ‘ 𝑥 ) ) = ( ◡ 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ 𝑥 ) ) ) ) ) ) |
| 56 |
55
|
imp31 |
⊢ ( ( ( ( ( ( 𝑆 ∈ UHGraph ∧ 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) ) ∧ 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) ) ) ∧ 𝑥 ∈ dom ( iEdg ‘ 𝑇 ) ) ∧ 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) ) → ( ( 𝑗 ‘ 𝑦 ) = 𝑥 → ( ( iEdg ‘ 𝑆 ) ‘ ( ◡ 𝑗 ‘ 𝑥 ) ) = ( ◡ 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ 𝑥 ) ) ) ) |
| 57 |
56
|
rexlimdva |
⊢ ( ( ( ( ( 𝑆 ∈ UHGraph ∧ 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) ) ∧ 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) ) ) ∧ 𝑥 ∈ dom ( iEdg ‘ 𝑇 ) ) → ( ∃ 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) ( 𝑗 ‘ 𝑦 ) = 𝑥 → ( ( iEdg ‘ 𝑆 ) ‘ ( ◡ 𝑗 ‘ 𝑥 ) ) = ( ◡ 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ 𝑥 ) ) ) ) |
| 58 |
17 57
|
mpd |
⊢ ( ( ( ( ( 𝑆 ∈ UHGraph ∧ 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) ) ∧ 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) ) ) ∧ 𝑥 ∈ dom ( iEdg ‘ 𝑇 ) ) → ( ( iEdg ‘ 𝑆 ) ‘ ( ◡ 𝑗 ‘ 𝑥 ) ) = ( ◡ 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ 𝑥 ) ) ) |
| 59 |
58
|
ralrimiva |
⊢ ( ( ( ( 𝑆 ∈ UHGraph ∧ 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) ) ∧ 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) ) ) → ∀ 𝑥 ∈ dom ( iEdg ‘ 𝑇 ) ( ( iEdg ‘ 𝑆 ) ‘ ( ◡ 𝑗 ‘ 𝑥 ) ) = ( ◡ 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ 𝑥 ) ) ) |
| 60 |
13 59
|
jca |
⊢ ( ( ( ( 𝑆 ∈ UHGraph ∧ 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) ) ∧ 𝐹 : ( 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 ‘ 𝑇 ) ‘ 𝑥 ) ) ) ) |
| 61 |
|
f1oeq1 |
⊢ ( 𝑓 = ◡ 𝑗 → ( 𝑓 : dom ( iEdg ‘ 𝑇 ) –1-1-onto→ dom ( iEdg ‘ 𝑆 ) ↔ ◡ 𝑗 : dom ( iEdg ‘ 𝑇 ) –1-1-onto→ dom ( iEdg ‘ 𝑆 ) ) ) |
| 62 |
|
fveq1 |
⊢ ( 𝑓 = ◡ 𝑗 → ( 𝑓 ‘ 𝑥 ) = ( ◡ 𝑗 ‘ 𝑥 ) ) |
| 63 |
62
|
fveqeq2d |
⊢ ( 𝑓 = ◡ 𝑗 → ( ( ( iEdg ‘ 𝑆 ) ‘ ( 𝑓 ‘ 𝑥 ) ) = ( ◡ 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ 𝑥 ) ) ↔ ( ( iEdg ‘ 𝑆 ) ‘ ( ◡ 𝑗 ‘ 𝑥 ) ) = ( ◡ 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ 𝑥 ) ) ) ) |
| 64 |
63
|
ralbidv |
⊢ ( 𝑓 = ◡ 𝑗 → ( ∀ 𝑥 ∈ dom ( iEdg ‘ 𝑇 ) ( ( iEdg ‘ 𝑆 ) ‘ ( 𝑓 ‘ 𝑥 ) ) = ( ◡ 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ 𝑥 ) ) ↔ ∀ 𝑥 ∈ dom ( iEdg ‘ 𝑇 ) ( ( iEdg ‘ 𝑆 ) ‘ ( ◡ 𝑗 ‘ 𝑥 ) ) = ( ◡ 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ 𝑥 ) ) ) ) |
| 65 |
61 64
|
anbi12d |
⊢ ( 𝑓 = ◡ 𝑗 → ( ( 𝑓 : dom ( iEdg ‘ 𝑇 ) –1-1-onto→ dom ( iEdg ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ dom ( iEdg ‘ 𝑇 ) ( ( iEdg ‘ 𝑆 ) ‘ ( 𝑓 ‘ 𝑥 ) ) = ( ◡ 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ 𝑥 ) ) ) ↔ ( ◡ 𝑗 : dom ( iEdg ‘ 𝑇 ) –1-1-onto→ dom ( iEdg ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ dom ( iEdg ‘ 𝑇 ) ( ( iEdg ‘ 𝑆 ) ‘ ( ◡ 𝑗 ‘ 𝑥 ) ) = ( ◡ 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ 𝑥 ) ) ) ) ) |
| 66 |
11 60 65
|
spcedv |
⊢ ( ( ( ( 𝑆 ∈ UHGraph ∧ 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) ) ∧ 𝐹 : ( 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 ‘ 𝑇 ) ‘ 𝑥 ) ) ) ) |
| 67 |
66
|
ex |
⊢ ( ( ( 𝑆 ∈ UHGraph ∧ 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) ) ∧ 𝐹 : ( 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 ‘ 𝑇 ) ‘ 𝑥 ) ) ) ) ) |
| 68 |
67
|
exlimdv |
⊢ ( ( ( 𝑆 ∈ UHGraph ∧ 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) ) ∧ 𝐹 : ( 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 ‘ 𝑇 ) ‘ 𝑥 ) ) ) ) ) |
| 69 |
68
|
impr |
⊢ ( ( ( 𝑆 ∈ UHGraph ∧ 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) ) ∧ ( 𝐹 : ( 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 ‘ 𝑇 ) ‘ 𝑥 ) ) ) ) |
| 70 |
|
grimdmrel |
⊢ Rel dom GraphIso |
| 71 |
70
|
ovrcl |
⊢ ( 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) → ( 𝑆 ∈ V ∧ 𝑇 ∈ V ) ) |
| 72 |
71
|
simprd |
⊢ ( 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) → 𝑇 ∈ V ) |
| 73 |
71
|
simpld |
⊢ ( 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) → 𝑆 ∈ V ) |
| 74 |
|
cnvexg |
⊢ ( 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) → ◡ 𝐹 ∈ V ) |
| 75 |
2 1 4 3
|
isgrim |
⊢ ( ( 𝑇 ∈ V ∧ 𝑆 ∈ V ∧ ◡ 𝐹 ∈ V ) → ( ◡ 𝐹 ∈ ( 𝑇 GraphIso 𝑆 ) ↔ ( ◡ 𝐹 : ( Vtx ‘ 𝑇 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) ∧ ∃ 𝑓 ( 𝑓 : dom ( iEdg ‘ 𝑇 ) –1-1-onto→ dom ( iEdg ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ dom ( iEdg ‘ 𝑇 ) ( ( iEdg ‘ 𝑆 ) ‘ ( 𝑓 ‘ 𝑥 ) ) = ( ◡ 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ 𝑥 ) ) ) ) ) ) |
| 76 |
72 73 74 75
|
syl3anc |
⊢ ( 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) → ( ◡ 𝐹 ∈ ( 𝑇 GraphIso 𝑆 ) ↔ ( ◡ 𝐹 : ( Vtx ‘ 𝑇 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) ∧ ∃ 𝑓 ( 𝑓 : dom ( iEdg ‘ 𝑇 ) –1-1-onto→ dom ( iEdg ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ dom ( iEdg ‘ 𝑇 ) ( ( iEdg ‘ 𝑆 ) ‘ ( 𝑓 ‘ 𝑥 ) ) = ( ◡ 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ 𝑥 ) ) ) ) ) ) |
| 77 |
76
|
ad2antlr |
⊢ ( ( ( 𝑆 ∈ UHGraph ∧ 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) ) ∧ ( 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ ∃ 𝑗 ( 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) ) ) ) → ( ◡ 𝐹 ∈ ( 𝑇 GraphIso 𝑆 ) ↔ ( ◡ 𝐹 : ( Vtx ‘ 𝑇 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) ∧ ∃ 𝑓 ( 𝑓 : dom ( iEdg ‘ 𝑇 ) –1-1-onto→ dom ( iEdg ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ dom ( iEdg ‘ 𝑇 ) ( ( iEdg ‘ 𝑆 ) ‘ ( 𝑓 ‘ 𝑥 ) ) = ( ◡ 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ 𝑥 ) ) ) ) ) ) |
| 78 |
8 69 77
|
mpbir2and |
⊢ ( ( ( 𝑆 ∈ UHGraph ∧ 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) ) ∧ ( 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ ∃ 𝑗 ( 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) ) ) ) → ◡ 𝐹 ∈ ( 𝑇 GraphIso 𝑆 ) ) |
| 79 |
6 78
|
mpdan |
⊢ ( ( 𝑆 ∈ UHGraph ∧ 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) ) → ◡ 𝐹 ∈ ( 𝑇 GraphIso 𝑆 ) ) |
| 80 |
79
|
ex |
⊢ ( 𝑆 ∈ UHGraph → ( 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) → ◡ 𝐹 ∈ ( 𝑇 GraphIso 𝑆 ) ) ) |