| Step |
Hyp |
Ref |
Expression |
| 1 |
|
grlicrcl |
⊢ ( 𝑅 ≃𝑙𝑔𝑟 𝑆 → ( 𝑅 ∈ V ∧ 𝑆 ∈ V ) ) |
| 2 |
|
grlicrcl |
⊢ ( 𝑆 ≃𝑙𝑔𝑟 𝑇 → ( 𝑆 ∈ V ∧ 𝑇 ∈ V ) ) |
| 3 |
1 2
|
anim12i |
⊢ ( ( 𝑅 ≃𝑙𝑔𝑟 𝑆 ∧ 𝑆 ≃𝑙𝑔𝑟 𝑇 ) → ( ( 𝑅 ∈ V ∧ 𝑆 ∈ V ) ∧ ( 𝑆 ∈ V ∧ 𝑇 ∈ V ) ) ) |
| 4 |
|
eqid |
⊢ ( Vtx ‘ 𝑅 ) = ( Vtx ‘ 𝑅 ) |
| 5 |
|
eqid |
⊢ ( Vtx ‘ 𝑆 ) = ( Vtx ‘ 𝑆 ) |
| 6 |
4 5
|
grilcbri |
⊢ ( 𝑅 ≃𝑙𝑔𝑟 𝑆 → ∃ 𝑔 ( 𝑔 : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) ∧ ∀ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ( 𝑅 ISubGr ( 𝑅 ClNeighbVtx 𝑟 ) ) ≃𝑔𝑟 ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx ( 𝑔 ‘ 𝑟 ) ) ) ) ) |
| 7 |
|
eqid |
⊢ ( Vtx ‘ 𝑇 ) = ( Vtx ‘ 𝑇 ) |
| 8 |
5 7
|
grilcbri |
⊢ ( 𝑆 ≃𝑙𝑔𝑟 𝑇 → ∃ ℎ ( ℎ : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ ∀ 𝑠 ∈ ( Vtx ‘ 𝑆 ) ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx 𝑠 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ℎ ‘ 𝑠 ) ) ) ) ) |
| 9 |
|
vex |
⊢ ℎ ∈ V |
| 10 |
|
vex |
⊢ 𝑔 ∈ V |
| 11 |
9 10
|
coex |
⊢ ( ℎ ∘ 𝑔 ) ∈ V |
| 12 |
11
|
a1i |
⊢ ( ( ( ℎ : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ ∀ 𝑠 ∈ ( Vtx ‘ 𝑆 ) ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx 𝑠 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ℎ ‘ 𝑠 ) ) ) ) ∧ ( 𝑔 : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) ∧ ∀ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ( 𝑅 ISubGr ( 𝑅 ClNeighbVtx 𝑟 ) ) ≃𝑔𝑟 ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx ( 𝑔 ‘ 𝑟 ) ) ) ) ) → ( ℎ ∘ 𝑔 ) ∈ V ) |
| 13 |
|
f1oco |
⊢ ( ( ℎ : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ 𝑔 : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) ) → ( ℎ ∘ 𝑔 ) : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) |
| 14 |
13
|
ad2ant2r |
⊢ ( ( ( ℎ : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ ∀ 𝑠 ∈ ( Vtx ‘ 𝑆 ) ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx 𝑠 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ℎ ‘ 𝑠 ) ) ) ) ∧ ( 𝑔 : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) ∧ ∀ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ( 𝑅 ISubGr ( 𝑅 ClNeighbVtx 𝑟 ) ) ≃𝑔𝑟 ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx ( 𝑔 ‘ 𝑟 ) ) ) ) ) → ( ℎ ∘ 𝑔 ) : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) |
| 15 |
|
f1of |
⊢ ( 𝑔 : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) → 𝑔 : ( Vtx ‘ 𝑅 ) ⟶ ( Vtx ‘ 𝑆 ) ) |
| 16 |
15
|
ffvelcdmda |
⊢ ( ( 𝑔 : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) ∧ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ) → ( 𝑔 ‘ 𝑟 ) ∈ ( Vtx ‘ 𝑆 ) ) |
| 17 |
|
oveq2 |
⊢ ( 𝑠 = ( 𝑔 ‘ 𝑟 ) → ( 𝑆 ClNeighbVtx 𝑠 ) = ( 𝑆 ClNeighbVtx ( 𝑔 ‘ 𝑟 ) ) ) |
| 18 |
17
|
oveq2d |
⊢ ( 𝑠 = ( 𝑔 ‘ 𝑟 ) → ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx 𝑠 ) ) = ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx ( 𝑔 ‘ 𝑟 ) ) ) ) |
| 19 |
|
fveq2 |
⊢ ( 𝑠 = ( 𝑔 ‘ 𝑟 ) → ( ℎ ‘ 𝑠 ) = ( ℎ ‘ ( 𝑔 ‘ 𝑟 ) ) ) |
| 20 |
19
|
oveq2d |
⊢ ( 𝑠 = ( 𝑔 ‘ 𝑟 ) → ( 𝑇 ClNeighbVtx ( ℎ ‘ 𝑠 ) ) = ( 𝑇 ClNeighbVtx ( ℎ ‘ ( 𝑔 ‘ 𝑟 ) ) ) ) |
| 21 |
20
|
oveq2d |
⊢ ( 𝑠 = ( 𝑔 ‘ 𝑟 ) → ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ℎ ‘ 𝑠 ) ) ) = ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ℎ ‘ ( 𝑔 ‘ 𝑟 ) ) ) ) ) |
| 22 |
18 21
|
breq12d |
⊢ ( 𝑠 = ( 𝑔 ‘ 𝑟 ) → ( ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx 𝑠 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ℎ ‘ 𝑠 ) ) ) ↔ ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx ( 𝑔 ‘ 𝑟 ) ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ℎ ‘ ( 𝑔 ‘ 𝑟 ) ) ) ) ) ) |
| 23 |
22
|
rspcv |
⊢ ( ( 𝑔 ‘ 𝑟 ) ∈ ( Vtx ‘ 𝑆 ) → ( ∀ 𝑠 ∈ ( Vtx ‘ 𝑆 ) ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx 𝑠 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ℎ ‘ 𝑠 ) ) ) → ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx ( 𝑔 ‘ 𝑟 ) ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ℎ ‘ ( 𝑔 ‘ 𝑟 ) ) ) ) ) ) |
| 24 |
16 23
|
syl |
⊢ ( ( 𝑔 : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) ∧ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ) → ( ∀ 𝑠 ∈ ( Vtx ‘ 𝑆 ) ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx 𝑠 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ℎ ‘ 𝑠 ) ) ) → ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx ( 𝑔 ‘ 𝑟 ) ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ℎ ‘ ( 𝑔 ‘ 𝑟 ) ) ) ) ) ) |
| 25 |
|
fvco3 |
⊢ ( ( 𝑔 : ( Vtx ‘ 𝑅 ) ⟶ ( Vtx ‘ 𝑆 ) ∧ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ) → ( ( ℎ ∘ 𝑔 ) ‘ 𝑟 ) = ( ℎ ‘ ( 𝑔 ‘ 𝑟 ) ) ) |
| 26 |
15 25
|
sylan |
⊢ ( ( 𝑔 : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) ∧ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ) → ( ( ℎ ∘ 𝑔 ) ‘ 𝑟 ) = ( ℎ ‘ ( 𝑔 ‘ 𝑟 ) ) ) |
| 27 |
26
|
eqcomd |
⊢ ( ( 𝑔 : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) ∧ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ) → ( ℎ ‘ ( 𝑔 ‘ 𝑟 ) ) = ( ( ℎ ∘ 𝑔 ) ‘ 𝑟 ) ) |
| 28 |
27
|
oveq2d |
⊢ ( ( 𝑔 : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) ∧ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ) → ( 𝑇 ClNeighbVtx ( ℎ ‘ ( 𝑔 ‘ 𝑟 ) ) ) = ( 𝑇 ClNeighbVtx ( ( ℎ ∘ 𝑔 ) ‘ 𝑟 ) ) ) |
| 29 |
28
|
oveq2d |
⊢ ( ( 𝑔 : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) ∧ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ) → ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ℎ ‘ ( 𝑔 ‘ 𝑟 ) ) ) ) = ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ( ℎ ∘ 𝑔 ) ‘ 𝑟 ) ) ) ) |
| 30 |
29
|
breq2d |
⊢ ( ( 𝑔 : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) ∧ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ) → ( ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx ( 𝑔 ‘ 𝑟 ) ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ℎ ‘ ( 𝑔 ‘ 𝑟 ) ) ) ) ↔ ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx ( 𝑔 ‘ 𝑟 ) ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ( ℎ ∘ 𝑔 ) ‘ 𝑟 ) ) ) ) ) |
| 31 |
24 30
|
sylibd |
⊢ ( ( 𝑔 : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) ∧ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ) → ( ∀ 𝑠 ∈ ( Vtx ‘ 𝑆 ) ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx 𝑠 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ℎ ‘ 𝑠 ) ) ) → ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx ( 𝑔 ‘ 𝑟 ) ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ( ℎ ∘ 𝑔 ) ‘ 𝑟 ) ) ) ) ) |
| 32 |
31
|
ex |
⊢ ( 𝑔 : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) → ( 𝑟 ∈ ( Vtx ‘ 𝑅 ) → ( ∀ 𝑠 ∈ ( Vtx ‘ 𝑆 ) ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx 𝑠 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ℎ ‘ 𝑠 ) ) ) → ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx ( 𝑔 ‘ 𝑟 ) ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ( ℎ ∘ 𝑔 ) ‘ 𝑟 ) ) ) ) ) ) |
| 33 |
32
|
com3r |
⊢ ( ∀ 𝑠 ∈ ( Vtx ‘ 𝑆 ) ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx 𝑠 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ℎ ‘ 𝑠 ) ) ) → ( 𝑔 : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) → ( 𝑟 ∈ ( Vtx ‘ 𝑅 ) → ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx ( 𝑔 ‘ 𝑟 ) ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ( ℎ ∘ 𝑔 ) ‘ 𝑟 ) ) ) ) ) ) |
| 34 |
33
|
imp31 |
⊢ ( ( ( ∀ 𝑠 ∈ ( Vtx ‘ 𝑆 ) ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx 𝑠 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ℎ ‘ 𝑠 ) ) ) ∧ 𝑔 : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) ) ∧ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ) → ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx ( 𝑔 ‘ 𝑟 ) ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ( ℎ ∘ 𝑔 ) ‘ 𝑟 ) ) ) ) |
| 35 |
34
|
anim1ci |
⊢ ( ( ( ( ∀ 𝑠 ∈ ( Vtx ‘ 𝑆 ) ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx 𝑠 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ℎ ‘ 𝑠 ) ) ) ∧ 𝑔 : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) ) ∧ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ) ∧ ( 𝑅 ISubGr ( 𝑅 ClNeighbVtx 𝑟 ) ) ≃𝑔𝑟 ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx ( 𝑔 ‘ 𝑟 ) ) ) ) → ( ( 𝑅 ISubGr ( 𝑅 ClNeighbVtx 𝑟 ) ) ≃𝑔𝑟 ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx ( 𝑔 ‘ 𝑟 ) ) ) ∧ ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx ( 𝑔 ‘ 𝑟 ) ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ( ℎ ∘ 𝑔 ) ‘ 𝑟 ) ) ) ) ) |
| 36 |
|
grictr |
⊢ ( ( ( 𝑅 ISubGr ( 𝑅 ClNeighbVtx 𝑟 ) ) ≃𝑔𝑟 ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx ( 𝑔 ‘ 𝑟 ) ) ) ∧ ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx ( 𝑔 ‘ 𝑟 ) ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ( ℎ ∘ 𝑔 ) ‘ 𝑟 ) ) ) ) → ( 𝑅 ISubGr ( 𝑅 ClNeighbVtx 𝑟 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ( ℎ ∘ 𝑔 ) ‘ 𝑟 ) ) ) ) |
| 37 |
35 36
|
syl |
⊢ ( ( ( ( ∀ 𝑠 ∈ ( Vtx ‘ 𝑆 ) ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx 𝑠 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ℎ ‘ 𝑠 ) ) ) ∧ 𝑔 : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) ) ∧ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ) ∧ ( 𝑅 ISubGr ( 𝑅 ClNeighbVtx 𝑟 ) ) ≃𝑔𝑟 ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx ( 𝑔 ‘ 𝑟 ) ) ) ) → ( 𝑅 ISubGr ( 𝑅 ClNeighbVtx 𝑟 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ( ℎ ∘ 𝑔 ) ‘ 𝑟 ) ) ) ) |
| 38 |
37
|
ex |
⊢ ( ( ( ∀ 𝑠 ∈ ( Vtx ‘ 𝑆 ) ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx 𝑠 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ℎ ‘ 𝑠 ) ) ) ∧ 𝑔 : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) ) ∧ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ) → ( ( 𝑅 ISubGr ( 𝑅 ClNeighbVtx 𝑟 ) ) ≃𝑔𝑟 ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx ( 𝑔 ‘ 𝑟 ) ) ) → ( 𝑅 ISubGr ( 𝑅 ClNeighbVtx 𝑟 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ( ℎ ∘ 𝑔 ) ‘ 𝑟 ) ) ) ) ) |
| 39 |
38
|
ralimdva |
⊢ ( ( ∀ 𝑠 ∈ ( Vtx ‘ 𝑆 ) ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx 𝑠 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ℎ ‘ 𝑠 ) ) ) ∧ 𝑔 : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) ) → ( ∀ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ( 𝑅 ISubGr ( 𝑅 ClNeighbVtx 𝑟 ) ) ≃𝑔𝑟 ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx ( 𝑔 ‘ 𝑟 ) ) ) → ∀ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ( 𝑅 ISubGr ( 𝑅 ClNeighbVtx 𝑟 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ( ℎ ∘ 𝑔 ) ‘ 𝑟 ) ) ) ) ) |
| 40 |
39
|
expimpd |
⊢ ( ∀ 𝑠 ∈ ( Vtx ‘ 𝑆 ) ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx 𝑠 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ℎ ‘ 𝑠 ) ) ) → ( ( 𝑔 : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) ∧ ∀ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ( 𝑅 ISubGr ( 𝑅 ClNeighbVtx 𝑟 ) ) ≃𝑔𝑟 ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx ( 𝑔 ‘ 𝑟 ) ) ) ) → ∀ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ( 𝑅 ISubGr ( 𝑅 ClNeighbVtx 𝑟 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ( ℎ ∘ 𝑔 ) ‘ 𝑟 ) ) ) ) ) |
| 41 |
40
|
adantl |
⊢ ( ( ℎ : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ ∀ 𝑠 ∈ ( Vtx ‘ 𝑆 ) ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx 𝑠 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ℎ ‘ 𝑠 ) ) ) ) → ( ( 𝑔 : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) ∧ ∀ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ( 𝑅 ISubGr ( 𝑅 ClNeighbVtx 𝑟 ) ) ≃𝑔𝑟 ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx ( 𝑔 ‘ 𝑟 ) ) ) ) → ∀ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ( 𝑅 ISubGr ( 𝑅 ClNeighbVtx 𝑟 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ( ℎ ∘ 𝑔 ) ‘ 𝑟 ) ) ) ) ) |
| 42 |
41
|
imp |
⊢ ( ( ( ℎ : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ ∀ 𝑠 ∈ ( Vtx ‘ 𝑆 ) ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx 𝑠 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ℎ ‘ 𝑠 ) ) ) ) ∧ ( 𝑔 : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) ∧ ∀ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ( 𝑅 ISubGr ( 𝑅 ClNeighbVtx 𝑟 ) ) ≃𝑔𝑟 ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx ( 𝑔 ‘ 𝑟 ) ) ) ) ) → ∀ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ( 𝑅 ISubGr ( 𝑅 ClNeighbVtx 𝑟 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ( ℎ ∘ 𝑔 ) ‘ 𝑟 ) ) ) ) |
| 43 |
14 42
|
jca |
⊢ ( ( ( ℎ : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ ∀ 𝑠 ∈ ( Vtx ‘ 𝑆 ) ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx 𝑠 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ℎ ‘ 𝑠 ) ) ) ) ∧ ( 𝑔 : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) ∧ ∀ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ( 𝑅 ISubGr ( 𝑅 ClNeighbVtx 𝑟 ) ) ≃𝑔𝑟 ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx ( 𝑔 ‘ 𝑟 ) ) ) ) ) → ( ( ℎ ∘ 𝑔 ) : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ ∀ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ( 𝑅 ISubGr ( 𝑅 ClNeighbVtx 𝑟 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ( ℎ ∘ 𝑔 ) ‘ 𝑟 ) ) ) ) ) |
| 44 |
|
f1oeq1 |
⊢ ( 𝑓 = ( ℎ ∘ 𝑔 ) → ( 𝑓 : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ↔ ( ℎ ∘ 𝑔 ) : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) ) |
| 45 |
|
fveq1 |
⊢ ( 𝑓 = ( ℎ ∘ 𝑔 ) → ( 𝑓 ‘ 𝑟 ) = ( ( ℎ ∘ 𝑔 ) ‘ 𝑟 ) ) |
| 46 |
45
|
oveq2d |
⊢ ( 𝑓 = ( ℎ ∘ 𝑔 ) → ( 𝑇 ClNeighbVtx ( 𝑓 ‘ 𝑟 ) ) = ( 𝑇 ClNeighbVtx ( ( ℎ ∘ 𝑔 ) ‘ 𝑟 ) ) ) |
| 47 |
46
|
oveq2d |
⊢ ( 𝑓 = ( ℎ ∘ 𝑔 ) → ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( 𝑓 ‘ 𝑟 ) ) ) = ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ( ℎ ∘ 𝑔 ) ‘ 𝑟 ) ) ) ) |
| 48 |
47
|
breq2d |
⊢ ( 𝑓 = ( ℎ ∘ 𝑔 ) → ( ( 𝑅 ISubGr ( 𝑅 ClNeighbVtx 𝑟 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( 𝑓 ‘ 𝑟 ) ) ) ↔ ( 𝑅 ISubGr ( 𝑅 ClNeighbVtx 𝑟 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ( ℎ ∘ 𝑔 ) ‘ 𝑟 ) ) ) ) ) |
| 49 |
48
|
ralbidv |
⊢ ( 𝑓 = ( ℎ ∘ 𝑔 ) → ( ∀ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ( 𝑅 ISubGr ( 𝑅 ClNeighbVtx 𝑟 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( 𝑓 ‘ 𝑟 ) ) ) ↔ ∀ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ( 𝑅 ISubGr ( 𝑅 ClNeighbVtx 𝑟 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ( ℎ ∘ 𝑔 ) ‘ 𝑟 ) ) ) ) ) |
| 50 |
44 49
|
anbi12d |
⊢ ( 𝑓 = ( ℎ ∘ 𝑔 ) → ( ( 𝑓 : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ ∀ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ( 𝑅 ISubGr ( 𝑅 ClNeighbVtx 𝑟 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( 𝑓 ‘ 𝑟 ) ) ) ) ↔ ( ( ℎ ∘ 𝑔 ) : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ ∀ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ( 𝑅 ISubGr ( 𝑅 ClNeighbVtx 𝑟 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ( ℎ ∘ 𝑔 ) ‘ 𝑟 ) ) ) ) ) ) |
| 51 |
12 43 50
|
spcedv |
⊢ ( ( ( ℎ : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ ∀ 𝑠 ∈ ( Vtx ‘ 𝑆 ) ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx 𝑠 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ℎ ‘ 𝑠 ) ) ) ) ∧ ( 𝑔 : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) ∧ ∀ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ( 𝑅 ISubGr ( 𝑅 ClNeighbVtx 𝑟 ) ) ≃𝑔𝑟 ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx ( 𝑔 ‘ 𝑟 ) ) ) ) ) → ∃ 𝑓 ( 𝑓 : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ ∀ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ( 𝑅 ISubGr ( 𝑅 ClNeighbVtx 𝑟 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( 𝑓 ‘ 𝑟 ) ) ) ) ) |
| 52 |
51
|
ex |
⊢ ( ( ℎ : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ ∀ 𝑠 ∈ ( Vtx ‘ 𝑆 ) ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx 𝑠 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ℎ ‘ 𝑠 ) ) ) ) → ( ( 𝑔 : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) ∧ ∀ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ( 𝑅 ISubGr ( 𝑅 ClNeighbVtx 𝑟 ) ) ≃𝑔𝑟 ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx ( 𝑔 ‘ 𝑟 ) ) ) ) → ∃ 𝑓 ( 𝑓 : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ ∀ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ( 𝑅 ISubGr ( 𝑅 ClNeighbVtx 𝑟 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( 𝑓 ‘ 𝑟 ) ) ) ) ) ) |
| 53 |
52
|
exlimiv |
⊢ ( ∃ ℎ ( ℎ : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ ∀ 𝑠 ∈ ( Vtx ‘ 𝑆 ) ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx 𝑠 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ℎ ‘ 𝑠 ) ) ) ) → ( ( 𝑔 : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) ∧ ∀ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ( 𝑅 ISubGr ( 𝑅 ClNeighbVtx 𝑟 ) ) ≃𝑔𝑟 ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx ( 𝑔 ‘ 𝑟 ) ) ) ) → ∃ 𝑓 ( 𝑓 : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ ∀ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ( 𝑅 ISubGr ( 𝑅 ClNeighbVtx 𝑟 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( 𝑓 ‘ 𝑟 ) ) ) ) ) ) |
| 54 |
53
|
com12 |
⊢ ( ( 𝑔 : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) ∧ ∀ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ( 𝑅 ISubGr ( 𝑅 ClNeighbVtx 𝑟 ) ) ≃𝑔𝑟 ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx ( 𝑔 ‘ 𝑟 ) ) ) ) → ( ∃ ℎ ( ℎ : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ ∀ 𝑠 ∈ ( Vtx ‘ 𝑆 ) ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx 𝑠 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ℎ ‘ 𝑠 ) ) ) ) → ∃ 𝑓 ( 𝑓 : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ ∀ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ( 𝑅 ISubGr ( 𝑅 ClNeighbVtx 𝑟 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( 𝑓 ‘ 𝑟 ) ) ) ) ) ) |
| 55 |
54
|
exlimiv |
⊢ ( ∃ 𝑔 ( 𝑔 : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) ∧ ∀ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ( 𝑅 ISubGr ( 𝑅 ClNeighbVtx 𝑟 ) ) ≃𝑔𝑟 ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx ( 𝑔 ‘ 𝑟 ) ) ) ) → ( ∃ ℎ ( ℎ : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ ∀ 𝑠 ∈ ( Vtx ‘ 𝑆 ) ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx 𝑠 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ℎ ‘ 𝑠 ) ) ) ) → ∃ 𝑓 ( 𝑓 : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ ∀ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ( 𝑅 ISubGr ( 𝑅 ClNeighbVtx 𝑟 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( 𝑓 ‘ 𝑟 ) ) ) ) ) ) |
| 56 |
55
|
imp |
⊢ ( ( ∃ 𝑔 ( 𝑔 : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) ∧ ∀ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ( 𝑅 ISubGr ( 𝑅 ClNeighbVtx 𝑟 ) ) ≃𝑔𝑟 ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx ( 𝑔 ‘ 𝑟 ) ) ) ) ∧ ∃ ℎ ( ℎ : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ ∀ 𝑠 ∈ ( Vtx ‘ 𝑆 ) ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx 𝑠 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ℎ ‘ 𝑠 ) ) ) ) ) → ∃ 𝑓 ( 𝑓 : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ ∀ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ( 𝑅 ISubGr ( 𝑅 ClNeighbVtx 𝑟 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( 𝑓 ‘ 𝑟 ) ) ) ) ) |
| 57 |
6 8 56
|
syl2an |
⊢ ( ( 𝑅 ≃𝑙𝑔𝑟 𝑆 ∧ 𝑆 ≃𝑙𝑔𝑟 𝑇 ) → ∃ 𝑓 ( 𝑓 : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ ∀ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ( 𝑅 ISubGr ( 𝑅 ClNeighbVtx 𝑟 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( 𝑓 ‘ 𝑟 ) ) ) ) ) |
| 58 |
57
|
adantr |
⊢ ( ( ( 𝑅 ≃𝑙𝑔𝑟 𝑆 ∧ 𝑆 ≃𝑙𝑔𝑟 𝑇 ) ∧ ( ( 𝑅 ∈ V ∧ 𝑆 ∈ V ) ∧ ( 𝑆 ∈ V ∧ 𝑇 ∈ V ) ) ) → ∃ 𝑓 ( 𝑓 : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ ∀ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ( 𝑅 ISubGr ( 𝑅 ClNeighbVtx 𝑟 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( 𝑓 ‘ 𝑟 ) ) ) ) ) |
| 59 |
4 7
|
dfgrlic2 |
⊢ ( ( 𝑅 ∈ V ∧ 𝑇 ∈ V ) → ( 𝑅 ≃𝑙𝑔𝑟 𝑇 ↔ ∃ 𝑓 ( 𝑓 : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ ∀ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ( 𝑅 ISubGr ( 𝑅 ClNeighbVtx 𝑟 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( 𝑓 ‘ 𝑟 ) ) ) ) ) ) |
| 60 |
59
|
ad2ant2rl |
⊢ ( ( ( 𝑅 ∈ V ∧ 𝑆 ∈ V ) ∧ ( 𝑆 ∈ V ∧ 𝑇 ∈ V ) ) → ( 𝑅 ≃𝑙𝑔𝑟 𝑇 ↔ ∃ 𝑓 ( 𝑓 : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ ∀ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ( 𝑅 ISubGr ( 𝑅 ClNeighbVtx 𝑟 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( 𝑓 ‘ 𝑟 ) ) ) ) ) ) |
| 61 |
60
|
adantl |
⊢ ( ( ( 𝑅 ≃𝑙𝑔𝑟 𝑆 ∧ 𝑆 ≃𝑙𝑔𝑟 𝑇 ) ∧ ( ( 𝑅 ∈ V ∧ 𝑆 ∈ V ) ∧ ( 𝑆 ∈ V ∧ 𝑇 ∈ V ) ) ) → ( 𝑅 ≃𝑙𝑔𝑟 𝑇 ↔ ∃ 𝑓 ( 𝑓 : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ ∀ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ( 𝑅 ISubGr ( 𝑅 ClNeighbVtx 𝑟 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( 𝑓 ‘ 𝑟 ) ) ) ) ) ) |
| 62 |
58 61
|
mpbird |
⊢ ( ( ( 𝑅 ≃𝑙𝑔𝑟 𝑆 ∧ 𝑆 ≃𝑙𝑔𝑟 𝑇 ) ∧ ( ( 𝑅 ∈ V ∧ 𝑆 ∈ V ) ∧ ( 𝑆 ∈ V ∧ 𝑇 ∈ V ) ) ) → 𝑅 ≃𝑙𝑔𝑟 𝑇 ) |
| 63 |
3 62
|
mpdan |
⊢ ( ( 𝑅 ≃𝑙𝑔𝑟 𝑆 ∧ 𝑆 ≃𝑙𝑔𝑟 𝑇 ) → 𝑅 ≃𝑙𝑔𝑟 𝑇 ) |