Metamath Proof Explorer

Theorem usgrexmpl2nb4

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