Metamath Proof Explorer

Theorem usgrexmpllem

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

Ref Expression
Hypotheses usgrexmpl.v ⊢ V = 0 … 4
usgrexmpl.e ⊢ E = ⟨“ 0 1 1 2 2 0 0 3 ”⟩
usgrexmpl.g ⊢ G = V E
Assertion usgrexmpllem ⊢ Vtx ⁡ G = V ∧ iEdg ⁡ G = E

Proof

Step Hyp Ref Expression
1 usgrexmpl.v ⊢ V = 0 … 4
2 usgrexmpl.e ⊢ E = ⟨“ 0 1 1 2 2 0 0 3 ”⟩
3 usgrexmpl.g ⊢ G = V E
4 1 ovexi ⊢ V ∈ 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 ⊢ E ∈ V
8 opvtxfv ⊢ V ∈ V ∧ E ∈ V → Vtx ⁡ V E = V
9 opiedgfv ⊢ V ∈ V ∧ E ∈ V → iEdg ⁡ V E = E
10 8 9 jca ⊢ V ∈ V ∧ E ∈ V → Vtx ⁡ V E = V ∧ iEdg ⁡ V E = E
11 4 7 10 mp2an ⊢ Vtx ⁡ V E = V ∧ iEdg ⁡ V E = E
12 3 fveq2i ⊢ Vtx ⁡ G = Vtx ⁡ V E
13 12 eqeq1i ⊢ Vtx ⁡ G = V ↔ Vtx ⁡ V E = V
14 3 fveq2i ⊢ iEdg ⁡ G = iEdg ⁡ V E
15 14 eqeq1i ⊢ iEdg ⁡ G = E ↔ iEdg ⁡ V E = E
16 13 15 anbi12i ⊢ Vtx ⁡ G = V ∧ iEdg ⁡ G = E ↔ Vtx ⁡ V E = V ∧ iEdg ⁡ V E = E
17 11 16 mpbir ⊢ Vtx ⁡ G = V ∧ iEdg ⁡ G = E