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 eqtrid ( ( ( 𝐺 ∈ 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 𝐾 ) = ( 𝑉 ∖ { 𝑁 , 𝐾 } ) ) )