Step |
Hyp |
Ref |
Expression |
1 |
|
isubgr3stgr.v |
⊢ 𝑉 = ( Vtx ‘ 𝐺 ) |
2 |
|
isubgr3stgr.u |
⊢ 𝑈 = ( 𝐺 NeighbVtx 𝑋 ) |
3 |
|
isubgr3stgr.c |
⊢ 𝐶 = ( 𝐺 ClNeighbVtx 𝑋 ) |
4 |
|
isubgr3stgr.f |
⊢ 𝐹 = ( 𝐻 ∪ { 〈 𝑋 , 𝑌 〉 } ) |
5 |
|
f1oeq2 |
⊢ ( 𝑈 = ( 𝐺 NeighbVtx 𝑋 ) → ( 𝐻 : 𝑈 –1-1-onto→ 𝑅 ↔ 𝐻 : ( 𝐺 NeighbVtx 𝑋 ) –1-1-onto→ 𝑅 ) ) |
6 |
2 5
|
ax-mp |
⊢ ( 𝐻 : 𝑈 –1-1-onto→ 𝑅 ↔ 𝐻 : ( 𝐺 NeighbVtx 𝑋 ) –1-1-onto→ 𝑅 ) |
7 |
6
|
biimpi |
⊢ ( 𝐻 : 𝑈 –1-1-onto→ 𝑅 → 𝐻 : ( 𝐺 NeighbVtx 𝑋 ) –1-1-onto→ 𝑅 ) |
8 |
7
|
3ad2ant1 |
⊢ ( ( 𝐻 : 𝑈 –1-1-onto→ 𝑅 ∧ 𝑋 ∈ 𝑉 ∧ ( 𝑌 ∈ 𝑊 ∧ 𝑌 ∉ 𝑅 ) ) → 𝐻 : ( 𝐺 NeighbVtx 𝑋 ) –1-1-onto→ 𝑅 ) |
9 |
|
simpl |
⊢ ( ( 𝑌 ∈ 𝑊 ∧ 𝑌 ∉ 𝑅 ) → 𝑌 ∈ 𝑊 ) |
10 |
9
|
anim2i |
⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( 𝑌 ∈ 𝑊 ∧ 𝑌 ∉ 𝑅 ) ) → ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ) |
11 |
10
|
3adant1 |
⊢ ( ( 𝐻 : 𝑈 –1-1-onto→ 𝑅 ∧ 𝑋 ∈ 𝑉 ∧ ( 𝑌 ∈ 𝑊 ∧ 𝑌 ∉ 𝑅 ) ) → ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ) |
12 |
|
nbgrnself2 |
⊢ 𝑋 ∉ ( 𝐺 NeighbVtx 𝑋 ) |
13 |
12
|
a1i |
⊢ ( ( 𝐻 : 𝑈 –1-1-onto→ 𝑅 ∧ 𝑋 ∈ 𝑉 ∧ ( 𝑌 ∈ 𝑊 ∧ 𝑌 ∉ 𝑅 ) ) → 𝑋 ∉ ( 𝐺 NeighbVtx 𝑋 ) ) |
14 |
|
simp3r |
⊢ ( ( 𝐻 : 𝑈 –1-1-onto→ 𝑅 ∧ 𝑋 ∈ 𝑉 ∧ ( 𝑌 ∈ 𝑊 ∧ 𝑌 ∉ 𝑅 ) ) → 𝑌 ∉ 𝑅 ) |
15 |
4
|
f1ounsn |
⊢ ( ( 𝐻 : ( 𝐺 NeighbVtx 𝑋 ) –1-1-onto→ 𝑅 ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ∧ ( 𝑋 ∉ ( 𝐺 NeighbVtx 𝑋 ) ∧ 𝑌 ∉ 𝑅 ) ) → 𝐹 : ( ( 𝐺 NeighbVtx 𝑋 ) ∪ { 𝑋 } ) –1-1-onto→ ( 𝑅 ∪ { 𝑌 } ) ) |
16 |
8 11 13 14 15
|
syl112anc |
⊢ ( ( 𝐻 : 𝑈 –1-1-onto→ 𝑅 ∧ 𝑋 ∈ 𝑉 ∧ ( 𝑌 ∈ 𝑊 ∧ 𝑌 ∉ 𝑅 ) ) → 𝐹 : ( ( 𝐺 NeighbVtx 𝑋 ) ∪ { 𝑋 } ) –1-1-onto→ ( 𝑅 ∪ { 𝑌 } ) ) |
17 |
1
|
dfclnbgr4 |
⊢ ( 𝑋 ∈ 𝑉 → ( 𝐺 ClNeighbVtx 𝑋 ) = ( { 𝑋 } ∪ ( 𝐺 NeighbVtx 𝑋 ) ) ) |
18 |
17
|
3ad2ant2 |
⊢ ( ( 𝐻 : 𝑈 –1-1-onto→ 𝑅 ∧ 𝑋 ∈ 𝑉 ∧ ( 𝑌 ∈ 𝑊 ∧ 𝑌 ∉ 𝑅 ) ) → ( 𝐺 ClNeighbVtx 𝑋 ) = ( { 𝑋 } ∪ ( 𝐺 NeighbVtx 𝑋 ) ) ) |
19 |
|
uncom |
⊢ ( { 𝑋 } ∪ ( 𝐺 NeighbVtx 𝑋 ) ) = ( ( 𝐺 NeighbVtx 𝑋 ) ∪ { 𝑋 } ) |
20 |
18 19
|
eqtrdi |
⊢ ( ( 𝐻 : 𝑈 –1-1-onto→ 𝑅 ∧ 𝑋 ∈ 𝑉 ∧ ( 𝑌 ∈ 𝑊 ∧ 𝑌 ∉ 𝑅 ) ) → ( 𝐺 ClNeighbVtx 𝑋 ) = ( ( 𝐺 NeighbVtx 𝑋 ) ∪ { 𝑋 } ) ) |
21 |
3 20
|
eqtrid |
⊢ ( ( 𝐻 : 𝑈 –1-1-onto→ 𝑅 ∧ 𝑋 ∈ 𝑉 ∧ ( 𝑌 ∈ 𝑊 ∧ 𝑌 ∉ 𝑅 ) ) → 𝐶 = ( ( 𝐺 NeighbVtx 𝑋 ) ∪ { 𝑋 } ) ) |
22 |
21
|
f1oeq2d |
⊢ ( ( 𝐻 : 𝑈 –1-1-onto→ 𝑅 ∧ 𝑋 ∈ 𝑉 ∧ ( 𝑌 ∈ 𝑊 ∧ 𝑌 ∉ 𝑅 ) ) → ( 𝐹 : 𝐶 –1-1-onto→ ( 𝑅 ∪ { 𝑌 } ) ↔ 𝐹 : ( ( 𝐺 NeighbVtx 𝑋 ) ∪ { 𝑋 } ) –1-1-onto→ ( 𝑅 ∪ { 𝑌 } ) ) ) |
23 |
16 22
|
mpbird |
⊢ ( ( 𝐻 : 𝑈 –1-1-onto→ 𝑅 ∧ 𝑋 ∈ 𝑉 ∧ ( 𝑌 ∈ 𝑊 ∧ 𝑌 ∉ 𝑅 ) ) → 𝐹 : 𝐶 –1-1-onto→ ( 𝑅 ∪ { 𝑌 } ) ) |