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