| Step | Hyp | Ref
| Expression |
| 1 | | clnbgr3stgrgrlic.v |
. . . . . . . 8
⊢ 𝑉 = (Vtx‘𝐺) |
| 2 | 1 | fvexi 6920 |
. . . . . . 7
⊢ 𝑉 ∈ V |
| 3 | | clnbgr3stgrgrlic.w |
. . . . . . . 8
⊢ 𝑊 = (Vtx‘𝐻) |
| 4 | 3 | fvexi 6920 |
. . . . . . 7
⊢ 𝑊 ∈ V |
| 5 | 2, 4 | pm3.2i 470 |
. . . . . 6
⊢ (𝑉 ∈ V ∧ 𝑊 ∈ V) |
| 6 | | breng 8994 |
. . . . . 6
⊢ ((𝑉 ∈ V ∧ 𝑊 ∈ V) → (𝑉 ≈ 𝑊 ↔ ∃𝑓 𝑓:𝑉–1-1-onto→𝑊)) |
| 7 | 5, 6 | mp1i 13 |
. . . . 5
⊢ ((𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph) → (𝑉 ≈ 𝑊 ↔ ∃𝑓 𝑓:𝑉–1-1-onto→𝑊)) |
| 8 | | usgruhgr 29203 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐻 ∈ USGraph → 𝐻 ∈
UHGraph) |
| 9 | 8 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph) → 𝐻 ∈
UHGraph) |
| 10 | 9 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊 ∧ ∀𝑦 ∈ 𝑊 (𝐻 ISubGr (𝐻 ClNeighbVtx 𝑦)) ≃𝑔𝑟
(StarGr‘𝑁)) →
𝐻 ∈
UHGraph) |
| 11 | 3 | clnbgrssvtx 47818 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐻 ClNeighbVtx (𝑓‘𝑥)) ⊆ 𝑊 |
| 12 | 11 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊 ∧ ∀𝑦 ∈ 𝑊 (𝐻 ISubGr (𝐻 ClNeighbVtx 𝑦)) ≃𝑔𝑟
(StarGr‘𝑁)) ∧
𝑥 ∈ 𝑉) → (𝐻 ClNeighbVtx (𝑓‘𝑥)) ⊆ 𝑊) |
| 13 | 3 | isubgruhgr 47854 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐻 ∈ UHGraph ∧ (𝐻 ClNeighbVtx (𝑓‘𝑥)) ⊆ 𝑊) → (𝐻 ISubGr (𝐻 ClNeighbVtx (𝑓‘𝑥))) ∈ UHGraph) |
| 14 | 10, 12, 13 | syl2an2r 685 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊 ∧ ∀𝑦 ∈ 𝑊 (𝐻 ISubGr (𝐻 ClNeighbVtx 𝑦)) ≃𝑔𝑟
(StarGr‘𝑁)) ∧
𝑥 ∈ 𝑉) → (𝐻 ISubGr (𝐻 ClNeighbVtx (𝑓‘𝑥))) ∈ UHGraph) |
| 15 | | f1of 6848 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑓:𝑉–1-1-onto→𝑊 → 𝑓:𝑉⟶𝑊) |
| 16 | 15 | 3ad2ant2 1135 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊 ∧ 𝑥 ∈ 𝑉) → 𝑓:𝑉⟶𝑊) |
| 17 | | simp3 1139 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊 ∧ 𝑥 ∈ 𝑉) → 𝑥 ∈ 𝑉) |
| 18 | 16, 17 | ffvelcdmd 7105 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊 ∧ 𝑥 ∈ 𝑉) → (𝑓‘𝑥) ∈ 𝑊) |
| 19 | | oveq2 7439 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 = (𝑓‘𝑥) → (𝐻 ClNeighbVtx 𝑦) = (𝐻 ClNeighbVtx (𝑓‘𝑥))) |
| 20 | 19 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 = (𝑓‘𝑥) → (𝐻 ISubGr (𝐻 ClNeighbVtx 𝑦)) = (𝐻 ISubGr (𝐻 ClNeighbVtx (𝑓‘𝑥)))) |
| 21 | 20 | breq1d 5153 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 = (𝑓‘𝑥) → ((𝐻 ISubGr (𝐻 ClNeighbVtx 𝑦)) ≃𝑔𝑟
(StarGr‘𝑁) ↔
(𝐻 ISubGr (𝐻 ClNeighbVtx (𝑓‘𝑥))) ≃𝑔𝑟
(StarGr‘𝑁))) |
| 22 | 21 | rspcv 3618 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑓‘𝑥) ∈ 𝑊 → (∀𝑦 ∈ 𝑊 (𝐻 ISubGr (𝐻 ClNeighbVtx 𝑦)) ≃𝑔𝑟
(StarGr‘𝑁) →
(𝐻 ISubGr (𝐻 ClNeighbVtx (𝑓‘𝑥))) ≃𝑔𝑟
(StarGr‘𝑁))) |
| 23 | 18, 22 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊 ∧ 𝑥 ∈ 𝑉) → (∀𝑦 ∈ 𝑊 (𝐻 ISubGr (𝐻 ClNeighbVtx 𝑦)) ≃𝑔𝑟
(StarGr‘𝑁) →
(𝐻 ISubGr (𝐻 ClNeighbVtx (𝑓‘𝑥))) ≃𝑔𝑟
(StarGr‘𝑁))) |
| 24 | 23 | 3exp 1120 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph) → (𝑓:𝑉–1-1-onto→𝑊 → (𝑥 ∈ 𝑉 → (∀𝑦 ∈ 𝑊 (𝐻 ISubGr (𝐻 ClNeighbVtx 𝑦)) ≃𝑔𝑟
(StarGr‘𝑁) →
(𝐻 ISubGr (𝐻 ClNeighbVtx (𝑓‘𝑥))) ≃𝑔𝑟
(StarGr‘𝑁))))) |
| 25 | 24 | com34 91 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph) → (𝑓:𝑉–1-1-onto→𝑊 → (∀𝑦 ∈ 𝑊 (𝐻 ISubGr (𝐻 ClNeighbVtx 𝑦)) ≃𝑔𝑟
(StarGr‘𝑁) →
(𝑥 ∈ 𝑉 → (𝐻 ISubGr (𝐻 ClNeighbVtx (𝑓‘𝑥))) ≃𝑔𝑟
(StarGr‘𝑁))))) |
| 26 | 25 | 3imp1 1348 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊 ∧ ∀𝑦 ∈ 𝑊 (𝐻 ISubGr (𝐻 ClNeighbVtx 𝑦)) ≃𝑔𝑟
(StarGr‘𝑁)) ∧
𝑥 ∈ 𝑉) → (𝐻 ISubGr (𝐻 ClNeighbVtx (𝑓‘𝑥))) ≃𝑔𝑟
(StarGr‘𝑁)) |
| 27 | | gricsym 47890 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐻 ISubGr (𝐻 ClNeighbVtx (𝑓‘𝑥))) ∈ UHGraph → ((𝐻 ISubGr (𝐻 ClNeighbVtx (𝑓‘𝑥))) ≃𝑔𝑟
(StarGr‘𝑁) →
(StarGr‘𝑁)
≃𝑔𝑟 (𝐻 ISubGr (𝐻 ClNeighbVtx (𝑓‘𝑥))))) |
| 28 | 14, 26, 27 | sylc 65 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊 ∧ ∀𝑦 ∈ 𝑊 (𝐻 ISubGr (𝐻 ClNeighbVtx 𝑦)) ≃𝑔𝑟
(StarGr‘𝑁)) ∧
𝑥 ∈ 𝑉) → (StarGr‘𝑁) ≃𝑔𝑟
(𝐻 ISubGr (𝐻 ClNeighbVtx (𝑓‘𝑥)))) |
| 29 | 28 | anim1ci 616 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐺 ∈
USGraph ∧ 𝐻 ∈
USGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊 ∧ ∀𝑦 ∈ 𝑊 (𝐻 ISubGr (𝐻 ClNeighbVtx 𝑦)) ≃𝑔𝑟
(StarGr‘𝑁)) ∧
𝑥 ∈ 𝑉) ∧ (𝐺 ISubGr (𝐺 ClNeighbVtx 𝑥)) ≃𝑔𝑟
(StarGr‘𝑁)) →
((𝐺 ISubGr (𝐺 ClNeighbVtx 𝑥)) ≃𝑔𝑟
(StarGr‘𝑁) ∧
(StarGr‘𝑁)
≃𝑔𝑟 (𝐻 ISubGr (𝐻 ClNeighbVtx (𝑓‘𝑥))))) |
| 30 | | grictr 47892 |
. . . . . . . . . . . . . . 15
⊢ (((𝐺 ISubGr (𝐺 ClNeighbVtx 𝑥)) ≃𝑔𝑟
(StarGr‘𝑁) ∧
(StarGr‘𝑁)
≃𝑔𝑟 (𝐻 ISubGr (𝐻 ClNeighbVtx (𝑓‘𝑥)))) → (𝐺 ISubGr (𝐺 ClNeighbVtx 𝑥)) ≃𝑔𝑟
(𝐻 ISubGr (𝐻 ClNeighbVtx (𝑓‘𝑥)))) |
| 31 | 29, 30 | syl 17 |
. . . . . . . . . . . . . 14
⊢
(((((𝐺 ∈
USGraph ∧ 𝐻 ∈
USGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊 ∧ ∀𝑦 ∈ 𝑊 (𝐻 ISubGr (𝐻 ClNeighbVtx 𝑦)) ≃𝑔𝑟
(StarGr‘𝑁)) ∧
𝑥 ∈ 𝑉) ∧ (𝐺 ISubGr (𝐺 ClNeighbVtx 𝑥)) ≃𝑔𝑟
(StarGr‘𝑁)) →
(𝐺 ISubGr (𝐺 ClNeighbVtx 𝑥)) ≃𝑔𝑟
(𝐻 ISubGr (𝐻 ClNeighbVtx (𝑓‘𝑥)))) |
| 32 | 31 | ex 412 |
. . . . . . . . . . . . 13
⊢ ((((𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊 ∧ ∀𝑦 ∈ 𝑊 (𝐻 ISubGr (𝐻 ClNeighbVtx 𝑦)) ≃𝑔𝑟
(StarGr‘𝑁)) ∧
𝑥 ∈ 𝑉) → ((𝐺 ISubGr (𝐺 ClNeighbVtx 𝑥)) ≃𝑔𝑟
(StarGr‘𝑁) →
(𝐺 ISubGr (𝐺 ClNeighbVtx 𝑥)) ≃𝑔𝑟
(𝐻 ISubGr (𝐻 ClNeighbVtx (𝑓‘𝑥))))) |
| 33 | 32 | ralimdva 3167 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊 ∧ ∀𝑦 ∈ 𝑊 (𝐻 ISubGr (𝐻 ClNeighbVtx 𝑦)) ≃𝑔𝑟
(StarGr‘𝑁)) →
(∀𝑥 ∈ 𝑉 (𝐺 ISubGr (𝐺 ClNeighbVtx 𝑥)) ≃𝑔𝑟
(StarGr‘𝑁) →
∀𝑥 ∈ 𝑉 (𝐺 ISubGr (𝐺 ClNeighbVtx 𝑥)) ≃𝑔𝑟
(𝐻 ISubGr (𝐻 ClNeighbVtx (𝑓‘𝑥))))) |
| 34 | 33 | 3exp 1120 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph) → (𝑓:𝑉–1-1-onto→𝑊 → (∀𝑦 ∈ 𝑊 (𝐻 ISubGr (𝐻 ClNeighbVtx 𝑦)) ≃𝑔𝑟
(StarGr‘𝑁) →
(∀𝑥 ∈ 𝑉 (𝐺 ISubGr (𝐺 ClNeighbVtx 𝑥)) ≃𝑔𝑟
(StarGr‘𝑁) →
∀𝑥 ∈ 𝑉 (𝐺 ISubGr (𝐺 ClNeighbVtx 𝑥)) ≃𝑔𝑟
(𝐻 ISubGr (𝐻 ClNeighbVtx (𝑓‘𝑥))))))) |
| 35 | 34 | com24 95 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph) →
(∀𝑥 ∈ 𝑉 (𝐺 ISubGr (𝐺 ClNeighbVtx 𝑥)) ≃𝑔𝑟
(StarGr‘𝑁) →
(∀𝑦 ∈ 𝑊 (𝐻 ISubGr (𝐻 ClNeighbVtx 𝑦)) ≃𝑔𝑟
(StarGr‘𝑁) →
(𝑓:𝑉–1-1-onto→𝑊 → ∀𝑥 ∈ 𝑉 (𝐺 ISubGr (𝐺 ClNeighbVtx 𝑥)) ≃𝑔𝑟
(𝐻 ISubGr (𝐻 ClNeighbVtx (𝑓‘𝑥))))))) |
| 36 | 35 | imp32 418 |
. . . . . . . . 9
⊢ (((𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph) ∧
(∀𝑥 ∈ 𝑉 (𝐺 ISubGr (𝐺 ClNeighbVtx 𝑥)) ≃𝑔𝑟
(StarGr‘𝑁) ∧
∀𝑦 ∈ 𝑊 (𝐻 ISubGr (𝐻 ClNeighbVtx 𝑦)) ≃𝑔𝑟
(StarGr‘𝑁))) →
(𝑓:𝑉–1-1-onto→𝑊 → ∀𝑥 ∈ 𝑉 (𝐺 ISubGr (𝐺 ClNeighbVtx 𝑥)) ≃𝑔𝑟
(𝐻 ISubGr (𝐻 ClNeighbVtx (𝑓‘𝑥))))) |
| 37 | 36 | ancld 550 |
. . . . . . . 8
⊢ (((𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph) ∧
(∀𝑥 ∈ 𝑉 (𝐺 ISubGr (𝐺 ClNeighbVtx 𝑥)) ≃𝑔𝑟
(StarGr‘𝑁) ∧
∀𝑦 ∈ 𝑊 (𝐻 ISubGr (𝐻 ClNeighbVtx 𝑦)) ≃𝑔𝑟
(StarGr‘𝑁))) →
(𝑓:𝑉–1-1-onto→𝑊 → (𝑓:𝑉–1-1-onto→𝑊 ∧ ∀𝑥 ∈ 𝑉 (𝐺 ISubGr (𝐺 ClNeighbVtx 𝑥)) ≃𝑔𝑟
(𝐻 ISubGr (𝐻 ClNeighbVtx (𝑓‘𝑥)))))) |
| 38 | 37 | eximdv 1917 |
. . . . . . 7
⊢ (((𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph) ∧
(∀𝑥 ∈ 𝑉 (𝐺 ISubGr (𝐺 ClNeighbVtx 𝑥)) ≃𝑔𝑟
(StarGr‘𝑁) ∧
∀𝑦 ∈ 𝑊 (𝐻 ISubGr (𝐻 ClNeighbVtx 𝑦)) ≃𝑔𝑟
(StarGr‘𝑁))) →
(∃𝑓 𝑓:𝑉–1-1-onto→𝑊 → ∃𝑓(𝑓:𝑉–1-1-onto→𝑊 ∧ ∀𝑥 ∈ 𝑉 (𝐺 ISubGr (𝐺 ClNeighbVtx 𝑥)) ≃𝑔𝑟
(𝐻 ISubGr (𝐻 ClNeighbVtx (𝑓‘𝑥)))))) |
| 39 | 38 | ex 412 |
. . . . . 6
⊢ ((𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph) →
((∀𝑥 ∈ 𝑉 (𝐺 ISubGr (𝐺 ClNeighbVtx 𝑥)) ≃𝑔𝑟
(StarGr‘𝑁) ∧
∀𝑦 ∈ 𝑊 (𝐻 ISubGr (𝐻 ClNeighbVtx 𝑦)) ≃𝑔𝑟
(StarGr‘𝑁)) →
(∃𝑓 𝑓:𝑉–1-1-onto→𝑊 → ∃𝑓(𝑓:𝑉–1-1-onto→𝑊 ∧ ∀𝑥 ∈ 𝑉 (𝐺 ISubGr (𝐺 ClNeighbVtx 𝑥)) ≃𝑔𝑟
(𝐻 ISubGr (𝐻 ClNeighbVtx (𝑓‘𝑥))))))) |
| 40 | 39 | com23 86 |
. . . . 5
⊢ ((𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph) →
(∃𝑓 𝑓:𝑉–1-1-onto→𝑊 → ((∀𝑥 ∈ 𝑉 (𝐺 ISubGr (𝐺 ClNeighbVtx 𝑥)) ≃𝑔𝑟
(StarGr‘𝑁) ∧
∀𝑦 ∈ 𝑊 (𝐻 ISubGr (𝐻 ClNeighbVtx 𝑦)) ≃𝑔𝑟
(StarGr‘𝑁)) →
∃𝑓(𝑓:𝑉–1-1-onto→𝑊 ∧ ∀𝑥 ∈ 𝑉 (𝐺 ISubGr (𝐺 ClNeighbVtx 𝑥)) ≃𝑔𝑟
(𝐻 ISubGr (𝐻 ClNeighbVtx (𝑓‘𝑥))))))) |
| 41 | 7, 40 | sylbid 240 |
. . . 4
⊢ ((𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph) → (𝑉 ≈ 𝑊 → ((∀𝑥 ∈ 𝑉 (𝐺 ISubGr (𝐺 ClNeighbVtx 𝑥)) ≃𝑔𝑟
(StarGr‘𝑁) ∧
∀𝑦 ∈ 𝑊 (𝐻 ISubGr (𝐻 ClNeighbVtx 𝑦)) ≃𝑔𝑟
(StarGr‘𝑁)) →
∃𝑓(𝑓:𝑉–1-1-onto→𝑊 ∧ ∀𝑥 ∈ 𝑉 (𝐺 ISubGr (𝐺 ClNeighbVtx 𝑥)) ≃𝑔𝑟
(𝐻 ISubGr (𝐻 ClNeighbVtx (𝑓‘𝑥))))))) |
| 42 | 41 | 3impia 1118 |
. . 3
⊢ ((𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph ∧ 𝑉 ≈ 𝑊) → ((∀𝑥 ∈ 𝑉 (𝐺 ISubGr (𝐺 ClNeighbVtx 𝑥)) ≃𝑔𝑟
(StarGr‘𝑁) ∧
∀𝑦 ∈ 𝑊 (𝐻 ISubGr (𝐻 ClNeighbVtx 𝑦)) ≃𝑔𝑟
(StarGr‘𝑁)) →
∃𝑓(𝑓:𝑉–1-1-onto→𝑊 ∧ ∀𝑥 ∈ 𝑉 (𝐺 ISubGr (𝐺 ClNeighbVtx 𝑥)) ≃𝑔𝑟
(𝐻 ISubGr (𝐻 ClNeighbVtx (𝑓‘𝑥)))))) |
| 43 | 42 | 3impib 1117 |
. 2
⊢ (((𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph ∧ 𝑉 ≈ 𝑊) ∧ ∀𝑥 ∈ 𝑉 (𝐺 ISubGr (𝐺 ClNeighbVtx 𝑥)) ≃𝑔𝑟
(StarGr‘𝑁) ∧
∀𝑦 ∈ 𝑊 (𝐻 ISubGr (𝐻 ClNeighbVtx 𝑦)) ≃𝑔𝑟
(StarGr‘𝑁)) →
∃𝑓(𝑓:𝑉–1-1-onto→𝑊 ∧ ∀𝑥 ∈ 𝑉 (𝐺 ISubGr (𝐺 ClNeighbVtx 𝑥)) ≃𝑔𝑟
(𝐻 ISubGr (𝐻 ClNeighbVtx (𝑓‘𝑥))))) |
| 44 | 1, 3 | dfgrlic2 47968 |
. . . 4
⊢ ((𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph) → (𝐺
≃𝑙𝑔𝑟 𝐻 ↔ ∃𝑓(𝑓:𝑉–1-1-onto→𝑊 ∧ ∀𝑥 ∈ 𝑉 (𝐺 ISubGr (𝐺 ClNeighbVtx 𝑥)) ≃𝑔𝑟
(𝐻 ISubGr (𝐻 ClNeighbVtx (𝑓‘𝑥)))))) |
| 45 | 44 | 3adant3 1133 |
. . 3
⊢ ((𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph ∧ 𝑉 ≈ 𝑊) → (𝐺
≃𝑙𝑔𝑟 𝐻 ↔ ∃𝑓(𝑓:𝑉–1-1-onto→𝑊 ∧ ∀𝑥 ∈ 𝑉 (𝐺 ISubGr (𝐺 ClNeighbVtx 𝑥)) ≃𝑔𝑟
(𝐻 ISubGr (𝐻 ClNeighbVtx (𝑓‘𝑥)))))) |
| 46 | 45 | 3ad2ant1 1134 |
. 2
⊢ (((𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph ∧ 𝑉 ≈ 𝑊) ∧ ∀𝑥 ∈ 𝑉 (𝐺 ISubGr (𝐺 ClNeighbVtx 𝑥)) ≃𝑔𝑟
(StarGr‘𝑁) ∧
∀𝑦 ∈ 𝑊 (𝐻 ISubGr (𝐻 ClNeighbVtx 𝑦)) ≃𝑔𝑟
(StarGr‘𝑁)) →
(𝐺
≃𝑙𝑔𝑟 𝐻 ↔ ∃𝑓(𝑓:𝑉–1-1-onto→𝑊 ∧ ∀𝑥 ∈ 𝑉 (𝐺 ISubGr (𝐺 ClNeighbVtx 𝑥)) ≃𝑔𝑟
(𝐻 ISubGr (𝐻 ClNeighbVtx (𝑓‘𝑥)))))) |
| 47 | 43, 46 | mpbird 257 |
1
⊢ (((𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph ∧ 𝑉 ≈ 𝑊) ∧ ∀𝑥 ∈ 𝑉 (𝐺 ISubGr (𝐺 ClNeighbVtx 𝑥)) ≃𝑔𝑟
(StarGr‘𝑁) ∧
∀𝑦 ∈ 𝑊 (𝐻 ISubGr (𝐻 ClNeighbVtx 𝑦)) ≃𝑔𝑟
(StarGr‘𝑁)) →
𝐺
≃𝑙𝑔𝑟 𝐻) |