Metamath Proof Explorer


Theorem upgrres1lem1

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 )