subumgredg2

Description: An edge of a subgraph of a multigraph connects exactly two different vertices. (Contributed by AV, 26-Nov-2020)

	Ref	Expression
Hypotheses	subumgredg2.v	$⊢ V = Vtx (S)$
	subumgredg2.i	$⊢ I = iEdg (S)$
Assertion	subumgredg2	$⊢ (S SubGraph G \land G \in UMGraph \land X \in dom I) \to I (X) \in \{e \in 𝒫 V \| \|e\| = 2\}$

Proof

Step	Hyp	Ref	Expression
1		subumgredg2.v	$⊢ V = Vtx (S)$
2		subumgredg2.i	$⊢ I = iEdg (S)$
3		fveqeq2	$⊢ e = I (X) \to (\|e\| = 2 \leftrightarrow \|I (X)\| = 2)$
4		umgruhgr	$⊢ G \in UMGraph \to G \in UHGraph$
5	4	3ad2ant2	$⊢ (S SubGraph G \land G \in UMGraph \land X \in dom I) \to G \in UHGraph$
6		simp1	$⊢ (S SubGraph G \land G \in UMGraph \land X \in dom I) \to S SubGraph G$
7		simp3	$⊢ (S SubGraph G \land G \in UMGraph \land X \in dom I) \to X \in dom I$
8	1 2 5 6 7	subgruhgredgd	$⊢ (S SubGraph G \land G \in UMGraph \land X \in dom I) \to I (X) \in (𝒫 V ∖ \{\emptyset\})$
9		eqid	$⊢ iEdg (G) = iEdg (G)$
10	9	uhgrfun	$⊢ G \in UHGraph \to Fun iEdg (G)$
11	4 10	syl	$⊢ G \in UMGraph \to Fun iEdg (G)$
12	11	3ad2ant2	$⊢ (S SubGraph G \land G \in UMGraph \land X \in dom I) \to Fun iEdg (G)$
13		eqid	$⊢ Vtx (S) = Vtx (S)$
14		eqid	$⊢ Vtx (G) = Vtx (G)$
15		eqid	$⊢ Edg (S) = Edg (S)$
16	13 14 2 9 15	subgrprop2	$⊢ S SubGraph G \to (Vtx (S) \subseteq Vtx (G) \land I \subseteq iEdg (G) \land Edg (S) \subseteq 𝒫 Vtx (S))$
17	16	simp2d	$⊢ S SubGraph G \to I \subseteq iEdg (G)$
18	17	3ad2ant1	$⊢ (S SubGraph G \land G \in UMGraph \land X \in dom I) \to I \subseteq iEdg (G)$
19		funssfv	$⊢ (Fun iEdg (G) \land I \subseteq iEdg (G) \land X \in dom I) \to iEdg (G) (X) = I (X)$
20	19	eqcomd	$⊢ (Fun iEdg (G) \land I \subseteq iEdg (G) \land X \in dom I) \to I (X) = iEdg (G) (X)$
21	12 18 7 20	syl3anc	$⊢ (S SubGraph G \land G \in UMGraph \land X \in dom I) \to I (X) = iEdg (G) (X)$
22	21	fveq2d	$⊢ (S SubGraph G \land G \in UMGraph \land X \in dom I) \to \|I (X)\| = \|iEdg (G) (X)\|$
23		simp2	$⊢ (S SubGraph G \land G \in UMGraph \land X \in dom I) \to G \in UMGraph$
24	2	dmeqi	$⊢ dom I = dom iEdg (S)$
25	24	eleq2i	$⊢ X \in dom I \leftrightarrow X \in dom iEdg (S)$
26		subgreldmiedg	$⊢ (S SubGraph G \land X \in dom iEdg (S)) \to X \in dom iEdg (G)$
27	26	ex	$⊢ S SubGraph G \to (X \in dom iEdg (S) \to X \in dom iEdg (G))$
28	25 27	biimtrid	$⊢ S SubGraph G \to (X \in dom I \to X \in dom iEdg (G))$
29	28	a1d	$⊢ S SubGraph G \to (G \in UMGraph \to (X \in dom I \to X \in dom iEdg (G)))$
30	29	3imp	$⊢ (S SubGraph G \land G \in UMGraph \land X \in dom I) \to X \in dom iEdg (G)$
31	14 9	umgredg2	$⊢ (G \in UMGraph \land X \in dom iEdg (G)) \to \|iEdg (G) (X)\| = 2$
32	23 30 31	syl2anc	$⊢ (S SubGraph G \land G \in UMGraph \land X \in dom I) \to \|iEdg (G) (X)\| = 2$
33	22 32	eqtrd	$⊢ (S SubGraph G \land G \in UMGraph \land X \in dom I) \to \|I (X)\| = 2$
34	3 8 33	elrabd	$⊢ (S SubGraph G \land G \in UMGraph \land X \in dom I) \to I (X) \in \{e \in (𝒫 V ∖ \{\emptyset\}) \| \|e\| = 2\}$
35		prprrab	$⊢ \{e \in (𝒫 V ∖ \{\emptyset\}) \| \|e\| = 2\} = \{e \in 𝒫 V \| \|e\| = 2\}$
36	34 35	eleqtrdi	$⊢ (S SubGraph G \land G \in UMGraph \land X \in dom I) \to I (X) \in \{e \in 𝒫 V \| \|e\| = 2\}$

Metamath Proof Explorer

Theorem subumgredg2

Proof