usgrexmpllem

Step	Hyp	Ref	Expression
1		usgrexmpl.v	$⊢ V = (0 \dots 4)$
2		usgrexmpl.e	$⊢ E = ⟨“ \{0, 1\} \{1, 2\} \{2, 0\} \{0, 3\} ”⟩$
3		usgrexmpl.g	$⊢ G = ⟨V, E⟩$
4	1	ovexi	$⊢ V \in V$
5		s4cli	$⊢ ⟨“ \{0, 1\} \{1, 2\} \{2, 0\} \{0, 3\} ”⟩ \in Word V$
6	5	elexi	$⊢ ⟨“ \{0, 1\} \{1, 2\} \{2, 0\} \{0, 3\} ”⟩ \in V$
7	2 6	eqeltri	$⊢ E \in V$
8		opvtxfv	$⊢ (V \in V \land E \in V) \to Vtx (⟨V, E⟩) = V$
9		opiedgfv	$⊢ (V \in V \land E \in V) \to iEdg (⟨V, E⟩) = E$
10	8 9	jca	$⊢ (V \in V \land E \in V) \to (Vtx (⟨V, E⟩) = V \land iEdg (⟨V, E⟩) = E)$
11	4 7 10	mp2an	$⊢ (Vtx (⟨V, E⟩) = V \land iEdg (⟨V, E⟩) = E)$
12	3	fveq2i	$⊢ Vtx (G) = Vtx (⟨V, E⟩)$
13	12	eqeq1i	$⊢ Vtx (G) = V \leftrightarrow Vtx (⟨V, E⟩) = V$
14	3	fveq2i	$⊢ iEdg (G) = iEdg (⟨V, E⟩)$
15	14	eqeq1i	$⊢ iEdg (G) = E \leftrightarrow iEdg (⟨V, E⟩) = E$
16	13 15	anbi12i	$⊢ (Vtx (G) = V \land iEdg (G) = E) \leftrightarrow (Vtx (⟨V, E⟩) = V \land iEdg (⟨V, E⟩) = E)$
17	11 16	mpbir	$⊢ (Vtx (G) = V \land iEdg (G) = E)$

Metamath Proof Explorer