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

Metamath Proof Explorer

Theorem usgrexmpllem

Description: Lemma for usgrexmpl . (Contributed by AV, 21-Oct-2020)

Ref Expression
Hypotheses usgrexmpl.v ⊢ 𝑉 = ( 0 ... 4 )
usgrexmpl.e ⊢ 𝐸 = ⟨“ { 0 , 1 } { 1 , 2 } { 2 , 0 } { 0 , 3 } ”⟩
usgrexmpl.g ⊢ 𝐺 = ⟨ 𝑉 , 𝐸 ⟩
Assertion usgrexmpllem ( ( Vtx ‘ 𝐺 ) = 𝑉 ∧ ( iEdg ‘ 𝐺 ) = 𝐸 )

Proof

Step Hyp Ref Expression
1 usgrexmpl.v ⊢ 𝑉 = ( 0 ... 4 )
2 usgrexmpl.e ⊢ 𝐸 = ⟨“ { 0 , 1 } { 1 , 2 } { 2 , 0 } { 0 , 3 } ”⟩
3 usgrexmpl.g ⊢ 𝐺 = ⟨ 𝑉 , 𝐸 ⟩
4 1 ovexi ⊢ 𝑉 ∈ V
5 s4cli ⊢ ⟨“ { 0 , 1 } { 1 , 2 } { 2 , 0 } { 0 , 3 } ”⟩ ∈ Word V
6 5 elexi ⊢ ⟨“ { 0 , 1 } { 1 , 2 } { 2 , 0 } { 0 , 3 } ”⟩ ∈ V
7 2 6 eqeltri ⊢ 𝐸 ∈ V
8 opvtxfv ⊢ ( ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) → ( Vtx ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = 𝑉 )
9 opiedgfv ⊢ ( ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) → ( iEdg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = 𝐸 )
10 8 9 jca ⊢ ( ( 𝑉 ∈ V ∧ 𝐸 ∈ V ) → ( ( Vtx ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = 𝑉 ∧ ( iEdg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = 𝐸 ) )
11 4 7 10 mp2an ⊢ ( ( Vtx ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = 𝑉 ∧ ( iEdg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = 𝐸 )
12 3 fveq2i ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ ⟨ 𝑉 , 𝐸 ⟩ )
13 12 eqeq1i ⊢ ( ( Vtx ‘ 𝐺 ) = 𝑉 ↔ ( Vtx ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = 𝑉 )
14 3 fveq2i ⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ ⟨ 𝑉 , 𝐸 ⟩ )
15 14 eqeq1i ⊢ ( ( iEdg ‘ 𝐺 ) = 𝐸 ↔ ( iEdg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = 𝐸 )
16 13 15 anbi12i ⊢ ( ( ( Vtx ‘ 𝐺 ) = 𝑉 ∧ ( iEdg ‘ 𝐺 ) = 𝐸 ) ↔ ( ( Vtx ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = 𝑉 ∧ ( iEdg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = 𝐸 ) )
17 11 16 mpbir ⊢ ( ( Vtx ‘ 𝐺 ) = 𝑉 ∧ ( iEdg ‘ 𝐺 ) = 𝐸 )