Metamath Proof Explorer
Description: Lemma 1 for upgrres1 . (Contributed by AV, 7-Nov-2020)
|
|
Ref |
Expression |
|
Hypotheses |
upgrres1.v |
⊢ 𝑉 = ( Vtx ‘ 𝐺 ) |
|
|
upgrres1.e |
⊢ 𝐸 = ( Edg ‘ 𝐺 ) |
|
|
upgrres1.f |
⊢ 𝐹 = { 𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒 } |
|
Assertion |
upgrres1lem1 |
⊢ ( ( 𝑉 ∖ { 𝑁 } ) ∈ V ∧ ( I ↾ 𝐹 ) ∈ V ) |
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
upgrres1.v |
⊢ 𝑉 = ( Vtx ‘ 𝐺 ) |
2 |
|
upgrres1.e |
⊢ 𝐸 = ( Edg ‘ 𝐺 ) |
3 |
|
upgrres1.f |
⊢ 𝐹 = { 𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒 } |
4 |
1
|
fvexi |
⊢ 𝑉 ∈ V |
5 |
4
|
difexi |
⊢ ( 𝑉 ∖ { 𝑁 } ) ∈ V |
6 |
2
|
fvexi |
⊢ 𝐸 ∈ V |
7 |
3 6
|
rabex2 |
⊢ 𝐹 ∈ V |
8 |
|
resiexg |
⊢ ( 𝐹 ∈ V → ( I ↾ 𝐹 ) ∈ V ) |
9 |
7 8
|
ax-mp |
⊢ ( I ↾ 𝐹 ) ∈ V |
10 |
5 9
|
pm3.2i |
⊢ ( ( 𝑉 ∖ { 𝑁 } ) ∈ V ∧ ( I ↾ 𝐹 ) ∈ V ) |