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 8992 |
. . . . . 6
⊢ ((𝑉 ∈ V ∧ 𝑊 ∈ V) → (𝑉 ≈ 𝑊 ↔ ∃𝑓 𝑓:𝑉–1-1-onto→𝑊)) |
7 | 5, 6 | mp1i 13 |
. . . . 5
⊢ ((𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph) → (𝑉 ≈ 𝑊 ↔ ∃𝑓 𝑓:𝑉–1-1-onto→𝑊)) |
8 | | usgruhgr 29217 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐻 ∈ USGraph → 𝐻 ∈
UHGraph) |
9 | 8 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph) → 𝐻 ∈
UHGraph) |
10 | 9 | 3ad2ant1 1132 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊 ∧ ∀𝑦 ∈ 𝑊 (𝐻 ISubGr (𝐻 ClNeighbVtx 𝑦)) ≃𝑔𝑟
(StarGr‘𝑁)) →
𝐻 ∈
UHGraph) |
11 | 3 | clnbgrssvtx 47755 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐻 ClNeighbVtx (𝑓‘𝑥)) ⊆ 𝑊 |
12 | 11 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊 ∧ ∀𝑦 ∈ 𝑊 (𝐻 ISubGr (𝐻 ClNeighbVtx 𝑦)) ≃𝑔𝑟
(StarGr‘𝑁)) ∧
𝑥 ∈ 𝑉) → (𝐻 ClNeighbVtx (𝑓‘𝑥)) ⊆ 𝑊) |
13 | 3 | isubgruhgr 47791 |
. . . . . . . . . . . . . . . . . 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 1133 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊 ∧ 𝑥 ∈ 𝑉) → 𝑓:𝑉⟶𝑊) |
17 | | simp3 1137 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊 ∧ 𝑥 ∈ 𝑉) → 𝑥 ∈ 𝑉) |
18 | 16, 17 | ffvelcdmd 7104 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊 ∧ 𝑥 ∈ 𝑉) → (𝑓‘𝑥) ∈ 𝑊) |
19 | | oveq2 7438 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 = (𝑓‘𝑥) → (𝐻 ClNeighbVtx 𝑦) = (𝐻 ClNeighbVtx (𝑓‘𝑥))) |
20 | 19 | oveq2d 7446 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 = (𝑓‘𝑥) → (𝐻 ISubGr (𝐻 ClNeighbVtx 𝑦)) = (𝐻 ISubGr (𝐻 ClNeighbVtx (𝑓‘𝑥)))) |
21 | 20 | breq1d 5157 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 = (𝑓‘𝑥) → ((𝐻 ISubGr (𝐻 ClNeighbVtx 𝑦)) ≃𝑔𝑟
(StarGr‘𝑁) ↔
(𝐻 ISubGr (𝐻 ClNeighbVtx (𝑓‘𝑥))) ≃𝑔𝑟
(StarGr‘𝑁))) |
22 | 21 | rspcv 3617 |
. . . . . . . . . . . . . . . . . . . . 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 1118 |
. . . . . . . . . . . . . . . . . . 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 1346 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊 ∧ ∀𝑦 ∈ 𝑊 (𝐻 ISubGr (𝐻 ClNeighbVtx 𝑦)) ≃𝑔𝑟
(StarGr‘𝑁)) ∧
𝑥 ∈ 𝑉) → (𝐻 ISubGr (𝐻 ClNeighbVtx (𝑓‘𝑥))) ≃𝑔𝑟
(StarGr‘𝑁)) |
27 | | gricsym 47827 |
. . . . . . . . . . . . . . . . 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 47829 |
. . . . . . . . . . . . . . 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 3164 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊 ∧ ∀𝑦 ∈ 𝑊 (𝐻 ISubGr (𝐻 ClNeighbVtx 𝑦)) ≃𝑔𝑟
(StarGr‘𝑁)) →
(∀𝑥 ∈ 𝑉 (𝐺 ISubGr (𝐺 ClNeighbVtx 𝑥)) ≃𝑔𝑟
(StarGr‘𝑁) →
∀𝑥 ∈ 𝑉 (𝐺 ISubGr (𝐺 ClNeighbVtx 𝑥)) ≃𝑔𝑟
(𝐻 ISubGr (𝐻 ClNeighbVtx (𝑓‘𝑥))))) |
34 | 33 | 3exp 1118 |
. . . . . . . . . . 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 1914 |
. . . . . . 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 1116 |
. . 3
⊢ ((𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph ∧ 𝑉 ≈ 𝑊) → ((∀𝑥 ∈ 𝑉 (𝐺 ISubGr (𝐺 ClNeighbVtx 𝑥)) ≃𝑔𝑟
(StarGr‘𝑁) ∧
∀𝑦 ∈ 𝑊 (𝐻 ISubGr (𝐻 ClNeighbVtx 𝑦)) ≃𝑔𝑟
(StarGr‘𝑁)) →
∃𝑓(𝑓:𝑉–1-1-onto→𝑊 ∧ ∀𝑥 ∈ 𝑉 (𝐺 ISubGr (𝐺 ClNeighbVtx 𝑥)) ≃𝑔𝑟
(𝐻 ISubGr (𝐻 ClNeighbVtx (𝑓‘𝑥)))))) |
43 | 42 | 3impib 1115 |
. 2
⊢ (((𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph ∧ 𝑉 ≈ 𝑊) ∧ ∀𝑥 ∈ 𝑉 (𝐺 ISubGr (𝐺 ClNeighbVtx 𝑥)) ≃𝑔𝑟
(StarGr‘𝑁) ∧
∀𝑦 ∈ 𝑊 (𝐻 ISubGr (𝐻 ClNeighbVtx 𝑦)) ≃𝑔𝑟
(StarGr‘𝑁)) →
∃𝑓(𝑓:𝑉–1-1-onto→𝑊 ∧ ∀𝑥 ∈ 𝑉 (𝐺 ISubGr (𝐺 ClNeighbVtx 𝑥)) ≃𝑔𝑟
(𝐻 ISubGr (𝐻 ClNeighbVtx (𝑓‘𝑥))))) |
44 | 1, 3 | dfgrlic2 47903 |
. . . 4
⊢ ((𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph) → (𝐺
≃𝑙𝑔𝑟 𝐻 ↔ ∃𝑓(𝑓:𝑉–1-1-onto→𝑊 ∧ ∀𝑥 ∈ 𝑉 (𝐺 ISubGr (𝐺 ClNeighbVtx 𝑥)) ≃𝑔𝑟
(𝐻 ISubGr (𝐻 ClNeighbVtx (𝑓‘𝑥)))))) |
45 | 44 | 3adant3 1131 |
. . 3
⊢ ((𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph ∧ 𝑉 ≈ 𝑊) → (𝐺
≃𝑙𝑔𝑟 𝐻 ↔ ∃𝑓(𝑓:𝑉–1-1-onto→𝑊 ∧ ∀𝑥 ∈ 𝑉 (𝐺 ISubGr (𝐺 ClNeighbVtx 𝑥)) ≃𝑔𝑟
(𝐻 ISubGr (𝐻 ClNeighbVtx (𝑓‘𝑥)))))) |
46 | 45 | 3ad2ant1 1132 |
. 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‘𝑁)) →
𝐺
≃𝑙𝑔𝑟 𝐻) |