Metamath Proof Explorer

Theorem nbupgrres

Description: The neighborhood of a vertex in a restricted pseudograph (not necessarily valid for a hypergraph, because N , K and M could be connected by one edge, so M is a neighbor of K in the original graph, but not in the restricted graph, because the edge between M and K , also incident with N , was removed). (Contributed by Alexander van der Vekens, 2-Jan-2018) (Revised by AV, 8-Nov-2020)

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

Proof

Step Hyp Ref Expression
1 nbupgrres.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 nbupgrres.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3 nbupgrres.f ⊢ 𝐹 = { 𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒 }
4 nbupgrres.s ⊢ 𝑆 = ⟨ ( 𝑉 ∖ { 𝑁 } ) , ( I ↾ 𝐹 ) ⟩
5 simp1l ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝐾 ∈ ( 𝑉 ∖ { 𝑁 } ) ∧ 𝑀 ∈ ( 𝑉 ∖ { 𝑁 , 𝐾 } ) ) → 𝐺 ∈ UPGraph )
6 eldifi ⊢ ( 𝐾 ∈ ( 𝑉 ∖ { 𝑁 } ) → 𝐾 ∈ 𝑉 )
7 6 3ad2ant2 ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝐾 ∈ ( 𝑉 ∖ { 𝑁 } ) ∧ 𝑀 ∈ ( 𝑉 ∖ { 𝑁 , 𝐾 } ) ) → 𝐾 ∈ 𝑉 )
8 eldifsn ⊢ ( 𝑀 ∈ ( ( 𝑉 ∖ { 𝑁 } ) ∖ { 𝐾 } ) ↔ ( 𝑀 ∈ ( 𝑉 ∖ { 𝑁 } ) ∧ 𝑀 ≠ 𝐾 ) )
9 eldifi ⊢ ( 𝑀 ∈ ( 𝑉 ∖ { 𝑁 } ) → 𝑀 ∈ 𝑉 )
10 9 anim1i ⊢ ( ( 𝑀 ∈ ( 𝑉 ∖ { 𝑁 } ) ∧ 𝑀 ≠ 𝐾 ) → ( 𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝐾 ) )
11 8 10 sylbi ⊢ ( 𝑀 ∈ ( ( 𝑉 ∖ { 𝑁 } ) ∖ { 𝐾 } ) → ( 𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝐾 ) )
12 difpr ⊢ ( 𝑉 ∖ { 𝑁 , 𝐾 } ) = ( ( 𝑉 ∖ { 𝑁 } ) ∖ { 𝐾 } )
13 11 12 eleq2s ⊢ ( 𝑀 ∈ ( 𝑉 ∖ { 𝑁 , 𝐾 } ) → ( 𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝐾 ) )
14 13 3ad2ant3 ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝐾 ∈ ( 𝑉 ∖ { 𝑁 } ) ∧ 𝑀 ∈ ( 𝑉 ∖ { 𝑁 , 𝐾 } ) ) → ( 𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝐾 ) )
15 1 2 nbupgrel ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝐾 ∈ 𝑉 ) ∧ ( 𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝐾 ) ) → ( 𝑀 ∈ ( 𝐺 NeighbVtx 𝐾 ) ↔ { 𝑀 , 𝐾 } ∈ 𝐸 ) )
16 5 7 14 15 syl21anc ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝐾 ∈ ( 𝑉 ∖ { 𝑁 } ) ∧ 𝑀 ∈ ( 𝑉 ∖ { 𝑁 , 𝐾 } ) ) → ( 𝑀 ∈ ( 𝐺 NeighbVtx 𝐾 ) ↔ { 𝑀 , 𝐾 } ∈ 𝐸 ) )
17 16 biimpa ⊢ ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝐾 ∈ ( 𝑉 ∖ { 𝑁 } ) ∧ 𝑀 ∈ ( 𝑉 ∖ { 𝑁 , 𝐾 } ) ) ∧ 𝑀 ∈ ( 𝐺 NeighbVtx 𝐾 ) ) → { 𝑀 , 𝐾 } ∈ 𝐸 )
18 12 eleq2i ⊢ ( 𝑀 ∈ ( 𝑉 ∖ { 𝑁 , 𝐾 } ) ↔ 𝑀 ∈ ( ( 𝑉 ∖ { 𝑁 } ) ∖ { 𝐾 } ) )
19 eldifsn ⊢ ( 𝑀 ∈ ( 𝑉 ∖ { 𝑁 } ) ↔ ( 𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑁 ) )
20 19 anbi1i ⊢ ( ( 𝑀 ∈ ( 𝑉 ∖ { 𝑁 } ) ∧ 𝑀 ≠ 𝐾 ) ↔ ( ( 𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑁 ) ∧ 𝑀 ≠ 𝐾 ) )
21 18 8 20 3bitri ⊢ ( 𝑀 ∈ ( 𝑉 ∖ { 𝑁 , 𝐾 } ) ↔ ( ( 𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑁 ) ∧ 𝑀 ≠ 𝐾 ) )
22 simpr ⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑁 ) → 𝑀 ≠ 𝑁 )
23 22 necomd ⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑁 ) → 𝑁 ≠ 𝑀 )
24 23 adantr ⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝑀 ≠ 𝑁 ) ∧ 𝑀 ≠ 𝐾 ) → 𝑁 ≠ 𝑀 )
25 21 24 sylbi ⊢ ( 𝑀 ∈ ( 𝑉 ∖ { 𝑁 , 𝐾 } ) → 𝑁 ≠ 𝑀 )
26 25 3ad2ant3 ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝐾 ∈ ( 𝑉 ∖ { 𝑁 } ) ∧ 𝑀 ∈ ( 𝑉 ∖ { 𝑁 , 𝐾 } ) ) → 𝑁 ≠ 𝑀 )
27 eldifsn ⊢ ( 𝐾 ∈ ( 𝑉 ∖ { 𝑁 } ) ↔ ( 𝐾 ∈ 𝑉 ∧ 𝐾 ≠ 𝑁 ) )
28 simpr ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝐾 ≠ 𝑁 ) → 𝐾 ≠ 𝑁 )
29 28 necomd ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝐾 ≠ 𝑁 ) → 𝑁 ≠ 𝐾 )
30 27 29 sylbi ⊢ ( 𝐾 ∈ ( 𝑉 ∖ { 𝑁 } ) → 𝑁 ≠ 𝐾 )
31 30 3ad2ant2 ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝐾 ∈ ( 𝑉 ∖ { 𝑁 } ) ∧ 𝑀 ∈ ( 𝑉 ∖ { 𝑁 , 𝐾 } ) ) → 𝑁 ≠ 𝐾 )
32 26 31 nelprd ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝐾 ∈ ( 𝑉 ∖ { 𝑁 } ) ∧ 𝑀 ∈ ( 𝑉 ∖ { 𝑁 , 𝐾 } ) ) → ¬ 𝑁 ∈ { 𝑀 , 𝐾 } )
33 df-nel ⊢ ( 𝑁 ∉ { 𝑀 , 𝐾 } ↔ ¬ 𝑁 ∈ { 𝑀 , 𝐾 } )
34 32 33 sylibr ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝐾 ∈ ( 𝑉 ∖ { 𝑁 } ) ∧ 𝑀 ∈ ( 𝑉 ∖ { 𝑁 , 𝐾 } ) ) → 𝑁 ∉ { 𝑀 , 𝐾 } )
35 34 adantr ⊢ ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝐾 ∈ ( 𝑉 ∖ { 𝑁 } ) ∧ 𝑀 ∈ ( 𝑉 ∖ { 𝑁 , 𝐾 } ) ) ∧ 𝑀 ∈ ( 𝐺 NeighbVtx 𝐾 ) ) → 𝑁 ∉ { 𝑀 , 𝐾 } )
36 neleq2 ⊢ ( 𝑒 = { 𝑀 , 𝐾 } → ( 𝑁 ∉ 𝑒 ↔ 𝑁 ∉ { 𝑀 , 𝐾 } ) )
37 36 3 elrab2 ⊢ ( { 𝑀 , 𝐾 } ∈ 𝐹 ↔ ( { 𝑀 , 𝐾 } ∈ 𝐸 ∧ 𝑁 ∉ { 𝑀 , 𝐾 } ) )
38 17 35 37 sylanbrc ⊢ ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝐾 ∈ ( 𝑉 ∖ { 𝑁 } ) ∧ 𝑀 ∈ ( 𝑉 ∖ { 𝑁 , 𝐾 } ) ) ∧ 𝑀 ∈ ( 𝐺 NeighbVtx 𝐾 ) ) → { 𝑀 , 𝐾 } ∈ 𝐹 )
39 1 2 3 4 upgrres1 ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) → 𝑆 ∈ UPGraph )
40 39 3ad2ant1 ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝐾 ∈ ( 𝑉 ∖ { 𝑁 } ) ∧ 𝑀 ∈ ( 𝑉 ∖ { 𝑁 , 𝐾 } ) ) → 𝑆 ∈ UPGraph )
41 simp2 ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝐾 ∈ ( 𝑉 ∖ { 𝑁 } ) ∧ 𝑀 ∈ ( 𝑉 ∖ { 𝑁 , 𝐾 } ) ) → 𝐾 ∈ ( 𝑉 ∖ { 𝑁 } ) )
42 18 8 sylbb ⊢ ( 𝑀 ∈ ( 𝑉 ∖ { 𝑁 , 𝐾 } ) → ( 𝑀 ∈ ( 𝑉 ∖ { 𝑁 } ) ∧ 𝑀 ≠ 𝐾 ) )
43 42 3ad2ant3 ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝐾 ∈ ( 𝑉 ∖ { 𝑁 } ) ∧ 𝑀 ∈ ( 𝑉 ∖ { 𝑁 , 𝐾 } ) ) → ( 𝑀 ∈ ( 𝑉 ∖ { 𝑁 } ) ∧ 𝑀 ≠ 𝐾 ) )
44 40 41 43 jca31 ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝐾 ∈ ( 𝑉 ∖ { 𝑁 } ) ∧ 𝑀 ∈ ( 𝑉 ∖ { 𝑁 , 𝐾 } ) ) → ( ( 𝑆 ∈ UPGraph ∧ 𝐾 ∈ ( 𝑉 ∖ { 𝑁 } ) ) ∧ ( 𝑀 ∈ ( 𝑉 ∖ { 𝑁 } ) ∧ 𝑀 ≠ 𝐾 ) ) )
45 44 adantr ⊢ ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝐾 ∈ ( 𝑉 ∖ { 𝑁 } ) ∧ 𝑀 ∈ ( 𝑉 ∖ { 𝑁 , 𝐾 } ) ) ∧ 𝑀 ∈ ( 𝐺 NeighbVtx 𝐾 ) ) → ( ( 𝑆 ∈ UPGraph ∧ 𝐾 ∈ ( 𝑉 ∖ { 𝑁 } ) ) ∧ ( 𝑀 ∈ ( 𝑉 ∖ { 𝑁 } ) ∧ 𝑀 ≠ 𝐾 ) ) )
46 1 2 3 4 upgrres1lem2 ⊢ ( Vtx ‘ 𝑆 ) = ( 𝑉 ∖ { 𝑁 } )
47 46 eqcomi ⊢ ( 𝑉 ∖ { 𝑁 } ) = ( Vtx ‘ 𝑆 )
48 edgval ⊢ ( Edg ‘ 𝑆 ) = ran ( iEdg ‘ 𝑆 )
49 1 2 3 4 upgrres1lem3 ⊢ ( iEdg ‘ 𝑆 ) = ( I ↾ 𝐹 )
50 49 rneqi ⊢ ran ( iEdg ‘ 𝑆 ) = ran ( I ↾ 𝐹 )
51 rnresi ⊢ ran ( I ↾ 𝐹 ) = 𝐹
52 48 50 51 3eqtrri ⊢ 𝐹 = ( Edg ‘ 𝑆 )
53 47 52 nbupgrel ⊢ ( ( ( 𝑆 ∈ UPGraph ∧ 𝐾 ∈ ( 𝑉 ∖ { 𝑁 } ) ) ∧ ( 𝑀 ∈ ( 𝑉 ∖ { 𝑁 } ) ∧ 𝑀 ≠ 𝐾 ) ) → ( 𝑀 ∈ ( 𝑆 NeighbVtx 𝐾 ) ↔ { 𝑀 , 𝐾 } ∈ 𝐹 ) )
54 45 53 syl ⊢ ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝐾 ∈ ( 𝑉 ∖ { 𝑁 } ) ∧ 𝑀 ∈ ( 𝑉 ∖ { 𝑁 , 𝐾 } ) ) ∧ 𝑀 ∈ ( 𝐺 NeighbVtx 𝐾 ) ) → ( 𝑀 ∈ ( 𝑆 NeighbVtx 𝐾 ) ↔ { 𝑀 , 𝐾 } ∈ 𝐹 ) )
55 38 54 mpbird ⊢ ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝐾 ∈ ( 𝑉 ∖ { 𝑁 } ) ∧ 𝑀 ∈ ( 𝑉 ∖ { 𝑁 , 𝐾 } ) ) ∧ 𝑀 ∈ ( 𝐺 NeighbVtx 𝐾 ) ) → 𝑀 ∈ ( 𝑆 NeighbVtx 𝐾 ) )
56 55 ex ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝐾 ∈ ( 𝑉 ∖ { 𝑁 } ) ∧ 𝑀 ∈ ( 𝑉 ∖ { 𝑁 , 𝐾 } ) ) → ( 𝑀 ∈ ( 𝐺 NeighbVtx 𝐾 ) → 𝑀 ∈ ( 𝑆 NeighbVtx 𝐾 ) ) )