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 ‘ 𝐺 ) = 𝐸 )