Metamath Proof Explorer

Theorem usgrexmpl2nb5

Description: The neighborhood of the sixth vertex of graph G . (Contributed by AV, 10-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 usgrexmpl2nb5 ( 𝐺 NeighbVtx 5 ) = { 0 , 4 }

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