Metamath Proof Explorer

Theorem nbupgr

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

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

Proof

Step Hyp Ref Expression
1 nbuhgr.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 nbuhgr.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3 1 2 nbgrval ⊢ ( 𝑁 ∈ 𝑉 → ( 𝐺 NeighbVtx 𝑁 ) = { 𝑛 ∈ ( 𝑉 ∖ { 𝑁 } ) ∣ ∃ 𝑒 ∈ 𝐸 { 𝑁 , 𝑛 } ⊆ 𝑒 } )
4 3 adantl ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) → ( 𝐺 NeighbVtx 𝑁 ) = { 𝑛 ∈ ( 𝑉 ∖ { 𝑁 } ) ∣ ∃ 𝑒 ∈ 𝐸 { 𝑁 , 𝑛 } ⊆ 𝑒 } )
5 simp-4l ⊢ ( ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑛 ∈ ( 𝑉 ∖ { 𝑁 } ) ) ∧ 𝑒 ∈ 𝐸 ) ∧ { 𝑁 , 𝑛 } ⊆ 𝑒 ) → 𝐺 ∈ UPGraph )
6 simpr ⊢ ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑛 ∈ ( 𝑉 ∖ { 𝑁 } ) ) ∧ 𝑒 ∈ 𝐸 ) → 𝑒 ∈ 𝐸 )
7 6 adantr ⊢ ( ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑛 ∈ ( 𝑉 ∖ { 𝑁 } ) ) ∧ 𝑒 ∈ 𝐸 ) ∧ { 𝑁 , 𝑛 } ⊆ 𝑒 ) → 𝑒 ∈ 𝐸 )
8 simpr ⊢ ( ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑛 ∈ ( 𝑉 ∖ { 𝑁 } ) ) ∧ 𝑒 ∈ 𝐸 ) ∧ { 𝑁 , 𝑛 } ⊆ 𝑒 ) → { 𝑁 , 𝑛 } ⊆ 𝑒 )
9 simpr ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) → 𝑁 ∈ 𝑉 )
10 9 adantr ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑛 ∈ ( 𝑉 ∖ { 𝑁 } ) ) → 𝑁 ∈ 𝑉 )
11 vex ⊢ 𝑛 ∈ V
12 11 a1i ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑛 ∈ ( 𝑉 ∖ { 𝑁 } ) ) → 𝑛 ∈ V )
13 eldifsn ⊢ ( 𝑛 ∈ ( 𝑉 ∖ { 𝑁 } ) ↔ ( 𝑛 ∈ 𝑉 ∧ 𝑛 ≠ 𝑁 ) )
14 simpr ⊢ ( ( 𝑛 ∈ 𝑉 ∧ 𝑛 ≠ 𝑁 ) → 𝑛 ≠ 𝑁 )
15 14 necomd ⊢ ( ( 𝑛 ∈ 𝑉 ∧ 𝑛 ≠ 𝑁 ) → 𝑁 ≠ 𝑛 )
16 13 15 sylbi ⊢ ( 𝑛 ∈ ( 𝑉 ∖ { 𝑁 } ) → 𝑁 ≠ 𝑛 )
17 16 adantl ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑛 ∈ ( 𝑉 ∖ { 𝑁 } ) ) → 𝑁 ≠ 𝑛 )
18 10 12 17 3jca ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑛 ∈ ( 𝑉 ∖ { 𝑁 } ) ) → ( 𝑁 ∈ 𝑉 ∧ 𝑛 ∈ V ∧ 𝑁 ≠ 𝑛 ) )
19 18 adantr ⊢ ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑛 ∈ ( 𝑉 ∖ { 𝑁 } ) ) ∧ 𝑒 ∈ 𝐸 ) → ( 𝑁 ∈ 𝑉 ∧ 𝑛 ∈ V ∧ 𝑁 ≠ 𝑛 ) )
20 19 adantr ⊢ ( ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑛 ∈ ( 𝑉 ∖ { 𝑁 } ) ) ∧ 𝑒 ∈ 𝐸 ) ∧ { 𝑁 , 𝑛 } ⊆ 𝑒 ) → ( 𝑁 ∈ 𝑉 ∧ 𝑛 ∈ V ∧ 𝑁 ≠ 𝑛 ) )
21 1 2 upgredgpr ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑒 ∈ 𝐸 ∧ { 𝑁 , 𝑛 } ⊆ 𝑒 ) ∧ ( 𝑁 ∈ 𝑉 ∧ 𝑛 ∈ V ∧ 𝑁 ≠ 𝑛 ) ) → { 𝑁 , 𝑛 } = 𝑒 )
22 5 7 8 20 21 syl31anc ⊢ ( ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑛 ∈ ( 𝑉 ∖ { 𝑁 } ) ) ∧ 𝑒 ∈ 𝐸 ) ∧ { 𝑁 , 𝑛 } ⊆ 𝑒 ) → { 𝑁 , 𝑛 } = 𝑒 )
23 22 ex ⊢ ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑛 ∈ ( 𝑉 ∖ { 𝑁 } ) ) ∧ 𝑒 ∈ 𝐸 ) → ( { 𝑁 , 𝑛 } ⊆ 𝑒 → { 𝑁 , 𝑛 } = 𝑒 ) )
24 eleq1 ⊢ ( { 𝑁 , 𝑛 } = 𝑒 → ( { 𝑁 , 𝑛 } ∈ 𝐸 ↔ 𝑒 ∈ 𝐸 ) )
25 24 biimprd ⊢ ( { 𝑁 , 𝑛 } = 𝑒 → ( 𝑒 ∈ 𝐸 → { 𝑁 , 𝑛 } ∈ 𝐸 ) )
26 23 6 25 syl6ci ⊢ ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑛 ∈ ( 𝑉 ∖ { 𝑁 } ) ) ∧ 𝑒 ∈ 𝐸 ) → ( { 𝑁 , 𝑛 } ⊆ 𝑒 → { 𝑁 , 𝑛 } ∈ 𝐸 ) )
27 26 rexlimdva ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑛 ∈ ( 𝑉 ∖ { 𝑁 } ) ) → ( ∃ 𝑒 ∈ 𝐸 { 𝑁 , 𝑛 } ⊆ 𝑒 → { 𝑁 , 𝑛 } ∈ 𝐸 ) )
28 simpr ⊢ ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑛 ∈ ( 𝑉 ∖ { 𝑁 } ) ) ∧ { 𝑁 , 𝑛 } ∈ 𝐸 ) → { 𝑁 , 𝑛 } ∈ 𝐸 )
29 sseq2 ⊢ ( 𝑒 = { 𝑁 , 𝑛 } → ( { 𝑁 , 𝑛 } ⊆ 𝑒 ↔ { 𝑁 , 𝑛 } ⊆ { 𝑁 , 𝑛 } ) )
30 29 adantl ⊢ ( ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑛 ∈ ( 𝑉 ∖ { 𝑁 } ) ) ∧ { 𝑁 , 𝑛 } ∈ 𝐸 ) ∧ 𝑒 = { 𝑁 , 𝑛 } ) → ( { 𝑁 , 𝑛 } ⊆ 𝑒 ↔ { 𝑁 , 𝑛 } ⊆ { 𝑁 , 𝑛 } ) )
31 ssidd ⊢ ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑛 ∈ ( 𝑉 ∖ { 𝑁 } ) ) ∧ { 𝑁 , 𝑛 } ∈ 𝐸 ) → { 𝑁 , 𝑛 } ⊆ { 𝑁 , 𝑛 } )
32 28 30 31 rspcedvd ⊢ ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑛 ∈ ( 𝑉 ∖ { 𝑁 } ) ) ∧ { 𝑁 , 𝑛 } ∈ 𝐸 ) → ∃ 𝑒 ∈ 𝐸 { 𝑁 , 𝑛 } ⊆ 𝑒 )
33 32 ex ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑛 ∈ ( 𝑉 ∖ { 𝑁 } ) ) → ( { 𝑁 , 𝑛 } ∈ 𝐸 → ∃ 𝑒 ∈ 𝐸 { 𝑁 , 𝑛 } ⊆ 𝑒 ) )
34 27 33 impbid ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑛 ∈ ( 𝑉 ∖ { 𝑁 } ) ) → ( ∃ 𝑒 ∈ 𝐸 { 𝑁 , 𝑛 } ⊆ 𝑒 ↔ { 𝑁 , 𝑛 } ∈ 𝐸 ) )
35 34 rabbidva ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) → { 𝑛 ∈ ( 𝑉 ∖ { 𝑁 } ) ∣ ∃ 𝑒 ∈ 𝐸 { 𝑁 , 𝑛 } ⊆ 𝑒 } = { 𝑛 ∈ ( 𝑉 ∖ { 𝑁 } ) ∣ { 𝑁 , 𝑛 } ∈ 𝐸 } )
36 4 35 eqtrd ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) → ( 𝐺 NeighbVtx 𝑁 ) = { 𝑛 ∈ ( 𝑉 ∖ { 𝑁 } ) ∣ { 𝑁 , 𝑛 } ∈ 𝐸 } )