| Step | Hyp | Ref
| Expression |
| 1 | | isubgr3stgr.h |
. . 3
⊢ 𝐻 = (𝑖 ∈ 𝐼 ↦ (𝐹 “ 𝑖)) |
| 2 | | imaeq2 6074 |
. . . 4
⊢ (𝑖 = 𝑘 → (𝐹 “ 𝑖) = (𝐹 “ 𝑘)) |
| 3 | 2 | cbvmptv 5255 |
. . 3
⊢ (𝑖 ∈ 𝐼 ↦ (𝐹 “ 𝑖)) = (𝑘 ∈ 𝐼 ↦ (𝐹 “ 𝑘)) |
| 4 | 1, 3 | eqtri 2765 |
. 2
⊢ 𝐻 = (𝑘 ∈ 𝐼 ↦ (𝐹 “ 𝑘)) |
| 5 | | f1of 6848 |
. . . . 5
⊢ (𝐹:𝐶–1-1-onto→𝑊 → 𝐹:𝐶⟶𝑊) |
| 6 | 5 | ad2antrl 728 |
. . . 4
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ ((♯‘𝑈) = 𝑁 ∧ ∀𝑥 ∈ 𝑈 ∀𝑦 ∈ 𝑈 {𝑥, 𝑦} ∉ 𝐸)) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) → 𝐹:𝐶⟶𝑊) |
| 7 | | isubgr3stgr.v |
. . . . 5
⊢ 𝑉 = (Vtx‘𝐺) |
| 8 | | isubgr3stgr.u |
. . . . 5
⊢ 𝑈 = (𝐺 NeighbVtx 𝑋) |
| 9 | | isubgr3stgr.c |
. . . . 5
⊢ 𝐶 = (𝐺 ClNeighbVtx 𝑋) |
| 10 | | isubgr3stgr.n |
. . . . 5
⊢ 𝑁 ∈
ℕ0 |
| 11 | | isubgr3stgr.s |
. . . . 5
⊢ 𝑆 = (StarGr‘𝑁) |
| 12 | | isubgr3stgr.w |
. . . . 5
⊢ 𝑊 = (Vtx‘𝑆) |
| 13 | | isubgr3stgr.e |
. . . . 5
⊢ 𝐸 = (Edg‘𝐺) |
| 14 | | isubgr3stgr.i |
. . . . 5
⊢ 𝐼 = (Edg‘(𝐺 ISubGr 𝐶)) |
| 15 | 7, 8, 9, 10, 11, 12, 13, 14, 1 | isubgr3stgrlem5 47937 |
. . . 4
⊢ ((𝐹:𝐶⟶𝑊 ∧ 𝑘 ∈ 𝐼) → (𝐻‘𝑘) = (𝐹 “ 𝑘)) |
| 16 | 6, 15 | sylan 580 |
. . 3
⊢
(((((𝐺 ∈
USGraph ∧ 𝑋 ∈
𝑉) ∧
((♯‘𝑈) = 𝑁 ∧ ∀𝑥 ∈ 𝑈 ∀𝑦 ∈ 𝑈 {𝑥, 𝑦} ∉ 𝐸)) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑘 ∈ 𝐼) → (𝐻‘𝑘) = (𝐹 “ 𝑘)) |
| 17 | 7, 8, 9, 10, 11, 12, 13, 14, 1 | isubgr3stgrlem6 47938 |
. . . 4
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ ((♯‘𝑈) = 𝑁 ∧ ∀𝑥 ∈ 𝑈 ∀𝑦 ∈ 𝑈 {𝑥, 𝑦} ∉ 𝐸)) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) → 𝐻:𝐼⟶(Edg‘(StarGr‘𝑁))) |
| 18 | 17 | ffvelcdmda 7104 |
. . 3
⊢
(((((𝐺 ∈
USGraph ∧ 𝑋 ∈
𝑉) ∧
((♯‘𝑈) = 𝑁 ∧ ∀𝑥 ∈ 𝑈 ∀𝑦 ∈ 𝑈 {𝑥, 𝑦} ∉ 𝐸)) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑘 ∈ 𝐼) → (𝐻‘𝑘) ∈ (Edg‘(StarGr‘𝑁))) |
| 19 | 16, 18 | eqeltrrd 2842 |
. 2
⊢
(((((𝐺 ∈
USGraph ∧ 𝑋 ∈
𝑉) ∧
((♯‘𝑈) = 𝑁 ∧ ∀𝑥 ∈ 𝑈 ∀𝑦 ∈ 𝑈 {𝑥, 𝑦} ∉ 𝐸)) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑘 ∈ 𝐼) → (𝐹 “ 𝑘) ∈ (Edg‘(StarGr‘𝑁))) |
| 20 | 7, 8, 9, 10, 11, 12, 13, 14, 1 | isubgr3stgrlem7 47939 |
. . 3
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0) ∧ 𝑗 ∈ (Edg‘(StarGr‘𝑁))) → (◡𝐹 “ 𝑗) ∈ 𝐼) |
| 21 | 20 | ad4ant134 1175 |
. 2
⊢
(((((𝐺 ∈
USGraph ∧ 𝑋 ∈
𝑉) ∧
((♯‘𝑈) = 𝑁 ∧ ∀𝑥 ∈ 𝑈 ∀𝑦 ∈ 𝑈 {𝑥, 𝑦} ∉ 𝐸)) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑗 ∈ (Edg‘(StarGr‘𝑁))) → (◡𝐹 “ 𝑗) ∈ 𝐼) |
| 22 | | f1ofo 6855 |
. . . . . 6
⊢ (𝐹:𝐶–1-1-onto→𝑊 → 𝐹:𝐶–onto→𝑊) |
| 23 | 22 | ad2antrl 728 |
. . . . 5
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ ((♯‘𝑈) = 𝑁 ∧ ∀𝑥 ∈ 𝑈 ∀𝑦 ∈ 𝑈 {𝑥, 𝑦} ∉ 𝐸)) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) → 𝐹:𝐶–onto→𝑊) |
| 24 | | stgrusgra 47926 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ (StarGr‘𝑁)
∈ USGraph) |
| 25 | 10, 24 | mp1i 13 |
. . . . . 6
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ ((♯‘𝑈) = 𝑁 ∧ ∀𝑥 ∈ 𝑈 ∀𝑦 ∈ 𝑈 {𝑥, 𝑦} ∉ 𝐸)) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) → (StarGr‘𝑁) ∈
USGraph) |
| 26 | | simpr 484 |
. . . . . 6
⊢ ((𝑘 ∈ 𝐼 ∧ 𝑗 ∈ (Edg‘(StarGr‘𝑁))) → 𝑗 ∈ (Edg‘(StarGr‘𝑁))) |
| 27 | 11 | fveq2i 6909 |
. . . . . . . . 9
⊢
(Vtx‘𝑆) =
(Vtx‘(StarGr‘𝑁)) |
| 28 | 12, 27 | eqtri 2765 |
. . . . . . . 8
⊢ 𝑊 =
(Vtx‘(StarGr‘𝑁)) |
| 29 | | eqid 2737 |
. . . . . . . 8
⊢
(Edg‘(StarGr‘𝑁)) = (Edg‘(StarGr‘𝑁)) |
| 30 | 28, 29 | edgssv2 29215 |
. . . . . . 7
⊢
(((StarGr‘𝑁)
∈ USGraph ∧ 𝑗
∈ (Edg‘(StarGr‘𝑁))) → (𝑗 ⊆ 𝑊 ∧ (♯‘𝑗) = 2)) |
| 31 | 30 | simpld 494 |
. . . . . 6
⊢
(((StarGr‘𝑁)
∈ USGraph ∧ 𝑗
∈ (Edg‘(StarGr‘𝑁))) → 𝑗 ⊆ 𝑊) |
| 32 | 25, 26, 31 | syl2an 596 |
. . . . 5
⊢
(((((𝐺 ∈
USGraph ∧ 𝑋 ∈
𝑉) ∧
((♯‘𝑈) = 𝑁 ∧ ∀𝑥 ∈ 𝑈 ∀𝑦 ∈ 𝑈 {𝑥, 𝑦} ∉ 𝐸)) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ (𝑘 ∈ 𝐼 ∧ 𝑗 ∈ (Edg‘(StarGr‘𝑁)))) → 𝑗 ⊆ 𝑊) |
| 33 | | foimacnv 6865 |
. . . . 5
⊢ ((𝐹:𝐶–onto→𝑊 ∧ 𝑗 ⊆ 𝑊) → (𝐹 “ (◡𝐹 “ 𝑗)) = 𝑗) |
| 34 | 23, 32, 33 | syl2an2r 685 |
. . . 4
⊢
(((((𝐺 ∈
USGraph ∧ 𝑋 ∈
𝑉) ∧
((♯‘𝑈) = 𝑁 ∧ ∀𝑥 ∈ 𝑈 ∀𝑦 ∈ 𝑈 {𝑥, 𝑦} ∉ 𝐸)) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ (𝑘 ∈ 𝐼 ∧ 𝑗 ∈ (Edg‘(StarGr‘𝑁)))) → (𝐹 “ (◡𝐹 “ 𝑗)) = 𝑗) |
| 35 | | imaeq2 6074 |
. . . . 5
⊢ (𝑘 = (◡𝐹 “ 𝑗) → (𝐹 “ 𝑘) = (𝐹 “ (◡𝐹 “ 𝑗))) |
| 36 | 35 | eqcomd 2743 |
. . . 4
⊢ (𝑘 = (◡𝐹 “ 𝑗) → (𝐹 “ (◡𝐹 “ 𝑗)) = (𝐹 “ 𝑘)) |
| 37 | 34, 36 | sylan9req 2798 |
. . 3
⊢
((((((𝐺 ∈
USGraph ∧ 𝑋 ∈
𝑉) ∧
((♯‘𝑈) = 𝑁 ∧ ∀𝑥 ∈ 𝑈 ∀𝑦 ∈ 𝑈 {𝑥, 𝑦} ∉ 𝐸)) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ (𝑘 ∈ 𝐼 ∧ 𝑗 ∈ (Edg‘(StarGr‘𝑁)))) ∧ 𝑘 = (◡𝐹 “ 𝑗)) → 𝑗 = (𝐹 “ 𝑘)) |
| 38 | | imaeq2 6074 |
. . . . 5
⊢ (𝑗 = (𝐹 “ 𝑘) → (◡𝐹 “ 𝑗) = (◡𝐹 “ (𝐹 “ 𝑘))) |
| 39 | | f1of1 6847 |
. . . . . . 7
⊢ (𝐹:𝐶–1-1-onto→𝑊 → 𝐹:𝐶–1-1→𝑊) |
| 40 | 39 | ad2antrl 728 |
. . . . . 6
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ ((♯‘𝑈) = 𝑁 ∧ ∀𝑥 ∈ 𝑈 ∀𝑦 ∈ 𝑈 {𝑥, 𝑦} ∉ 𝐸)) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) → 𝐹:𝐶–1-1→𝑊) |
| 41 | | usgruhgr 29203 |
. . . . . . . . . 10
⊢ (𝐺 ∈ USGraph → 𝐺 ∈
UHGraph) |
| 42 | 41 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ ((♯‘𝑈) = 𝑁 ∧ ∀𝑥 ∈ 𝑈 ∀𝑦 ∈ 𝑈 {𝑥, 𝑦} ∉ 𝐸)) → 𝐺 ∈ UHGraph) |
| 43 | 7 | clnbgrssvtx 47818 |
. . . . . . . . . . 11
⊢ (𝐺 ClNeighbVtx 𝑋) ⊆ 𝑉 |
| 44 | 9, 43 | eqsstri 4030 |
. . . . . . . . . 10
⊢ 𝐶 ⊆ 𝑉 |
| 45 | 44 | a1i 11 |
. . . . . . . . 9
⊢ ((𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0) → 𝐶 ⊆ 𝑉) |
| 46 | | eqid 2737 |
. . . . . . . . . 10
⊢
(Edg‘𝐺) =
(Edg‘𝐺) |
| 47 | | eqid 2737 |
. . . . . . . . . 10
⊢ (𝐺 ISubGr 𝐶) = (𝐺 ISubGr 𝐶) |
| 48 | 7, 46, 47, 14 | isubgredg 47852 |
. . . . . . . . 9
⊢ ((𝐺 ∈ UHGraph ∧ 𝐶 ⊆ 𝑉) → (𝑘 ∈ 𝐼 ↔ (𝑘 ∈ (Edg‘𝐺) ∧ 𝑘 ⊆ 𝐶))) |
| 49 | 42, 45, 48 | syl2an 596 |
. . . . . . . 8
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ ((♯‘𝑈) = 𝑁 ∧ ∀𝑥 ∈ 𝑈 ∀𝑦 ∈ 𝑈 {𝑥, 𝑦} ∉ 𝐸)) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) → (𝑘 ∈ 𝐼 ↔ (𝑘 ∈ (Edg‘𝐺) ∧ 𝑘 ⊆ 𝐶))) |
| 50 | | simpr 484 |
. . . . . . . . 9
⊢ ((𝑘 ∈ (Edg‘𝐺) ∧ 𝑘 ⊆ 𝐶) → 𝑘 ⊆ 𝐶) |
| 51 | 50 | a1d 25 |
. . . . . . . 8
⊢ ((𝑘 ∈ (Edg‘𝐺) ∧ 𝑘 ⊆ 𝐶) → (𝑗 ∈ (Edg‘(StarGr‘𝑁)) → 𝑘 ⊆ 𝐶)) |
| 52 | 49, 51 | biimtrdi 253 |
. . . . . . 7
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ ((♯‘𝑈) = 𝑁 ∧ ∀𝑥 ∈ 𝑈 ∀𝑦 ∈ 𝑈 {𝑥, 𝑦} ∉ 𝐸)) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) → (𝑘 ∈ 𝐼 → (𝑗 ∈ (Edg‘(StarGr‘𝑁)) → 𝑘 ⊆ 𝐶))) |
| 53 | 52 | imp32 418 |
. . . . . 6
⊢
(((((𝐺 ∈
USGraph ∧ 𝑋 ∈
𝑉) ∧
((♯‘𝑈) = 𝑁 ∧ ∀𝑥 ∈ 𝑈 ∀𝑦 ∈ 𝑈 {𝑥, 𝑦} ∉ 𝐸)) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ (𝑘 ∈ 𝐼 ∧ 𝑗 ∈ (Edg‘(StarGr‘𝑁)))) → 𝑘 ⊆ 𝐶) |
| 54 | | f1imacnv 6864 |
. . . . . 6
⊢ ((𝐹:𝐶–1-1→𝑊 ∧ 𝑘 ⊆ 𝐶) → (◡𝐹 “ (𝐹 “ 𝑘)) = 𝑘) |
| 55 | 40, 53, 54 | syl2an2r 685 |
. . . . 5
⊢
(((((𝐺 ∈
USGraph ∧ 𝑋 ∈
𝑉) ∧
((♯‘𝑈) = 𝑁 ∧ ∀𝑥 ∈ 𝑈 ∀𝑦 ∈ 𝑈 {𝑥, 𝑦} ∉ 𝐸)) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ (𝑘 ∈ 𝐼 ∧ 𝑗 ∈ (Edg‘(StarGr‘𝑁)))) → (◡𝐹 “ (𝐹 “ 𝑘)) = 𝑘) |
| 56 | 38, 55 | sylan9eqr 2799 |
. . . 4
⊢
((((((𝐺 ∈
USGraph ∧ 𝑋 ∈
𝑉) ∧
((♯‘𝑈) = 𝑁 ∧ ∀𝑥 ∈ 𝑈 ∀𝑦 ∈ 𝑈 {𝑥, 𝑦} ∉ 𝐸)) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ (𝑘 ∈ 𝐼 ∧ 𝑗 ∈ (Edg‘(StarGr‘𝑁)))) ∧ 𝑗 = (𝐹 “ 𝑘)) → (◡𝐹 “ 𝑗) = 𝑘) |
| 57 | 56 | eqcomd 2743 |
. . 3
⊢
((((((𝐺 ∈
USGraph ∧ 𝑋 ∈
𝑉) ∧
((♯‘𝑈) = 𝑁 ∧ ∀𝑥 ∈ 𝑈 ∀𝑦 ∈ 𝑈 {𝑥, 𝑦} ∉ 𝐸)) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ (𝑘 ∈ 𝐼 ∧ 𝑗 ∈ (Edg‘(StarGr‘𝑁)))) ∧ 𝑗 = (𝐹 “ 𝑘)) → 𝑘 = (◡𝐹 “ 𝑗)) |
| 58 | 37, 57 | impbida 801 |
. 2
⊢
(((((𝐺 ∈
USGraph ∧ 𝑋 ∈
𝑉) ∧
((♯‘𝑈) = 𝑁 ∧ ∀𝑥 ∈ 𝑈 ∀𝑦 ∈ 𝑈 {𝑥, 𝑦} ∉ 𝐸)) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ (𝑘 ∈ 𝐼 ∧ 𝑗 ∈ (Edg‘(StarGr‘𝑁)))) → (𝑘 = (◡𝐹 “ 𝑗) ↔ 𝑗 = (𝐹 “ 𝑘))) |
| 59 | 4, 19, 21, 58 | f1o2d 7687 |
1
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ ((♯‘𝑈) = 𝑁 ∧ ∀𝑥 ∈ 𝑈 ∀𝑦 ∈ 𝑈 {𝑥, 𝑦} ∉ 𝐸)) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) → 𝐻:𝐼–1-1-onto→(Edg‘(StarGr‘𝑁))) |