lpvtx

Description: The endpoints of a loop (which is an edge at index J ) are two (identical) vertices A . (Contributed by AV, 1-Feb-2021)

		Ref	Expression
	Hypothesis	lpvtx.i	$⊢ I = iEdg (G)$
	Assertion	lpvtx	$⊢ (G \in UHGraph \land J \in dom I \land I (J) = \{A\}) \to A \in Vtx (G)$

Proof

Step	Hyp	Ref	Expression
1		lpvtx.i	$⊢ I = iEdg (G)$
2		simp1	$⊢ (G \in UHGraph \land J \in dom I \land I (J) = \{A\}) \to G \in UHGraph$
3	1	uhgrfun	$⊢ G \in UHGraph \to Fun I$
4	3	funfnd	$⊢ G \in UHGraph \to I Fn dom I$
5	4	3ad2ant1	$⊢ (G \in UHGraph \land J \in dom I \land I (J) = \{A\}) \to I Fn dom I$
6		simp2	$⊢ (G \in UHGraph \land J \in dom I \land I (J) = \{A\}) \to J \in dom I$
7	1	uhgrn0	$⊢ (G \in UHGraph \land I Fn dom I \land J \in dom I) \to I (J) \neq \emptyset$
8	2 5 6 7	syl3anc	$⊢ (G \in UHGraph \land J \in dom I \land I (J) = \{A\}) \to I (J) \neq \emptyset$
9		neeq1	$⊢ I (J) = \{A\} \to (I (J) \neq \emptyset \leftrightarrow \{A\} \neq \emptyset)$
10	9	biimpd	$⊢ I (J) = \{A\} \to (I (J) \neq \emptyset \to \{A\} \neq \emptyset)$
11	10	3ad2ant3	$⊢ (G \in UHGraph \land J \in dom I \land I (J) = \{A\}) \to (I (J) \neq \emptyset \to \{A\} \neq \emptyset)$
12	8 11	mpd	$⊢ (G \in UHGraph \land J \in dom I \land I (J) = \{A\}) \to \{A\} \neq \emptyset$
13		eqid	$⊢ Vtx (G) = Vtx (G)$
14	13 1	uhgrss	$⊢ (G \in UHGraph \land J \in dom I) \to I (J) \subseteq Vtx (G)$
15	14	3adant3	$⊢ (G \in UHGraph \land J \in dom I \land I (J) = \{A\}) \to I (J) \subseteq Vtx (G)$
16		sseq1	$⊢ I (J) = \{A\} \to (I (J) \subseteq Vtx (G) \leftrightarrow \{A\} \subseteq Vtx (G))$
17	16	3ad2ant3	$⊢ (G \in UHGraph \land J \in dom I \land I (J) = \{A\}) \to (I (J) \subseteq Vtx (G) \leftrightarrow \{A\} \subseteq Vtx (G))$
18	15 17	mpbid	$⊢ (G \in UHGraph \land J \in dom I \land I (J) = \{A\}) \to \{A\} \subseteq Vtx (G)$
19		snnzb	$⊢ A \in V \leftrightarrow \{A\} \neq \emptyset$
20		snssg	$⊢ A \in V \to (A \in Vtx (G) \leftrightarrow \{A\} \subseteq Vtx (G))$
21	19 20	sylbir	$⊢ \{A\} \neq \emptyset \to (A \in Vtx (G) \leftrightarrow \{A\} \subseteq Vtx (G))$
22	18 21	syl5ibrcom	$⊢ (G \in UHGraph \land J \in dom I \land I (J) = \{A\}) \to (\{A\} \neq \emptyset \to A \in Vtx (G))$
23	12 22	mpd	$⊢ (G \in UHGraph \land J \in dom I \land I (J) = \{A\}) \to A \in Vtx (G)$

Metamath Proof Explorer

Theorem lpvtx

Proof