This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nbumgrvtx

Description: The set of neighbors of a vertex in a multigraph. (Contributed by AV, 27-Nov-2020) (Proof shortened by AV, 30-Dec-2020)

Ref Expression
Hypotheses nbuhgr.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
nbuhgr.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion nbumgrvtx ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉 ) → ( 𝐺 NeighbVtx 𝑁 ) = { 𝑛 ∈ 𝑉 ∣ { 𝑁 , 𝑛 } ∈ 𝐸 } )

Proof

Step Hyp Ref Expression
1 nbuhgr.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 nbuhgr.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3 1 2 nbgrval ⊢ ( 𝑁 ∈ 𝑉 → ( 𝐺 NeighbVtx 𝑁 ) = { 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ∣ ∃ 𝑒 ∈ 𝐸 { 𝑁 , 𝑣 } ⊆ 𝑒 } )
4 3 adantl ⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉 ) → ( 𝐺 NeighbVtx 𝑁 ) = { 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ∣ ∃ 𝑒 ∈ 𝐸 { 𝑁 , 𝑣 } ⊆ 𝑒 } )
5 eldifi ⊢ ( 𝑥 ∈ ( 𝑉 ∖ { 𝑁 } ) → 𝑥 ∈ 𝑉 )
6 5 adantl ⊢ ( ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 𝑁 } ) ) → 𝑥 ∈ 𝑉 )
7 6 adantr ⊢ ( ( ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 𝑁 } ) ) ∧ ( 𝑒 ∈ 𝐸 ∧ { 𝑁 , 𝑥 } ⊆ 𝑒 ) ) → 𝑥 ∈ 𝑉 )
8 umgrupgr ⊢ ( 𝐺 ∈ UMGraph → 𝐺 ∈ UPGraph )
9 8 ad4antr ⊢ ( ( ( ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 𝑁 } ) ) ∧ 𝑒 ∈ 𝐸 ) ∧ { 𝑁 , 𝑥 } ⊆ 𝑒 ) → 𝐺 ∈ UPGraph )
10 simpr ⊢ ( ( ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 𝑁 } ) ) ∧ 𝑒 ∈ 𝐸 ) → 𝑒 ∈ 𝐸 )
11 10 adantr ⊢ ( ( ( ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 𝑁 } ) ) ∧ 𝑒 ∈ 𝐸 ) ∧ { 𝑁 , 𝑥 } ⊆ 𝑒 ) → 𝑒 ∈ 𝐸 )
12 simpr ⊢ ( ( ( ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 𝑁 } ) ) ∧ 𝑒 ∈ 𝐸 ) ∧ { 𝑁 , 𝑥 } ⊆ 𝑒 ) → { 𝑁 , 𝑥 } ⊆ 𝑒 )
13 simpr ⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉 ) → 𝑁 ∈ 𝑉 )
14 13 adantr ⊢ ( ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 𝑁 } ) ) → 𝑁 ∈ 𝑉 )
15 vex ⊢ 𝑥 ∈ V
16 15 a1i ⊢ ( ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 𝑁 } ) ) → 𝑥 ∈ V )
17 eldifsn ⊢ ( 𝑥 ∈ ( 𝑉 ∖ { 𝑁 } ) ↔ ( 𝑥 ∈ 𝑉 ∧ 𝑥 ≠ 𝑁 ) )
18 simpr ⊢ ( ( 𝑥 ∈ 𝑉 ∧ 𝑥 ≠ 𝑁 ) → 𝑥 ≠ 𝑁 )
19 18 necomd ⊢ ( ( 𝑥 ∈ 𝑉 ∧ 𝑥 ≠ 𝑁 ) → 𝑁 ≠ 𝑥 )
20 17 19 sylbi ⊢ ( 𝑥 ∈ ( 𝑉 ∖ { 𝑁 } ) → 𝑁 ≠ 𝑥 )
21 20 adantl ⊢ ( ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 𝑁 } ) ) → 𝑁 ≠ 𝑥 )
22 14 16 21 3jca ⊢ ( ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 𝑁 } ) ) → ( 𝑁 ∈ 𝑉 ∧ 𝑥 ∈ V ∧ 𝑁 ≠ 𝑥 ) )
23 22 adantr ⊢ ( ( ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 𝑁 } ) ) ∧ 𝑒 ∈ 𝐸 ) → ( 𝑁 ∈ 𝑉 ∧ 𝑥 ∈ V ∧ 𝑁 ≠ 𝑥 ) )
24 23 adantr ⊢ ( ( ( ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 𝑁 } ) ) ∧ 𝑒 ∈ 𝐸 ) ∧ { 𝑁 , 𝑥 } ⊆ 𝑒 ) → ( 𝑁 ∈ 𝑉 ∧ 𝑥 ∈ V ∧ 𝑁 ≠ 𝑥 ) )
25 1 2 upgredgpr ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑒 ∈ 𝐸 ∧ { 𝑁 , 𝑥 } ⊆ 𝑒 ) ∧ ( 𝑁 ∈ 𝑉 ∧ 𝑥 ∈ V ∧ 𝑁 ≠ 𝑥 ) ) → { 𝑁 , 𝑥 } = 𝑒 )
26 9 11 12 24 25 syl31anc ⊢ ( ( ( ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 𝑁 } ) ) ∧ 𝑒 ∈ 𝐸 ) ∧ { 𝑁 , 𝑥 } ⊆ 𝑒 ) → { 𝑁 , 𝑥 } = 𝑒 )
27 26 ex ⊢ ( ( ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 𝑁 } ) ) ∧ 𝑒 ∈ 𝐸 ) → ( { 𝑁 , 𝑥 } ⊆ 𝑒 → { 𝑁 , 𝑥 } = 𝑒 ) )
28 eleq1 ⊢ ( { 𝑁 , 𝑥 } = 𝑒 → ( { 𝑁 , 𝑥 } ∈ 𝐸 ↔ 𝑒 ∈ 𝐸 ) )
29 28 biimprd ⊢ ( { 𝑁 , 𝑥 } = 𝑒 → ( 𝑒 ∈ 𝐸 → { 𝑁 , 𝑥 } ∈ 𝐸 ) )
30 27 10 29 syl6ci ⊢ ( ( ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 𝑁 } ) ) ∧ 𝑒 ∈ 𝐸 ) → ( { 𝑁 , 𝑥 } ⊆ 𝑒 → { 𝑁 , 𝑥 } ∈ 𝐸 ) )
31 30 impr ⊢ ( ( ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 𝑁 } ) ) ∧ ( 𝑒 ∈ 𝐸 ∧ { 𝑁 , 𝑥 } ⊆ 𝑒 ) ) → { 𝑁 , 𝑥 } ∈ 𝐸 )
32 7 31 jca ⊢ ( ( ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 𝑁 } ) ) ∧ ( 𝑒 ∈ 𝐸 ∧ { 𝑁 , 𝑥 } ⊆ 𝑒 ) ) → ( 𝑥 ∈ 𝑉 ∧ { 𝑁 , 𝑥 } ∈ 𝐸 ) )
33 32 rexlimdvaa ⊢ ( ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑥 ∈ ( 𝑉 ∖ { 𝑁 } ) ) → ( ∃ 𝑒 ∈ 𝐸 { 𝑁 , 𝑥 } ⊆ 𝑒 → ( 𝑥 ∈ 𝑉 ∧ { 𝑁 , 𝑥 } ∈ 𝐸 ) ) )
34 33 expimpd ⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉 ) → ( ( 𝑥 ∈ ( 𝑉 ∖ { 𝑁 } ) ∧ ∃ 𝑒 ∈ 𝐸 { 𝑁 , 𝑥 } ⊆ 𝑒 ) → ( 𝑥 ∈ 𝑉 ∧ { 𝑁 , 𝑥 } ∈ 𝐸 ) ) )
35 simprl ⊢ ( ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑥 ∈ 𝑉 ∧ { 𝑁 , 𝑥 } ∈ 𝐸 ) ) → 𝑥 ∈ 𝑉 )
36 2 umgredgne ⊢ ( ( 𝐺 ∈ UMGraph ∧ { 𝑁 , 𝑥 } ∈ 𝐸 ) → 𝑁 ≠ 𝑥 )
37 36 ad2ant2rl ⊢ ( ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑥 ∈ 𝑉 ∧ { 𝑁 , 𝑥 } ∈ 𝐸 ) ) → 𝑁 ≠ 𝑥 )
38 37 necomd ⊢ ( ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑥 ∈ 𝑉 ∧ { 𝑁 , 𝑥 } ∈ 𝐸 ) ) → 𝑥 ≠ 𝑁 )
39 35 38 17 sylanbrc ⊢ ( ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑥 ∈ 𝑉 ∧ { 𝑁 , 𝑥 } ∈ 𝐸 ) ) → 𝑥 ∈ ( 𝑉 ∖ { 𝑁 } ) )
40 simpr ⊢ ( ( 𝑥 ∈ 𝑉 ∧ { 𝑁 , 𝑥 } ∈ 𝐸 ) → { 𝑁 , 𝑥 } ∈ 𝐸 )
41 40 adantl ⊢ ( ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑥 ∈ 𝑉 ∧ { 𝑁 , 𝑥 } ∈ 𝐸 ) ) → { 𝑁 , 𝑥 } ∈ 𝐸 )
42 sseq2 ⊢ ( 𝑒 = { 𝑁 , 𝑥 } → ( { 𝑁 , 𝑥 } ⊆ 𝑒 ↔ { 𝑁 , 𝑥 } ⊆ { 𝑁 , 𝑥 } ) )
43 42 adantl ⊢ ( ( ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑥 ∈ 𝑉 ∧ { 𝑁 , 𝑥 } ∈ 𝐸 ) ) ∧ 𝑒 = { 𝑁 , 𝑥 } ) → ( { 𝑁 , 𝑥 } ⊆ 𝑒 ↔ { 𝑁 , 𝑥 } ⊆ { 𝑁 , 𝑥 } ) )
44 ssidd ⊢ ( ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑥 ∈ 𝑉 ∧ { 𝑁 , 𝑥 } ∈ 𝐸 ) ) → { 𝑁 , 𝑥 } ⊆ { 𝑁 , 𝑥 } )
45 41 43 44 rspcedvd ⊢ ( ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑥 ∈ 𝑉 ∧ { 𝑁 , 𝑥 } ∈ 𝐸 ) ) → ∃ 𝑒 ∈ 𝐸 { 𝑁 , 𝑥 } ⊆ 𝑒 )
46 39 45 jca ⊢ ( ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑥 ∈ 𝑉 ∧ { 𝑁 , 𝑥 } ∈ 𝐸 ) ) → ( 𝑥 ∈ ( 𝑉 ∖ { 𝑁 } ) ∧ ∃ 𝑒 ∈ 𝐸 { 𝑁 , 𝑥 } ⊆ 𝑒 ) )
47 46 ex ⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉 ) → ( ( 𝑥 ∈ 𝑉 ∧ { 𝑁 , 𝑥 } ∈ 𝐸 ) → ( 𝑥 ∈ ( 𝑉 ∖ { 𝑁 } ) ∧ ∃ 𝑒 ∈ 𝐸 { 𝑁 , 𝑥 } ⊆ 𝑒 ) ) )
48 34 47 impbid ⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉 ) → ( ( 𝑥 ∈ ( 𝑉 ∖ { 𝑁 } ) ∧ ∃ 𝑒 ∈ 𝐸 { 𝑁 , 𝑥 } ⊆ 𝑒 ) ↔ ( 𝑥 ∈ 𝑉 ∧ { 𝑁 , 𝑥 } ∈ 𝐸 ) ) )
49 preq2 ⊢ ( 𝑣 = 𝑥 → { 𝑁 , 𝑣 } = { 𝑁 , 𝑥 } )
50 49 sseq1d ⊢ ( 𝑣 = 𝑥 → ( { 𝑁 , 𝑣 } ⊆ 𝑒 ↔ { 𝑁 , 𝑥 } ⊆ 𝑒 ) )
51 50 rexbidv ⊢ ( 𝑣 = 𝑥 → ( ∃ 𝑒 ∈ 𝐸 { 𝑁 , 𝑣 } ⊆ 𝑒 ↔ ∃ 𝑒 ∈ 𝐸 { 𝑁 , 𝑥 } ⊆ 𝑒 ) )
52 51 elrab ⊢ ( 𝑥 ∈ { 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ∣ ∃ 𝑒 ∈ 𝐸 { 𝑁 , 𝑣 } ⊆ 𝑒 } ↔ ( 𝑥 ∈ ( 𝑉 ∖ { 𝑁 } ) ∧ ∃ 𝑒 ∈ 𝐸 { 𝑁 , 𝑥 } ⊆ 𝑒 ) )
53 preq2 ⊢ ( 𝑛 = 𝑥 → { 𝑁 , 𝑛 } = { 𝑁 , 𝑥 } )
54 53 eleq1d ⊢ ( 𝑛 = 𝑥 → ( { 𝑁 , 𝑛 } ∈ 𝐸 ↔ { 𝑁 , 𝑥 } ∈ 𝐸 ) )
55 54 elrab ⊢ ( 𝑥 ∈ { 𝑛 ∈ 𝑉 ∣ { 𝑁 , 𝑛 } ∈ 𝐸 } ↔ ( 𝑥 ∈ 𝑉 ∧ { 𝑁 , 𝑥 } ∈ 𝐸 ) )
56 48 52 55 3bitr4g ⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉 ) → ( 𝑥 ∈ { 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ∣ ∃ 𝑒 ∈ 𝐸 { 𝑁 , 𝑣 } ⊆ 𝑒 } ↔ 𝑥 ∈ { 𝑛 ∈ 𝑉 ∣ { 𝑁 , 𝑛 } ∈ 𝐸 } ) )
57 56 eqrdv ⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉 ) → { 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ∣ ∃ 𝑒 ∈ 𝐸 { 𝑁 , 𝑣 } ⊆ 𝑒 } = { 𝑛 ∈ 𝑉 ∣ { 𝑁 , 𝑛 } ∈ 𝐸 } )
58 4 57 eqtrd ⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉 ) → ( 𝐺 NeighbVtx 𝑁 ) = { 𝑛 ∈ 𝑉 ∣ { 𝑁 , 𝑛 } ∈ 𝐸 } )