Step | Hyp | Ref
| Expression |
1 | | isubgr3stgr.h |
. . 3
⊢ 𝐻 = (𝑖 ∈ 𝐼 ↦ (𝐹 “ 𝑖)) |
2 | | imaeq2 6075 |
. . . 4
⊢ (𝑖 = 𝑘 → (𝐹 “ 𝑖) = (𝐹 “ 𝑘)) |
3 | 2 | cbvmptv 5260 |
. . 3
⊢ (𝑖 ∈ 𝐼 ↦ (𝐹 “ 𝑖)) = (𝑘 ∈ 𝐼 ↦ (𝐹 “ 𝑘)) |
4 | 1, 3 | eqtri 2762 |
. 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 47872 |
. . . 4
⊢ ((𝐹:𝐶⟶𝑊 ∧ 𝑘 ∈ 𝐼) → (𝐻‘𝑘) = (𝐹 “ 𝑘)) |
16 | 6, 15 | sylan 580 |
. . 3
⊢
(((((𝐺 ∈
USGraph ∧ 𝑋 ∈
𝑉) ∧
((♯‘𝑈) = 𝑁 ∧ ∀𝑥 ∈ 𝑈 ∀𝑦 ∈ 𝑈 {𝑥, 𝑦} ∉ 𝐸)) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑘 ∈ 𝐼) → (𝐻‘𝑘) = (𝐹 “ 𝑘)) |
17 | 7, 8, 9, 10, 11, 12, 13, 14, 1 | isubgr3stgrlem6 47873 |
. . . 4
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ ((♯‘𝑈) = 𝑁 ∧ ∀𝑥 ∈ 𝑈 ∀𝑦 ∈ 𝑈 {𝑥, 𝑦} ∉ 𝐸)) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) → 𝐻:𝐼⟶(Edg‘(StarGr‘𝑁))) |
18 | 17 | ffvelcdmda 7103 |
. . 3
⊢
(((((𝐺 ∈
USGraph ∧ 𝑋 ∈
𝑉) ∧
((♯‘𝑈) = 𝑁 ∧ ∀𝑥 ∈ 𝑈 ∀𝑦 ∈ 𝑈 {𝑥, 𝑦} ∉ 𝐸)) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑘 ∈ 𝐼) → (𝐻‘𝑘) ∈ (Edg‘(StarGr‘𝑁))) |
19 | 16, 18 | eqeltrrd 2839 |
. 2
⊢
(((((𝐺 ∈
USGraph ∧ 𝑋 ∈
𝑉) ∧
((♯‘𝑈) = 𝑁 ∧ ∀𝑥 ∈ 𝑈 ∀𝑦 ∈ 𝑈 {𝑥, 𝑦} ∉ 𝐸)) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑘 ∈ 𝐼) → (𝐹 “ 𝑘) ∈ (Edg‘(StarGr‘𝑁))) |
20 | 7, 8, 9, 10, 11, 12, 13, 14, 1 | isubgr3stgrlem7 47874 |
. . 3
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0) ∧ 𝑗 ∈ (Edg‘(StarGr‘𝑁))) → (◡𝐹 “ 𝑗) ∈ 𝐼) |
21 | 20 | ad4ant134 1173 |
. 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 47861 |
. . . . . . 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 2762 |
. . . . . . . 8
⊢ 𝑊 =
(Vtx‘(StarGr‘𝑁)) |
29 | | eqid 2734 |
. . . . . . . 8
⊢
(Edg‘(StarGr‘𝑁)) = (Edg‘(StarGr‘𝑁)) |
30 | 28, 29 | edgssv2 29229 |
. . . . . . 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 6075 |
. . . . 5
⊢ (𝑘 = (◡𝐹 “ 𝑗) → (𝐹 “ 𝑘) = (𝐹 “ (◡𝐹 “ 𝑗))) |
36 | 35 | eqcomd 2740 |
. . . 4
⊢ (𝑘 = (◡𝐹 “ 𝑗) → (𝐹 “ (◡𝐹 “ 𝑗)) = (𝐹 “ 𝑘)) |
37 | 34, 36 | sylan9req 2795 |
. . 3
⊢
((((((𝐺 ∈
USGraph ∧ 𝑋 ∈
𝑉) ∧
((♯‘𝑈) = 𝑁 ∧ ∀𝑥 ∈ 𝑈 ∀𝑦 ∈ 𝑈 {𝑥, 𝑦} ∉ 𝐸)) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ (𝑘 ∈ 𝐼 ∧ 𝑗 ∈ (Edg‘(StarGr‘𝑁)))) ∧ 𝑘 = (◡𝐹 “ 𝑗)) → 𝑗 = (𝐹 “ 𝑘)) |
38 | | imaeq2 6075 |
. . . . 5
⊢ (𝑗 = (𝐹 “ 𝑘) → (◡𝐹 “ 𝑗) = (◡𝐹 “ (𝐹 “ 𝑘))) |
39 | | f1of1 6847 |
. . . . . . 7
⊢ (𝐹:𝐶–1-1-onto→𝑊 → 𝐹:𝐶–1-1→𝑊) |
40 | 39 | ad2antrl 728 |
. . . . . 6
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ ((♯‘𝑈) = 𝑁 ∧ ∀𝑥 ∈ 𝑈 ∀𝑦 ∈ 𝑈 {𝑥, 𝑦} ∉ 𝐸)) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) → 𝐹:𝐶–1-1→𝑊) |
41 | | usgruhgr 29217 |
. . . . . . . . . 10
⊢ (𝐺 ∈ USGraph → 𝐺 ∈
UHGraph) |
42 | 41 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ ((♯‘𝑈) = 𝑁 ∧ ∀𝑥 ∈ 𝑈 ∀𝑦 ∈ 𝑈 {𝑥, 𝑦} ∉ 𝐸)) → 𝐺 ∈ UHGraph) |
43 | 7 | clnbgrssvtx 47755 |
. . . . . . . . . . 11
⊢ (𝐺 ClNeighbVtx 𝑋) ⊆ 𝑉 |
44 | 9, 43 | eqsstri 4029 |
. . . . . . . . . 10
⊢ 𝐶 ⊆ 𝑉 |
45 | 44 | a1i 11 |
. . . . . . . . 9
⊢ ((𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0) → 𝐶 ⊆ 𝑉) |
46 | | eqid 2734 |
. . . . . . . . . 10
⊢
(Edg‘𝐺) =
(Edg‘𝐺) |
47 | | eqid 2734 |
. . . . . . . . . 10
⊢ (𝐺 ISubGr 𝐶) = (𝐺 ISubGr 𝐶) |
48 | 7, 46, 47, 14 | isubgredg 47789 |
. . . . . . . . 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 2796 |
. . . 4
⊢
((((((𝐺 ∈
USGraph ∧ 𝑋 ∈
𝑉) ∧
((♯‘𝑈) = 𝑁 ∧ ∀𝑥 ∈ 𝑈 ∀𝑦 ∈ 𝑈 {𝑥, 𝑦} ∉ 𝐸)) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ (𝑘 ∈ 𝐼 ∧ 𝑗 ∈ (Edg‘(StarGr‘𝑁)))) ∧ 𝑗 = (𝐹 “ 𝑘)) → (◡𝐹 “ 𝑗) = 𝑘) |
57 | 56 | eqcomd 2740 |
. . 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 7686 |
1
⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ ((♯‘𝑈) = 𝑁 ∧ ∀𝑥 ∈ 𝑈 ∀𝑦 ∈ 𝑈 {𝑥, 𝑦} ∉ 𝐸)) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) → 𝐻:𝐼–1-1-onto→(Edg‘(StarGr‘𝑁))) |