Metamath Proof Explorer

Theorem nbupgruvtxres

Description: The neighborhood of a universal vertex in a restricted pseudograph. (Contributed by Alexander van der Vekens, 2-Jan-2018) (Revised by AV, 8-Nov-2020) (Proof shortened by AV, 13-Feb-2022)

Ref Expression
Hypotheses nbupgruvtxres.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
nbupgruvtxres.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
nbupgruvtxres.f ⊢ 𝐹 = { 𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒 }
nbupgruvtxres.s ⊢ 𝑆 = ⟨ ( 𝑉 ∖ { 𝑁 } ) , ( I ↾ 𝐹 ) ⟩
Assertion nbupgruvtxres ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝐾 ∈ ( 𝑉 ∖ { 𝑁 } ) ) → ( ( 𝐺 NeighbVtx 𝐾 ) = ( 𝑉 ∖ { 𝐾 } ) → ( 𝑆 NeighbVtx 𝐾 ) = ( 𝑉 ∖ { 𝑁 , 𝐾 } ) ) )

Proof

Step Hyp Ref Expression
1 nbupgruvtxres.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 nbupgruvtxres.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3 nbupgruvtxres.f ⊢ 𝐹 = { 𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒 }
4 nbupgruvtxres.s ⊢ 𝑆 = ⟨ ( 𝑉 ∖ { 𝑁 } ) , ( I ↾ 𝐹 ) ⟩
5 eqid ⊢ ( Vtx ‘ 𝑆 ) = ( Vtx ‘ 𝑆 )
6 5 nbgrssovtx ⊢ ( 𝑆 NeighbVtx 𝐾 ) ⊆ ( ( Vtx ‘ 𝑆 ) ∖ { 𝐾 } )
7 difpr ⊢ ( 𝑉 ∖ { 𝑁 , 𝐾 } ) = ( ( 𝑉 ∖ { 𝑁 } ) ∖ { 𝐾 } )
8 1 2 3 4 upgrres1lem2 ⊢ ( Vtx ‘ 𝑆 ) = ( 𝑉 ∖ { 𝑁 } )
9 8 eqcomi ⊢ ( 𝑉 ∖ { 𝑁 } ) = ( Vtx ‘ 𝑆 )
10 9 a1i ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝐾 ∈ ( 𝑉 ∖ { 𝑁 } ) ) → ( 𝑉 ∖ { 𝑁 } ) = ( Vtx ‘ 𝑆 ) )
11 10 difeq1d ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝐾 ∈ ( 𝑉 ∖ { 𝑁 } ) ) → ( ( 𝑉 ∖ { 𝑁 } ) ∖ { 𝐾 } ) = ( ( Vtx ‘ 𝑆 ) ∖ { 𝐾 } ) )
12 7 11 syl5eq ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝐾 ∈ ( 𝑉 ∖ { 𝑁 } ) ) → ( 𝑉 ∖ { 𝑁 , 𝐾 } ) = ( ( Vtx ‘ 𝑆 ) ∖ { 𝐾 } ) )
13 6 12 sseqtrrid ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝐾 ∈ ( 𝑉 ∖ { 𝑁 } ) ) → ( 𝑆 NeighbVtx 𝐾 ) ⊆ ( 𝑉 ∖ { 𝑁 , 𝐾 } ) )
14 13 adantr ⊢ ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝐾 ∈ ( 𝑉 ∖ { 𝑁 } ) ) ∧ ( 𝐺 NeighbVtx 𝐾 ) = ( 𝑉 ∖ { 𝐾 } ) ) → ( 𝑆 NeighbVtx 𝐾 ) ⊆ ( 𝑉 ∖ { 𝑁 , 𝐾 } ) )
15 simpl ⊢ ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝐾 ∈ ( 𝑉 ∖ { 𝑁 } ) ) ∧ ( 𝐺 NeighbVtx 𝐾 ) = ( 𝑉 ∖ { 𝐾 } ) ) → ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝐾 ∈ ( 𝑉 ∖ { 𝑁 } ) ) )
16 15 anim1i ⊢ ( ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝐾 ∈ ( 𝑉 ∖ { 𝑁 } ) ) ∧ ( 𝐺 NeighbVtx 𝐾 ) = ( 𝑉 ∖ { 𝐾 } ) ) ∧ 𝑛 ∈ ( 𝑉 ∖ { 𝑁 , 𝐾 } ) ) → ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝐾 ∈ ( 𝑉 ∖ { 𝑁 } ) ) ∧ 𝑛 ∈ ( 𝑉 ∖ { 𝑁 , 𝐾 } ) ) )
17 df-3an ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝐾 ∈ ( 𝑉 ∖ { 𝑁 } ) ∧ 𝑛 ∈ ( 𝑉 ∖ { 𝑁 , 𝐾 } ) ) ↔ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝐾 ∈ ( 𝑉 ∖ { 𝑁 } ) ) ∧ 𝑛 ∈ ( 𝑉 ∖ { 𝑁 , 𝐾 } ) ) )
18 16 17 sylibr ⊢ ( ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝐾 ∈ ( 𝑉 ∖ { 𝑁 } ) ) ∧ ( 𝐺 NeighbVtx 𝐾 ) = ( 𝑉 ∖ { 𝐾 } ) ) ∧ 𝑛 ∈ ( 𝑉 ∖ { 𝑁 , 𝐾 } ) ) → ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝐾 ∈ ( 𝑉 ∖ { 𝑁 } ) ∧ 𝑛 ∈ ( 𝑉 ∖ { 𝑁 , 𝐾 } ) ) )
19 dif32 ⊢ ( ( 𝑉 ∖ { 𝑁 } ) ∖ { 𝐾 } ) = ( ( 𝑉 ∖ { 𝐾 } ) ∖ { 𝑁 } )
20 7 19 eqtri ⊢ ( 𝑉 ∖ { 𝑁 , 𝐾 } ) = ( ( 𝑉 ∖ { 𝐾 } ) ∖ { 𝑁 } )
21 20 eleq2i ⊢ ( 𝑛 ∈ ( 𝑉 ∖ { 𝑁 , 𝐾 } ) ↔ 𝑛 ∈ ( ( 𝑉 ∖ { 𝐾 } ) ∖ { 𝑁 } ) )
22 eldifsn ⊢ ( 𝑛 ∈ ( ( 𝑉 ∖ { 𝐾 } ) ∖ { 𝑁 } ) ↔ ( 𝑛 ∈ ( 𝑉 ∖ { 𝐾 } ) ∧ 𝑛 ≠ 𝑁 ) )
23 21 22 bitri ⊢ ( 𝑛 ∈ ( 𝑉 ∖ { 𝑁 , 𝐾 } ) ↔ ( 𝑛 ∈ ( 𝑉 ∖ { 𝐾 } ) ∧ 𝑛 ≠ 𝑁 ) )
24 23 simplbi ⊢ ( 𝑛 ∈ ( 𝑉 ∖ { 𝑁 , 𝐾 } ) → 𝑛 ∈ ( 𝑉 ∖ { 𝐾 } ) )
25 eleq2 ⊢ ( ( 𝐺 NeighbVtx 𝐾 ) = ( 𝑉 ∖ { 𝐾 } ) → ( 𝑛 ∈ ( 𝐺 NeighbVtx 𝐾 ) ↔ 𝑛 ∈ ( 𝑉 ∖ { 𝐾 } ) ) )
26 24 25 syl5ibr ⊢ ( ( 𝐺 NeighbVtx 𝐾 ) = ( 𝑉 ∖ { 𝐾 } ) → ( 𝑛 ∈ ( 𝑉 ∖ { 𝑁 , 𝐾 } ) → 𝑛 ∈ ( 𝐺 NeighbVtx 𝐾 ) ) )
27 26 adantl ⊢ ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝐾 ∈ ( 𝑉 ∖ { 𝑁 } ) ) ∧ ( 𝐺 NeighbVtx 𝐾 ) = ( 𝑉 ∖ { 𝐾 } ) ) → ( 𝑛 ∈ ( 𝑉 ∖ { 𝑁 , 𝐾 } ) → 𝑛 ∈ ( 𝐺 NeighbVtx 𝐾 ) ) )
28 27 imp ⊢ ( ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝐾 ∈ ( 𝑉 ∖ { 𝑁 } ) ) ∧ ( 𝐺 NeighbVtx 𝐾 ) = ( 𝑉 ∖ { 𝐾 } ) ) ∧ 𝑛 ∈ ( 𝑉 ∖ { 𝑁 , 𝐾 } ) ) → 𝑛 ∈ ( 𝐺 NeighbVtx 𝐾 ) )
29 1 2 3 4 nbupgrres ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝐾 ∈ ( 𝑉 ∖ { 𝑁 } ) ∧ 𝑛 ∈ ( 𝑉 ∖ { 𝑁 , 𝐾 } ) ) → ( 𝑛 ∈ ( 𝐺 NeighbVtx 𝐾 ) → 𝑛 ∈ ( 𝑆 NeighbVtx 𝐾 ) ) )
30 18 28 29 sylc ⊢ ( ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝐾 ∈ ( 𝑉 ∖ { 𝑁 } ) ) ∧ ( 𝐺 NeighbVtx 𝐾 ) = ( 𝑉 ∖ { 𝐾 } ) ) ∧ 𝑛 ∈ ( 𝑉 ∖ { 𝑁 , 𝐾 } ) ) → 𝑛 ∈ ( 𝑆 NeighbVtx 𝐾 ) )
31 14 30 eqelssd ⊢ ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝐾 ∈ ( 𝑉 ∖ { 𝑁 } ) ) ∧ ( 𝐺 NeighbVtx 𝐾 ) = ( 𝑉 ∖ { 𝐾 } ) ) → ( 𝑆 NeighbVtx 𝐾 ) = ( 𝑉 ∖ { 𝑁 , 𝐾 } ) )
32 31 ex ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝐾 ∈ ( 𝑉 ∖ { 𝑁 } ) ) → ( ( 𝐺 NeighbVtx 𝐾 ) = ( 𝑉 ∖ { 𝐾 } ) → ( 𝑆 NeighbVtx 𝐾 ) = ( 𝑉 ∖ { 𝑁 , 𝐾 } ) ) )