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 47869 |
. 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 1191 |
. . . . . . 7
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ (♯‘𝑈) = 𝑁) ∧ 𝑓:𝑈–1-1-onto→(𝑊 ∖ {0})) → 𝑋 ∈ 𝑉) |
11 | | c0ex 11252 |
. . . . . . . 8
⊢ 0 ∈
V |
12 | 11 | a1i 11 |
. . . . . . 7
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ (♯‘𝑈) = 𝑁) ∧ 𝑓:𝑈–1-1-onto→(𝑊 ∖ {0})) → 0 ∈
V) |
13 | | neldifsnd 4797 |
. . . . . . . 8
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ (♯‘𝑈) = 𝑁) ∧ 𝑓:𝑈–1-1-onto→(𝑊 ∖ {0})) → ¬ 0 ∈ (𝑊 ∖ {0})) |
14 | | df-nel 3044 |
. . . . . . . 8
⊢ (0
∉ (𝑊 ∖ {0})
↔ ¬ 0 ∈ (𝑊
∖ {0})) |
15 | 13, 14 | sylibr 234 |
. . . . . . 7
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ (♯‘𝑈) = 𝑁) ∧ 𝑓:𝑈–1-1-onto→(𝑊 ∖ {0})) → 0 ∉ (𝑊 ∖ {0})) |
16 | | eqid 2734 |
. . . . . . . 8
⊢ (𝑓 ∪ {〈𝑋, 0〉}) = (𝑓 ∪ {〈𝑋, 0〉}) |
17 | 1, 2, 3, 16 | isubgr3stgrlem1 47868 |
. . . . . . 7
⊢ ((𝑓:𝑈–1-1-onto→(𝑊 ∖ {0}) ∧ 𝑋 ∈ 𝑉 ∧ (0 ∈ V ∧ 0 ∉ (𝑊 ∖ {0}))) → (𝑓 ∪ {〈𝑋, 0〉}):𝐶–1-1-onto→((𝑊 ∖ {0}) ∪ {0})) |
18 | 9, 10, 12, 15, 17 | syl112anc 1373 |
. . . . . 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 1133 |
. . . . . . . 8
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ (♯‘𝑈) = 𝑁) ∧ (𝑓 ∪ {〈𝑋, 0〉}):𝐶–1-1-onto→((𝑊 ∖ {0}) ∪ {0}) ∧ dom 𝑓 = 𝑈) → (𝑓 ∪ {〈𝑋, 0〉}):𝐶⟶((𝑊 ∖ {0}) ∪ {0})) |
22 | 3 | ovexi 7464 |
. . . . . . . . 9
⊢ 𝐶 ∈ V |
23 | 22 | a1i 11 |
. . . . . . . 8
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ (♯‘𝑈) = 𝑁) ∧ (𝑓 ∪ {〈𝑋, 0〉}):𝐶–1-1-onto→((𝑊 ∖ {0}) ∪ {0}) ∧ dom 𝑓 = 𝑈) → 𝐶 ∈ V) |
24 | 21, 23 | fexd 7246 |
. . . . . . 7
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ (♯‘𝑈) = 𝑁) ∧ (𝑓 ∪ {〈𝑋, 0〉}):𝐶–1-1-onto→((𝑊 ∖ {0}) ∪ {0}) ∧ dom 𝑓 = 𝑈) → (𝑓 ∪ {〈𝑋, 0〉}) ∈ V) |
25 | 5, 6 | stgrvtx0 47864 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ0
→ 0 ∈ 𝑊) |
26 | 4, 25 | mp1i 13 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ (♯‘𝑈) = 𝑁) → 0 ∈ 𝑊) |
27 | 26 | snssd 4813 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ (♯‘𝑈) = 𝑁) → {0} ⊆ 𝑊) |
28 | | undifr 4488 |
. . . . . . . . . . . 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 1131 |
. . . . . . . 8
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ (♯‘𝑈) = 𝑁) ∧ (𝑓 ∪ {〈𝑋, 0〉}):𝐶–1-1-onto→((𝑊 ∖ {0}) ∪ {0}) ∧ dom 𝑓 = 𝑈) → (𝑓 ∪ {〈𝑋, 0〉}):𝐶–1-1-onto→𝑊) |
33 | | simp12 1203 |
. . . . . . . . 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 29391 |
. . . . . . . . . . 11
⊢ 𝑋 ∉ (𝐺 NeighbVtx 𝑋) |
36 | | df-nel 3044 |
. . . . . . . . . . . 12
⊢ (𝑋 ∉ (𝐺 NeighbVtx 𝑋) ↔ ¬ 𝑋 ∈ (𝐺 NeighbVtx 𝑋)) |
37 | 2 | eleq2i 2830 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ 𝑈 ↔ 𝑋 ∈ (𝐺 NeighbVtx 𝑋)) |
38 | 36, 37 | xchbinxr 335 |
. . . . . . . . . . 11
⊢ (𝑋 ∉ (𝐺 NeighbVtx 𝑋) ↔ ¬ 𝑋 ∈ 𝑈) |
39 | 35, 38 | mpbi 230 |
. . . . . . . . . 10
⊢ ¬
𝑋 ∈ 𝑈 |
40 | | eleq2 2827 |
. . . . . . . . . . . 12
⊢ (dom
𝑓 = 𝑈 → (𝑋 ∈ dom 𝑓 ↔ 𝑋 ∈ 𝑈)) |
41 | 40 | notbid 318 |
. . . . . . . . . . 11
⊢ (dom
𝑓 = 𝑈 → (¬ 𝑋 ∈ dom 𝑓 ↔ ¬ 𝑋 ∈ 𝑈)) |
42 | 41 | 3ad2ant3 1134 |
. . . . . . . . . 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 7206 |
. . . . . . . . 9
⊢ ((𝑋 ∈ 𝑉 ∧ 0 ∈ V ∧ ¬ 𝑋 ∈ dom 𝑓) → ((𝑓 ∪ {〈𝑋, 0〉})‘𝑋) = 0) |
45 | 33, 34, 43, 44 | syl3anc 1370 |
. . . . . . . 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 2736 |
. . . . . . . 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 3597 |
. . . . . 6
⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ (♯‘𝑈) = 𝑁) ∧ (𝑓 ∪ {〈𝑋, 0〉}):𝐶–1-1-onto→((𝑊 ∖ {0}) ∪ {0}) ∧ dom 𝑓 = 𝑈) → ∃𝑔(𝑔:𝐶–1-1-onto→𝑊 ∧ (𝑔‘𝑋) = 0)) |
52 | 51 | 3exp 1118 |
. . . . 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 1930 |
. 2
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ (♯‘𝑈) = 𝑁) → (∃𝑓 𝑓:𝑈–1-1-onto→(𝑊 ∖ {0}) → ∃𝑔(𝑔:𝐶–1-1-onto→𝑊 ∧ (𝑔‘𝑋) = 0))) |
56 | 7, 55 | mpd 15 |
1
⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ (♯‘𝑈) = 𝑁) → ∃𝑔(𝑔:𝐶–1-1-onto→𝑊 ∧ (𝑔‘𝑋) = 0)) |