Metamath Proof Explorer

Theorem usgrexmpl2nb0

Description: The neighborhood of the first 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 usgrexmpl2nb0 ( 𝐺 NeighbVtx 0 ) = { 1 , 3 , 5 }

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 c0ex ⊢ 0 ∈ V
5 4 tpid1 ⊢ 0 ∈ { 0 , 1 , 2 }
6 5 orci ⊢ ( 0 ∈ { 0 , 1 , 2 } ∨ 0 ∈ { 3 , 4 , 5 } )
7 elun ⊢ ( 0 ∈ ( { 0 , 1 , 2 } ∪ { 3 , 4 , 5 } ) ↔ ( 0 ∈ { 0 , 1 , 2 } ∨ 0 ∈ { 3 , 4 , 5 } ) )
8 6 7 mpbir ⊢ 0 ∈ ( { 0 , 1 , 2 } ∪ { 3 , 4 , 5 } )
9 1 2 3 usgrexmpl2nblem ⊢ ( 0 ∈ ( { 0 , 1 , 2 } ∪ { 3 , 4 , 5 } ) → ( 𝐺 NeighbVtx 0 ) = { 𝑛 ∈ ( { 0 , 1 , 2 } ∪ { 3 , 4 , 5 } ) ∣ { 0 , 𝑛 } ∈ ( { { 0 , 3 } } ∪ ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } ∪ { { 3 , 4 } , { 4 , 5 } , { 0 , 5 } } ) ) } )
10 8 9 ax-mp ⊢ ( 𝐺 NeighbVtx 0 ) = { 𝑛 ∈ ( { 0 , 1 , 2 } ∪ { 3 , 4 , 5 } ) ∣ { 0 , 𝑛 } ∈ ( { { 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 5nn0 ⊢ 5 ∈ ℕ0
22 21 elexi ⊢ 5 ∈ V
23 22 tpid3 ⊢ 5 ∈ { 3 , 4 , 5 }
24 23 olci ⊢ ( 5 ∈ { 0 , 1 , 2 } ∨ 5 ∈ { 3 , 4 , 5 } )
25 elun ⊢ ( 5 ∈ ( { 0 , 1 , 2 } ∪ { 3 , 4 , 5 } ) ↔ ( 5 ∈ { 0 , 1 , 2 } ∨ 5 ∈ { 3 , 4 , 5 } ) )
26 24 25 mpbir ⊢ 5 ∈ ( { 0 , 1 , 2 } ∪ { 3 , 4 , 5 } )
27 tpssi ⊢ ( ( 1 ∈ ( { 0 , 1 , 2 } ∪ { 3 , 4 , 5 } ) ∧ 3 ∈ ( { 0 , 1 , 2 } ∪ { 3 , 4 , 5 } ) ∧ 5 ∈ ( { 0 , 1 , 2 } ∪ { 3 , 4 , 5 } ) ) → { 1 , 3 , 5 } ⊆ ( { 0 , 1 , 2 } ∪ { 3 , 4 , 5 } ) )
28 3orcoma ⊢ ( ( 𝑛 = 3 ∨ 𝑛 = 1 ∨ 𝑛 = 5 ) ↔ ( 𝑛 = 1 ∨ 𝑛 = 3 ∨ 𝑛 = 5 ) )
29 3orass ⊢ ( ( 𝑛 = 3 ∨ 𝑛 = 1 ∨ 𝑛 = 5 ) ↔ ( 𝑛 = 3 ∨ ( 𝑛 = 1 ∨ 𝑛 = 5 ) ) )
30 28 29 bitr3i ⊢ ( ( 𝑛 = 1 ∨ 𝑛 = 3 ∨ 𝑛 = 5 ) ↔ ( 𝑛 = 3 ∨ ( 𝑛 = 1 ∨ 𝑛 = 5 ) ) )
31 vex ⊢ 𝑛 ∈ V
32 31 eltp ⊢ ( 𝑛 ∈ { 1 , 3 , 5 } ↔ ( 𝑛 = 1 ∨ 𝑛 = 3 ∨ 𝑛 = 5 ) )
33 prex ⊢ { 0 , 𝑛 } ∈ V
34 el7g ⊢ ( { 0 , 𝑛 } ∈ V → ( { 0 , 𝑛 } ∈ ( { { 0 , 3 } } ∪ ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } ∪ { { 3 , 4 } , { 4 , 5 } , { 0 , 5 } } ) ) ↔ ( { 0 , 𝑛 } = { 0 , 3 } ∨ ( ( { 0 , 𝑛 } = { 0 , 1 } ∨ { 0 , 𝑛 } = { 1 , 2 } ∨ { 0 , 𝑛 } = { 2 , 3 } ) ∨ ( { 0 , 𝑛 } = { 3 , 4 } ∨ { 0 , 𝑛 } = { 4 , 5 } ∨ { 0 , 𝑛 } = { 0 , 5 } ) ) ) ) )
35 33 34 ax-mp ⊢ ( { 0 , 𝑛 } ∈ ( { { 0 , 3 } } ∪ ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } ∪ { { 3 , 4 } , { 4 , 5 } , { 0 , 5 } } ) ) ↔ ( { 0 , 𝑛 } = { 0 , 3 } ∨ ( ( { 0 , 𝑛 } = { 0 , 1 } ∨ { 0 , 𝑛 } = { 1 , 2 } ∨ { 0 , 𝑛 } = { 2 , 3 } ) ∨ ( { 0 , 𝑛 } = { 3 , 4 } ∨ { 0 , 𝑛 } = { 4 , 5 } ∨ { 0 , 𝑛 } = { 0 , 5 } ) ) ) )
36 31 a1i ⊢ ( 3 ∈ V → 𝑛 ∈ V )
37 elex ⊢ ( 3 ∈ V → 3 ∈ V )
38 36 37 preq2b ⊢ ( 3 ∈ V → ( { 0 , 𝑛 } = { 0 , 3 } ↔ 𝑛 = 3 ) )
39 16 38 ax-mp ⊢ ( { 0 , 𝑛 } = { 0 , 3 } ↔ 𝑛 = 3 )
40 3orrot ⊢ ( ( { 0 , 𝑛 } = { 0 , 1 } ∨ { 0 , 𝑛 } = { 1 , 2 } ∨ { 0 , 𝑛 } = { 2 , 3 } ) ↔ ( { 0 , 𝑛 } = { 1 , 2 } ∨ { 0 , 𝑛 } = { 2 , 3 } ∨ { 0 , 𝑛 } = { 0 , 1 } ) )
41 4 31 pm3.2i ⊢ ( 0 ∈ V ∧ 𝑛 ∈ V )
42 2ex ⊢ 2 ∈ V
43 11 42 pm3.2i ⊢ ( 1 ∈ V ∧ 2 ∈ V )
44 41 43 pm3.2i ⊢ ( ( 0 ∈ V ∧ 𝑛 ∈ V ) ∧ ( 1 ∈ V ∧ 2 ∈ V ) )
45 0ne1 ⊢ 0 ≠ 1
46 0ne2 ⊢ 0 ≠ 2
47 45 46 pm3.2i ⊢ ( 0 ≠ 1 ∧ 0 ≠ 2 )
48 47 orci ⊢ ( ( 0 ≠ 1 ∧ 0 ≠ 2 ) ∨ ( 𝑛 ≠ 1 ∧ 𝑛 ≠ 2 ) )
49 prneimg ⊢ ( ( ( 0 ∈ V ∧ 𝑛 ∈ V ) ∧ ( 1 ∈ V ∧ 2 ∈ V ) ) → ( ( ( 0 ≠ 1 ∧ 0 ≠ 2 ) ∨ ( 𝑛 ≠ 1 ∧ 𝑛 ≠ 2 ) ) → { 0 , 𝑛 } ≠ { 1 , 2 } ) )
50 44 48 49 mp2 ⊢ { 0 , 𝑛 } ≠ { 1 , 2 }
51 50 neii ⊢ ¬ { 0 , 𝑛 } = { 1 , 2 }
52 id ⊢ ( ¬ { 0 , 𝑛 } = { 1 , 2 } → ¬ { 0 , 𝑛 } = { 1 , 2 } )
53 42 16 pm3.2i ⊢ ( 2 ∈ V ∧ 3 ∈ V )
54 41 53 pm3.2i ⊢ ( ( 0 ∈ V ∧ 𝑛 ∈ V ) ∧ ( 2 ∈ V ∧ 3 ∈ V ) )
55 0re ⊢ 0 ∈ ℝ
56 3pos ⊢ 0 < 3
57 55 56 ltneii ⊢ 0 ≠ 3
58 46 57 pm3.2i ⊢ ( 0 ≠ 2 ∧ 0 ≠ 3 )
59 58 orci ⊢ ( ( 0 ≠ 2 ∧ 0 ≠ 3 ) ∨ ( 𝑛 ≠ 2 ∧ 𝑛 ≠ 3 ) )
60 prneimg ⊢ ( ( ( 0 ∈ V ∧ 𝑛 ∈ V ) ∧ ( 2 ∈ V ∧ 3 ∈ V ) ) → ( ( ( 0 ≠ 2 ∧ 0 ≠ 3 ) ∨ ( 𝑛 ≠ 2 ∧ 𝑛 ≠ 3 ) ) → { 0 , 𝑛 } ≠ { 2 , 3 } ) )
61 54 59 60 mp2 ⊢ { 0 , 𝑛 } ≠ { 2 , 3 }
62 61 neii ⊢ ¬ { 0 , 𝑛 } = { 2 , 3 }
63 62 a1i ⊢ ( ¬ { 0 , 𝑛 } = { 1 , 2 } → ¬ { 0 , 𝑛 } = { 2 , 3 } )
64 52 63 3bior2fd ⊢ ( ¬ { 0 , 𝑛 } = { 1 , 2 } → ( { 0 , 𝑛 } = { 0 , 1 } ↔ ( { 0 , 𝑛 } = { 1 , 2 } ∨ { 0 , 𝑛 } = { 2 , 3 } ∨ { 0 , 𝑛 } = { 0 , 1 } ) ) )
65 51 64 ax-mp ⊢ ( { 0 , 𝑛 } = { 0 , 1 } ↔ ( { 0 , 𝑛 } = { 1 , 2 } ∨ { 0 , 𝑛 } = { 2 , 3 } ∨ { 0 , 𝑛 } = { 0 , 1 } ) )
66 31 a1i ⊢ ( 1 ∈ V → 𝑛 ∈ V )
67 elex ⊢ ( 1 ∈ V → 1 ∈ V )
68 66 67 preq2b ⊢ ( 1 ∈ V → ( { 0 , 𝑛 } = { 0 , 1 } ↔ 𝑛 = 1 ) )
69 11 68 ax-mp ⊢ ( { 0 , 𝑛 } = { 0 , 1 } ↔ 𝑛 = 1 )
70 65 69 bitr3i ⊢ ( ( { 0 , 𝑛 } = { 1 , 2 } ∨ { 0 , 𝑛 } = { 2 , 3 } ∨ { 0 , 𝑛 } = { 0 , 1 } ) ↔ 𝑛 = 1 )
71 40 70 bitri ⊢ ( ( { 0 , 𝑛 } = { 0 , 1 } ∨ { 0 , 𝑛 } = { 1 , 2 } ∨ { 0 , 𝑛 } = { 2 , 3 } ) ↔ 𝑛 = 1 )
72 4nn0 ⊢ 4 ∈ ℕ0
73 16 72 pm3.2i ⊢ ( 3 ∈ V ∧ 4 ∈ ℕ0 )
74 41 73 pm3.2i ⊢ ( ( 0 ∈ V ∧ 𝑛 ∈ V ) ∧ ( 3 ∈ V ∧ 4 ∈ ℕ0 ) )
75 4pos ⊢ 0 < 4
76 55 75 ltneii ⊢ 0 ≠ 4
77 57 76 pm3.2i ⊢ ( 0 ≠ 3 ∧ 0 ≠ 4 )
78 77 orci ⊢ ( ( 0 ≠ 3 ∧ 0 ≠ 4 ) ∨ ( 𝑛 ≠ 3 ∧ 𝑛 ≠ 4 ) )
79 prneimg ⊢ ( ( ( 0 ∈ V ∧ 𝑛 ∈ V ) ∧ ( 3 ∈ V ∧ 4 ∈ ℕ0 ) ) → ( ( ( 0 ≠ 3 ∧ 0 ≠ 4 ) ∨ ( 𝑛 ≠ 3 ∧ 𝑛 ≠ 4 ) ) → { 0 , 𝑛 } ≠ { 3 , 4 } ) )
80 74 78 79 mp2 ⊢ { 0 , 𝑛 } ≠ { 3 , 4 }
81 80 neii ⊢ ¬ { 0 , 𝑛 } = { 3 , 4 }
82 id ⊢ ( ¬ { 0 , 𝑛 } = { 3 , 4 } → ¬ { 0 , 𝑛 } = { 3 , 4 } )
83 72 21 pm3.2i ⊢ ( 4 ∈ ℕ0 ∧ 5 ∈ ℕ0 )
84 41 83 pm3.2i ⊢ ( ( 0 ∈ V ∧ 𝑛 ∈ V ) ∧ ( 4 ∈ ℕ0 ∧ 5 ∈ ℕ0 ) )
85 5pos ⊢ 0 < 5
86 55 85 ltneii ⊢ 0 ≠ 5
87 76 86 pm3.2i ⊢ ( 0 ≠ 4 ∧ 0 ≠ 5 )
88 87 orci ⊢ ( ( 0 ≠ 4 ∧ 0 ≠ 5 ) ∨ ( 𝑛 ≠ 4 ∧ 𝑛 ≠ 5 ) )
89 prneimg ⊢ ( ( ( 0 ∈ V ∧ 𝑛 ∈ V ) ∧ ( 4 ∈ ℕ0 ∧ 5 ∈ ℕ0 ) ) → ( ( ( 0 ≠ 4 ∧ 0 ≠ 5 ) ∨ ( 𝑛 ≠ 4 ∧ 𝑛 ≠ 5 ) ) → { 0 , 𝑛 } ≠ { 4 , 5 } ) )
90 84 88 89 mp2 ⊢ { 0 , 𝑛 } ≠ { 4 , 5 }
91 90 neii ⊢ ¬ { 0 , 𝑛 } = { 4 , 5 }
92 91 a1i ⊢ ( ¬ { 0 , 𝑛 } = { 3 , 4 } → ¬ { 0 , 𝑛 } = { 4 , 5 } )
93 82 92 3bior2fd ⊢ ( ¬ { 0 , 𝑛 } = { 3 , 4 } → ( { 0 , 𝑛 } = { 0 , 5 } ↔ ( { 0 , 𝑛 } = { 3 , 4 } ∨ { 0 , 𝑛 } = { 4 , 5 } ∨ { 0 , 𝑛 } = { 0 , 5 } ) ) )
94 81 93 ax-mp ⊢ ( { 0 , 𝑛 } = { 0 , 5 } ↔ ( { 0 , 𝑛 } = { 3 , 4 } ∨ { 0 , 𝑛 } = { 4 , 5 } ∨ { 0 , 𝑛 } = { 0 , 5 } ) )
95 31 a1i ⊢ ( 5 ∈ ℕ0 → 𝑛 ∈ V )
96 elex ⊢ ( 5 ∈ ℕ0 → 5 ∈ V )
97 95 96 preq2b ⊢ ( 5 ∈ ℕ0 → ( { 0 , 𝑛 } = { 0 , 5 } ↔ 𝑛 = 5 ) )
98 21 97 ax-mp ⊢ ( { 0 , 𝑛 } = { 0 , 5 } ↔ 𝑛 = 5 )
99 94 98 bitr3i ⊢ ( ( { 0 , 𝑛 } = { 3 , 4 } ∨ { 0 , 𝑛 } = { 4 , 5 } ∨ { 0 , 𝑛 } = { 0 , 5 } ) ↔ 𝑛 = 5 )
100 71 99 orbi12i ⊢ ( ( ( { 0 , 𝑛 } = { 0 , 1 } ∨ { 0 , 𝑛 } = { 1 , 2 } ∨ { 0 , 𝑛 } = { 2 , 3 } ) ∨ ( { 0 , 𝑛 } = { 3 , 4 } ∨ { 0 , 𝑛 } = { 4 , 5 } ∨ { 0 , 𝑛 } = { 0 , 5 } ) ) ↔ ( 𝑛 = 1 ∨ 𝑛 = 5 ) )
101 39 100 orbi12i ⊢ ( ( { 0 , 𝑛 } = { 0 , 3 } ∨ ( ( { 0 , 𝑛 } = { 0 , 1 } ∨ { 0 , 𝑛 } = { 1 , 2 } ∨ { 0 , 𝑛 } = { 2 , 3 } ) ∨ ( { 0 , 𝑛 } = { 3 , 4 } ∨ { 0 , 𝑛 } = { 4 , 5 } ∨ { 0 , 𝑛 } = { 0 , 5 } ) ) ) ↔ ( 𝑛 = 3 ∨ ( 𝑛 = 1 ∨ 𝑛 = 5 ) ) )
102 35 101 bitri ⊢ ( { 0 , 𝑛 } ∈ ( { { 0 , 3 } } ∪ ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } ∪ { { 3 , 4 } , { 4 , 5 } , { 0 , 5 } } ) ) ↔ ( 𝑛 = 3 ∨ ( 𝑛 = 1 ∨ 𝑛 = 5 ) ) )
103 30 32 102 3bitr4i ⊢ ( 𝑛 ∈ { 1 , 3 , 5 } ↔ { 0 , 𝑛 } ∈ ( { { 0 , 3 } } ∪ ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } ∪ { { 3 , 4 } , { 4 , 5 } , { 0 , 5 } } ) ) )
104 103 a1i ⊢ ( ( ( 1 ∈ ( { 0 , 1 , 2 } ∪ { 3 , 4 , 5 } ) ∧ 3 ∈ ( { 0 , 1 , 2 } ∪ { 3 , 4 , 5 } ) ∧ 5 ∈ ( { 0 , 1 , 2 } ∪ { 3 , 4 , 5 } ) ) ∧ 𝑛 ∈ ( { 0 , 1 , 2 } ∪ { 3 , 4 , 5 } ) ) → ( 𝑛 ∈ { 1 , 3 , 5 } ↔ { 0 , 𝑛 } ∈ ( { { 0 , 3 } } ∪ ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } ∪ { { 3 , 4 } , { 4 , 5 } , { 0 , 5 } } ) ) ) )
105 27 104 eqrrabd ⊢ ( ( 1 ∈ ( { 0 , 1 , 2 } ∪ { 3 , 4 , 5 } ) ∧ 3 ∈ ( { 0 , 1 , 2 } ∪ { 3 , 4 , 5 } ) ∧ 5 ∈ ( { 0 , 1 , 2 } ∪ { 3 , 4 , 5 } ) ) → { 1 , 3 , 5 } = { 𝑛 ∈ ( { 0 , 1 , 2 } ∪ { 3 , 4 , 5 } ) ∣ { 0 , 𝑛 } ∈ ( { { 0 , 3 } } ∪ ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } ∪ { { 3 , 4 } , { 4 , 5 } , { 0 , 5 } } ) ) } )
106 15 20 26 105 mp3an ⊢ { 1 , 3 , 5 } = { 𝑛 ∈ ( { 0 , 1 , 2 } ∪ { 3 , 4 , 5 } ) ∣ { 0 , 𝑛 } ∈ ( { { 0 , 3 } } ∪ ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } ∪ { { 3 , 4 } , { 4 , 5 } , { 0 , 5 } } ) ) }
107 10 106 eqtr4i ⊢ ( 𝐺 NeighbVtx 0 ) = { 1 , 3 , 5 }