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

Metamath Proof Explorer

Theorem uhgrspan1lem1

Description: Lemma 1 for uhgrspan1 . (Contributed by AV, 19-Nov-2020)

Ref Expression
Hypotheses uhgrspan1.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
uhgrspan1.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
uhgrspan1.f ⊢ 𝐹 = { 𝑖 ∈ dom 𝐼 ∣ 𝑁 ∉ ( 𝐼 ‘ 𝑖 ) }
Assertion uhgrspan1lem1 ( ( 𝑉 ∖ { 𝑁 } ) ∈ V ∧ ( 𝐼 ↾ 𝐹 ) ∈ V )

Proof

Step Hyp Ref Expression
1 uhgrspan1.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 uhgrspan1.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
3 uhgrspan1.f ⊢ 𝐹 = { 𝑖 ∈ dom 𝐼 ∣ 𝑁 ∉ ( 𝐼 ‘ 𝑖 ) }
4 1 fvexi ⊢ 𝑉 ∈ V
5 4 difexi ⊢ ( 𝑉 ∖ { 𝑁 } ) ∈ V
6 2 fvexi ⊢ 𝐼 ∈ V
7 6 resex ⊢ ( 𝐼 ↾ 𝐹 ) ∈ V
8 5 7 pm3.2i ⊢ ( ( 𝑉 ∖ { 𝑁 } ) ∈ V ∧ ( 𝐼 ↾ 𝐹 ) ∈ V )