| Step |
Hyp |
Ref |
Expression |
| 1 |
|
fvexd |
⊢ ( 𝐺 ∈ UHGraph → ( Vtx ‘ 𝐺 ) ∈ V ) |
| 2 |
1
|
resiexd |
⊢ ( 𝐺 ∈ UHGraph → ( I ↾ ( Vtx ‘ 𝐺 ) ) ∈ V ) |
| 3 |
|
eqid |
⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 ) |
| 4 |
3
|
clnbgrssvtx |
⊢ ( 𝐺 ClNeighbVtx 𝑣 ) ⊆ ( Vtx ‘ 𝐺 ) |
| 5 |
4
|
a1i |
⊢ ( 𝑣 ∈ ( Vtx ‘ 𝐺 ) → ( 𝐺 ClNeighbVtx 𝑣 ) ⊆ ( Vtx ‘ 𝐺 ) ) |
| 6 |
3
|
isubgruhgr |
⊢ ( ( 𝐺 ∈ UHGraph ∧ ( 𝐺 ClNeighbVtx 𝑣 ) ⊆ ( Vtx ‘ 𝐺 ) ) → ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ∈ UHGraph ) |
| 7 |
5 6
|
sylan2 |
⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ) → ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ∈ UHGraph ) |
| 8 |
|
gricref |
⊢ ( ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ∈ UHGraph → ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ) |
| 9 |
7 8
|
syl |
⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ) → ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ) |
| 10 |
9
|
ralrimiva |
⊢ ( 𝐺 ∈ UHGraph → ∀ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ) |
| 11 |
|
f1oi |
⊢ ( I ↾ ( Vtx ‘ 𝐺 ) ) : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐺 ) |
| 12 |
10 11
|
jctil |
⊢ ( 𝐺 ∈ UHGraph → ( ( I ↾ ( Vtx ‘ 𝐺 ) ) : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ) ) |
| 13 |
|
f1oeq1 |
⊢ ( 𝑓 = ( I ↾ ( Vtx ‘ 𝐺 ) ) → ( 𝑓 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐺 ) ↔ ( I ↾ ( Vtx ‘ 𝐺 ) ) : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐺 ) ) ) |
| 14 |
|
fveq1 |
⊢ ( 𝑓 = ( I ↾ ( Vtx ‘ 𝐺 ) ) → ( 𝑓 ‘ 𝑣 ) = ( ( I ↾ ( Vtx ‘ 𝐺 ) ) ‘ 𝑣 ) ) |
| 15 |
14
|
oveq2d |
⊢ ( 𝑓 = ( I ↾ ( Vtx ‘ 𝐺 ) ) → ( 𝐺 ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) = ( 𝐺 ClNeighbVtx ( ( I ↾ ( Vtx ‘ 𝐺 ) ) ‘ 𝑣 ) ) ) |
| 16 |
15
|
oveq2d |
⊢ ( 𝑓 = ( I ↾ ( Vtx ‘ 𝐺 ) ) → ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) ) = ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx ( ( I ↾ ( Vtx ‘ 𝐺 ) ) ‘ 𝑣 ) ) ) ) |
| 17 |
16
|
breq2d |
⊢ ( 𝑓 = ( I ↾ ( Vtx ‘ 𝐺 ) ) → ( ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) ) ↔ ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx ( ( I ↾ ( Vtx ‘ 𝐺 ) ) ‘ 𝑣 ) ) ) ) ) |
| 18 |
|
fvresi |
⊢ ( 𝑣 ∈ ( Vtx ‘ 𝐺 ) → ( ( I ↾ ( Vtx ‘ 𝐺 ) ) ‘ 𝑣 ) = 𝑣 ) |
| 19 |
18
|
oveq2d |
⊢ ( 𝑣 ∈ ( Vtx ‘ 𝐺 ) → ( 𝐺 ClNeighbVtx ( ( I ↾ ( Vtx ‘ 𝐺 ) ) ‘ 𝑣 ) ) = ( 𝐺 ClNeighbVtx 𝑣 ) ) |
| 20 |
19
|
oveq2d |
⊢ ( 𝑣 ∈ ( Vtx ‘ 𝐺 ) → ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx ( ( I ↾ ( Vtx ‘ 𝐺 ) ) ‘ 𝑣 ) ) ) = ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ) |
| 21 |
20
|
breq2d |
⊢ ( 𝑣 ∈ ( Vtx ‘ 𝐺 ) → ( ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx ( ( I ↾ ( Vtx ‘ 𝐺 ) ) ‘ 𝑣 ) ) ) ↔ ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ) ) |
| 22 |
17 21
|
sylan9bb |
⊢ ( ( 𝑓 = ( I ↾ ( Vtx ‘ 𝐺 ) ) ∧ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ) → ( ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) ) ↔ ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ) ) |
| 23 |
22
|
ralbidva |
⊢ ( 𝑓 = ( I ↾ ( Vtx ‘ 𝐺 ) ) → ( ∀ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) ) ↔ ∀ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ) ) |
| 24 |
13 23
|
anbi12d |
⊢ ( 𝑓 = ( I ↾ ( Vtx ‘ 𝐺 ) ) → ( ( 𝑓 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) ) ) ↔ ( ( I ↾ ( Vtx ‘ 𝐺 ) ) : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ) ) ) |
| 25 |
2 12 24
|
spcedv |
⊢ ( 𝐺 ∈ UHGraph → ∃ 𝑓 ( 𝑓 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) ) ) ) |
| 26 |
3 3
|
dfgrlic2 |
⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐺 ∈ UHGraph ) → ( 𝐺 ≃𝑙𝑔𝑟 𝐺 ↔ ∃ 𝑓 ( 𝑓 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) ) ) ) ) |
| 27 |
26
|
anidms |
⊢ ( 𝐺 ∈ UHGraph → ( 𝐺 ≃𝑙𝑔𝑟 𝐺 ↔ ∃ 𝑓 ( 𝑓 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) ) ) ) ) |
| 28 |
25 27
|
mpbird |
⊢ ( 𝐺 ∈ UHGraph → 𝐺 ≃𝑙𝑔𝑟 𝐺 ) |