Metamath Proof Explorer

Theorem usgrexmpl2nb3

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