Metamath Proof Explorer

Theorem usgrexmpl2nb2

Description: The neighborhood of the third vertex of graph G . (Contributed by AV, 9-Aug-2025)

Ref Expression
Hypotheses usgrexmpl2.v ⊢ 𝑉 = ( 0 ... 5 )
usgrexmpl2.e ⊢ 𝐸 = ⟨“ { 0 , 1 } { 1 , 2 } { 2 , 3 } { 3 , 4 } { 4 , 5 } { 0 , 3 } { 0 , 5 } ”⟩
usgrexmpl2.g ⊢ 𝐺 = ⟨ 𝑉 , 𝐸 ⟩
Assertion usgrexmpl2nb2 ( 𝐺 NeighbVtx 2 ) = { 1 , 3 }

Proof

Step Hyp Ref Expression
1 usgrexmpl2.v ⊢ 𝑉 = ( 0 ... 5 )
2 usgrexmpl2.e ⊢ 𝐸 = ⟨“ { 0 , 1 } { 1 , 2 } { 2 , 3 } { 3 , 4 } { 4 , 5 } { 0 , 3 } { 0 , 5 } ”⟩
3 usgrexmpl2.g ⊢ 𝐺 = ⟨ 𝑉 , 𝐸 ⟩
4 2ex ⊢ 2 ∈ V
5 4 tpid3 ⊢ 2 ∈ { 0 , 1 , 2 }
6 5 orci ⊢ ( 2 ∈ { 0 , 1 , 2 } ∨ 2 ∈ { 3 , 4 , 5 } )
7 elun ⊢ ( 2 ∈ ( { 0 , 1 , 2 } ∪ { 3 , 4 , 5 } ) ↔ ( 2 ∈ { 0 , 1 , 2 } ∨ 2 ∈ { 3 , 4 , 5 } ) )
8 6 7 mpbir ⊢ 2 ∈ ( { 0 , 1 , 2 } ∪ { 3 , 4 , 5 } )
9 1 2 3 usgrexmpl2nblem ⊢ ( 2 ∈ ( { 0 , 1 , 2 } ∪ { 3 , 4 , 5 } ) → ( 𝐺 NeighbVtx 2 ) = { 𝑛 ∈ ( { 0 , 1 , 2 } ∪ { 3 , 4 , 5 } ) ∣ { 2 , 𝑛 } ∈ ( { { 0 , 3 } } ∪ ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } ∪ { { 3 , 4 } , { 4 , 5 } , { 0 , 5 } } ) ) } )
10 8 9 ax-mp ⊢ ( 𝐺 NeighbVtx 2 ) = { 𝑛 ∈ ( { 0 , 1 , 2 } ∪ { 3 , 4 , 5 } ) ∣ { 2 , 𝑛 } ∈ ( { { 0 , 3 } } ∪ ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } ∪ { { 3 , 4 } , { 4 , 5 } , { 0 , 5 } } ) ) }
11 1ex ⊢ 1 ∈ V
12 11 tpid2 ⊢ 1 ∈ { 0 , 1 , 2 }
13 12 orci ⊢ ( 1 ∈ { 0 , 1 , 2 } ∨ 1 ∈ { 3 , 4 , 5 } )
14 elun ⊢ ( 1 ∈ ( { 0 , 1 , 2 } ∪ { 3 , 4 , 5 } ) ↔ ( 1 ∈ { 0 , 1 , 2 } ∨ 1 ∈ { 3 , 4 , 5 } ) )
15 13 14 mpbir ⊢ 1 ∈ ( { 0 , 1 , 2 } ∪ { 3 , 4 , 5 } )
16 3ex ⊢ 3 ∈ V
17 16 tpid1 ⊢ 3 ∈ { 3 , 4 , 5 }
18 17 olci ⊢ ( 3 ∈ { 0 , 1 , 2 } ∨ 3 ∈ { 3 , 4 , 5 } )
19 elun ⊢ ( 3 ∈ ( { 0 , 1 , 2 } ∪ { 3 , 4 , 5 } ) ↔ ( 3 ∈ { 0 , 1 , 2 } ∨ 3 ∈ { 3 , 4 , 5 } ) )
20 18 19 mpbir ⊢ 3 ∈ ( { 0 , 1 , 2 } ∪ { 3 , 4 , 5 } )
21 prssi ⊢ ( ( 1 ∈ ( { 0 , 1 , 2 } ∪ { 3 , 4 , 5 } ) ∧ 3 ∈ ( { 0 , 1 , 2 } ∪ { 3 , 4 , 5 } ) ) → { 1 , 3 } ⊆ ( { 0 , 1 , 2 } ∪ { 3 , 4 , 5 } ) )
22 vex ⊢ 𝑛 ∈ V
23 4 22 pm3.2i ⊢ ( 2 ∈ V ∧ 𝑛 ∈ V )
24 c0ex ⊢ 0 ∈ V
25 24 11 pm3.2i ⊢ ( 0 ∈ V ∧ 1 ∈ V )
26 23 25 pm3.2i ⊢ ( ( 2 ∈ V ∧ 𝑛 ∈ V ) ∧ ( 0 ∈ V ∧ 1 ∈ V ) )
27 2ne0 ⊢ 2 ≠ 0
28 1ne2 ⊢ 1 ≠ 2
29 28 necomi ⊢ 2 ≠ 1
30 27 29 pm3.2i ⊢ ( 2 ≠ 0 ∧ 2 ≠ 1 )
31 30 orci ⊢ ( ( 2 ≠ 0 ∧ 2 ≠ 1 ) ∨ ( 𝑛 ≠ 0 ∧ 𝑛 ≠ 1 ) )
32 prneimg ⊢ ( ( ( 2 ∈ V ∧ 𝑛 ∈ V ) ∧ ( 0 ∈ V ∧ 1 ∈ V ) ) → ( ( ( 2 ≠ 0 ∧ 2 ≠ 1 ) ∨ ( 𝑛 ≠ 0 ∧ 𝑛 ≠ 1 ) ) → { 2 , 𝑛 } ≠ { 0 , 1 } ) )
33 26 31 32 mp2 ⊢ { 2 , 𝑛 } ≠ { 0 , 1 }
34 33 neii ⊢ ¬ { 2 , 𝑛 } = { 0 , 1 }
35 34 biorfi ⊢ ( ( { 2 , 𝑛 } = { 1 , 2 } ∨ { 2 , 𝑛 } = { 2 , 3 } ) ↔ ( { 2 , 𝑛 } = { 0 , 1 } ∨ ( { 2 , 𝑛 } = { 1 , 2 } ∨ { 2 , 𝑛 } = { 2 , 3 } ) ) )
36 prcom ⊢ { 1 , 2 } = { 2 , 1 }
37 36 eqeq2i ⊢ ( { 2 , 𝑛 } = { 1 , 2 } ↔ { 2 , 𝑛 } = { 2 , 1 } )
38 22 a1i ⊢ ( 1 ∈ V → 𝑛 ∈ V )
39 id ⊢ ( 1 ∈ V → 1 ∈ V )
40 38 39 preq2b ⊢ ( 1 ∈ V → ( { 2 , 𝑛 } = { 2 , 1 } ↔ 𝑛 = 1 ) )
41 11 40 ax-mp ⊢ ( { 2 , 𝑛 } = { 2 , 1 } ↔ 𝑛 = 1 )
42 37 41 bitr2i ⊢ ( 𝑛 = 1 ↔ { 2 , 𝑛 } = { 1 , 2 } )
43 3nn0 ⊢ 3 ∈ ℕ0
44 22 a1i ⊢ ( 3 ∈ ℕ0 → 𝑛 ∈ V )
45 id ⊢ ( 3 ∈ ℕ0 → 3 ∈ ℕ0 )
46 44 45 preq2b ⊢ ( 3 ∈ ℕ0 → ( { 2 , 𝑛 } = { 2 , 3 } ↔ 𝑛 = 3 ) )
47 46 bicomd ⊢ ( 3 ∈ ℕ0 → ( 𝑛 = 3 ↔ { 2 , 𝑛 } = { 2 , 3 } ) )
48 43 47 ax-mp ⊢ ( 𝑛 = 3 ↔ { 2 , 𝑛 } = { 2 , 3 } )
49 42 48 orbi12i ⊢ ( ( 𝑛 = 1 ∨ 𝑛 = 3 ) ↔ ( { 2 , 𝑛 } = { 1 , 2 } ∨ { 2 , 𝑛 } = { 2 , 3 } ) )
50 3orass ⊢ ( ( { 2 , 𝑛 } = { 0 , 1 } ∨ { 2 , 𝑛 } = { 1 , 2 } ∨ { 2 , 𝑛 } = { 2 , 3 } ) ↔ ( { 2 , 𝑛 } = { 0 , 1 } ∨ ( { 2 , 𝑛 } = { 1 , 2 } ∨ { 2 , 𝑛 } = { 2 , 3 } ) ) )
51 35 49 50 3bitr4i ⊢ ( ( 𝑛 = 1 ∨ 𝑛 = 3 ) ↔ ( { 2 , 𝑛 } = { 0 , 1 } ∨ { 2 , 𝑛 } = { 1 , 2 } ∨ { 2 , 𝑛 } = { 2 , 3 } ) )
52 2re ⊢ 2 ∈ ℝ
53 52 22 pm3.2i ⊢ ( 2 ∈ ℝ ∧ 𝑛 ∈ V )
54 4nn0 ⊢ 4 ∈ ℕ0
55 16 54 pm3.2i ⊢ ( 3 ∈ V ∧ 4 ∈ ℕ0 )
56 53 55 pm3.2i ⊢ ( ( 2 ∈ ℝ ∧ 𝑛 ∈ V ) ∧ ( 3 ∈ V ∧ 4 ∈ ℕ0 ) )
57 2lt3 ⊢ 2 < 3
58 52 57 ltneii ⊢ 2 ≠ 3
59 2lt4 ⊢ 2 < 4
60 52 59 ltneii ⊢ 2 ≠ 4
61 58 60 pm3.2i ⊢ ( 2 ≠ 3 ∧ 2 ≠ 4 )
62 61 orci ⊢ ( ( 2 ≠ 3 ∧ 2 ≠ 4 ) ∨ ( 𝑛 ≠ 3 ∧ 𝑛 ≠ 4 ) )
63 prneimg ⊢ ( ( ( 2 ∈ ℝ ∧ 𝑛 ∈ V ) ∧ ( 3 ∈ V ∧ 4 ∈ ℕ0 ) ) → ( ( ( 2 ≠ 3 ∧ 2 ≠ 4 ) ∨ ( 𝑛 ≠ 3 ∧ 𝑛 ≠ 4 ) ) → { 2 , 𝑛 } ≠ { 3 , 4 } ) )
64 56 62 63 mp2 ⊢ { 2 , 𝑛 } ≠ { 3 , 4 }
65 64 neii ⊢ ¬ { 2 , 𝑛 } = { 3 , 4 }
66 5nn0 ⊢ 5 ∈ ℕ0
67 54 66 pm3.2i ⊢ ( 4 ∈ ℕ0 ∧ 5 ∈ ℕ0 )
68 53 67 pm3.2i ⊢ ( ( 2 ∈ ℝ ∧ 𝑛 ∈ V ) ∧ ( 4 ∈ ℕ0 ∧ 5 ∈ ℕ0 ) )
69 2lt5 ⊢ 2 < 5
70 52 69 ltneii ⊢ 2 ≠ 5
71 60 70 pm3.2i ⊢ ( 2 ≠ 4 ∧ 2 ≠ 5 )
72 71 orci ⊢ ( ( 2 ≠ 4 ∧ 2 ≠ 5 ) ∨ ( 𝑛 ≠ 4 ∧ 𝑛 ≠ 5 ) )
73 prneimg ⊢ ( ( ( 2 ∈ ℝ ∧ 𝑛 ∈ V ) ∧ ( 4 ∈ ℕ0 ∧ 5 ∈ ℕ0 ) ) → ( ( ( 2 ≠ 4 ∧ 2 ≠ 5 ) ∨ ( 𝑛 ≠ 4 ∧ 𝑛 ≠ 5 ) ) → { 2 , 𝑛 } ≠ { 4 , 5 } ) )
74 68 72 73 mp2 ⊢ { 2 , 𝑛 } ≠ { 4 , 5 }
75 74 neii ⊢ ¬ { 2 , 𝑛 } = { 4 , 5 }
76 24 66 pm3.2i ⊢ ( 0 ∈ V ∧ 5 ∈ ℕ0 )
77 53 76 pm3.2i ⊢ ( ( 2 ∈ ℝ ∧ 𝑛 ∈ V ) ∧ ( 0 ∈ V ∧ 5 ∈ ℕ0 ) )
78 27 70 pm3.2i ⊢ ( 2 ≠ 0 ∧ 2 ≠ 5 )
79 78 orci ⊢ ( ( 2 ≠ 0 ∧ 2 ≠ 5 ) ∨ ( 𝑛 ≠ 0 ∧ 𝑛 ≠ 5 ) )
80 prneimg ⊢ ( ( ( 2 ∈ ℝ ∧ 𝑛 ∈ V ) ∧ ( 0 ∈ V ∧ 5 ∈ ℕ0 ) ) → ( ( ( 2 ≠ 0 ∧ 2 ≠ 5 ) ∨ ( 𝑛 ≠ 0 ∧ 𝑛 ≠ 5 ) ) → { 2 , 𝑛 } ≠ { 0 , 5 } ) )
81 77 79 80 mp2 ⊢ { 2 , 𝑛 } ≠ { 0 , 5 }
82 81 neii ⊢ ¬ { 2 , 𝑛 } = { 0 , 5 }
83 65 75 82 3pm3.2ni ⊢ ¬ ( { 2 , 𝑛 } = { 3 , 4 } ∨ { 2 , 𝑛 } = { 4 , 5 } ∨ { 2 , 𝑛 } = { 0 , 5 } )
84 83 biorfri ⊢ ( ( { 2 , 𝑛 } = { 0 , 1 } ∨ { 2 , 𝑛 } = { 1 , 2 } ∨ { 2 , 𝑛 } = { 2 , 3 } ) ↔ ( ( { 2 , 𝑛 } = { 0 , 1 } ∨ { 2 , 𝑛 } = { 1 , 2 } ∨ { 2 , 𝑛 } = { 2 , 3 } ) ∨ ( { 2 , 𝑛 } = { 3 , 4 } ∨ { 2 , 𝑛 } = { 4 , 5 } ∨ { 2 , 𝑛 } = { 0 , 5 } ) ) )
85 24 16 pm3.2i ⊢ ( 0 ∈ V ∧ 3 ∈ V )
86 53 85 pm3.2i ⊢ ( ( 2 ∈ ℝ ∧ 𝑛 ∈ V ) ∧ ( 0 ∈ V ∧ 3 ∈ V ) )
87 27 58 pm3.2i ⊢ ( 2 ≠ 0 ∧ 2 ≠ 3 )
88 87 orci ⊢ ( ( 2 ≠ 0 ∧ 2 ≠ 3 ) ∨ ( 𝑛 ≠ 0 ∧ 𝑛 ≠ 3 ) )
89 prneimg ⊢ ( ( ( 2 ∈ ℝ ∧ 𝑛 ∈ V ) ∧ ( 0 ∈ V ∧ 3 ∈ V ) ) → ( ( ( 2 ≠ 0 ∧ 2 ≠ 3 ) ∨ ( 𝑛 ≠ 0 ∧ 𝑛 ≠ 3 ) ) → { 2 , 𝑛 } ≠ { 0 , 3 } ) )
90 86 88 89 mp2 ⊢ { 2 , 𝑛 } ≠ { 0 , 3 }
91 90 neii ⊢ ¬ { 2 , 𝑛 } = { 0 , 3 }
92 91 biorfi ⊢ ( ( ( { 2 , 𝑛 } = { 0 , 1 } ∨ { 2 , 𝑛 } = { 1 , 2 } ∨ { 2 , 𝑛 } = { 2 , 3 } ) ∨ ( { 2 , 𝑛 } = { 3 , 4 } ∨ { 2 , 𝑛 } = { 4 , 5 } ∨ { 2 , 𝑛 } = { 0 , 5 } ) ) ↔ ( { 2 , 𝑛 } = { 0 , 3 } ∨ ( ( { 2 , 𝑛 } = { 0 , 1 } ∨ { 2 , 𝑛 } = { 1 , 2 } ∨ { 2 , 𝑛 } = { 2 , 3 } ) ∨ ( { 2 , 𝑛 } = { 3 , 4 } ∨ { 2 , 𝑛 } = { 4 , 5 } ∨ { 2 , 𝑛 } = { 0 , 5 } ) ) ) )
93 51 84 92 3bitri ⊢ ( ( 𝑛 = 1 ∨ 𝑛 = 3 ) ↔ ( { 2 , 𝑛 } = { 0 , 3 } ∨ ( ( { 2 , 𝑛 } = { 0 , 1 } ∨ { 2 , 𝑛 } = { 1 , 2 } ∨ { 2 , 𝑛 } = { 2 , 3 } ) ∨ ( { 2 , 𝑛 } = { 3 , 4 } ∨ { 2 , 𝑛 } = { 4 , 5 } ∨ { 2 , 𝑛 } = { 0 , 5 } ) ) ) )
94 22 elpr ⊢ ( 𝑛 ∈ { 1 , 3 } ↔ ( 𝑛 = 1 ∨ 𝑛 = 3 ) )
95 prex ⊢ { 2 , 𝑛 } ∈ V
96 el7g ⊢ ( { 2 , 𝑛 } ∈ V → ( { 2 , 𝑛 } ∈ ( { { 0 , 3 } } ∪ ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } ∪ { { 3 , 4 } , { 4 , 5 } , { 0 , 5 } } ) ) ↔ ( { 2 , 𝑛 } = { 0 , 3 } ∨ ( ( { 2 , 𝑛 } = { 0 , 1 } ∨ { 2 , 𝑛 } = { 1 , 2 } ∨ { 2 , 𝑛 } = { 2 , 3 } ) ∨ ( { 2 , 𝑛 } = { 3 , 4 } ∨ { 2 , 𝑛 } = { 4 , 5 } ∨ { 2 , 𝑛 } = { 0 , 5 } ) ) ) ) )
97 95 96 ax-mp ⊢ ( { 2 , 𝑛 } ∈ ( { { 0 , 3 } } ∪ ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } ∪ { { 3 , 4 } , { 4 , 5 } , { 0 , 5 } } ) ) ↔ ( { 2 , 𝑛 } = { 0 , 3 } ∨ ( ( { 2 , 𝑛 } = { 0 , 1 } ∨ { 2 , 𝑛 } = { 1 , 2 } ∨ { 2 , 𝑛 } = { 2 , 3 } ) ∨ ( { 2 , 𝑛 } = { 3 , 4 } ∨ { 2 , 𝑛 } = { 4 , 5 } ∨ { 2 , 𝑛 } = { 0 , 5 } ) ) ) )
98 93 94 97 3bitr4i ⊢ ( 𝑛 ∈ { 1 , 3 } ↔ { 2 , 𝑛 } ∈ ( { { 0 , 3 } } ∪ ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } ∪ { { 3 , 4 } , { 4 , 5 } , { 0 , 5 } } ) ) )
99 98 a1i ⊢ ( ( ( 1 ∈ ( { 0 , 1 , 2 } ∪ { 3 , 4 , 5 } ) ∧ 3 ∈ ( { 0 , 1 , 2 } ∪ { 3 , 4 , 5 } ) ) ∧ 𝑛 ∈ ( { 0 , 1 , 2 } ∪ { 3 , 4 , 5 } ) ) → ( 𝑛 ∈ { 1 , 3 } ↔ { 2 , 𝑛 } ∈ ( { { 0 , 3 } } ∪ ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } ∪ { { 3 , 4 } , { 4 , 5 } , { 0 , 5 } } ) ) ) )
100 21 99 eqrrabd ⊢ ( ( 1 ∈ ( { 0 , 1 , 2 } ∪ { 3 , 4 , 5 } ) ∧ 3 ∈ ( { 0 , 1 , 2 } ∪ { 3 , 4 , 5 } ) ) → { 1 , 3 } = { 𝑛 ∈ ( { 0 , 1 , 2 } ∪ { 3 , 4 , 5 } ) ∣ { 2 , 𝑛 } ∈ ( { { 0 , 3 } } ∪ ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } ∪ { { 3 , 4 } , { 4 , 5 } , { 0 , 5 } } ) ) } )
101 100 eqcomd ⊢ ( ( 1 ∈ ( { 0 , 1 , 2 } ∪ { 3 , 4 , 5 } ) ∧ 3 ∈ ( { 0 , 1 , 2 } ∪ { 3 , 4 , 5 } ) ) → { 𝑛 ∈ ( { 0 , 1 , 2 } ∪ { 3 , 4 , 5 } ) ∣ { 2 , 𝑛 } ∈ ( { { 0 , 3 } } ∪ ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } ∪ { { 3 , 4 } , { 4 , 5 } , { 0 , 5 } } ) ) } = { 1 , 3 } )
102 15 20 101 mp2an ⊢ { 𝑛 ∈ ( { 0 , 1 , 2 } ∪ { 3 , 4 , 5 } ) ∣ { 2 , 𝑛 } ∈ ( { { 0 , 3 } } ∪ ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } ∪ { { 3 , 4 } , { 4 , 5 } , { 0 , 5 } } ) ) } = { 1 , 3 }
103 10 102 eqtri ⊢ ( 𝐺 NeighbVtx 2 ) = { 1 , 3 }