| Step | Hyp | Ref
| Expression |
| 1 | | isubgr3stgr.v |
. . 3
⊢ 𝑉 = (Vtx‘𝐺) |
| 2 | | isubgr3stgr.u |
. . 3
⊢ 𝑈 = (𝐺 NeighbVtx 𝑋) |
| 3 | | isubgr3stgr.c |
. . 3
⊢ 𝐶 = (𝐺 ClNeighbVtx 𝑋) |
| 4 | | isubgr3stgr.n |
. . 3
⊢ 𝑁 ∈
ℕ0 |
| 5 | | isubgr3stgr.s |
. . 3
⊢ 𝑆 = (StarGr‘𝑁) |
| 6 | | isubgr3stgr.w |
. . 3
⊢ 𝑊 = (Vtx‘𝑆) |
| 7 | 1, 2, 3, 4, 5, 6 | isubgr3stgrlem2 47934 |
. 2
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ (♯‘𝑈) = 𝑁) → ∃𝑓 𝑓:𝑈–1-1-onto→(𝑊 ∖ {0})) |
| 8 | | f1odm 6852 |
. . . 4
⊢ (𝑓:𝑈–1-1-onto→(𝑊 ∖ {0}) → dom 𝑓 = 𝑈) |
| 9 | | simpr 484 |
. . . . . . 7
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ (♯‘𝑈) = 𝑁) ∧ 𝑓:𝑈–1-1-onto→(𝑊 ∖ {0})) → 𝑓:𝑈–1-1-onto→(𝑊 ∖ {0})) |
| 10 | | simpl2 1193 |
. . . . . . 7
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ (♯‘𝑈) = 𝑁) ∧ 𝑓:𝑈–1-1-onto→(𝑊 ∖ {0})) → 𝑋 ∈ 𝑉) |
| 11 | | c0ex 11255 |
. . . . . . . 8
⊢ 0 ∈
V |
| 12 | 11 | a1i 11 |
. . . . . . 7
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ (♯‘𝑈) = 𝑁) ∧ 𝑓:𝑈–1-1-onto→(𝑊 ∖ {0})) → 0 ∈
V) |
| 13 | | neldifsnd 4793 |
. . . . . . . 8
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ (♯‘𝑈) = 𝑁) ∧ 𝑓:𝑈–1-1-onto→(𝑊 ∖ {0})) → ¬ 0 ∈ (𝑊 ∖ {0})) |
| 14 | | df-nel 3047 |
. . . . . . . 8
⊢ (0
∉ (𝑊 ∖ {0})
↔ ¬ 0 ∈ (𝑊
∖ {0})) |
| 15 | 13, 14 | sylibr 234 |
. . . . . . 7
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ (♯‘𝑈) = 𝑁) ∧ 𝑓:𝑈–1-1-onto→(𝑊 ∖ {0})) → 0 ∉ (𝑊 ∖ {0})) |
| 16 | | eqid 2737 |
. . . . . . . 8
⊢ (𝑓 ∪ {〈𝑋, 0〉}) = (𝑓 ∪ {〈𝑋, 0〉}) |
| 17 | 1, 2, 3, 16 | isubgr3stgrlem1 47933 |
. . . . . . 7
⊢ ((𝑓:𝑈–1-1-onto→(𝑊 ∖ {0}) ∧ 𝑋 ∈ 𝑉 ∧ (0 ∈ V ∧ 0 ∉ (𝑊 ∖ {0}))) → (𝑓 ∪ {〈𝑋, 0〉}):𝐶–1-1-onto→((𝑊 ∖ {0}) ∪ {0})) |
| 18 | 9, 10, 12, 15, 17 | syl112anc 1376 |
. . . . . 6
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ (♯‘𝑈) = 𝑁) ∧ 𝑓:𝑈–1-1-onto→(𝑊 ∖ {0})) → (𝑓 ∪ {〈𝑋, 0〉}):𝐶–1-1-onto→((𝑊 ∖ {0}) ∪ {0})) |
| 19 | 18 | ex 412 |
. . . . 5
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ (♯‘𝑈) = 𝑁) → (𝑓:𝑈–1-1-onto→(𝑊 ∖ {0}) → (𝑓 ∪ {〈𝑋, 0〉}):𝐶–1-1-onto→((𝑊 ∖ {0}) ∪ {0}))) |
| 20 | | f1of 6848 |
. . . . . . . . 9
⊢ ((𝑓 ∪ {〈𝑋, 0〉}):𝐶–1-1-onto→((𝑊 ∖ {0}) ∪ {0}) → (𝑓 ∪ {〈𝑋, 0〉}):𝐶⟶((𝑊 ∖ {0}) ∪ {0})) |
| 21 | 20 | 3ad2ant2 1135 |
. . . . . . . 8
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ (♯‘𝑈) = 𝑁) ∧ (𝑓 ∪ {〈𝑋, 0〉}):𝐶–1-1-onto→((𝑊 ∖ {0}) ∪ {0}) ∧ dom 𝑓 = 𝑈) → (𝑓 ∪ {〈𝑋, 0〉}):𝐶⟶((𝑊 ∖ {0}) ∪ {0})) |
| 22 | 3 | ovexi 7465 |
. . . . . . . . 9
⊢ 𝐶 ∈ V |
| 23 | 22 | a1i 11 |
. . . . . . . 8
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ (♯‘𝑈) = 𝑁) ∧ (𝑓 ∪ {〈𝑋, 0〉}):𝐶–1-1-onto→((𝑊 ∖ {0}) ∪ {0}) ∧ dom 𝑓 = 𝑈) → 𝐶 ∈ V) |
| 24 | 21, 23 | fexd 7247 |
. . . . . . 7
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ (♯‘𝑈) = 𝑁) ∧ (𝑓 ∪ {〈𝑋, 0〉}):𝐶–1-1-onto→((𝑊 ∖ {0}) ∪ {0}) ∧ dom 𝑓 = 𝑈) → (𝑓 ∪ {〈𝑋, 0〉}) ∈ V) |
| 25 | 5, 6 | stgrvtx0 47929 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ0
→ 0 ∈ 𝑊) |
| 26 | 4, 25 | mp1i 13 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ (♯‘𝑈) = 𝑁) → 0 ∈ 𝑊) |
| 27 | 26 | snssd 4809 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ (♯‘𝑈) = 𝑁) → {0} ⊆ 𝑊) |
| 28 | | undifr 4483 |
. . . . . . . . . . . 12
⊢ ({0}
⊆ 𝑊 ↔ ((𝑊 ∖ {0}) ∪ {0}) = 𝑊) |
| 29 | 27, 28 | sylib 218 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ (♯‘𝑈) = 𝑁) → ((𝑊 ∖ {0}) ∪ {0}) = 𝑊) |
| 30 | 29 | f1oeq3d 6845 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ (♯‘𝑈) = 𝑁) → ((𝑓 ∪ {〈𝑋, 0〉}):𝐶–1-1-onto→((𝑊 ∖ {0}) ∪ {0}) ↔ (𝑓 ∪ {〈𝑋, 0〉}):𝐶–1-1-onto→𝑊)) |
| 31 | 30 | biimpa 476 |
. . . . . . . . 9
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ (♯‘𝑈) = 𝑁) ∧ (𝑓 ∪ {〈𝑋, 0〉}):𝐶–1-1-onto→((𝑊 ∖ {0}) ∪ {0})) → (𝑓 ∪ {〈𝑋, 0〉}):𝐶–1-1-onto→𝑊) |
| 32 | 31 | 3adant3 1133 |
. . . . . . . 8
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ (♯‘𝑈) = 𝑁) ∧ (𝑓 ∪ {〈𝑋, 0〉}):𝐶–1-1-onto→((𝑊 ∖ {0}) ∪ {0}) ∧ dom 𝑓 = 𝑈) → (𝑓 ∪ {〈𝑋, 0〉}):𝐶–1-1-onto→𝑊) |
| 33 | | simp12 1205 |
. . . . . . . . 9
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ (♯‘𝑈) = 𝑁) ∧ (𝑓 ∪ {〈𝑋, 0〉}):𝐶–1-1-onto→((𝑊 ∖ {0}) ∪ {0}) ∧ dom 𝑓 = 𝑈) → 𝑋 ∈ 𝑉) |
| 34 | 11 | a1i 11 |
. . . . . . . . 9
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ (♯‘𝑈) = 𝑁) ∧ (𝑓 ∪ {〈𝑋, 0〉}):𝐶–1-1-onto→((𝑊 ∖ {0}) ∪ {0}) ∧ dom 𝑓 = 𝑈) → 0 ∈ V) |
| 35 | | nbgrnself2 29377 |
. . . . . . . . . . 11
⊢ 𝑋 ∉ (𝐺 NeighbVtx 𝑋) |
| 36 | | df-nel 3047 |
. . . . . . . . . . . 12
⊢ (𝑋 ∉ (𝐺 NeighbVtx 𝑋) ↔ ¬ 𝑋 ∈ (𝐺 NeighbVtx 𝑋)) |
| 37 | 2 | eleq2i 2833 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ 𝑈 ↔ 𝑋 ∈ (𝐺 NeighbVtx 𝑋)) |
| 38 | 36, 37 | xchbinxr 335 |
. . . . . . . . . . 11
⊢ (𝑋 ∉ (𝐺 NeighbVtx 𝑋) ↔ ¬ 𝑋 ∈ 𝑈) |
| 39 | 35, 38 | mpbi 230 |
. . . . . . . . . 10
⊢ ¬
𝑋 ∈ 𝑈 |
| 40 | | eleq2 2830 |
. . . . . . . . . . . 12
⊢ (dom
𝑓 = 𝑈 → (𝑋 ∈ dom 𝑓 ↔ 𝑋 ∈ 𝑈)) |
| 41 | 40 | notbid 318 |
. . . . . . . . . . 11
⊢ (dom
𝑓 = 𝑈 → (¬ 𝑋 ∈ dom 𝑓 ↔ ¬ 𝑋 ∈ 𝑈)) |
| 42 | 41 | 3ad2ant3 1136 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ (♯‘𝑈) = 𝑁) ∧ (𝑓 ∪ {〈𝑋, 0〉}):𝐶–1-1-onto→((𝑊 ∖ {0}) ∪ {0}) ∧ dom 𝑓 = 𝑈) → (¬ 𝑋 ∈ dom 𝑓 ↔ ¬ 𝑋 ∈ 𝑈)) |
| 43 | 39, 42 | mpbiri 258 |
. . . . . . . . 9
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ (♯‘𝑈) = 𝑁) ∧ (𝑓 ∪ {〈𝑋, 0〉}):𝐶–1-1-onto→((𝑊 ∖ {0}) ∪ {0}) ∧ dom 𝑓 = 𝑈) → ¬ 𝑋 ∈ dom 𝑓) |
| 44 | | fsnunfv 7207 |
. . . . . . . . 9
⊢ ((𝑋 ∈ 𝑉 ∧ 0 ∈ V ∧ ¬ 𝑋 ∈ dom 𝑓) → ((𝑓 ∪ {〈𝑋, 0〉})‘𝑋) = 0) |
| 45 | 33, 34, 43, 44 | syl3anc 1373 |
. . . . . . . 8
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ (♯‘𝑈) = 𝑁) ∧ (𝑓 ∪ {〈𝑋, 0〉}):𝐶–1-1-onto→((𝑊 ∖ {0}) ∪ {0}) ∧ dom 𝑓 = 𝑈) → ((𝑓 ∪ {〈𝑋, 0〉})‘𝑋) = 0) |
| 46 | 32, 45 | jca 511 |
. . . . . . 7
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ (♯‘𝑈) = 𝑁) ∧ (𝑓 ∪ {〈𝑋, 0〉}):𝐶–1-1-onto→((𝑊 ∖ {0}) ∪ {0}) ∧ dom 𝑓 = 𝑈) → ((𝑓 ∪ {〈𝑋, 0〉}):𝐶–1-1-onto→𝑊 ∧ ((𝑓 ∪ {〈𝑋, 0〉})‘𝑋) = 0)) |
| 47 | | f1oeq1 6836 |
. . . . . . . 8
⊢ (𝑔 = (𝑓 ∪ {〈𝑋, 0〉}) → (𝑔:𝐶–1-1-onto→𝑊 ↔ (𝑓 ∪ {〈𝑋, 0〉}):𝐶–1-1-onto→𝑊)) |
| 48 | | fveq1 6905 |
. . . . . . . . 9
⊢ (𝑔 = (𝑓 ∪ {〈𝑋, 0〉}) → (𝑔‘𝑋) = ((𝑓 ∪ {〈𝑋, 0〉})‘𝑋)) |
| 49 | 48 | eqeq1d 2739 |
. . . . . . . 8
⊢ (𝑔 = (𝑓 ∪ {〈𝑋, 0〉}) → ((𝑔‘𝑋) = 0 ↔ ((𝑓 ∪ {〈𝑋, 0〉})‘𝑋) = 0)) |
| 50 | 47, 49 | anbi12d 632 |
. . . . . . 7
⊢ (𝑔 = (𝑓 ∪ {〈𝑋, 0〉}) → ((𝑔:𝐶–1-1-onto→𝑊 ∧ (𝑔‘𝑋) = 0) ↔ ((𝑓 ∪ {〈𝑋, 0〉}):𝐶–1-1-onto→𝑊 ∧ ((𝑓 ∪ {〈𝑋, 0〉})‘𝑋) = 0))) |
| 51 | 24, 46, 50 | spcedv 3598 |
. . . . . 6
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ (♯‘𝑈) = 𝑁) ∧ (𝑓 ∪ {〈𝑋, 0〉}):𝐶–1-1-onto→((𝑊 ∖ {0}) ∪ {0}) ∧ dom 𝑓 = 𝑈) → ∃𝑔(𝑔:𝐶–1-1-onto→𝑊 ∧ (𝑔‘𝑋) = 0)) |
| 52 | 51 | 3exp 1120 |
. . . . 5
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ (♯‘𝑈) = 𝑁) → ((𝑓 ∪ {〈𝑋, 0〉}):𝐶–1-1-onto→((𝑊 ∖ {0}) ∪ {0}) → (dom 𝑓 = 𝑈 → ∃𝑔(𝑔:𝐶–1-1-onto→𝑊 ∧ (𝑔‘𝑋) = 0)))) |
| 53 | 19, 52 | syld 47 |
. . . 4
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ (♯‘𝑈) = 𝑁) → (𝑓:𝑈–1-1-onto→(𝑊 ∖ {0}) → (dom 𝑓 = 𝑈 → ∃𝑔(𝑔:𝐶–1-1-onto→𝑊 ∧ (𝑔‘𝑋) = 0)))) |
| 54 | 8, 53 | mpdi 45 |
. . 3
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ (♯‘𝑈) = 𝑁) → (𝑓:𝑈–1-1-onto→(𝑊 ∖ {0}) → ∃𝑔(𝑔:𝐶–1-1-onto→𝑊 ∧ (𝑔‘𝑋) = 0))) |
| 55 | 54 | exlimdv 1933 |
. 2
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ (♯‘𝑈) = 𝑁) → (∃𝑓 𝑓:𝑈–1-1-onto→(𝑊 ∖ {0}) → ∃𝑔(𝑔:𝐶–1-1-onto→𝑊 ∧ (𝑔‘𝑋) = 0))) |
| 56 | 7, 55 | mpd 15 |
1
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ (♯‘𝑈) = 𝑁) → ∃𝑔(𝑔:𝐶–1-1-onto→𝑊 ∧ (𝑔‘𝑋) = 0)) |