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 𝑁 ) = { 𝑛𝑉 ∣ { 𝑁 , 𝑛 } ∈ 𝐸 } )