Metamath Proof Explorer

Theorem usgrexmpl2nb1

Description: The neighborhood of the second 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 usgrexmpl2nb1 ( 𝐺 NeighbVtx 1 ) = { 0 , 2 }

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