1hevtxdg1

Description: The vertex degree of vertex D in a graph G with only one hyperedge E (not being a loop) is 1 if D is incident with the edge E . (Contributed by AV, 2-Mar-2021) (Proof shortened by AV, 17-Apr-2021)

	Ref	Expression
Hypotheses	1hevtxdg0.i	$⊢ φ \to iEdg (G) = \{⟨A, E⟩\}$
	1hevtxdg0.v	$⊢ φ \to Vtx (G) = V$
	1hevtxdg0.a	$⊢ φ \to A \in X$
	1hevtxdg0.d	$⊢ φ \to D \in V$
	1hevtxdg1.e	$⊢ φ \to E \in 𝒫 V$
	1hevtxdg1.n	$⊢ φ \to D \in E$
	1hevtxdg1.l	$⊢ φ \to 2 \leq \|E\|$
Assertion	1hevtxdg1	$⊢ φ \to VtxDeg (G) (D) = 1$

Proof

Step	Hyp	Ref	Expression
1		1hevtxdg0.i	$⊢ φ \to iEdg (G) = \{⟨A, E⟩\}$
2		1hevtxdg0.v	$⊢ φ \to Vtx (G) = V$
3		1hevtxdg0.a	$⊢ φ \to A \in X$
4		1hevtxdg0.d	$⊢ φ \to D \in V$
5		1hevtxdg1.e	$⊢ φ \to E \in 𝒫 V$
6		1hevtxdg1.n	$⊢ φ \to D \in E$
7		1hevtxdg1.l	$⊢ φ \to 2 \leq \|E\|$
8	1	dmeqd	$⊢ φ \to dom iEdg (G) = dom \{⟨A, E⟩\}$
9		dmsnopg	$⊢ E \in 𝒫 V \to dom \{⟨A, E⟩\} = \{A\}$
10	5 9	syl	$⊢ φ \to dom \{⟨A, E⟩\} = \{A\}$
11	8 10	eqtrd	$⊢ φ \to dom iEdg (G) = \{A\}$
12		fveq2	$⊢ x = E \to \|x\| = \|E\|$
13	12	breq2d	$⊢ x = E \to (2 \leq \|x\| \leftrightarrow 2 \leq \|E\|)$
14	2	pweqd	$⊢ φ \to 𝒫 Vtx (G) = 𝒫 V$
15	5 14	eleqtrrd	$⊢ φ \to E \in 𝒫 Vtx (G)$
16	13 15 7	elrabd	$⊢ φ \to E \in \{x \in 𝒫 Vtx (G) \| 2 \leq \|x\|\}$
17	3 16	fsnd	$⊢ φ \to \{⟨A, E⟩\} : \{A\} ⟶ \{x \in 𝒫 Vtx (G) \| 2 \leq \|x\|\}$
18	17	adantr	$⊢ (φ \land dom iEdg (G) = \{A\}) \to \{⟨A, E⟩\} : \{A\} ⟶ \{x \in 𝒫 Vtx (G) \| 2 \leq \|x\|\}$
19	1	adantr	$⊢ (φ \land dom iEdg (G) = \{A\}) \to iEdg (G) = \{⟨A, E⟩\}$
20		simpr	$⊢ (φ \land dom iEdg (G) = \{A\}) \to dom iEdg (G) = \{A\}$
21	19 20	feq12d	$⊢ (φ \land dom iEdg (G) = \{A\}) \to (iEdg (G) : dom iEdg (G) ⟶ \{x \in 𝒫 Vtx (G) \| 2 \leq \|x\|\} \leftrightarrow \{⟨A, E⟩\} : \{A\} ⟶ \{x \in 𝒫 Vtx (G) \| 2 \leq \|x\|\})$
22	18 21	mpbird	$⊢ (φ \land dom iEdg (G) = \{A\}) \to iEdg (G) : dom iEdg (G) ⟶ \{x \in 𝒫 Vtx (G) \| 2 \leq \|x\|\}$
23	4 2	eleqtrrd	$⊢ φ \to D \in Vtx (G)$
24	23	adantr	$⊢ (φ \land dom iEdg (G) = \{A\}) \to D \in Vtx (G)$
25		eqid	$⊢ Vtx (G) = Vtx (G)$
26		eqid	$⊢ iEdg (G) = iEdg (G)$
27		eqid	$⊢ dom iEdg (G) = dom iEdg (G)$
28		eqid	$⊢ VtxDeg (G) = VtxDeg (G)$
29	25 26 27 28	vtxdlfgrval	$⊢ (iEdg (G) : dom iEdg (G) ⟶ \{x \in 𝒫 Vtx (G) \| 2 \leq \|x\|\} \land D \in Vtx (G)) \to VtxDeg (G) (D) = \|\{x \in dom iEdg (G) \| D \in iEdg (G) (x)\}\|$
30	22 24 29	syl2anc	$⊢ (φ \land dom iEdg (G) = \{A\}) \to VtxDeg (G) (D) = \|\{x \in dom iEdg (G) \| D \in iEdg (G) (x)\}\|$
31		rabeq	$⊢ dom iEdg (G) = \{A\} \to \{x \in dom iEdg (G) \| D \in iEdg (G) (x)\} = \{x \in \{A\} \| D \in iEdg (G) (x)\}$
32	31	adantl	$⊢ (φ \land dom iEdg (G) = \{A\}) \to \{x \in dom iEdg (G) \| D \in iEdg (G) (x)\} = \{x \in \{A\} \| D \in iEdg (G) (x)\}$
33	32	fveq2d	$⊢ (φ \land dom iEdg (G) = \{A\}) \to \|\{x \in dom iEdg (G) \| D \in iEdg (G) (x)\}\| = \|\{x \in \{A\} \| D \in iEdg (G) (x)\}\|$
34		fveq2	$⊢ x = A \to iEdg (G) (x) = iEdg (G) (A)$
35	34	eleq2d	$⊢ x = A \to (D \in iEdg (G) (x) \leftrightarrow D \in iEdg (G) (A))$
36	35	rabsnif	$⊢ \{x \in \{A\} \| D \in iEdg (G) (x)\} = if (D \in iEdg (G) (A), \{A\}, \emptyset)$
37	1	fveq1d	$⊢ φ \to iEdg (G) (A) = \{⟨A, E⟩\} (A)$
38		fvsng	$⊢ (A \in X \land E \in 𝒫 V) \to \{⟨A, E⟩\} (A) = E$
39	3 5 38	syl2anc	$⊢ φ \to \{⟨A, E⟩\} (A) = E$
40	37 39	eqtrd	$⊢ φ \to iEdg (G) (A) = E$
41	6 40	eleqtrrd	$⊢ φ \to D \in iEdg (G) (A)$
42	41	iftrued	$⊢ φ \to if (D \in iEdg (G) (A), \{A\}, \emptyset) = \{A\}$
43	36 42	eqtrid	$⊢ φ \to \{x \in \{A\} \| D \in iEdg (G) (x)\} = \{A\}$
44	43	fveq2d	$⊢ φ \to \|\{x \in \{A\} \| D \in iEdg (G) (x)\}\| = \|\{A\}\|$
45		hashsng	$⊢ A \in X \to \|\{A\}\| = 1$
46	3 45	syl	$⊢ φ \to \|\{A\}\| = 1$
47	44 46	eqtrd	$⊢ φ \to \|\{x \in \{A\} \| D \in iEdg (G) (x)\}\| = 1$
48	47	adantr	$⊢ (φ \land dom iEdg (G) = \{A\}) \to \|\{x \in \{A\} \| D \in iEdg (G) (x)\}\| = 1$
49	30 33 48	3eqtrd	$⊢ (φ \land dom iEdg (G) = \{A\}) \to VtxDeg (G) (D) = 1$
50	11 49	mpdan	$⊢ φ \to VtxDeg (G) (D) = 1$

Metamath Proof Explorer

Theorem 1hevtxdg1

Proof