This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )